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