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