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