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