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