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