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