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