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