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