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