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