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