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