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