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