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