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