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