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