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