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