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