## ams_version=1.0 Model Main_sporttournament46 { Variable b1 { Range: binary; } Variable b2 { Range: binary; } Variable b3 { Range: binary; } Variable b4 { Range: binary; } Variable b5 { Range: binary; } Variable b6 { Range: binary; } Variable b7 { Range: binary; } Variable b8 { Range: binary; } Variable b9 { Range: binary; } Variable b10 { Range: binary; } Variable b11 { Range: binary; } Variable b12 { Range: binary; } Variable b13 { Range: binary; } Variable b14 { Range: binary; } Variable b15 { Range: binary; } Variable b16 { Range: binary; } Variable b17 { Range: binary; } Variable b18 { Range: binary; } Variable b19 { Range: binary; } Variable b20 { Range: binary; } Variable b21 { Range: binary; } Variable b22 { Range: binary; } Variable b23 { Range: binary; } Variable b24 { Range: binary; } Variable b25 { Range: binary; } Variable b26 { Range: binary; } Variable b27 { Range: binary; } Variable b28 { Range: binary; } Variable b29 { Range: binary; } Variable b30 { Range: binary; } Variable b31 { Range: binary; } Variable b32 { Range: binary; } Variable b33 { Range: binary; } Variable b34 { Range: binary; } Variable b35 { Range: binary; } Variable b36 { Range: binary; } Variable b37 { Range: binary; } Variable b38 { Range: binary; } Variable b39 { Range: binary; } Variable b40 { Range: binary; } Variable b41 { Range: binary; } Variable b42 { Range: binary; } Variable b43 { Range: binary; } Variable b44 { Range: binary; } Variable b45 { Range: binary; } Variable b46 { Range: binary; } Variable b47 { Range: binary; } Variable b48 { Range: binary; } Variable b49 { Range: binary; } Variable b50 { Range: binary; } Variable b51 { Range: binary; } Variable b52 { Range: binary; } Variable b53 { Range: binary; } Variable b54 { Range: binary; } Variable b55 { Range: binary; } Variable b56 { Range: binary; } Variable b57 { Range: binary; } Variable b58 { Range: binary; } Variable b59 { Range: binary; } Variable b60 { Range: binary; } Variable b61 { Range: binary; } Variable b62 { Range: binary; } Variable b63 { Range: binary; } Variable b64 { Range: binary; } Variable b65 { Range: binary; } Variable b66 { Range: binary; } Variable b67 { Range: binary; } Variable b68 { Range: binary; } Variable b69 { Range: binary; } Variable b70 { Range: binary; } Variable b71 { Range: binary; } Variable b72 { Range: binary; } Variable b73 { Range: binary; } Variable b74 { Range: binary; } Variable b75 { Range: binary; } Variable b76 { Range: binary; } Variable b77 { Range: binary; } Variable b78 { Range: binary; } Variable b79 { Range: binary; } Variable b80 { Range: binary; } Variable b81 { Range: binary; } Variable b82 { Range: binary; } Variable b83 { Range: binary; } Variable b84 { Range: binary; } Variable b85 { Range: binary; } Variable b86 { Range: binary; } Variable b87 { Range: binary; } Variable b88 { Range: binary; } Variable b89 { Range: binary; } Variable b90 { Range: binary; } Variable b91 { Range: binary; } Variable b92 { Range: binary; } Variable b93 { Range: binary; } Variable b94 { Range: binary; } Variable b95 { Range: binary; } Variable b96 { Range: binary; } Variable b97 { Range: binary; } Variable b98 { Range: binary; } Variable b99 { Range: binary; } Variable b100 { Range: binary; } Variable b101 { Range: binary; } Variable b102 { Range: binary; } Variable b103 { Range: binary; } Variable b104 { Range: binary; } Variable b105 { Range: binary; } Variable b106 { Range: binary; } Variable b107 { Range: binary; } Variable b108 { Range: binary; } Variable b109 { Range: binary; } Variable b110 { Range: binary; } Variable b111 { Range: binary; } Variable b112 { Range: binary; } Variable b113 { Range: binary; } Variable b114 { Range: binary; } Variable b115 { Range: binary; } Variable b116 { Range: binary; } Variable b117 { Range: binary; } Variable b118 { Range: binary; } Variable b119 { Range: binary; } Variable b120 { Range: binary; } Variable b121 { Range: binary; } Variable b122 { Range: binary; } Variable b123 { Range: binary; } Variable b124 { Range: binary; } Variable b125 { Range: binary; } Variable b126 { Range: binary; } Variable b127 { Range: binary; } Variable b128 { Range: binary; } Variable b129 { Range: binary; } Variable b130 { Range: binary; } Variable b131 { Range: binary; } Variable b132 { Range: binary; } Variable b133 { Range: binary; } Variable b134 { Range: binary; } Variable b135 { Range: binary; } Variable b136 { Range: binary; } Variable b137 { Range: binary; } Variable b138 { Range: binary; } Variable b139 { Range: binary; } Variable b140 { Range: binary; } Variable b141 { Range: binary; } Variable b142 { Range: binary; } Variable b143 { Range: binary; } Variable b144 { Range: binary; } Variable b145 { Range: binary; } Variable b146 { Range: binary; } Variable b147 { Range: binary; } Variable b148 { Range: binary; } Variable b149 { Range: binary; } Variable b150 { Range: binary; } Variable b151 { Range: binary; } Variable b152 { Range: binary; } Variable b153 { Range: binary; } Variable b154 { Range: binary; } Variable b155 { Range: binary; } Variable b156 { Range: binary; } Variable b157 { Range: binary; } Variable b158 { Range: binary; } Variable b159 { Range: binary; } Variable b160 { Range: binary; } Variable b161 { Range: binary; } Variable b162 { Range: binary; } Variable b163 { Range: binary; } Variable b164 { Range: binary; } Variable b165 { Range: binary; } Variable b166 { Range: binary; } Variable b167 { Range: binary; } Variable b168 { Range: binary; } Variable b169 { Range: binary; } Variable b170 { Range: binary; } Variable b171 { Range: binary; } Variable b172 { Range: binary; } Variable b173 { Range: binary; } Variable b174 { Range: binary; } Variable b175 { Range: binary; } Variable b176 { Range: binary; } Variable b177 { Range: binary; } Variable b178 { Range: binary; } Variable b179 { Range: binary; } Variable b180 { Range: binary; } Variable b181 { Range: binary; } Variable b182 { Range: binary; } Variable b183 { Range: binary; } Variable b184 { Range: binary; } Variable b185 { Range: binary; } Variable b186 { Range: binary; } Variable b187 { Range: binary; } Variable b188 { Range: binary; } Variable b189 { Range: binary; } Variable b190 { Range: binary; } Variable b191 { Range: binary; } Variable b192 { Range: binary; } Variable b193 { Range: binary; } Variable b194 { Range: binary; } Variable b195 { Range: binary; } Variable b196 { Range: binary; } Variable b197 { Range: binary; } Variable b198 { Range: binary; } Variable b199 { Range: binary; } Variable b200 { Range: binary; } Variable b201 { Range: binary; } Variable b202 { Range: binary; } Variable b203 { Range: binary; } Variable b204 { Range: binary; } Variable b205 { Range: binary; } Variable b206 { Range: binary; } Variable b207 { Range: binary; } Variable b208 { Range: binary; } Variable b209 { Range: binary; } Variable b210 { Range: binary; } Variable b211 { Range: binary; } Variable b212 { Range: binary; } Variable b213 { Range: binary; } Variable b214 { Range: binary; } Variable b215 { Range: binary; } Variable b216 { Range: binary; } Variable b217 { Range: binary; } Variable b218 { Range: binary; } Variable b219 { Range: binary; } Variable b220 { Range: binary; } Variable b221 { Range: binary; } Variable b222 { Range: binary; } Variable b223 { Range: binary; } Variable b224 { Range: binary; } Variable b225 { Range: binary; } Variable b226 { Range: binary; } Variable b227 { Range: binary; } Variable b228 { Range: binary; } Variable b229 { Range: binary; } Variable b230 { Range: binary; } Variable b231 { Range: binary; } Variable b232 { Range: binary; } Variable b233 { Range: binary; } Variable b234 { Range: binary; } Variable b235 { Range: binary; } Variable b236 { Range: binary; } Variable b237 { Range: binary; } Variable b238 { Range: binary; } Variable b239 { Range: binary; } Variable b240 { Range: binary; } Variable b241 { Range: binary; } Variable b242 { Range: binary; } Variable b243 { Range: binary; } Variable b244 { Range: binary; } Variable b245 { Range: binary; } Variable b246 { Range: binary; } Variable b247 { Range: binary; } Variable b248 { Range: binary; } Variable b249 { Range: binary; } Variable b250 { Range: binary; } Variable b251 { Range: binary; } Variable b252 { Range: binary; } Variable b253 { Range: binary; } Variable b254 { Range: binary; } Variable b255 { Range: binary; } Variable b256 { Range: binary; } Variable b257 { Range: binary; } Variable b258 { Range: binary; } Variable b259 { Range: binary; } Variable b260 { Range: binary; } Variable b261 { Range: binary; } Variable b262 { Range: binary; } Variable b263 { Range: binary; } Variable b264 { Range: binary; } Variable b265 { Range: binary; } Variable b266 { Range: binary; } Variable b267 { Range: binary; } Variable b268 { Range: binary; } Variable b269 { Range: binary; } Variable b270 { Range: binary; } Variable b271 { Range: binary; } Variable b272 { Range: binary; } Variable b273 { Range: binary; } Variable b274 { Range: binary; } Variable b275 { Range: binary; } Variable b276 { Range: binary; } Variable b277 { Range: binary; } Variable b278 { Range: binary; } Variable b279 { Range: binary; } Variable b280 { Range: binary; } Variable b281 { Range: binary; } Variable b282 { Range: binary; } Variable b283 { Range: binary; } Variable b284 { Range: binary; } Variable b285 { Range: binary; } Variable b286 { Range: binary; } Variable b287 { Range: binary; } Variable b288 { Range: binary; } Variable b289 { Range: binary; } Variable b290 { Range: binary; } Variable b291 { Range: binary; } Variable b292 { Range: binary; } Variable b293 { Range: binary; } Variable b294 { Range: binary; } Variable b295 { Range: binary; } Variable b296 { Range: binary; } Variable b297 { Range: binary; } Variable b298 { Range: binary; } Variable b299 { Range: binary; } Variable b300 { Range: binary; } Variable b301 { Range: binary; } Variable b302 { Range: binary; } Variable b303 { Range: binary; } Variable b304 { Range: binary; } Variable b305 { Range: binary; } Variable b306 { Range: binary; } Variable b307 { Range: binary; } Variable b308 { Range: binary; } Variable b309 { Range: binary; } Variable b310 { Range: binary; } Variable b311 { Range: binary; } Variable b312 { Range: binary; } Variable b313 { Range: binary; } Variable b314 { Range: binary; } Variable b315 { Range: binary; } Variable b316 { Range: binary; } Variable b317 { Range: binary; } Variable b318 { Range: binary; } Variable b319 { Range: binary; } Variable b320 { Range: binary; } Variable b321 { Range: binary; } Variable b322 { Range: binary; } Variable b323 { Range: binary; } Variable b324 { Range: binary; } Variable b325 { Range: binary; } Variable b326 { Range: binary; } Variable b327 { Range: binary; } Variable b328 { Range: binary; } Variable b329 { Range: binary; } Variable b330 { Range: binary; } Variable b331 { Range: binary; } Variable b332 { Range: binary; } Variable b333 { Range: binary; } Variable b334 { Range: binary; } Variable b335 { Range: binary; } Variable b336 { Range: binary; } Variable b337 { Range: binary; } Variable b338 { Range: binary; } Variable b339 { Range: binary; } Variable b340 { Range: binary; } Variable b341 { Range: binary; } Variable b342 { Range: binary; } Variable b343 { Range: binary; } Variable b344 { Range: binary; } Variable b345 { Range: binary; } Variable b346 { Range: binary; } Variable b347 { Range: binary; } Variable b348 { Range: binary; } Variable b349 { Range: binary; } Variable b350 { Range: binary; } Variable b351 { Range: binary; } Variable b352 { Range: binary; } Variable b353 { Range: binary; } Variable b354 { Range: binary; } Variable b355 { Range: binary; } Variable b356 { Range: binary; } Variable b357 { Range: binary; } Variable b358 { Range: binary; } Variable b359 { Range: binary; } Variable b360 { Range: binary; } Variable b361 { Range: binary; } Variable b362 { Range: binary; } Variable b363 { Range: binary; } Variable b364 { Range: binary; } Variable b365 { Range: binary; } Variable b366 { Range: binary; } Variable b367 { Range: binary; } Variable b368 { Range: binary; } Variable b369 { Range: binary; } Variable b370 { Range: binary; } Variable b371 { Range: binary; } Variable b372 { Range: binary; } Variable b373 { Range: binary; } Variable b374 { Range: binary; } Variable b375 { Range: binary; } Variable b376 { Range: binary; } Variable b377 { Range: binary; } Variable b378 { Range: binary; } Variable b379 { Range: binary; } Variable b380 { Range: binary; } Variable b381 { Range: binary; } Variable b382 { Range: binary; } Variable b383 { Range: binary; } Variable b384 { Range: binary; } Variable b385 { Range: binary; } Variable b386 { Range: binary; } Variable b387 { Range: binary; } Variable b388 { Range: binary; } Variable b389 { Range: binary; } Variable b390 { Range: binary; } Variable b391 { Range: binary; } Variable b392 { Range: binary; } Variable b393 { Range: binary; } Variable b394 { Range: binary; } Variable b395 { Range: binary; } Variable b396 { Range: binary; } Variable b397 { Range: binary; } Variable b398 { Range: binary; } Variable b399 { Range: binary; } Variable b400 { Range: binary; } Variable b401 { Range: binary; } Variable b402 { Range: binary; } Variable b403 { Range: binary; } Variable b404 { Range: binary; } Variable b405 { Range: binary; } Variable b406 { Range: binary; } Variable b407 { Range: binary; } Variable b408 { Range: binary; } Variable b409 { Range: binary; } Variable b410 { Range: binary; } Variable b411 { Range: binary; } Variable b412 { Range: binary; } Variable b413 { Range: binary; } Variable b414 { Range: binary; } Variable b415 { Range: binary; } Variable b416 { Range: binary; } Variable b417 { Range: binary; } Variable b418 { Range: binary; } Variable b419 { Range: binary; } Variable b420 { Range: binary; } Variable b421 { Range: binary; } Variable b422 { Range: binary; } Variable b423 { Range: binary; } Variable b424 { Range: binary; } Variable b425 { Range: binary; } Variable b426 { Range: binary; } Variable b427 { Range: binary; } Variable b428 { Range: binary; } Variable b429 { Range: binary; } Variable b430 { Range: binary; } Variable b431 { Range: binary; } Variable b432 { Range: binary; } Variable b433 { Range: binary; } Variable b434 { Range: binary; } Variable b435 { Range: binary; } Variable b436 { Range: binary; } Variable b437 { Range: binary; } Variable b438 { Range: binary; } Variable b439 { Range: binary; } Variable b440 { Range: binary; } Variable b441 { Range: binary; } Variable b442 { Range: binary; } Variable b443 { Range: binary; } Variable b444 { Range: binary; } Variable b445 { Range: binary; } Variable b446 { Range: binary; } Variable b447 { Range: binary; } Variable b448 { Range: binary; } Variable b449 { Range: binary; } Variable b450 { Range: binary; } Variable b451 { Range: binary; } Variable b452 { Range: binary; } Variable b453 { Range: binary; } Variable b454 { Range: binary; } Variable b455 { Range: binary; } Variable b456 { Range: binary; } Variable b457 { Range: binary; } Variable b458 { Range: binary; } Variable b459 { Range: binary; } Variable b460 { Range: binary; } Variable b461 { Range: binary; } Variable b462 { Range: binary; } Variable b463 { Range: binary; } Variable b464 { Range: binary; } Variable b465 { Range: binary; } Variable b466 { Range: binary; } Variable b467 { Range: binary; } Variable b468 { Range: binary; } Variable b469 { Range: binary; } Variable b470 { Range: binary; } Variable b471 { Range: binary; } Variable b472 { Range: binary; } Variable b473 { Range: binary; } Variable b474 { Range: binary; } Variable b475 { Range: binary; } Variable b476 { Range: binary; } Variable b477 { Range: binary; } Variable b478 { Range: binary; } Variable b479 { Range: binary; } Variable b480 { Range: binary; } Variable b481 { Range: binary; } Variable b482 { Range: binary; } Variable b483 { Range: binary; } Variable b484 { Range: binary; } Variable b485 { Range: binary; } Variable b486 { Range: binary; } Variable b487 { Range: binary; } Variable b488 { Range: binary; } Variable b489 { Range: binary; } Variable b490 { Range: binary; } Variable b491 { Range: binary; } Variable b492 { Range: binary; } Variable b493 { Range: binary; } Variable b494 { Range: binary; } Variable b495 { Range: binary; } Variable b496 { Range: binary; } Variable b497 { Range: binary; } Variable b498 { Range: binary; } Variable b499 { Range: binary; } Variable b500 { Range: binary; } Variable b501 { Range: binary; } Variable b502 { Range: binary; } Variable b503 { Range: binary; } Variable b504 { Range: binary; } Variable b505 { Range: binary; } Variable b506 { Range: binary; } Variable b507 { Range: binary; } Variable b508 { Range: binary; } Variable b509 { Range: binary; } Variable b510 { Range: binary; } Variable b511 { Range: binary; } Variable b512 { Range: binary; } Variable b513 { Range: binary; } Variable b514 { Range: binary; } Variable b515 { Range: binary; } Variable b516 { Range: binary; } Variable b517 { Range: binary; } Variable b518 { Range: binary; } Variable b519 { Range: binary; } Variable b520 { Range: binary; } Variable b521 { Range: binary; } Variable b522 { Range: binary; } Variable b523 { Range: binary; } Variable b524 { Range: binary; } Variable b525 { Range: binary; } Variable b526 { Range: binary; } Variable b527 { Range: binary; } Variable b528 { Range: binary; } Variable b529 { Range: binary; } Variable b530 { Range: binary; } Variable b531 { Range: binary; } Variable b532 { Range: binary; } Variable b533 { Range: binary; } Variable b534 { Range: binary; } Variable b535 { Range: binary; } Variable b536 { Range: binary; } Variable b537 { Range: binary; } Variable b538 { Range: binary; } Variable b539 { Range: binary; } Variable b540 { Range: binary; } Variable b541 { Range: binary; } Variable b542 { Range: binary; } Variable b543 { Range: binary; } Variable b544 { Range: binary; } Variable b545 { Range: binary; } Variable b546 { Range: binary; } Variable b547 { Range: binary; } Variable b548 { Range: binary; } Variable b549 { Range: binary; } Variable b550 { Range: binary; } Variable b551 { Range: binary; } Variable b552 { Range: binary; } Variable b553 { Range: binary; } Variable b554 { Range: binary; } Variable b555 { Range: binary; } Variable b556 { Range: binary; } Variable b557 { Range: binary; } Variable b558 { Range: binary; } Variable b559 { Range: binary; } Variable b560 { Range: binary; } Variable b561 { Range: binary; } Variable b562 { Range: binary; } Variable b563 { Range: binary; } Variable b564 { Range: binary; } Variable b565 { Range: binary; } Variable b566 { Range: binary; } Variable b567 { Range: binary; } Variable b568 { Range: binary; } Variable b569 { Range: binary; } Variable b570 { Range: binary; } Variable b571 { Range: binary; } Variable b572 { Range: binary; } Variable b573 { Range: binary; } Variable b574 { Range: binary; } Variable b575 { Range: binary; } Variable b576 { Range: binary; } Variable b577 { Range: binary; } Variable b578 { Range: binary; } Variable b579 { Range: binary; } Variable b580 { Range: binary; } Variable b581 { Range: binary; } Variable b582 { Range: binary; } Variable b583 { Range: binary; } Variable b584 { Range: binary; } Variable b585 { Range: binary; } Variable b586 { Range: binary; } Variable b587 { Range: binary; } Variable b588 { Range: binary; } Variable b589 { Range: binary; } Variable b590 { Range: binary; } Variable b591 { Range: binary; } Variable b592 { Range: binary; } Variable b593 { Range: binary; } Variable b594 { Range: binary; } Variable b595 { Range: binary; } Variable b596 { Range: binary; } Variable b597 { Range: binary; } Variable b598 { Range: binary; } Variable b599 { Range: binary; } Variable b600 { Range: binary; } Variable b601 { Range: binary; } Variable b602 { Range: binary; } Variable b603 { Range: binary; } Variable b604 { Range: binary; } Variable b605 { Range: binary; } Variable b606 { Range: binary; } Variable b607 { Range: binary; } Variable b608 { Range: binary; } Variable b609 { Range: binary; } Variable b610 { Range: binary; } Variable b611 { Range: binary; } Variable b612 { Range: binary; } Variable b613 { Range: binary; } Variable b614 { Range: binary; } Variable b615 { Range: binary; } Variable b616 { Range: binary; } Variable b617 { Range: binary; } Variable b618 { Range: binary; } Variable b619 { Range: binary; } Variable b620 { Range: binary; } Variable b621 { Range: binary; } Variable b622 { Range: binary; } Variable b623 { Range: binary; } Variable b624 { Range: binary; } Variable b625 { Range: binary; } Variable b626 { Range: binary; } Variable b627 { Range: binary; } Variable b628 { Range: binary; } Variable b629 { Range: binary; } Variable b630 { Range: binary; } Variable b631 { Range: binary; } Variable b632 { Range: binary; } Variable b633 { Range: binary; } Variable b634 { Range: binary; } Variable b635 { Range: binary; } Variable b636 { Range: binary; } Variable b637 { Range: binary; } Variable b638 { Range: binary; } Variable b639 { Range: binary; } Variable b640 { Range: binary; } Variable b641 { Range: binary; } Variable b642 { Range: binary; } Variable b643 { Range: binary; } Variable b644 { Range: binary; } Variable b645 { Range: binary; } Variable b646 { Range: binary; } Variable b647 { Range: binary; } Variable b648 { Range: binary; } Variable b649 { Range: binary; } Variable b650 { Range: binary; } Variable b651 { Range: binary; } Variable b652 { Range: binary; } Variable b653 { Range: binary; } Variable b654 { Range: binary; } Variable b655 { Range: binary; } Variable b656 { Range: binary; } Variable b657 { Range: binary; } Variable b658 { Range: binary; } Variable b659 { Range: binary; } Variable b660 { Range: binary; } Variable b661 { Range: binary; } Variable b662 { Range: binary; } Variable b663 { Range: binary; } Variable b664 { Range: binary; } Variable b665 { Range: binary; } Variable b666 { Range: binary; } Variable b667 { Range: binary; } Variable b668 { Range: binary; } Variable b669 { Range: binary; } Variable b670 { Range: binary; } Variable b671 { Range: binary; } Variable b672 { Range: binary; } Variable b673 { Range: binary; } Variable b674 { Range: binary; } Variable b675 { Range: binary; } Variable b676 { Range: binary; } Variable b677 { Range: binary; } Variable b678 { Range: binary; } Variable b679 { Range: binary; } Variable b680 { Range: binary; } Variable b681 { Range: binary; } Variable b682 { Range: binary; } Variable b683 { Range: binary; } Variable b684 { Range: binary; } Variable b685 { Range: binary; } Variable b686 { Range: binary; } Variable b687 { Range: binary; } Variable b688 { Range: binary; } Variable b689 { Range: binary; } Variable b690 { Range: binary; } Variable b691 { Range: binary; } Variable b692 { Range: binary; } Variable b693 { Range: binary; } Variable b694 { Range: binary; } Variable b695 { Range: binary; } Variable b696 { Range: binary; } Variable b697 { Range: binary; } Variable b698 { Range: binary; } Variable b699 { Range: binary; } Variable b700 { Range: binary; } Variable b701 { Range: binary; } Variable b702 { Range: binary; } Variable b703 { Range: binary; } Variable b704 { Range: binary; } Variable b705 { Range: binary; } Variable b706 { Range: binary; } Variable b707 { Range: binary; } Variable b708 { Range: binary; } Variable b709 { Range: binary; } Variable b710 { Range: binary; } Variable b711 { Range: binary; } Variable b712 { Range: binary; } Variable b713 { Range: binary; } Variable b714 { Range: binary; } Variable b715 { Range: binary; } Variable b716 { Range: binary; } Variable b717 { Range: binary; } Variable b718 { Range: binary; } Variable b719 { Range: binary; } Variable b720 { Range: binary; } Variable b721 { Range: binary; } Variable b722 { Range: binary; } Variable b723 { Range: binary; } Variable b724 { Range: binary; } Variable b725 { Range: binary; } Variable b726 { Range: binary; } Variable b727 { Range: binary; } Variable b728 { Range: binary; } Variable b729 { Range: binary; } Variable b730 { Range: binary; } Variable b731 { Range: binary; } Variable b732 { Range: binary; } Variable b733 { Range: binary; } Variable b734 { Range: binary; } Variable b735 { Range: binary; } Variable b736 { Range: binary; } Variable b737 { Range: binary; } Variable b738 { Range: binary; } Variable b739 { Range: binary; } Variable b740 { Range: binary; } Variable b741 { Range: binary; } Variable b742 { Range: binary; } Variable b743 { Range: binary; } Variable b744 { Range: binary; } Variable b745 { Range: binary; } Variable b746 { Range: binary; } Variable b747 { Range: binary; } Variable b748 { Range: binary; } Variable b749 { Range: binary; } Variable b750 { Range: binary; } Variable b751 { Range: binary; } Variable b752 { Range: binary; } Variable b753 { Range: binary; } Variable b754 { Range: binary; } Variable b755 { Range: binary; } Variable b756 { Range: binary; } Variable b757 { Range: binary; } Variable b758 { Range: binary; } Variable b759 { Range: binary; } Variable b760 { Range: binary; } Variable b761 { Range: binary; } Variable b762 { Range: binary; } Variable b763 { Range: binary; } Variable b764 { Range: binary; } Variable b765 { Range: binary; } Variable b766 { Range: binary; } Variable b767 { Range: binary; } Variable b768 { Range: binary; } Variable b769 { Range: binary; } Variable b770 { Range: binary; } Variable b771 { Range: binary; } Variable b772 { Range: binary; } Variable b773 { Range: binary; } Variable b774 { Range: binary; } Variable b775 { Range: binary; } Variable b776 { Range: binary; } Variable b777 { Range: binary; } Variable b778 { Range: binary; } Variable b779 { Range: binary; } Variable b780 { Range: binary; } Variable b781 { Range: binary; } Variable b782 { Range: binary; } Variable b783 { Range: binary; } Variable b784 { Range: binary; } Variable b785 { Range: binary; } Variable b786 { Range: binary; } Variable b787 { Range: binary; } Variable b788 { Range: binary; } Variable b789 { Range: binary; } Variable b790 { Range: binary; } Variable b791 { Range: binary; } Variable b792 { Range: binary; } Variable b793 { Range: binary; } Variable b794 { Range: binary; } Variable b795 { Range: binary; } Variable b796 { Range: binary; } Variable b797 { Range: binary; } Variable b798 { Range: binary; } Variable b799 { Range: binary; } Variable b800 { Range: binary; } Variable b801 { Range: binary; } Variable b802 { Range: binary; } Variable b803 { Range: binary; } Variable b804 { Range: binary; } Variable b805 { Range: binary; } Variable b806 { Range: binary; } Variable b807 { Range: binary; } Variable b808 { Range: binary; } Variable b809 { Range: binary; } Variable b810 { Range: binary; } Variable b811 { Range: binary; } Variable b812 { Range: binary; } Variable b813 { Range: binary; } Variable b814 { Range: binary; } Variable b815 { Range: binary; } Variable b816 { Range: binary; } Variable b817 { Range: binary; } Variable b818 { Range: binary; } Variable b819 { Range: binary; } Variable b820 { Range: binary; } Variable b821 { Range: binary; } Variable b822 { Range: binary; } Variable b823 { Range: binary; } Variable b824 { Range: binary; } Variable b825 { Range: binary; } Variable b826 { Range: binary; } Variable b827 { Range: binary; } Variable b828 { Range: binary; } Variable b829 { Range: binary; } Variable b830 { Range: binary; } Variable b831 { Range: binary; } Variable b832 { Range: binary; } Variable b833 { Range: binary; } Variable b834 { Range: binary; } Variable b835 { Range: binary; } Variable b836 { Range: binary; } Variable b837 { Range: binary; } Variable b838 { Range: binary; } Variable b839 { Range: binary; } Variable b840 { Range: binary; } Variable b841 { Range: binary; } Variable b842 { Range: binary; } Variable b843 { Range: binary; } Variable b844 { Range: binary; } Variable b845 { Range: binary; } Variable b846 { Range: binary; } Variable b847 { Range: binary; } Variable b848 { Range: binary; } Variable b849 { Range: binary; } Variable b850 { Range: binary; } Variable b851 { Range: binary; } Variable b852 { Range: binary; } Variable b853 { Range: binary; } Variable b854 { Range: binary; } Variable b855 { Range: binary; } Variable b856 { Range: binary; } Variable b857 { Range: binary; } Variable b858 { Range: binary; } Variable b859 { Range: binary; } Variable b860 { Range: binary; } Variable b861 { Range: binary; } Variable b862 { Range: binary; } Variable b863 { Range: binary; } Variable b864 { Range: binary; } Variable b865 { Range: binary; } Variable b866 { Range: binary; } Variable b867 { Range: binary; } Variable b868 { Range: binary; } Variable b869 { Range: binary; } Variable b870 { Range: binary; } Variable b871 { Range: binary; } Variable b872 { Range: binary; } Variable b873 { Range: binary; } Variable b874 { Range: binary; } Variable b875 { Range: binary; } Variable b876 { Range: binary; } Variable b877 { Range: binary; } Variable b878 { Range: binary; } Variable b879 { Range: binary; } Variable b880 { Range: binary; } Variable b881 { Range: binary; } Variable b882 { Range: binary; } Variable b883 { Range: binary; } Variable b884 { Range: binary; } Variable b885 { Range: binary; } Variable b886 { Range: binary; } Variable b887 { Range: binary; } Variable b888 { Range: binary; } Variable b889 { Range: binary; } Variable b890 { Range: binary; } Variable b891 { Range: binary; } Variable b892 { Range: binary; } Variable b893 { Range: binary; } Variable b894 { Range: binary; } Variable b895 { Range: binary; } Variable b896 { Range: binary; } Variable b897 { Range: binary; } Variable b898 { Range: binary; } Variable b899 { Range: binary; } Variable b900 { Range: binary; } Variable b901 { Range: binary; } Variable b902 { Range: binary; } Variable b903 { Range: binary; } Variable b904 { Range: binary; } Variable b905 { Range: binary; } Variable b906 { Range: binary; } Variable b907 { Range: binary; } Variable b908 { Range: binary; } Variable b909 { Range: binary; } Variable b910 { Range: binary; } Variable b911 { Range: binary; } Variable b912 { Range: binary; } Variable b913 { Range: binary; } Variable b914 { Range: binary; } Variable b915 { Range: binary; } Variable b916 { Range: binary; } Variable b917 { Range: binary; } Variable b918 { Range: binary; } Variable b919 { Range: binary; } Variable b920 { Range: binary; } Variable b921 { Range: binary; } Variable b922 { Range: binary; } Variable b923 { Range: binary; } Variable b924 { Range: binary; } Variable b925 { Range: binary; } Variable b926 { Range: binary; } Variable b927 { Range: binary; } Variable b928 { Range: binary; } Variable b929 { Range: binary; } Variable b930 { Range: binary; } Variable b931 { Range: binary; } Variable b932 { Range: binary; } Variable b933 { Range: binary; } Variable b934 { Range: binary; } Variable b935 { Range: binary; } Variable b936 { Range: binary; } Variable b937 { Range: binary; } Variable b938 { Range: binary; } Variable b939 { Range: binary; } Variable b940 { Range: binary; } Variable b941 { Range: binary; } Variable b942 { Range: binary; } Variable b943 { Range: binary; } Variable b944 { Range: binary; } Variable b945 { Range: binary; } Variable b946 { Range: binary; } Variable b947 { Range: binary; } Variable b948 { Range: binary; } Variable b949 { Range: binary; } Variable b950 { Range: binary; } Variable b951 { Range: binary; } Variable b952 { Range: binary; } Variable b953 { Range: binary; } Variable b954 { Range: binary; } Variable b955 { Range: binary; } Variable b956 { Range: binary; } Variable b957 { Range: binary; } Variable b958 { Range: binary; } Variable b959 { Range: binary; } Variable b960 { Range: binary; } Variable b961 { Range: binary; } Variable b962 { Range: binary; } Variable b963 { Range: binary; } Variable b964 { Range: binary; } Variable b965 { Range: binary; } Variable b966 { Range: binary; } Variable b967 { Range: binary; } Variable b968 { Range: binary; } Variable b969 { Range: binary; } Variable b970 { Range: binary; } Variable b971 { Range: binary; } Variable b972 { Range: binary; } Variable b973 { Range: binary; } Variable b974 { Range: binary; } Variable b975 { Range: binary; } Variable b976 { Range: binary; } Variable b977 { Range: binary; } Variable b978 { Range: binary; } Variable b979 { Range: binary; } Variable b980 { Range: binary; } Variable b981 { Range: binary; } Variable b982 { Range: binary; } Variable b983 { Range: binary; } Variable b984 { Range: binary; } Variable b985 { Range: binary; } Variable b986 { Range: binary; } Variable b987 { Range: binary; } Variable b988 { Range: binary; } Variable b989 { Range: binary; } Variable b990 { Range: binary; } Variable b991 { Range: binary; } Variable b992 { Range: binary; } Variable b993 { Range: binary; } Variable b994 { Range: binary; } Variable b995 { Range: binary; } Variable b996 { Range: binary; } Variable b997 { Range: binary; } Variable b998 { Range: binary; } Variable b999 { Range: binary; } Variable b1000 { Range: binary; } Variable b1001 { Range: binary; } Variable b1002 { Range: binary; } Variable b1003 { Range: binary; } Variable b1004 { Range: binary; } Variable b1005 { Range: binary; } Variable b1006 { Range: binary; } Variable b1007 { Range: binary; } Variable b1008 { Range: binary; } Variable b1009 { Range: binary; } Variable b1010 { Range: binary; } Variable b1011 { Range: binary; } Variable b1012 { Range: binary; } Variable b1013 { Range: binary; } Variable b1014 { Range: binary; } Variable b1015 { Range: binary; } Variable b1016 { Range: binary; } Variable b1017 { Range: binary; } Variable b1018 { Range: binary; } Variable b1019 { Range: binary; } Variable b1020 { Range: binary; } Variable b1021 { Range: binary; } Variable b1022 { Range: binary; } Variable b1023 { Range: binary; } Variable b1024 { Range: binary; } Variable b1025 { Range: binary; } Variable b1026 { Range: binary; } Variable b1027 { Range: binary; } Variable b1028 { Range: binary; } Variable b1029 { Range: binary; } Variable b1030 { Range: binary; } Variable b1031 { Range: binary; } Variable b1032 { Range: binary; } Variable b1033 { Range: binary; } Variable b1034 { Range: binary; } Variable b1035 { Range: binary; } Variable objvar; Constraint e1 { Definition: { 2*b1*b52 - 2*b1 - 2*b52 - 2*b1*b651 + 2*b1*b652 + 2*b1*b661 + 2*b2*b478 - 2*b2 - 2*b478 - 2*b2*b524 + 2*b524 + 2*b2*b653 + 2*b2*b666 - 2*b3*b579 - 2 *b3 + 2*b579 + 2*b3*b657 + 2*b3*b658 + 2*b3*b678 + 2*b4*b65 - 2*b4 - 2*b65 + 2*b4*b96 - 2*b96 + 2*b4*b143 - 2*b143 - 2*b4*b168 + 2*b168 + 2*b5*b9 - 4*b5 - 2*b9 + 2*b5*b42 - 2*b42 + 2*b5*b279 - 2*b279 + 2*b5*b683 + 2*b6* b118 - 2*b6 - 2*b118 + 2*b6*b169 - 2*b169 - 2*b6*b192 + 2*b192 + 2*b6*b734 + 2*b7*b96 - 2*b7 + 2*b7*b144 - 2*b144 + 2*b7*b193 - 2*b193 - 2*b7*b748 + 2*b8*b118 - 2*b8 + 2*b8*b170 - 2*b170 + 2*b8*b217 - 4*b217 - 2*b8*b251 + 2*b251 + 2*b9*b534 - 2*b534 + 2*b9*b721 - 2*b9*b756 + 2*b10*b144 - 2* b10 + 2*b10*b194 - 2*b194 + 2*b10*b252 - 4*b252 - 2*b10*b287 + 2*b287 + 2* b11*b125 - 2*b11 - 2*b125 + 2*b11*b664 - 2*b11*b738 + 2*b11*b739 + 2*b12* b587 - 2*b12 - 2*b587 + 2*b12*b706 + 2*b12*b746 - 2*b12*b767 + 2*b13*b170 - 2*b13 + 2*b13*b219 - 2*b219 + 2*b13*b288 - 4*b288 - 2*b13*b323 + 2*b323 + 2*b14*b150 - 2*b14 - 2*b150 + 2*b14*b508 + 2*b508 + 2*b14*b665 - 2*b14* b752 + 2*b15*b194 - 2*b15 + 2*b15*b254 - 2*b254 + 2*b15*b324 - 4*b324 - 2* b15*b365 + 2*b365 + 2*b16*b177 - 2*b16 - 2*b177 + 2*b16*b456 + 2*b456 + 2* b16*b676 - 2*b16*b760 + 2*b17*b219 - 2*b17 + 2*b17*b290 - 2*b290 + 2*b17* b366 - 4*b366 - 2*b17*b401 + 2*b401 + 2*b18*b204 - 2*b18 - 2*b204 + 2*b18* b689 + 2*b18*b690 - 2*b18*b772 - 2*b19*b374 - 2*b19 + 2*b374 + 2*b19*b376 - 2*b376 + 2*b19*b617 - 4*b617 + 2*b19*b728 + 2*b20*b155 - 2*b20 - 2*b155 - 2*b20*b517 + 2*b517 + 2*b20*b801 + 2*b20*b802 + 2*b21*b254 - 2*b21 + 2* b21*b326 - 2*b326 + 2*b21*b402 - 4*b402 - 2*b21*b444 + 2*b444 + 2*b22*b230 - 2*b22 - 2*b230 - 2*b22*b411 + 2*b411 + 2*b22*b675 + 2*b22*b702 + 2*b23* b181 - 2*b23 - 2*b181 - 2*b23*b568 + 4*b568 + 2*b23*b815 + 2*b23*b816 + 2* b24*b263 - 2*b24 - 2*b263 - 2*b24*b454 + 2*b454 + 2*b24*b664 + 2*b24*b714 + 2*b25*b131 - 2*b25 - 2*b131 + 2*b25*b206 - 2*b206 + 2*b25*b305 - 2*b305 - 2*b25*b626 + 2*b626 + 2*b26*b48 - 2*b26 - 2*b48 + 2*b26*b481 - 4*b481 + 2*b27*b155 - 2*b27 + 2*b27*b232 - 4*b232 + 2*b27*b342 - 2*b342 - 2*b27* b842 + 2*b28*b41 - 2*b28 - 2*b41 + 2*b28*b681 + 2*b28*b695 - 2*b28*b779 + 2*b29*b245 - 2*b29 - 2*b245 + 2*b29*b357 - 2*b357 + 2*b29*b659 - 2*b29* b846 + 2*b30*b181 - 2*b30 + 2*b30*b267 - 4*b267 + 2*b30*b381 - 4*b381 - 2* b30*b855 + 2*b31*b316 - 2*b31 - 2*b316 + 2*b31*b668 + 2*b31*b747 - 2*b31* b859 + 2*b32*b505 - 2*b32 - 2*b505 + 2*b32*b558 - 2*b558 + 2*b32*b752 - 2* b32*b825 + 2*b33*b206 - 2*b33 + 2*b33*b306 - 4*b306 + 2*b33*b424 - 4*b424 - 2*b33*b867 + 2*b34*b88 - 2*b34 - 4*b88 - 2*b34*b181 + 2*b34*b306 + 2* b34*b868 + 2*b35*b91 - 2*b35 - 2*b91 + 2*b35*b844 + 2*b36*b280 - 2*b36 - 2 *b280 + 2*b36*b680 + 2*b36*b757 - 2*b36*b871 + 2*b37*b451 - 2*b37 - 2*b451 + 2*b37*b738 - 2*b37*b837 + 2*b37*b838 + 2*b38*b232 - 2*b38 + 2*b38*b343 - 4*b343 + 2*b38*b467 - 4*b467 - 2*b38*b878 + 2*b39*b58 - 2*b39 - 2*b58 + 2*b39*b107 - 4*b107 - 2*b39*b155 + 2*b39*b343 + 2*b40*b112 - 2*b40 - 2* b112 + 2*b40*b857 + 2*b41*b245 + 2*b41*b768 - 2*b41*b881 + 2*b42*b43 - 2* b43 + 2*b42*b757 - 2*b42*b769 + 2*b43*b63 - 2*b63 - 2*b43*b359 + 4*b359 + 2*b43*b646 + 2*b44*b117 - 2*b44 - 2*b117 + 2*b44*b247 - 4*b247 + 2*b44* b651 - 2*b44*b903 + 2*b45*b454 - 2*b45 + 2*b45*b726 - 2*b45*b852 + 2*b45* b853 + 2*b46*b267 - 2*b46 + 2*b46*b382 - 4*b382 + 2*b46*b518 - 4*b518 - 2* b46*b886 + 2*b47*b72 - 2*b47 - 4*b72 - 2*b47*b131 + 2*b47*b133 - 4*b133 + 2*b47*b382 + 2*b48*b49 - 2*b49 - 2*b48*b111 - 2*b111 + 2*b48*b241 - 4*b241 + 2*b49*b136 - 4*b136 + 2*b50*b164 - 2*b50 - 2*b164 + 2*b50*b804 + 2*b51* b52 - 4*b51 + 2*b51*b746 + 2*b51*b768 + 2*b51*b769 + 2*b52*b78 - 2*b78 - 2 *b52*b395 + 2*b395 + 2*b53*b117 - 2*b53 + 2*b53*b166 - 2*b166 + 2*b53*b647 - 2*b53*b882 + 2*b54*b68 - 2*b54 - 2*b68 + 2*b54*b333 - 2*b333 - 2*b54* b809 + 2*b54*b810 + 2*b55*b411 - 2*b55 + 2*b55*b712 - 2*b55*b865 + 2*b55* b866 + 2*b56*b306 - 4*b56 + 2*b56*b425 - 4*b425 + 2*b56*b569 - 4*b569 + 2* b56*b886 + 2*b57*b88 - 2*b57 + 2*b57*b157 - 4*b157 + 2*b57*b425 - 2*b57* b816 + 2*b58*b573 - 4*b573 + 2*b58*b843 - 2*b58*b879 + 2*b59*b89 - 2*b59 - 2*b89 - 2*b59*b91 + 2*b59*b161 - 4*b161 + 2*b59*b899 + 2*b60*b61 - 2* b60 - 2*b61 - 2*b60*b90 - 2*b90 + 2*b60*b275 - 4*b275 + 2*b60*b880 + 2*b61 *b161 + 2*b62*b139 - 2*b62 - 2*b139 + 2*b62*b484 + 2*b484 + 2*b63*b190 - 4 *b190 - 2*b63*b872 + 2*b63*b903 + 2*b64*b117 - 4*b64 + 2*b64*b190 + 2*b64* b709 + 2*b64*b748 + 2*b65*b171 - 2*b171 + 2*b65*b708 - 2*b65*b930 + 2*b66* b80 + 2*b66 + 2*b80 - 2*b66*b199 + 4*b199 - 2*b66*b685 - 2*b66*b749 + 2* b67*b370 - 2*b67 - 2*b370 - 2*b67*b822 + 2*b67*b823 + 2*b67*b824 + 2*b68* b641 + 2*b68*b751 - 2*b68*b812 + 2*b69*b700 - 2*b69 + 2*b69*b772 - 2*b69* b876 + 2*b69*b877 + 2*b70*b343 - 4*b70 + 2*b70*b469 - 4*b469 + 2*b70*b627 - 4*b627 + 2*b70*b878 + 2*b71*b107 - 2*b71 + 2*b71*b183 - 4*b183 + 2*b71* b469 - 2*b71*b802 + 2*b72*b235 - 4*b235 + 2*b72*b829 + 2*b72*b869 + 2*b73* b74 - 2*b73 - 2*b74 + 2*b73*b901 - 2*b73*b911 + 2*b73*b912 - 2*b74*b75 - 2 *b75 + 2*b74*b110 - 4*b110 + 2*b74*b186 - 4*b186 + 2*b75*b76 - 2*b76 + 2* b75*b313 - 4*b313 + 2*b75*b887 + 2*b76*b186 + 2*b77*b115 - 2*b77 - 2*b115 + 2*b77*b436 + 2*b436 + 2*b78*b166 + 2*b78*b214 - 4*b214 - 2*b78*b860 - 2 *b79*b605 + 2*b79 + 2*b605 - 2*b79*b670 + 2*b79*b673 - 2*b79*b758 - 2*b80* b603 + 2*b603 - 2*b80*b687 - 2*b80*b932 + 2*b81*b226 - 2*b81 - 2*b226 + 2* b81*b409 - 2*b409 - 2*b81*b835 + 2*b81*b836 + 2*b82*b229 - 2*b82 - 4*b229 + 2*b82*b409 - 2*b82*b798 + 2*b82*b824 + 2*b83*b149 - 4*b83 - 2*b149 + 2* b83*b334 - 2*b334 + 2*b83*b760 + 2*b83*b876 + 2*b84*b85 - 2*b84 - 2*b85 + 2*b84*b103 - 2*b103 + 2*b84*b300 - 4*b300 - 2*b84*b740 + 2*b85*b127 - 2* b127 + 2*b85*b179 - 2*b179 - 2*b85*b942 + 2*b86*b382 - 2*b86 + 2*b86*b520 - 2*b520 - 2*b86*b648 + 2*b86*b867 + 2*b87*b133 - 4*b87 + 2*b87*b208 - 4* b208 + 2*b87*b520 + 2*b87*b802 + 2*b88*b817 + 2*b88*b879 + 2*b89*b90 - 2* b89*b923 + 2*b89*b924 + 2*b90*b134 - 4*b134 + 2*b90*b211 - 4*b211 + 2*b91* b92 - 2*b92 + 2*b91*b638 - 2*b638 + 2*b92*b211 + 2*b93*b94 - 2*b93 - 4*b94 + 2*b93*b391 + 2*b391 + 2*b94*b95 - 4*b95 + 2*b94*b390 - 2*b390 + 2*b94* b660 + 2*b95*b354 - 4*b354 + 2*b95*b654 + 2*b95*b881 + 2*b96*b600 - 2*b600 - 2*b96*b905 + 2*b97*b99 + 2*b97 - 2*b99 - 2*b97*b331 - 2*b331 - 2*b97* b550 + 2*b550 - 2*b97*b662 - 2*b98*b548 + 2*b98 + 2*b548 - 2*b98*b698 + 2* b98*b735 - 2*b98*b920 + 2*b99*b687 + 2*b99*b920 - 2*b99*b950 + 2*b100*b227 - 4*b100 - 4*b227 + 2*b100*b450 - 2*b450 + 2*b100*b835 + 2*b100*b851 + 2* b101*b262 - 2*b101 - 2*b262 + 2*b101*b450 - 2*b101*b785 + 2*b101*b836 + 2* b102*b124 - 4*b102 - 2*b124 + 2*b102*b371 - 2*b371 + 2*b102*b752 + 2*b102* b865 + 2*b103*b152 - 2*b152 + 2*b103*b339 - 2*b339 - 2*b103*b464 + 4*b464 + 2*b104*b153 - 2*b104 - 4*b153 - 2*b104*b568 + 2*b104*b648 + 2*b104*b788 + 2*b105*b425 - 2*b105 + 2*b105*b571 - 2*b571 - 2*b105*b643 + 2*b105*b855 + 2*b106*b157 - 4*b106 + 2*b106*b234 - 4*b234 + 2*b106*b571 + 2*b106*b816 + 2*b107*b803 + 2*b107*b870 - 2*b108*b109 - 2*b108 + 2*b109 + 2*b108*b645 + 2*b108*b657 + 2*b108*b870 + 2*b109*b159 - 4*b159 - 2*b109*b899 - 2*b109 *b953 + 2*b110*b111 + 2*b110*b923 + 2*b110*b935 + 2*b111*b159 + 2*b111* b242 - 4*b242 + 2*b112*b113 - 2*b113 + 2*b112*b582 - 2*b582 - 2*b112*b901 + 2*b113*b242 + 2*b114*b116 - 2*b114 - 4*b116 + 2*b114*b353 + 2*b353 + 2* b115*b352 - 2*b352 + 2*b115*b485 + 2*b485 - 2*b115*b937 + 2*b116*b435 - 2* b435 + 2*b116*b669 + 2*b116*b937 - 2*b117*b893 - 2*b118*b368 + 2*b368 + 2* b118*b686 + 2*b119*b121 + 2*b119 - 2*b121 - 2*b119*b294 - 2*b294 - 2*b119* b499 + 2*b499 - 2*b119*b656 - 2*b120*b497 + 2*b120 + 2*b497 - 2*b120*b710 + 2*b120*b723 - 2*b120*b907 + 2*b121*b698 + 2*b121*b907 - 2*b121*b959 + 2 *b122*b260 - 4*b122 - 4*b260 + 2*b122*b504 - 2*b504 + 2*b122*b822 + 2*b122 *b864 + 2*b123*b125 - 4*b123 + 2*b123*b410 - 4*b410 + 2*b123*b738 + 2*b123 *b852 + 2*b124*b262 + 2*b124*b725 - 2*b124*b961 - 2*b125*b960 + 2*b125* b961 + 2*b126*b128 - 2*b126 - 4*b128 + 2*b126*b301 - 2*b301 - 2*b126*b515 + 4*b515 + 2*b126*b728 + 2*b127*b129 - 4*b129 + 2*b127*b644 - 2*b127*b800 + 2*b128*b129 + 2*b128*b644 + 2*b128*b922 + 2*b129*b517 + 2*b129*b643 + 2 *b130*b469 - 4*b130 + 2*b130*b629 - 2*b629 + 2*b130*b648 + 2*b130*b842 + 2 *b131*b132 - 4*b132 + 2*b131*b789 + 2*b132*b183 + 2*b132*b269 - 4*b269 + 2 *b132*b629 + 2*b133*b791 + 2*b133*b856 + 2*b134*b135 - 2*b135 + 2*b134* b239 - 2*b239 + 2*b134*b911 + 2*b135*b184 - 4*b184 + 2*b135*b276 - 2*b276 - 2*b135*b857 + 2*b136*b137 - 2*b137 + 2*b136*b527 - 2*b527 + 2*b136*b901 + 2*b137*b276 + 2*b138*b140 - 2*b138 - 4*b140 + 2*b138*b730 + 2*b139*b532 + 2*b532 + 2*b139*b925 - 2*b139*b927 + 2*b140*b483 - 2*b483 + 2*b140*b682 + 2*b140*b927 + 2*b141*b143 - 2*b141 + 2*b141*b321 - 4*b321 - 2*b141*b365 + 2*b141*b903 - 2*b142*b707 + 2*b142 - 2*b142*b708 + 2*b142*b893 - 2*b142 *b968 - 2*b143*b285 + 2*b285 + 2*b143*b968 - 2*b144*b328 + 2*b328 + 2*b144 *b671 - 2*b145*b723 + 4*b145 - 2*b145*b724 - 2*b145*b895 - 2*b145*b896 + 2 *b146*b404 - 4*b146 - 4*b404 + 2*b146*b710 + 2*b146*b794 + 2*b146*b896 + 2 *b147*b296 - 4*b147 - 4*b296 + 2*b147*b555 - 2*b555 + 2*b147*b809 + 2*b147 *b875 + 2*b148*b150 - 4*b148 + 2*b148*b452 - 4*b452 + 2*b148*b726 + 2*b148 *b837 + 2*b149*b229 + 2*b149*b711 - 2*b149*b971 - 2*b150*b970 + 2*b150* b971 + 2*b151*b153 - 2*b151 + 2*b151*b265 - 2*b265 - 2*b151*b566 + 4*b566 + 2*b151*b716 + 2*b152*b154 + 2*b154 + 2*b152*b933 - 2*b152*b951 + 2*b153 *b910 + 2*b153*b951 - 2*b154*b466 + 2*b466 - 2*b154*b648 - 2*b154*b788 + 2 *b155*b156 - 2*b156 + 2*b156*b208 + 2*b156*b308 - 4*b308 - 2*b156*b630 - 2 *b630 + 2*b157*b778 + 2*b157*b843 + 2*b158*b235 - 2*b158 + 2*b158*b475 + 2 *b475 + 2*b158*b634 - 4*b634 - 2*b158*b912 + 2*b159*b160 - 2*b160 + 2*b159 *b273 - 2*b273 + 2*b160*b209 - 4*b209 + 2*b160*b314 - 2*b314 - 2*b160*b844 + 2*b161*b162 - 2*b162 + 2*b161*b479 - 4*b479 + 2*b162*b314 + 2*b163*b165 - 2*b163 - 4*b165 + 2*b163*b719 + 2*b164*b585 + 2*b585 + 2*b164*b913 - 2* b164*b915 + 2*b165*b531 - 2*b531 + 2*b165*b695 + 2*b165*b915 + 2*b166*b167 - 2*b167 - 2*b166*b917 + 2*b167*b169 + 2*b167*b362 - 4*b362 - 2*b167*b401 - 2*b168*b218 - 2*b218 - 2*b168*b722 + 2*b168*b904 + 2*b169*b218 - 2*b169 *b249 + 2*b249 + 2*b170*b172 - 2*b172 - 2*b170*b292 + 2*b292 + 2*b171*b290 + 2*b171*b330 - 2*b330 - 2*b171*b833 - 2*b172*b662 + 2*b172*b833 + 2*b172 *b969 - 2*b173*b405 + 4*b173 - 2*b405 - 2*b173*b735 - 2*b173*b737 - 2*b173 *b890 + 2*b174*b724 - 4*b174 + 2*b174*b808 + 2*b174*b890 + 2*b174*b959 + 2 *b175*b202 - 4*b175 - 4*b202 + 2*b175*b332 - 4*b332 + 2*b175*b610 - 2*b610 + 2*b175*b796 + 2*b176*b177 - 4*b176 + 2*b176*b506 - 4*b506 + 2*b176*b712 + 2*b176*b825 + 2*b177*b335 - 2*b335 - 2*b177*b977 + 2*b178*b299 - 4*b178 - 2*b299 + 2*b178*b335 + 2*b178*b458 + 2*b458 + 2*b178*b699 - 2*b179*b180 + 2*b180 + 2*b179*b727 + 2*b179*b775 + 2*b180*b423 + 2*b423 - 2*b180*b626 - 2*b180*b979 + 2*b181*b182 - 2*b182 + 2*b182*b234 + 2*b182*b346 - 4*b346 - 2*b182*b572 - 2*b572 + 2*b183*b766 + 2*b183*b829 + 2*b184*b185 - 4*b185 + 2*b184*b311 - 2*b311 + 2*b184*b900 + 2*b185*b240 - 4*b240 + 2*b185*b351 - 2*b351 + 2*b185*b844 + 2*b186*b187 - 2*b187 + 2*b186*b528 - 4*b528 + 2* b187*b351 + 2*b188*b681 - 2*b188 + 2*b188*b805 + 2*b188*b902 - 2*b188*b916 + 2*b189*b279 - 2*b189 + 2*b189*b437 - 2*b437 - 2*b189*b831 + 2*b189*b916 + 2*b190*b191 - 2*b191 + 2*b190*b929 + 2*b191*b193 + 2*b191*b398 - 4*b398 - 2*b191*b444 - 2*b192*b253 - 2*b253 - 2*b192*b733 + 2*b192*b917 - 2*b193 *b215 + 2*b215 + 2*b193*b253 + 2*b194*b196 - 2*b196 - 2*b194*b256 + 2*b256 + 2*b195*b196 - 2*b195 + 2*b195*b253 - 2*b195*b686 + 2*b195*b968 + 2*b196 *b197 - 2*b197 - 2*b196*b656 - 2*b197*b198 - 2*b198 + 2*b197*b849 + 2*b197 *b950 + 2*b198*b200 - 4*b200 + 2*b198*b670 + 2*b198*b821 - 2*b199*b446 - 2 *b446 - 2*b199*b750 - 2*b199*b884 + 2*b200*b737 + 2*b200*b884 + 2*b200* b950 + 2*b201*b228 - 4*b201 - 4*b228 + 2*b201*b369 - 4*b369 + 2*b201*b642 + 2*b201*b783 + 2*b202*b451 + 2*b202*b759 + 2*b202*b876 + 2*b203*b204 - 4 *b203 + 2*b203*b557 - 4*b557 + 2*b203*b700 + 2*b203*b812 + 2*b204*b372 - 2 *b372 - 2*b204*b985 - 2*b205*b764 + 2*b205 + 2*b205*b790 - 2*b205*b842 - 2 *b205*b987 + 2*b206*b207 - 2*b207 - 2*b206*b869 + 2*b207*b269 + 2*b207* b384 - 4*b384 - 2*b207*b521 - 2*b521 + 2*b208*b270 - 2*b270 + 2*b208*b817 + 2*b209*b210 - 4*b210 + 2*b209*b349 - 2*b349 + 2*b209*b912 + 2*b210*b274 - 4*b274 + 2*b210*b389 - 2*b389 + 2*b210*b857 + 2*b211*b212 - 2*b212 + 2* b211*b583 - 4*b583 + 2*b212*b389 + 2*b213*b486 - 2*b213 - 2*b486 - 2*b213* b819 + 2*b213*b928 + 2*b213*b990 + 2*b214*b216 - 2*b216 + 2*b214*b917 + 2* b214*b939 + 2*b215*b217 - 2*b215*b595 - 2*b595 - 2*b215*b661 + 2*b216*b217 + 2*b216*b442 - 4*b442 - 2*b216*b862 + 2*b217*b289 - 2*b289 + 2*b218*b220 - 2*b220 + 2*b218*b969 - 2*b219*b221 + 2*b221 + 2*b219*b222 - 4*b222 + 2* b220*b222 + 2*b220*b289 - 2*b220*b600 + 2*b221*b223 - 2*b223 - 2*b221*b599 - 2*b599 - 2*b221*b958 + 2*b222*b223 + 2*b222*b656 - 2*b223*b808 + 2*b223 *b941 + 2*b224*b225 - 2*b224 - 4*b225 + 2*b224*b685 - 2*b224*b833 + 2*b224 *b834 + 2*b225*b750 + 2*b225*b874 + 2*b225*b941 - 2*b226*b609 + 2*b609 + 2 *b226*b687 + 2*b226*b884 + 2*b227*b609 + 2*b227*b698 + 2*b227*b874 + 2* b228*b770 + 2*b228*b853 + 2*b228*b865 + 2*b229*b230 + 2*b229*b612 - 4*b612 + 2*b230*b412 - 2*b412 - 2*b230*b453 + 2*b453 - 2*b231*b755 + 2*b231 + 2* b231*b801 - 2*b231*b855 - 2*b231*b995 + 2*b232*b233 - 2*b233 + 2*b232*b573 + 2*b233*b308 + 2*b233*b428 - 4*b428 - 2*b233*b470 - 2*b470 + 2*b234*b236 - 4*b236 + 2*b234*b803 + 2*b235*b238 - 4*b238 + 2*b235*b576 - 4*b576 + 2* b236*b238 + 2*b236*b428 + 2*b236*b777 - 2*b237*b239 + 2*b237 + 2*b237*b474 - 4*b474 - 2*b237*b650 - 2*b237*b856 + 2*b238*b239 + 2*b238*b650 + 2*b239 *b312 - 4*b312 + 2*b240*b241 + 2*b240*b387 - 2*b387 + 2*b240*b924 + 2*b241 *b312 + 2*b241*b434 - 4*b434 + 2*b242*b243 - 2*b243 + 2*b242*b639 - 4*b639 + 2*b243*b434 + 2*b244*b356 - 2*b244 - 2*b356 + 2*b244*b533 - 2*b533 - 2* b244*b806 + 2*b244*b938 + 2*b245*b731 - 2*b245*b883 + 2*b246*b320 + 2*b246 - 4*b320 - 2*b246*b745 - 2*b246*b781 - 2*b246*b975 + 2*b247*b320 + 2*b247 *b683 + 2*b247*b883 + 2*b248*b250 - 4*b248 - 2*b250 + 2*b248*b904 + 2*b248 *b929 + 2*b248*b947 + 2*b249*b252 - 2*b249*b542 - 2*b542 - 2*b249*b655 + 2 *b250*b252 + 2*b250*b492 - 4*b492 - 2*b250*b709 - 2*b251*b325 - 2*b325 + 2 *b251*b544 - 4*b544 - 2*b251*b917 + 2*b252*b325 + 2*b253*b255 - 2*b255 + 2 *b254*b257 - 4*b257 - 2*b254*b849 + 2*b255*b257 + 2*b255*b325 - 2*b255* b546 - 2*b546 + 2*b256*b258 - 2*b258 - 2*b256*b545 - 2*b545 - 2*b256*b949 + 2*b257*b258 + 2*b257*b662 + 2*b258*b603 - 2*b258*b794 + 2*b259*b260 + 2 *b259 - 2*b259*b550 - 2*b259*b822 - 2*b259*b997 + 2*b260*b554 + 2*b554 + 2 *b260*b710 + 2*b261*b782 - 2*b261 + 2*b261*b852 + 2*b261*b866 - 2*b261* b897 + 2*b262*b263 - 2*b262*b641 + 2*b263*b455 - 2*b455 - 2*b263*b507 + 2* b507 + 2*b264*b337 - 2*b264 + 2*b337 + 2*b264*b455 - 2*b264*b616 + 2*b616 + 2*b264*b961 + 2*b265*b338 - 2*b338 - 2*b265*b463 + 2*b463 + 2*b265*b787 - 2*b266*b742 + 2*b266 + 2*b266*b815 - 2*b266*b867 - 2*b266*b1000 + 2* b267*b268 - 2*b268 + 2*b267*b869 + 2*b268*b346 - 2*b268*b426 - 2*b426 + 2* b268*b472 - 4*b472 + 2*b269*b271 - 4*b271 + 2*b269*b791 + 2*b270*b384 + 2* b270*b765 - 2*b270*b988 + 2*b271*b431 + 2*b431 + 2*b271*b472 + 2*b271*b988 - 2*b272*b273 + 2*b272 + 2*b272*b430 - 4*b430 - 2*b272*b579 - 2*b272*b843 + 2*b273*b350 - 4*b350 + 2*b273*b988 + 2*b274*b275 + 2*b274*b432 - 2*b432 + 2*b274*b935 + 2*b275*b350 + 2*b275*b480 - 4*b480 + 2*b276*b277 - 2*b277 - 2*b276*b678 + 2*b277*b480 + 2*b278*b393 - 2*b278 - 2*b393 + 2*b278*b586 - 4*b586 - 2*b278*b792 + 2*b278*b945 + 2*b279*b654 - 2*b279*b982 + 2*b280 *b720 + 2*b280*b831 - 2*b280*b873 - 2*b281*b651 + 4*b281 - 2*b281*b747 - 2 *b281*b991 - 2*b281*b992 + 2*b282*b361 + 2*b282 - 4*b361 - 2*b282*b731 - 2 *b282*b793 - 2*b282*b966 + 2*b283*b442 - 2*b283 + 2*b283*b541 - 4*b541 + 2 *b283*b769 - 2*b283*b992 + 2*b284*b286 - 4*b284 - 4*b286 + 2*b284*b893 + 2 *b284*b939 + 2*b284*b956 + 2*b285*b288 - 2*b285*b493 - 2*b493 - 2*b285* b652 + 2*b286*b288 + 2*b286*b541 + 2*b286*b862 - 2*b287*b367 - 2*b367 + 2* b287*b543 - 2*b543 - 2*b287*b904 + 2*b288*b367 + 2*b289*b291 - 2*b291 - 2* b289*b748 + 2*b290*b293 - 4*b293 - 2*b290*b598 - 2*b598 + 2*b291*b293 + 2* b291*b367 - 2*b291*b930 + 2*b292*b294 - 2*b292*b495 - 2*b495 - 2*b292*b940 + 2*b293*b294 + 2*b293*b670 + 2*b294*b548 + 2*b295*b296 + 2*b295 - 2*b295 *b499 - 2*b295*b835 - 2*b295*b1002 + 2*b296*b503 + 2*b503 + 2*b296*b724 + 2*b297*b795 - 2*b297 + 2*b297*b837 + 2*b297*b877 - 2*b297*b908 + 2*b298* b813 - 2*b298 - 2*b298*b898 + 2*b298*b971 + 2*b298*b1004 + 2*b299*b300 - 2 *b299*b373 - 2*b373 + 2*b299*b417 - 2*b417 + 2*b300*b302 - 2*b302 + 2*b300 *b813 + 2*b301*b375 - 2*b375 - 2*b301*b420 + 2*b420 + 2*b301*b774 + 2*b302 *b420 + 2*b302*b619 - 2*b619 - 2*b302*b933 - 2*b303*b304 + 2*b303 + 2*b304 - 2*b303*b622 + 2*b622 - 2*b303*b691 + 2*b303*b729 + 2*b304*b305 - 2*b304 *b878 - 2*b304*b1005 - 2*b305*b729 + 2*b305*b1006 + 2*b306*b307 - 2*b307 + 2*b307*b384 + 2*b307*b522 - 4*b522 - 2*b307*b1007 + 2*b308*b309 - 4* b309 + 2*b308*b778 + 2*b309*b386 + 2*b386 + 2*b309*b522 + 2*b309*b980 - 2* b310*b311 + 2*b310 + 2*b310*b385 - 4*b385 - 2*b310*b524 - 2*b310*b829 + 2* b311*b388 - 4*b388 + 2*b311*b980 + 2*b312*b313 + 2*b312*b476 - 2*b476 + 2* b313*b388 + 2*b313*b529 - 4*b529 + 2*b314*b315 - 2*b315 - 2*b314*b666 + 2* b315*b529 + 2*b316*b705 + 2*b316*b819 - 2*b316*b861 - 2*b317*b359 - 2*b317 + 2*b317*b438 - 2*b438 + 2*b317*b861 + 2*b317*b990 - 2*b318*b647 + 4*b318 - 2*b318*b757 - 2*b318*b982 - 2*b318*b984 + 2*b319*b397 + 2*b319 - 4*b397 - 2*b319*b720 - 2*b319*b807 - 2*b319*b956 + 2*b320*b492 + 2*b320*b594 - 4 *b594 + 2*b321*b322 - 4*b322 + 2*b321*b947 + 2*b321*b966 + 2*b322*b324 + 2 *b322*b444 + 2*b322*b594 - 2*b323*b403 - 2*b403 + 2*b323*b596 - 2*b596 - 2 *b323*b893 + 2*b324*b403 + 2*b324*b707 + 2*b325*b327 - 2*b327 + 2*b326* b329 - 4*b329 - 2*b326*b848 + 2*b326*b849 + 2*b327*b329 + 2*b327*b403 - 2* b327*b918 + 2*b328*b331 - 2*b328*b889 - 2*b328*b931 + 2*b329*b331 + 2*b329 *b685 + 2*b330*b404 - 2*b330*b497 + 2*b330*b905 + 2*b331*b497 + 2*b332* b448 + 2*b448 + 2*b332*b737 + 2*b332*b850 + 2*b333*b334 + 2*b333*b825 - 2* b333*b921 - 2*b334*b1010 + 2*b334*b1011 + 2*b335*b336 - 2*b336 - 2*b335* b700 + 2*b336*b799 - 2*b336*b909 + 2*b336*b1012 - 2*b337*b676 - 2*b337* b740 - 2*b337*b999 + 2*b338*b713 + 2*b338*b898 - 2*b338*b942 - 2*b339*b378 + 2*b378 + 2*b339*b417 + 2*b339*b762 - 2*b340*b341 + 2*b340 + 2*b341 - 2* b340*b703 + 2*b340*b717 - 2*b340*b891 + 2*b341*b342 - 2*b341*b886 - 2*b341 *b1014 + 2*b342*b468 - 2*b468 - 2*b342*b717 + 2*b343*b345 - 4*b345 + 2* b344*b345 - 4*b344 + 2*b344*b468 + 2*b344*b573 + 2*b344*b776 + 2*b345*b428 + 2*b345*b575 - 4*b575 + 2*b346*b347 - 4*b347 + 2*b346*b766 + 2*b347*b348 + 2*b348 + 2*b347*b575 + 2*b347*b974 - 2*b348*b349 - 2*b348*b475 - 2*b348 *b817 + 2*b349*b433 - 4*b433 + 2*b349*b974 + 2*b350*b525 - 2*b525 + 2*b350 *b638 - 2*b351*b658 + 2*b351*b1015 + 2*b352*b354 - 2*b353*b355 - 2*b355 - 2*b353*b660 - 2*b353*b858 + 2*b354*b355 + 2*b354*b584 - 2*b584 + 2*b355* b767 + 2*b355*b859 + 2*b356*b358 - 2*b358 - 2*b356*b859 + 2*b356*b991 + 2* b357*b696 + 2*b357*b806 - 2*b357*b847 - 2*b358*b395 + 2*b358*b488 - 2*b488 + 2*b358*b847 - 2*b359*b768 - 2*b359*b976 + 2*b360*b441 + 2*b360 - 4*b441 - 2*b360*b705 - 2*b360*b820 - 2*b360*b947 + 2*b361*b363 - 2*b363 + 2*b361 *b541 + 2*b361*b992 + 2*b362*b364 - 4*b364 + 2*b362*b956 + 2*b362*b975 + 2 *b363*b364 + 2*b363*b441 - 2*b363*b733 + 2*b364*b366 + 2*b364*b401 + 2* b365*b400 - 4*b400 - 2*b365*b445 - 2*b445 + 2*b366*b445 + 2*b366*b722 + 2* b367*b906 + 2*b368*b758 - 2*b368*b894 - 2*b368*b919 + 2*b369*b407 + 2*b407 + 2*b369*b750 + 2*b369*b863 + 2*b370*b371 - 2*b370*b449 + 2*b449 + 2*b370 *b812 + 2*b371*b507 - 2*b371*b1019 + 2*b372*b373 - 2*b372*b712 + 2*b372* b972 + 2*b373*b786 + 2*b373*b1020 - 2*b374*b690 + 2*b374*b962 - 2*b374* b994 - 2*b375*b377 - 2*b377 + 2*b375*b701 + 2*b375*b909 + 2*b376*b727 + 2* b376*b840 - 2*b376*b841 + 2*b377*b841 + 2*b377*b933 + 2*b377*b994 - 2*b378 *b515 + 2*b378*b942 - 2*b378*b1014 - 2*b379*b380 + 4*b379 - 2*b380 - 2* b379*b715 - 2*b379*b717 - 2*b379*b885 + 2*b380*b381 + 2*b380*b886 + 2*b380 *b1014 + 2*b381*b519 - 2*b519 + 2*b381*b717 + 2*b382*b383 - 4*b383 + 2* b383*b472 + 2*b383*b633 - 4*b633 + 2*b383*b1007 + 2*b384*b385 + 2*b385* b633 + 2*b385*b965 - 2*b386*b387 - 2*b386*b653 - 2*b386*b803 + 2*b387*b477 - 2*b477 + 2*b387*b965 + 2*b388*b580 - 4*b580 + 2*b388*b582 - 2*b389*b478 + 2*b389*b1022 + 2*b390*b1008 - 2*b391*b392 - 2*b392 - 2*b391*b669 - 2* b391*b845 + 2*b392*b756 + 2*b392*b846 + 2*b392*b1008 + 2*b393*b394 - 2* b394 - 2*b393*b871 + 2*b393*b982 + 2*b394*b535 - 2*b535 + 2*b394*b832 - 2* b394*b955 + 2*b395*b590 - 4*b590 - 2*b395*b967 + 2*b396*b491 + 2*b396 - 4* b491 - 2*b396*b696 - 2*b396*b832 - 2*b396*b939 + 2*b397*b399 - 2*b399 + 2* b397*b594 + 2*b397*b984 + 2*b398*b400 + 2*b398*b966 + 2*b398*b983 + 2*b399 *b400 + 2*b399*b491 - 2*b399*b722 + 2*b400*b402 - 2*b401*b494 - 2*b494 + 2 *b402*b494 + 2*b402*b733 + 2*b403*b894 + 2*b404*b406 - 4*b406 + 2*b404* b601 - 2*b601 + 2*b405*b406 + 2*b405*b749 + 2*b405*b931 + 2*b406*b606 - 2* b606 + 2*b406*b672 - 2*b407*b450 - 2*b407*b784 - 2*b407*b1019 - 2*b408* b409 + 2*b408 - 2*b408*b771 + 2*b408*b1019 - 2*b408*b1024 + 2*b409*b410 + 2*b410*b453 + 2*b410*b1019 - 2*b411*b413 + 2*b413 - 2*b411*b785 + 2*b412* b414 - 4*b414 - 2*b412*b726 + 2*b412*b962 + 2*b413*b414 - 2*b413*b714 - 2* b413*b1025 + 2*b414*b416 - 2*b416 + 2*b414*b909 - 2*b415*b702 + 2*b415 - 2 *b415*b762 + 2*b415*b972 - 2*b415*b986 - 2*b416*b689 + 2*b416*b773 + 2* b416*b986 - 2*b417*b419 - 2*b419 + 2*b417*b688 + 2*b418*b715 - 2*b418 + 2* b418*b740 + 2*b418*b827 - 2*b418*b828 + 2*b419*b828 + 2*b419*b922 + 2*b419 *b986 - 2*b420*b464 - 2*b420*b1005 - 2*b421*b422 + 4*b421 - 2*b422 - 2* b421*b463 - 2*b421*b727 - 2*b421*b729 + 2*b422*b424 + 2*b422*b878 + 2*b422 *b1005 - 2*b423*b570 - 2*b570 - 2*b423*b775 - 2*b423*b776 + 2*b424*b570 + 2*b424*b729 + 2*b425*b427 - 4*b427 + 2*b426*b427 + 2*b426*b570 + 2*b426* b1006 + 2*b427*b429 - 2*b429 + 2*b427*b522 + 2*b428*b430 + 2*b429*b430 + 2 *b429*b574 - 4*b574 - 2*b429*b645 + 2*b430*b953 - 2*b431*b432 - 2*b431* b657 - 2*b431*b791 + 2*b432*b526 - 2*b526 + 2*b432*b953 + 2*b433*b527 + 2* b433*b636 - 4*b636 + 2*b433*b638 + 2*b434*b658 + 2*b434*b1026 + 2*b435* b1001 - 2*b436*b437 - 2*b436*b682 - 2*b436*b830 + 2*b437*b744 + 2*b437* b1001 + 2*b438*b439 - 2*b439 + 2*b438*b780 - 2*b438*b881 + 2*b439*b588 - 2 *b588 + 2*b439*b820 - 2*b439*b946 + 2*b440*b539 + 2*b440 - 4*b539 - 2*b440 *b683 - 2*b440*b847 - 2*b440*b929 + 2*b441*b443 - 2*b443 + 2*b441*b976 + 2 *b442*b596 + 2*b442*b975 + 2*b443*b539 + 2*b443*b596 - 2*b443*b707 - 2* b444*b1028 + 2*b445*b889 + 2*b445*b906 + 2*b446*b736 + 2*b446*b940 + 2* b446*b1018 - 2*b447*b449 + 2*b447 - 2*b447*b737 + 2*b447*b759 - 2*b447* b932 - 2*b448*b504 - 2*b448*b797 - 2*b448*b1010 + 2*b449*b1010 - 2*b449* b1031 + 2*b450*b452 + 2*b451*b642 - 2*b451*b985 + 2*b452*b985 + 2*b452* b1010 - 2*b453*b853 - 2*b453*b1025 - 2*b454*b798 - 2*b454*b854 + 2*b455* b457 - 4*b457 - 2*b455*b738 - 2*b456*b459 - 2*b459 - 2*b456*b699 - 2*b456* b701 + 2*b457*b459 + 2*b457*b854 + 2*b457*b898 - 2*b458*b460 - 2*b460 - 2* b458*b714 - 2*b458*b774 + 2*b459*b460 + 2*b459*b761 + 2*b460*b462 - 2*b462 + 2*b460*b978 + 2*b461*b562 - 2*b461 + 2*b562 + 2*b461*b703 + 2*b461*b753 - 2*b461*b814 + 2*b462*b814 - 2*b462*b840 + 2*b462*b910 + 2*b463*b963 - 2 *b463*b1000 - 2*b464*b465 - 2*b465 - 2*b464*b741 + 2*b465*b467 + 2*b465* b867 + 2*b465*b1000 - 2*b466*b628 - 2*b628 - 2*b466*b789 + 2*b466*b951 + 2 *b467*b628 + 2*b467*b741 + 2*b468*b470 - 2*b468*b801 + 2*b469*b471 - 4* b471 + 2*b470*b471 + 2*b470*b628 + 2*b471*b473 - 4*b473 + 2*b471*b575 + 2* b472*b474 + 2*b473*b474 + 2*b473*b632 - 4*b632 + 2*b473*b645 + 2*b474*b944 - 2*b475*b581 - 2*b581 - 2*b475*b649 + 2*b476*b581 - 2*b476*b777 + 2*b476 *b944 + 2*b477*b479 + 2*b477*b582 - 2*b477*b657 + 2*b478*b481 + 2*b478* b649 + 2*b479*b481 + 2*b479*b581 + 2*b480*b482 - 2*b482 + 2*b480*b666 + 2* b481*b482 + 2*b483*b996 - 2*b484*b486 - 2*b484*b695 - 2*b484*b818 - 2*b485 *b487 - 2*b487 - 2*b485*b654 - 2*b485*b730 + 2*b486*b487 + 2*b486*b996 + 2 *b487*b489 - 2*b489 + 2*b487*b743 + 2*b488*b490 - 4*b490 + 2*b488*b767 - 2 *b488*b936 + 2*b489*b490 - 2*b489*b768 + 2*b489*b914 + 2*b490*b807 + 2* b490*b946 + 2*b491*b493 + 2*b491*b967 + 2*b492*b543 + 2*b492*b983 + 2*b493 *b543 + 2*b493*b592 - 4*b592 + 2*b494*b495 + 2*b494*b894 + 2*b495*b1030 + 2*b495*b1032 + 2*b496*b498 - 2*b496 - 2*b498 - 2*b496*b723 + 2*b496*b930 + 2*b496*b1030 - 2*b497*b1009 - 2*b498*b605 + 2*b498*b949 + 2*b498*b1009 + 2*b499*b500 - 4*b500 - 2*b499*b604 - 2*b604 + 2*b500*b502 - 4*b502 + 2* b500*b783 + 2*b500*b1009 - 2*b501*b750 + 4*b501 - 2*b501*b751 - 2*b501* b920 - 2*b501*b921 + 2*b502*b672 + 2*b502*b751 + 2*b502*b921 - 2*b503*b555 - 2*b503*b810 - 2*b503*b1003 + 2*b504*b506 + 2*b504*b611 - 2*b611 + 2* b505*b610 + 2*b505*b875 - 2*b505*b977 + 2*b506*b977 + 2*b506*b1003 - 2* b507*b866 - 2*b507*b1021 - 2*b508*b511 - 2*b511 - 2*b508*b711 - 2*b508* b713 + 2*b509*b511 - 4*b509 + 2*b509*b616 + 2*b509*b839 + 2*b509*b1004 - 2 *b510*b512 + 2*b510 - 2*b512 + 2*b510*b615 - 4*b615 - 2*b510*b787 - 2*b510 *b972 + 2*b511*b512 + 2*b511*b753 + 2*b512*b514 - 2*b514 + 2*b512*b973 + 2 *b513*b618 - 2*b513 + 2*b618 + 2*b513*b691 + 2*b513*b761 - 2*b513*b800 + 2 *b514*b622 + 2*b514*b800 - 2*b514*b827 - 2*b515*b516 - 2*b516 - 2*b515* b754 + 2*b516*b518 + 2*b516*b855 + 2*b516*b995 - 2*b517*b644 - 2*b517*b964 + 2*b518*b754 + 2*b518*b964 + 2*b519*b521 - 2*b519*b790 + 2*b519*b1007 + 2*b520*b631 - 2*b631 - 2*b520*b943 + 2*b521*b631 + 2*b521*b964 + 2*b522* b523 - 2*b523 + 2*b523*b677 + 2*b523*b934 - 2*b523*b1034 - 2*b524*b637 - 2 *b637 + 2*b524*b693 + 2*b525*b637 - 2*b525*b765 + 2*b525*b934 + 2*b526* b527 + 2*b526*b528 - 2*b526*b653 - 2*b527*b1027 + 2*b528*b637 + 2*b528* b1027 + 2*b529*b530 - 2*b530 + 2*b529*b678 + 2*b530*b1027 + 2*b531*b989 - 2*b532*b534 - 2*b532*b659 - 2*b532*b719 + 2*b533*b534 - 2*b533*b804 + 2* b533*b989 + 2*b534*b536 - 2*b536 + 2*b535*b537 - 4*b537 + 2*b535*b756 - 2* b535*b926 + 2*b536*b537 - 2*b536*b757 + 2*b536*b926 + 2*b537*b793 + 2*b537 *b955 + 2*b538*b540 - 2*b538 - 2*b540 + 2*b538*b793 - 2*b538*b939 + 2*b538 *b946 + 2*b539*b542 + 2*b539*b957 + 2*b540*b542 - 2*b540*b661 + 2*b540* b872 + 2*b541*b544 + 2*b542*b544 - 2*b543*b1033 + 2*b544*b1033 + 2*b545* b848 + 2*b545*b1023 + 2*b545*b1028 + 2*b546*b547 - 4*b547 + 2*b546*b734 + 2*b546*b940 + 2*b547*b549 - 2*b549 + 2*b547*b723 + 2*b547*b1023 - 2*b548* b919 - 2*b548*b1002 - 2*b549*b550 + 2*b549*b958 + 2*b549*b1002 + 2*b550* b552 - 4*b552 + 2*b551*b796 - 2*b551 + 2*b551*b834 + 2*b551*b1018 - 2*b551 *b1031 + 2*b552*b608 + 2*b608 + 2*b552*b1002 + 2*b552*b1031 + 2*b553*b607 + 2*b553 - 4*b607 - 2*b553*b759 - 2*b553*b907 - 2*b553*b908 - 2*b554*b610 - 2*b554*b823 - 2*b554*b998 + 2*b555*b556 - 2*b556 + 2*b555*b557 + 2*b556 *b811 + 2*b556*b864 - 2*b556*b970 + 2*b557*b970 + 2*b557*b998 + 2*b558* b699 + 2*b558*b785 - 2*b558*b826 + 2*b559*b560 - 4*b559 + 2*b560 + 2*b559* b561 - 2*b561 + 2*b559*b826 + 2*b559*b1012 - 2*b560*b563 - 2*b563 - 2*b560 *b618 - 2*b560*b962 + 2*b561*b563 - 2*b561*b739 + 2*b561*b740 - 2*b562* b564 - 2*b564 - 2*b562*b616 - 2*b562*b663 + 2*b563*b564 + 2*b563*b963 + 2* b564*b565 - 2*b565 + 2*b564*b891 - 2*b565*b692 + 2*b565*b788 + 2*b565*b987 - 2*b566*b567 - 2*b567 - 2*b566*b763 - 2*b566*b841 + 2*b567*b569 + 2*b567 *b842 + 2*b567*b987 - 2*b568*b951 - 2*b568*b952 + 2*b569*b763 + 2*b569* b952 + 2*b570*b572 + 2*b571*b574 - 2*b571*b952 + 2*b572*b574 + 2*b572*b952 + 2*b573*b576 + 2*b574*b576 + 2*b575*b577 - 4*b577 + 2*b576*b577 + 2*b577 *b578 - 2*b578 + 2*b577*b693 + 2*b578*b580 - 2*b578*b843 + 2*b578*b923 + 2 *b579*b677 - 2*b579*b679 + 2*b580*b679 + 2*b580*b765 + 2*b581*b583 - 2* b582*b640 + 2*b640 + 2*b583*b640 + 2*b583*b679 + 2*b584*b981 - 2*b585*b587 - 2*b585*b668 - 2*b585*b704 + 2*b586*b587 + 2*b586*b804 + 2*b586*b981 + 2 *b587*b589 - 2*b589 + 2*b588*b590 + 2*b588*b744 - 2*b588*b914 + 2*b589* b590 - 2*b589*b747 + 2*b589*b936 + 2*b590*b781 + 2*b591*b593 - 2*b591 - 2* b593 + 2*b591*b781 - 2*b591*b929 + 2*b591*b955 + 2*b592*b595 + 2*b592*b860 + 2*b592*b948 + 2*b593*b595 - 2*b593*b655 + 2*b593*b882 + 2*b594*b597 - 4 *b597 + 2*b595*b597 - 2*b596*b1029 + 2*b597*b748 + 2*b597*b1029 + 2*b598* b599 + 2*b598*b862 + 2*b598*b1029 + 2*b599*b1017 + 2*b599*b1032 + 2*b600* b602 - 4*b602 + 2*b600*b949 + 2*b601*b604 + 2*b601*b671 - 2*b601*b849 + 2* b602*b604 + 2*b602*b735 + 2*b602*b1017 - 2*b603*b931 - 2*b603*b997 + 2* b604*b997 + 2*b605*b607 - 2*b605*b874 + 2*b606*b809 + 2*b606*b821 - 2*b606 *b1024 + 2*b607*b997 + 2*b607*b1024 - 2*b608*b770 - 2*b608*b896 - 2*b608* b897 - 2*b609*b642 - 2*b609*b993 + 2*b610*b612 + 2*b611*b798 + 2*b611*b851 - 2*b611*b960 + 2*b612*b960 + 2*b612*b993 + 2*b613*b614 - 2*b613 - 2*b614 + 2*b613*b960 - 2*b613*b1004 + 2*b613*b1011 + 2*b614*b615 - 2*b614*b665 + 2*b614*b838 + 2*b615*b617 + 2*b615*b1020 - 2*b616*b619 + 2*b617*b619 + 2*b617*b739 - 2*b618*b621 - 2*b621 - 2*b618*b674 + 2*b619*b621 - 2*b620* b623 + 2*b620 - 2*b623 - 2*b620*b703 - 2*b620*b773 + 2*b620*b774 + 2*b621* b623 + 2*b621*b885 - 2*b622*b978 - 2*b622*b979 + 2*b623*b624 + 2*b624 + 2* b623*b979 - 2*b624*b625 - 2*b625 - 2*b624*b775 - 2*b624*b828 + 2*b625*b626 + 2*b625*b627 + 2*b625*b979 - 2*b626*b943 + 2*b627*b775 + 2*b627*b943 + 2 *b628*b630 + 2*b629*b632 - 2*b629*b964 + 2*b630*b632 + 2*b630*b943 + 2* b631*b633 - 2*b631*b1034 + 2*b632*b1034 + 2*b633*b634 + 2*b634*b635 - 2* b635 + 2*b634*b1034 + 2*b635*b636 - 2*b635*b856 + 2*b635*b911 + 2*b636* b667 + 2*b636*b777 + 2*b637*b639 - 2*b638*b1016 + 2*b639*b667 + 2*b639* b1016 - 2*b640*b1022 - 2*b640*b1035 - 2*b641*b642 + 2*b641*b785 - 2*b643* b644 + 2*b643*b776 - 2*b645*b718 - 2*b646*b647 - 2*b646*b652 + 2*b646*b655 + 2*b647*b745 + 2*b649*b650 - 2*b649*b658 - 2*b650*b667 + 2*b651*b731 + 2 *b652*b707 + 2*b653*b718 - 2*b654*b831 + 2*b655*b722 + 2*b656*b794 + 2* b659*b660 - 2*b659*b819 - 2*b660*b744 + 2*b661*b733 + 2*b662*b808 - 2*b663 *b664 + 2*b663*b665 + 2*b663*b827 - 2*b664*b799 - 2*b665*b813 - 2*b666* b667 + 2*b668*b669 - 2*b668*b806 - 2*b669*b756 - 2*b670*b671 - 2*b671*b969 - 2*b672*b673 - 2*b672*b823 + 2*b673*b932 - 2*b673*b941 - 2*b674*b675 + 2 *b674*b676 + 2*b674*b840 + 2*b675*b725 - 2*b675*b786 - 2*b676*b826 - 2* b677*b870 - 2*b677*b935 - 2*b678*b679 - 2*b680*b681 + 2*b680*b682 - 2*b680 *b792 - 2*b681*b694 - 2*b682*b767 - 2*b683*b684 + 2*b684*b792 + 2*b684* b831 - 2*b684*b832 - 2*b685*b686 + 2*b686*b958 - 2*b687*b810 - 2*b688*b689 + 2*b688*b690 - 2*b688*b787 + 2*b689*b711 - 2*b690*b839 - 2*b691*b692 + 2 *b691*b742 + 2*b692*b773 + 2*b692*b787 - 2*b693*b879 - 2*b693*b924 + 2* b694*b818 + 2*b694*b892 - 2*b694*b928 - 2*b695*b780 - 2*b696*b697 + 2*b696 *b860 + 2*b697*b779 + 2*b697*b819 - 2*b697*b820 - 2*b698*b797 - 2*b699* b700 + 2*b701*b702 - 2*b701*b774 - 2*b702*b854 + 2*b703*b755 + 2*b704*b830 + 2*b704*b888 - 2*b704*b938 - 2*b705*b706 + 2*b705*b872 + 2*b706*b806 - 2 *b706*b807 + 2*b708*b709 - 2*b708*b734 - 2*b709*b848 - 2*b710*b784 - 2* b711*b712 + 2*b713*b714 - 2*b713*b762 - 2*b715*b716 + 2*b715*b764 - 2*b716 *b761 + 2*b716*b762 + 2*b718*b879 - 2*b718*b900 + 2*b719*b845 - 2*b719* b945 - 2*b720*b721 + 2*b720*b882 + 2*b721*b792 - 2*b721*b793 - 2*b724*b771 - 2*b725*b726 - 2*b725*b739 - 2*b727*b728 - 2*b728*b753 + 2*b730*b858 - 2 *b730*b954 - 2*b731*b732 + 2*b732*b743 + 2*b732*b779 - 2*b732*b781 - 2* b734*b918 - 2*b735*b736 + 2*b736*b918 - 2*b736*b1030 + 2*b741*b742 - 2* b741*b815 - 2*b742*b910 - 2*b743*b744 - 2*b743*b746 - 2*b745*b746 + 2*b745 *b747 + 2*b749*b905 - 2*b749*b1023 - 2*b751*b875 - 2*b752*b1004 - 2*b753* b813 + 2*b754*b755 - 2*b754*b801 - 2*b755*b922 + 2*b758*b895 - 2*b758* b1017 - 2*b759*b864 + 2*b760*b811 - 2*b760*b1012 - 2*b761*b799 + 2*b763* b764 - 2*b763*b790 - 2*b764*b933 - 2*b765*b766 - 2*b766*b980 - 2*b769*b983 + 2*b770*b771 - 2*b770*b851 + 2*b771*b932 + 2*b772*b798 - 2*b772*b1020 - 2*b773*b786 - 2*b776*b816 - 2*b777*b778 - 2*b778*b974 - 2*b779*b780 + 2* b780*b954 - 2*b782*b783 + 2*b782*b784 - 2*b782*b836 - 2*b783*b890 + 2*b784 *b920 + 2*b786*b994 - 2*b788*b814 + 2*b789*b790 - 2*b789*b802 - 2*b791* b965 - 2*b794*b834 - 2*b795*b796 + 2*b795*b797 - 2*b795*b824 - 2*b796*b884 + 2*b797*b907 + 2*b799*b999 + 2*b800*b995 - 2*b803*b953 - 2*b804*b805 + 2 *b807*b948 - 2*b808*b821 - 2*b809*b874 + 2*b810*b896 - 2*b811*b812 - 2* b811*b838 + 2*b814*b1000 - 2*b815*b1006 - 2*b817*b944 + 2*b820*b957 - 2* b821*b863 + 2*b822*b863 + 2*b823*b890 - 2*b824*b825 + 2*b826*b1013 - 2* b827*b898 + 2*b828*b1005 - 2*b829*b934 + 2*b832*b967 + 2*b833*b959 - 2* b834*b850 + 2*b835*b850 - 2*b836*b837 - 2*b838*b839 + 2*b839*b1021 - 2* b840*b909 + 2*b841*b1014 - 2*b844*b887 + 2*b846*b915 - 2*b846*b990 + 2* b847*b976 + 2*b848*b1033 - 2*b850*b1009 - 2*b851*b852 - 2*b853*b993 + 2* b854*b1025 + 2*b856*b868 - 2*b857*b880 + 2*b859*b927 - 2*b860*b861 + 2* b861*b984 - 2*b862*b1032 - 2*b863*b1018 - 2*b864*b865 - 2*b866*b998 - 2* b868*b869 - 2*b868*b870 + 2*b871*b937 + 2*b871*b954 - 2*b872*b873 + 2*b873 *b982 + 2*b873*b992 - 2*b875*b876 - 2*b877*b1003 - 2*b877*b1011 + 2*b881* b945 - 2*b882*b883 + 2*b883*b991 + 2*b885*b973 - 2*b885*b995 - 2*b888*b981 + 2*b889*b1028 - 2*b889*b1030 + 2*b891*b978 - 2*b891*b987 - 2*b892*b989 - 2*b894*b1023 + 2*b895*b919 - 2*b895*b1018 + 2*b897*b993 + 2*b897*b1024 + 2*b899*b900 - 2*b899*b901 - 2*b900*b965 - 2*b902*b996 - 2*b903*b904 - 2 *b905*b906 - 2*b906*b1017 + 2*b908*b998 + 2*b908*b1031 - 2*b910*b973 - 2* b911*b944 - 2*b912*b974 - 2*b913*b1001 - 2*b914*b915 + 2*b914*b916 - 2* b916*b981 + 2*b918*b919 + 2*b921*b1003 - 2*b922*b963 - 2*b923*b934 - 2* b924*b980 - 2*b925*b1008 - 2*b926*b927 + 2*b926*b928 - 2*b928*b989 + 2* b930*b931 - 2*b935*b988 - 2*b936*b937 + 2*b936*b938 - 2*b938*b996 - 2*b940 *b941 + 2*b942*b999 - 2*b945*b1001 - 2*b946*b948 - 2*b947*b948 - 2*b949* b950 - 2*b954*b1008 - 2*b955*b957 - 2*b956*b957 - 2*b958*b959 - 2*b961* b962 - 2*b963*b999 - 2*b966*b967 - 2*b968*b969 + 2*b970*b1013 - 2*b971* b972 - 2*b973*b994 - 2*b975*b976 + 2*b977*b1021 - 2*b978*b986 - 2*b983* b984 + 2*b985*b1025 - 2*b990*b991 - 2*b1006*b1007 - 2*b1011*b1013 - 2* b1012*b1013 - 2*b1015*b1016 + 2*b1016*b1035 - 2*b1020*b1021 - 2*b1026* b1027 - 2*b1028*b1029 - 2*b1032*b1033 + objvar <= 0 } } Procedure MainInitialization; MathematicalProgram sporttournament46 { Objective: objvar; Direction: maximize; Constraints: AllConstraints; Variables: AllVariables; Type: MINLP; } ElementParameter myGMP { Range: AllGeneratedMathematicalPrograms; } Procedure MainExecution { Body: { solve sporttournament46; } } Procedure MainTermination { Body: { return 1; } } }