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