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