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