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