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