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