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