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