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