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 250  1065 
 128 -13 129 0
-190 79 -246 0
-127 193 -235 0
125 1 114 0
-128 -192 -203 0
132 19 -2 0
112 -223 -63 0
57 38 -126 0
10 -159 232 0
-199 117 -248 0
-142 -174 -157 0
-128 -47 162 0
-123 211 -111 0
-229 -13 54 0
15 -84 -159 0
151 127 125 0
-246 147 106 0
231 -209 -220 0
236 -185 235 0
-83 -159 -204 0
192 -72 65 0
125 231 -230 0
12 -25 -209 0
-89 166 165 0
-210 -219 -238 0
-142 212 241 0
82 -215 55 0
50 8 -146 0
189 198 42 0
137 -36 -71 0
50 127 172 0
-114 -165 -226 0
-39 26 229 0
61 222 37 0
204 211 -147 0
-234 -134 10 0
-167 -37 -8 0
114 -243 9 0
-182 237 14 0
-79 43 -48 0
108 -50 -14 0
-210 121 -223 0
-202 -127 170 0
2 150 -83 0
-102 -196 213 0
30 -29 79 0
-231 106 -153 0
130 -25 42 0
-144 237 160 0
147 103 -223 0
-139 32 173 0
-250 56 -174 0
68 -138 21 0
120 80 -242 0
56 203 96 0
172 -201 -129 0
162 168 9 0
82 -137 154 0
107 -115 -169 0
-90 -200 -177 0
-32 -150 190 0
114 -156 25 0
138 -72 -231 0
130 -30 -91 0
-22 -218 -185 0
-187 185 63 0
234 208 -213 0
102 218 -25 0
-59 -139 228 0
134 -209 -73 0
231 -93 159 0
100 -202 211 0
15 -62 7 0
-238 202 154 0
-70 234 -48 0
116 33 47 0
-27 -176 -218 0
26 3 -238 0
-48 -29 -82 0
41 -63 -166 0
43 70 1 0
105 121 -3 0
-249 -133 244 0
-118 -214 64 0
131 205 121 0
15 -86 -145 0
93 30 -109 0
87 100 99 0
-115 -204 -227 0
237 34 -96 0
182 95 -226 0
-65 203 180 0
-139 -134 -131 0
-1 78 170 0
-118 243 -106 0
102 30 -31 0
-227 170 -93 0
188 -232 -24 0
-35 -219 65 0
-27 62 -64 0
68 -126 192 0
238 180 218 0
-221 24 42 0
232 126 -228 0
-118 -107 234 0
93 -56 134 0
83 -141 16 0
-110 -192 -126 0
-160 -168 -92 0
59 81 28 0
-51 -104 -71 0
21 221 115 0
138 129 -27 0
230 189 130 0
243 -134 -174 0
37 -226 -38 0
-81 -181 -147 0
31 105 45 0
-20 -97 12 0
-242 -161 -221 0
-99 218 123 0
-63 157 -213 0
-125 -132 -33 0
243 208 -246 0
92 99 75 0
209 -112 224 0
113 60 205 0
4 143 -188 0
-186 55 -85 0
-95 -151 40 0
-175 171 -164 0
-197 -115 -221 0
-207 -193 -131 0
21 165 248 0
46 191 -207 0
137 -34 90 0
-211 129 -206 0
170 -237 88 0
-243 152 231 0
47 -52 -17 0
172 23 160 0
103 -33 -220 0
203 -133 236 0
107 -176 19 0
-164 -212 -75 0
-56 -136 233 0
56 250 87 0
26 10 183 0
-128 -157 -41 0
-170 157 -167 0
-206 142 -17 0
243 -162 -163 0
130 -213 230 0
-178 -101 -186 0
174 -167 -86 0
-221 116 -63 0
150 -46 81 0
33 5 -230 0
-42 -245 54 0
-155 -135 -217 0
-162 -195 243 0
-144 -82 -93 0
-242 -177 222 0
-174 -231 -33 0
-28 112 129 0
121 -14 -48 0
160 133 -61 0
-219 97 132 0
229 -241 52 0
-6 -246 -121 0
239 -109 -236 0
16 -132 -107 0
-31 101 -60 0
233 20 118 0
-42 -37 81 0
134 -160 -179 0
-95 211 -32 0
-164 -67 15 0
-100 -212 75 0
-53 -37 143 0
-203 -83 -224 0
32 -47 -131 0
-227 -162 -234 0
47 -233 -174 0
227 -3 -205 0
-184 -90 -236 0
-77 2 -235 0
123 42 144 0
-70 -79 -10 0
162 177 212 0
20 -229 -187 0
-193 -212 -159 0
159 -42 16 0
79 -218 127 0
47 -122 2 0
107 7 -27 0
200 -204 124 0
83 40 -84 0
146 170 -199 0
98 54 30 0
-147 -168 23 0
-85 161 238 0
1 -103 -158 0
66 96 -168 0
-173 216 228 0
-218 -212 -208 0
25 -220 79 0
131 179 -202 0
-36 79 248 0
127 -15 -81 0
144 -184 -107 0
19 -200 -210 0
-197 -93 66 0
49 165 -157 0
-161 244 -14 0
-136 242 164 0
-233 -111 -38 0
-79 156 -92 0
-223 -102 137 0
-129 59 249 0
122 -186 -88 0
-124 160 -41 0
162 180 -155 0
225 -47 -60 0
116 -55 16 0
210 69 -2 0
227 -228 -88 0
-16 50 -117 0
-128 -28 -237 0
-145 4 -217 0
-226 77 232 0
-155 99 -64 0
180 131 2 0
-237 179 -83 0
135 -10 225 0
-14 146 168 0
-82 28 139 0
97 -200 -135 0
-154 -233 -115 0
-207 -89 -240 0
-22 -204 -56 0
229 -30 -206 0
121 21 -175 0
190 22 153 0
34 -213 -196 0
-184 165 89 0
167 -81 -67 0
99 68 -11 0
194 12 -150 0
-204 100 120 0
34 57 177 0
-159 212 111 0
-215 -183 -126 0
103 -150 209 0
160 199 -125 0
-42 131 54 0
248 -161 -61 0
166 100 78 0
-239 -177 -183 0
222 88 -127 0
-93 -158 106 0
245 -124 -19 0
200 -148 3 0
-62 177 -3 0
173 -95 -20 0
-24 -33 -44 0
237 -174 43 0
-158 -179 171 0
-237 18 -36 0
-170 -184 -4 0
75 -7 -228 0
38 -121 80 0
103 -33 -237 0
-133 -180 -210 0
77 89 -154 0
25 -103 144 0
-158 8 149 0
46 -190 57 0
-224 96 180 0
153 -91 -187 0
194 -195 67 0
115 104 -44 0
37 -137 71 0
94 142 -129 0
122 227 -233 0
23 227 98 0
-126 -177 -148 0
50 226 125 0
154 -164 184 0
-174 59 235 0
-59 -139 244 0
200 103 -232 0
-86 -72 -147 0
-4 -95 130 0
-195 -50 -125 0
-196 -15 131 0
-245 -120 -211 0
146 52 -53 0
-8 -16 -88 0
204 147 -14 0
-70 -22 -234 0
58 -205 -23 0
250 76 41 0
-46 126 68 0
98 217 -168 0
82 114 -15 0
-219 -122 179 0
231 -138 185 0
-75 235 -179 0
163 216 -158 0
73 -158 -66 0
-61 -192 -1 0
99 -164 -27 0
85 -10 201 0
205 -64 35 0
-65 216 -20 0
10 112 184 0
-150 -199 -31 0
142 67 -226 0
-162 -35 191 0
58 211 49 0
70 101 212 0
-121 -11 -12 0
117 -79 -60 0
-219 83 173 0
243 -86 30 0
141 -232 222 0
-165 106 94 0
-169 -123 109 0
116 184 -112 0
-108 -86 -226 0
-9 18 120 0
-63 -34 -210 0
186 128 89 0
-73 221 237 0
74 117 166 0
187 -12 -59 0
161 -54 -212 0
-86 -147 -48 0
-228 -14 -123 0
-45 21 248 0
1 5 12 0
-238 221 57 0
-120 178 163 0
-70 80 117 0
73 88 -84 0
70 48 -158 0
-85 96 189 0
159 165 207 0
175 152 -138 0
-104 -166 19 0
-90 -56 -113 0
-215 222 66 0
-184 22 25 0
199 17 8 0
17 162 18 0
-101 -189 -58 0
-183 151 167 0
-108 -238 -51 0
-239 -77 -161 0
97 -180 -129 0
-117 65 166 0
120 -210 2 0
-66 -44 117 0
-186 -248 -171 0
-29 89 -16 0
-9 -118 160 0
53 105 13 0
155 128 112 0
-32 -10 -30 0
89 219 28 0
98 120 198 0
18 -105 197 0
99 -136 -211 0
151 -221 -24 0
191 -130 241 0
-144 -111 19 0
-169 -17 57 0
48 -59 -201 0
2 -79 132 0
-239 -122 -173 0
50 -60 -24 0
-179 129 -203 0
51 -125 -222 0
163 -135 -228 0
87 -149 -30 0
-173 -177 -6 0
131 -174 -95 0
-247 -209 -46 0
117 -123 -63 0
3 -121 -33 0
-184 -174 -235 0
11 -92 -46 0
90 -209 -13 0
175 -41 -3 0
22 -210 95 0
33 156 -16 0
218 -45 25 0
-230 229 -233 0
-182 -210 -191 0
159 250 107 0
96 87 234 0
45 71 -63 0
93 63 -179 0
-226 -236 -175 0
-64 79 -153 0
-249 178 -43 0
250 -83 217 0
-14 244 -113 0
157 -45 153 0
-233 -25 -151 0
-92 -195 -161 0
-30 -177 -32 0
-46 -2 -178 0
-75 -101 41 0
-50 164 -26 0
184 140 166 0
44 53 19 0
9 -95 -186 0
78 -53 -223 0
105 -147 -249 0
239 85 -135 0
-127 -162 244 0
-211 54 -9 0
79 -133 -14 0
24 43 143 0
-242 -87 172 0
101 -47 -191 0
96 209 205 0
66 -185 143 0
-75 9 -123 0
-54 -22 -57 0
-5 248 22 0
97 189 229 0
-61 -108 19 0
-35 -12 13 0
-127 33 -65 0
-158 -13 210 0
-200 55 241 0
12 166 141 0
34 154 89 0
-89 187 100 0
116 -27 120 0
128 156 -133 0
151 95 154 0
-118 -158 -177 0
24 -43 173 0
229 -61 69 0
176 -13 180 0
-46 31 -108 0
-222 -190 140 0
135 170 58 0
21 142 -168 0
45 -40 -123 0
148 201 -243 0
-68 213 -114 0
-100 28 -91 0
-6 -89 63 0
-116 2 129 0
123 1 250 0
-89 -165 234 0
-158 -230 -120 0
-169 143 -28 0
-70 -182 236 0
-247 -42 -90 0
18 -245 -101 0
-94 104 211 0
-152 20 241 0
-163 71 -239 0
238 15 201 0
14 27 102 0
96 122 151 0
-154 -235 22 0
-202 -76 93 0
99 212 -125 0
156 -52 -162 0
-55 11 -61 0
-207 221 130 0
250 67 118 0
203 -106 53 0
213 61 142 0
63 124 -68 0
-18 36 -105 0
189 14 36 0
-148 -59 149 0
-41 -99 -114 0
240 -35 -56 0
191 176 -170 0
14 11 198 0
-93 -215 -112 0
-44 -206 97 0
-90 -127 103 0
-30 -124 187 0
133 -182 20 0
-134 73 -52 0
244 107 171 0
159 -104 185 0
-23 -29 -241 0
-218 -111 90 0
75 -143 126 0
-64 62 12 0
62 -180 5 0
95 -208 113 0
22 -46 -110 0
-84 -61 72 0
50 196 -88 0
-133 -161 94 0
9 -79 -229 0
142 -154 -209 0
180 -247 -7 0
27 6 -83 0
29 200 92 0
144 -95 154 0
-37 108 190 0
-191 38 100 0
-84 -65 -60 0
-98 208 -76 0
-15 223 -6 0
-205 -132 -80 0
247 68 225 0
-151 98 77 0
-86 112 213 0
73 -66 15 0
-51 189 242 0
67 -81 -186 0
-53 77 48 0
135 122 -174 0
-140 -106 40 0
14 234 213 0
124 -180 126 0
10 -24 -128 0
120 -38 36 0
17 -24 173 0
80 -192 -91 0
-88 -71 134 0
-16 -141 128 0
58 -68 -93 0
-126 -227 -84 0
11 96 -30 0
141 -114 -117 0
120 135 -99 0
-70 151 -198 0
-73 136 127 0
95 -78 -127 0
-109 20 33 0
197 243 -162 0
175 -76 -145 0
-23 -60 41 0
179 -60 185 0
224 43 -84 0
-32 214 -199 0
188 185 29 0
238 -79 76 0
136 -157 100 0
-134 -185 77 0
174 -222 59 0
76 -103 2 0
-120 -173 137 0
236 -86 -21 0
-120 39 166 0
40 179 -78 0
-166 -127 96 0
226 100 -202 0
-226 31 -237 0
-227 -236 -181 0
249 221 -116 0
-69 -235 42 0
-194 -127 -122 0
47 -215 198 0
176 188 -49 0
-43 -78 201 0
74 -223 -3 0
138 -80 31 0
177 21 -233 0
-189 231 -130 0
-217 129 -38 0
-186 -111 164 0
92 114 129 0
140 -50 -124 0
-66 112 -159 0
-155 -65 -125 0
133 166 -22 0
-96 196 -111 0
-78 207 -33 0
130 145 -68 0
-34 -244 -230 0
68 -127 90 0
-210 -176 -197 0
-11 199 -212 0
-92 173 -235 0
163 -5 130 0
-138 7 -217 0
63 80 122 0
-189 -25 63 0
68 -78 13 0
201 -120 -29 0
-170 77 225 0
-83 -117 -176 0
-68 -65 -214 0
-221 32 -28 0
7 34 105 0
-3 -33 -121 0
-73 -2 -41 0
-188 -25 -231 0
-102 125 228 0
-114 -113 -94 0
-11 -150 -240 0
55 -200 161 0
-12 136 141 0
-188 139 170 0
225 130 140 0
25 -109 187 0
173 -44 -14 0
199 -151 -98 0
134 -81 23 0
-80 221 169 0
-5 64 125 0
4 250 157 0
229 32 197 0
-210 4 -169 0
-21 137 -134 0
206 110 236 0
193 54 -63 0
145 49 177 0
180 84 51 0
-13 86 244 0
69 230 207 0
-117 1 -61 0
75 245 180 0
47 16 -137 0
-204 126 38 0
45 -90 43 0
9 -11 -103 0
-199 14 197 0
182 -61 -49 0
20 112 38 0
-121 104 150 0
14 -114 -54 0
68 131 7 0
48 190 -82 0
8 28 -101 0
105 206 13 0
48 -132 -232 0
94 65 44 0
-121 -127 -242 0
193 230 27 0
-203 -131 -67 0
84 182 66 0
228 -126 -127 0
74 97 82 0
64 241 34 0
203 -236 190 0
204 34 6 0
-82 77 -164 0
-164 -172 235 0
50 -51 25 0
143 93 -44 0
-156 66 -29 0
200 166 204 0
-1 37 -223 0
19 -82 -9 0
-101 -58 243 0
-139 -46 170 0
-43 157 170 0
47 19 81 0
-228 22 195 0
-136 165 168 0
-232 197 104 0
-156 -217 76 0
-199 4 200 0
-195 30 7 0
-67 9 34 0
177 -14 195 0
234 -32 -223 0
-178 131 -211 0
-189 -43 248 0
62 -41 -99 0
-187 -162 179 0
138 224 86 0
67 209 -150 0
-246 -24 41 0
-83 30 55 0
98 -62 -203 0
-80 -81 -165 0
184 7 -155 0
81 29 -13 0
-135 104 -11 0
-229 -133 -197 0
123 -238 -221 0
-235 -88 -167 0
-129 250 -228 0
-123 -5 -102 0
-18 173 -19 0
106 227 165 0
-237 -248 155 0
104 -15 -75 0
-79 -29 -200 0
67 -179 -65 0
-12 249 -144 0
-244 -62 156 0
223 -68 -57 0
-242 -228 191 0
225 -82 148 0
-71 224 209 0
-240 110 22 0
-110 142 120 0
149 -18 -75 0
172 -150 58 0
135 30 7 0
-210 -15 -164 0
-45 -12 -130 0
248 -66 188 0
49 -77 -13 0
-140 30 1 0
200 83 -40 0
-101 109 203 0
150 22 186 0
-200 -142 167 0
-184 139 -91 0
-210 234 47 0
-191 -199 -220 0
-13 -78 15 0
-39 114 -250 0
17 -9 -137 0
72 -153 155 0
-229 -92 -201 0
-192 -248 206 0
64 -236 233 0
-61 208 67 0
118 136 162 0
-25 -233 -156 0
103 122 138 0
-178 -140 70 0
-218 14 35 0
79 -168 206 0
126 154 175 0
203 205 -11 0
172 107 98 0
138 84 -100 0
178 -33 100 0
154 -107 44 0
-207 -146 61 0
154 -99 204 0
-67 -111 154 0
-60 -137 51 0
28 70 112 0
-179 -30 198 0
87 -150 -224 0
110 -217 57 0
32 192 154 0
-87 -128 -139 0
-250 128 -241 0
72 -203 136 0
241 102 -4 0
-64 -146 -78 0
-36 64 56 0
-136 -12 -132 0
-113 30 -200 0
36 65 -44 0
175 -176 53 0
-182 179 93 0
242 239 116 0
121 -227 -104 0
13 11 243 0
213 -224 -31 0
-44 -158 -102 0
240 137 193 0
179 -131 34 0
-210 214 19 0
57 -231 42 0
10 -39 177 0
67 165 -208 0
66 -199 98 0
-109 -191 11 0
-195 199 11 0
-5 -45 181 0
-222 -135 -210 0
-47 104 24 0
-4 -25 83 0
76 -115 -123 0
-67 194 -174 0
-250 71 -27 0
-136 -98 35 0
232 -247 144 0
177 203 175 0
178 82 18 0
244 79 -188 0
-202 173 86 0
-105 -64 -75 0
-58 54 -155 0
57 -31 1 0
-191 -125 -159 0
-117 97 -120 0
31 -187 -16 0
-56 -242 197 0
-130 31 -81 0
211 -46 -86 0
-66 -40 -77 0
-137 -23 97 0
-44 -183 -23 0
40 -22 -27 0
-82 -113 177 0
-148 -48 -140 0
-134 119 154 0
11 64 213 0
30 -94 127 0
188 -45 142 0
213 109 -172 0
-234 -218 23 0
-168 -208 -106 0
235 21 -3 0
141 -14 -11 0
156 -91 -82 0
232 177 132 0
-47 232 38 0
61 -96 -49 0
30 -97 140 0
13 35 107 0
-9 95 226 0
220 145 -21 0
35 -107 -228 0
209 -200 -32 0
-115 4 196 0
-20 -106 -152 0
35 -216 -144 0
-188 7 -47 0
-100 -50 -167 0
-42 -12 160 0
-45 -2 112 0
196 30 73 0
30 -22 -52 0
-42 -37 191 0
115 -209 100 0
-31 -240 82 0
250 -132 -108 0
-117 250 -215 0
-59 118 187 0
-88 -190 63 0
18 -245 -248 0
177 -136 64 0
-227 -74 34 0
92 50 227 0
-133 137 -242 0
-203 -90 200 0
-132 -116 -222 0
230 127 -3 0
123 -159 45 0
-151 69 230 0
98 -216 143 0
134 -47 197 0
35 -221 223 0
32 -107 -199 0
-169 -107 -204 0
201 -98 182 0
175 -29 -143 0
-218 -168 106 0
-231 236 -197 0
64 -229 10 0
-234 -79 107 0
-12 -96 -30 0
-40 -185 80 0
-235 106 19 0
85 99 -58 0
-103 99 -13 0
-211 -26 -30 0
-153 220 181 0
16 100 -162 0
-113 -116 -45 0
105 63 9 0
51 -233 -49 0
77 125 199 0
-63 -123 -164 0
-171 -20 61 0
-125 -45 82 0
-156 213 86 0
-183 120 -131 0
-190 162 109 0
84 89 -113 0
173 -74 214 0
-211 -199 -152 0
-97 -111 -142 0
172 177 -93 0
-83 -174 1 0
78 -146 103 0
109 162 36 0
220 -172 -138 0
-42 71 -52 0
47 -183 66 0
-76 -206 -184 0
16 106 46 0
-79 -85 -43 0
-92 237 12 0
36 -168 -44 0
140 -39 128 0
208 232 230 0
-124 112 179 0
109 170 -110 0
232 -99 148 0
197 -90 150 0
-199 121 -98 0
-23 -247 243 0
-74 -22 240 0
164 -123 152 0
172 -95 191 0
187 118 224 0
-165 68 94 0
-227 93 -29 0
-20 190 -43 0
-23 -173 -35 0
67 -181 71 0
-137 129 -184 0
238 -12 45 0
-187 -248 11 0
-169 -192 -184 0
-156 222 107 0
92 -149 -200 0
227 -117 -246 0
93 70 -223 0
114 -216 -83 0
223 75 -209 0
150 -142 -118 0
84 -144 -114 0
54 8 66 0
-167 223 -80 0
-237 242 72 0
164 221 -14 0
-29 -153 -74 0
-139 36 246 0
-69 -229 78 0
-146 -214 -88 0
89 73 -129 0
33 133 102 0
95 164 -120 0
197 187 -159 0
-121 -229 100 0
-117 -35 -80 0
194 170 67 0
-129 -120 5 0
179 -157 -59 0
223 51 121 0
-81 125 -101 0
-94 64 -157 0
1 -237 52 0
-128 -164 170 0
-79 223 -151 0
16 125 -34 0
104 129 217 0
-193 39 62 0
-7 171 -209 0
-25 -185 -182 0
85 149 -101 0
-21 -120 14 0
62 73 -91 0
-168 -73 -54 0
86 -23 -94 0
243 -32 -127 0
-229 -171 -11 0
-45 219 213 0
18 -9 101 0
231 -221 121 0
-51 231 -100 0
69 53 170 0
-220 -90 -46 0
212 241 145 0
161 42 -2 0
-100 166 220 0
199 -161 -96 0
-196 -209 -230 0
128 -103 193 0
53 76 -46 0
44 -206 -77 0
-56 -103 79 0
41 -167 -28 0
-223 36 -21 0
-170 -111 11 0
-126 -209 -73 0
-121 -27 79 0
18 -218 216 0
-214 210 -159 0
-170 44 -77 0
48 134 -200 0
-96 -206 197 0
-224 -173 91 0
-63 -181 -38 0
187 85 -206 0
-6 -62 -98 0
125 -27 140 0
195 174 -217 0
-114 -175 115 0
64 83 -113 0
233 101 190 0
-14 181 147 0
-197 -22 164 0
-96 -59 -212 0
60 -37 -103 0
-61 234 169 0
154 -220 186 0
-3 -168 -55 0
-14 -246 -247 0
215 -52 237 0
-47 191 -103 0
-5 235 111 0
225 -45 -250 0
-217 -224 -145 0
-164 -163 189 0
20 -28 10 0
14 -248 76 0
-207 -163 161 0
106 158 95 0
138 -34 -206 0
-145 204 -213 0
246 -90 -204 0
188 -171 -55 0
220 -232 154 0
108 -120 -57 0
-250 -91 195 0
169 240 110 0
14 248 243 0
-65 -66 102 0
241 237 -204 0
-39 50 -239 0
3 180 224 0
-185 -66 -32 0
-47 -199 193 0
-232 -158 60 0
83 -244 -160 0
56 229 -101 0
63 -25 218 0
-221 -249 -51 0
236 128 124 0
155 -145 72 0
235 21 27 0
-238 -112 142 0
57 176 -93 0
-73 76 -117 0
25 26 72 0
-145 -75 59 0
-37 148 -220 0
22 159 -101 0
-102 88 -16 0
-146 -59 162 0
5 -50 -76 0
-171 -6 -132 0
-64 205 -142 0
104 -171 244 0
-5 34 -85 0
-167 6 39 0
227 -239 -14 0
-92 192 -153 0
-140 210 141 0
-159 -83 62 0
233 -165 -68 0
29 -132 124 0
-240 82 194 0
112 204 10 0
31 -244 -170 0
-154 -220 -83 0
-107 20 120 0
-233 -52 191 0
-226 55 209 0
-72 -87 38 0
-160 83 -245 0
230 -161 5 0
-210 123 118 0
156 25 -115 0