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