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