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