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