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