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