sidekick/tests/lia-sample/ex4960_2400_100.smt2

(set-info :smt-lib-version 2.6)
(set-logic QF_LIA)
(set-info :source |
Benchmarks from Miquel Bofill <mbofill@ima.udg.edu>
coming from a wastewater treatment scheduling problem
|)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun xH1 () Int)
(declare-fun xH2 () Int)
(declare-fun xH3 () Int)
(declare-fun xH4 () Int)
(declare-fun xH5 () Int)
(declare-fun xH6 () Int)
(declare-fun xH7 () Int)
(declare-fun xH8 () Int)
(declare-fun xH9 () Int)
(declare-fun xH10 () Int)
(declare-fun xH11 () Int)
(declare-fun xH12 () Int)
(declare-fun xH13 () Int)
(declare-fun xH14 () Int)
(declare-fun xH15 () Int)
(declare-fun xH16 () Int)
(declare-fun xH17 () Int)
(declare-fun xH18 () Int)
(declare-fun xH19 () Int)
(declare-fun xH20 () Int)
(declare-fun xH21 () Int)
(declare-fun xH22 () Int)
(declare-fun xH23 () Int)
(declare-fun xH24 () Int)
(declare-fun xH25 () Int)
(declare-fun xH26 () Int)
(declare-fun xH27 () Int)
(declare-fun xH28 () Int)
(declare-fun xH29 () Int)
(declare-fun xH30 () Int)
(declare-fun xH31 () Int)
(declare-fun xH32 () Int)
(declare-fun xH33 () Int)
(declare-fun xH34 () Int)
(declare-fun xH35 () Int)
(declare-fun xH36 () Int)
(declare-fun xH37 () Int)
(declare-fun xH38 () Int)
(declare-fun xH39 () Int)
(declare-fun xH40 () Int)
(declare-fun xH41 () Int)
(declare-fun xH42 () Int)
(declare-fun xH43 () Int)
(declare-fun xH44 () Int)
(declare-fun xH45 () Int)
(declare-fun xH46 () Int)
(declare-fun xH47 () Int)
(declare-fun xH48 () Int)
(declare-fun xH49 () Int)
(declare-fun xH50 () Int)
(declare-fun xH51 () Int)
(declare-fun xH52 () Int)
(declare-fun xH53 () Int)
(declare-fun xH54 () Int)
(declare-fun xH55 () Int)
(declare-fun xH56 () Int)
(declare-fun xH57 () Int)
(declare-fun xH58 () Int)
(declare-fun xH59 () Int)
(declare-fun xH60 () Int)
(declare-fun xH61 () Int)
(declare-fun xH62 () Int)
(declare-fun xH63 () Int)
(declare-fun xH64 () Int)
(declare-fun xH65 () Int)
(declare-fun xH66 () Int)
(declare-fun xH67 () Int)
(declare-fun xH68 () Int)
(declare-fun xH69 () Int)
(declare-fun xH70 () Int)
(declare-fun xH71 () Int)
(declare-fun xH72 () Int)
(declare-fun xH73 () Int)
(declare-fun xH74 () Int)
(declare-fun xH75 () Int)
(declare-fun xH76 () Int)
(declare-fun xH77 () Int)
(declare-fun xH78 () Int)
(declare-fun xH79 () Int)
(declare-fun xH80 () Int)
(declare-fun xH81 () Int)
(declare-fun xH82 () Int)
(declare-fun xH83 () Int)
(declare-fun xH84 () Int)
(declare-fun xH85 () Int)
(declare-fun xH86 () Int)
(declare-fun xH87 () Int)
(declare-fun xH88 () Int)
(declare-fun xH89 () Int)
(declare-fun xH90 () Int)
(declare-fun xH91 () Int)
(declare-fun xH92 () Int)
(declare-fun xH93 () Int)
(declare-fun xH94 () Int)
(declare-fun xH95 () Int)
(declare-fun xH96 () Int)
(declare-fun xH97 () Int)
(declare-fun xH98 () Int)
(declare-fun xH99 () Int)
(declare-fun xH100 () Int)
(declare-fun xH101 () Int)
(declare-fun xH102 () Int)
(declare-fun xH103 () Int)
(declare-fun xH104 () Int)
(declare-fun xH105 () Int)
(declare-fun xH106 () Int)
(declare-fun xH107 () Int)
(declare-fun xH108 () Int)
(declare-fun xH109 () Int)
(declare-fun xH110 () Int)
(declare-fun xH111 () Int)
(declare-fun xH112 () Int)
(declare-fun xH113 () Int)
(declare-fun xH114 () Int)
(declare-fun xH115 () Int)
(declare-fun xH116 () Int)
(declare-fun xH117 () Int)
(declare-fun xH118 () Int)
(declare-fun xH119 () Int)
(declare-fun xH120 () Int)
(declare-fun xH121 () Int)
(declare-fun xH122 () Int)
(declare-fun xH123 () Int)
(declare-fun xH124 () Int)
(declare-fun xH125 () Int)
(declare-fun xH126 () Int)
(declare-fun xH127 () Int)
(declare-fun xH128 () Int)
(declare-fun xH129 () Int)
(declare-fun xH130 () Int)
(declare-fun xH131 () Int)
(declare-fun xH132 () Int)
(declare-fun xH133 () Int)
(declare-fun xH134 () Int)
(declare-fun xH135 () Int)
(declare-fun xH136 () Int)
(declare-fun xH137 () Int)
(declare-fun xH138 () Int)
(declare-fun xH139 () Int)
(declare-fun xH140 () Int)
(declare-fun xH141 () Int)
(declare-fun xH142 () Int)
(declare-fun xH143 () Int)
(declare-fun xH144 () Int)
(declare-fun xH145 () Int)
(declare-fun xH146 () Int)
(declare-fun xH147 () Int)
(declare-fun xH148 () Int)
(declare-fun xH149 () Int)
(declare-fun xH150 () Int)
(declare-fun xH151 () Int)
(declare-fun xH152 () Int)
(declare-fun xH153 () Int)
(declare-fun xH154 () Int)
(declare-fun xH155 () Int)
(declare-fun xH156 () Int)
(declare-fun xH157 () Int)
(declare-fun xH158 () Int)
(declare-fun xH159 () Int)
(declare-fun xH160 () Int)
(declare-fun xH161 () Int)
(declare-fun xH162 () Int)
(declare-fun xH163 () Int)
(declare-fun xH164 () Int)
(declare-fun xH165 () Int)
(declare-fun xH166 () Int)
(declare-fun xH167 () Int)
(declare-fun xH168 () Int)
(declare-fun xH169 () Int)
(declare-fun xH170 () Int)
(declare-fun xH171 () Int)
(declare-fun xH172 () Int)
(declare-fun xH173 () Int)
(declare-fun xH174 () Int)
(declare-fun xH175 () Int)
(declare-fun xH176 () Int)
(declare-fun xH177 () Int)
(declare-fun xH178 () Int)
(declare-fun xH179 () Int)
(declare-fun xH180 () Int)
(declare-fun xH181 () Int)
(declare-fun xH182 () Int)
(declare-fun xH183 () Int)
(declare-fun xH184 () Int)
(declare-fun xH185 () Int)
(declare-fun xH186 () Int)
(declare-fun xH187 () Int)
(declare-fun xH188 () Int)
(declare-fun xH189 () Int)
(declare-fun xH190 () Int)
(declare-fun xH191 () Int)
(declare-fun xH192 () Int)
(declare-fun xH193 () Int)
(declare-fun xH194 () Int)
(declare-fun xH195 () Int)
(declare-fun xH196 () Int)
(declare-fun xH197 () Int)
(declare-fun xH198 () Int)
(declare-fun xH199 () Int)
(declare-fun xH200 () Int)
(declare-fun xH201 () Int)
(declare-fun xH202 () Int)
(declare-fun xH203 () Int)
(declare-fun xH204 () Int)
(declare-fun xH205 () Int)
(declare-fun xH206 () Int)
(declare-fun xH207 () Int)
(declare-fun xH208 () Int)
(declare-fun xH209 () Int)
(declare-fun xH210 () Int)
(declare-fun xH211 () Int)
(declare-fun xH212 () Int)
(declare-fun xH213 () Int)
(declare-fun xH214 () Int)
(declare-fun xH215 () Int)
(declare-fun xH216 () Int)
(declare-fun xH217 () Int)
(declare-fun xH218 () Int)
(declare-fun xH219 () Int)
(declare-fun xH220 () Int)
(declare-fun xH221 () Int)
(declare-fun xH222 () Int)
(declare-fun xH223 () Int)
(declare-fun xH224 () Int)
(declare-fun xH225 () Int)
(declare-fun xH226 () Int)
(declare-fun xH227 () Int)
(declare-fun xH228 () Int)
(declare-fun xH229 () Int)
(declare-fun xH230 () Int)
(declare-fun xH231 () Int)
(declare-fun xH232 () Int)
(declare-fun xH233 () Int)
(declare-fun xH234 () Int)
(declare-fun xH235 () Int)
(declare-fun xH236 () Int)
(declare-fun xH237 () Int)
(declare-fun xH238 () Int)
(declare-fun xH239 () Int)
(declare-fun xH240 () Int)
(declare-fun xH241 () Int)
(declare-fun xH242 () Int)
(declare-fun xH243 () Int)
(declare-fun xH244 () Int)
(declare-fun xH245 () Int)
(declare-fun xH246 () Int)
(declare-fun xH247 () Int)
(declare-fun xH248 () Int)
(declare-fun xH249 () Int)
(declare-fun xH250 () Int)
(declare-fun xH251 () Int)
(declare-fun xH252 () Int)
(declare-fun xH253 () Int)
(declare-fun xH254 () Int)
(declare-fun xH255 () Int)
(declare-fun xH256 () Int)
(declare-fun xH257 () Int)
(declare-fun xH258 () Int)
(declare-fun xH259 () Int)
(declare-fun xH260 () Int)
(declare-fun xH261 () Int)
(declare-fun xH262 () Int)
(declare-fun xH263 () Int)
(declare-fun xH264 () Int)
(declare-fun xH265 () Int)
(declare-fun xH266 () Int)
(declare-fun xH267 () Int)
(declare-fun xH268 () Int)
(declare-fun xH269 () Int)
(declare-fun xH270 () Int)
(declare-fun xH271 () Int)
(declare-fun xH272 () Int)
(declare-fun xH273 () Int)
(declare-fun xH274 () Int)
(declare-fun xH275 () Int)
(declare-fun xH276 () Int)
(declare-fun xH277 () Int)
(declare-fun xH278 () Int)
(declare-fun xH279 () Int)
(declare-fun xH280 () Int)
(declare-fun xH281 () Int)
(declare-fun xH282 () Int)
(declare-fun xH283 () Int)
(declare-fun xH284 () Int)
(declare-fun xH285 () Int)
(declare-fun xH286 () Int)
(declare-fun xH287 () Int)
(declare-fun xH288 () Int)
(declare-fun xH289 () Int)
(declare-fun xH290 () Int)
(declare-fun xH291 () Int)
(declare-fun xH292 () Int)
(declare-fun xH293 () Int)
(declare-fun xH294 () Int)
(declare-fun xH295 () Int)
(declare-fun xH296 () Int)
(declare-fun xH297 () Int)
(declare-fun xH298 () Int)
(declare-fun xH299 () Int)
(declare-fun xH300 () Int)
(declare-fun xH301 () Int)
(declare-fun xH302 () Int)
(declare-fun xH303 () Int)
(declare-fun xH304 () Int)
(declare-fun xH305 () Int)
(declare-fun xH306 () Int)
(declare-fun xH307 () Int)
(declare-fun xH308 () Int)
(declare-fun xH309 () Int)
(declare-fun xH310 () Int)
(declare-fun xH311 () Int)
(declare-fun xH312 () Int)
(declare-fun xH313 () Int)
(declare-fun xH314 () Int)
(declare-fun xH315 () Int)
(declare-fun xH316 () Int)
(declare-fun xH317 () Int)
(declare-fun xH318 () Int)
(declare-fun xH319 () Int)
(declare-fun xH320 () Int)
(declare-fun xH321 () Int)
(declare-fun xH322 () Int)
(declare-fun xH323 () Int)
(declare-fun xH324 () Int)
(declare-fun xH325 () Int)
(declare-fun xH326 () Int)
(declare-fun xH327 () Int)
(declare-fun xH328 () Int)
(declare-fun xH329 () Int)
(declare-fun xH330 () Int)
(declare-fun xH331 () Int)
(declare-fun xH332 () Int)
(declare-fun xH333 () Int)
(declare-fun xH334 () Int)
(declare-fun xH335 () Int)
(declare-fun xH336 () Int)
(declare-fun xH337 () Int)
(declare-fun xH338 () Int)
(declare-fun xH339 () Int)
(declare-fun xH340 () Int)
(declare-fun xH341 () Int)
(declare-fun xH342 () Int)
(declare-fun xH343 () Int)
(declare-fun xH344 () Int)
(declare-fun xH345 () Int)
(declare-fun xH346 () Int)
(declare-fun xH347 () Int)
(declare-fun xH348 () Int)
(declare-fun xH349 () Int)
(declare-fun xH350 () Int)
(declare-fun xH351 () Int)
(declare-fun xH352 () Int)
(declare-fun xH353 () Int)
(declare-fun xH354 () Int)
(declare-fun xH355 () Int)
(declare-fun xH356 () Int)
(declare-fun xH357 () Int)
(declare-fun xH358 () Int)
(declare-fun xH359 () Int)
(declare-fun xH360 () Int)
(declare-fun xH361 () Int)
(declare-fun xH362 () Int)
(declare-fun xH363 () Int)
(declare-fun xH364 () Int)
(declare-fun xH365 () Int)
(declare-fun xH366 () Int)
(declare-fun xH367 () Int)
(declare-fun xH368 () Int)
(declare-fun xH369 () Int)
(declare-fun xH370 () Int)
(declare-fun xH371 () Int)
(declare-fun xH372 () Int)
(declare-fun xH373 () Int)
(declare-fun xH374 () Int)
(declare-fun xH375 () Int)
(declare-fun xH376 () Int)
(declare-fun xH377 () Int)
(declare-fun xH378 () Int)
(declare-fun xH379 () Int)
(declare-fun xH380 () Int)
(declare-fun xH381 () Int)
(declare-fun xH382 () Int)
(declare-fun xH383 () Int)
(declare-fun xH384 () Int)
(declare-fun xH385 () Int)
(declare-fun xH386 () Int)
(declare-fun xH387 () Int)
(declare-fun xH388 () Int)
(declare-fun xH389 () Int)
(declare-fun xH390 () Int)
(declare-fun xH391 () Int)
(declare-fun xH392 () Int)
(declare-fun xH393 () Int)
(declare-fun xH394 () Int)
(declare-fun xH395 () Int)
(declare-fun xH396 () Int)
(declare-fun xH397 () Int)
(declare-fun xH398 () Int)
(declare-fun xH399 () Int)
(declare-fun xH400 () Int)
(declare-fun xH401 () Int)
(declare-fun xH402 () Int)
(declare-fun xH403 () Int)
(declare-fun xH404 () Int)
(declare-fun xH405 () Int)
(declare-fun xH406 () Int)
(declare-fun xH407 () Int)
(declare-fun xH408 () Int)
(declare-fun xH409 () Int)
(declare-fun xH410 () Int)
(declare-fun xH411 () Int)
(declare-fun xH412 () Int)
(declare-fun xH413 () Int)
(declare-fun xH414 () Int)
(declare-fun xH415 () Int)
(declare-fun xH416 () Int)
(declare-fun xH417 () Int)
(declare-fun xH418 () Int)
(declare-fun xH419 () Int)
(declare-fun xH420 () Int)
(declare-fun xH421 () Int)
(declare-fun xH422 () Int)
(declare-fun xH423 () Int)
(declare-fun xH424 () Int)
(declare-fun xH425 () Int)
(declare-fun xH426 () Int)
(declare-fun xH427 () Int)
(declare-fun xH428 () Int)
(declare-fun xH429 () Int)
(declare-fun xH430 () Int)
(declare-fun xH431 () Int)
(declare-fun xH432 () Int)
(declare-fun xH433 () Int)
(declare-fun xH434 () Int)
(declare-fun xH435 () Int)
(declare-fun xH436 () Int)
(declare-fun xH437 () Int)
(declare-fun xH438 () Int)
(declare-fun xH439 () Int)
(declare-fun xH440 () Int)
(declare-fun xH441 () Int)
(declare-fun xH442 () Int)
(declare-fun xH443 () Int)
(declare-fun xH444 () Int)
(declare-fun xH445 () Int)
(declare-fun xH446 () Int)
(declare-fun xH447 () Int)
(declare-fun xH448 () Int)
(declare-fun xH449 () Int)
(declare-fun xH450 () Int)
(declare-fun xH451 () Int)
(declare-fun xH452 () Int)
(declare-fun xH453 () Int)
(declare-fun xH454 () Int)
(declare-fun xH455 () Int)
(declare-fun xH456 () Int)
(declare-fun xH457 () Int)
(declare-fun xH458 () Int)
(declare-fun xH459 () Int)
(declare-fun xH460 () Int)
(declare-fun xH461 () Int)
(declare-fun xH462 () Int)
(declare-fun xH463 () Int)
(declare-fun xH464 () Int)
(declare-fun xH465 () Int)
(declare-fun xH466 () Int)
(declare-fun xH467 () Int)
(declare-fun xH468 () Int)
(declare-fun xH469 () Int)
(declare-fun xH470 () Int)
(declare-fun xH471 () Int)
(declare-fun xH472 () Int)
(declare-fun xH473 () Int)
(declare-fun xH474 () Int)
(declare-fun xH475 () Int)
(declare-fun xH476 () Int)
(declare-fun xH477 () Int)
(declare-fun xH478 () Int)
(declare-fun xH479 () Int)
(declare-fun xH480 () Int)
(declare-fun xH481 () Int)
(declare-fun xH482 () Int)
(declare-fun xH483 () Int)
(declare-fun xH484 () Int)
(declare-fun xH485 () Int)
(declare-fun xH486 () Int)
(declare-fun xH487 () Int)
(declare-fun xH488 () Int)
(declare-fun xH489 () Int)
(declare-fun xH490 () Int)
(declare-fun xH491 () Int)
(declare-fun xH492 () Int)
(declare-fun xH493 () Int)
(declare-fun xH494 () Int)
(declare-fun xH495 () Int)
(declare-fun xH496 () Int)
(declare-fun xH497 () Int)
(declare-fun xH498 () Int)
(declare-fun xH499 () Int)
(declare-fun xH500 () Int)
(declare-fun xH501 () Int)
(declare-fun xH502 () Int)
(declare-fun xH503 () Int)
(declare-fun xH504 () Int)
(declare-fun xH505 () Int)
(declare-fun xH506 () Int)
(declare-fun xH507 () Int)
(declare-fun xH508 () Int)
(declare-fun xH509 () Int)
(declare-fun xH510 () Int)
(declare-fun xH511 () Int)
(declare-fun xH512 () Int)
(declare-fun xH513 () Int)
(declare-fun xH514 () Int)
(declare-fun xH515 () Int)
(declare-fun xH516 () Int)
(declare-fun xH517 () Int)
(declare-fun xH518 () Int)
(declare-fun xH519 () Int)
(declare-fun xH520 () Int)
(declare-fun xH521 () Int)
(declare-fun xH522 () Int)
(declare-fun xH523 () Int)
(declare-fun xH524 () Int)
(declare-fun xH525 () Int)
(declare-fun xH526 () Int)
(declare-fun xH527 () Int)
(declare-fun xH528 () Int)
(declare-fun xH529 () Int)
(declare-fun xH530 () Int)
(declare-fun xH531 () Int)
(declare-fun xH532 () Int)
(declare-fun xH533 () Int)
(declare-fun xH534 () Int)
(declare-fun xH535 () Int)
(declare-fun xH536 () Int)
(declare-fun xH537 () Int)
(declare-fun xH538 () Int)
(declare-fun xH539 () Int)
(declare-fun xH540 () Int)
(declare-fun xH541 () Int)
(declare-fun xH542 () Int)
(declare-fun xH543 () Int)
(declare-fun xH544 () Int)
(declare-fun xH545 () Int)
(declare-fun xH546 () Int)
(declare-fun xH547 () Int)
(declare-fun xH548 () Int)
(declare-fun xH549 () Int)
(declare-fun xH550 () Int)
(declare-fun xH551 () Int)
(declare-fun xH552 () Int)
(declare-fun xH553 () Int)
(declare-fun xH554 () Int)
(declare-fun xH555 () Int)
(declare-fun xH556 () Int)
(declare-fun xH557 () Int)
(declare-fun xH558 () Int)
(declare-fun xH559 () Int)
(declare-fun xH560 () Int)
(declare-fun xH561 () Int)
(declare-fun xH562 () Int)
(declare-fun xH563 () Int)
(declare-fun xH564 () Int)
(declare-fun xH565 () Int)
(declare-fun xH566 () Int)
(declare-fun xH567 () Int)
(declare-fun xH568 () Int)
(declare-fun xH569 () Int)
(declare-fun xH570 () Int)
(declare-fun xH571 () Int)
(declare-fun xH572 () Int)
(declare-fun xH573 () Int)
(declare-fun xH574 () Int)
(declare-fun xH575 () Int)
(declare-fun xH576 () Int)
(assert (and (= xH1 0) (= xH385 0) (= xH2 (- xH1 xH194)) (= xH386 0) (= xH3 (- (+ (- xH2 xH195) 4000) xH387)) (or (= xH387 4000) (= xH387 0)) (= xH4 (- xH3 xH196)) (= xH388 0) (= xH5 (- (+ (- xH4 xH197) 2000) xH389)) (or (= xH389 2000) (= xH389 0)) (= xH6 (- xH5 xH198)) (= xH390 0) (= xH7 (- (+ (- xH6 xH199) 3800) xH391)) (or (= xH391 3800) (= xH391 0)) (= xH8 (- xH7 xH200)) (= xH392 0) (= xH9 (- (+ (- xH8 xH201) 1000) xH393)) (or (= xH393 1000) (= xH393 0)) (= xH10 (- xH9 xH202)) (= xH394 0) (= xH11 (- (+ (- xH10 xH203) 4000) xH395)) (or (= xH395 4000) (= xH395 0)) (= xH12 (- xH11 xH204)) (= xH396 0) (= xH13 (- (+ (- xH12 xH205) 2500) xH397)) (or (= xH397 2500) (= xH397 0)) (= xH14 (- xH13 xH206)) (= xH398 0) (= xH15 (- (+ (- xH14 xH207) 3000) xH399)) (or (= xH399 3000) (= xH399 0)) (= xH16 (- xH15 xH208)) (= xH400 0) (= xH17 (- (+ (- xH16 xH209) 4000) xH401)) (or (= xH401 4000) (= xH401 0)) (= xH18 (- xH17 xH210)) (= xH402 0) (= xH19 (- (+ (- xH18 xH211) 2000) xH403)) (or (= xH403 2000) (= xH403 0)) (= xH20 (- xH19 xH212)) (= xH404 0) (= xH21 (- (+ (- xH20 xH213) 1500) xH405)) (or (= xH405 1500) (= xH405 0)) (= xH22 (- xH21 xH214)) (= xH406 0) (= xH23 (- (+ (- xH22 xH215) 2500) xH407)) (or (= xH407 2500) (= xH407 0)) (= xH24 (- xH23 xH216)) (= xH408 0) (= xH25 0) (= xH409 0) (= xH26 (- xH25 xH218)) (= xH410 0) (= xH27 (- xH26 xH219)) (= xH411 0) (= xH28 (- xH27 xH220)) (= xH412 0) (= xH29 (- xH28 xH221)) (= xH413 0) (= xH30 (- xH29 xH222)) (= xH414 0) (= xH31 (- xH30 xH223)) (= xH415 0) (= xH32 (- xH31 xH224)) (= xH416 0) (= xH33 (- xH32 xH225)) (= xH417 0) (= xH34 (- xH33 xH226)) (= xH418 0) (= xH35 (- xH34 xH227)) (= xH419 0) (= xH36 (- xH35 xH228)) (= xH420 0) (= xH37 (- (+ (- xH36 xH229) 2600) xH421)) (or (= xH421 2600) (= xH421 0)) (= xH38 (- xH37 xH230)) (= xH422 0) (= xH39 (- xH38 xH231)) (= xH423 0) (= xH40 (- xH39 xH232)) (= xH424 0) (= xH41 (- xH40 xH233)) (= xH425 0) (= xH42 (- xH41 xH234)) (= xH426 0) (= xH43 (- xH42 xH235)) (= xH427 0) (= xH44 (- xH43 xH236)) (= xH428 0) (= xH45 (- xH44 xH237)) (= xH429 0) (= xH46 (- xH45 xH238)) (= xH430 0) (= xH47 (- xH46 xH239)) (= xH431 0) (= xH48 (- xH47 xH240)) (= xH432 0) (= xH49 0) (= xH433 0) (= xH50 (- xH49 xH242)) (= xH434 0) (= xH51 (- xH50 xH243)) (= xH435 0) (= xH52 (- (+ (- xH51 xH244) 1000) xH436)) (= xH53 (- (+ (- xH52 xH245) 1000) xH437)) (or (and (= xH436 1000) (= xH437 1000)) (and (= xH436 0) (= xH437 0))) (= xH54 (- xH53 xH246)) (= xH438 0) (= xH55 (- xH54 xH247)) (= xH439 0) (= xH56 (- xH55 xH248)) (= xH440 0) (= xH57 (- xH56 xH249)) (= xH441 0) (= xH58 (- (+ (- xH57 xH250) 1500) xH442)) (or (= xH442 1500) (= xH442 0)) (= xH59 (- xH58 xH251)) (= xH443 0) (= xH60 (- xH59 xH252)) (= xH444 0) (= xH61 (- xH60 xH253)) (= xH445 0) (= xH62 (- (+ (- xH61 xH254) 300) xH446)) (= xH63 (- (+ (- xH62 xH255) 300) xH447)) (= xH64 (- (+ (- xH63 xH256) 300) xH448)) (or (and (= xH446 300) (= xH447 300) (= xH448 300)) (and (= xH446 0) (= xH447 0) (= xH448 0))) (= xH65 (- xH64 xH257)) (= xH449 0) (= xH66 (- xH65 xH258)) (= xH450 0) (= xH67 (- xH66 xH259)) (= xH451 0) (= xH68 (- xH67 xH260)) (= xH452 0) (= xH69 (- (+ (- xH68 xH261) 2000) xH453)) (or (= xH453 2000) (= xH453 0)) (= xH70 (- xH69 xH262)) (= xH454 0) (= xH71 (- xH70 xH263)) (= xH455 0) (= xH72 (- xH71 xH264)) (= xH456 0) (= xH73 (- 750 xH457)) (or (= xH457 750) (= xH457 0)) (= xH74 (- (+ (- xH73 xH266) 750) xH458)) (or (= xH458 750) (= xH458 0)) (= xH75 (- (+ (- xH74 xH267) 750) xH459)) (or (= xH459 750) (= xH459 0)) (= xH76 (- (+ (- xH75 xH268) 750) xH460)) (or (= xH460 750) (= xH460 0)) (= xH77 (- (+ (- xH76 xH269) 750) xH461)) (or (= xH461 750) (= xH461 0)) (= xH78 (- (+ (- xH77 xH270) 750) xH462)) (or (= xH462 750) (= xH462 0)) (= xH79 (- (+ (- xH78 xH271) 750) xH463)) (or (= xH463 750) (= xH463 0)) (= xH80 (- (+ (- xH79 xH272) 750) xH464)) (or (= xH464 750) (= xH464 0)) (= xH81 (- (+ (- xH80 xH273) 750) xH465)) (or (= xH465 750) (= xH465 0)) (= xH82 (- (+ (- xH81 xH274) 750) xH466)) (or (= xH466 750) (= xH466 0)) (= xH83 (- (+ (- xH82 xH275) 750) xH467)) (or (= xH467 750) (= xH467 0)) (= xH84 (- (+ (- xH83 xH276) 750) xH468)) (or (= xH468 750) (= xH468 0)) (= xH85 (- (+ (- xH84 xH277) 750) xH469)) (or (= xH469 750) (= xH469 0)) (= xH86 (- (+ (- xH85 xH278) 750) xH470)) (or (= xH470 750) (= xH470 0)) (= xH87 (- (+ (- xH86 xH279) 750) xH471)) (or (= xH471 750) (= xH471 0)) (= xH88 (- (+ (- xH87 xH280) 750) xH472)) (or (= xH472 750) (= xH472 0)) (= xH89 (- (+ (- xH88 xH281) 750) xH473)) (or (= xH473 750) (= xH473 0)) (= xH90 (- (+ (- xH89 xH282) 750) xH474)) (or (= xH474 750) (= xH474 0)) (= xH91 (- (+ (- xH90 xH283) 750) xH475)) (or (= xH475 750) (= xH475 0)) (= xH92 (- (+ (- xH91 xH284) 750) xH476)) (or (= xH476 750) (= xH476 0)) (= xH93 (- (+ (- xH92 xH285) 750) xH477)) (or (= xH477 750) (= xH477 0)) (= xH94 (- (+ (- xH93 xH286) 750) xH478)) (or (= xH478 750) (= xH478 0)) (= xH95 (- (+ (- xH94 xH287) 750) xH479)) (or (= xH479 750) (= xH479 0)) (= xH96 (- (+ (- xH95 xH288) 750) xH480)) (or (= xH480 750) (= xH480 0)) (= xH97 0) (= xH481 0) (= xH98 (- xH97 xH290)) (= xH482 0) (= xH99 (- xH98 xH291)) (= xH483 0) (= xH100 (- xH99 xH292)) (= xH484 0) (= xH101 (- xH100 xH293)) (= xH485 0) (= xH102 (- (+ (- xH101 xH294) 2500) xH486)) (or (= xH486 2500) (= xH486 0)) (= xH103 (- xH102 xH295)) (= xH487 0) (= xH104 (- xH103 xH296)) (= xH488 0) (= xH105 (- xH104 xH297)) (= xH489 0) (= xH106 (- xH105 xH298)) (= xH490 0) (= xH107 (- xH106 xH299)) (= xH491 0) (= xH108 (- xH107 xH300)) (= xH492 0) (= xH109 (- xH108 xH301)) (= xH493 0) (= xH110 (- xH109 xH302)) (= xH494 0) (= xH111 (- xH110 xH303)) (= xH495 0) (= xH112 (- (+ (- xH111 xH304) 3000) xH496)) (or (= xH496 3000) (= xH496 0)) (= xH113 (- xH112 xH305)) (= xH497 0) (= xH114 (- xH113 xH306)) (= xH498 0) (= xH115 (- xH114 xH307)) (= xH499 0) (= xH116 (- xH115 xH308)) (= xH500 0) (= xH117 (- xH116 xH309)) (= xH501 0) (= xH118 (- xH117 xH310)) (= xH502 0) (= xH119 (- xH118 xH311)) (= xH503 0) (= xH120 (- xH119 xH312)) (= xH504 0) (= xH121 0) (= xH505 0) (= xH122 (- (+ (- xH121 xH314) 2000) xH506)) (= xH123 (- (+ (- xH122 xH315) 2000) xH507)) (or (and (= xH506 2000) (= xH507 2000)) (and (= xH506 0) (= xH507 0))) (= xH124 (- xH123 xH316)) (= xH508 0) (= xH125 (- xH124 xH317)) (= xH509 0) (= xH126 (- xH125 xH318)) (= xH510 0) (= xH127 (- xH126 xH319)) (= xH511 0) (= xH128 (- (+ (- xH127 xH320) 500) xH512)) (= xH129 (- (+ (- xH128 xH321) 500) xH513)) (= xH130 (- (+ (- xH129 xH322) 500) xH514)) (or (and (= xH512 500) (= xH513 500) (= xH514 500)) (and (= xH512 0) (= xH513 0) (= xH514 0))) (= xH131 (- xH130 xH323)) (= xH515 0) (= xH132 (- xH131 xH324)) (= xH516 0) (= xH133 (- (+ (- xH132 xH325) 1700) xH517)) (or (= xH517 1700) (= xH517 0)) (= xH134 (- xH133 xH326)) (= xH518 0) (= xH135 (- xH134 xH327)) (= xH519 0) (= xH136 (- (+ (- xH135 xH328) 1300) xH520)) (or (= xH520 1300) (= xH520 0)) (= xH137 (- xH136 xH329)) (= xH521 0) (= xH138 (- xH137 xH330)) (= xH522 0) (= xH139 (- xH138 xH331)) (= xH523 0) (= xH140 (- xH139 xH332)) (= xH524 0) (= xH141 (- (+ (- xH140 xH333) 1500) xH525)) (= xH142 (- (+ (- xH141 xH334) 1500) xH526)) (or (and (= xH525 1500) (= xH526 1500)) (and (= xH525 0) (= xH526 0))) (= xH143 (- xH142 xH335)) (= xH527 0) (= xH144 (- xH143 xH336)) (= xH528 0) (= xH145 (- 650 xH529)) (or (= xH529 650) (= xH529 0)) (= xH146 (- (+ (- xH145 xH338) 650) xH530)) (or (= xH530 650) (= xH530 0)) (= xH147 (- (+ (- xH146 xH339) 650) xH531)) (or (= xH531 650) (= xH531 0)) (= xH148 (- (+ (- xH147 xH340) 850) xH532)) (or (= xH532 850) (= xH532 0)) (= xH149 (- (+ (- xH148 xH341) 650) xH533)) (or (= xH533 650) (= xH533 0)) (= xH150 (- (+ (- xH149 xH342) 650) xH534)) (or (= xH534 650) (= xH534 0)) (= xH151 (- (+ (- xH150 xH343) 650) xH535)) (or (= xH535 650) (= xH535 0)) (= xH152 (- (+ (- xH151 xH344) 650) xH536)) (or (= xH536 650) (= xH536 0)) (= xH153 (- (+ (- xH152 xH345) 650) xH537)) (or (= xH537 650) (= xH537 0)) (= xH154 (- (+ (- xH153 xH346) 650) xH538)) (or (= xH538 650) (= xH538 0)) (= xH155 (- (+ (- xH154 xH347) 650) xH539)) (or (= xH539 650) (= xH539 0)) (= xH156 (- (+ (- xH155 xH348) 650) xH540)) (or (= xH540 650) (= xH540 0)) (= xH157 (- (+ (- xH156 xH349) 850) xH541)) (or (= xH541 850) (= xH541 0)) (= xH158 (- (+ (- xH157 xH350) 650) xH542)) (or (= xH542 650) (= xH542 0)) (= xH159 (- (+ (- xH158 xH351) 650) xH543)) (or (= xH543 650) (= xH543 0)) (= xH160 (- (+ (- xH159 xH352) 650) xH544)) (or (= xH544 650) (= xH544 0)) (= xH161 (- (+ (- xH160 xH353) 650) xH545)) (or (= xH545 650) (= xH545 0)) (= xH162 (- (+ (- xH161 xH354) 650) xH546)) (or (= xH546 650) (= xH546 0)) (= xH163 (- (+ (- xH162 xH355) 650) xH547)) (or (= xH547 650) (= xH547 0)) (= xH164 (- (+ (- xH163 xH356) 850) xH548)) (or (= xH548 850) (= xH548 0)) (= xH165 (- (+ (- xH164 xH357) 650) xH549)) (or (= xH549 650) (= xH549 0)) (= xH166 (- (+ (- xH165 xH358) 650) xH550)) (or (= xH550 650) (= xH550 0)) (= xH167 (- (+ (- xH166 xH359) 650) xH551)) (or (= xH551 650) (= xH551 0)) (= xH168 (- xH167 xH360)) (= xH552 0) (= xH169 0) (= xH553 0) (= xH170 (- xH169 xH362)) (= xH554 0) (= xH171 (- (+ (- xH170 xH363) 4000) xH555)) (or (= xH555 4000) (= xH555 0)) (= xH172 (- xH171 xH364)) (= xH556 0) (= xH173 (- (+ (- xH172 xH365) 2000) xH557)) (or (= xH557 2000) (= xH557 0)) (= xH174 (- xH173 xH366)) (= xH558 0) (= xH175 (- (+ (- xH174 xH367) 3800) xH559)) (or (= xH559 3800) (= xH559 0)) (= xH176 (- xH175 xH368)) (= xH560 0) (= xH177 (- (+ (- xH176 xH369) 1000) xH561)) (or (= xH561 1000) (= xH561 0)) (= xH178 (- xH177 xH370)) (= xH562 0) (= xH179 (- (+ (- xH178 xH371) 4000) xH563)) (or (= xH563 4000) (= xH563 0)) (= xH180 (- xH179 xH372)) (= xH564 0) (= xH181 (- xH180 xH373)) (= xH565 0) (= xH182 (- xH181 xH374)) (= xH566 0) (= xH183 (- (+ (- xH182 xH375) 750) xH567)) (or (= xH567 750) (= xH567 0)) (= xH184 (- (+ (- xH183 xH376) 750) xH568)) (or (= xH568 750) (= xH568 0)) (= xH185 (- (+ (- xH184 xH377) 750) xH569)) (or (= xH569 750) (= xH569 0)) (= xH186 (- (+ (- xH185 xH378) 750) xH570)) (or (= xH570 750) (= xH570 0)) (= xH187 (- (+ (- xH186 xH379) 750) xH571)) (or (= xH571 750) (= xH571 0)) (= xH188 (- (+ (- xH187 xH380) 750) xH572)) (or (= xH572 750) (= xH572 0)) (= xH189 (- (+ (- xH188 xH381) 750) xH573)) (or (= xH573 750) (= xH573 0)) (= xH190 (- (+ (- xH189 xH382) 750) xH574)) (or (= xH574 750) (= xH574 0)) (= xH191 (- (+ (- xH190 xH383) 750) xH575)) (or (= xH575 750) (= xH575 0)) (= xH192 (- (+ (- xH191 xH384) 750) xH576)) (or (= xH576 750) (= xH576 0)) (<= 0 xH1) (<= xH1 10000) (<= 0 xH2) (<= xH2 10000) (<= 0 xH3) (<= xH3 10000) (<= 0 xH4) (<= xH4 10000) (<= 0 xH5) (<= xH5 10000) (<= 0 xH6) (<= xH6 10000) (<= 0 xH7) (<= xH7 10000) (<= 0 xH8) (<= xH8 10000) (<= 0 xH9) (<= xH9 10000) (<= 0 xH10) (<= xH10 10000) (<= 0 xH11) (<= xH11 10000) (<= 0 xH12) (<= xH12 10000) (<= 0 xH13) (<= xH13 10000) (<= 0 xH14) (<= xH14 10000) (<= 0 xH15) (<= xH15 10000) (<= 0 xH16) (<= xH16 10000) (<= 0 xH17) (<= xH17 10000) (<= 0 xH18) (<= xH18 10000) (<= 0 xH19) (<= xH19 10000) (<= 0 xH20) (<= xH20 10000) (<= 0 xH21) (<= xH21 10000) (<= 0 xH22) (<= xH22 10000) (<= 0 xH23) (<= xH23 10000) (= xH24 0) (<= 0 xH25) (<= xH25 5000) (<= 0 xH26) (<= xH26 5000) (<= 0 xH27) (<= xH27 5000) (<= 0 xH28) (<= xH28 5000) (<= 0 xH29) (<= xH29 5000) (<= 0 xH30) (<= xH30 5000) (<= 0 xH31) (<= xH31 5000) (<= 0 xH32) (<= xH32 5000) (<= 0 xH33) (<= xH33 5000) (<= 0 xH34) (<= xH34 5000) (<= 0 xH35) (<= xH35 5000) (<= 0 xH36) (<= xH36 5000) (<= 0 xH37) (<= xH37 5000) (<= 0 xH38) (<= xH38 5000) (<= 0 xH39) (<= xH39 5000) (<= 0 xH40) (<= xH40 5000) (<= 0 xH41) (<= xH41 5000) (<= 0 xH42) (<= xH42 5000) (<= 0 xH43) (<= xH43 5000) (<= 0 xH44) (<= xH44 5000) (<= 0 xH45) (<= xH45 5000) (<= 0 xH46) (<= xH46 5000) (<= 0 xH47) (<= xH47 5000) (= xH48 0) (<= 0 xH49) (<= xH49 5000) (<= 0 xH50) (<= xH50 5000) (<= 0 xH51) (<= xH51 5000) (<= 0 xH52) (<= xH52 5000) (<= 0 xH53) (<= xH53 5000) (<= 0 xH54) (<= xH54 5000) (<= 0 xH55) (<= xH55 5000) (<= 0 xH56) (<= xH56 5000) (<= 0 xH57) (<= xH57 5000) (<= 0 xH58) (<= xH58 5000) (<= 0 xH59) (<= xH59 5000) (<= 0 xH60) (<= xH60 5000) (<= 0 xH61) (<= xH61 5000) (<= 0 xH62) (<= xH62 5000) (<= 0 xH63) (<= xH63 5000) (<= 0 xH64) (<= xH64 5000) (<= 0 xH65) (<= xH65 5000) (<= 0 xH66) (<= xH66 5000) (<= 0 xH67) (<= xH67 5000) (<= 0 xH68) (<= xH68 5000) (<= 0 xH69) (<= xH69 5000) (<= 0 xH70) (<= xH70 5000) (<= 0 xH71) (<= xH71 5000) (= xH72 0) (<= 0 xH73) (<= xH73 10000) (<= 0 xH74) (<= xH74 10000) (<= 0 xH75) (<= xH75 10000) (<= 0 xH76) (<= xH76 10000) (<= 0 xH77) (<= xH77 10000) (<= 0 xH78) (<= xH78 10000) (<= 0 xH79) (<= xH79 10000) (<= 0 xH80) (<= xH80 10000) (<= 0 xH81) (<= xH81 10000) (<= 0 xH82) (<= xH82 10000) (<= 0 xH83) (<= xH83 10000) (<= 0 xH84) (<= xH84 10000) (<= 0 xH85) (<= xH85 10000) (<= 0 xH86) (<= xH86 10000) (<= 0 xH87) (<= xH87 10000) (<= 0 xH88) (<= xH88 10000) (<= 0 xH89) (<= xH89 10000) (<= 0 xH90) (<= xH90 10000) (<= 0 xH91) (<= xH91 10000) (<= 0 xH92) (<= xH92 10000) (<= 0 xH93) (<= xH93 10000) (<= 0 xH94) (<= xH94 10000) (<= 0 xH95) (<= xH95 10000) (= xH96 0) (<= 0 xH97) (<= xH97 5000) (<= 0 xH98) (<= xH98 5000) (<= 0 xH99) (<= xH99 5000) (<= 0 xH100) (<= xH100 5000) (<= 0 xH101) (<= xH101 5000) (<= 0 xH102) (<= xH102 5000) (<= 0 xH103) (<= xH103 5000) (<= 0 xH104) (<= xH104 5000) (<= 0 xH105) (<= xH105 5000) (<= 0 xH106) (<= xH106 5000) (<= 0 xH107) (<= xH107 5000) (<= 0 xH108) (<= xH108 5000) (<= 0 xH109) (<= xH109 5000) (<= 0 xH110) (<= xH110 5000) (<= 0 xH111) (<= xH111 5000) (<= 0 xH112) (<= xH112 5000) (<= 0 xH113) (<= xH113 5000) (<= 0 xH114) (<= xH114 5000) (<= 0 xH115) (<= xH115 5000) (<= 0 xH116) (<= xH116 5000) (<= 0 xH117) (<= xH117 5000) (<= 0 xH118) (<= xH118 5000) (<= 0 xH119) (<= xH119 5000) (= xH120 0) (<= 0 xH121) (<= xH121 5000) (<= 0 xH122) (<= xH122 5000) (<= 0 xH123) (<= xH123 5000) (<= 0 xH124) (<= xH124 5000) (<= 0 xH125) (<= xH125 5000) (<= 0 xH126) (<= xH126 5000) (<= 0 xH127) (<= xH127 5000) (<= 0 xH128) (<= xH128 5000) (<= 0 xH129) (<= xH129 5000) (<= 0 xH130) (<= xH130 5000) (<= 0 xH131) (<= xH131 5000) (<= 0 xH132) (<= xH132 5000) (<= 0 xH133) (<= xH133 5000) (<= 0 xH134) (<= xH134 5000) (<= 0 xH135) (<= xH135 5000) (<= 0 xH136) (<= xH136 5000) (<= 0 xH137) (<= xH137 5000) (<= 0 xH138) (<= xH138 5000) (<= 0 xH139) (<= xH139 5000) (<= 0 xH140) (<= xH140 5000) (<= 0 xH141) (<= xH141 5000) (<= 0 xH142) (<= xH142 5000) (<= 0 xH143) (<= xH143 5000) (= xH144 0) (<= 0 xH145) (<= xH145 10000) (<= 0 xH146) (<= xH146 10000) (<= 0 xH147) (<= xH147 10000) (<= 0 xH148) (<= xH148 10000) (<= 0 xH149) (<= xH149 10000) (<= 0 xH150) (<= xH150 10000) (<= 0 xH151) (<= xH151 10000) (<= 0 xH152) (<= xH152 10000) (<= 0 xH153) (<= xH153 10000) (<= 0 xH154) (<= xH154 10000) (<= 0 xH155) (<= xH155 10000) (<= 0 xH156) (<= xH156 10000) (<= 0 xH157) (<= xH157 10000) (<= 0 xH158) (<= xH158 10000) (<= 0 xH159) (<= xH159 10000) (<= 0 xH160) (<= xH160 10000) (<= 0 xH161) (<= xH161 10000) (<= 0 xH162) (<= xH162 10000) (<= 0 xH163) (<= xH163 10000) (<= 0 xH164) (<= xH164 10000) (<= 0 xH165) (<= xH165 10000) (<= 0 xH166) (<= xH166 10000) (<= 0 xH167) (<= xH167 10000) (= xH168 0) (<= 0 xH169) (<= xH169 10000) (<= 0 xH170) (<= xH170 10000) (<= 0 xH171) (<= xH171 10000) (<= 0 xH172) (<= xH172 10000) (<= 0 xH173) (<= xH173 10000) (<= 0 xH174) (<= xH174 10000) (<= 0 xH175) (<= xH175 10000) (<= 0 xH176) (<= xH176 10000) (<= 0 xH177) (<= xH177 10000) (<= 0 xH178) (<= xH178 10000) (<= 0 xH179) (<= xH179 10000) (<= 0 xH180) (<= xH180 10000) (<= 0 xH181) (<= xH181 10000) (<= 0 xH182) (<= xH182 10000) (<= 0 xH183) (<= xH183 10000) (<= 0 xH184) (<= xH184 10000) (<= 0 xH185) (<= xH185 10000) (<= 0 xH186) (<= xH186 10000) (<= 0 xH187) (<= xH187 10000) (<= 0 xH188) (<= xH188 10000) (<= 0 xH189) (<= xH189 10000) (<= 0 xH190) (<= xH190 10000) (<= 0 xH191) (<= xH191 10000) (= xH192 0) (= xH193 0) (or (= xH194 0) (and (= xH194 2500) (>= xH1 2500)) (and (= xH194 xH1) (<= xH1 2500))) (or (= xH195 0) (and (= xH195 2500) (>= xH2 2500)) (and (= xH195 xH2) (<= xH2 2500))) (or (= xH196 0) (and (= xH196 2500) (>= xH3 2500)) (and (= xH196 xH3) (<= xH3 2500))) (or (= xH197 0) (and (= xH197 2500) (>= xH4 2500)) (and (= xH197 xH4) (<= xH4 2500))) (or (= xH198 0) (and (= xH198 2500) (>= xH5 2500)) (and (= xH198 xH5) (<= xH5 2500))) (or (= xH199 0) (and (= xH199 2500) (>= xH6 2500)) (and (= xH199 xH6) (<= xH6 2500))) (or (= xH200 0) (and (= xH200 2500) (>= xH7 2500)) (and (= xH200 xH7) (<= xH7 2500))) (or (= xH201 0) (and (= xH201 2500) (>= xH8 2500)) (and (= xH201 xH8) (<= xH8 2500))) (or (= xH202 0) (and (= xH202 2500) (>= xH9 2500)) (and (= xH202 xH9) (<= xH9 2500))) (or (= xH203 0) (and (= xH203 2500) (>= xH10 2500)) (and (= xH203 xH10) (<= xH10 2500))) (or (= xH204 0) (and (= xH204 2500) (>= xH11 2500)) (and (= xH204 xH11) (<= xH11 2500))) (or (= xH205 0) (and (= xH205 2500) (>= xH12 2500)) (and (= xH205 xH12) (<= xH12 2500))) (or (= xH206 0) (and (= xH206 2500) (>= xH13 2500)) (and (= xH206 xH13) (<= xH13 2500))) (or (= xH207 0) (and (= xH207 2500) (>= xH14 2500)) (and (= xH207 xH14) (<= xH14 2500))) (or (= xH208 0) (and (= xH208 2500) (>= xH15 2500)) (and (= xH208 xH15) (<= xH15 2500))) (or (= xH209 0) (and (= xH209 2500) (>= xH16 2500)) (and (= xH209 xH16) (<= xH16 2500))) (or (= xH210 0) (and (= xH210 2500) (>= xH17 2500)) (and (= xH210 xH17) (<= xH17 2500))) (or (= xH211 0) (and (= xH211 2500) (>= xH18 2500)) (and (= xH211 xH18) (<= xH18 2500))) (or (= xH212 0) (and (= xH212 2500) (>= xH19 2500)) (and (= xH212 xH19) (<= xH19 2500))) (or (= xH213 0) (and (= xH213 2500) (>= xH20 2500)) (and (= xH213 xH20) (<= xH20 2500))) (or (= xH214 0) (and (= xH214 2500) (>= xH21 2500)) (and (= xH214 xH21) (<= xH21 2500))) (or (= xH215 0) (and (= xH215 2500) (>= xH22 2500)) (and (= xH215 xH22) (<= xH22 2500))) (or (= xH216 0) (and (= xH216 2500) (>= xH23 2500)) (and (= xH216 xH23) (<= xH23 2500))) (= xH217 0) (or (= xH218 0) (and (= xH218 3000) (>= xH25 3000)) (and (= xH218 xH25) (<= xH25 3000))) (or (= xH219 0) (and (= xH219 3000) (>= xH26 3000)) (and (= xH219 xH26) (<= xH26 3000))) (or (= xH220 0) (and (= xH220 3000) (>= xH27 3000)) (and (= xH220 xH27) (<= xH27 3000))) (or (= xH221 0) (and (= xH221 3000) (>= xH28 3000)) (and (= xH221 xH28) (<= xH28 3000))) (or (= xH222 0) (and (= xH222 3000) (>= xH29 3000)) (and (= xH222 xH29) (<= xH29 3000))) (or (= xH223 0) (and (= xH223 3000) (>= xH30 3000)) (and (= xH223 xH30) (<= xH30 3000))) (or (= xH224 0) (and (= xH224 3000) (>= xH31 3000)) (and (= xH224 xH31) (<= xH31 3000))) (or (= xH225 0) (and (= xH225 3000) (>= xH32 3000)) (and (= xH225 xH32) (<= xH32 3000))) (or (= xH226 0) (and (= xH226 3000) (>= xH33 3000)) (and (= xH226 xH33) (<= xH33 3000))) (or (= xH227 0) (and (= xH227 3000) (>= xH34 3000)) (and (= xH227 xH34) (<= xH34 3000))) (or (= xH228 0) (and (= xH228 3000) (>= xH35 3000)) (and (= xH228 xH35) (<= xH35 3000))) (or (= xH229 0) (and (= xH229 3000) (>= xH36 3000)) (and (= xH229 xH36) (<= xH36 3000))) (or (= xH230 0) (and (= xH230 3000) (>= xH37 3000)) (and (= xH230 xH37) (<= xH37 3000))) (or (= xH231 0) (and (= xH231 3000) (>= xH38 3000)) (and (= xH231 xH38) (<= xH38 3000))) (or (= xH232 0) (and (= xH232 3000) (>= xH39 3000)) (and (= xH232 xH39) (<= xH39 3000))) (or (= xH233 0) (and (= xH233 3000) (>= xH40 3000)) (and (= xH233 xH40) (<= xH40 3000))) (or (= xH234 0) (and (= xH234 3000) (>= xH41 3000)) (and (= xH234 xH41) (<= xH41 3000))) (or (= xH235 0) (and (= xH235 3000) (>= xH42 3000)) (and (= xH235 xH42) (<= xH42 3000))) (or (= xH236 0) (and (= xH236 3000) (>= xH43 3000)) (and (= xH236 xH43) (<= xH43 3000))) (or (= xH237 0) (and (= xH237 3000) (>= xH44 3000)) (and (= xH237 xH44) (<= xH44 3000))) (or (= xH238 0) (and (= xH238 3000) (>= xH45 3000)) (and (= xH238 xH45) (<= xH45 3000))) (or (= xH239 0) (and (= xH239 3000) (>= xH46 3000)) (and (= xH239 xH46) (<= xH46 3000))) (or (= xH240 0) (and (= xH240 3000) (>= xH47 3000)) (and (= xH240 xH47) (<= xH47 3000))) (= xH241 0) (or (= xH242 0) (and (= xH242 1500) (>= xH49 1500)) (and (= xH242 xH49) (<= xH49 1500))) (or (= xH243 0) (and (= xH243 1500) (>= xH50 1500)) (and (= xH243 xH50) (<= xH50 1500))) (or (= xH244 0) (and (= xH244 1500) (>= xH51 1500)) (and (= xH244 xH51) (<= xH51 1500))) (or (= xH245 0) (and (= xH245 1500) (>= xH52 1500)) (and (= xH245 xH52) (<= xH52 1500))) (or (= xH246 0) (and (= xH246 1500) (>= xH53 1500)) (and (= xH246 xH53) (<= xH53 1500))) (or (= xH247 0) (and (= xH247 1500) (>= xH54 1500)) (and (= xH247 xH54) (<= xH54 1500))) (or (= xH248 0) (and (= xH248 1500) (>= xH55 1500)) (and (= xH248 xH55) (<= xH55 1500))) (or (= xH249 0) (and (= xH249 1500) (>= xH56 1500)) (and (= xH249 xH56) (<= xH56 1500))) (or (= xH250 0) (and (= xH250 1500) (>= xH57 1500)) (and (= xH250 xH57) (<= xH57 1500))) (or (= xH251 0) (and (= xH251 1500) (>= xH58 1500)) (and (= xH251 xH58) (<= xH58 1500))) (or (= xH252 0) (and (= xH252 1500) (>= xH59 1500)) (and (= xH252 xH59) (<= xH59 1500))) (or (= xH253 0) (and (= xH253 1500) (>= xH60 1500)) (and (= xH253 xH60) (<= xH60 1500))) (or (= xH254 0) (and (= xH254 1500) (>= xH61 1500)) (and (= xH254 xH61) (<= xH61 1500))) (or (= xH255 0) (and (= xH255 1500) (>= xH62 1500)) (and (= xH255 xH62) (<= xH62 1500))) (or (= xH256 0) (and (= xH256 1500) (>= xH63 1500)) (and (= xH256 xH63) (<= xH63 1500))) (or (= xH257 0) (and (= xH257 1500) (>= xH64 1500)) (and (= xH257 xH64) (<= xH64 1500))) (or (= xH258 0) (and (= xH258 1500) (>= xH65 1500)) (and (= xH258 xH65) (<= xH65 1500))) (or (= xH259 0) (and (= xH259 1500) (>= xH66 1500)) (and (= xH259 xH66) (<= xH66 1500))) (or (= xH260 0) (and (= xH260 1500) (>= xH67 1500)) (and (= xH260 xH67) (<= xH67 1500))) (or (= xH261 0) (and (= xH261 1500) (>= xH68 1500)) (and (= xH261 xH68) (<= xH68 1500))) (or (= xH262 0) (and (= xH262 1500) (>= xH69 1500)) (and (= xH262 xH69) (<= xH69 1500))) (or (= xH263 0) (and (= xH263 1500) (>= xH70 1500)) (and (= xH263 xH70) (<= xH70 1500))) (or (= xH264 0) (and (= xH264 1500) (>= xH71 1500)) (and (= xH264 xH71) (<= xH71 1500))) (= xH265 0) (or (= xH266 0) (and (= xH266 1000) (>= xH73 1000)) (and (= xH266 xH73) (<= xH73 1000))) (or (= xH267 0) (and (= xH267 1000) (>= xH74 1000)) (and (= xH267 xH74) (<= xH74 1000))) (or (= xH268 0) (and (= xH268 1000) (>= xH75 1000)) (and (= xH268 xH75) (<= xH75 1000))) (or (= xH269 0) (and (= xH269 1000) (>= xH76 1000)) (and (= xH269 xH76) (<= xH76 1000))) (or (= xH270 0) (and (= xH270 1000) (>= xH77 1000)) (and (= xH270 xH77) (<= xH77 1000))) (or (= xH271 0) (and (= xH271 1000) (>= xH78 1000)) (and (= xH271 xH78) (<= xH78 1000))) (or (= xH272 0) (and (= xH272 1000) (>= xH79 1000)) (and (= xH272 xH79) (<= xH79 1000))) (or (= xH273 0) (and (= xH273 1000) (>= xH80 1000)) (and (= xH273 xH80) (<= xH80 1000))) (or (= xH274 0) (and (= xH274 1000) (>= xH81 1000)) (and (= xH274 xH81) (<= xH81 1000))) (or (= xH275 0) (and (= xH275 1000) (>= xH82 1000)) (and (= xH275 xH82) (<= xH82 1000))) (or (= xH276 0) (and (= xH276 1000) (>= xH83 1000)) (and (= xH276 xH83) (<= xH83 1000))) (or (= xH277 0) (and (= xH277 1000) (>= xH84 1000)) (and (= xH277 xH84) (<= xH84 1000))) (or (= xH278 0) (and (= xH278 1000) (>= xH85 1000)) (and (= xH278 xH85) (<= xH85 1000))) (or (= xH279 0) (and (= xH279 1000) (>= xH86 1000)) (and (= xH279 xH86) (<= xH86 1000))) (or (= xH280 0) (and (= xH280 1000) (>= xH87 1000)) (and (= xH280 xH87) (<= xH87 1000))) (or (= xH281 0) (and (= xH281 1000) (>= xH88 1000)) (and (= xH281 xH88) (<= xH88 1000))) (or (= xH282 0) (and (= xH282 1000) (>= xH89 1000)) (and (= xH282 xH89) (<= xH89 1000))) (or (= xH283 0) (and (= xH283 1000) (>= xH90 1000)) (and (= xH283 xH90) (<= xH90 1000))) (or (= xH284 0) (and (= xH284 1000) (>= xH91 1000)) (and (= xH284 xH91) (<= xH91 1000))) (or (= xH285 0) (and (= xH285 1000) (>= xH92 1000)) (and (= xH285 xH92) (<= xH92 1000))) (or (= xH286 0) (and (= xH286 1000) (>= xH93 1000)) (and (= xH286 xH93) (<= xH93 1000))) (or (= xH287 0) (and (= xH287 1000) (>= xH94 1000)) (and (= xH287 xH94) (<= xH94 1000))) (or (= xH288 0) (and (= xH288 1000) (>= xH95 1000)) (and (= xH288 xH95) (<= xH95 1000))) (= xH289 0) (or (= xH290 0) (and (= xH290 3000) (>= xH97 3000)) (and (= xH290 xH97) (<= xH97 3000))) (or (= xH291 0) (and (= xH291 3000) (>= xH98 3000)) (and (= xH291 xH98) (<= xH98 3000))) (or (= xH292 0) (and (= xH292 3000) (>= xH99 3000)) (and (= xH292 xH99) (<= xH99 3000))) (or (= xH293 0) (and (= xH293 3000) (>= xH100 3000)) (and (= xH293 xH100) (<= xH100 3000))) (or (= xH294 0) (and (= xH294 3000) (>= xH101 3000)) (and (= xH294 xH101) (<= xH101 3000))) (or (= xH295 0) (and (= xH295 3000) (>= xH102 3000)) (and (= xH295 xH102) (<= xH102 3000))) (or (= xH296 0) (and (= xH296 3000) (>= xH103 3000)) (and (= xH296 xH103) (<= xH103 3000))) (or (= xH297 0) (and (= xH297 3000) (>= xH104 3000)) (and (= xH297 xH104) (<= xH104 3000))) (or (= xH298 0) (and (= xH298 3000) (>= xH105 3000)) (and (= xH298 xH105) (<= xH105 3000))) (or (= xH299 0) (and (= xH299 3000) (>= xH106 3000)) (and (= xH299 xH106) (<= xH106 3000))) (or (= xH300 0) (and (= xH300 3000) (>= xH107 3000)) (and (= xH300 xH107) (<= xH107 3000))) (or (= xH301 0) (and (= xH301 3000) (>= xH108 3000)) (and (= xH301 xH108) (<= xH108 3000))) (or (= xH302 0) (and (= xH302 3000) (>= xH109 3000)) (and (= xH302 xH109) (<= xH109 3000))) (or (= xH303 0) (and (= xH303 3000) (>= xH110 3000)) (and (= xH303 xH110) (<= xH110 3000))) (or (= xH304 0) (and (= xH304 3000) (>= xH111 3000)) (and (= xH304 xH111) (<= xH111 3000))) (or (= xH305 0) (and (= xH305 3000) (>= xH112 3000)) (and (= xH305 xH112) (<= xH112 3000))) (or (= xH306 0) (and (= xH306 3000) (>= xH113 3000)) (and (= xH306 xH113) (<= xH113 3000))) (or (= xH307 0) (and (= xH307 3000) (>= xH114 3000)) (and (= xH307 xH114) (<= xH114 3000))) (or (= xH308 0) (and (= xH308 3000) (>= xH115 3000)) (and (= xH308 xH115) (<= xH115 3000))) (or (= xH309 0) (and (= xH309 3000) (>= xH116 3000)) (and (= xH309 xH116) (<= xH116 3000))) (or (= xH310 0) (and (= xH310 3000) (>= xH117 3000)) (and (= xH310 xH117) (<= xH117 3000))) (or (= xH311 0) (and (= xH311 3000) (>= xH118 3000)) (and (= xH311 xH118) (<= xH118 3000))) (or (= xH312 0) (and (= xH312 3000) (>= xH119 3000)) (and (= xH312 xH119) (<= xH119 3000))) (= xH313 0) (or (= xH314 0) (and (= xH314 1500) (>= xH121 1500)) (and (= xH314 xH121) (<= xH121 1500))) (or (= xH315 0) (and (= xH315 1500) (>= xH122 1500)) (and (= xH315 xH122) (<= xH122 1500))) (or (= xH316 0) (and (= xH316 1500) (>= xH123 1500)) (and (= xH316 xH123) (<= xH123 1500))) (or (= xH317 0) (and (= xH317 1500) (>= xH124 1500)) (and (= xH317 xH124) (<= xH124 1500))) (or (= xH318 0) (and (= xH318 1500) (>= xH125 1500)) (and (= xH318 xH125) (<= xH125 1500))) (or (= xH319 0) (and (= xH319 1500) (>= xH126 1500)) (and (= xH319 xH126) (<= xH126 1500))) (or (= xH320 0) (and (= xH320 1500) (>= xH127 1500)) (and (= xH320 xH127) (<= xH127 1500))) (or (= xH321 0) (and (= xH321 1500) (>= xH128 1500)) (and (= xH321 xH128) (<= xH128 1500))) (or (= xH322 0) (and (= xH322 1500) (>= xH129 1500)) (and (= xH322 xH129) (<= xH129 1500))) (or (= xH323 0) (and (= xH323 1500) (>= xH130 1500)) (and (= xH323 xH130) (<= xH130 1500))) (or (= xH324 0) (and (= xH324 1500) (>= xH131 1500)) (and (= xH324 xH131) (<= xH131 1500))) (or (= xH325 0) (and (= xH325 1500) (>= xH132 1500)) (and (= xH325 xH132) (<= xH132 1500))) (or (= xH326 0) (and (= xH326 1500) (>= xH133 1500)) (and (= xH326 xH133) (<= xH133 1500))) (or (= xH327 0) (and (= xH327 1500) (>= xH134 1500)) (and (= xH327 xH134) (<= xH134 1500))) (or (= xH328 0) (and (= xH328 1500) (>= xH135 1500)) (and (= xH328 xH135) (<= xH135 1500))) (or (= xH329 0) (and (= xH329 1500) (>= xH136 1500)) (and (= xH329 xH136) (<= xH136 1500))) (or (= xH330 0) (and (= xH330 1500) (>= xH137 1500)) (and (= xH330 xH137) (<= xH137 1500))) (or (= xH331 0) (and (= xH331 1500) (>= xH138 1500)) (and (= xH331 xH138) (<= xH138 1500))) (or (= xH332 0) (and (= xH332 1500) (>= xH139 1500)) (and (= xH332 xH139) (<= xH139 1500))) (or (= xH333 0) (and (= xH333 1500) (>= xH140 1500)) (and (= xH333 xH140) (<= xH140 1500))) (or (= xH334 0) (and (= xH334 1500) (>= xH141 1500)) (and (= xH334 xH141) (<= xH141 1500))) (or (= xH335 0) (and (= xH335 1500) (>= xH142 1500)) (and (= xH335 xH142) (<= xH142 1500))) (or (= xH336 0) (and (= xH336 1500) (>= xH143 1500)) (and (= xH336 xH143) (<= xH143 1500))) (= xH337 0) (or (= xH338 0) (and (= xH338 1000) (>= xH145 1000)) (and (= xH338 xH145) (<= xH145 1000))) (or (= xH339 0) (and (= xH339 1000) (>= xH146 1000)) (and (= xH339 xH146) (<= xH146 1000))) (or (= xH340 0) (and (= xH340 1000) (>= xH147 1000)) (and (= xH340 xH147) (<= xH147 1000))) (or (= xH341 0) (and (= xH341 1000) (>= xH148 1000)) (and (= xH341 xH148) (<= xH148 1000))) (or (= xH342 0) (and (= xH342 1000) (>= xH149 1000)) (and (= xH342 xH149) (<= xH149 1000))) (or (= xH343 0) (and (= xH343 1000) (>= xH150 1000)) (and (= xH343 xH150) (<= xH150 1000))) (or (= xH344 0) (and (= xH344 1000) (>= xH151 1000)) (and (= xH344 xH151) (<= xH151 1000))) (or (= xH345 0) (and (= xH345 1000) (>= xH152 1000)) (and (= xH345 xH152) (<= xH152 1000))) (or (= xH346 0) (and (= xH346 1000) (>= xH153 1000)) (and (= xH346 xH153) (<= xH153 1000))) (or (= xH347 0) (and (= xH347 1000) (>= xH154 1000)) (and (= xH347 xH154) (<= xH154 1000))) (or (= xH348 0) (and (= xH348 1000) (>= xH155 1000)) (and (= xH348 xH155) (<= xH155 1000))) (or (= xH349 0) (and (= xH349 1000) (>= xH156 1000)) (and (= xH349 xH156) (<= xH156 1000))) (or (= xH350 0) (and (= xH350 1000) (>= xH157 1000)) (and (= xH350 xH157) (<= xH157 1000))) (or (= xH351 0) (and (= xH351 1000) (>= xH158 1000)) (and (= xH351 xH158) (<= xH158 1000))) (or (= xH352 0) (and (= xH352 1000) (>= xH159 1000)) (and (= xH352 xH159) (<= xH159 1000))) (or (= xH353 0) (and (= xH353 1000) (>= xH160 1000)) (and (= xH353 xH160) (<= xH160 1000))) (or (= xH354 0) (and (= xH354 1000) (>= xH161 1000)) (and (= xH354 xH161) (<= xH161 1000))) (or (= xH355 0) (and (= xH355 1000) (>= xH162 1000)) (and (= xH355 xH162) (<= xH162 1000))) (or (= xH356 0) (and (= xH356 1000) (>= xH163 1000)) (and (= xH356 xH163) (<= xH163 1000))) (or (= xH357 0) (and (= xH357 1000) (>= xH164 1000)) (and (= xH357 xH164) (<= xH164 1000))) (or (= xH358 0) (and (= xH358 1000) (>= xH165 1000)) (and (= xH358 xH165) (<= xH165 1000))) (or (= xH359 0) (and (= xH359 1000) (>= xH166 1000)) (and (= xH359 xH166) (<= xH166 1000))) (or (= xH360 0) (and (= xH360 1000) (>= xH167 1000)) (and (= xH360 xH167) (<= xH167 1000))) (= xH361 0) (or (= xH362 0) (and (= xH362 2500) (>= xH169 2500)) (and (= xH362 xH169) (<= xH169 2500))) (or (= xH363 0) (and (= xH363 2500) (>= xH170 2500)) (and (= xH363 xH170) (<= xH170 2500))) (or (= xH364 0) (and (= xH364 2500) (>= xH171 2500)) (and (= xH364 xH171) (<= xH171 2500))) (or (= xH365 0) (and (= xH365 2500) (>= xH172 2500)) (and (= xH365 xH172) (<= xH172 2500))) (or (= xH366 0) (and (= xH366 2500) (>= xH173 2500)) (and (= xH366 xH173) (<= xH173 2500))) (or (= xH367 0) (and (= xH367 2500) (>= xH174 2500)) (and (= xH367 xH174) (<= xH174 2500))) (or (= xH368 0) (and (= xH368 2500) (>= xH175 2500)) (and (= xH368 xH175) (<= xH175 2500))) (or (= xH369 0) (and (= xH369 2500) (>= xH176 2500)) (and (= xH369 xH176) (<= xH176 2500))) (or (= xH370 0) (and (= xH370 2500) (>= xH177 2500)) (and (= xH370 xH177) (<= xH177 2500))) (or (= xH371 0) (and (= xH371 2500) (>= xH178 2500)) (and (= xH371 xH178) (<= xH178 2500))) (or (= xH372 0) (and (= xH372 2500) (>= xH179 2500)) (and (= xH372 xH179) (<= xH179 2500))) (or (= xH373 0) (and (= xH373 2500) (>= xH180 2500)) (and (= xH373 xH180) (<= xH180 2500))) (or (= xH374 0) (and (= xH374 2500) (>= xH181 2500)) (and (= xH374 xH181) (<= xH181 2500))) (or (= xH375 0) (and (= xH375 2500) (>= xH182 2500)) (and (= xH375 xH182) (<= xH182 2500))) (or (= xH376 0) (and (= xH376 2500) (>= xH183 2500)) (and (= xH376 xH183) (<= xH183 2500))) (or (= xH377 0) (and (= xH377 2500) (>= xH184 2500)) (and (= xH377 xH184) (<= xH184 2500))) (or (= xH378 0) (and (= xH378 2500) (>= xH185 2500)) (and (= xH378 xH185) (<= xH185 2500))) (or (= xH379 0) (and (= xH379 2500) (>= xH186 2500)) (and (= xH379 xH186) (<= xH186 2500))) (or (= xH380 0) (and (= xH380 2500) (>= xH187 2500)) (and (= xH380 xH187) (<= xH187 2500))) (or (= xH381 0) (and (= xH381 2500) (>= xH188 2500)) (and (= xH381 xH188) (<= xH188 2500))) (or (= xH382 0) (and (= xH382 2500) (>= xH189 2500)) (and (= xH382 xH189) (<= xH189 2500))) (or (= xH383 0) (and (= xH383 2500) (>= xH190 2500)) (and (= xH383 xH190) (<= xH190 2500))) (or (= xH384 0) (and (= xH384 2500) (>= xH191 2500)) (and (= xH384 xH191) (<= xH191 2500))) (<= (+ xH385 xH409 xH433 xH457 xH481 xH505 xH529 xH553 xH193 xH217 xH241 xH265 xH289 xH313 xH337 xH361) 4960) (<= (+ xH386 xH410 xH434 xH458 xH482 xH506 xH530 xH554 xH194 xH218 xH242 xH266 xH290 xH314 xH338 xH362) 4960) (<= (+ xH387 xH411 xH435 xH459 xH483 xH507 xH531 xH555 xH195 xH219 xH243 xH267 xH291 xH315 xH339 xH363) 4960) (<= (+ xH388 xH412 xH436 xH460 xH484 xH508 xH532 xH556 xH196 xH220 xH244 xH268 xH292 xH316 xH340 xH364) 4960) (<= (+ xH389 xH413 xH437 xH461 xH485 xH509 xH533 xH557 xH197 xH221 xH245 xH269 xH293 xH317 xH341 xH365) 4960) (<= (+ xH390 xH414 xH438 xH462 xH486 xH510 xH534 xH558 xH198 xH222 xH246 xH270 xH294 xH318 xH342 xH366) 4960) (<= (+ xH391 xH415 xH439 xH463 xH487 xH511 xH535 xH559 xH199 xH223 xH247 xH271 xH295 xH319 xH343 xH367) 4960) (<= (+ xH392 xH416 xH440 xH464 xH488 xH512 xH536 xH560 xH200 xH224 xH248 xH272 xH296 xH320 xH344 xH368) 4960) (<= (+ xH393 xH417 xH441 xH465 xH489 xH513 xH537 xH561 xH201 xH225 xH249 xH273 xH297 xH321 xH345 xH369) 4960) (<= (+ xH394 xH418 xH442 xH466 xH490 xH514 xH538 xH562 xH202 xH226 xH250 xH274 xH298 xH322 xH346 xH370) 4960) (<= (+ xH395 xH419 xH443 xH467 xH491 xH515 xH539 xH563 xH203 xH227 xH251 xH275 xH299 xH323 xH347 xH371) 4960) (<= (+ xH396 xH420 xH444 xH468 xH492 xH516 xH540 xH564 xH204 xH228 xH252 xH276 xH300 xH324 xH348 xH372) 4960) (<= (+ xH397 xH421 xH445 xH469 xH493 xH517 xH541 xH565 xH205 xH229 xH253 xH277 xH301 xH325 xH349 xH373) 4960) (<= (+ xH398 xH422 xH446 xH470 xH494 xH518 xH542 xH566 xH206 xH230 xH254 xH278 xH302 xH326 xH350 xH374) 4960) (<= (+ xH399 xH423 xH447 xH471 xH495 xH519 xH543 xH567 xH207 xH231 xH255 xH279 xH303 xH327 xH351 xH375) 4960) (<= (+ xH400 xH424 xH448 xH472 xH496 xH520 xH544 xH568 xH208 xH232 xH256 xH280 xH304 xH328 xH352 xH376) 4960) (<= (+ xH401 xH425 xH449 xH473 xH497 xH521 xH545 xH569 xH209 xH233 xH257 xH281 xH305 xH329 xH353 xH377) 4960) (<= (+ xH402 xH426 xH450 xH474 xH498 xH522 xH546 xH570 xH210 xH234 xH258 xH282 xH306 xH330 xH354 xH378) 4960) (<= (+ xH403 xH427 xH451 xH475 xH499 xH523 xH547 xH571 xH211 xH235 xH259 xH283 xH307 xH331 xH355 xH379) 4960) (<= (+ xH404 xH428 xH452 xH476 xH500 xH524 xH548 xH572 xH212 xH236 xH260 xH284 xH308 xH332 xH356 xH380) 4960) (<= (+ xH405 xH429 xH453 xH477 xH501 xH525 xH549 xH573 xH213 xH237 xH261 xH285 xH309 xH333 xH357 xH381) 4960) (<= (+ xH406 xH430 xH454 xH478 xH502 xH526 xH550 xH574 xH214 xH238 xH262 xH286 xH310 xH334 xH358 xH382) 4960) (<= (+ xH407 xH431 xH455 xH479 xH503 xH527 xH551 xH575 xH215 xH239 xH263 xH287 xH311 xH335 xH359 xH383) 4960) (<= (+ xH408 xH432 xH456 xH480 xH504 xH528 xH552 xH576 xH216 xH240 xH264 xH288 xH312 xH336 xH360 xH384) 4960) (<= 0 xH193) (<= xH193 2500) (<= 0 xH194) (<= xH194 2500) (<= 0 xH195) (<= xH195 2500) (<= 0 xH196) (<= xH196 2500) (<= 0 xH197) (<= xH197 2500) (<= 0 xH198) (<= xH198 2500) (<= 0 xH199) (<= xH199 2500) (<= 0 xH200) (<= xH200 2500) (<= 0 xH201) (<= xH201 2500) (<= 0 xH202) (<= xH202 2500) (<= 0 xH203) (<= xH203 2500) (<= 0 xH204) (<= xH204 2500) (<= 0 xH205) (<= xH205 2500) (<= 0 xH206) (<= xH206 2500) (<= 0 xH207) (<= xH207 2500) (<= 0 xH208) (<= xH208 2500) (<= 0 xH209) (<= xH209 2500) (<= 0 xH210) (<= xH210 2500) (<= 0 xH211) (<= xH211 2500) (<= 0 xH212) (<= xH212 2500) (<= 0 xH213) (<= xH213 2500) (<= 0 xH214) (<= xH214 2500) (<= 0 xH215) (<= xH215 2500) (<= 0 xH216) (<= xH216 2500) (<= 0 xH217) (<= xH217 3000) (<= 0 xH218) (<= xH218 3000) (<= 0 xH219) (<= xH219 3000) (<= 0 xH220) (<= xH220 3000) (<= 0 xH221) (<= xH221 3000) (<= 0 xH222) (<= xH222 3000) (<= 0 xH223) (<= xH223 3000) (<= 0 xH224) (<= xH224 3000) (<= 0 xH225) (<= xH225 3000) (<= 0 xH226) (<= xH226 3000) (<= 0 xH227) (<= xH227 3000) (<= 0 xH228) (<= xH228 3000) (<= 0 xH229) (<= xH229 3000) (<= 0 xH230) (<= xH230 3000) (<= 0 xH231) (<= xH231 3000) (<= 0 xH232) (<= xH232 3000) (<= 0 xH233) (<= xH233 3000) (<= 0 xH234) (<= xH234 3000) (<= 0 xH235) (<= xH235 3000) (<= 0 xH236) (<= xH236 3000) (<= 0 xH237) (<= xH237 3000) (<= 0 xH238) (<= xH238 3000) (<= 0 xH239) (<= xH239 3000) (<= 0 xH240) (<= xH240 3000) (<= 0 xH241) (<= xH241 1500) (<= 0 xH242) (<= xH242 1500) (<= 0 xH243) (<= xH243 1500) (<= 0 xH244) (<= xH244 1500) (<= 0 xH245) (<= xH245 1500) (<= 0 xH246) (<= xH246 1500) (<= 0 xH247) (<= xH247 1500) (<= 0 xH248) (<= xH248 1500) (<= 0 xH249) (<= xH249 1500) (<= 0 xH250) (<= xH250 1500) (<= 0 xH251) (<= xH251 1500) (<= 0 xH252) (<= xH252 1500) (<= 0 xH253) (<= xH253 1500) (<= 0 xH254) (<= xH254 1500) (<= 0 xH255) (<= xH255 1500) (<= 0 xH256) (<= xH256 1500) (<= 0 xH257) (<= xH257 1500) (<= 0 xH258) (<= xH258 1500) (<= 0 xH259) (<= xH259 1500) (<= 0 xH260) (<= xH260 1500) (<= 0 xH261) (<= xH261 1500) (<= 0 xH262) (<= xH262 1500) (<= 0 xH263) (<= xH263 1500) (<= 0 xH264) (<= xH264 1500) (<= 0 xH265) (<= xH265 1000) (<= 0 xH266) (<= xH266 1000) (<= 0 xH267) (<= xH267 1000) (<= 0 xH268) (<= xH268 1000) (<= 0 xH269) (<= xH269 1000) (<= 0 xH270) (<= xH270 1000) (<= 0 xH271) (<= xH271 1000) (<= 0 xH272) (<= xH272 1000) (<= 0 xH273) (<= xH273 1000) (<= 0 xH274) (<= xH274 1000) (<= 0 xH275) (<= xH275 1000) (<= 0 xH276) (<= xH276 1000) (<= 0 xH277) (<= xH277 1000) (<= 0 xH278) (<= xH278 1000) (<= 0 xH279) (<= xH279 1000) (<= 0 xH280) (<= xH280 1000) (<= 0 xH281) (<= xH281 1000) (<= 0 xH282) (<= xH282 1000) (<= 0 xH283) (<= xH283 1000) (<= 0 xH284) (<= xH284 1000) (<= 0 xH285) (<= xH285 1000) (<= 0 xH286) (<= xH286 1000) (<= 0 xH287) (<= xH287 1000) (<= 0 xH288) (<= xH288 1000) (<= 0 xH289) (<= xH289 3000) (<= 0 xH290) (<= xH290 3000) (<= 0 xH291) (<= xH291 3000) (<= 0 xH292) (<= xH292 3000) (<= 0 xH293) (<= xH293 3000) (<= 0 xH294) (<= xH294 3000) (<= 0 xH295) (<= xH295 3000) (<= 0 xH296) (<= xH296 3000) (<= 0 xH297) (<= xH297 3000) (<= 0 xH298) (<= xH298 3000) (<= 0 xH299) (<= xH299 3000) (<= 0 xH300) (<= xH300 3000) (<= 0 xH301) (<= xH301 3000) (<= 0 xH302) (<= xH302 3000) (<= 0 xH303) (<= xH303 3000) (<= 0 xH304) (<= xH304 3000) (<= 0 xH305) (<= xH305 3000) (<= 0 xH306) (<= xH306 3000) (<= 0 xH307) (<= xH307 3000) (<= 0 xH308) (<= xH308 3000) (<= 0 xH309) (<= xH309 3000) (<= 0 xH310) (<= xH310 3000) (<= 0 xH311) (<= xH311 3000) (<= 0 xH312) (<= xH312 3000) (<= 0 xH313) (<= xH313 1500) (<= 0 xH314) (<= xH314 1500) (<= 0 xH315) (<= xH315 1500) (<= 0 xH316) (<= xH316 1500) (<= 0 xH317) (<= xH317 1500) (<= 0 xH318) (<= xH318 1500) (<= 0 xH319) (<= xH319 1500) (<= 0 xH320) (<= xH320 1500) (<= 0 xH321) (<= xH321 1500) (<= 0 xH322) (<= xH322 1500) (<= 0 xH323) (<= xH323 1500) (<= 0 xH324) (<= xH324 1500) (<= 0 xH325) (<= xH325 1500) (<= 0 xH326) (<= xH326 1500) (<= 0 xH327) (<= xH327 1500) (<= 0 xH328) (<= xH328 1500) (<= 0 xH329) (<= xH329 1500) (<= 0 xH330) (<= xH330 1500) (<= 0 xH331) (<= xH331 1500) (<= 0 xH332) (<= xH332 1500) (<= 0 xH333) (<= xH333 1500) (<= 0 xH334) (<= xH334 1500) (<= 0 xH335) (<= xH335 1500) (<= 0 xH336) (<= xH336 1500) (<= 0 xH337) (<= xH337 1000) (<= 0 xH338) (<= xH338 1000) (<= 0 xH339) (<= xH339 1000) (<= 0 xH340) (<= xH340 1000) (<= 0 xH341) (<= xH341 1000) (<= 0 xH342) (<= xH342 1000) (<= 0 xH343) (<= xH343 1000) (<= 0 xH344) (<= xH344 1000) (<= 0 xH345) (<= xH345 1000) (<= 0 xH346) (<= xH346 1000) (<= 0 xH347) (<= xH347 1000) (<= 0 xH348) (<= xH348 1000) (<= 0 xH349) (<= xH349 1000) (<= 0 xH350) (<= xH350 1000) (<= 0 xH351) (<= xH351 1000) (<= 0 xH352) (<= xH352 1000) (<= 0 xH353) (<= xH353 1000) (<= 0 xH354) (<= xH354 1000) (<= 0 xH355) (<= xH355 1000) (<= 0 xH356) (<= xH356 1000) (<= 0 xH357) (<= xH357 1000) (<= 0 xH358) (<= xH358 1000) (<= 0 xH359) (<= xH359 1000) (<= 0 xH360) (<= xH360 1000) (<= 0 xH361) (<= xH361 2500) (<= 0 xH362) (<= xH362 2500) (<= 0 xH363) (<= xH363 2500) (<= 0 xH364) (<= xH364 2500) (<= 0 xH365) (<= xH365 2500) (<= 0 xH366) (<= xH366 2500) (<= 0 xH367) (<= xH367 2500) (<= 0 xH368) (<= xH368 2500) (<= 0 xH369) (<= xH369 2500) (<= 0 xH370) (<= xH370 2500) (<= 0 xH371) (<= xH371 2500) (<= 0 xH372) (<= xH372 2500) (<= 0 xH373) (<= xH373 2500) (<= 0 xH374) (<= xH374 2500) (<= 0 xH375) (<= xH375 2500) (<= 0 xH376) (<= xH376 2500) (<= 0 xH377) (<= xH377 2500) (<= 0 xH378) (<= xH378 2500) (<= 0 xH379) (<= xH379 2500) (<= 0 xH380) (<= xH380 2500) (<= 0 xH381) (<= xH381 2500) (<= 0 xH382) (<= xH382 2500) (<= 0 xH383) (<= xH383 2500) (<= 0 xH384) (<= xH384 2500) (<= xH194 xH1) (<= xH195 xH2) (<= xH196 xH3) (<= xH197 xH4) (<= xH198 xH5) (<= xH199 xH6) (<= xH200 xH7) (<= xH201 xH8) (<= xH202 xH9) (<= xH203 xH10) (<= xH204 xH11) (<= xH205 xH12) (<= xH206 xH13) (<= xH207 xH14) (<= xH208 xH15) (<= xH209 xH16) (<= xH210 xH17) (<= xH211 xH18) (<= xH212 xH19) (<= xH213 xH20) (<= xH214 xH21) (<= xH215 xH22) (<= xH216 xH23) (<= xH218 xH25) (<= xH219 xH26) (<= xH220 xH27) (<= xH221 xH28) (<= xH222 xH29) (<= xH223 xH30) (<= xH224 xH31) (<= xH225 xH32) (<= xH226 xH33) (<= xH227 xH34) (<= xH228 xH35) (<= xH229 xH36) (<= xH230 xH37) (<= xH231 xH38) (<= xH232 xH39) (<= xH233 xH40) (<= xH234 xH41) (<= xH235 xH42) (<= xH236 xH43) (<= xH237 xH44) (<= xH238 xH45) (<= xH239 xH46) (<= xH240 xH47) (<= xH242 xH49) (<= xH243 xH50) (<= xH244 xH51) (<= xH245 xH52) (<= xH246 xH53) (<= xH247 xH54) (<= xH248 xH55) (<= xH249 xH56) (<= xH250 xH57) (<= xH251 xH58) (<= xH252 xH59) (<= xH253 xH60) (<= xH254 xH61) (<= xH255 xH62) (<= xH256 xH63) (<= xH257 xH64) (<= xH258 xH65) (<= xH259 xH66) (<= xH260 xH67) (<= xH261 xH68) (<= xH262 xH69) (<= xH263 xH70) (<= xH264 xH71) (<= xH266 xH73) (<= xH267 xH74) (<= xH268 xH75) (<= xH269 xH76) (<= xH270 xH77) (<= xH271 xH78) (<= xH272 xH79) (<= xH273 xH80) (<= xH274 xH81) (<= xH275 xH82) (<= xH276 xH83) (<= xH277 xH84) (<= xH278 xH85) (<= xH279 xH86) (<= xH280 xH87) (<= xH281 xH88) (<= xH282 xH89) (<= xH283 xH90) (<= xH284 xH91) (<= xH285 xH92) (<= xH286 xH93) (<= xH287 xH94) (<= xH288 xH95) (<= xH290 xH97) (<= xH291 xH98) (<= xH292 xH99) (<= xH293 xH100) (<= xH294 xH101) (<= xH295 xH102) (<= xH296 xH103) (<= xH297 xH104) (<= xH298 xH105) (<= xH299 xH106) (<= xH300 xH107) (<= xH301 xH108) (<= xH302 xH109) (<= xH303 xH110) (<= xH304 xH111) (<= xH305 xH112) (<= xH306 xH113) (<= xH307 xH114) (<= xH308 xH115) (<= xH309 xH116) (<= xH310 xH117) (<= xH311 xH118) (<= xH312 xH119) (<= xH314 xH121) (<= xH315 xH122) (<= xH316 xH123) (<= xH317 xH124) (<= xH318 xH125) (<= xH319 xH126) (<= xH320 xH127) (<= xH321 xH128) (<= xH322 xH129) (<= xH323 xH130) (<= xH324 xH131) (<= xH325 xH132) (<= xH326 xH133) (<= xH327 xH134) (<= xH328 xH135) (<= xH329 xH136) (<= xH330 xH137) (<= xH331 xH138) (<= xH332 xH139) (<= xH333 xH140) (<= xH334 xH141) (<= xH335 xH142) (<= xH336 xH143) (<= xH338 xH145) (<= xH339 xH146) (<= xH340 xH147) (<= xH341 xH148) (<= xH342 xH149) (<= xH343 xH150) (<= xH344 xH151) (<= xH345 xH152) (<= xH346 xH153) (<= xH347 xH154) (<= xH348 xH155) (<= xH349 xH156) (<= xH350 xH157) (<= xH351 xH158) (<= xH352 xH159) (<= xH353 xH160) (<= xH354 xH161) (<= xH355 xH162) (<= xH356 xH163) (<= xH357 xH164) (<= xH358 xH165) (<= xH359 xH166) (<= xH360 xH167) (<= xH362 xH169) (<= xH363 xH170) (<= xH364 xH171) (<= xH365 xH172) (<= xH366 xH173) (<= xH367 xH174) (<= xH368 xH175) (<= xH369 xH176) (<= xH370 xH177) (<= xH371 xH178) (<= xH372 xH179) (<= xH373 xH180) (<= xH374 xH181) (<= xH375 xH182) (<= xH376 xH183) (<= xH377 xH184) (<= xH378 xH185) (<= xH379 xH186) (<= xH380 xH187) (<= xH381 xH188) (<= xH382 xH189) (<= xH383 xH190) (<= xH384 xH191)))
(check-sat)
(exit)