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