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