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