c This Formular is generated by mcnf
c
c    horn? no 
c    forced? no 
c    mixed sat? no 
c    clause length = 3 
c
p cnf 100  430 
 58 -61 -2 0
-64 69 -73 0
62 1 46 0
10 45 57 0
71 -98 43 0
37 -32 -1 0
-23 44 -50 0
77 -66 -57 0
64 94 29 0
-43 79 38 0
26 -62 43 0
-7 22 -66 0
-13 93 36 0
-54 -79 14 0
-23 42 1 0
72 -53 -88 0
37 85 9 0
73 54 17 0
28 -77 11 0
-63 82 -51 0
-89 13 30 0
-63 -65 92 0
96 40 87 0
-45 75 85 0
64 78 -25 0
92 30 80 0
29 69 71 0
54 35 77 0
49 92 99 0
77 9 92 0
69 14 -63 0
55 -64 -36 0
63 -38 -10 0
-64 -26 -49 0
-77 36 3 0
-2 -6 -39 0
-32 8 37 0
-42 95 59 0
-9 -97 62 0
-50 36 -57 0
77 -5 -1 0
88 -100 -62 0
46 -8 89 0
40 68 -20 0
-22 73 14 0
-73 1 -21 0
-28 3 -88 0
-84 -72 62 0
95 16 89 0
92 39 85 0
21 -91 10 0
31 -91 -28 0
73 63 26 0
55 29 17 0
55 34 -73 0
-49 60 80 0
84 -32 34 0
-65 -23 76 0
93 -12 -39 0
43 9 -15 0
-5 -97 13 0
-26 38 -45 0
72 14 -18 0
-57 97 85 0
-76 -50 -48 0
-43 -69 92 0
69 78 85 0
-9 -47 -26 0
11 -48 84 0
-81 -3 -71 0
-13 -35 58 0
36 64 89 0
-58 -9 68 0
-82 -74 66 0
-88 59 -21 0
-24 41 22 0
-86 -44 -72 0
-95 50 80 0
81 -14 -17 0
-64 67 -53 0
-72 47 21 0
-2 -13 -72 0
45 82 14 0
-68 -24 59 0
78 33 4 0
11 -89 75 0
61 -84 16 0
96 2 84 0
55 -95 51 0
-51 -56 -52 0
-82 97 58 0
-59 89 -24 0
-76 17 83 0
86 -80 -4 0
55 -44 37 0
75 80 19 0
-73 -94 -35 0
-77 43 -72 0
-69 87 -77 0
-53 -76 12 0
11 -57 89 0
75 -62 -18 0
65 -35 28 0
33 63 15 0
-78 -87 -13 0
-98 86 51 0
10 -89 -2 0
12 -64 -95 0
-67 32 -52 0
18 73 31 0
-5 34 76 0
100 37 -18 0
-37 -99 -72 0
42 -31 -11 0
-42 -89 70 0
-96 -100 -52 0
87 89 -36 0
-80 51 -70 0
11 -67 -99 0
-18 32 -58 0
-5 -99 52 0
-55 -57 29 0
61 -40 93 0
-99 1 -84 0
67 41 6 0
77 -32 -9 0
-69 42 -34 0
40 93 33 0
50 23 24 0
8 86 87 0
23 86 46 0
9 -84 75 0
-36 -21 100 0
91 2 -46 0
61 -43 -51 0
61 78 -47 0
39 -17 44 0
20 -95 -45 0
-42 -54 100 0
52 -29 77 0
63 36 11 0
69 -80 -36 0
-36 12 -90 0
-79 -72 -7 0
-13 10 -4 0
22 -75 -15 0
-52 -51 35 0
-82 -99 -38 0
24 58 -40 0
4 48 8 0
-86 -58 -94 0
-55 41 -28 0
-15 -10 -89 0
-21 5 -26 0
-58 38 9 0
-85 31 -2 0
-55 -85 -33 0
-72 88 70 0
-29 61 -55 0
15 78 -25 0
-67 27 100 0
-61 59 -15 0
53 -12 76 0
72 -100 -77 0
14 -69 73 0
8 58 42 0
-37 -87 5 0
39 -32 57 0
30 -25 -28 0
-2 64 49 0
89 11 98 0
-76 55 -11 0
-25 -44 -21 0
9 -87 99 0
-17 -94 13 0
5 -57 26 0
26 62 97 0
26 67 46 0
20 -56 -90 0
-67 -8 76 0
95 -77 -100 0
-63 5 -48 0
61 66 56 0
-10 31 58 0
-82 -15 56 0
-100 88 -5 0
85 70 87 0
-21 -90 93 0
78 6 -35 0
84 86 -97 0
-68 42 -78 0
-55 -25 -42 0
-77 -72 -62 0
-30 -73 -100 0
-49 63 -78 0
57 -48 45 0
83 -13 -84 0
-94 -46 38 0
21 -27 -78 0
-3 41 18 0
-48 86 -70 0
22 97 71 0
72 -14 -85 0
-14 90 9 0
-46 -12 -42 0
-86 40 -56 0
-13 -53 -66 0
22 29 -100 0
-89 52 -57 0
99 -88 -78 0
-11 -36 9 0
35 -4 93 0
-86 9 79 0
53 4 68 0
-76 100 98 0
23 49 -84 0
-71 50 -78 0
-13 36 -72 0
-8 -73 -90 0
-84 57 90 0
29 -33 -78 0
-88 -35 -42 0
29 12 27 0
-88 -10 -18 0
68 -56 -57 0
-78 -99 -62 0
78 -98 -96 0
-72 7 -13 0
59 19 -77 0
-3 71 -32 0
45 -97 -95 0
-60 66 55 0
-41 -79 -56 0
-12 10 -83 0
-63 48 -55 0
-91 -52 -71 0
-43 -18 24 0
46 -13 -10 0
65 -78 71 0
-31 27 -64 0
59 -10 -22 0
88 37 -96 0
-42 -79 81 0
-13 -44 -24 0
-98 22 14 0
-31 -66 44 0
31 -83 76 0
-94 -36 -87 0
21 -100 10 0
32 79 22 0
79 70 -95 0
61 -53 -73 0
45 73 -2 0
98 68 -89 0
8 -44 -48 0
-58 -68 -57 0
41 -51 32 0
-80 -32 84 0
-70 -61 99 0
-28 75 54 0
63 61 -10 0
98 -53 50 0
39 45 68 0
-53 -96 -91 0
61 -81 33 0
-56 19 96 0
64 -35 60 0
50 2 -70 0
48 76 91 0
96 87 -25 0
-64 57 99 0
67 -86 70 0
51 -49 -35 0
-14 -34 4 0
-48 47 -72 0
-40 5 -51 0
-65 12 -56 0
-40 60 -22 0
-73 -40 -13 0
-24 40 -19 0
-48 -55 -70 0
84 18 8 0
27 47 78 0
28 -79 43 0
12 -79 -74 0
-95 22 -45 0
-60 3 15 0
85 -68 -62 0
-44 52 8 0
94 -84 16 0
-18 -79 50 0
42 1 -61 0
-93 10 49 0
19 -69 -73 0
-68 -46 62 0
88 -86 -98 0
83 10 95 0
-25 -10 -47 0
-95 83 -42 0
46 -76 38 0
27 -46 -92 0
19 65 -69 0
-50 33 -96 0
69 -1 42 0
2 14 -26 0
45 -48 30 0
-96 90 -77 0
50 52 17 0
5 16 -22 0
96 -27 3 0
5 11 72 0
46 43 32 0
6 57 86 0
-44 -6 -49 0
-54 -47 -1 0
-80 73 76 0
94 -53 -65 0
58 80 28 0
77 45 -34 0
-99 64 -32 0
65 -100 -73 0
63 -44 32 0
98 -27 -86 0
-54 -46 32 0
73 -70 5 0
-4 -33 -24 0
-55 -35 -19 0
-92 -60 -13 0
-64 39 -28 0
36 99 68 0
-65 -7 69 0
-64 37 77 0
-69 -14 -98 0
-64 54 21 0
-90 84 45 0
-94 -90 53 0
-4 41 -72 0
18 -92 -8 0
98 36 -52 0
64 -17 84 0
54 69 -97 0
41 35 16 0
6 33 30 0
-12 -45 -38 0
62 25 -82 0
53 -86 -25 0
24 33 91 0
78 -51 -38 0
8 76 -30 0
-11 100 17 0
-48 98 34 0
28 71 59 0
-23 -87 54 0
-45 1 93 0
-66 57 -30 0
-30 -97 72 0
89 -97 -48 0
-37 -86 4 0
41 80 14 0
-81 83 74 0
-92 -28 20 0
-44 93 28 0
42 -11 -45 0
-79 -69 80 0
74 77 97 0
-27 35 65 0
25 23 -31 0
58 71 -67 0
68 -87 25 0
-71 -54 95 0
-13 -16 -37 0
81 22 90 0
67 -95 -89 0
90 65 -83 0
33 -83 17 0
-30 63 21 0
33 21 -39 0
40 98 -70 0
25 21 31 0
-70 -67 -26 0
92 -24 -39 0
-28 22 99 0
42 84 -27 0
79 36 78 0
-52 -13 -79 0
-53 90 -96 0
-69 -30 -7 0
96 37 35 0
-80 27 83 0
69 -88 38 0
19 18 27 0
99 77 -57 0
-57 -40 89 0
38 -42 -64 0
-45 66 -87 0
19 31 -70 0
73 44 -55 0
-81 -6 -38 0
-7 -34 41 0
-70 -98 5 0
-9 99 -48 0
55 17 -37 0
7 -27 -92 0
-44 -3 -22 0
24 -43 -71 0
-45 -8 -49 0
86 40 -10 0
-8 -55 -82 0
87 43 -81 0
-82 -50 -96 0
3 -23 52 0
100 -27 54 0
29 -90 28 0
-69 -47 22 0
46 -96 -55 0
-45 -94 -9 0
-60 -7 6 0
10 9 -3 0
-52 -5 16 0
76 -45 12 0
-88 -13 -95 0
-49 31 -82 0
-69 -22 72 0
-41 -11 12 0
-72 -60 57 0
-85 -77 36 0
55 -21 38 0
-100 44 72 0
-78 55 42 0
-1 -83 -85 0
%
0