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