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