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