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