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