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