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