\* Problem: Unknown *\ Maximize obj: 0 z_1 Subject To r_1: + z_5 + z_4 + z_3 + z_2 + z_1 <= 1 r_2: + z_10 + z_9 + z_8 + z_7 + z_6 <= 1 r_3: + z_15 + z_14 + z_13 + z_12 + z_11 <= 1 r_4: + z_20 + z_19 + z_18 + z_17 + z_16 <= 1 r_5: + z_25 + z_24 + z_23 + z_22 + z_21 <= 1 r_6: + z_30 + z_29 + z_28 + z_27 + z_26 <= 1 r_7: + z_35 + z_34 + z_33 + z_32 + z_31 <= 1 r_8: + z_40 + z_39 + z_38 + z_37 + z_36 <= 1 r_9: + z_45 + z_44 + z_43 + z_42 + z_41 <= 1 r_10: + z_50 + z_49 + z_48 + z_47 + z_46 <= 1 r_11: + z_55 + z_54 + z_53 + z_52 + z_51 <= 1 r_12: + z_60 + z_59 + z_58 + z_57 + z_56 <= 1 r_13: + z_65 + z_64 + z_63 + z_62 + z_61 <= 1 r_14: + z_70 + z_69 + z_68 + z_67 + z_66 <= 1 r_15: + z_75 + z_74 + z_73 + z_72 + z_71 <= 1 r_16: + z_80 + z_79 + z_78 + z_77 + z_76 <= 1 r_17: + z_85 + z_84 + z_83 + z_82 + z_81 <= 1 r_18: + z_90 + z_89 + z_88 + z_87 + z_86 <= 1 r_19: + z_95 + z_94 + z_93 + z_92 + z_91 <= 1 r_20: + z_100 + z_99 + z_98 + z_97 + z_96 <= 1 r_21: + z_105 + z_104 + z_103 + z_102 + z_101 <= 1 r_22: + z_110 + z_109 + z_108 + z_107 + z_106 <= 1 r_23: + z_115 + z_114 + z_113 + z_112 + z_111 <= 1 r_24: + z_120 + z_119 + z_118 + z_117 + z_116 <= 1 r_25: + z_125 + z_124 + z_123 + z_122 + z_121 <= 1 r_26: + z_130 + z_129 + z_128 + z_127 + z_126 <= 1 r_27: + z_135 + z_134 + z_133 + z_132 + z_131 <= 1 r_28: + z_140 + z_139 + z_138 + z_137 + z_136 <= 1 r_29: + z_145 + z_144 + z_143 + z_142 + z_141 <= 1 r_30: + z_150 + z_149 + z_148 + z_147 + z_146 <= 1 r_31: + z_155 + z_154 + z_153 + z_152 + z_151 <= 1 r_32: + z_160 + z_159 + z_158 + z_157 + z_156 <= 1 r_33: + z_165 + z_164 + z_163 + z_162 + z_161 <= 1 r_34: + z_170 + z_169 + z_168 + z_167 + z_166 <= 1 r_35: + z_175 + z_174 + z_173 + z_172 + z_171 <= 1 r_36: + z_180 + z_179 + z_178 + z_177 + z_176 <= 1 r_37: + z_185 + z_184 + z_183 + z_182 + z_181 <= 1 r_38: + z_190 + z_189 + z_188 + z_187 + z_186 <= 1 r_39: + z_195 + z_194 + z_193 + z_192 + z_191 <= 1 r_40: + z_200 + z_199 + z_198 + z_197 + z_196 <= 1 r_41: + z_205 + z_204 + z_203 + z_202 + z_201 <= 1 r_42: + z_210 + z_209 + z_208 + z_207 + z_206 <= 1 r_43: + z_215 + z_214 + z_213 + z_212 + z_211 <= 1 r_44: + z_220 + z_219 + z_218 + z_217 + z_216 <= 1 r_45: + z_225 + z_224 + z_223 + z_222 + z_221 <= 1 r_46: + z_230 + z_229 + z_228 + z_227 + z_226 <= 1 r_47: + z_235 + z_234 + z_233 + z_232 + z_231 <= 1 r_48: + z_240 + z_239 + z_238 + z_237 + z_236 <= 1 r_49: + z_245 + z_244 + z_243 + z_242 + z_241 <= 1 r_50: + z_250 + z_249 + z_248 + z_247 + z_246 <= 1 r_51: + z_255 + z_254 + z_253 + z_252 + z_251 <= 1 r_52: + z_260 + z_259 + z_258 + z_257 + z_256 <= 1 r_53: + z_265 + z_264 + z_263 + z_262 + z_261 <= 1 r_54: + z_270 + z_269 + z_268 + z_267 + z_266 <= 1 r_55: + z_275 + z_274 + z_273 + z_272 + z_271 <= 1 r_56: + z_280 + z_279 + z_278 + z_277 + z_276 <= 1 r_57: + z_285 + z_284 + z_283 + z_282 + z_281 <= 1 r_58: + z_290 + z_289 + z_288 + z_287 + z_286 <= 1 r_59: + z_295 + z_294 + z_293 + z_292 + z_291 <= 1 r_60: + z_300 + z_299 + z_298 + z_297 + z_296 <= 1 r_61: + z_305 + z_304 + z_303 + z_302 + z_301 <= 1 r_62: + z_310 + z_309 + z_308 + z_307 + z_306 <= 1 r_63: + z_315 + z_314 + z_313 + z_312 + z_311 <= 1 r_64: + z_320 + z_319 + z_318 + z_317 + z_316 <= 1 r_65: + z_325 + z_324 + z_323 + z_322 + z_321 <= 1 r_66: + z_330 + z_329 + z_328 + z_327 + z_326 <= 1 r_67: + z_335 + z_334 + z_333 + z_332 + z_331 <= 1 r_68: + z_340 + z_339 + z_338 + z_337 + z_336 <= 1 r_69: + z_345 + z_344 + z_343 + z_342 + z_341 <= 1 r_70: + z_350 + z_349 + z_348 + z_347 + z_346 <= 1 r_71: + z_355 + z_354 + z_353 + z_352 + z_351 <= 1 r_72: + z_360 + z_359 + z_358 + z_357 + z_356 <= 1 r_73: + z_365 + z_364 + z_363 + z_362 + z_361 <= 1 r_74: + z_370 + z_369 + z_368 + z_367 + z_366 <= 1 r_75: + z_375 + z_374 + z_373 + z_372 + z_371 <= 1 r_76: + z_380 + z_379 + z_378 + z_377 + z_376 <= 1 r_77: + z_385 + z_384 + z_383 + z_382 + z_381 <= 1 r_78: + z_390 + z_389 + z_388 + z_387 + z_386 <= 1 r_79: + z_395 + z_394 + z_393 + z_392 + z_391 <= 1 r_80: + z_400 + z_399 + z_398 + z_397 + z_396 <= 1 r_81: + z_405 + z_404 + z_403 + z_402 + z_401 <= 1 r_82: + z_410 + z_409 + z_408 + z_407 + z_406 <= 1 r_83: + z_415 + z_414 + z_413 + z_412 + z_411 <= 1 r_84: + z_420 + z_419 + z_418 + z_417 + z_416 <= 1 r_85: + z_425 + z_424 + z_423 + z_422 + z_421 <= 1 r_86: + z_430 + z_429 + z_428 + z_427 + z_426 <= 1 r_87: + z_435 + z_434 + z_433 + z_432 + z_431 <= 1 r_88: + z_440 + z_439 + z_438 + z_437 + z_436 <= 1 r_89: + z_445 + z_444 + z_443 + z_442 + z_441 <= 1 r_90: + z_450 + z_449 + z_448 + z_447 + z_446 <= 1 r_91: + z_455 + z_454 + z_453 + z_452 + z_451 <= 1 r_92: + z_460 + z_459 + z_458 + z_457 + z_456 <= 1 r_93: + z_465 + z_464 + z_463 + z_462 + z_461 <= 1 r_94: + z_470 + z_469 + z_468 + z_467 + z_466 <= 1 r_95: + z_475 + z_474 + z_473 + z_472 + z_471 <= 1 r_96: + z_480 + z_479 + z_478 + z_477 + z_476 <= 1 r_97: + z_485 + z_484 + z_483 + z_482 + z_481 <= 1 r_98: + z_490 + z_489 + z_488 + z_487 + z_486 <= 1 r_99: + z_495 + z_494 + z_493 + z_492 + z_491 <= 1 r_100: + z_500 + z_499 + z_498 + z_497 + z_496 <= 1 r_101: + z_505 + z_504 + z_503 + z_502 + z_501 <= 1 r_102: + z_510 + z_509 + z_508 + z_507 + z_506 <= 1 r_103: + z_515 + z_514 + z_513 + z_512 + z_511 <= 1 r_104: + z_520 + z_519 + z_518 + z_517 + z_516 <= 1 r_105: + z_525 + z_524 + z_523 + z_522 + z_521 <= 1 r_106: + z_530 + z_529 + z_528 + z_527 + z_526 <= 1 r_107: + z_535 + z_534 + z_533 + z_532 + z_531 <= 1 r_108: + z_540 + z_539 + z_538 + z_537 + z_536 <= 1 r_109: + z_545 + z_544 + z_543 + z_542 + z_541 <= 1 r_110: + z_550 + z_549 + z_548 + z_547 + z_546 <= 1 r_111: + z_555 + z_554 + z_553 + z_552 + z_551 <= 1 r_112: + z_560 + z_559 + z_558 + z_557 + z_556 <= 1 r_113: + z_565 + z_564 + z_563 + z_562 + z_561 <= 1 r_114: + z_570 + z_569 + z_568 + z_567 + z_566 <= 1 r_115: + z_575 + z_574 + z_573 + z_572 + z_571 <= 1 r_116: + z_580 + z_579 + z_578 + z_577 + z_576 <= 1 r_117: + z_585 + z_584 + z_583 + z_582 + z_581 <= 1 r_118: + z_590 + z_589 + z_588 + z_587 + z_586 <= 1 r_119: + z_595 + z_594 + z_593 + z_592 + z_591 <= 1 r_120: + z_600 + z_599 + z_598 + z_597 + z_596 <= 1 r_121: + z_605 + z_604 + z_603 + z_602 + z_601 <= 1 r_122: + z_610 + z_609 + z_608 + z_607 + z_606 <= 1 r_123: + z_615 + z_614 + z_613 + z_612 + z_611 <= 1 r_124: + z_620 + z_619 + z_618 + z_617 + z_616 <= 1 r_125: + z_625 + z_624 + z_623 + z_622 + z_621 <= 1 r_126: + z_630 + z_629 + z_628 + z_627 + z_626 <= 1 r_127: + z_635 + z_634 + z_633 + z_632 + z_631 <= 1 r_128: + z_640 + z_639 + z_638 + z_637 + z_636 <= 1 r_129: + z_645 + z_644 + z_643 + z_642 + z_641 <= 1 r_130: + z_650 + z_649 + z_648 + z_647 + z_646 <= 1 r_131: + z_655 + z_654 + z_653 + z_652 + z_651 <= 1 r_132: + z_660 + z_659 + z_658 + z_657 + z_656 <= 1 r_133: + z_665 + z_664 + z_663 + z_662 + z_661 <= 1 r_134: + z_670 + z_669 + z_668 + z_667 + z_666 <= 1 r_135: + z_675 + z_674 + z_673 + z_672 + z_671 <= 1 r_136: + z_680 + z_679 + z_678 + z_677 + z_676 <= 1 r_137: + z_685 + z_684 + z_683 + z_682 + z_681 <= 1 r_138: + z_690 + z_689 + z_688 + z_687 + z_686 <= 1 r_139: + z_695 + z_694 + z_693 + z_692 + z_691 <= 1 r_140: + z_700 + z_699 + z_698 + z_697 + z_696 <= 1 r_141: + z_705 + z_704 + z_703 + z_702 + z_701 <= 1 r_142: + z_710 + z_709 + z_708 + z_707 + z_706 <= 1 r_143: + z_715 + z_714 + z_713 + z_712 + z_711 <= 1 r_144: + z_720 + z_719 + z_718 + z_717 + z_716 <= 1 r_145: + z_725 + z_724 + z_723 + z_722 + z_721 <= 1 r_146: + z_730 + z_729 + z_728 + z_727 + z_726 <= 1 r_147: + z_735 + z_734 + z_733 + z_732 + z_731 <= 1 r_148: + z_740 + z_739 + z_738 + z_737 + z_736 <= 1 r_149: + z_745 + z_744 + z_743 + z_742 + z_741 <= 1 r_150: + z_750 + z_749 + z_748 + z_747 + z_746 <= 1 r_151: + z_755 + z_754 + z_753 + z_752 + z_751 <= 1 r_152: + z_760 + z_759 + z_758 + z_757 + z_756 <= 1 r_153: + z_765 + z_764 + z_763 + z_762 + z_761 <= 1 r_154: + z_770 + z_769 + z_768 + z_767 + z_766 <= 1 r_155: + z_775 + z_774 + z_773 + z_772 + z_771 <= 1 r_156: + z_780 + z_779 + z_778 + z_777 + z_776 <= 1 r_157: + z_785 + z_784 + z_783 + z_782 + z_781 <= 1 r_158: + z_790 + z_789 + z_788 + z_787 + z_786 <= 1 r_159: + z_795 + z_794 + z_793 + z_792 + z_791 <= 1 r_160: + z_800 + z_799 + z_798 + z_797 + z_796 <= 1 r_161: + z_805 + z_804 + z_803 + z_802 + z_801 <= 1 r_162: + z_810 + z_809 + z_808 + z_807 + z_806 <= 1 r_163: + z_815 + z_814 + z_813 + z_812 + z_811 <= 1 r_164: + z_820 + z_819 + z_818 + z_817 + z_816 <= 1 r_165: + z_825 + z_824 + z_823 + z_822 + z_821 <= 1 r_166: + z_830 + z_829 + z_828 + z_827 + z_826 <= 1 r_167: + z_835 + z_834 + z_833 + z_832 + z_831 <= 1 r_168: + z_840 + z_839 + z_838 + z_837 + z_836 <= 1 r_169: + z_845 + z_844 + z_843 + z_842 + z_841 <= 1 r_170: + z_850 + z_849 + z_848 + z_847 + z_846 <= 1 r_171: + z_855 + z_854 + z_853 + z_852 + z_851 <= 1 r_172: + z_860 + z_859 + z_858 + z_857 + z_856 <= 1 r_173: + z_865 + z_864 + z_863 + z_862 + z_861 <= 1 r_174: + z_870 + z_869 + z_868 + z_867 + z_866 <= 1 r_175: + z_875 + z_874 + z_873 + z_872 + z_871 <= 1 r_176: + z_880 + z_879 + z_878 + z_877 + z_876 <= 1 r_177: + z_885 + z_884 + z_883 + z_882 + z_881 <= 1 r_178: + z_890 + z_889 + z_888 + z_887 + z_886 <= 1 r_179: + z_895 + z_894 + z_893 + z_892 + z_891 <= 1 r_180: + z_900 + z_899 + z_898 + z_897 + z_896 <= 1 r_181: + z_905 + z_904 + z_903 + z_902 + z_901 <= 1 r_182: + z_910 + z_909 + z_908 + z_907 + z_906 <= 1 r_183: + z_915 + z_914 + z_913 + z_912 + z_911 <= 1 r_184: + z_920 + z_919 + z_918 + z_917 + z_916 <= 1 r_185: + z_925 + z_924 + z_923 + z_922 + z_921 <= 1 r_186: + z_930 + z_929 + z_928 + z_927 + z_926 <= 1 r_187: + z_935 + z_934 + z_933 + z_932 + z_931 <= 1 r_188: + z_940 + z_939 + z_938 + z_937 + z_936 <= 1 r_189: + z_945 + z_944 + z_943 + z_942 + z_941 <= 1 r_190: + z_950 + z_949 + z_948 + z_947 + z_946 <= 1 r_191: + z_955 + z_954 + z_953 + z_952 + z_951 <= 1 r_192: + z_960 + z_959 + z_958 + z_957 + z_956 <= 1 r_193: + z_965 + z_964 + z_963 + z_962 + z_961 <= 1 r_194: + z_970 + z_969 + z_968 + z_967 + z_966 <= 1 r_195: + z_975 + z_974 + z_973 + z_972 + z_971 <= 1 r_196: + z_980 + z_979 + z_978 + z_977 + z_976 <= 1 r_197: + z_985 + z_984 + z_983 + z_982 + z_981 <= 1 r_198: + z_990 + z_989 + z_988 + z_987 + z_986 <= 1 r_199: + z_995 + z_994 + z_993 + z_992 + z_991 <= 1 r_200: + z_1000 + z_999 + z_998 + z_997 + z_996 <= 1 r_201: + z_1005 + z_1004 + z_1003 + z_1002 + z_1001 <= 1 r_202: + z_1010 + z_1009 + z_1008 + z_1007 + z_1006 <= 1 r_203: + z_1015 + z_1014 + z_1013 + z_1012 + z_1011 <= 1 r_204: + z_1020 + z_1019 + z_1018 + z_1017 + z_1016 <= 1 r_205: + z_1025 + z_1024 + z_1023 + z_1022 + z_1021 <= 1 r_206: + z_1030 + z_1029 + z_1028 + z_1027 + z_1026 <= 1 r_207: + z_1035 + z_1034 + z_1033 + z_1032 + z_1031 <= 1 r_208: + z_1040 + z_1039 + z_1038 + z_1037 + z_1036 <= 1 r_209: + z_1045 + z_1044 + z_1043 + z_1042 + z_1041 <= 1 r_210: + z_1050 + z_1049 + z_1048 + z_1047 + z_1046 <= 1 r_211: + z_1055 + z_1054 + z_1053 + z_1052 + z_1051 <= 1 r_212: + z_1060 + z_1059 + z_1058 + z_1057 + z_1056 <= 1 r_213: + z_1065 + z_1064 + z_1063 + z_1062 + z_1061 <= 1 r_214: + z_1070 + z_1069 + z_1068 + z_1067 + z_1066 <= 1 r_215: + z_1075 + z_1074 + z_1073 + z_1072 + z_1071 <= 1 r_216: + z_1080 + z_1079 + z_1078 + z_1077 + z_1076 <= 1 r_217: + z_1085 + z_1084 + z_1083 + z_1082 + z_1081 <= 1 r_218: + z_1090 + z_1089 + z_1088 + z_1087 + z_1086 <= 1 r_219: + z_1095 + z_1094 + z_1093 + z_1092 + z_1091 <= 1 r_220: + z_1100 + z_1099 + z_1098 + z_1097 + z_1096 <= 1 r_221: + z_1105 + z_1104 + z_1103 + z_1102 + z_1101 <= 1 r_222: + z_1110 + z_1109 + z_1108 + z_1107 + z_1106 <= 1 r_223: + z_1115 + z_1114 + z_1113 + z_1112 + z_1111 <= 1 r_224: + z_1120 + z_1119 + z_1118 + z_1117 + z_1116 <= 1 r_225: + z_1125 + z_1124 + z_1123 + z_1122 + z_1121 <= 1 r_226: + z_1130 + z_1129 + z_1128 + z_1127 + z_1126 <= 1 r_227: + z_1135 + z_1134 + z_1133 + z_1132 + z_1131 <= 1 r_228: + z_1140 + z_1139 + z_1138 + z_1137 + z_1136 <= 1 r_229: + z_1145 + z_1144 + z_1143 + z_1142 + z_1141 <= 1 r_230: + z_1150 + z_1149 + z_1148 + z_1147 + z_1146 <= 1 r_231: + z_1155 + z_1154 + z_1153 + z_1152 + z_1151 <= 1 r_232: + z_1160 + z_1159 + z_1158 + z_1157 + z_1156 <= 1 r_233: + z_1165 + z_1164 + z_1163 + z_1162 + z_1161 <= 1 r_234: + z_1170 + z_1169 + z_1168 + z_1167 + z_1166 <= 1 r_235: + z_1175 + z_1174 + z_1173 + z_1172 + z_1171 <= 1 r_236: + z_1180 + z_1179 + z_1178 + z_1177 + z_1176 <= 1 r_237: + z_1185 + z_1184 + z_1183 + z_1182 + z_1181 <= 1 r_238: + z_1190 + z_1189 + z_1188 + z_1187 + z_1186 <= 1 r_239: + z_1195 + z_1194 + z_1193 + z_1192 + z_1191 <= 1 r_240: + z_1200 + z_1199 + z_1198 + z_1197 + z_1196 <= 1 r_241: + z_1205 + z_1204 + z_1203 + z_1202 + z_1201 <= 1 r_242: + z_1210 + z_1209 + z_1208 + z_1207 + z_1206 <= 1 r_243: + z_1215 + z_1214 + z_1213 + z_1212 + z_1211 <= 1 r_244: + z_1211 + z_1206 + z_1201 + z_1196 + z_1191 + z_1186 + z_1181 + z_1176 + z_1171 + z_1166 + z_1161 + z_1156 + z_1151 + z_1146 + z_1141 + z_1136 + z_1131 + z_1126 + z_1121 + z_1116 + z_1111 + z_1106 + z_1101 + z_1096 + z_1091 + z_1086 + z_1081 + z_1076 + z_1071 + z_1066 + z_1061 + z_1056 + z_1051 + z_1046 + z_1041 + z_1036 + z_1031 + z_1026 + z_1021 + z_1016 + z_1011 + z_1006 + z_1001 + z_996 + z_991 + z_986 + z_981 + z_976 + z_971 + z_966 + z_961 + z_956 + z_951 + z_946 + z_941 + z_936 + z_931 + z_926 + z_921 + z_916 + z_911 + z_906 + z_901 + z_896 + z_891 + z_886 + z_881 + z_876 + z_871 + z_866 + z_861 + z_856 + z_851 + z_846 + z_841 + z_836 + z_831 + z_826 + z_821 + z_816 + z_811 + z_806 + z_801 + z_796 + z_791 + z_786 + z_781 + z_776 + z_771 + z_766 + z_761 + z_756 + z_751 + z_746 + z_741 + z_736 + z_731 + z_726 + z_721 + z_716 + z_711 + z_706 + z_701 + z_696 + z_691 + z_686 + z_681 + z_676 + z_671 + z_666 + z_661 + z_656 + z_651 + z_646 + z_641 + z_636 + z_631 + z_626 + z_621 + z_616 + z_611 + z_606 + z_601 + z_596 + z_591 + z_586 + z_581 + z_576 + z_571 + z_566 + z_561 + z_556 + z_551 + z_546 + z_541 + z_536 + z_531 + z_526 + z_521 + z_516 + z_511 + z_506 + z_501 + z_496 + z_491 + z_486 + z_481 + z_476 + z_471 + z_466 + z_461 + z_456 + z_451 + z_446 + z_441 + z_436 + z_431 + z_426 + z_421 + z_416 + z_411 + z_406 + z_401 + z_396 + z_391 + z_386 + z_381 + z_376 + z_371 + z_366 + z_361 + z_356 + z_351 + z_346 + z_341 + z_336 + z_331 + z_326 + z_321 + z_316 + z_311 + z_306 + z_301 + z_296 + z_291 + z_286 + z_281 + z_276 + z_271 + z_266 + z_261 + z_256 + z_251 + z_246 + z_241 + z_236 + z_231 + z_226 + z_221 + z_216 + z_211 + z_206 + z_201 + z_196 + z_191 + z_186 + z_181 + z_176 + z_171 + z_166 + z_161 + z_156 + z_151 + z_146 + z_141 + z_136 + z_131 + z_126 + z_121 + z_116 + z_111 + z_106 + z_101 + z_96 + z_91 + z_86 + z_81 + z_76 + z_71 + z_66 + z_61 + z_56 + z_51 + z_46 + z_41 + z_36 + z_31 + z_26 + z_21 + z_16 + z_11 + z_6 + z_1 = 27 r_245: + z_621 + z_581 + z_491 + z_1116 + z_1051 + z_231 + z_916 + z_876 + z_676 = 0 r_246: + z_1056 + z_1026 + z_336 + z_201 + z_881 + z_836 = 1 r_247: + z_1156 + z_1121 + z_436 + z_341 + z_961 + z_241 + z_726 + z_36 + z_681 = 1 r_248: + z_441 + z_381 + z_1001 + z_966 + z_886 + z_86 + z_1 = 1 r_249: + z_626 + z_531 + z_1166 + z_496 + z_446 + z_386 + z_1036 + z_351 + z_1011 + z_301 + z_211 + z_841 + z_136 + z_96 + z_736 + z_46 + z_6 = 1 r_250: + z_506 + z_1131 + z_1071 + z_306 + z_251 + z_141 + z_696 = 1 r_251: + z_1176 + z_456 + z_1081 + z_366 + z_316 + z_216 + z_891 + z_846 + z_11 = 1 r_252: + z_636 + z_1186 + z_1136 + z_461 + z_1086 + z_396 + z_266 + z_936 + z_146 + z_791 + z_101 + z_56 = 1 r_253: + z_466 + z_1091 + z_406 + z_976 + z_896 + z_801 + z_111 + z_751 = 1 r_254: + z_646 + z_1196 + z_1141 + z_1101 + z_271 + z_221 + z_901 + z_181 + z_151 + z_806 + z_756 = 1 r_255: + z_571 + z_1201 + z_416 + z_911 + z_126 + z_66 = 1 r_256: + z_606 + z_551 + z_1206 + z_476 + z_991 + z_281 + z_816 + z_131 + z_71 + z_711 = 1 r_257: + z_661 + z_611 + z_996 + z_226 + z_196 + z_156 + z_826 = 1 r_258: + z_666 + z_616 + z_1146 + z_481 + z_866 + z_721 + z_21 = 1 r_259: + z_671 + z_1151 + z_486 + z_1106 + z_1016 + z_286 + z_161 + z_831 = 1 r_260: + z_1211 + z_521 + z_1111 + z_421 + z_1021 + z_951 + z_871 + z_771 + z_26 = 1 r_261: + z_586 + z_526 + z_426 + z_291 + z_921 + z_76 + z_31 = 1 r_262: + z_431 + z_1061 + z_956 + z_236 + z_776 + z_81 = 1 r_263: + z_556 + z_376 + z_346 + z_296 + z_41 = 1 r_264: + z_1161 + z_1031 + z_1006 + z_246 + z_206 + z_166 + z_91 + z_731 + z_686 = 1 r_265: + z_631 + z_591 + z_501 + z_1126 + z_1066 + z_1041 + z_356 + z_926 + z_781 + z_691 = 1 r_266: + z_561 + z_1171 + z_451 + z_1076 + z_391 + z_361 + z_311 + z_971 + z_256 + z_741 + z_701 = 1 r_267: + z_536 + z_1181 + z_1046 + z_261 + z_931 + z_851 + z_786 + z_746 + z_51 = 1 r_268: + z_641 + z_401 + z_371 + z_171 + z_796 + z_106 = 1 r_269: + z_596 + z_566 + z_541 + z_1191 + z_471 + z_1096 + z_981 + z_176 + z_116 + z_706 + z_16 = 1 r_270: + z_651 + z_511 + z_411 + z_321 + z_986 + z_906 + z_186 + z_856 + z_811 + z_121 + z_761 + z_61 = 1 r_271: + z_656 + z_601 + z_546 + z_326 + z_276 + z_941 + z_861 = 1 r_272: + z_576 + z_516 + z_331 + z_946 + z_191 + z_821 + z_766 + z_716 = 1 r_273: - z_26 - z_21 - z_16 - z_11 - z_6 - z_1 - z_621 - z_581 - z_491 - z_1116 - z_1051 - z_231 - z_916 - z_876 - z_676 <= -1 r_274: - z_71 - z_66 - z_61 - z_56 - z_51 - z_46 - z_41 - z_36 - z_31 - z_1056 - z_1026 - z_336 - z_201 - z_881 - z_836 <= -1 r_275: - z_131 - z_126 - z_121 - z_116 - z_111 - z_106 - z_101 - z_96 - z_91 - z_86 - z_81 - z_76 - z_1156 - z_1121 - z_436 - z_341 - z_961 - z_241 - z_726 - z_36 - z_681 <= -1 r_276: - z_161 - z_156 - z_151 - z_146 - z_141 - z_136 - z_441 - z_381 - z_1001 - z_966 - z_886 - z_86 - z_1 <= -1 r_277: - z_196 - z_191 - z_186 - z_181 - z_176 - z_171 - z_166 - z_626 - z_531 - z_1166 - z_496 - z_446 - z_386 - z_1036 - z_351 - z_1011 - z_301 - z_211 - z_841 - z_136 - z_96 - z_736 - z_46 - z_6 <= -1 r_278: - z_226 - z_221 - z_216 - z_211 - z_206 - z_201 - z_506 - z_1131 - z_1071 - z_306 - z_251 - z_141 - z_696 <= -1 r_279: - z_286 - z_281 - z_276 - z_271 - z_266 - z_261 - z_256 - z_251 - z_246 - z_241 - z_236 - z_231 - z_1176 - z_456 - z_1081 - z_366 - z_316 - z_216 - z_891 - z_846 - z_11 <= -1 r_280: - z_331 - z_326 - z_321 - z_316 - z_311 - z_306 - z_301 - z_296 - z_291 - z_636 - z_1186 - z_1136 - z_461 - z_1086 - z_396 - z_266 - z_936 - z_146 - z_791 - z_101 - z_56 <= -1 r_281: - z_371 - z_366 - z_361 - z_356 - z_351 - z_346 - z_341 - z_336 - z_466 - z_1091 - z_406 - z_976 - z_896 - z_801 - z_111 - z_751 <= -1 r_282: - z_421 - z_416 - z_411 - z_406 - z_401 - z_396 - z_391 - z_386 - z_381 - z_376 - z_646 - z_1196 - z_1141 - z_1101 - z_271 - z_221 - z_901 - z_181 - z_151 - z_806 - z_756 <= -1 r_283: - z_486 - z_481 - z_476 - z_471 - z_466 - z_461 - z_456 - z_451 - z_446 - z_441 - z_436 - z_431 - z_426 - z_571 - z_1201 - z_416 - z_911 - z_126 - z_66 <= -1 r_284: - z_521 - z_516 - z_511 - z_506 - z_501 - z_496 - z_491 - z_606 - z_551 - z_1206 - z_476 - z_991 - z_281 - z_816 - z_131 - z_71 - z_711 <= -1 r_285: - z_551 - z_546 - z_541 - z_536 - z_531 - z_526 - z_661 - z_611 - z_996 - z_226 - z_196 - z_156 - z_826 <= -1 r_286: - z_576 - z_571 - z_566 - z_561 - z_556 - z_666 - z_616 - z_1146 - z_481 - z_866 - z_721 - z_21 <= -1 r_287: - z_616 - z_611 - z_606 - z_601 - z_596 - z_591 - z_586 - z_581 - z_671 - z_1151 - z_486 - z_1106 - z_1016 - z_286 - z_161 - z_831 <= -1 r_288: - z_671 - z_666 - z_661 - z_656 - z_651 - z_646 - z_641 - z_636 - z_631 - z_626 - z_621 - z_1211 - z_521 - z_1111 - z_421 - z_1021 - z_951 - z_871 - z_771 - z_26 <= -1 r_289: - z_721 - z_716 - z_711 - z_706 - z_701 - z_696 - z_691 - z_686 - z_681 - z_676 - z_586 - z_526 - z_426 - z_291 - z_921 - z_76 - z_31 <= -1 r_290: - z_771 - z_766 - z_761 - z_756 - z_751 - z_746 - z_741 - z_736 - z_731 - z_726 - z_431 - z_1061 - z_956 - z_236 - z_776 - z_81 <= -1 r_291: - z_831 - z_826 - z_821 - z_816 - z_811 - z_806 - z_801 - z_796 - z_791 - z_786 - z_781 - z_776 - z_556 - z_376 - z_346 - z_296 - z_41 <= -1 r_292: - z_871 - z_866 - z_861 - z_856 - z_851 - z_846 - z_841 - z_836 - z_1161 - z_1031 - z_1006 - z_246 - z_206 - z_166 - z_91 - z_731 - z_686 <= -1 r_293: - z_911 - z_906 - z_901 - z_896 - z_891 - z_886 - z_881 - z_876 - z_631 - z_591 - z_501 - z_1126 - z_1066 - z_1041 - z_356 - z_926 - z_781 - z_691 <= -1 r_294: - z_951 - z_946 - z_941 - z_936 - z_931 - z_926 - z_921 - z_916 - z_561 - z_1171 - z_451 - z_1076 - z_391 - z_361 - z_311 - z_971 - z_256 - z_741 - z_701 <= -1 r_295: - z_996 - z_991 - z_986 - z_981 - z_976 - z_971 - z_966 - z_961 - z_956 - z_536 - z_1181 - z_1046 - z_261 - z_931 - z_851 - z_786 - z_746 - z_51 <= -1 r_296: - z_1021 - z_1016 - z_1011 - z_1006 - z_1001 - z_641 - z_401 - z_371 - z_171 - z_796 - z_106 <= -1 r_297: - z_1046 - z_1041 - z_1036 - z_1031 - z_1026 - z_596 - z_566 - z_541 - z_1191 - z_471 - z_1096 - z_981 - z_176 - z_116 - z_706 - z_16 <= -1 r_298: - z_1111 - z_1106 - z_1101 - z_1096 - z_1091 - z_1086 - z_1081 - z_1076 - z_1071 - z_1066 - z_1061 - z_1056 - z_1051 - z_651 - z_511 - z_411 - z_321 - z_986 - z_906 - z_186 - z_856 - z_811 - z_121 - z_761 - z_61 <= -1 r_299: - z_1151 - z_1146 - z_1141 - z_1136 - z_1131 - z_1126 - z_1121 - z_1116 - z_656 - z_601 - z_546 - z_326 - z_276 - z_941 - z_861 <= -1 r_300: - z_1211 - z_1206 - z_1201 - z_1196 - z_1191 - z_1186 - z_1181 - z_1176 - z_1171 - z_1166 - z_1161 - z_1156 - z_576 - z_516 - z_331 - z_946 - z_191 - z_821 - z_766 - z_716 <= -1 r_301: - x_1217 + 28 z_1 + x_1216 <= 27 r_302: - x_1218 + 28 z_6 + x_1216 <= 27 r_303: - x_1219 + 25 z_231 + 27 z_11 + x_1216 <= 26 r_304: - x_1220 + 28 z_16 + x_1216 <= 27 r_305: - x_1221 + 28 z_21 + x_1216 <= 27 r_306: - x_1222 + 25 z_621 + 27 z_26 + x_1216 <= 26 r_307: - x_1224 + 28 z_31 + x_1223 <= 27 r_308: - x_1225 + 28 z_36 + x_1223 <= 27 r_309: - x_1226 + 28 z_41 + x_1223 <= 27 r_310: - x_1218 + 28 z_46 + x_1223 <= 27 r_311: - x_1227 + 28 z_51 + x_1223 <= 27 r_312: - x_1228 + 28 z_56 + x_1223 <= 27 r_313: - x_1229 + 25 z_1056 + 27 z_61 + x_1223 <= 26 r_314: - x_1230 + 28 z_66 + x_1223 <= 27 r_315: - x_1231 + 28 z_71 + x_1223 <= 27 r_316: - x_1224 + 25 z_681 + 27 z_76 + x_1225 <= 26 r_317: - x_1232 + 25 z_726 + 27 z_81 + x_1225 <= 26 r_318: - x_1217 + 28 z_86 + x_1225 <= 27 r_319: - x_1233 + 28 z_91 + x_1225 <= 27 r_320: - x_1218 + 28 z_96 + x_1225 <= 27 r_321: - x_1228 + 28 z_101 + x_1225 <= 27 r_322: - x_1234 + 28 z_106 + x_1225 <= 27 r_323: - x_1235 + 25 z_341 + 27 z_111 + x_1225 <= 26 r_324: - x_1220 + 28 z_116 + x_1225 <= 27 r_325: - x_1229 + 28 z_121 + x_1225 <= 27 r_326: - x_1230 + 25 z_436 + 27 z_126 + x_1225 <= 26 r_327: - x_1231 + 28 z_131 + x_1225 <= 27 r_328: - x_1218 + 28 z_136 + x_1217 <= 27 r_329: - x_1236 + 28 z_141 + x_1217 <= 27 r_330: - x_1228 + 28 z_146 + x_1217 <= 27 r_331: - x_1237 + 25 z_381 + 27 z_151 + x_1217 <= 26 r_332: - x_1238 + 28 z_156 + x_1217 <= 27 r_333: - x_1239 + 28 z_161 + x_1217 <= 27 r_334: - x_1233 + 25 z_841 + 27 z_166 + x_1218 <= 26 r_335: - x_1234 + 25 z_1011 + 27 z_171 + x_1218 <= 26 r_336: - x_1220 + 25 z_1036 + 27 z_176 + x_1218 <= 26 r_337: - x_1237 + 25 z_386 + 27 z_181 + x_1218 <= 26 r_338: - x_1229 + 28 z_186 + x_1218 <= 27 r_339: - x_1240 + 25 z_1166 + 27 z_191 + x_1218 <= 26 r_340: - x_1238 + 25 z_531 + 27 z_196 + x_1218 <= 26 r_341: - x_1223 + 28 z_201 + x_1236 <= 27 r_342: - x_1233 + 28 z_206 + x_1236 <= 27 r_343: - x_1218 + 28 z_211 + x_1236 <= 27 r_344: - x_1219 + 25 z_251 + 27 z_216 + x_1236 <= 26 r_345: - x_1237 + 28 z_221 + x_1236 <= 27 r_346: - x_1238 + 28 z_226 + x_1236 <= 27 r_347: - x_1216 + 25 z_11 + 27 z_231 + x_1219 <= 26 r_348: - x_1232 + 28 z_236 + x_1219 <= 27 r_349: - x_1225 + 28 z_241 + x_1219 <= 27 r_350: - x_1233 + 25 z_846 + 27 z_246 + x_1219 <= 26 r_351: - x_1236 + 25 z_216 + 27 z_251 + x_1219 <= 26 r_352: - x_1241 + 28 z_256 + x_1219 <= 27 r_353: - x_1227 + 28 z_261 + x_1219 <= 27 r_354: - x_1228 + 25 z_316 + 27 z_266 + x_1219 <= 26 r_355: - x_1237 + 28 z_271 + x_1219 <= 27 r_356: - x_1242 + 28 z_276 + x_1219 <= 27 r_357: - x_1231 + 28 z_281 + x_1219 <= 27 r_358: - x_1239 + 28 z_286 + x_1219 <= 27 r_359: - x_1224 + 28 z_291 + x_1228 <= 27 r_360: - x_1226 + 25 z_791 + 27 z_296 + x_1228 <= 26 r_361: - x_1218 + 28 z_301 + x_1228 <= 27 r_362: - x_1236 + 28 z_306 + x_1228 <= 27 r_363: - x_1241 + 25 z_936 + 27 z_311 + x_1228 <= 26 r_364: - x_1219 + 25 z_266 + 27 z_316 + x_1228 <= 26 r_365: - x_1229 + 25 z_1086 + 27 z_321 + x_1228 <= 26 r_366: - x_1242 + 25 z_1136 + 27 z_326 + x_1228 <= 26 r_367: - x_1240 + 25 z_1186 + 27 z_331 + x_1228 <= 26 r_368: - x_1223 + 28 z_336 + x_1235 <= 27 r_369: - x_1225 + 25 z_111 + 27 z_341 + x_1235 <= 26 r_370: - x_1226 + 25 z_801 + 27 z_346 + x_1235 <= 26 r_371: - x_1218 + 28 z_351 + x_1235 <= 27 r_372: - x_1243 + 25 z_896 + 27 z_356 + x_1235 <= 26 r_373: - x_1241 + 28 z_361 + x_1235 <= 27 r_374: - x_1219 + 28 z_366 + x_1235 <= 27 r_375: - x_1234 + 28 z_371 + x_1235 <= 27 r_376: - x_1226 + 25 z_806 + 27 z_376 + x_1237 <= 26 r_377: - x_1217 + 25 z_151 + 27 z_381 + x_1237 <= 26 r_378: - x_1218 + 25 z_181 + 27 z_386 + x_1237 <= 26 r_379: - x_1241 + 28 z_391 + x_1237 <= 27 r_380: - x_1228 + 28 z_396 + x_1237 <= 27 r_381: - x_1234 + 28 z_401 + x_1237 <= 27 r_382: - x_1235 + 28 z_406 + x_1237 <= 27 r_383: - x_1229 + 25 z_1101 + 27 z_411 + x_1237 <= 26 r_384: - x_1230 + 28 z_416 + x_1237 <= 27 r_385: - x_1222 + 25 z_646 + 27 z_421 + x_1237 <= 26 r_386: - x_1224 + 28 z_426 + x_1230 <= 27 r_387: - x_1232 + 28 z_431 + x_1230 <= 27 r_388: - x_1225 + 25 z_126 + 27 z_436 + x_1230 <= 26 r_389: - x_1217 + 28 z_441 + x_1230 <= 27 r_390: - x_1218 + 28 z_446 + x_1230 <= 27 r_391: - x_1241 + 28 z_451 + x_1230 <= 27 r_392: - x_1219 + 28 z_456 + x_1230 <= 27 r_393: - x_1228 + 28 z_461 + x_1230 <= 27 r_394: - x_1235 + 28 z_466 + x_1230 <= 27 r_395: - x_1220 + 28 z_471 + x_1230 <= 27 r_396: - x_1231 + 28 z_476 + x_1230 <= 27 r_397: - x_1221 + 25 z_571 + 27 z_481 + x_1230 <= 26 r_398: - x_1239 + 28 z_486 + x_1230 <= 27 r_399: - x_1216 + 28 z_491 + x_1231 <= 27 r_400: - x_1218 + 28 z_496 + x_1231 <= 27 r_401: - x_1243 + 28 z_501 + x_1231 <= 27 r_402: - x_1236 + 28 z_506 + x_1231 <= 27 r_403: - x_1229 + 28 z_511 + x_1231 <= 27 r_404: - x_1240 + 25 z_1206 + 27 z_516 + x_1231 <= 26 r_405: - x_1222 + 28 z_521 + x_1231 <= 27 r_406: - x_1224 + 28 z_526 + x_1238 <= 27 r_407: - x_1218 + 25 z_196 + 27 z_531 + x_1238 <= 26 r_408: - x_1227 + 25 z_996 + 27 z_536 + x_1238 <= 26 r_409: - x_1220 + 28 z_541 + x_1238 <= 27 r_410: - x_1242 + 28 z_546 + x_1238 <= 27 r_411: - x_1231 + 28 z_551 + x_1238 <= 27 r_412: - x_1226 + 28 z_556 + x_1221 <= 27 r_413: - x_1241 + 28 z_561 + x_1221 <= 27 r_414: - x_1220 + 28 z_566 + x_1221 <= 27 r_415: - x_1230 + 25 z_481 + 27 z_571 + x_1221 <= 26 r_416: - x_1240 + 28 z_576 + x_1221 <= 27 r_417: - x_1216 + 28 z_581 + x_1239 <= 27 r_418: - x_1224 + 28 z_586 + x_1239 <= 27 r_419: - x_1243 + 28 z_591 + x_1239 <= 27 r_420: - x_1220 + 28 z_596 + x_1239 <= 27 r_421: - x_1242 + 25 z_1151 + 27 z_601 + x_1239 <= 26 r_422: - x_1231 + 28 z_606 + x_1239 <= 27 r_423: - x_1238 + 28 z_611 + x_1239 <= 27 r_424: - x_1221 + 28 z_616 + x_1239 <= 27 r_425: - x_1216 + 25 z_26 + 27 z_621 + x_1222 <= 26 r_426: - x_1218 + 28 z_626 + x_1222 <= 27 r_427: - x_1243 + 28 z_631 + x_1222 <= 27 r_428: - x_1228 + 28 z_636 + x_1222 <= 27 r_429: - x_1234 + 25 z_1021 + 27 z_641 + x_1222 <= 26 r_430: - x_1237 + 25 z_421 + 27 z_646 + x_1222 <= 26 r_431: - x_1229 + 25 z_1111 + 27 z_651 + x_1222 <= 26 r_432: - x_1242 + 28 z_656 + x_1222 <= 27 r_433: - x_1238 + 28 z_661 + x_1222 <= 27 r_434: - x_1221 + 28 z_666 + x_1222 <= 27 r_435: - x_1239 + 28 z_671 + x_1222 <= 27 r_436: - x_1216 + 28 z_676 + x_1224 <= 27 r_437: - x_1225 + 25 z_76 + 27 z_681 + x_1224 <= 26 r_438: - x_1233 + 28 z_686 + x_1224 <= 27 r_439: - x_1243 + 28 z_691 + x_1224 <= 27 r_440: - x_1236 + 28 z_696 + x_1224 <= 27 r_441: - x_1241 + 25 z_921 + 27 z_701 + x_1224 <= 26 r_442: - x_1220 + 28 z_706 + x_1224 <= 27 r_443: - x_1231 + 28 z_711 + x_1224 <= 27 r_444: - x_1240 + 28 z_716 + x_1224 <= 27 r_445: - x_1221 + 28 z_721 + x_1224 <= 27 r_446: - x_1225 + 25 z_81 + 27 z_726 + x_1232 <= 26 r_447: - x_1233 + 28 z_731 + x_1232 <= 27 r_448: - x_1218 + 28 z_736 + x_1232 <= 27 r_449: - x_1241 + 28 z_741 + x_1232 <= 27 r_450: - x_1227 + 25 z_956 + 27 z_746 + x_1232 <= 26 r_451: - x_1235 + 28 z_751 + x_1232 <= 27 r_452: - x_1237 + 28 z_756 + x_1232 <= 27 r_453: - x_1229 + 25 z_1061 + 27 z_761 + x_1232 <= 26 r_454: - x_1240 + 28 z_766 + x_1232 <= 27 r_455: - x_1222 + 28 z_771 + x_1232 <= 27 r_456: - x_1232 + 28 z_776 + x_1226 <= 27 r_457: - x_1243 + 28 z_781 + x_1226 <= 27 r_458: - x_1227 + 28 z_786 + x_1226 <= 27 r_459: - x_1228 + 25 z_296 + 27 z_791 + x_1226 <= 26 r_460: - x_1234 + 28 z_796 + x_1226 <= 27 r_461: - x_1235 + 25 z_346 + 27 z_801 + x_1226 <= 26 r_462: - x_1237 + 25 z_376 + 27 z_806 + x_1226 <= 26 r_463: - x_1229 + 28 z_811 + x_1226 <= 27 r_464: - x_1231 + 28 z_816 + x_1226 <= 27 r_465: - x_1240 + 28 z_821 + x_1226 <= 27 r_466: - x_1238 + 28 z_826 + x_1226 <= 27 r_467: - x_1239 + 28 z_831 + x_1226 <= 27 r_468: - x_1223 + 28 z_836 + x_1233 <= 27 r_469: - x_1218 + 25 z_166 + 27 z_841 + x_1233 <= 26 r_470: - x_1219 + 25 z_246 + 27 z_846 + x_1233 <= 26 r_471: - x_1227 + 28 z_851 + x_1233 <= 27 r_472: - x_1229 + 28 z_856 + x_1233 <= 27 r_473: - x_1242 + 28 z_861 + x_1233 <= 27 r_474: - x_1221 + 28 z_866 + x_1233 <= 27 r_475: - x_1222 + 28 z_871 + x_1233 <= 27 r_476: - x_1216 + 28 z_876 + x_1243 <= 27 r_477: - x_1223 + 28 z_881 + x_1243 <= 27 r_478: - x_1217 + 28 z_886 + x_1243 <= 27 r_479: - x_1219 + 28 z_891 + x_1243 <= 27 r_480: - x_1235 + 25 z_356 + 27 z_896 + x_1243 <= 26 r_481: - x_1237 + 28 z_901 + x_1243 <= 27 r_482: - x_1229 + 25 z_1066 + 27 z_906 + x_1243 <= 26 r_483: - x_1230 + 28 z_911 + x_1243 <= 27 r_484: - x_1216 + 28 z_916 + x_1241 <= 27 r_485: - x_1224 + 25 z_701 + 27 z_921 + x_1241 <= 26 r_486: - x_1243 + 28 z_926 + x_1241 <= 27 r_487: - x_1227 + 25 z_971 + 27 z_931 + x_1241 <= 26 r_488: - x_1228 + 25 z_311 + 27 z_936 + x_1241 <= 26 r_489: - x_1242 + 28 z_941 + x_1241 <= 27 r_490: - x_1240 + 25 z_1171 + 27 z_946 + x_1241 <= 26 r_491: - x_1222 + 28 z_951 + x_1241 <= 27 r_492: - x_1232 + 25 z_746 + 27 z_956 + x_1227 <= 26 r_493: - x_1225 + 28 z_961 + x_1227 <= 27 r_494: - x_1217 + 28 z_966 + x_1227 <= 27 r_495: - x_1241 + 25 z_931 + 27 z_971 + x_1227 <= 26 r_496: - x_1235 + 28 z_976 + x_1227 <= 27 r_497: - x_1220 + 25 z_1046 + 27 z_981 + x_1227 <= 26 r_498: - x_1229 + 28 z_986 + x_1227 <= 27 r_499: - x_1231 + 28 z_991 + x_1227 <= 27 r_500: - x_1238 + 25 z_536 + 27 z_996 + x_1227 <= 26 r_501: - x_1217 + 28 z_1001 + x_1234 <= 27 r_502: - x_1233 + 28 z_1006 + x_1234 <= 27 r_503: - x_1218 + 25 z_171 + 27 z_1011 + x_1234 <= 26 r_504: - x_1239 + 28 z_1016 + x_1234 <= 27 r_505: - x_1222 + 25 z_641 + 27 z_1021 + x_1234 <= 26 r_506: - x_1223 + 28 z_1026 + x_1220 <= 27 r_507: - x_1233 + 28 z_1031 + x_1220 <= 27 r_508: - x_1218 + 25 z_176 + 27 z_1036 + x_1220 <= 26 r_509: - x_1243 + 28 z_1041 + x_1220 <= 27 r_510: - x_1227 + 25 z_981 + 27 z_1046 + x_1220 <= 26 r_511: - x_1216 + 28 z_1051 + x_1229 <= 27 r_512: - x_1223 + 25 z_61 + 27 z_1056 + x_1229 <= 26 r_513: - x_1232 + 25 z_761 + 27 z_1061 + x_1229 <= 26 r_514: - x_1243 + 25 z_906 + 27 z_1066 + x_1229 <= 26 r_515: - x_1236 + 28 z_1071 + x_1229 <= 27 r_516: - x_1241 + 28 z_1076 + x_1229 <= 27 r_517: - x_1219 + 28 z_1081 + x_1229 <= 27 r_518: - x_1228 + 25 z_321 + 27 z_1086 + x_1229 <= 26 r_519: - x_1235 + 28 z_1091 + x_1229 <= 27 r_520: - x_1220 + 28 z_1096 + x_1229 <= 27 r_521: - x_1237 + 25 z_411 + 27 z_1101 + x_1229 <= 26 r_522: - x_1239 + 28 z_1106 + x_1229 <= 27 r_523: - x_1222 + 25 z_651 + 27 z_1111 + x_1229 <= 26 r_524: - x_1216 + 28 z_1116 + x_1242 <= 27 r_525: - x_1225 + 28 z_1121 + x_1242 <= 27 r_526: - x_1243 + 28 z_1126 + x_1242 <= 27 r_527: - x_1236 + 28 z_1131 + x_1242 <= 27 r_528: - x_1228 + 25 z_326 + 27 z_1136 + x_1242 <= 26 r_529: - x_1237 + 28 z_1141 + x_1242 <= 27 r_530: - x_1221 + 28 z_1146 + x_1242 <= 27 r_531: - x_1239 + 25 z_601 + 27 z_1151 + x_1242 <= 26 r_532: - x_1225 + 28 z_1156 + x_1240 <= 27 r_533: - x_1233 + 28 z_1161 + x_1240 <= 27 r_534: - x_1218 + 25 z_191 + 27 z_1166 + x_1240 <= 26 r_535: - x_1241 + 25 z_946 + 27 z_1171 + x_1240 <= 26 r_536: - x_1219 + 28 z_1176 + x_1240 <= 27 r_537: - x_1227 + 28 z_1181 + x_1240 <= 27 r_538: - x_1228 + 25 z_331 + 27 z_1186 + x_1240 <= 26 r_539: - x_1220 + 28 z_1191 + x_1240 <= 27 r_540: - x_1237 + 28 z_1196 + x_1240 <= 27 r_541: - x_1230 + 28 z_1201 + x_1240 <= 27 r_542: - x_1231 + 25 z_516 + 27 z_1206 + x_1240 <= 26 r_543: - x_1222 + 28 z_1211 + x_1240 <= 27 r_544: 0 z_1 <= 0 r_545: - x_1223 + x_1216 <= -2 r_546: - x_1225 + x_1216 <= -2 r_547: - x_1217 + x_1216 <= -1 r_548: - x_1218 + x_1216 <= -1 r_549: - x_1236 + x_1216 <= -2 r_550: - x_1219 + x_1216 <= -1 r_551: - x_1228 + x_1216 <= -2 r_552: - x_1235 + x_1216 <= -3 r_553: - x_1237 + x_1216 <= -2 r_554: - x_1230 + x_1216 <= -2 r_555: - x_1231 + x_1216 <= -2 r_556: - x_1238 + x_1216 <= -2 r_557: - x_1221 + x_1216 <= -1 r_558: - x_1239 + x_1216 <= -2 r_559: - x_1222 + x_1216 <= -1 r_560: - x_1224 + x_1216 <= -3 r_561: - x_1232 + x_1216 <= -2 r_562: - x_1226 + x_1216 <= -2 r_563: - x_1233 + x_1216 <= -2 r_564: - x_1243 + x_1216 <= -2 r_565: - x_1241 + x_1216 <= -2 r_566: - x_1227 + x_1216 <= -2 r_567: - x_1234 + x_1216 <= -2 r_568: - x_1220 + x_1216 <= -1 r_569: - x_1229 + x_1216 <= -2 r_570: - x_1242 + x_1216 <= -2 r_571: - x_1240 + x_1216 <= -2 r_572: + z_1212 + z_1207 + z_1202 + z_1197 + z_1192 + z_1187 + z_1182 + z_1177 + z_1172 + z_1167 + z_1162 + z_1157 + z_1152 + z_1147 + z_1142 + z_1137 + z_1132 + z_1127 + z_1122 + z_1117 + z_1112 + z_1107 + z_1102 + z_1097 + z_1092 + z_1087 + z_1082 + z_1077 + z_1072 + z_1067 + z_1062 + z_1057 + z_1052 + z_1047 + z_1042 + z_1037 + z_1032 + z_1027 + z_1022 + z_1017 + z_1012 + z_1007 + z_1002 + z_997 + z_992 + z_987 + z_982 + z_977 + z_972 + z_967 + z_962 + z_957 + z_952 + z_947 + z_942 + z_937 + z_932 + z_927 + z_922 + z_917 + z_912 + z_907 + z_902 + z_897 + z_892 + z_887 + z_882 + z_877 + z_872 + z_867 + z_862 + z_857 + z_852 + z_847 + z_842 + z_837 + z_832 + z_827 + z_822 + z_817 + z_812 + z_807 + z_802 + z_797 + z_792 + z_787 + z_782 + z_777 + z_772 + z_767 + z_762 + z_757 + z_752 + z_747 + z_742 + z_737 + z_732 + z_727 + z_722 + z_717 + z_712 + z_707 + z_702 + z_697 + z_692 + z_687 + z_682 + z_677 + z_672 + z_667 + z_662 + z_657 + z_652 + z_647 + z_642 + z_637 + z_632 + z_627 + z_622 + z_617 + z_612 + z_607 + z_602 + z_597 + z_592 + z_587 + z_582 + z_577 + z_572 + z_567 + z_562 + z_557 + z_552 + z_547 + z_542 + z_537 + z_532 + z_527 + z_522 + z_517 + z_512 + z_507 + z_502 + z_497 + z_492 + z_487 + z_482 + z_477 + z_472 + z_467 + z_462 + z_457 + z_452 + z_447 + z_442 + z_437 + z_432 + z_427 + z_422 + z_417 + z_412 + z_407 + z_402 + z_397 + z_392 + z_387 + z_382 + z_377 + z_372 + z_367 + z_362 + z_357 + z_352 + z_347 + z_342 + z_337 + z_332 + z_327 + z_322 + z_317 + z_312 + z_307 + z_302 + z_297 + z_292 + z_287 + z_282 + z_277 + z_272 + z_267 + z_262 + z_257 + z_252 + z_247 + z_242 + z_237 + z_232 + z_227 + z_222 + z_217 + z_212 + z_207 + z_202 + z_197 + z_192 + z_187 + z_182 + z_177 + z_172 + z_167 + z_162 + z_157 + z_152 + z_147 + z_142 + z_137 + z_132 + z_127 + z_122 + z_117 + z_112 + z_107 + z_102 + z_97 + z_92 + z_87 + z_82 + z_77 + z_72 + z_67 + z_62 + z_57 + z_52 + z_47 + z_42 + z_37 + z_32 + z_27 + z_22 + z_17 + z_12 + z_7 + z_2 = 27 r_573: + z_622 + z_582 + z_492 + z_1117 + z_1052 + z_232 + z_917 + z_877 + z_677 = 0 r_574: + z_1057 + z_1027 + z_337 + z_202 + z_882 + z_837 = 1 r_575: + z_1157 + z_1122 + z_437 + z_342 + z_962 + z_242 + z_727 + z_37 + z_682 = 1 r_576: + z_442 + z_382 + z_1002 + z_967 + z_887 + z_87 + z_2 = 1 r_577: + z_627 + z_532 + z_1167 + z_497 + z_447 + z_387 + z_1037 + z_352 + z_1012 + z_302 + z_212 + z_842 + z_137 + z_97 + z_737 + z_47 + z_7 = 1 r_578: + z_507 + z_1132 + z_1072 + z_307 + z_252 + z_142 + z_697 = 1 r_579: + z_1177 + z_457 + z_1082 + z_367 + z_317 + z_217 + z_892 + z_847 + z_12 = 1 r_580: + z_637 + z_1187 + z_1137 + z_462 + z_1087 + z_397 + z_267 + z_937 + z_147 + z_792 + z_102 + z_57 = 1 r_581: + z_467 + z_1092 + z_407 + z_977 + z_897 + z_802 + z_112 + z_752 = 1 r_582: + z_647 + z_1197 + z_1142 + z_1102 + z_272 + z_222 + z_902 + z_182 + z_152 + z_807 + z_757 = 1 r_583: + z_572 + z_1202 + z_417 + z_912 + z_127 + z_67 = 1 r_584: + z_607 + z_552 + z_1207 + z_477 + z_992 + z_282 + z_817 + z_132 + z_72 + z_712 = 1 r_585: + z_662 + z_612 + z_997 + z_227 + z_197 + z_157 + z_827 = 1 r_586: + z_667 + z_617 + z_1147 + z_482 + z_867 + z_722 + z_22 = 1 r_587: + z_672 + z_1152 + z_487 + z_1107 + z_1017 + z_287 + z_162 + z_832 = 1 r_588: + z_1212 + z_522 + z_1112 + z_422 + z_1022 + z_952 + z_872 + z_772 + z_27 = 1 r_589: + z_587 + z_527 + z_427 + z_292 + z_922 + z_77 + z_32 = 1 r_590: + z_432 + z_1062 + z_957 + z_237 + z_777 + z_82 = 1 r_591: + z_557 + z_377 + z_347 + z_297 + z_42 = 1 r_592: + z_1162 + z_1032 + z_1007 + z_247 + z_207 + z_167 + z_92 + z_732 + z_687 = 1 r_593: + z_632 + z_592 + z_502 + z_1127 + z_1067 + z_1042 + z_357 + z_927 + z_782 + z_692 = 1 r_594: + z_562 + z_1172 + z_452 + z_1077 + z_392 + z_362 + z_312 + z_972 + z_257 + z_742 + z_702 = 1 r_595: + z_537 + z_1182 + z_1047 + z_262 + z_932 + z_852 + z_787 + z_747 + z_52 = 1 r_596: + z_642 + z_402 + z_372 + z_172 + z_797 + z_107 = 1 r_597: + z_597 + z_567 + z_542 + z_1192 + z_472 + z_1097 + z_982 + z_177 + z_117 + z_707 + z_17 = 1 r_598: + z_652 + z_512 + z_412 + z_322 + z_987 + z_907 + z_187 + z_857 + z_812 + z_122 + z_762 + z_62 = 1 r_599: + z_657 + z_602 + z_547 + z_327 + z_277 + z_942 + z_862 = 1 r_600: + z_577 + z_517 + z_332 + z_947 + z_192 + z_822 + z_767 + z_717 = 1 r_601: - z_27 - z_22 - z_17 - z_12 - z_7 - z_2 - z_622 - z_582 - z_492 - z_1117 - z_1052 - z_232 - z_917 - z_877 - z_677 <= -1 r_602: - z_72 - z_67 - z_62 - z_57 - z_52 - z_47 - z_42 - z_37 - z_32 - z_1057 - z_1027 - z_337 - z_202 - z_882 - z_837 <= -1 r_603: - z_132 - z_127 - z_122 - z_117 - z_112 - z_107 - z_102 - z_97 - z_92 - z_87 - z_82 - z_77 - z_1157 - z_1122 - z_437 - z_342 - z_962 - z_242 - z_727 - z_37 - z_682 <= -1 r_604: - z_162 - z_157 - z_152 - z_147 - z_142 - z_137 - z_442 - z_382 - z_1002 - z_967 - z_887 - z_87 - z_2 <= -1 r_605: - z_197 - z_192 - z_187 - z_182 - z_177 - z_172 - z_167 - z_627 - z_532 - z_1167 - z_497 - z_447 - z_387 - z_1037 - z_352 - z_1012 - z_302 - z_212 - z_842 - z_137 - z_97 - z_737 - z_47 - z_7 <= -1 r_606: - z_227 - z_222 - z_217 - z_212 - z_207 - z_202 - z_507 - z_1132 - z_1072 - z_307 - z_252 - z_142 - z_697 <= -1 r_607: - z_287 - z_282 - z_277 - z_272 - z_267 - z_262 - z_257 - z_252 - z_247 - z_242 - z_237 - z_232 - z_1177 - z_457 - z_1082 - z_367 - z_317 - z_217 - z_892 - z_847 - z_12 <= -1 r_608: - z_332 - z_327 - z_322 - z_317 - z_312 - z_307 - z_302 - z_297 - z_292 - z_637 - z_1187 - z_1137 - z_462 - z_1087 - z_397 - z_267 - z_937 - z_147 - z_792 - z_102 - z_57 <= -1 r_609: - z_372 - z_367 - z_362 - z_357 - z_352 - z_347 - z_342 - z_337 - z_467 - z_1092 - z_407 - z_977 - z_897 - z_802 - z_112 - z_752 <= -1 r_610: - z_422 - z_417 - z_412 - z_407 - z_402 - z_397 - z_392 - z_387 - z_382 - z_377 - z_647 - z_1197 - z_1142 - z_1102 - z_272 - z_222 - z_902 - z_182 - z_152 - z_807 - z_757 <= -1 r_611: - z_487 - z_482 - z_477 - z_472 - z_467 - z_462 - z_457 - z_452 - z_447 - z_442 - z_437 - z_432 - z_427 - z_572 - z_1202 - z_417 - z_912 - z_127 - z_67 <= -1 r_612: - z_522 - z_517 - z_512 - z_507 - z_502 - z_497 - z_492 - z_607 - z_552 - z_1207 - z_477 - z_992 - z_282 - z_817 - z_132 - z_72 - z_712 <= -1 r_613: - z_552 - z_547 - z_542 - z_537 - z_532 - z_527 - z_662 - z_612 - z_997 - z_227 - z_197 - z_157 - z_827 <= -1 r_614: - z_577 - z_572 - z_567 - z_562 - z_557 - z_667 - z_617 - z_1147 - z_482 - z_867 - z_722 - z_22 <= -1 r_615: - z_617 - z_612 - z_607 - z_602 - z_597 - z_592 - z_587 - z_582 - z_672 - z_1152 - z_487 - z_1107 - z_1017 - z_287 - z_162 - z_832 <= -1 r_616: - z_672 - z_667 - z_662 - z_657 - z_652 - z_647 - z_642 - z_637 - z_632 - z_627 - z_622 - z_1212 - z_522 - z_1112 - z_422 - z_1022 - z_952 - z_872 - z_772 - z_27 <= -1 r_617: - z_722 - z_717 - z_712 - z_707 - z_702 - z_697 - z_692 - z_687 - z_682 - z_677 - z_587 - z_527 - z_427 - z_292 - z_922 - z_77 - z_32 <= -1 r_618: - z_772 - z_767 - z_762 - z_757 - z_752 - z_747 - z_742 - z_737 - z_732 - z_727 - z_432 - z_1062 - z_957 - z_237 - z_777 - z_82 <= -1 r_619: - z_832 - z_827 - z_822 - z_817 - z_812 - z_807 - z_802 - z_797 - z_792 - z_787 - z_782 - z_777 - z_557 - z_377 - z_347 - z_297 - z_42 <= -1 r_620: - z_872 - z_867 - z_862 - z_857 - z_852 - z_847 - z_842 - z_837 - z_1162 - z_1032 - z_1007 - z_247 - z_207 - z_167 - z_92 - z_732 - z_687 <= -1 r_621: - z_912 - z_907 - z_902 - z_897 - z_892 - z_887 - z_882 - z_877 - z_632 - z_592 - z_502 - z_1127 - z_1067 - z_1042 - z_357 - z_927 - z_782 - z_692 <= -1 r_622: - z_952 - z_947 - z_942 - z_937 - z_932 - z_927 - z_922 - z_917 - z_562 - z_1172 - z_452 - z_1077 - z_392 - z_362 - z_312 - z_972 - z_257 - z_742 - z_702 <= -1 r_623: - z_997 - z_992 - z_987 - z_982 - z_977 - z_972 - z_967 - z_962 - z_957 - z_537 - z_1182 - z_1047 - z_262 - z_932 - z_852 - z_787 - z_747 - z_52 <= -1 r_624: - z_1022 - z_1017 - z_1012 - z_1007 - z_1002 - z_642 - z_402 - z_372 - z_172 - z_797 - z_107 <= -1 r_625: - z_1047 - z_1042 - z_1037 - z_1032 - z_1027 - z_597 - z_567 - z_542 - z_1192 - z_472 - z_1097 - z_982 - z_177 - z_117 - z_707 - z_17 <= -1 r_626: - z_1112 - z_1107 - z_1102 - z_1097 - z_1092 - z_1087 - z_1082 - z_1077 - z_1072 - z_1067 - z_1062 - z_1057 - z_1052 - z_652 - z_512 - z_412 - z_322 - z_987 - z_907 - z_187 - z_857 - z_812 - z_122 - z_762 - z_62 <= -1 r_627: - z_1152 - z_1147 - z_1142 - z_1137 - z_1132 - z_1127 - z_1122 - z_1117 - z_657 - z_602 - z_547 - z_327 - z_277 - z_942 - z_862 <= -1 r_628: - z_1212 - z_1207 - z_1202 - z_1197 - z_1192 - z_1187 - z_1182 - z_1177 - z_1172 - z_1167 - z_1162 - z_1157 - z_577 - z_517 - z_332 - z_947 - z_192 - z_822 - z_767 - z_717 <= -1 r_629: - x_1245 + 28 z_2 + x_1244 <= 27 r_630: - x_1246 + 28 z_7 + x_1244 <= 27 r_631: - x_1247 + 25 z_232 + 27 z_12 + x_1244 <= 26 r_632: - x_1248 + 28 z_17 + x_1244 <= 27 r_633: - x_1249 + 28 z_22 + x_1244 <= 27 r_634: - x_1250 + 25 z_622 + 27 z_27 + x_1244 <= 26 r_635: - x_1252 + 28 z_32 + x_1251 <= 27 r_636: - x_1253 + 28 z_37 + x_1251 <= 27 r_637: - x_1254 + 28 z_42 + x_1251 <= 27 r_638: - x_1246 + 28 z_47 + x_1251 <= 27 r_639: - x_1255 + 28 z_52 + x_1251 <= 27 r_640: - x_1256 + 28 z_57 + x_1251 <= 27 r_641: - x_1257 + 25 z_1057 + 27 z_62 + x_1251 <= 26 r_642: - x_1258 + 28 z_67 + x_1251 <= 27 r_643: - x_1259 + 28 z_72 + x_1251 <= 27 r_644: - x_1252 + 25 z_682 + 27 z_77 + x_1253 <= 26 r_645: - x_1260 + 25 z_727 + 27 z_82 + x_1253 <= 26 r_646: - x_1245 + 28 z_87 + x_1253 <= 27 r_647: - x_1261 + 28 z_92 + x_1253 <= 27 r_648: - x_1246 + 28 z_97 + x_1253 <= 27 r_649: - x_1256 + 28 z_102 + x_1253 <= 27 r_650: - x_1262 + 28 z_107 + x_1253 <= 27 r_651: - x_1263 + 25 z_342 + 27 z_112 + x_1253 <= 26 r_652: - x_1248 + 28 z_117 + x_1253 <= 27 r_653: - x_1257 + 28 z_122 + x_1253 <= 27 r_654: - x_1258 + 25 z_437 + 27 z_127 + x_1253 <= 26 r_655: - x_1259 + 28 z_132 + x_1253 <= 27 r_656: - x_1246 + 28 z_137 + x_1245 <= 27 r_657: - x_1264 + 28 z_142 + x_1245 <= 27 r_658: - x_1256 + 28 z_147 + x_1245 <= 27 r_659: - x_1265 + 25 z_382 + 27 z_152 + x_1245 <= 26 r_660: - x_1266 + 28 z_157 + x_1245 <= 27 r_661: - x_1267 + 28 z_162 + x_1245 <= 27 r_662: - x_1261 + 25 z_842 + 27 z_167 + x_1246 <= 26 r_663: - x_1262 + 25 z_1012 + 27 z_172 + x_1246 <= 26 r_664: - x_1248 + 25 z_1037 + 27 z_177 + x_1246 <= 26 r_665: - x_1265 + 25 z_387 + 27 z_182 + x_1246 <= 26 r_666: - x_1257 + 28 z_187 + x_1246 <= 27 r_667: - x_1268 + 25 z_1167 + 27 z_192 + x_1246 <= 26 r_668: - x_1266 + 25 z_532 + 27 z_197 + x_1246 <= 26 r_669: - x_1251 + 28 z_202 + x_1264 <= 27 r_670: - x_1261 + 28 z_207 + x_1264 <= 27 r_671: - x_1246 + 28 z_212 + x_1264 <= 27 r_672: - x_1247 + 25 z_252 + 27 z_217 + x_1264 <= 26 r_673: - x_1265 + 28 z_222 + x_1264 <= 27 r_674: - x_1266 + 28 z_227 + x_1264 <= 27 r_675: - x_1244 + 25 z_12 + 27 z_232 + x_1247 <= 26 r_676: - x_1260 + 28 z_237 + x_1247 <= 27 r_677: - x_1253 + 28 z_242 + x_1247 <= 27 r_678: - x_1261 + 25 z_847 + 27 z_247 + x_1247 <= 26 r_679: - x_1264 + 25 z_217 + 27 z_252 + x_1247 <= 26 r_680: - x_1269 + 28 z_257 + x_1247 <= 27 r_681: - x_1255 + 28 z_262 + x_1247 <= 27 r_682: - x_1256 + 25 z_317 + 27 z_267 + x_1247 <= 26 r_683: - x_1265 + 28 z_272 + x_1247 <= 27 r_684: - x_1270 + 28 z_277 + x_1247 <= 27 r_685: - x_1259 + 28 z_282 + x_1247 <= 27 r_686: - x_1267 + 28 z_287 + x_1247 <= 27 r_687: - x_1252 + 28 z_292 + x_1256 <= 27 r_688: - x_1254 + 25 z_792 + 27 z_297 + x_1256 <= 26 r_689: - x_1246 + 28 z_302 + x_1256 <= 27 r_690: - x_1264 + 28 z_307 + x_1256 <= 27 r_691: - x_1269 + 25 z_937 + 27 z_312 + x_1256 <= 26 r_692: - x_1247 + 25 z_267 + 27 z_317 + x_1256 <= 26 r_693: - x_1257 + 25 z_1087 + 27 z_322 + x_1256 <= 26 r_694: - x_1270 + 25 z_1137 + 27 z_327 + x_1256 <= 26 r_695: - x_1268 + 25 z_1187 + 27 z_332 + x_1256 <= 26 r_696: - x_1251 + 28 z_337 + x_1263 <= 27 r_697: - x_1253 + 25 z_112 + 27 z_342 + x_1263 <= 26 r_698: - x_1254 + 25 z_802 + 27 z_347 + x_1263 <= 26 r_699: - x_1246 + 28 z_352 + x_1263 <= 27 r_700: - x_1271 + 25 z_897 + 27 z_357 + x_1263 <= 26 r_701: - x_1269 + 28 z_362 + x_1263 <= 27 r_702: - x_1247 + 28 z_367 + x_1263 <= 27 r_703: - x_1262 + 28 z_372 + x_1263 <= 27 r_704: - x_1254 + 25 z_807 + 27 z_377 + x_1265 <= 26 r_705: - x_1245 + 25 z_152 + 27 z_382 + x_1265 <= 26 r_706: - x_1246 + 25 z_182 + 27 z_387 + x_1265 <= 26 r_707: - x_1269 + 28 z_392 + x_1265 <= 27 r_708: - x_1256 + 28 z_397 + x_1265 <= 27 r_709: - x_1262 + 28 z_402 + x_1265 <= 27 r_710: - x_1263 + 28 z_407 + x_1265 <= 27 r_711: - x_1257 + 25 z_1102 + 27 z_412 + x_1265 <= 26 r_712: - x_1258 + 28 z_417 + x_1265 <= 27 r_713: - x_1250 + 25 z_647 + 27 z_422 + x_1265 <= 26 r_714: - x_1252 + 28 z_427 + x_1258 <= 27 r_715: - x_1260 + 28 z_432 + x_1258 <= 27 r_716: - x_1253 + 25 z_127 + 27 z_437 + x_1258 <= 26 r_717: - x_1245 + 28 z_442 + x_1258 <= 27 r_718: - x_1246 + 28 z_447 + x_1258 <= 27 r_719: - x_1269 + 28 z_452 + x_1258 <= 27 r_720: - x_1247 + 28 z_457 + x_1258 <= 27 r_721: - x_1256 + 28 z_462 + x_1258 <= 27 r_722: - x_1263 + 28 z_467 + x_1258 <= 27 r_723: - x_1248 + 28 z_472 + x_1258 <= 27 r_724: - x_1259 + 28 z_477 + x_1258 <= 27 r_725: - x_1249 + 25 z_572 + 27 z_482 + x_1258 <= 26 r_726: - x_1267 + 28 z_487 + x_1258 <= 27 r_727: - x_1244 + 28 z_492 + x_1259 <= 27 r_728: - x_1246 + 28 z_497 + x_1259 <= 27 r_729: - x_1271 + 28 z_502 + x_1259 <= 27 r_730: - x_1264 + 28 z_507 + x_1259 <= 27 r_731: - x_1257 + 28 z_512 + x_1259 <= 27 r_732: - x_1268 + 25 z_1207 + 27 z_517 + x_1259 <= 26 r_733: - x_1250 + 28 z_522 + x_1259 <= 27 r_734: - x_1252 + 28 z_527 + x_1266 <= 27 r_735: - x_1246 + 25 z_197 + 27 z_532 + x_1266 <= 26 r_736: - x_1255 + 25 z_997 + 27 z_537 + x_1266 <= 26 r_737: - x_1248 + 28 z_542 + x_1266 <= 27 r_738: - x_1270 + 28 z_547 + x_1266 <= 27 r_739: - x_1259 + 28 z_552 + x_1266 <= 27 r_740: - x_1254 + 28 z_557 + x_1249 <= 27 r_741: - x_1269 + 28 z_562 + x_1249 <= 27 r_742: - x_1248 + 28 z_567 + x_1249 <= 27 r_743: - x_1258 + 25 z_482 + 27 z_572 + x_1249 <= 26 r_744: - x_1268 + 28 z_577 + x_1249 <= 27 r_745: - x_1244 + 28 z_582 + x_1267 <= 27 r_746: - x_1252 + 28 z_587 + x_1267 <= 27 r_747: - x_1271 + 28 z_592 + x_1267 <= 27 r_748: - x_1248 + 28 z_597 + x_1267 <= 27 r_749: - x_1270 + 25 z_1152 + 27 z_602 + x_1267 <= 26 r_750: - x_1259 + 28 z_607 + x_1267 <= 27 r_751: - x_1266 + 28 z_612 + x_1267 <= 27 r_752: - x_1249 + 28 z_617 + x_1267 <= 27 r_753: - x_1244 + 25 z_27 + 27 z_622 + x_1250 <= 26 r_754: - x_1246 + 28 z_627 + x_1250 <= 27 r_755: - x_1271 + 28 z_632 + x_1250 <= 27 r_756: - x_1256 + 28 z_637 + x_1250 <= 27 r_757: - x_1262 + 25 z_1022 + 27 z_642 + x_1250 <= 26 r_758: - x_1265 + 25 z_422 + 27 z_647 + x_1250 <= 26 r_759: - x_1257 + 25 z_1112 + 27 z_652 + x_1250 <= 26 r_760: - x_1270 + 28 z_657 + x_1250 <= 27 r_761: - x_1266 + 28 z_662 + x_1250 <= 27 r_762: - x_1249 + 28 z_667 + x_1250 <= 27 r_763: - x_1267 + 28 z_672 + x_1250 <= 27 r_764: - x_1244 + 28 z_677 + x_1252 <= 27 r_765: - x_1253 + 25 z_77 + 27 z_682 + x_1252 <= 26 r_766: - x_1261 + 28 z_687 + x_1252 <= 27 r_767: - x_1271 + 28 z_692 + x_1252 <= 27 r_768: - x_1264 + 28 z_697 + x_1252 <= 27 r_769: - x_1269 + 25 z_922 + 27 z_702 + x_1252 <= 26 r_770: - x_1248 + 28 z_707 + x_1252 <= 27 r_771: - x_1259 + 28 z_712 + x_1252 <= 27 r_772: - x_1268 + 28 z_717 + x_1252 <= 27 r_773: - x_1249 + 28 z_722 + x_1252 <= 27 r_774: - x_1253 + 25 z_82 + 27 z_727 + x_1260 <= 26 r_775: - x_1261 + 28 z_732 + x_1260 <= 27 r_776: - x_1246 + 28 z_737 + x_1260 <= 27 r_777: - x_1269 + 28 z_742 + x_1260 <= 27 r_778: - x_1255 + 25 z_957 + 27 z_747 + x_1260 <= 26 r_779: - x_1263 + 28 z_752 + x_1260 <= 27 r_780: - x_1265 + 28 z_757 + x_1260 <= 27 r_781: - x_1257 + 25 z_1062 + 27 z_762 + x_1260 <= 26 r_782: - x_1268 + 28 z_767 + x_1260 <= 27 r_783: - x_1250 + 28 z_772 + x_1260 <= 27 r_784: - x_1260 + 28 z_777 + x_1254 <= 27 r_785: - x_1271 + 28 z_782 + x_1254 <= 27 r_786: - x_1255 + 28 z_787 + x_1254 <= 27 r_787: - x_1256 + 25 z_297 + 27 z_792 + x_1254 <= 26 r_788: - x_1262 + 28 z_797 + x_1254 <= 27 r_789: - x_1263 + 25 z_347 + 27 z_802 + x_1254 <= 26 r_790: - x_1265 + 25 z_377 + 27 z_807 + x_1254 <= 26 r_791: - x_1257 + 28 z_812 + x_1254 <= 27 r_792: - x_1259 + 28 z_817 + x_1254 <= 27 r_793: - x_1268 + 28 z_822 + x_1254 <= 27 r_794: - x_1266 + 28 z_827 + x_1254 <= 27 r_795: - x_1267 + 28 z_832 + x_1254 <= 27 r_796: - x_1251 + 28 z_837 + x_1261 <= 27 r_797: - x_1246 + 25 z_167 + 27 z_842 + x_1261 <= 26 r_798: - x_1247 + 25 z_247 + 27 z_847 + x_1261 <= 26 r_799: - x_1255 + 28 z_852 + x_1261 <= 27 r_800: - x_1257 + 28 z_857 + x_1261 <= 27 r_801: - x_1270 + 28 z_862 + x_1261 <= 27 r_802: - x_1249 + 28 z_867 + x_1261 <= 27 r_803: - x_1250 + 28 z_872 + x_1261 <= 27 r_804: - x_1244 + 28 z_877 + x_1271 <= 27 r_805: - x_1251 + 28 z_882 + x_1271 <= 27 r_806: - x_1245 + 28 z_887 + x_1271 <= 27 r_807: - x_1247 + 28 z_892 + x_1271 <= 27 r_808: - x_1263 + 25 z_357 + 27 z_897 + x_1271 <= 26 r_809: - x_1265 + 28 z_902 + x_1271 <= 27 r_810: - x_1257 + 25 z_1067 + 27 z_907 + x_1271 <= 26 r_811: - x_1258 + 28 z_912 + x_1271 <= 27 r_812: - x_1244 + 28 z_917 + x_1269 <= 27 r_813: - x_1252 + 25 z_702 + 27 z_922 + x_1269 <= 26 r_814: - x_1271 + 28 z_927 + x_1269 <= 27 r_815: - x_1255 + 25 z_972 + 27 z_932 + x_1269 <= 26 r_816: - x_1256 + 25 z_312 + 27 z_937 + x_1269 <= 26 r_817: - x_1270 + 28 z_942 + x_1269 <= 27 r_818: - x_1268 + 25 z_1172 + 27 z_947 + x_1269 <= 26 r_819: - x_1250 + 28 z_952 + x_1269 <= 27 r_820: - x_1260 + 25 z_747 + 27 z_957 + x_1255 <= 26 r_821: - x_1253 + 28 z_962 + x_1255 <= 27 r_822: - x_1245 + 28 z_967 + x_1255 <= 27 r_823: - x_1269 + 25 z_932 + 27 z_972 + x_1255 <= 26 r_824: - x_1263 + 28 z_977 + x_1255 <= 27 r_825: - x_1248 + 25 z_1047 + 27 z_982 + x_1255 <= 26 r_826: - x_1257 + 28 z_987 + x_1255 <= 27 r_827: - x_1259 + 28 z_992 + x_1255 <= 27 r_828: - x_1266 + 25 z_537 + 27 z_997 + x_1255 <= 26 r_829: - x_1245 + 28 z_1002 + x_1262 <= 27 r_830: - x_1261 + 28 z_1007 + x_1262 <= 27 r_831: - x_1246 + 25 z_172 + 27 z_1012 + x_1262 <= 26 r_832: - x_1267 + 28 z_1017 + x_1262 <= 27 r_833: - x_1250 + 25 z_642 + 27 z_1022 + x_1262 <= 26 r_834: - x_1251 + 28 z_1027 + x_1248 <= 27 r_835: - x_1261 + 28 z_1032 + x_1248 <= 27 r_836: - x_1246 + 25 z_177 + 27 z_1037 + x_1248 <= 26 r_837: - x_1271 + 28 z_1042 + x_1248 <= 27 r_838: - x_1255 + 25 z_982 + 27 z_1047 + x_1248 <= 26 r_839: - x_1244 + 28 z_1052 + x_1257 <= 27 r_840: - x_1251 + 25 z_62 + 27 z_1057 + x_1257 <= 26 r_841: - x_1260 + 25 z_762 + 27 z_1062 + x_1257 <= 26 r_842: - x_1271 + 25 z_907 + 27 z_1067 + x_1257 <= 26 r_843: - x_1264 + 28 z_1072 + x_1257 <= 27 r_844: - x_1269 + 28 z_1077 + x_1257 <= 27 r_845: - x_1247 + 28 z_1082 + x_1257 <= 27 r_846: - x_1256 + 25 z_322 + 27 z_1087 + x_1257 <= 26 r_847: - x_1263 + 28 z_1092 + x_1257 <= 27 r_848: - x_1248 + 28 z_1097 + x_1257 <= 27 r_849: - x_1265 + 25 z_412 + 27 z_1102 + x_1257 <= 26 r_850: - x_1267 + 28 z_1107 + x_1257 <= 27 r_851: - x_1250 + 25 z_652 + 27 z_1112 + x_1257 <= 26 r_852: - x_1244 + 28 z_1117 + x_1270 <= 27 r_853: - x_1253 + 28 z_1122 + x_1270 <= 27 r_854: - x_1271 + 28 z_1127 + x_1270 <= 27 r_855: - x_1264 + 28 z_1132 + x_1270 <= 27 r_856: - x_1256 + 25 z_327 + 27 z_1137 + x_1270 <= 26 r_857: - x_1265 + 28 z_1142 + x_1270 <= 27 r_858: - x_1249 + 28 z_1147 + x_1270 <= 27 r_859: - x_1267 + 25 z_602 + 27 z_1152 + x_1270 <= 26 r_860: - x_1253 + 28 z_1157 + x_1268 <= 27 r_861: - x_1261 + 28 z_1162 + x_1268 <= 27 r_862: - x_1246 + 25 z_192 + 27 z_1167 + x_1268 <= 26 r_863: - x_1269 + 25 z_947 + 27 z_1172 + x_1268 <= 26 r_864: - x_1247 + 28 z_1177 + x_1268 <= 27 r_865: - x_1255 + 28 z_1182 + x_1268 <= 27 r_866: - x_1256 + 25 z_332 + 27 z_1187 + x_1268 <= 26 r_867: - x_1248 + 28 z_1192 + x_1268 <= 27 r_868: - x_1265 + 28 z_1197 + x_1268 <= 27 r_869: - x_1258 + 28 z_1202 + x_1268 <= 27 r_870: - x_1259 + 25 z_517 + 27 z_1207 + x_1268 <= 26 r_871: - x_1250 + 28 z_1212 + x_1268 <= 27 r_872: 0 z_1 <= 0 r_873: - x_1251 + x_1244 <= -2 r_874: - x_1253 + x_1244 <= -2 r_875: - x_1245 + x_1244 <= -1 r_876: - x_1246 + x_1244 <= -1 r_877: - x_1264 + x_1244 <= -2 r_878: - x_1247 + x_1244 <= -1 r_879: - x_1256 + x_1244 <= -2 r_880: - x_1263 + x_1244 <= -3 r_881: - x_1265 + x_1244 <= -2 r_882: - x_1258 + x_1244 <= -2 r_883: - x_1259 + x_1244 <= -2 r_884: - x_1266 + x_1244 <= -2 r_885: - x_1249 + x_1244 <= -1 r_886: - x_1267 + x_1244 <= -2 r_887: - x_1250 + x_1244 <= -1 r_888: - x_1252 + x_1244 <= -3 r_889: - x_1260 + x_1244 <= -2 r_890: - x_1254 + x_1244 <= -2 r_891: - x_1261 + x_1244 <= -2 r_892: - x_1271 + x_1244 <= -2 r_893: - x_1269 + x_1244 <= -2 r_894: - x_1255 + x_1244 <= -2 r_895: - x_1262 + x_1244 <= -2 r_896: - x_1248 + x_1244 <= -1 r_897: - x_1257 + x_1244 <= -2 r_898: - x_1270 + x_1244 <= -2 r_899: - x_1268 + x_1244 <= -2 r_900: + z_1213 + z_1208 + z_1203 + z_1198 + z_1193 + z_1188 + z_1183 + z_1178 + z_1173 + z_1168 + z_1163 + z_1158 + z_1153 + z_1148 + z_1143 + z_1138 + z_1133 + z_1128 + z_1123 + z_1118 + z_1113 + z_1108 + z_1103 + z_1098 + z_1093 + z_1088 + z_1083 + z_1078 + z_1073 + z_1068 + z_1063 + z_1058 + z_1053 + z_1048 + z_1043 + z_1038 + z_1033 + z_1028 + z_1023 + z_1018 + z_1013 + z_1008 + z_1003 + z_998 + z_993 + z_988 + z_983 + z_978 + z_973 + z_968 + z_963 + z_958 + z_953 + z_948 + z_943 + z_938 + z_933 + z_928 + z_923 + z_918 + z_913 + z_908 + z_903 + z_898 + z_893 + z_888 + z_883 + z_878 + z_873 + z_868 + z_863 + z_858 + z_853 + z_848 + z_843 + z_838 + z_833 + z_828 + z_823 + z_818 + z_813 + z_808 + z_803 + z_798 + z_793 + z_788 + z_783 + z_778 + z_773 + z_768 + z_763 + z_758 + z_753 + z_748 + z_743 + z_738 + z_733 + z_728 + z_723 + z_718 + z_713 + z_708 + z_703 + z_698 + z_693 + z_688 + z_683 + z_678 + z_673 + z_668 + z_663 + z_658 + z_653 + z_648 + z_643 + z_638 + z_633 + z_628 + z_623 + z_618 + z_613 + z_608 + z_603 + z_598 + z_593 + z_588 + z_583 + z_578 + z_573 + z_568 + z_563 + z_558 + z_553 + z_548 + z_543 + z_538 + z_533 + z_528 + z_523 + z_518 + z_513 + z_508 + z_503 + z_498 + z_493 + z_488 + z_483 + z_478 + z_473 + z_468 + z_463 + z_458 + z_453 + z_448 + z_443 + z_438 + z_433 + z_428 + z_423 + z_418 + z_413 + z_408 + z_403 + z_398 + z_393 + z_388 + z_383 + z_378 + z_373 + z_368 + z_363 + z_358 + z_353 + z_348 + z_343 + z_338 + z_333 + z_328 + z_323 + z_318 + z_313 + z_308 + z_303 + z_298 + z_293 + z_288 + z_283 + z_278 + z_273 + z_268 + z_263 + z_258 + z_253 + z_248 + z_243 + z_238 + z_233 + z_228 + z_223 + z_218 + z_213 + z_208 + z_203 + z_198 + z_193 + z_188 + z_183 + z_178 + z_173 + z_168 + z_163 + z_158 + z_153 + z_148 + z_143 + z_138 + z_133 + z_128 + z_123 + z_118 + z_113 + z_108 + z_103 + z_98 + z_93 + z_88 + z_83 + z_78 + z_73 + z_68 + z_63 + z_58 + z_53 + z_48 + z_43 + z_38 + z_33 + z_28 + z_23 + z_18 + z_13 + z_8 + z_3 = 27 r_901: + z_623 + z_583 + z_493 + z_1118 + z_1053 + z_233 + z_918 + z_878 + z_678 = 0 r_902: + z_1058 + z_1028 + z_338 + z_203 + z_883 + z_838 = 1 r_903: + z_1158 + z_1123 + z_438 + z_343 + z_963 + z_243 + z_728 + z_38 + z_683 = 1 r_904: + z_443 + z_383 + z_1003 + z_968 + z_888 + z_88 + z_3 = 1 r_905: + z_628 + z_533 + z_1168 + z_498 + z_448 + z_388 + z_1038 + z_353 + z_1013 + z_303 + z_213 + z_843 + z_138 + z_98 + z_738 + z_48 + z_8 = 1 r_906: + z_508 + z_1133 + z_1073 + z_308 + z_253 + z_143 + z_698 = 1 r_907: + z_1178 + z_458 + z_1083 + z_368 + z_318 + z_218 + z_893 + z_848 + z_13 = 1 r_908: + z_638 + z_1188 + z_1138 + z_463 + z_1088 + z_398 + z_268 + z_938 + z_148 + z_793 + z_103 + z_58 = 1 r_909: + z_468 + z_1093 + z_408 + z_978 + z_898 + z_803 + z_113 + z_753 = 1 r_910: + z_648 + z_1198 + z_1143 + z_1103 + z_273 + z_223 + z_903 + z_183 + z_153 + z_808 + z_758 = 1 r_911: + z_573 + z_1203 + z_418 + z_913 + z_128 + z_68 = 1 r_912: + z_608 + z_553 + z_1208 + z_478 + z_993 + z_283 + z_818 + z_133 + z_73 + z_713 = 1 r_913: + z_663 + z_613 + z_998 + z_228 + z_198 + z_158 + z_828 = 1 r_914: + z_668 + z_618 + z_1148 + z_483 + z_868 + z_723 + z_23 = 1 r_915: + z_673 + z_1153 + z_488 + z_1108 + z_1018 + z_288 + z_163 + z_833 = 1 r_916: + z_1213 + z_523 + z_1113 + z_423 + z_1023 + z_953 + z_873 + z_773 + z_28 = 1 r_917: + z_588 + z_528 + z_428 + z_293 + z_923 + z_78 + z_33 = 1 r_918: + z_433 + z_1063 + z_958 + z_238 + z_778 + z_83 = 1 r_919: + z_558 + z_378 + z_348 + z_298 + z_43 = 1 r_920: + z_1163 + z_1033 + z_1008 + z_248 + z_208 + z_168 + z_93 + z_733 + z_688 = 1 r_921: + z_633 + z_593 + z_503 + z_1128 + z_1068 + z_1043 + z_358 + z_928 + z_783 + z_693 = 1 r_922: + z_563 + z_1173 + z_453 + z_1078 + z_393 + z_363 + z_313 + z_973 + z_258 + z_743 + z_703 = 1 r_923: + z_538 + z_1183 + z_1048 + z_263 + z_933 + z_853 + z_788 + z_748 + z_53 = 1 r_924: + z_643 + z_403 + z_373 + z_173 + z_798 + z_108 = 1 r_925: + z_598 + z_568 + z_543 + z_1193 + z_473 + z_1098 + z_983 + z_178 + z_118 + z_708 + z_18 = 1 r_926: + z_653 + z_513 + z_413 + z_323 + z_988 + z_908 + z_188 + z_858 + z_813 + z_123 + z_763 + z_63 = 1 r_927: + z_658 + z_603 + z_548 + z_328 + z_278 + z_943 + z_863 = 1 r_928: + z_578 + z_518 + z_333 + z_948 + z_193 + z_823 + z_768 + z_718 = 1 r_929: - z_28 - z_23 - z_18 - z_13 - z_8 - z_3 - z_623 - z_583 - z_493 - z_1118 - z_1053 - z_233 - z_918 - z_878 - z_678 <= -1 r_930: - z_73 - z_68 - z_63 - z_58 - z_53 - z_48 - z_43 - z_38 - z_33 - z_1058 - z_1028 - z_338 - z_203 - z_883 - z_838 <= -1 r_931: - z_133 - z_128 - z_123 - z_118 - z_113 - z_108 - z_103 - z_98 - z_93 - z_88 - z_83 - z_78 - z_1158 - z_1123 - z_438 - z_343 - z_963 - z_243 - z_728 - z_38 - z_683 <= -1 r_932: - z_163 - z_158 - z_153 - z_148 - z_143 - z_138 - z_443 - z_383 - z_1003 - z_968 - z_888 - z_88 - z_3 <= -1 r_933: - z_198 - z_193 - z_188 - z_183 - z_178 - z_173 - z_168 - z_628 - z_533 - z_1168 - z_498 - z_448 - z_388 - z_1038 - z_353 - z_1013 - z_303 - z_213 - z_843 - z_138 - z_98 - z_738 - z_48 - z_8 <= -1 r_934: - z_228 - z_223 - z_218 - z_213 - z_208 - z_203 - z_508 - z_1133 - z_1073 - z_308 - z_253 - z_143 - z_698 <= -1 r_935: - z_288 - z_283 - z_278 - z_273 - z_268 - z_263 - z_258 - z_253 - z_248 - z_243 - z_238 - z_233 - z_1178 - z_458 - z_1083 - z_368 - z_318 - z_218 - z_893 - z_848 - z_13 <= -1 r_936: - z_333 - z_328 - z_323 - z_318 - z_313 - z_308 - z_303 - z_298 - z_293 - z_638 - z_1188 - z_1138 - z_463 - z_1088 - z_398 - z_268 - z_938 - z_148 - z_793 - z_103 - z_58 <= -1 r_937: - z_373 - z_368 - z_363 - z_358 - z_353 - z_348 - z_343 - z_338 - z_468 - z_1093 - z_408 - z_978 - z_898 - z_803 - z_113 - z_753 <= -1 r_938: - z_423 - z_418 - z_413 - z_408 - z_403 - z_398 - z_393 - z_388 - z_383 - z_378 - z_648 - z_1198 - z_1143 - z_1103 - z_273 - z_223 - z_903 - z_183 - z_153 - z_808 - z_758 <= -1 r_939: - z_488 - z_483 - z_478 - z_473 - z_468 - z_463 - z_458 - z_453 - z_448 - z_443 - z_438 - z_433 - z_428 - z_573 - z_1203 - z_418 - z_913 - z_128 - z_68 <= -1 r_940: - z_523 - z_518 - z_513 - z_508 - z_503 - z_498 - z_493 - z_608 - z_553 - z_1208 - z_478 - z_993 - z_283 - z_818 - z_133 - z_73 - z_713 <= -1 r_941: - z_553 - z_548 - z_543 - z_538 - z_533 - z_528 - z_663 - z_613 - z_998 - z_228 - z_198 - z_158 - z_828 <= -1 r_942: - z_578 - z_573 - z_568 - z_563 - z_558 - z_668 - z_618 - z_1148 - z_483 - z_868 - z_723 - z_23 <= -1 r_943: - z_618 - z_613 - z_608 - z_603 - z_598 - z_593 - z_588 - z_583 - z_673 - z_1153 - z_488 - z_1108 - z_1018 - z_288 - z_163 - z_833 <= -1 r_944: - z_673 - z_668 - z_663 - z_658 - z_653 - z_648 - z_643 - z_638 - z_633 - z_628 - z_623 - z_1213 - z_523 - z_1113 - z_423 - z_1023 - z_953 - z_873 - z_773 - z_28 <= -1 r_945: - z_723 - z_718 - z_713 - z_708 - z_703 - z_698 - z_693 - z_688 - z_683 - z_678 - z_588 - z_528 - z_428 - z_293 - z_923 - z_78 - z_33 <= -1 r_946: - z_773 - z_768 - z_763 - z_758 - z_753 - z_748 - z_743 - z_738 - z_733 - z_728 - z_433 - z_1063 - z_958 - z_238 - z_778 - z_83 <= -1 r_947: - z_833 - z_828 - z_823 - z_818 - z_813 - z_808 - z_803 - z_798 - z_793 - z_788 - z_783 - z_778 - z_558 - z_378 - z_348 - z_298 - z_43 <= -1 r_948: - z_873 - z_868 - z_863 - z_858 - z_853 - z_848 - z_843 - z_838 - z_1163 - z_1033 - z_1008 - z_248 - z_208 - z_168 - z_93 - z_733 - z_688 <= -1 r_949: - z_913 - z_908 - z_903 - z_898 - z_893 - z_888 - z_883 - z_878 - z_633 - z_593 - z_503 - z_1128 - z_1068 - z_1043 - z_358 - z_928 - z_783 - z_693 <= -1 r_950: - z_953 - z_948 - z_943 - z_938 - z_933 - z_928 - z_923 - z_918 - z_563 - z_1173 - z_453 - z_1078 - z_393 - z_363 - z_313 - z_973 - z_258 - z_743 - z_703 <= -1 r_951: - z_998 - z_993 - z_988 - z_983 - z_978 - z_973 - z_968 - z_963 - z_958 - z_538 - z_1183 - z_1048 - z_263 - z_933 - z_853 - z_788 - z_748 - z_53 <= -1 r_952: - z_1023 - z_1018 - z_1013 - z_1008 - z_1003 - z_643 - z_403 - z_373 - z_173 - z_798 - z_108 <= -1 r_953: - z_1048 - z_1043 - z_1038 - z_1033 - z_1028 - z_598 - z_568 - z_543 - z_1193 - z_473 - z_1098 - z_983 - z_178 - z_118 - z_708 - z_18 <= -1 r_954: - z_1113 - z_1108 - z_1103 - z_1098 - z_1093 - z_1088 - z_1083 - z_1078 - z_1073 - z_1068 - z_1063 - z_1058 - z_1053 - z_653 - z_513 - z_413 - z_323 - z_988 - z_908 - z_188 - z_858 - z_813 - z_123 - z_763 - z_63 <= -1 r_955: - z_1153 - z_1148 - z_1143 - z_1138 - z_1133 - z_1128 - z_1123 - z_1118 - z_658 - z_603 - z_548 - z_328 - z_278 - z_943 - z_863 <= -1 r_956: - z_1213 - z_1208 - z_1203 - z_1198 - z_1193 - z_1188 - z_1183 - z_1178 - z_1173 - z_1168 - z_1163 - z_1158 - z_578 - z_518 - z_333 - z_948 - z_193 - z_823 - z_768 - z_718 <= -1 r_957: - x_1273 + 28 z_3 + x_1272 <= 27 r_958: - x_1274 + 28 z_8 + x_1272 <= 27 r_959: - x_1275 + 25 z_233 + 27 z_13 + x_1272 <= 26 r_960: - x_1276 + 28 z_18 + x_1272 <= 27 r_961: - x_1277 + 28 z_23 + x_1272 <= 27 r_962: - x_1278 + 25 z_623 + 27 z_28 + x_1272 <= 26 r_963: - x_1280 + 28 z_33 + x_1279 <= 27 r_964: - x_1281 + 28 z_38 + x_1279 <= 27 r_965: - x_1282 + 28 z_43 + x_1279 <= 27 r_966: - x_1274 + 28 z_48 + x_1279 <= 27 r_967: - x_1283 + 28 z_53 + x_1279 <= 27 r_968: - x_1284 + 28 z_58 + x_1279 <= 27 r_969: - x_1285 + 25 z_1058 + 27 z_63 + x_1279 <= 26 r_970: - x_1286 + 28 z_68 + x_1279 <= 27 r_971: - x_1287 + 28 z_73 + x_1279 <= 27 r_972: - x_1280 + 25 z_683 + 27 z_78 + x_1281 <= 26 r_973: - x_1288 + 25 z_728 + 27 z_83 + x_1281 <= 26 r_974: - x_1273 + 28 z_88 + x_1281 <= 27 r_975: - x_1289 + 28 z_93 + x_1281 <= 27 r_976: - x_1274 + 28 z_98 + x_1281 <= 27 r_977: - x_1284 + 28 z_103 + x_1281 <= 27 r_978: - x_1290 + 28 z_108 + x_1281 <= 27 r_979: - x_1291 + 25 z_343 + 27 z_113 + x_1281 <= 26 r_980: - x_1276 + 28 z_118 + x_1281 <= 27 r_981: - x_1285 + 28 z_123 + x_1281 <= 27 r_982: - x_1286 + 25 z_438 + 27 z_128 + x_1281 <= 26 r_983: - x_1287 + 28 z_133 + x_1281 <= 27 r_984: - x_1274 + 28 z_138 + x_1273 <= 27 r_985: - x_1292 + 28 z_143 + x_1273 <= 27 r_986: - x_1284 + 28 z_148 + x_1273 <= 27 r_987: - x_1293 + 25 z_383 + 27 z_153 + x_1273 <= 26 r_988: - x_1294 + 28 z_158 + x_1273 <= 27 r_989: - x_1295 + 28 z_163 + x_1273 <= 27 r_990: - x_1289 + 25 z_843 + 27 z_168 + x_1274 <= 26 r_991: - x_1290 + 25 z_1013 + 27 z_173 + x_1274 <= 26 r_992: - x_1276 + 25 z_1038 + 27 z_178 + x_1274 <= 26 r_993: - x_1293 + 25 z_388 + 27 z_183 + x_1274 <= 26 r_994: - x_1285 + 28 z_188 + x_1274 <= 27 r_995: - x_1296 + 25 z_1168 + 27 z_193 + x_1274 <= 26 r_996: - x_1294 + 25 z_533 + 27 z_198 + x_1274 <= 26 r_997: - x_1279 + 28 z_203 + x_1292 <= 27 r_998: - x_1289 + 28 z_208 + x_1292 <= 27 r_999: - x_1274 + 28 z_213 + x_1292 <= 27 r_1000: - x_1275 + 25 z_253 + 27 z_218 + x_1292 <= 26 r_1001: - x_1293 + 28 z_223 + x_1292 <= 27 r_1002: - x_1294 + 28 z_228 + x_1292 <= 27 r_1003: - x_1272 + 25 z_13 + 27 z_233 + x_1275 <= 26 r_1004: - x_1288 + 28 z_238 + x_1275 <= 27 r_1005: - x_1281 + 28 z_243 + x_1275 <= 27 r_1006: - x_1289 + 25 z_848 + 27 z_248 + x_1275 <= 26 r_1007: - x_1292 + 25 z_218 + 27 z_253 + x_1275 <= 26 r_1008: - x_1297 + 28 z_258 + x_1275 <= 27 r_1009: - x_1283 + 28 z_263 + x_1275 <= 27 r_1010: - x_1284 + 25 z_318 + 27 z_268 + x_1275 <= 26 r_1011: - x_1293 + 28 z_273 + x_1275 <= 27 r_1012: - x_1298 + 28 z_278 + x_1275 <= 27 r_1013: - x_1287 + 28 z_283 + x_1275 <= 27 r_1014: - x_1295 + 28 z_288 + x_1275 <= 27 r_1015: - x_1280 + 28 z_293 + x_1284 <= 27 r_1016: - x_1282 + 25 z_793 + 27 z_298 + x_1284 <= 26 r_1017: - x_1274 + 28 z_303 + x_1284 <= 27 r_1018: - x_1292 + 28 z_308 + x_1284 <= 27 r_1019: - x_1297 + 25 z_938 + 27 z_313 + x_1284 <= 26 r_1020: - x_1275 + 25 z_268 + 27 z_318 + x_1284 <= 26 r_1021: - x_1285 + 25 z_1088 + 27 z_323 + x_1284 <= 26 r_1022: - x_1298 + 25 z_1138 + 27 z_328 + x_1284 <= 26 r_1023: - x_1296 + 25 z_1188 + 27 z_333 + x_1284 <= 26 r_1024: - x_1279 + 28 z_338 + x_1291 <= 27 r_1025: - x_1281 + 25 z_113 + 27 z_343 + x_1291 <= 26 r_1026: - x_1282 + 25 z_803 + 27 z_348 + x_1291 <= 26 r_1027: - x_1274 + 28 z_353 + x_1291 <= 27 r_1028: - x_1299 + 25 z_898 + 27 z_358 + x_1291 <= 26 r_1029: - x_1297 + 28 z_363 + x_1291 <= 27 r_1030: - x_1275 + 28 z_368 + x_1291 <= 27 r_1031: - x_1290 + 28 z_373 + x_1291 <= 27 r_1032: - x_1282 + 25 z_808 + 27 z_378 + x_1293 <= 26 r_1033: - x_1273 + 25 z_153 + 27 z_383 + x_1293 <= 26 r_1034: - x_1274 + 25 z_183 + 27 z_388 + x_1293 <= 26 r_1035: - x_1297 + 28 z_393 + x_1293 <= 27 r_1036: - x_1284 + 28 z_398 + x_1293 <= 27 r_1037: - x_1290 + 28 z_403 + x_1293 <= 27 r_1038: - x_1291 + 28 z_408 + x_1293 <= 27 r_1039: - x_1285 + 25 z_1103 + 27 z_413 + x_1293 <= 26 r_1040: - x_1286 + 28 z_418 + x_1293 <= 27 r_1041: - x_1278 + 25 z_648 + 27 z_423 + x_1293 <= 26 r_1042: - x_1280 + 28 z_428 + x_1286 <= 27 r_1043: - x_1288 + 28 z_433 + x_1286 <= 27 r_1044: - x_1281 + 25 z_128 + 27 z_438 + x_1286 <= 26 r_1045: - x_1273 + 28 z_443 + x_1286 <= 27 r_1046: - x_1274 + 28 z_448 + x_1286 <= 27 r_1047: - x_1297 + 28 z_453 + x_1286 <= 27 r_1048: - x_1275 + 28 z_458 + x_1286 <= 27 r_1049: - x_1284 + 28 z_463 + x_1286 <= 27 r_1050: - x_1291 + 28 z_468 + x_1286 <= 27 r_1051: - x_1276 + 28 z_473 + x_1286 <= 27 r_1052: - x_1287 + 28 z_478 + x_1286 <= 27 r_1053: - x_1277 + 25 z_573 + 27 z_483 + x_1286 <= 26 r_1054: - x_1295 + 28 z_488 + x_1286 <= 27 r_1055: - x_1272 + 28 z_493 + x_1287 <= 27 r_1056: - x_1274 + 28 z_498 + x_1287 <= 27 r_1057: - x_1299 + 28 z_503 + x_1287 <= 27 r_1058: - x_1292 + 28 z_508 + x_1287 <= 27 r_1059: - x_1285 + 28 z_513 + x_1287 <= 27 r_1060: - x_1296 + 25 z_1208 + 27 z_518 + x_1287 <= 26 r_1061: - x_1278 + 28 z_523 + x_1287 <= 27 r_1062: - x_1280 + 28 z_528 + x_1294 <= 27 r_1063: - x_1274 + 25 z_198 + 27 z_533 + x_1294 <= 26 r_1064: - x_1283 + 25 z_998 + 27 z_538 + x_1294 <= 26 r_1065: - x_1276 + 28 z_543 + x_1294 <= 27 r_1066: - x_1298 + 28 z_548 + x_1294 <= 27 r_1067: - x_1287 + 28 z_553 + x_1294 <= 27 r_1068: - x_1282 + 28 z_558 + x_1277 <= 27 r_1069: - x_1297 + 28 z_563 + x_1277 <= 27 r_1070: - x_1276 + 28 z_568 + x_1277 <= 27 r_1071: - x_1286 + 25 z_483 + 27 z_573 + x_1277 <= 26 r_1072: - x_1296 + 28 z_578 + x_1277 <= 27 r_1073: - x_1272 + 28 z_583 + x_1295 <= 27 r_1074: - x_1280 + 28 z_588 + x_1295 <= 27 r_1075: - x_1299 + 28 z_593 + x_1295 <= 27 r_1076: - x_1276 + 28 z_598 + x_1295 <= 27 r_1077: - x_1298 + 25 z_1153 + 27 z_603 + x_1295 <= 26 r_1078: - x_1287 + 28 z_608 + x_1295 <= 27 r_1079: - x_1294 + 28 z_613 + x_1295 <= 27 r_1080: - x_1277 + 28 z_618 + x_1295 <= 27 r_1081: - x_1272 + 25 z_28 + 27 z_623 + x_1278 <= 26 r_1082: - x_1274 + 28 z_628 + x_1278 <= 27 r_1083: - x_1299 + 28 z_633 + x_1278 <= 27 r_1084: - x_1284 + 28 z_638 + x_1278 <= 27 r_1085: - x_1290 + 25 z_1023 + 27 z_643 + x_1278 <= 26 r_1086: - x_1293 + 25 z_423 + 27 z_648 + x_1278 <= 26 r_1087: - x_1285 + 25 z_1113 + 27 z_653 + x_1278 <= 26 r_1088: - x_1298 + 28 z_658 + x_1278 <= 27 r_1089: - x_1294 + 28 z_663 + x_1278 <= 27 r_1090: - x_1277 + 28 z_668 + x_1278 <= 27 r_1091: - x_1295 + 28 z_673 + x_1278 <= 27 r_1092: - x_1272 + 28 z_678 + x_1280 <= 27 r_1093: - x_1281 + 25 z_78 + 27 z_683 + x_1280 <= 26 r_1094: - x_1289 + 28 z_688 + x_1280 <= 27 r_1095: - x_1299 + 28 z_693 + x_1280 <= 27 r_1096: - x_1292 + 28 z_698 + x_1280 <= 27 r_1097: - x_1297 + 25 z_923 + 27 z_703 + x_1280 <= 26 r_1098: - x_1276 + 28 z_708 + x_1280 <= 27 r_1099: - x_1287 + 28 z_713 + x_1280 <= 27 r_1100: - x_1296 + 28 z_718 + x_1280 <= 27 r_1101: - x_1277 + 28 z_723 + x_1280 <= 27 r_1102: - x_1281 + 25 z_83 + 27 z_728 + x_1288 <= 26 r_1103: - x_1289 + 28 z_733 + x_1288 <= 27 r_1104: - x_1274 + 28 z_738 + x_1288 <= 27 r_1105: - x_1297 + 28 z_743 + x_1288 <= 27 r_1106: - x_1283 + 25 z_958 + 27 z_748 + x_1288 <= 26 r_1107: - x_1291 + 28 z_753 + x_1288 <= 27 r_1108: - x_1293 + 28 z_758 + x_1288 <= 27 r_1109: - x_1285 + 25 z_1063 + 27 z_763 + x_1288 <= 26 r_1110: - x_1296 + 28 z_768 + x_1288 <= 27 r_1111: - x_1278 + 28 z_773 + x_1288 <= 27 r_1112: - x_1288 + 28 z_778 + x_1282 <= 27 r_1113: - x_1299 + 28 z_783 + x_1282 <= 27 r_1114: - x_1283 + 28 z_788 + x_1282 <= 27 r_1115: - x_1284 + 25 z_298 + 27 z_793 + x_1282 <= 26 r_1116: - x_1290 + 28 z_798 + x_1282 <= 27 r_1117: - x_1291 + 25 z_348 + 27 z_803 + x_1282 <= 26 r_1118: - x_1293 + 25 z_378 + 27 z_808 + x_1282 <= 26 r_1119: - x_1285 + 28 z_813 + x_1282 <= 27 r_1120: - x_1287 + 28 z_818 + x_1282 <= 27 r_1121: - x_1296 + 28 z_823 + x_1282 <= 27 r_1122: - x_1294 + 28 z_828 + x_1282 <= 27 r_1123: - x_1295 + 28 z_833 + x_1282 <= 27 r_1124: - x_1279 + 28 z_838 + x_1289 <= 27 r_1125: - x_1274 + 25 z_168 + 27 z_843 + x_1289 <= 26 r_1126: - x_1275 + 25 z_248 + 27 z_848 + x_1289 <= 26 r_1127: - x_1283 + 28 z_853 + x_1289 <= 27 r_1128: - x_1285 + 28 z_858 + x_1289 <= 27 r_1129: - x_1298 + 28 z_863 + x_1289 <= 27 r_1130: - x_1277 + 28 z_868 + x_1289 <= 27 r_1131: - x_1278 + 28 z_873 + x_1289 <= 27 r_1132: - x_1272 + 28 z_878 + x_1299 <= 27 r_1133: - x_1279 + 28 z_883 + x_1299 <= 27 r_1134: - x_1273 + 28 z_888 + x_1299 <= 27 r_1135: - x_1275 + 28 z_893 + x_1299 <= 27 r_1136: - x_1291 + 25 z_358 + 27 z_898 + x_1299 <= 26 r_1137: - x_1293 + 28 z_903 + x_1299 <= 27 r_1138: - x_1285 + 25 z_1068 + 27 z_908 + x_1299 <= 26 r_1139: - x_1286 + 28 z_913 + x_1299 <= 27 r_1140: - x_1272 + 28 z_918 + x_1297 <= 27 r_1141: - x_1280 + 25 z_703 + 27 z_923 + x_1297 <= 26 r_1142: - x_1299 + 28 z_928 + x_1297 <= 27 r_1143: - x_1283 + 25 z_973 + 27 z_933 + x_1297 <= 26 r_1144: - x_1284 + 25 z_313 + 27 z_938 + x_1297 <= 26 r_1145: - x_1298 + 28 z_943 + x_1297 <= 27 r_1146: - x_1296 + 25 z_1173 + 27 z_948 + x_1297 <= 26 r_1147: - x_1278 + 28 z_953 + x_1297 <= 27 r_1148: - x_1288 + 25 z_748 + 27 z_958 + x_1283 <= 26 r_1149: - x_1281 + 28 z_963 + x_1283 <= 27 r_1150: - x_1273 + 28 z_968 + x_1283 <= 27 r_1151: - x_1297 + 25 z_933 + 27 z_973 + x_1283 <= 26 r_1152: - x_1291 + 28 z_978 + x_1283 <= 27 r_1153: - x_1276 + 25 z_1048 + 27 z_983 + x_1283 <= 26 r_1154: - x_1285 + 28 z_988 + x_1283 <= 27 r_1155: - x_1287 + 28 z_993 + x_1283 <= 27 r_1156: - x_1294 + 25 z_538 + 27 z_998 + x_1283 <= 26 r_1157: - x_1273 + 28 z_1003 + x_1290 <= 27 r_1158: - x_1289 + 28 z_1008 + x_1290 <= 27 r_1159: - x_1274 + 25 z_173 + 27 z_1013 + x_1290 <= 26 r_1160: - x_1295 + 28 z_1018 + x_1290 <= 27 r_1161: - x_1278 + 25 z_643 + 27 z_1023 + x_1290 <= 26 r_1162: - x_1279 + 28 z_1028 + x_1276 <= 27 r_1163: - x_1289 + 28 z_1033 + x_1276 <= 27 r_1164: - x_1274 + 25 z_178 + 27 z_1038 + x_1276 <= 26 r_1165: - x_1299 + 28 z_1043 + x_1276 <= 27 r_1166: - x_1283 + 25 z_983 + 27 z_1048 + x_1276 <= 26 r_1167: - x_1272 + 28 z_1053 + x_1285 <= 27 r_1168: - x_1279 + 25 z_63 + 27 z_1058 + x_1285 <= 26 r_1169: - x_1288 + 25 z_763 + 27 z_1063 + x_1285 <= 26 r_1170: - x_1299 + 25 z_908 + 27 z_1068 + x_1285 <= 26 r_1171: - x_1292 + 28 z_1073 + x_1285 <= 27 r_1172: - x_1297 + 28 z_1078 + x_1285 <= 27 r_1173: - x_1275 + 28 z_1083 + x_1285 <= 27 r_1174: - x_1284 + 25 z_323 + 27 z_1088 + x_1285 <= 26 r_1175: - x_1291 + 28 z_1093 + x_1285 <= 27 r_1176: - x_1276 + 28 z_1098 + x_1285 <= 27 r_1177: - x_1293 + 25 z_413 + 27 z_1103 + x_1285 <= 26 r_1178: - x_1295 + 28 z_1108 + x_1285 <= 27 r_1179: - x_1278 + 25 z_653 + 27 z_1113 + x_1285 <= 26 r_1180: - x_1272 + 28 z_1118 + x_1298 <= 27 r_1181: - x_1281 + 28 z_1123 + x_1298 <= 27 r_1182: - x_1299 + 28 z_1128 + x_1298 <= 27 r_1183: - x_1292 + 28 z_1133 + x_1298 <= 27 r_1184: - x_1284 + 25 z_328 + 27 z_1138 + x_1298 <= 26 r_1185: - x_1293 + 28 z_1143 + x_1298 <= 27 r_1186: - x_1277 + 28 z_1148 + x_1298 <= 27 r_1187: - x_1295 + 25 z_603 + 27 z_1153 + x_1298 <= 26 r_1188: - x_1281 + 28 z_1158 + x_1296 <= 27 r_1189: - x_1289 + 28 z_1163 + x_1296 <= 27 r_1190: - x_1274 + 25 z_193 + 27 z_1168 + x_1296 <= 26 r_1191: - x_1297 + 25 z_948 + 27 z_1173 + x_1296 <= 26 r_1192: - x_1275 + 28 z_1178 + x_1296 <= 27 r_1193: - x_1283 + 28 z_1183 + x_1296 <= 27 r_1194: - x_1284 + 25 z_333 + 27 z_1188 + x_1296 <= 26 r_1195: - x_1276 + 28 z_1193 + x_1296 <= 27 r_1196: - x_1293 + 28 z_1198 + x_1296 <= 27 r_1197: - x_1286 + 28 z_1203 + x_1296 <= 27 r_1198: - x_1287 + 25 z_518 + 27 z_1208 + x_1296 <= 26 r_1199: - x_1278 + 28 z_1213 + x_1296 <= 27 r_1200: 0 z_1 <= 0 r_1201: - x_1279 + x_1272 <= -2 r_1202: - x_1281 + x_1272 <= -2 r_1203: - x_1273 + x_1272 <= -1 r_1204: - x_1274 + x_1272 <= -1 r_1205: - x_1292 + x_1272 <= -2 r_1206: - x_1275 + x_1272 <= -1 r_1207: - x_1284 + x_1272 <= -2 r_1208: - x_1291 + x_1272 <= -3 r_1209: - x_1293 + x_1272 <= -2 r_1210: - x_1286 + x_1272 <= -2 r_1211: - x_1287 + x_1272 <= -2 r_1212: - x_1294 + x_1272 <= -2 r_1213: - x_1277 + x_1272 <= -1 r_1214: - x_1295 + x_1272 <= -2 r_1215: - x_1278 + x_1272 <= -1 r_1216: - x_1280 + x_1272 <= -3 r_1217: - x_1288 + x_1272 <= -2 r_1218: - x_1282 + x_1272 <= -2 r_1219: - x_1289 + x_1272 <= -2 r_1220: - x_1299 + x_1272 <= -2 r_1221: - x_1297 + x_1272 <= -2 r_1222: - x_1283 + x_1272 <= -2 r_1223: - x_1290 + x_1272 <= -2 r_1224: - x_1276 + x_1272 <= -1 r_1225: - x_1285 + x_1272 <= -2 r_1226: - x_1298 + x_1272 <= -2 r_1227: - x_1296 + x_1272 <= -2 r_1228: + z_1214 + z_1209 + z_1204 + z_1199 + z_1194 + z_1189 + z_1184 + z_1179 + z_1174 + z_1169 + z_1164 + z_1159 + z_1154 + z_1149 + z_1144 + z_1139 + z_1134 + z_1129 + z_1124 + z_1119 + z_1114 + z_1109 + z_1104 + z_1099 + z_1094 + z_1089 + z_1084 + z_1079 + z_1074 + z_1069 + z_1064 + z_1059 + z_1054 + z_1049 + z_1044 + z_1039 + z_1034 + z_1029 + z_1024 + z_1019 + z_1014 + z_1009 + z_1004 + z_999 + z_994 + z_989 + z_984 + z_979 + z_974 + z_969 + z_964 + z_959 + z_954 + z_949 + z_944 + z_939 + z_934 + z_929 + z_924 + z_919 + z_914 + z_909 + z_904 + z_899 + z_894 + z_889 + z_884 + z_879 + z_874 + z_869 + z_864 + z_859 + z_854 + z_849 + z_844 + z_839 + z_834 + z_829 + z_824 + z_819 + z_814 + z_809 + z_804 + z_799 + z_794 + z_789 + z_784 + z_779 + z_774 + z_769 + z_764 + z_759 + z_754 + z_749 + z_744 + z_739 + z_734 + z_729 + z_724 + z_719 + z_714 + z_709 + z_704 + z_699 + z_694 + z_689 + z_684 + z_679 + z_674 + z_669 + z_664 + z_659 + z_654 + z_649 + z_644 + z_639 + z_634 + z_629 + z_624 + z_619 + z_614 + z_609 + z_604 + z_599 + z_594 + z_589 + z_584 + z_579 + z_574 + z_569 + z_564 + z_559 + z_554 + z_549 + z_544 + z_539 + z_534 + z_529 + z_524 + z_519 + z_514 + z_509 + z_504 + z_499 + z_494 + z_489 + z_484 + z_479 + z_474 + z_469 + z_464 + z_459 + z_454 + z_449 + z_444 + z_439 + z_434 + z_429 + z_424 + z_419 + z_414 + z_409 + z_404 + z_399 + z_394 + z_389 + z_384 + z_379 + z_374 + z_369 + z_364 + z_359 + z_354 + z_349 + z_344 + z_339 + z_334 + z_329 + z_324 + z_319 + z_314 + z_309 + z_304 + z_299 + z_294 + z_289 + z_284 + z_279 + z_274 + z_269 + z_264 + z_259 + z_254 + z_249 + z_244 + z_239 + z_234 + z_229 + z_224 + z_219 + z_214 + z_209 + z_204 + z_199 + z_194 + z_189 + z_184 + z_179 + z_174 + z_169 + z_164 + z_159 + z_154 + z_149 + z_144 + z_139 + z_134 + z_129 + z_124 + z_119 + z_114 + z_109 + z_104 + z_99 + z_94 + z_89 + z_84 + z_79 + z_74 + z_69 + z_64 + z_59 + z_54 + z_49 + z_44 + z_39 + z_34 + z_29 + z_24 + z_19 + z_14 + z_9 + z_4 = 27 r_1229: + z_624 + z_584 + z_494 + z_1119 + z_1054 + z_234 + z_919 + z_879 + z_679 = 0 r_1230: + z_1059 + z_1029 + z_339 + z_204 + z_884 + z_839 = 1 r_1231: + z_1159 + z_1124 + z_439 + z_344 + z_964 + z_244 + z_729 + z_39 + z_684 = 1 r_1232: + z_444 + z_384 + z_1004 + z_969 + z_889 + z_89 + z_4 = 1 r_1233: + z_629 + z_534 + z_1169 + z_499 + z_449 + z_389 + z_1039 + z_354 + z_1014 + z_304 + z_214 + z_844 + z_139 + z_99 + z_739 + z_49 + z_9 = 1 r_1234: + z_509 + z_1134 + z_1074 + z_309 + z_254 + z_144 + z_699 = 1 r_1235: + z_1179 + z_459 + z_1084 + z_369 + z_319 + z_219 + z_894 + z_849 + z_14 = 1 r_1236: + z_639 + z_1189 + z_1139 + z_464 + z_1089 + z_399 + z_269 + z_939 + z_149 + z_794 + z_104 + z_59 = 1 r_1237: + z_469 + z_1094 + z_409 + z_979 + z_899 + z_804 + z_114 + z_754 = 1 r_1238: + z_649 + z_1199 + z_1144 + z_1104 + z_274 + z_224 + z_904 + z_184 + z_154 + z_809 + z_759 = 1 r_1239: + z_574 + z_1204 + z_419 + z_914 + z_129 + z_69 = 1 r_1240: + z_609 + z_554 + z_1209 + z_479 + z_994 + z_284 + z_819 + z_134 + z_74 + z_714 = 1 r_1241: + z_664 + z_614 + z_999 + z_229 + z_199 + z_159 + z_829 = 1 r_1242: + z_669 + z_619 + z_1149 + z_484 + z_869 + z_724 + z_24 = 1 r_1243: + z_674 + z_1154 + z_489 + z_1109 + z_1019 + z_289 + z_164 + z_834 = 1 r_1244: + z_1214 + z_524 + z_1114 + z_424 + z_1024 + z_954 + z_874 + z_774 + z_29 = 1 r_1245: + z_589 + z_529 + z_429 + z_294 + z_924 + z_79 + z_34 = 1 r_1246: + z_434 + z_1064 + z_959 + z_239 + z_779 + z_84 = 1 r_1247: + z_559 + z_379 + z_349 + z_299 + z_44 = 1 r_1248: + z_1164 + z_1034 + z_1009 + z_249 + z_209 + z_169 + z_94 + z_734 + z_689 = 1 r_1249: + z_634 + z_594 + z_504 + z_1129 + z_1069 + z_1044 + z_359 + z_929 + z_784 + z_694 = 1 r_1250: + z_564 + z_1174 + z_454 + z_1079 + z_394 + z_364 + z_314 + z_974 + z_259 + z_744 + z_704 = 1 r_1251: + z_539 + z_1184 + z_1049 + z_264 + z_934 + z_854 + z_789 + z_749 + z_54 = 1 r_1252: + z_644 + z_404 + z_374 + z_174 + z_799 + z_109 = 1 r_1253: + z_599 + z_569 + z_544 + z_1194 + z_474 + z_1099 + z_984 + z_179 + z_119 + z_709 + z_19 = 1 r_1254: + z_654 + z_514 + z_414 + z_324 + z_989 + z_909 + z_189 + z_859 + z_814 + z_124 + z_764 + z_64 = 1 r_1255: + z_659 + z_604 + z_549 + z_329 + z_279 + z_944 + z_864 = 1 r_1256: + z_579 + z_519 + z_334 + z_949 + z_194 + z_824 + z_769 + z_719 = 1 r_1257: - z_29 - z_24 - z_19 - z_14 - z_9 - z_4 - z_624 - z_584 - z_494 - z_1119 - z_1054 - z_234 - z_919 - z_879 - z_679 <= -1 r_1258: - z_74 - z_69 - z_64 - z_59 - z_54 - z_49 - z_44 - z_39 - z_34 - z_1059 - z_1029 - z_339 - z_204 - z_884 - z_839 <= -1 r_1259: - z_134 - z_129 - z_124 - z_119 - z_114 - z_109 - z_104 - z_99 - z_94 - z_89 - z_84 - z_79 - z_1159 - z_1124 - z_439 - z_344 - z_964 - z_244 - z_729 - z_39 - z_684 <= -1 r_1260: - z_164 - z_159 - z_154 - z_149 - z_144 - z_139 - z_444 - z_384 - z_1004 - z_969 - z_889 - z_89 - z_4 <= -1 r_1261: - z_199 - z_194 - z_189 - z_184 - z_179 - z_174 - z_169 - z_629 - z_534 - z_1169 - z_499 - z_449 - z_389 - z_1039 - z_354 - z_1014 - z_304 - z_214 - z_844 - z_139 - z_99 - z_739 - z_49 - z_9 <= -1 r_1262: - z_229 - z_224 - z_219 - z_214 - z_209 - z_204 - z_509 - z_1134 - z_1074 - z_309 - z_254 - z_144 - z_699 <= -1 r_1263: - z_289 - z_284 - z_279 - z_274 - z_269 - z_264 - z_259 - z_254 - z_249 - z_244 - z_239 - z_234 - z_1179 - z_459 - z_1084 - z_369 - z_319 - z_219 - z_894 - z_849 - z_14 <= -1 r_1264: - z_334 - z_329 - z_324 - z_319 - z_314 - z_309 - z_304 - z_299 - z_294 - z_639 - z_1189 - z_1139 - z_464 - z_1089 - z_399 - z_269 - z_939 - z_149 - z_794 - z_104 - z_59 <= -1 r_1265: - z_374 - z_369 - z_364 - z_359 - z_354 - z_349 - z_344 - z_339 - z_469 - z_1094 - z_409 - z_979 - z_899 - z_804 - z_114 - z_754 <= -1 r_1266: - z_424 - z_419 - z_414 - z_409 - z_404 - z_399 - z_394 - z_389 - z_384 - z_379 - z_649 - z_1199 - z_1144 - z_1104 - z_274 - z_224 - z_904 - z_184 - z_154 - z_809 - z_759 <= -1 r_1267: - z_489 - z_484 - z_479 - z_474 - z_469 - z_464 - z_459 - z_454 - z_449 - z_444 - z_439 - z_434 - z_429 - z_574 - z_1204 - z_419 - z_914 - z_129 - z_69 <= -1 r_1268: - z_524 - z_519 - z_514 - z_509 - z_504 - z_499 - z_494 - z_609 - z_554 - z_1209 - z_479 - z_994 - z_284 - z_819 - z_134 - z_74 - z_714 <= -1 r_1269: - z_554 - z_549 - z_544 - z_539 - z_534 - z_529 - z_664 - z_614 - z_999 - z_229 - z_199 - z_159 - z_829 <= -1 r_1270: - z_579 - z_574 - z_569 - z_564 - z_559 - z_669 - z_619 - z_1149 - z_484 - z_869 - z_724 - z_24 <= -1 r_1271: - z_619 - z_614 - z_609 - z_604 - z_599 - z_594 - z_589 - z_584 - z_674 - z_1154 - z_489 - z_1109 - z_1019 - z_289 - z_164 - z_834 <= -1 r_1272: - z_674 - z_669 - z_664 - z_659 - z_654 - z_649 - z_644 - z_639 - z_634 - z_629 - z_624 - z_1214 - z_524 - z_1114 - z_424 - z_1024 - z_954 - z_874 - z_774 - z_29 <= -1 r_1273: - z_724 - z_719 - z_714 - z_709 - z_704 - z_699 - z_694 - z_689 - z_684 - z_679 - z_589 - z_529 - z_429 - z_294 - z_924 - z_79 - z_34 <= -1 r_1274: - z_774 - z_769 - z_764 - z_759 - z_754 - z_749 - z_744 - z_739 - z_734 - z_729 - z_434 - z_1064 - z_959 - z_239 - z_779 - z_84 <= -1 r_1275: - z_834 - z_829 - z_824 - z_819 - z_814 - z_809 - z_804 - z_799 - z_794 - z_789 - z_784 - z_779 - z_559 - z_379 - z_349 - z_299 - z_44 <= -1 r_1276: - z_874 - z_869 - z_864 - z_859 - z_854 - z_849 - z_844 - z_839 - z_1164 - z_1034 - z_1009 - z_249 - z_209 - z_169 - z_94 - z_734 - z_689 <= -1 r_1277: - z_914 - z_909 - z_904 - z_899 - z_894 - z_889 - z_884 - z_879 - z_634 - z_594 - z_504 - z_1129 - z_1069 - z_1044 - z_359 - z_929 - z_784 - z_694 <= -1 r_1278: - z_954 - z_949 - z_944 - z_939 - z_934 - z_929 - z_924 - z_919 - z_564 - z_1174 - z_454 - z_1079 - z_394 - z_364 - z_314 - z_974 - z_259 - z_744 - z_704 <= -1 r_1279: - z_999 - z_994 - z_989 - z_984 - z_979 - z_974 - z_969 - z_964 - z_959 - z_539 - z_1184 - z_1049 - z_264 - z_934 - z_854 - z_789 - z_749 - z_54 <= -1 r_1280: - z_1024 - z_1019 - z_1014 - z_1009 - z_1004 - z_644 - z_404 - z_374 - z_174 - z_799 - z_109 <= -1 r_1281: - z_1049 - z_1044 - z_1039 - z_1034 - z_1029 - z_599 - z_569 - z_544 - z_1194 - z_474 - z_1099 - z_984 - z_179 - z_119 - z_709 - z_19 <= -1 r_1282: - z_1114 - z_1109 - z_1104 - z_1099 - z_1094 - z_1089 - z_1084 - z_1079 - z_1074 - z_1069 - z_1064 - z_1059 - z_1054 - z_654 - z_514 - z_414 - z_324 - z_989 - z_909 - z_189 - z_859 - z_814 - z_124 - z_764 - z_64 <= -1 r_1283: - z_1154 - z_1149 - z_1144 - z_1139 - z_1134 - z_1129 - z_1124 - z_1119 - z_659 - z_604 - z_549 - z_329 - z_279 - z_944 - z_864 <= -1 r_1284: - z_1214 - z_1209 - z_1204 - z_1199 - z_1194 - z_1189 - z_1184 - z_1179 - z_1174 - z_1169 - z_1164 - z_1159 - z_579 - z_519 - z_334 - z_949 - z_194 - z_824 - z_769 - z_719 <= -1 r_1285: - x_1301 + 28 z_4 + x_1300 <= 27 r_1286: - x_1302 + 28 z_9 + x_1300 <= 27 r_1287: - x_1303 + 25 z_234 + 27 z_14 + x_1300 <= 26 r_1288: - x_1304 + 28 z_19 + x_1300 <= 27 r_1289: - x_1305 + 28 z_24 + x_1300 <= 27 r_1290: - x_1306 + 25 z_624 + 27 z_29 + x_1300 <= 26 r_1291: - x_1308 + 28 z_34 + x_1307 <= 27 r_1292: - x_1309 + 28 z_39 + x_1307 <= 27 r_1293: - x_1310 + 28 z_44 + x_1307 <= 27 r_1294: - x_1302 + 28 z_49 + x_1307 <= 27 r_1295: - x_1311 + 28 z_54 + x_1307 <= 27 r_1296: - x_1312 + 28 z_59 + x_1307 <= 27 r_1297: - x_1313 + 25 z_1059 + 27 z_64 + x_1307 <= 26 r_1298: - x_1314 + 28 z_69 + x_1307 <= 27 r_1299: - x_1315 + 28 z_74 + x_1307 <= 27 r_1300: - x_1308 + 25 z_684 + 27 z_79 + x_1309 <= 26 r_1301: - x_1316 + 25 z_729 + 27 z_84 + x_1309 <= 26 r_1302: - x_1301 + 28 z_89 + x_1309 <= 27 r_1303: - x_1317 + 28 z_94 + x_1309 <= 27 r_1304: - x_1302 + 28 z_99 + x_1309 <= 27 r_1305: - x_1312 + 28 z_104 + x_1309 <= 27 r_1306: - x_1318 + 28 z_109 + x_1309 <= 27 r_1307: - x_1319 + 25 z_344 + 27 z_114 + x_1309 <= 26 r_1308: - x_1304 + 28 z_119 + x_1309 <= 27 r_1309: - x_1313 + 28 z_124 + x_1309 <= 27 r_1310: - x_1314 + 25 z_439 + 27 z_129 + x_1309 <= 26 r_1311: - x_1315 + 28 z_134 + x_1309 <= 27 r_1312: - x_1302 + 28 z_139 + x_1301 <= 27 r_1313: - x_1320 + 28 z_144 + x_1301 <= 27 r_1314: - x_1312 + 28 z_149 + x_1301 <= 27 r_1315: - x_1321 + 25 z_384 + 27 z_154 + x_1301 <= 26 r_1316: - x_1322 + 28 z_159 + x_1301 <= 27 r_1317: - x_1323 + 28 z_164 + x_1301 <= 27 r_1318: - x_1317 + 25 z_844 + 27 z_169 + x_1302 <= 26 r_1319: - x_1318 + 25 z_1014 + 27 z_174 + x_1302 <= 26 r_1320: - x_1304 + 25 z_1039 + 27 z_179 + x_1302 <= 26 r_1321: - x_1321 + 25 z_389 + 27 z_184 + x_1302 <= 26 r_1322: - x_1313 + 28 z_189 + x_1302 <= 27 r_1323: - x_1324 + 25 z_1169 + 27 z_194 + x_1302 <= 26 r_1324: - x_1322 + 25 z_534 + 27 z_199 + x_1302 <= 26 r_1325: - x_1307 + 28 z_204 + x_1320 <= 27 r_1326: - x_1317 + 28 z_209 + x_1320 <= 27 r_1327: - x_1302 + 28 z_214 + x_1320 <= 27 r_1328: - x_1303 + 25 z_254 + 27 z_219 + x_1320 <= 26 r_1329: - x_1321 + 28 z_224 + x_1320 <= 27 r_1330: - x_1322 + 28 z_229 + x_1320 <= 27 r_1331: - x_1300 + 25 z_14 + 27 z_234 + x_1303 <= 26 r_1332: - x_1316 + 28 z_239 + x_1303 <= 27 r_1333: - x_1309 + 28 z_244 + x_1303 <= 27 r_1334: - x_1317 + 25 z_849 + 27 z_249 + x_1303 <= 26 r_1335: - x_1320 + 25 z_219 + 27 z_254 + x_1303 <= 26 r_1336: - x_1325 + 28 z_259 + x_1303 <= 27 r_1337: - x_1311 + 28 z_264 + x_1303 <= 27 r_1338: - x_1312 + 25 z_319 + 27 z_269 + x_1303 <= 26 r_1339: - x_1321 + 28 z_274 + x_1303 <= 27 r_1340: - x_1326 + 28 z_279 + x_1303 <= 27 r_1341: - x_1315 + 28 z_284 + x_1303 <= 27 r_1342: - x_1323 + 28 z_289 + x_1303 <= 27 r_1343: - x_1308 + 28 z_294 + x_1312 <= 27 r_1344: - x_1310 + 25 z_794 + 27 z_299 + x_1312 <= 26 r_1345: - x_1302 + 28 z_304 + x_1312 <= 27 r_1346: - x_1320 + 28 z_309 + x_1312 <= 27 r_1347: - x_1325 + 25 z_939 + 27 z_314 + x_1312 <= 26 r_1348: - x_1303 + 25 z_269 + 27 z_319 + x_1312 <= 26 r_1349: - x_1313 + 25 z_1089 + 27 z_324 + x_1312 <= 26 r_1350: - x_1326 + 25 z_1139 + 27 z_329 + x_1312 <= 26 r_1351: - x_1324 + 25 z_1189 + 27 z_334 + x_1312 <= 26 r_1352: - x_1307 + 28 z_339 + x_1319 <= 27 r_1353: - x_1309 + 25 z_114 + 27 z_344 + x_1319 <= 26 r_1354: - x_1310 + 25 z_804 + 27 z_349 + x_1319 <= 26 r_1355: - x_1302 + 28 z_354 + x_1319 <= 27 r_1356: - x_1327 + 25 z_899 + 27 z_359 + x_1319 <= 26 r_1357: - x_1325 + 28 z_364 + x_1319 <= 27 r_1358: - x_1303 + 28 z_369 + x_1319 <= 27 r_1359: - x_1318 + 28 z_374 + x_1319 <= 27 r_1360: - x_1310 + 25 z_809 + 27 z_379 + x_1321 <= 26 r_1361: - x_1301 + 25 z_154 + 27 z_384 + x_1321 <= 26 r_1362: - x_1302 + 25 z_184 + 27 z_389 + x_1321 <= 26 r_1363: - x_1325 + 28 z_394 + x_1321 <= 27 r_1364: - x_1312 + 28 z_399 + x_1321 <= 27 r_1365: - x_1318 + 28 z_404 + x_1321 <= 27 r_1366: - x_1319 + 28 z_409 + x_1321 <= 27 r_1367: - x_1313 + 25 z_1104 + 27 z_414 + x_1321 <= 26 r_1368: - x_1314 + 28 z_419 + x_1321 <= 27 r_1369: - x_1306 + 25 z_649 + 27 z_424 + x_1321 <= 26 r_1370: - x_1308 + 28 z_429 + x_1314 <= 27 r_1371: - x_1316 + 28 z_434 + x_1314 <= 27 r_1372: - x_1309 + 25 z_129 + 27 z_439 + x_1314 <= 26 r_1373: - x_1301 + 28 z_444 + x_1314 <= 27 r_1374: - x_1302 + 28 z_449 + x_1314 <= 27 r_1375: - x_1325 + 28 z_454 + x_1314 <= 27 r_1376: - x_1303 + 28 z_459 + x_1314 <= 27 r_1377: - x_1312 + 28 z_464 + x_1314 <= 27 r_1378: - x_1319 + 28 z_469 + x_1314 <= 27 r_1379: - x_1304 + 28 z_474 + x_1314 <= 27 r_1380: - x_1315 + 28 z_479 + x_1314 <= 27 r_1381: - x_1305 + 25 z_574 + 27 z_484 + x_1314 <= 26 r_1382: - x_1323 + 28 z_489 + x_1314 <= 27 r_1383: - x_1300 + 28 z_494 + x_1315 <= 27 r_1384: - x_1302 + 28 z_499 + x_1315 <= 27 r_1385: - x_1327 + 28 z_504 + x_1315 <= 27 r_1386: - x_1320 + 28 z_509 + x_1315 <= 27 r_1387: - x_1313 + 28 z_514 + x_1315 <= 27 r_1388: - x_1324 + 25 z_1209 + 27 z_519 + x_1315 <= 26 r_1389: - x_1306 + 28 z_524 + x_1315 <= 27 r_1390: - x_1308 + 28 z_529 + x_1322 <= 27 r_1391: - x_1302 + 25 z_199 + 27 z_534 + x_1322 <= 26 r_1392: - x_1311 + 25 z_999 + 27 z_539 + x_1322 <= 26 r_1393: - x_1304 + 28 z_544 + x_1322 <= 27 r_1394: - x_1326 + 28 z_549 + x_1322 <= 27 r_1395: - x_1315 + 28 z_554 + x_1322 <= 27 r_1396: - x_1310 + 28 z_559 + x_1305 <= 27 r_1397: - x_1325 + 28 z_564 + x_1305 <= 27 r_1398: - x_1304 + 28 z_569 + x_1305 <= 27 r_1399: - x_1314 + 25 z_484 + 27 z_574 + x_1305 <= 26 r_1400: - x_1324 + 28 z_579 + x_1305 <= 27 r_1401: - x_1300 + 28 z_584 + x_1323 <= 27 r_1402: - x_1308 + 28 z_589 + x_1323 <= 27 r_1403: - x_1327 + 28 z_594 + x_1323 <= 27 r_1404: - x_1304 + 28 z_599 + x_1323 <= 27 r_1405: - x_1326 + 25 z_1154 + 27 z_604 + x_1323 <= 26 r_1406: - x_1315 + 28 z_609 + x_1323 <= 27 r_1407: - x_1322 + 28 z_614 + x_1323 <= 27 r_1408: - x_1305 + 28 z_619 + x_1323 <= 27 r_1409: - x_1300 + 25 z_29 + 27 z_624 + x_1306 <= 26 r_1410: - x_1302 + 28 z_629 + x_1306 <= 27 r_1411: - x_1327 + 28 z_634 + x_1306 <= 27 r_1412: - x_1312 + 28 z_639 + x_1306 <= 27 r_1413: - x_1318 + 25 z_1024 + 27 z_644 + x_1306 <= 26 r_1414: - x_1321 + 25 z_424 + 27 z_649 + x_1306 <= 26 r_1415: - x_1313 + 25 z_1114 + 27 z_654 + x_1306 <= 26 r_1416: - x_1326 + 28 z_659 + x_1306 <= 27 r_1417: - x_1322 + 28 z_664 + x_1306 <= 27 r_1418: - x_1305 + 28 z_669 + x_1306 <= 27 r_1419: - x_1323 + 28 z_674 + x_1306 <= 27 r_1420: - x_1300 + 28 z_679 + x_1308 <= 27 r_1421: - x_1309 + 25 z_79 + 27 z_684 + x_1308 <= 26 r_1422: - x_1317 + 28 z_689 + x_1308 <= 27 r_1423: - x_1327 + 28 z_694 + x_1308 <= 27 r_1424: - x_1320 + 28 z_699 + x_1308 <= 27 r_1425: - x_1325 + 25 z_924 + 27 z_704 + x_1308 <= 26 r_1426: - x_1304 + 28 z_709 + x_1308 <= 27 r_1427: - x_1315 + 28 z_714 + x_1308 <= 27 r_1428: - x_1324 + 28 z_719 + x_1308 <= 27 r_1429: - x_1305 + 28 z_724 + x_1308 <= 27 r_1430: - x_1309 + 25 z_84 + 27 z_729 + x_1316 <= 26 r_1431: - x_1317 + 28 z_734 + x_1316 <= 27 r_1432: - x_1302 + 28 z_739 + x_1316 <= 27 r_1433: - x_1325 + 28 z_744 + x_1316 <= 27 r_1434: - x_1311 + 25 z_959 + 27 z_749 + x_1316 <= 26 r_1435: - x_1319 + 28 z_754 + x_1316 <= 27 r_1436: - x_1321 + 28 z_759 + x_1316 <= 27 r_1437: - x_1313 + 25 z_1064 + 27 z_764 + x_1316 <= 26 r_1438: - x_1324 + 28 z_769 + x_1316 <= 27 r_1439: - x_1306 + 28 z_774 + x_1316 <= 27 r_1440: - x_1316 + 28 z_779 + x_1310 <= 27 r_1441: - x_1327 + 28 z_784 + x_1310 <= 27 r_1442: - x_1311 + 28 z_789 + x_1310 <= 27 r_1443: - x_1312 + 25 z_299 + 27 z_794 + x_1310 <= 26 r_1444: - x_1318 + 28 z_799 + x_1310 <= 27 r_1445: - x_1319 + 25 z_349 + 27 z_804 + x_1310 <= 26 r_1446: - x_1321 + 25 z_379 + 27 z_809 + x_1310 <= 26 r_1447: - x_1313 + 28 z_814 + x_1310 <= 27 r_1448: - x_1315 + 28 z_819 + x_1310 <= 27 r_1449: - x_1324 + 28 z_824 + x_1310 <= 27 r_1450: - x_1322 + 28 z_829 + x_1310 <= 27 r_1451: - x_1323 + 28 z_834 + x_1310 <= 27 r_1452: - x_1307 + 28 z_839 + x_1317 <= 27 r_1453: - x_1302 + 25 z_169 + 27 z_844 + x_1317 <= 26 r_1454: - x_1303 + 25 z_249 + 27 z_849 + x_1317 <= 26 r_1455: - x_1311 + 28 z_854 + x_1317 <= 27 r_1456: - x_1313 + 28 z_859 + x_1317 <= 27 r_1457: - x_1326 + 28 z_864 + x_1317 <= 27 r_1458: - x_1305 + 28 z_869 + x_1317 <= 27 r_1459: - x_1306 + 28 z_874 + x_1317 <= 27 r_1460: - x_1300 + 28 z_879 + x_1327 <= 27 r_1461: - x_1307 + 28 z_884 + x_1327 <= 27 r_1462: - x_1301 + 28 z_889 + x_1327 <= 27 r_1463: - x_1303 + 28 z_894 + x_1327 <= 27 r_1464: - x_1319 + 25 z_359 + 27 z_899 + x_1327 <= 26 r_1465: - x_1321 + 28 z_904 + x_1327 <= 27 r_1466: - x_1313 + 25 z_1069 + 27 z_909 + x_1327 <= 26 r_1467: - x_1314 + 28 z_914 + x_1327 <= 27 r_1468: - x_1300 + 28 z_919 + x_1325 <= 27 r_1469: - x_1308 + 25 z_704 + 27 z_924 + x_1325 <= 26 r_1470: - x_1327 + 28 z_929 + x_1325 <= 27 r_1471: - x_1311 + 25 z_974 + 27 z_934 + x_1325 <= 26 r_1472: - x_1312 + 25 z_314 + 27 z_939 + x_1325 <= 26 r_1473: - x_1326 + 28 z_944 + x_1325 <= 27 r_1474: - x_1324 + 25 z_1174 + 27 z_949 + x_1325 <= 26 r_1475: - x_1306 + 28 z_954 + x_1325 <= 27 r_1476: - x_1316 + 25 z_749 + 27 z_959 + x_1311 <= 26 r_1477: - x_1309 + 28 z_964 + x_1311 <= 27 r_1478: - x_1301 + 28 z_969 + x_1311 <= 27 r_1479: - x_1325 + 25 z_934 + 27 z_974 + x_1311 <= 26 r_1480: - x_1319 + 28 z_979 + x_1311 <= 27 r_1481: - x_1304 + 25 z_1049 + 27 z_984 + x_1311 <= 26 r_1482: - x_1313 + 28 z_989 + x_1311 <= 27 r_1483: - x_1315 + 28 z_994 + x_1311 <= 27 r_1484: - x_1322 + 25 z_539 + 27 z_999 + x_1311 <= 26 r_1485: - x_1301 + 28 z_1004 + x_1318 <= 27 r_1486: - x_1317 + 28 z_1009 + x_1318 <= 27 r_1487: - x_1302 + 25 z_174 + 27 z_1014 + x_1318 <= 26 r_1488: - x_1323 + 28 z_1019 + x_1318 <= 27 r_1489: - x_1306 + 25 z_644 + 27 z_1024 + x_1318 <= 26 r_1490: - x_1307 + 28 z_1029 + x_1304 <= 27 r_1491: - x_1317 + 28 z_1034 + x_1304 <= 27 r_1492: - x_1302 + 25 z_179 + 27 z_1039 + x_1304 <= 26 r_1493: - x_1327 + 28 z_1044 + x_1304 <= 27 r_1494: - x_1311 + 25 z_984 + 27 z_1049 + x_1304 <= 26 r_1495: - x_1300 + 28 z_1054 + x_1313 <= 27 r_1496: - x_1307 + 25 z_64 + 27 z_1059 + x_1313 <= 26 r_1497: - x_1316 + 25 z_764 + 27 z_1064 + x_1313 <= 26 r_1498: - x_1327 + 25 z_909 + 27 z_1069 + x_1313 <= 26 r_1499: - x_1320 + 28 z_1074 + x_1313 <= 27 r_1500: - x_1325 + 28 z_1079 + x_1313 <= 27 r_1501: - x_1303 + 28 z_1084 + x_1313 <= 27 r_1502: - x_1312 + 25 z_324 + 27 z_1089 + x_1313 <= 26 r_1503: - x_1319 + 28 z_1094 + x_1313 <= 27 r_1504: - x_1304 + 28 z_1099 + x_1313 <= 27 r_1505: - x_1321 + 25 z_414 + 27 z_1104 + x_1313 <= 26 r_1506: - x_1323 + 28 z_1109 + x_1313 <= 27 r_1507: - x_1306 + 25 z_654 + 27 z_1114 + x_1313 <= 26 r_1508: - x_1300 + 28 z_1119 + x_1326 <= 27 r_1509: - x_1309 + 28 z_1124 + x_1326 <= 27 r_1510: - x_1327 + 28 z_1129 + x_1326 <= 27 r_1511: - x_1320 + 28 z_1134 + x_1326 <= 27 r_1512: - x_1312 + 25 z_329 + 27 z_1139 + x_1326 <= 26 r_1513: - x_1321 + 28 z_1144 + x_1326 <= 27 r_1514: - x_1305 + 28 z_1149 + x_1326 <= 27 r_1515: - x_1323 + 25 z_604 + 27 z_1154 + x_1326 <= 26 r_1516: - x_1309 + 28 z_1159 + x_1324 <= 27 r_1517: - x_1317 + 28 z_1164 + x_1324 <= 27 r_1518: - x_1302 + 25 z_194 + 27 z_1169 + x_1324 <= 26 r_1519: - x_1325 + 25 z_949 + 27 z_1174 + x_1324 <= 26 r_1520: - x_1303 + 28 z_1179 + x_1324 <= 27 r_1521: - x_1311 + 28 z_1184 + x_1324 <= 27 r_1522: - x_1312 + 25 z_334 + 27 z_1189 + x_1324 <= 26 r_1523: - x_1304 + 28 z_1194 + x_1324 <= 27 r_1524: - x_1321 + 28 z_1199 + x_1324 <= 27 r_1525: - x_1314 + 28 z_1204 + x_1324 <= 27 r_1526: - x_1315 + 25 z_519 + 27 z_1209 + x_1324 <= 26 r_1527: - x_1306 + 28 z_1214 + x_1324 <= 27 r_1528: 0 z_1 <= 0 r_1529: - x_1307 + x_1300 <= -2 r_1530: - x_1309 + x_1300 <= -2 r_1531: - x_1301 + x_1300 <= -1 r_1532: - x_1302 + x_1300 <= -1 r_1533: - x_1320 + x_1300 <= -2 r_1534: - x_1303 + x_1300 <= -1 r_1535: - x_1312 + x_1300 <= -2 r_1536: - x_1319 + x_1300 <= -3 r_1537: - x_1321 + x_1300 <= -2 r_1538: - x_1314 + x_1300 <= -2 r_1539: - x_1315 + x_1300 <= -2 r_1540: - x_1322 + x_1300 <= -2 r_1541: - x_1305 + x_1300 <= -1 r_1542: - x_1323 + x_1300 <= -2 r_1543: - x_1306 + x_1300 <= -1 r_1544: - x_1308 + x_1300 <= -3 r_1545: - x_1316 + x_1300 <= -2 r_1546: - x_1310 + x_1300 <= -2 r_1547: - x_1317 + x_1300 <= -2 r_1548: - x_1327 + x_1300 <= -2 r_1549: - x_1325 + x_1300 <= -2 r_1550: - x_1311 + x_1300 <= -2 r_1551: - x_1318 + x_1300 <= -2 r_1552: - x_1304 + x_1300 <= -1 r_1553: - x_1313 + x_1300 <= -2 r_1554: - x_1326 + x_1300 <= -2 r_1555: - x_1324 + x_1300 <= -2 r_1556: + z_1215 + z_1210 + z_1205 + z_1200 + z_1195 + z_1190 + z_1185 + z_1180 + z_1175 + z_1170 + z_1165 + z_1160 + z_1155 + z_1150 + z_1145 + z_1140 + z_1135 + z_1130 + z_1125 + z_1120 + z_1115 + z_1110 + z_1105 + z_1100 + z_1095 + z_1090 + z_1085 + z_1080 + z_1075 + z_1070 + z_1065 + z_1060 + z_1055 + z_1050 + z_1045 + z_1040 + z_1035 + z_1030 + z_1025 + z_1020 + z_1015 + z_1010 + z_1005 + z_1000 + z_995 + z_990 + z_985 + z_980 + z_975 + z_970 + z_965 + z_960 + z_955 + z_950 + z_945 + z_940 + z_935 + z_930 + z_925 + z_920 + z_915 + z_910 + z_905 + z_900 + z_895 + z_890 + z_885 + z_880 + z_875 + z_870 + z_865 + z_860 + z_855 + z_850 + z_845 + z_840 + z_835 + z_830 + z_825 + z_820 + z_815 + z_810 + z_805 + z_800 + z_795 + z_790 + z_785 + z_780 + z_775 + z_770 + z_765 + z_760 + z_755 + z_750 + z_745 + z_740 + z_735 + z_730 + z_725 + z_720 + z_715 + z_710 + z_705 + z_700 + z_695 + z_690 + z_685 + z_680 + z_675 + z_670 + z_665 + z_660 + z_655 + z_650 + z_645 + z_640 + z_635 + z_630 + z_625 + z_620 + z_615 + z_610 + z_605 + z_600 + z_595 + z_590 + z_585 + z_580 + z_575 + z_570 + z_565 + z_560 + z_555 + z_550 + z_545 + z_540 + z_535 + z_530 + z_525 + z_520 + z_515 + z_510 + z_505 + z_500 + z_495 + z_490 + z_485 + z_480 + z_475 + z_470 + z_465 + z_460 + z_455 + z_450 + z_445 + z_440 + z_435 + z_430 + z_425 + z_420 + z_415 + z_410 + z_405 + z_400 + z_395 + z_390 + z_385 + z_380 + z_375 + z_370 + z_365 + z_360 + z_355 + z_350 + z_345 + z_340 + z_335 + z_330 + z_325 + z_320 + z_315 + z_310 + z_305 + z_300 + z_295 + z_290 + z_285 + z_280 + z_275 + z_270 + z_265 + z_260 + z_255 + z_250 + z_245 + z_240 + z_235 + z_230 + z_225 + z_220 + z_215 + z_210 + z_205 + z_200 + z_195 + z_190 + z_185 + z_180 + z_175 + z_170 + z_165 + z_160 + z_155 + z_150 + z_145 + z_140 + z_135 + z_130 + z_125 + z_120 + z_115 + z_110 + z_105 + z_100 + z_95 + z_90 + z_85 + z_80 + z_75 + z_70 + z_65 + z_60 + z_55 + z_50 + z_45 + z_40 + z_35 + z_30 + z_25 + z_20 + z_15 + z_10 + z_5 = 27 r_1557: + z_625 + z_585 + z_495 + z_1120 + z_1055 + z_235 + z_920 + z_880 + z_680 = 0 r_1558: + z_1060 + z_1030 + z_340 + z_205 + z_885 + z_840 = 1 r_1559: + z_1160 + z_1125 + z_440 + z_345 + z_965 + z_245 + z_730 + z_40 + z_685 = 1 r_1560: + z_445 + z_385 + z_1005 + z_970 + z_890 + z_90 + z_5 = 1 r_1561: + z_630 + z_535 + z_1170 + z_500 + z_450 + z_390 + z_1040 + z_355 + z_1015 + z_305 + z_215 + z_845 + z_140 + z_100 + z_740 + z_50 + z_10 = 1 r_1562: + z_510 + z_1135 + z_1075 + z_310 + z_255 + z_145 + z_700 = 1 r_1563: + z_1180 + z_460 + z_1085 + z_370 + z_320 + z_220 + z_895 + z_850 + z_15 = 1 r_1564: + z_640 + z_1190 + z_1140 + z_465 + z_1090 + z_400 + z_270 + z_940 + z_150 + z_795 + z_105 + z_60 = 1 r_1565: + z_470 + z_1095 + z_410 + z_980 + z_900 + z_805 + z_115 + z_755 = 1 r_1566: + z_650 + z_1200 + z_1145 + z_1105 + z_275 + z_225 + z_905 + z_185 + z_155 + z_810 + z_760 = 1 r_1567: + z_575 + z_1205 + z_420 + z_915 + z_130 + z_70 = 1 r_1568: + z_610 + z_555 + z_1210 + z_480 + z_995 + z_285 + z_820 + z_135 + z_75 + z_715 = 1 r_1569: + z_665 + z_615 + z_1000 + z_230 + z_200 + z_160 + z_830 = 1 r_1570: + z_670 + z_620 + z_1150 + z_485 + z_870 + z_725 + z_25 = 1 r_1571: + z_675 + z_1155 + z_490 + z_1110 + z_1020 + z_290 + z_165 + z_835 = 1 r_1572: + z_1215 + z_525 + z_1115 + z_425 + z_1025 + z_955 + z_875 + z_775 + z_30 = 1 r_1573: + z_590 + z_530 + z_430 + z_295 + z_925 + z_80 + z_35 = 1 r_1574: + z_435 + z_1065 + z_960 + z_240 + z_780 + z_85 = 1 r_1575: + z_560 + z_380 + z_350 + z_300 + z_45 = 1 r_1576: + z_1165 + z_1035 + z_1010 + z_250 + z_210 + z_170 + z_95 + z_735 + z_690 = 1 r_1577: + z_635 + z_595 + z_505 + z_1130 + z_1070 + z_1045 + z_360 + z_930 + z_785 + z_695 = 1 r_1578: + z_565 + z_1175 + z_455 + z_1080 + z_395 + z_365 + z_315 + z_975 + z_260 + z_745 + z_705 = 1 r_1579: + z_540 + z_1185 + z_1050 + z_265 + z_935 + z_855 + z_790 + z_750 + z_55 = 1 r_1580: + z_645 + z_405 + z_375 + z_175 + z_800 + z_110 = 1 r_1581: + z_600 + z_570 + z_545 + z_1195 + z_475 + z_1100 + z_985 + z_180 + z_120 + z_710 + z_20 = 1 r_1582: + z_655 + z_515 + z_415 + z_325 + z_990 + z_910 + z_190 + z_860 + z_815 + z_125 + z_765 + z_65 = 1 r_1583: + z_660 + z_605 + z_550 + z_330 + z_280 + z_945 + z_865 = 1 r_1584: + z_580 + z_520 + z_335 + z_950 + z_195 + z_825 + z_770 + z_720 = 1 r_1585: - z_30 - z_25 - z_20 - z_15 - z_10 - z_5 - z_625 - z_585 - z_495 - z_1120 - z_1055 - z_235 - z_920 - z_880 - z_680 <= -1 r_1586: - z_75 - z_70 - z_65 - z_60 - z_55 - z_50 - z_45 - z_40 - z_35 - z_1060 - z_1030 - z_340 - z_205 - z_885 - z_840 <= -1 r_1587: - z_135 - z_130 - z_125 - z_120 - z_115 - z_110 - z_105 - z_100 - z_95 - z_90 - z_85 - z_80 - z_1160 - z_1125 - z_440 - z_345 - z_965 - z_245 - z_730 - z_40 - z_685 <= -1 r_1588: - z_165 - z_160 - z_155 - z_150 - z_145 - z_140 - z_445 - z_385 - z_1005 - z_970 - z_890 - z_90 - z_5 <= -1 r_1589: - z_200 - z_195 - z_190 - z_185 - z_180 - z_175 - z_170 - z_630 - z_535 - z_1170 - z_500 - z_450 - z_390 - z_1040 - z_355 - z_1015 - z_305 - z_215 - z_845 - z_140 - z_100 - z_740 - z_50 - z_10 <= -1 r_1590: - z_230 - z_225 - z_220 - z_215 - z_210 - z_205 - z_510 - z_1135 - z_1075 - z_310 - z_255 - z_145 - z_700 <= -1 r_1591: - z_290 - z_285 - z_280 - z_275 - z_270 - z_265 - z_260 - z_255 - z_250 - z_245 - z_240 - z_235 - z_1180 - z_460 - z_1085 - z_370 - z_320 - z_220 - z_895 - z_850 - z_15 <= -1 r_1592: - z_335 - z_330 - z_325 - z_320 - z_315 - z_310 - z_305 - z_300 - z_295 - z_640 - z_1190 - z_1140 - z_465 - z_1090 - z_400 - z_270 - z_940 - z_150 - z_795 - z_105 - z_60 <= -1 r_1593: - z_375 - z_370 - z_365 - z_360 - z_355 - z_350 - z_345 - z_340 - z_470 - z_1095 - z_410 - z_980 - z_900 - z_805 - z_115 - z_755 <= -1 r_1594: - z_425 - z_420 - z_415 - z_410 - z_405 - z_400 - z_395 - z_390 - z_385 - z_380 - z_650 - z_1200 - z_1145 - z_1105 - z_275 - z_225 - z_905 - z_185 - z_155 - z_810 - z_760 <= -1 r_1595: - z_490 - z_485 - z_480 - z_475 - z_470 - z_465 - z_460 - z_455 - z_450 - z_445 - z_440 - z_435 - z_430 - z_575 - z_1205 - z_420 - z_915 - z_130 - z_70 <= -1 r_1596: - z_525 - z_520 - z_515 - z_510 - z_505 - z_500 - z_495 - z_610 - z_555 - z_1210 - z_480 - z_995 - z_285 - z_820 - z_135 - z_75 - z_715 <= -1 r_1597: - z_555 - z_550 - z_545 - z_540 - z_535 - z_530 - z_665 - z_615 - z_1000 - z_230 - z_200 - z_160 - z_830 <= -1 r_1598: - z_580 - z_575 - z_570 - z_565 - z_560 - z_670 - z_620 - z_1150 - z_485 - z_870 - z_725 - z_25 <= -1 r_1599: - z_620 - z_615 - z_610 - z_605 - z_600 - z_595 - z_590 - z_585 - z_675 - z_1155 - z_490 - z_1110 - z_1020 - z_290 - z_165 - z_835 <= -1 r_1600: - z_675 - z_670 - z_665 - z_660 - z_655 - z_650 - z_645 - z_640 - z_635 - z_630 - z_625 - z_1215 - z_525 - z_1115 - z_425 - z_1025 - z_955 - z_875 - z_775 - z_30 <= -1 r_1601: - z_725 - z_720 - z_715 - z_710 - z_705 - z_700 - z_695 - z_690 - z_685 - z_680 - z_590 - z_530 - z_430 - z_295 - z_925 - z_80 - z_35 <= -1 r_1602: - z_775 - z_770 - z_765 - z_760 - z_755 - z_750 - z_745 - z_740 - z_735 - z_730 - z_435 - z_1065 - z_960 - z_240 - z_780 - z_85 <= -1 r_1603: - z_835 - z_830 - z_825 - z_820 - z_815 - z_810 - z_805 - z_800 - z_795 - z_790 - z_785 - z_780 - z_560 - z_380 - z_350 - z_300 - z_45 <= -1 r_1604: - z_875 - z_870 - z_865 - z_860 - z_855 - z_850 - z_845 - z_840 - z_1165 - z_1035 - z_1010 - z_250 - z_210 - z_170 - z_95 - z_735 - z_690 <= -1 r_1605: - z_915 - z_910 - z_905 - z_900 - z_895 - z_890 - z_885 - z_880 - z_635 - z_595 - z_505 - z_1130 - z_1070 - z_1045 - z_360 - z_930 - z_785 - z_695 <= -1 r_1606: - z_955 - z_950 - z_945 - z_940 - z_935 - z_930 - z_925 - z_920 - z_565 - z_1175 - z_455 - z_1080 - z_395 - z_365 - z_315 - z_975 - z_260 - z_745 - z_705 <= -1 r_1607: - z_1000 - z_995 - z_990 - z_985 - z_980 - z_975 - z_970 - z_965 - z_960 - z_540 - z_1185 - z_1050 - z_265 - z_935 - z_855 - z_790 - z_750 - z_55 <= -1 r_1608: - z_1025 - z_1020 - z_1015 - z_1010 - z_1005 - z_645 - z_405 - z_375 - z_175 - z_800 - z_110 <= -1 r_1609: - z_1050 - z_1045 - z_1040 - z_1035 - z_1030 - z_600 - z_570 - z_545 - z_1195 - z_475 - z_1100 - z_985 - z_180 - z_120 - z_710 - z_20 <= -1 r_1610: - z_1115 - z_1110 - z_1105 - z_1100 - z_1095 - z_1090 - z_1085 - z_1080 - z_1075 - z_1070 - z_1065 - z_1060 - z_1055 - z_655 - z_515 - z_415 - z_325 - z_990 - z_910 - z_190 - z_860 - z_815 - z_125 - z_765 - z_65 <= -1 r_1611: - z_1155 - z_1150 - z_1145 - z_1140 - z_1135 - z_1130 - z_1125 - z_1120 - z_660 - z_605 - z_550 - z_330 - z_280 - z_945 - z_865 <= -1 r_1612: - z_1215 - z_1210 - z_1205 - z_1200 - z_1195 - z_1190 - z_1185 - z_1180 - z_1175 - z_1170 - z_1165 - z_1160 - z_580 - z_520 - z_335 - z_950 - z_195 - z_825 - z_770 - z_720 <= -1 r_1613: - x_1329 + 28 z_5 + x_1328 <= 27 r_1614: - x_1330 + 28 z_10 + x_1328 <= 27 r_1615: - x_1331 + 25 z_235 + 27 z_15 + x_1328 <= 26 r_1616: - x_1332 + 28 z_20 + x_1328 <= 27 r_1617: - x_1333 + 28 z_25 + x_1328 <= 27 r_1618: - x_1334 + 25 z_625 + 27 z_30 + x_1328 <= 26 r_1619: - x_1336 + 28 z_35 + x_1335 <= 27 r_1620: - x_1337 + 28 z_40 + x_1335 <= 27 r_1621: - x_1338 + 28 z_45 + x_1335 <= 27 r_1622: - x_1330 + 28 z_50 + x_1335 <= 27 r_1623: - x_1339 + 28 z_55 + x_1335 <= 27 r_1624: - x_1340 + 28 z_60 + x_1335 <= 27 r_1625: - x_1341 + 25 z_1060 + 27 z_65 + x_1335 <= 26 r_1626: - x_1342 + 28 z_70 + x_1335 <= 27 r_1627: - x_1343 + 28 z_75 + x_1335 <= 27 r_1628: - x_1336 + 25 z_685 + 27 z_80 + x_1337 <= 26 r_1629: - x_1344 + 25 z_730 + 27 z_85 + x_1337 <= 26 r_1630: - x_1329 + 28 z_90 + x_1337 <= 27 r_1631: - x_1345 + 28 z_95 + x_1337 <= 27 r_1632: - x_1330 + 28 z_100 + x_1337 <= 27 r_1633: - x_1340 + 28 z_105 + x_1337 <= 27 r_1634: - x_1346 + 28 z_110 + x_1337 <= 27 r_1635: - x_1347 + 25 z_345 + 27 z_115 + x_1337 <= 26 r_1636: - x_1332 + 28 z_120 + x_1337 <= 27 r_1637: - x_1341 + 28 z_125 + x_1337 <= 27 r_1638: - x_1342 + 25 z_440 + 27 z_130 + x_1337 <= 26 r_1639: - x_1343 + 28 z_135 + x_1337 <= 27 r_1640: - x_1330 + 28 z_140 + x_1329 <= 27 r_1641: - x_1348 + 28 z_145 + x_1329 <= 27 r_1642: - x_1340 + 28 z_150 + x_1329 <= 27 r_1643: - x_1349 + 25 z_385 + 27 z_155 + x_1329 <= 26 r_1644: - x_1350 + 28 z_160 + x_1329 <= 27 r_1645: - x_1351 + 28 z_165 + x_1329 <= 27 r_1646: - x_1345 + 25 z_845 + 27 z_170 + x_1330 <= 26 r_1647: - x_1346 + 25 z_1015 + 27 z_175 + x_1330 <= 26 r_1648: - x_1332 + 25 z_1040 + 27 z_180 + x_1330 <= 26 r_1649: - x_1349 + 25 z_390 + 27 z_185 + x_1330 <= 26 r_1650: - x_1341 + 28 z_190 + x_1330 <= 27 r_1651: - x_1352 + 25 z_1170 + 27 z_195 + x_1330 <= 26 r_1652: - x_1350 + 25 z_535 + 27 z_200 + x_1330 <= 26 r_1653: - x_1335 + 28 z_205 + x_1348 <= 27 r_1654: - x_1345 + 28 z_210 + x_1348 <= 27 r_1655: - x_1330 + 28 z_215 + x_1348 <= 27 r_1656: - x_1331 + 25 z_255 + 27 z_220 + x_1348 <= 26 r_1657: - x_1349 + 28 z_225 + x_1348 <= 27 r_1658: - x_1350 + 28 z_230 + x_1348 <= 27 r_1659: - x_1328 + 25 z_15 + 27 z_235 + x_1331 <= 26 r_1660: - x_1344 + 28 z_240 + x_1331 <= 27 r_1661: - x_1337 + 28 z_245 + x_1331 <= 27 r_1662: - x_1345 + 25 z_850 + 27 z_250 + x_1331 <= 26 r_1663: - x_1348 + 25 z_220 + 27 z_255 + x_1331 <= 26 r_1664: - x_1353 + 28 z_260 + x_1331 <= 27 r_1665: - x_1339 + 28 z_265 + x_1331 <= 27 r_1666: - x_1340 + 25 z_320 + 27 z_270 + x_1331 <= 26 r_1667: - x_1349 + 28 z_275 + x_1331 <= 27 r_1668: - x_1354 + 28 z_280 + x_1331 <= 27 r_1669: - x_1343 + 28 z_285 + x_1331 <= 27 r_1670: - x_1351 + 28 z_290 + x_1331 <= 27 r_1671: - x_1336 + 28 z_295 + x_1340 <= 27 r_1672: - x_1338 + 25 z_795 + 27 z_300 + x_1340 <= 26 r_1673: - x_1330 + 28 z_305 + x_1340 <= 27 r_1674: - x_1348 + 28 z_310 + x_1340 <= 27 r_1675: - x_1353 + 25 z_940 + 27 z_315 + x_1340 <= 26 r_1676: - x_1331 + 25 z_270 + 27 z_320 + x_1340 <= 26 r_1677: - x_1341 + 25 z_1090 + 27 z_325 + x_1340 <= 26 r_1678: - x_1354 + 25 z_1140 + 27 z_330 + x_1340 <= 26 r_1679: - x_1352 + 25 z_1190 + 27 z_335 + x_1340 <= 26 r_1680: - x_1335 + 28 z_340 + x_1347 <= 27 r_1681: - x_1337 + 25 z_115 + 27 z_345 + x_1347 <= 26 r_1682: - x_1338 + 25 z_805 + 27 z_350 + x_1347 <= 26 r_1683: - x_1330 + 28 z_355 + x_1347 <= 27 r_1684: - x_1355 + 25 z_900 + 27 z_360 + x_1347 <= 26 r_1685: - x_1353 + 28 z_365 + x_1347 <= 27 r_1686: - x_1331 + 28 z_370 + x_1347 <= 27 r_1687: - x_1346 + 28 z_375 + x_1347 <= 27 r_1688: - x_1338 + 25 z_810 + 27 z_380 + x_1349 <= 26 r_1689: - x_1329 + 25 z_155 + 27 z_385 + x_1349 <= 26 r_1690: - x_1330 + 25 z_185 + 27 z_390 + x_1349 <= 26 r_1691: - x_1353 + 28 z_395 + x_1349 <= 27 r_1692: - x_1340 + 28 z_400 + x_1349 <= 27 r_1693: - x_1346 + 28 z_405 + x_1349 <= 27 r_1694: - x_1347 + 28 z_410 + x_1349 <= 27 r_1695: - x_1341 + 25 z_1105 + 27 z_415 + x_1349 <= 26 r_1696: - x_1342 + 28 z_420 + x_1349 <= 27 r_1697: - x_1334 + 25 z_650 + 27 z_425 + x_1349 <= 26 r_1698: - x_1336 + 28 z_430 + x_1342 <= 27 r_1699: - x_1344 + 28 z_435 + x_1342 <= 27 r_1700: - x_1337 + 25 z_130 + 27 z_440 + x_1342 <= 26 r_1701: - x_1329 + 28 z_445 + x_1342 <= 27 r_1702: - x_1330 + 28 z_450 + x_1342 <= 27 r_1703: - x_1353 + 28 z_455 + x_1342 <= 27 r_1704: - x_1331 + 28 z_460 + x_1342 <= 27 r_1705: - x_1340 + 28 z_465 + x_1342 <= 27 r_1706: - x_1347 + 28 z_470 + x_1342 <= 27 r_1707: - x_1332 + 28 z_475 + x_1342 <= 27 r_1708: - x_1343 + 28 z_480 + x_1342 <= 27 r_1709: - x_1333 + 25 z_575 + 27 z_485 + x_1342 <= 26 r_1710: - x_1351 + 28 z_490 + x_1342 <= 27 r_1711: - x_1328 + 28 z_495 + x_1343 <= 27 r_1712: - x_1330 + 28 z_500 + x_1343 <= 27 r_1713: - x_1355 + 28 z_505 + x_1343 <= 27 r_1714: - x_1348 + 28 z_510 + x_1343 <= 27 r_1715: - x_1341 + 28 z_515 + x_1343 <= 27 r_1716: - x_1352 + 25 z_1210 + 27 z_520 + x_1343 <= 26 r_1717: - x_1334 + 28 z_525 + x_1343 <= 27 r_1718: - x_1336 + 28 z_530 + x_1350 <= 27 r_1719: - x_1330 + 25 z_200 + 27 z_535 + x_1350 <= 26 r_1720: - x_1339 + 25 z_1000 + 27 z_540 + x_1350 <= 26 r_1721: - x_1332 + 28 z_545 + x_1350 <= 27 r_1722: - x_1354 + 28 z_550 + x_1350 <= 27 r_1723: - x_1343 + 28 z_555 + x_1350 <= 27 r_1724: - x_1338 + 28 z_560 + x_1333 <= 27 r_1725: - x_1353 + 28 z_565 + x_1333 <= 27 r_1726: - x_1332 + 28 z_570 + x_1333 <= 27 r_1727: - x_1342 + 25 z_485 + 27 z_575 + x_1333 <= 26 r_1728: - x_1352 + 28 z_580 + x_1333 <= 27 r_1729: - x_1328 + 28 z_585 + x_1351 <= 27 r_1730: - x_1336 + 28 z_590 + x_1351 <= 27 r_1731: - x_1355 + 28 z_595 + x_1351 <= 27 r_1732: - x_1332 + 28 z_600 + x_1351 <= 27 r_1733: - x_1354 + 25 z_1155 + 27 z_605 + x_1351 <= 26 r_1734: - x_1343 + 28 z_610 + x_1351 <= 27 r_1735: - x_1350 + 28 z_615 + x_1351 <= 27 r_1736: - x_1333 + 28 z_620 + x_1351 <= 27 r_1737: - x_1328 + 25 z_30 + 27 z_625 + x_1334 <= 26 r_1738: - x_1330 + 28 z_630 + x_1334 <= 27 r_1739: - x_1355 + 28 z_635 + x_1334 <= 27 r_1740: - x_1340 + 28 z_640 + x_1334 <= 27 r_1741: - x_1346 + 25 z_1025 + 27 z_645 + x_1334 <= 26 r_1742: - x_1349 + 25 z_425 + 27 z_650 + x_1334 <= 26 r_1743: - x_1341 + 25 z_1115 + 27 z_655 + x_1334 <= 26 r_1744: - x_1354 + 28 z_660 + x_1334 <= 27 r_1745: - x_1350 + 28 z_665 + x_1334 <= 27 r_1746: - x_1333 + 28 z_670 + x_1334 <= 27 r_1747: - x_1351 + 28 z_675 + x_1334 <= 27 r_1748: - x_1328 + 28 z_680 + x_1336 <= 27 r_1749: - x_1337 + 25 z_80 + 27 z_685 + x_1336 <= 26 r_1750: - x_1345 + 28 z_690 + x_1336 <= 27 r_1751: - x_1355 + 28 z_695 + x_1336 <= 27 r_1752: - x_1348 + 28 z_700 + x_1336 <= 27 r_1753: - x_1353 + 25 z_925 + 27 z_705 + x_1336 <= 26 r_1754: - x_1332 + 28 z_710 + x_1336 <= 27 r_1755: - x_1343 + 28 z_715 + x_1336 <= 27 r_1756: - x_1352 + 28 z_720 + x_1336 <= 27 r_1757: - x_1333 + 28 z_725 + x_1336 <= 27 r_1758: - x_1337 + 25 z_85 + 27 z_730 + x_1344 <= 26 r_1759: - x_1345 + 28 z_735 + x_1344 <= 27 r_1760: - x_1330 + 28 z_740 + x_1344 <= 27 r_1761: - x_1353 + 28 z_745 + x_1344 <= 27 r_1762: - x_1339 + 25 z_960 + 27 z_750 + x_1344 <= 26 r_1763: - x_1347 + 28 z_755 + x_1344 <= 27 r_1764: - x_1349 + 28 z_760 + x_1344 <= 27 r_1765: - x_1341 + 25 z_1065 + 27 z_765 + x_1344 <= 26 r_1766: - x_1352 + 28 z_770 + x_1344 <= 27 r_1767: - x_1334 + 28 z_775 + x_1344 <= 27 r_1768: - x_1344 + 28 z_780 + x_1338 <= 27 r_1769: - x_1355 + 28 z_785 + x_1338 <= 27 r_1770: - x_1339 + 28 z_790 + x_1338 <= 27 r_1771: - x_1340 + 25 z_300 + 27 z_795 + x_1338 <= 26 r_1772: - x_1346 + 28 z_800 + x_1338 <= 27 r_1773: - x_1347 + 25 z_350 + 27 z_805 + x_1338 <= 26 r_1774: - x_1349 + 25 z_380 + 27 z_810 + x_1338 <= 26 r_1775: - x_1341 + 28 z_815 + x_1338 <= 27 r_1776: - x_1343 + 28 z_820 + x_1338 <= 27 r_1777: - x_1352 + 28 z_825 + x_1338 <= 27 r_1778: - x_1350 + 28 z_830 + x_1338 <= 27 r_1779: - x_1351 + 28 z_835 + x_1338 <= 27 r_1780: - x_1335 + 28 z_840 + x_1345 <= 27 r_1781: - x_1330 + 25 z_170 + 27 z_845 + x_1345 <= 26 r_1782: - x_1331 + 25 z_250 + 27 z_850 + x_1345 <= 26 r_1783: - x_1339 + 28 z_855 + x_1345 <= 27 r_1784: - x_1341 + 28 z_860 + x_1345 <= 27 r_1785: - x_1354 + 28 z_865 + x_1345 <= 27 r_1786: - x_1333 + 28 z_870 + x_1345 <= 27 r_1787: - x_1334 + 28 z_875 + x_1345 <= 27 r_1788: - x_1328 + 28 z_880 + x_1355 <= 27 r_1789: - x_1335 + 28 z_885 + x_1355 <= 27 r_1790: - x_1329 + 28 z_890 + x_1355 <= 27 r_1791: - x_1331 + 28 z_895 + x_1355 <= 27 r_1792: - x_1347 + 25 z_360 + 27 z_900 + x_1355 <= 26 r_1793: - x_1349 + 28 z_905 + x_1355 <= 27 r_1794: - x_1341 + 25 z_1070 + 27 z_910 + x_1355 <= 26 r_1795: - x_1342 + 28 z_915 + x_1355 <= 27 r_1796: - x_1328 + 28 z_920 + x_1353 <= 27 r_1797: - x_1336 + 25 z_705 + 27 z_925 + x_1353 <= 26 r_1798: - x_1355 + 28 z_930 + x_1353 <= 27 r_1799: - x_1339 + 25 z_975 + 27 z_935 + x_1353 <= 26 r_1800: - x_1340 + 25 z_315 + 27 z_940 + x_1353 <= 26 r_1801: - x_1354 + 28 z_945 + x_1353 <= 27 r_1802: - x_1352 + 25 z_1175 + 27 z_950 + x_1353 <= 26 r_1803: - x_1334 + 28 z_955 + x_1353 <= 27 r_1804: - x_1344 + 25 z_750 + 27 z_960 + x_1339 <= 26 r_1805: - x_1337 + 28 z_965 + x_1339 <= 27 r_1806: - x_1329 + 28 z_970 + x_1339 <= 27 r_1807: - x_1353 + 25 z_935 + 27 z_975 + x_1339 <= 26 r_1808: - x_1347 + 28 z_980 + x_1339 <= 27 r_1809: - x_1332 + 25 z_1050 + 27 z_985 + x_1339 <= 26 r_1810: - x_1341 + 28 z_990 + x_1339 <= 27 r_1811: - x_1343 + 28 z_995 + x_1339 <= 27 r_1812: - x_1350 + 25 z_540 + 27 z_1000 + x_1339 <= 26 r_1813: - x_1329 + 28 z_1005 + x_1346 <= 27 r_1814: - x_1345 + 28 z_1010 + x_1346 <= 27 r_1815: - x_1330 + 25 z_175 + 27 z_1015 + x_1346 <= 26 r_1816: - x_1351 + 28 z_1020 + x_1346 <= 27 r_1817: - x_1334 + 25 z_645 + 27 z_1025 + x_1346 <= 26 r_1818: - x_1335 + 28 z_1030 + x_1332 <= 27 r_1819: - x_1345 + 28 z_1035 + x_1332 <= 27 r_1820: - x_1330 + 25 z_180 + 27 z_1040 + x_1332 <= 26 r_1821: - x_1355 + 28 z_1045 + x_1332 <= 27 r_1822: - x_1339 + 25 z_985 + 27 z_1050 + x_1332 <= 26 r_1823: - x_1328 + 28 z_1055 + x_1341 <= 27 r_1824: - x_1335 + 25 z_65 + 27 z_1060 + x_1341 <= 26 r_1825: - x_1344 + 25 z_765 + 27 z_1065 + x_1341 <= 26 r_1826: - x_1355 + 25 z_910 + 27 z_1070 + x_1341 <= 26 r_1827: - x_1348 + 28 z_1075 + x_1341 <= 27 r_1828: - x_1353 + 28 z_1080 + x_1341 <= 27 r_1829: - x_1331 + 28 z_1085 + x_1341 <= 27 r_1830: - x_1340 + 25 z_325 + 27 z_1090 + x_1341 <= 26 r_1831: - x_1347 + 28 z_1095 + x_1341 <= 27 r_1832: - x_1332 + 28 z_1100 + x_1341 <= 27 r_1833: - x_1349 + 25 z_415 + 27 z_1105 + x_1341 <= 26 r_1834: - x_1351 + 28 z_1110 + x_1341 <= 27 r_1835: - x_1334 + 25 z_655 + 27 z_1115 + x_1341 <= 26 r_1836: - x_1328 + 28 z_1120 + x_1354 <= 27 r_1837: - x_1337 + 28 z_1125 + x_1354 <= 27 r_1838: - x_1355 + 28 z_1130 + x_1354 <= 27 r_1839: - x_1348 + 28 z_1135 + x_1354 <= 27 r_1840: - x_1340 + 25 z_330 + 27 z_1140 + x_1354 <= 26 r_1841: - x_1349 + 28 z_1145 + x_1354 <= 27 r_1842: - x_1333 + 28 z_1150 + x_1354 <= 27 r_1843: - x_1351 + 25 z_605 + 27 z_1155 + x_1354 <= 26 r_1844: - x_1337 + 28 z_1160 + x_1352 <= 27 r_1845: - x_1345 + 28 z_1165 + x_1352 <= 27 r_1846: - x_1330 + 25 z_195 + 27 z_1170 + x_1352 <= 26 r_1847: - x_1353 + 25 z_950 + 27 z_1175 + x_1352 <= 26 r_1848: - x_1331 + 28 z_1180 + x_1352 <= 27 r_1849: - x_1339 + 28 z_1185 + x_1352 <= 27 r_1850: - x_1340 + 25 z_335 + 27 z_1190 + x_1352 <= 26 r_1851: - x_1332 + 28 z_1195 + x_1352 <= 27 r_1852: - x_1349 + 28 z_1200 + x_1352 <= 27 r_1853: - x_1342 + 28 z_1205 + x_1352 <= 27 r_1854: - x_1343 + 25 z_520 + 27 z_1210 + x_1352 <= 26 r_1855: - x_1334 + 28 z_1215 + x_1352 <= 27 r_1856: 0 z_1 <= 0 r_1857: - x_1335 + x_1328 <= -2 r_1858: - x_1337 + x_1328 <= -2 r_1859: - x_1329 + x_1328 <= -1 r_1860: - x_1330 + x_1328 <= -1 r_1861: - x_1348 + x_1328 <= -2 r_1862: - x_1331 + x_1328 <= -1 r_1863: - x_1340 + x_1328 <= -2 r_1864: - x_1347 + x_1328 <= -3 r_1865: - x_1349 + x_1328 <= -2 r_1866: - x_1342 + x_1328 <= -2 r_1867: - x_1343 + x_1328 <= -2 r_1868: - x_1350 + x_1328 <= -2 r_1869: - x_1333 + x_1328 <= -1 r_1870: - x_1351 + x_1328 <= -2 r_1871: - x_1334 + x_1328 <= -1 r_1872: - x_1336 + x_1328 <= -3 r_1873: - x_1344 + x_1328 <= -2 r_1874: - x_1338 + x_1328 <= -2 r_1875: - x_1345 + x_1328 <= -2 r_1876: - x_1355 + x_1328 <= -2 r_1877: - x_1353 + x_1328 <= -2 r_1878: - x_1339 + x_1328 <= -2 r_1879: - x_1346 + x_1328 <= -2 r_1880: - x_1332 + x_1328 <= -1 r_1881: - x_1341 + x_1328 <= -2 r_1882: - x_1354 + x_1328 <= -2 r_1883: - x_1352 + x_1328 <= -2 Bounds 0 <= z_1 <= 1 0 <= z_2 <= 1 0 <= z_3 <= 1 0 <= z_4 <= 1 0 <= z_5 <= 1 0 <= z_6 <= 1 0 <= z_7 <= 1 0 <= z_8 <= 1 0 <= z_9 <= 1 0 <= z_10 <= 1 0 <= z_11 <= 1 0 <= z_12 <= 1 0 <= z_13 <= 1 0 <= z_14 <= 1 0 <= z_15 <= 1 0 <= z_16 <= 1 0 <= z_17 <= 1 0 <= z_18 <= 1 0 <= z_19 <= 1 0 <= z_20 <= 1 0 <= z_21 <= 1 0 <= z_22 <= 1 0 <= z_23 <= 1 0 <= z_24 <= 1 0 <= z_25 <= 1 0 <= z_26 <= 1 0 <= z_27 <= 1 0 <= z_28 <= 1 0 <= z_29 <= 1 0 <= z_30 <= 1 0 <= z_31 <= 1 0 <= z_32 <= 1 0 <= z_33 <= 1 0 <= z_34 <= 1 0 <= z_35 <= 1 0 <= z_36 <= 1 0 <= z_37 <= 1 0 <= z_38 <= 1 0 <= z_39 <= 1 0 <= z_40 <= 1 0 <= z_41 <= 1 0 <= z_42 <= 1 0 <= z_43 <= 1 0 <= z_44 <= 1 0 <= z_45 <= 1 0 <= z_46 <= 1 0 <= z_47 <= 1 0 <= z_48 <= 1 0 <= z_49 <= 1 0 <= z_50 <= 1 0 <= z_51 <= 1 0 <= z_52 <= 1 0 <= z_53 <= 1 0 <= z_54 <= 1 0 <= z_55 <= 1 0 <= z_56 <= 1 0 <= z_57 <= 1 0 <= z_58 <= 1 0 <= z_59 <= 1 0 <= z_60 <= 1 0 <= z_61 <= 1 0 <= z_62 <= 1 0 <= z_63 <= 1 0 <= z_64 <= 1 0 <= z_65 <= 1 0 <= z_66 <= 1 0 <= z_67 <= 1 0 <= z_68 <= 1 0 <= z_69 <= 1 0 <= z_70 <= 1 0 <= z_71 <= 1 0 <= z_72 <= 1 0 <= z_73 <= 1 0 <= z_74 <= 1 0 <= z_75 <= 1 0 <= z_76 <= 1 0 <= z_77 <= 1 0 <= z_78 <= 1 0 <= z_79 <= 1 0 <= z_80 <= 1 0 <= z_81 <= 1 0 <= z_82 <= 1 0 <= z_83 <= 1 0 <= z_84 <= 1 0 <= z_85 <= 1 0 <= z_86 <= 1 0 <= z_87 <= 1 0 <= z_88 <= 1 0 <= z_89 <= 1 0 <= z_90 <= 1 0 <= z_91 <= 1 0 <= z_92 <= 1 0 <= z_93 <= 1 0 <= z_94 <= 1 0 <= z_95 <= 1 0 <= z_96 <= 1 0 <= z_97 <= 1 0 <= z_98 <= 1 0 <= z_99 <= 1 0 <= z_100 <= 1 0 <= z_101 <= 1 0 <= z_102 <= 1 0 <= z_103 <= 1 0 <= z_104 <= 1 0 <= z_105 <= 1 0 <= z_106 <= 1 0 <= z_107 <= 1 0 <= z_108 <= 1 0 <= z_109 <= 1 0 <= z_110 <= 1 0 <= z_111 <= 1 0 <= z_112 <= 1 0 <= z_113 <= 1 0 <= z_114 <= 1 0 <= z_115 <= 1 0 <= z_116 <= 1 0 <= z_117 <= 1 0 <= z_118 <= 1 0 <= z_119 <= 1 0 <= z_120 <= 1 0 <= z_121 <= 1 0 <= z_122 <= 1 0 <= z_123 <= 1 0 <= z_124 <= 1 0 <= z_125 <= 1 0 <= z_126 <= 1 0 <= z_127 <= 1 0 <= z_128 <= 1 0 <= z_129 <= 1 0 <= z_130 <= 1 0 <= z_131 <= 1 0 <= z_132 <= 1 0 <= z_133 <= 1 0 <= z_134 <= 1 0 <= z_135 <= 1 0 <= z_136 <= 1 0 <= z_137 <= 1 0 <= z_138 <= 1 0 <= z_139 <= 1 0 <= z_140 <= 1 0 <= z_141 <= 1 0 <= z_142 <= 1 0 <= z_143 <= 1 0 <= z_144 <= 1 0 <= z_145 <= 1 0 <= z_146 <= 1 0 <= z_147 <= 1 0 <= z_148 <= 1 0 <= z_149 <= 1 0 <= z_150 <= 1 0 <= z_151 <= 1 0 <= z_152 <= 1 0 <= z_153 <= 1 0 <= z_154 <= 1 0 <= z_155 <= 1 0 <= z_156 <= 1 0 <= z_157 <= 1 0 <= z_158 <= 1 0 <= z_159 <= 1 0 <= z_160 <= 1 0 <= z_161 <= 1 0 <= z_162 <= 1 0 <= z_163 <= 1 0 <= z_164 <= 1 0 <= z_165 <= 1 0 <= z_166 <= 1 0 <= z_167 <= 1 0 <= z_168 <= 1 0 <= z_169 <= 1 0 <= z_170 <= 1 0 <= z_171 <= 1 0 <= z_172 <= 1 0 <= z_173 <= 1 0 <= z_174 <= 1 0 <= z_175 <= 1 0 <= z_176 <= 1 0 <= z_177 <= 1 0 <= z_178 <= 1 0 <= z_179 <= 1 0 <= z_180 <= 1 0 <= z_181 <= 1 0 <= z_182 <= 1 0 <= z_183 <= 1 0 <= z_184 <= 1 0 <= z_185 <= 1 0 <= z_186 <= 1 0 <= z_187 <= 1 0 <= z_188 <= 1 0 <= z_189 <= 1 0 <= z_190 <= 1 0 <= z_191 <= 1 0 <= z_192 <= 1 0 <= z_193 <= 1 0 <= z_194 <= 1 0 <= z_195 <= 1 0 <= z_196 <= 1 0 <= z_197 <= 1 0 <= z_198 <= 1 0 <= z_199 <= 1 0 <= z_200 <= 1 0 <= z_201 <= 1 0 <= z_202 <= 1 0 <= z_203 <= 1 0 <= z_204 <= 1 0 <= z_205 <= 1 0 <= z_206 <= 1 0 <= z_207 <= 1 0 <= z_208 <= 1 0 <= z_209 <= 1 0 <= z_210 <= 1 0 <= z_211 <= 1 0 <= z_212 <= 1 0 <= z_213 <= 1 0 <= z_214 <= 1 0 <= z_215 <= 1 0 <= z_216 <= 1 0 <= z_217 <= 1 0 <= z_218 <= 1 0 <= z_219 <= 1 0 <= z_220 <= 1 0 <= z_221 <= 1 0 <= z_222 <= 1 0 <= z_223 <= 1 0 <= z_224 <= 1 0 <= z_225 <= 1 0 <= z_226 <= 1 0 <= z_227 <= 1 0 <= z_228 <= 1 0 <= z_229 <= 1 0 <= z_230 <= 1 0 <= z_231 <= 1 0 <= z_232 <= 1 0 <= z_233 <= 1 0 <= z_234 <= 1 0 <= z_235 <= 1 0 <= z_236 <= 1 0 <= z_237 <= 1 0 <= z_238 <= 1 0 <= z_239 <= 1 0 <= z_240 <= 1 0 <= z_241 <= 1 0 <= z_242 <= 1 0 <= z_243 <= 1 0 <= z_244 <= 1 0 <= z_245 <= 1 0 <= z_246 <= 1 0 <= z_247 <= 1 0 <= z_248 <= 1 0 <= z_249 <= 1 0 <= z_250 <= 1 0 <= z_251 <= 1 0 <= z_252 <= 1 0 <= z_253 <= 1 0 <= z_254 <= 1 0 <= z_255 <= 1 0 <= z_256 <= 1 0 <= z_257 <= 1 0 <= z_258 <= 1 0 <= z_259 <= 1 0 <= z_260 <= 1 0 <= z_261 <= 1 0 <= z_262 <= 1 0 <= z_263 <= 1 0 <= z_264 <= 1 0 <= z_265 <= 1 0 <= z_266 <= 1 0 <= z_267 <= 1 0 <= z_268 <= 1 0 <= z_269 <= 1 0 <= z_270 <= 1 0 <= z_271 <= 1 0 <= z_272 <= 1 0 <= z_273 <= 1 0 <= z_274 <= 1 0 <= z_275 <= 1 0 <= z_276 <= 1 0 <= z_277 <= 1 0 <= z_278 <= 1 0 <= z_279 <= 1 0 <= z_280 <= 1 0 <= z_281 <= 1 0 <= z_282 <= 1 0 <= z_283 <= 1 0 <= z_284 <= 1 0 <= z_285 <= 1 0 <= z_286 <= 1 0 <= z_287 <= 1 0 <= z_288 <= 1 0 <= z_289 <= 1 0 <= z_290 <= 1 0 <= z_291 <= 1 0 <= z_292 <= 1 0 <= z_293 <= 1 0 <= z_294 <= 1 0 <= z_295 <= 1 0 <= z_296 <= 1 0 <= z_297 <= 1 0 <= z_298 <= 1 0 <= z_299 <= 1 0 <= z_300 <= 1 0 <= z_301 <= 1 0 <= z_302 <= 1 0 <= z_303 <= 1 0 <= z_304 <= 1 0 <= z_305 <= 1 0 <= z_306 <= 1 0 <= z_307 <= 1 0 <= z_308 <= 1 0 <= z_309 <= 1 0 <= z_310 <= 1 0 <= z_311 <= 1 0 <= z_312 <= 1 0 <= z_313 <= 1 0 <= z_314 <= 1 0 <= z_315 <= 1 0 <= z_316 <= 1 0 <= z_317 <= 1 0 <= z_318 <= 1 0 <= z_319 <= 1 0 <= z_320 <= 1 0 <= z_321 <= 1 0 <= z_322 <= 1 0 <= z_323 <= 1 0 <= z_324 <= 1 0 <= z_325 <= 1 0 <= z_326 <= 1 0 <= z_327 <= 1 0 <= z_328 <= 1 0 <= z_329 <= 1 0 <= z_330 <= 1 0 <= z_331 <= 1 0 <= z_332 <= 1 0 <= z_333 <= 1 0 <= z_334 <= 1 0 <= z_335 <= 1 0 <= z_336 <= 1 0 <= z_337 <= 1 0 <= z_338 <= 1 0 <= z_339 <= 1 0 <= z_340 <= 1 0 <= z_341 <= 1 0 <= z_342 <= 1 0 <= z_343 <= 1 0 <= z_344 <= 1 0 <= z_345 <= 1 0 <= z_346 <= 1 0 <= z_347 <= 1 0 <= z_348 <= 1 0 <= z_349 <= 1 0 <= z_350 <= 1 0 <= z_351 <= 1 0 <= z_352 <= 1 0 <= z_353 <= 1 0 <= z_354 <= 1 0 <= z_355 <= 1 0 <= z_356 <= 1 0 <= z_357 <= 1 0 <= z_358 <= 1 0 <= z_359 <= 1 0 <= z_360 <= 1 0 <= z_361 <= 1 0 <= z_362 <= 1 0 <= z_363 <= 1 0 <= z_364 <= 1 0 <= z_365 <= 1 0 <= z_366 <= 1 0 <= z_367 <= 1 0 <= z_368 <= 1 0 <= z_369 <= 1 0 <= z_370 <= 1 0 <= z_371 <= 1 0 <= z_372 <= 1 0 <= z_373 <= 1 0 <= z_374 <= 1 0 <= z_375 <= 1 0 <= z_376 <= 1 0 <= z_377 <= 1 0 <= z_378 <= 1 0 <= z_379 <= 1 0 <= z_380 <= 1 0 <= z_381 <= 1 0 <= z_382 <= 1 0 <= z_383 <= 1 0 <= z_384 <= 1 0 <= z_385 <= 1 0 <= z_386 <= 1 0 <= z_387 <= 1 0 <= z_388 <= 1 0 <= z_389 <= 1 0 <= z_390 <= 1 0 <= z_391 <= 1 0 <= z_392 <= 1 0 <= z_393 <= 1 0 <= z_394 <= 1 0 <= z_395 <= 1 0 <= z_396 <= 1 0 <= z_397 <= 1 0 <= z_398 <= 1 0 <= z_399 <= 1 0 <= z_400 <= 1 0 <= z_401 <= 1 0 <= z_402 <= 1 0 <= z_403 <= 1 0 <= z_404 <= 1 0 <= z_405 <= 1 0 <= z_406 <= 1 0 <= z_407 <= 1 0 <= z_408 <= 1 0 <= z_409 <= 1 0 <= z_410 <= 1 0 <= z_411 <= 1 0 <= z_412 <= 1 0 <= z_413 <= 1 0 <= z_414 <= 1 0 <= z_415 <= 1 0 <= z_416 <= 1 0 <= z_417 <= 1 0 <= z_418 <= 1 0 <= z_419 <= 1 0 <= z_420 <= 1 0 <= z_421 <= 1 0 <= z_422 <= 1 0 <= z_423 <= 1 0 <= z_424 <= 1 0 <= z_425 <= 1 0 <= z_426 <= 1 0 <= z_427 <= 1 0 <= z_428 <= 1 0 <= z_429 <= 1 0 <= z_430 <= 1 0 <= z_431 <= 1 0 <= z_432 <= 1 0 <= z_433 <= 1 0 <= z_434 <= 1 0 <= z_435 <= 1 0 <= z_436 <= 1 0 <= z_437 <= 1 0 <= z_438 <= 1 0 <= z_439 <= 1 0 <= z_440 <= 1 0 <= z_441 <= 1 0 <= z_442 <= 1 0 <= z_443 <= 1 0 <= z_444 <= 1 0 <= z_445 <= 1 0 <= z_446 <= 1 0 <= z_447 <= 1 0 <= z_448 <= 1 0 <= z_449 <= 1 0 <= z_450 <= 1 0 <= z_451 <= 1 0 <= z_452 <= 1 0 <= z_453 <= 1 0 <= z_454 <= 1 0 <= z_455 <= 1 0 <= z_456 <= 1 0 <= z_457 <= 1 0 <= z_458 <= 1 0 <= z_459 <= 1 0 <= z_460 <= 1 0 <= z_461 <= 1 0 <= z_462 <= 1 0 <= z_463 <= 1 0 <= z_464 <= 1 0 <= z_465 <= 1 0 <= z_466 <= 1 0 <= z_467 <= 1 0 <= z_468 <= 1 0 <= z_469 <= 1 0 <= z_470 <= 1 0 <= z_471 <= 1 0 <= z_472 <= 1 0 <= z_473 <= 1 0 <= z_474 <= 1 0 <= z_475 <= 1 0 <= z_476 <= 1 0 <= z_477 <= 1 0 <= z_478 <= 1 0 <= z_479 <= 1 0 <= z_480 <= 1 0 <= z_481 <= 1 0 <= z_482 <= 1 0 <= z_483 <= 1 0 <= z_484 <= 1 0 <= z_485 <= 1 0 <= z_486 <= 1 0 <= z_487 <= 1 0 <= z_488 <= 1 0 <= z_489 <= 1 0 <= z_490 <= 1 0 <= z_491 <= 1 0 <= z_492 <= 1 0 <= z_493 <= 1 0 <= z_494 <= 1 0 <= z_495 <= 1 0 <= z_496 <= 1 0 <= z_497 <= 1 0 <= z_498 <= 1 0 <= z_499 <= 1 0 <= z_500 <= 1 0 <= z_501 <= 1 0 <= z_502 <= 1 0 <= z_503 <= 1 0 <= z_504 <= 1 0 <= z_505 <= 1 0 <= z_506 <= 1 0 <= z_507 <= 1 0 <= z_508 <= 1 0 <= z_509 <= 1 0 <= z_510 <= 1 0 <= z_511 <= 1 0 <= z_512 <= 1 0 <= z_513 <= 1 0 <= z_514 <= 1 0 <= z_515 <= 1 0 <= z_516 <= 1 0 <= z_517 <= 1 0 <= z_518 <= 1 0 <= z_519 <= 1 0 <= z_520 <= 1 0 <= z_521 <= 1 0 <= z_522 <= 1 0 <= z_523 <= 1 0 <= z_524 <= 1 0 <= z_525 <= 1 0 <= z_526 <= 1 0 <= z_527 <= 1 0 <= z_528 <= 1 0 <= z_529 <= 1 0 <= z_530 <= 1 0 <= z_531 <= 1 0 <= z_532 <= 1 0 <= z_533 <= 1 0 <= z_534 <= 1 0 <= z_535 <= 1 0 <= z_536 <= 1 0 <= z_537 <= 1 0 <= z_538 <= 1 0 <= z_539 <= 1 0 <= z_540 <= 1 0 <= z_541 <= 1 0 <= z_542 <= 1 0 <= z_543 <= 1 0 <= z_544 <= 1 0 <= z_545 <= 1 0 <= z_546 <= 1 0 <= z_547 <= 1 0 <= z_548 <= 1 0 <= z_549 <= 1 0 <= z_550 <= 1 0 <= z_551 <= 1 0 <= z_552 <= 1 0 <= z_553 <= 1 0 <= z_554 <= 1 0 <= z_555 <= 1 0 <= z_556 <= 1 0 <= z_557 <= 1 0 <= z_558 <= 1 0 <= z_559 <= 1 0 <= z_560 <= 1 0 <= z_561 <= 1 0 <= z_562 <= 1 0 <= z_563 <= 1 0 <= z_564 <= 1 0 <= z_565 <= 1 0 <= z_566 <= 1 0 <= z_567 <= 1 0 <= z_568 <= 1 0 <= z_569 <= 1 0 <= z_570 <= 1 0 <= z_571 <= 1 0 <= z_572 <= 1 0 <= z_573 <= 1 0 <= z_574 <= 1 0 <= z_575 <= 1 0 <= z_576 <= 1 0 <= z_577 <= 1 0 <= z_578 <= 1 0 <= z_579 <= 1 0 <= z_580 <= 1 0 <= z_581 <= 1 0 <= z_582 <= 1 0 <= z_583 <= 1 0 <= z_584 <= 1 0 <= z_585 <= 1 0 <= z_586 <= 1 0 <= z_587 <= 1 0 <= z_588 <= 1 0 <= z_589 <= 1 0 <= z_590 <= 1 0 <= z_591 <= 1 0 <= z_592 <= 1 0 <= z_593 <= 1 0 <= z_594 <= 1 0 <= z_595 <= 1 0 <= z_596 <= 1 0 <= z_597 <= 1 0 <= z_598 <= 1 0 <= z_599 <= 1 0 <= z_600 <= 1 0 <= z_601 <= 1 0 <= z_602 <= 1 0 <= z_603 <= 1 0 <= z_604 <= 1 0 <= z_605 <= 1 0 <= z_606 <= 1 0 <= z_607 <= 1 0 <= z_608 <= 1 0 <= z_609 <= 1 0 <= z_610 <= 1 0 <= z_611 <= 1 0 <= z_612 <= 1 0 <= z_613 <= 1 0 <= z_614 <= 1 0 <= z_615 <= 1 0 <= z_616 <= 1 0 <= z_617 <= 1 0 <= z_618 <= 1 0 <= z_619 <= 1 0 <= z_620 <= 1 0 <= z_621 <= 1 0 <= z_622 <= 1 0 <= z_623 <= 1 0 <= z_624 <= 1 0 <= z_625 <= 1 0 <= z_626 <= 1 0 <= z_627 <= 1 0 <= z_628 <= 1 0 <= z_629 <= 1 0 <= z_630 <= 1 0 <= z_631 <= 1 0 <= z_632 <= 1 0 <= z_633 <= 1 0 <= z_634 <= 1 0 <= z_635 <= 1 0 <= z_636 <= 1 0 <= z_637 <= 1 0 <= z_638 <= 1 0 <= z_639 <= 1 0 <= z_640 <= 1 0 <= z_641 <= 1 0 <= z_642 <= 1 0 <= z_643 <= 1 0 <= z_644 <= 1 0 <= z_645 <= 1 0 <= z_646 <= 1 0 <= z_647 <= 1 0 <= z_648 <= 1 0 <= z_649 <= 1 0 <= z_650 <= 1 0 <= z_651 <= 1 0 <= z_652 <= 1 0 <= z_653 <= 1 0 <= z_654 <= 1 0 <= z_655 <= 1 0 <= z_656 <= 1 0 <= z_657 <= 1 0 <= z_658 <= 1 0 <= z_659 <= 1 0 <= z_660 <= 1 0 <= z_661 <= 1 0 <= z_662 <= 1 0 <= z_663 <= 1 0 <= z_664 <= 1 0 <= z_665 <= 1 0 <= z_666 <= 1 0 <= z_667 <= 1 0 <= z_668 <= 1 0 <= z_669 <= 1 0 <= z_670 <= 1 0 <= z_671 <= 1 0 <= z_672 <= 1 0 <= z_673 <= 1 0 <= z_674 <= 1 0 <= z_675 <= 1 0 <= z_676 <= 1 0 <= z_677 <= 1 0 <= z_678 <= 1 0 <= z_679 <= 1 0 <= z_680 <= 1 0 <= z_681 <= 1 0 <= z_682 <= 1 0 <= z_683 <= 1 0 <= z_684 <= 1 0 <= z_685 <= 1 0 <= z_686 <= 1 0 <= z_687 <= 1 0 <= z_688 <= 1 0 <= z_689 <= 1 0 <= z_690 <= 1 0 <= z_691 <= 1 0 <= z_692 <= 1 0 <= z_693 <= 1 0 <= z_694 <= 1 0 <= z_695 <= 1 0 <= z_696 <= 1 0 <= z_697 <= 1 0 <= z_698 <= 1 0 <= z_699 <= 1 0 <= z_700 <= 1 0 <= z_701 <= 1 0 <= z_702 <= 1 0 <= z_703 <= 1 0 <= z_704 <= 1 0 <= z_705 <= 1 0 <= z_706 <= 1 0 <= z_707 <= 1 0 <= z_708 <= 1 0 <= z_709 <= 1 0 <= z_710 <= 1 0 <= z_711 <= 1 0 <= z_712 <= 1 0 <= z_713 <= 1 0 <= z_714 <= 1 0 <= z_715 <= 1 0 <= z_716 <= 1 0 <= z_717 <= 1 0 <= z_718 <= 1 0 <= z_719 <= 1 0 <= z_720 <= 1 0 <= z_721 <= 1 0 <= z_722 <= 1 0 <= z_723 <= 1 0 <= z_724 <= 1 0 <= z_725 <= 1 0 <= z_726 <= 1 0 <= z_727 <= 1 0 <= z_728 <= 1 0 <= z_729 <= 1 0 <= z_730 <= 1 0 <= z_731 <= 1 0 <= z_732 <= 1 0 <= z_733 <= 1 0 <= z_734 <= 1 0 <= z_735 <= 1 0 <= z_736 <= 1 0 <= z_737 <= 1 0 <= z_738 <= 1 0 <= z_739 <= 1 0 <= z_740 <= 1 0 <= z_741 <= 1 0 <= z_742 <= 1 0 <= z_743 <= 1 0 <= z_744 <= 1 0 <= z_745 <= 1 0 <= z_746 <= 1 0 <= z_747 <= 1 0 <= z_748 <= 1 0 <= z_749 <= 1 0 <= z_750 <= 1 0 <= z_751 <= 1 0 <= z_752 <= 1 0 <= z_753 <= 1 0 <= z_754 <= 1 0 <= z_755 <= 1 0 <= z_756 <= 1 0 <= z_757 <= 1 0 <= z_758 <= 1 0 <= z_759 <= 1 0 <= z_760 <= 1 0 <= z_761 <= 1 0 <= z_762 <= 1 0 <= z_763 <= 1 0 <= z_764 <= 1 0 <= z_765 <= 1 0 <= z_766 <= 1 0 <= z_767 <= 1 0 <= z_768 <= 1 0 <= z_769 <= 1 0 <= z_770 <= 1 0 <= z_771 <= 1 0 <= z_772 <= 1 0 <= z_773 <= 1 0 <= z_774 <= 1 0 <= z_775 <= 1 0 <= z_776 <= 1 0 <= z_777 <= 1 0 <= z_778 <= 1 0 <= z_779 <= 1 0 <= z_780 <= 1 0 <= z_781 <= 1 0 <= z_782 <= 1 0 <= z_783 <= 1 0 <= z_784 <= 1 0 <= z_785 <= 1 0 <= z_786 <= 1 0 <= z_787 <= 1 0 <= z_788 <= 1 0 <= z_789 <= 1 0 <= z_790 <= 1 0 <= z_791 <= 1 0 <= z_792 <= 1 0 <= z_793 <= 1 0 <= z_794 <= 1 0 <= z_795 <= 1 0 <= z_796 <= 1 0 <= z_797 <= 1 0 <= z_798 <= 1 0 <= z_799 <= 1 0 <= z_800 <= 1 0 <= z_801 <= 1 0 <= z_802 <= 1 0 <= z_803 <= 1 0 <= z_804 <= 1 0 <= z_805 <= 1 0 <= z_806 <= 1 0 <= z_807 <= 1 0 <= z_808 <= 1 0 <= z_809 <= 1 0 <= z_810 <= 1 0 <= z_811 <= 1 0 <= z_812 <= 1 0 <= z_813 <= 1 0 <= z_814 <= 1 0 <= z_815 <= 1 0 <= z_816 <= 1 0 <= z_817 <= 1 0 <= z_818 <= 1 0 <= z_819 <= 1 0 <= z_820 <= 1 0 <= z_821 <= 1 0 <= z_822 <= 1 0 <= z_823 <= 1 0 <= z_824 <= 1 0 <= z_825 <= 1 0 <= z_826 <= 1 0 <= z_827 <= 1 0 <= z_828 <= 1 0 <= z_829 <= 1 0 <= z_830 <= 1 0 <= z_831 <= 1 0 <= z_832 <= 1 0 <= z_833 <= 1 0 <= z_834 <= 1 0 <= z_835 <= 1 0 <= z_836 <= 1 0 <= z_837 <= 1 0 <= z_838 <= 1 0 <= z_839 <= 1 0 <= z_840 <= 1 0 <= z_841 <= 1 0 <= z_842 <= 1 0 <= z_843 <= 1 0 <= z_844 <= 1 0 <= z_845 <= 1 0 <= z_846 <= 1 0 <= z_847 <= 1 0 <= z_848 <= 1 0 <= z_849 <= 1 0 <= z_850 <= 1 0 <= z_851 <= 1 0 <= z_852 <= 1 0 <= z_853 <= 1 0 <= z_854 <= 1 0 <= z_855 <= 1 0 <= z_856 <= 1 0 <= z_857 <= 1 0 <= z_858 <= 1 0 <= z_859 <= 1 0 <= z_860 <= 1 0 <= z_861 <= 1 0 <= z_862 <= 1 0 <= z_863 <= 1 0 <= z_864 <= 1 0 <= z_865 <= 1 0 <= z_866 <= 1 0 <= z_867 <= 1 0 <= z_868 <= 1 0 <= z_869 <= 1 0 <= z_870 <= 1 0 <= z_871 <= 1 0 <= z_872 <= 1 0 <= z_873 <= 1 0 <= z_874 <= 1 0 <= z_875 <= 1 0 <= z_876 <= 1 0 <= z_877 <= 1 0 <= z_878 <= 1 0 <= z_879 <= 1 0 <= z_880 <= 1 0 <= z_881 <= 1 0 <= z_882 <= 1 0 <= z_883 <= 1 0 <= z_884 <= 1 0 <= z_885 <= 1 0 <= z_886 <= 1 0 <= z_887 <= 1 0 <= z_888 <= 1 0 <= z_889 <= 1 0 <= z_890 <= 1 0 <= z_891 <= 1 0 <= z_892 <= 1 0 <= z_893 <= 1 0 <= z_894 <= 1 0 <= z_895 <= 1 0 <= z_896 <= 1 0 <= z_897 <= 1 0 <= z_898 <= 1 0 <= z_899 <= 1 0 <= z_900 <= 1 0 <= z_901 <= 1 0 <= z_902 <= 1 0 <= z_903 <= 1 0 <= z_904 <= 1 0 <= z_905 <= 1 0 <= z_906 <= 1 0 <= z_907 <= 1 0 <= z_908 <= 1 0 <= z_909 <= 1 0 <= z_910 <= 1 0 <= z_911 <= 1 0 <= z_912 <= 1 0 <= z_913 <= 1 0 <= z_914 <= 1 0 <= z_915 <= 1 0 <= z_916 <= 1 0 <= z_917 <= 1 0 <= z_918 <= 1 0 <= z_919 <= 1 0 <= z_920 <= 1 0 <= z_921 <= 1 0 <= z_922 <= 1 0 <= z_923 <= 1 0 <= z_924 <= 1 0 <= z_925 <= 1 0 <= z_926 <= 1 0 <= z_927 <= 1 0 <= z_928 <= 1 0 <= z_929 <= 1 0 <= z_930 <= 1 0 <= z_931 <= 1 0 <= z_932 <= 1 0 <= z_933 <= 1 0 <= z_934 <= 1 0 <= z_935 <= 1 0 <= z_936 <= 1 0 <= z_937 <= 1 0 <= z_938 <= 1 0 <= z_939 <= 1 0 <= z_940 <= 1 0 <= z_941 <= 1 0 <= z_942 <= 1 0 <= z_943 <= 1 0 <= z_944 <= 1 0 <= z_945 <= 1 0 <= z_946 <= 1 0 <= z_947 <= 1 0 <= z_948 <= 1 0 <= z_949 <= 1 0 <= z_950 <= 1 0 <= z_951 <= 1 0 <= z_952 <= 1 0 <= z_953 <= 1 0 <= z_954 <= 1 0 <= z_955 <= 1 0 <= z_956 <= 1 0 <= z_957 <= 1 0 <= z_958 <= 1 0 <= z_959 <= 1 0 <= z_960 <= 1 0 <= z_961 <= 1 0 <= z_962 <= 1 0 <= z_963 <= 1 0 <= z_964 <= 1 0 <= z_965 <= 1 0 <= z_966 <= 1 0 <= z_967 <= 1 0 <= z_968 <= 1 0 <= z_969 <= 1 0 <= z_970 <= 1 0 <= z_971 <= 1 0 <= z_972 <= 1 0 <= z_973 <= 1 0 <= z_974 <= 1 0 <= z_975 <= 1 0 <= z_976 <= 1 0 <= z_977 <= 1 0 <= z_978 <= 1 0 <= z_979 <= 1 0 <= z_980 <= 1 0 <= z_981 <= 1 0 <= z_982 <= 1 0 <= z_983 <= 1 0 <= z_984 <= 1 0 <= z_985 <= 1 0 <= z_986 <= 1 0 <= z_987 <= 1 0 <= z_988 <= 1 0 <= z_989 <= 1 0 <= z_990 <= 1 0 <= z_991 <= 1 0 <= z_992 <= 1 0 <= z_993 <= 1 0 <= z_994 <= 1 0 <= z_995 <= 1 0 <= z_996 <= 1 0 <= z_997 <= 1 0 <= z_998 <= 1 0 <= z_999 <= 1 0 <= z_1000 <= 1 0 <= z_1001 <= 1 0 <= z_1002 <= 1 0 <= z_1003 <= 1 0 <= z_1004 <= 1 0 <= z_1005 <= 1 0 <= z_1006 <= 1 0 <= z_1007 <= 1 0 <= z_1008 <= 1 0 <= z_1009 <= 1 0 <= z_1010 <= 1 0 <= z_1011 <= 1 0 <= z_1012 <= 1 0 <= z_1013 <= 1 0 <= z_1014 <= 1 0 <= z_1015 <= 1 0 <= z_1016 <= 1 0 <= z_1017 <= 1 0 <= z_1018 <= 1 0 <= z_1019 <= 1 0 <= z_1020 <= 1 0 <= z_1021 <= 1 0 <= z_1022 <= 1 0 <= z_1023 <= 1 0 <= z_1024 <= 1 0 <= z_1025 <= 1 0 <= z_1026 <= 1 0 <= z_1027 <= 1 0 <= z_1028 <= 1 0 <= z_1029 <= 1 0 <= z_1030 <= 1 0 <= z_1031 <= 1 0 <= z_1032 <= 1 0 <= z_1033 <= 1 0 <= z_1034 <= 1 0 <= z_1035 <= 1 0 <= z_1036 <= 1 0 <= z_1037 <= 1 0 <= z_1038 <= 1 0 <= z_1039 <= 1 0 <= z_1040 <= 1 0 <= z_1041 <= 1 0 <= z_1042 <= 1 0 <= z_1043 <= 1 0 <= z_1044 <= 1 0 <= z_1045 <= 1 0 <= z_1046 <= 1 0 <= z_1047 <= 1 0 <= z_1048 <= 1 0 <= z_1049 <= 1 0 <= z_1050 <= 1 0 <= z_1051 <= 1 0 <= z_1052 <= 1 0 <= z_1053 <= 1 0 <= z_1054 <= 1 0 <= z_1055 <= 1 0 <= z_1056 <= 1 0 <= z_1057 <= 1 0 <= z_1058 <= 1 0 <= z_1059 <= 1 0 <= z_1060 <= 1 0 <= z_1061 <= 1 0 <= z_1062 <= 1 0 <= z_1063 <= 1 0 <= z_1064 <= 1 0 <= z_1065 <= 1 0 <= z_1066 <= 1 0 <= z_1067 <= 1 0 <= z_1068 <= 1 0 <= z_1069 <= 1 0 <= z_1070 <= 1 0 <= z_1071 <= 1 0 <= z_1072 <= 1 0 <= z_1073 <= 1 0 <= z_1074 <= 1 0 <= z_1075 <= 1 0 <= z_1076 <= 1 0 <= z_1077 <= 1 0 <= z_1078 <= 1 0 <= z_1079 <= 1 0 <= z_1080 <= 1 0 <= z_1081 <= 1 0 <= z_1082 <= 1 0 <= z_1083 <= 1 0 <= z_1084 <= 1 0 <= z_1085 <= 1 0 <= z_1086 <= 1 0 <= z_1087 <= 1 0 <= z_1088 <= 1 0 <= z_1089 <= 1 0 <= z_1090 <= 1 0 <= z_1091 <= 1 0 <= z_1092 <= 1 0 <= z_1093 <= 1 0 <= z_1094 <= 1 0 <= z_1095 <= 1 0 <= z_1096 <= 1 0 <= z_1097 <= 1 0 <= z_1098 <= 1 0 <= z_1099 <= 1 0 <= z_1100 <= 1 0 <= z_1101 <= 1 0 <= z_1102 <= 1 0 <= z_1103 <= 1 0 <= z_1104 <= 1 0 <= z_1105 <= 1 0 <= z_1106 <= 1 0 <= z_1107 <= 1 0 <= z_1108 <= 1 0 <= z_1109 <= 1 0 <= z_1110 <= 1 0 <= z_1111 <= 1 0 <= z_1112 <= 1 0 <= z_1113 <= 1 0 <= z_1114 <= 1 0 <= z_1115 <= 1 0 <= z_1116 <= 1 0 <= z_1117 <= 1 0 <= z_1118 <= 1 0 <= z_1119 <= 1 0 <= z_1120 <= 1 0 <= z_1121 <= 1 0 <= z_1122 <= 1 0 <= z_1123 <= 1 0 <= z_1124 <= 1 0 <= z_1125 <= 1 0 <= z_1126 <= 1 0 <= z_1127 <= 1 0 <= z_1128 <= 1 0 <= z_1129 <= 1 0 <= z_1130 <= 1 0 <= z_1131 <= 1 0 <= z_1132 <= 1 0 <= z_1133 <= 1 0 <= z_1134 <= 1 0 <= z_1135 <= 1 0 <= z_1136 <= 1 0 <= z_1137 <= 1 0 <= z_1138 <= 1 0 <= z_1139 <= 1 0 <= z_1140 <= 1 0 <= z_1141 <= 1 0 <= z_1142 <= 1 0 <= z_1143 <= 1 0 <= z_1144 <= 1 0 <= z_1145 <= 1 0 <= z_1146 <= 1 0 <= z_1147 <= 1 0 <= z_1148 <= 1 0 <= z_1149 <= 1 0 <= z_1150 <= 1 0 <= z_1151 <= 1 0 <= z_1152 <= 1 0 <= z_1153 <= 1 0 <= z_1154 <= 1 0 <= z_1155 <= 1 0 <= z_1156 <= 1 0 <= z_1157 <= 1 0 <= z_1158 <= 1 0 <= z_1159 <= 1 0 <= z_1160 <= 1 0 <= z_1161 <= 1 0 <= z_1162 <= 1 0 <= z_1163 <= 1 0 <= z_1164 <= 1 0 <= z_1165 <= 1 0 <= z_1166 <= 1 0 <= z_1167 <= 1 0 <= z_1168 <= 1 0 <= z_1169 <= 1 0 <= z_1170 <= 1 0 <= z_1171 <= 1 0 <= z_1172 <= 1 0 <= z_1173 <= 1 0 <= z_1174 <= 1 0 <= z_1175 <= 1 0 <= z_1176 <= 1 0 <= z_1177 <= 1 0 <= z_1178 <= 1 0 <= z_1179 <= 1 0 <= z_1180 <= 1 0 <= z_1181 <= 1 0 <= z_1182 <= 1 0 <= z_1183 <= 1 0 <= z_1184 <= 1 0 <= z_1185 <= 1 0 <= z_1186 <= 1 0 <= z_1187 <= 1 0 <= z_1188 <= 1 0 <= z_1189 <= 1 0 <= z_1190 <= 1 0 <= z_1191 <= 1 0 <= z_1192 <= 1 0 <= z_1193 <= 1 0 <= z_1194 <= 1 0 <= z_1195 <= 1 0 <= z_1196 <= 1 0 <= z_1197 <= 1 0 <= z_1198 <= 1 0 <= z_1199 <= 1 0 <= z_1200 <= 1 0 <= z_1201 <= 1 0 <= z_1202 <= 1 0 <= z_1203 <= 1 0 <= z_1204 <= 1 0 <= z_1205 <= 1 0 <= z_1206 <= 1 0 <= z_1207 <= 1 0 <= z_1208 <= 1 0 <= z_1209 <= 1 0 <= z_1210 <= 1 0 <= z_1211 <= 1 0 <= z_1212 <= 1 0 <= z_1213 <= 1 0 <= z_1214 <= 1 0 <= z_1215 <= 1 x_1216 free x_1217 free x_1218 free x_1219 free x_1220 free x_1221 free x_1222 free x_1223 free x_1224 free x_1225 free x_1226 free x_1227 free x_1228 free x_1229 free x_1230 free x_1231 free x_1232 free x_1233 free x_1234 free x_1235 free x_1236 free x_1237 free x_1238 free x_1239 free x_1240 free x_1241 free x_1242 free x_1243 free x_1244 free x_1245 free x_1246 free x_1247 free x_1248 free x_1249 free x_1250 free x_1251 free x_1252 free x_1253 free x_1254 free x_1255 free x_1256 free x_1257 free x_1258 free x_1259 free x_1260 free x_1261 free x_1262 free x_1263 free x_1264 free x_1265 free x_1266 free x_1267 free x_1268 free x_1269 free x_1270 free x_1271 free x_1272 free x_1273 free x_1274 free x_1275 free x_1276 free x_1277 free x_1278 free x_1279 free x_1280 free x_1281 free x_1282 free x_1283 free x_1284 free x_1285 free x_1286 free x_1287 free x_1288 free x_1289 free x_1290 free x_1291 free x_1292 free x_1293 free x_1294 free x_1295 free x_1296 free x_1297 free x_1298 free x_1299 free x_1300 free x_1301 free x_1302 free x_1303 free x_1304 free x_1305 free x_1306 free x_1307 free x_1308 free x_1309 free x_1310 free x_1311 free x_1312 free x_1313 free x_1314 free x_1315 free x_1316 free x_1317 free x_1318 free x_1319 free x_1320 free x_1321 free x_1322 free x_1323 free x_1324 free x_1325 free x_1326 free x_1327 free x_1328 free x_1329 free x_1330 free x_1331 free x_1332 free x_1333 free x_1334 free x_1335 free x_1336 free x_1337 free x_1338 free x_1339 free x_1340 free x_1341 free x_1342 free x_1343 free x_1344 free x_1345 free x_1346 free x_1347 free x_1348 free x_1349 free x_1350 free x_1351 free x_1352 free x_1353 free x_1354 free x_1355 free Generals z_1 z_2 z_3 z_4 z_5 z_6 z_7 z_8 z_9 z_10 z_11 z_12 z_13 z_14 z_15 z_16 z_17 z_18 z_19 z_20 z_21 z_22 z_23 z_24 z_25 z_26 z_27 z_28 z_29 z_30 z_31 z_32 z_33 z_34 z_35 z_36 z_37 z_38 z_39 z_40 z_41 z_42 z_43 z_44 z_45 z_46 z_47 z_48 z_49 z_50 z_51 z_52 z_53 z_54 z_55 z_56 z_57 z_58 z_59 z_60 z_61 z_62 z_63 z_64 z_65 z_66 z_67 z_68 z_69 z_70 z_71 z_72 z_73 z_74 z_75 z_76 z_77 z_78 z_79 z_80 z_81 z_82 z_83 z_84 z_85 z_86 z_87 z_88 z_89 z_90 z_91 z_92 z_93 z_94 z_95 z_96 z_97 z_98 z_99 z_100 z_101 z_102 z_103 z_104 z_105 z_106 z_107 z_108 z_109 z_110 z_111 z_112 z_113 z_114 z_115 z_116 z_117 z_118 z_119 z_120 z_121 z_122 z_123 z_124 z_125 z_126 z_127 z_128 z_129 z_130 z_131 z_132 z_133 z_134 z_135 z_136 z_137 z_138 z_139 z_140 z_141 z_142 z_143 z_144 z_145 z_146 z_147 z_148 z_149 z_150 z_151 z_152 z_153 z_154 z_155 z_156 z_157 z_158 z_159 z_160 z_161 z_162 z_163 z_164 z_165 z_166 z_167 z_168 z_169 z_170 z_171 z_172 z_173 z_174 z_175 z_176 z_177 z_178 z_179 z_180 z_181 z_182 z_183 z_184 z_185 z_186 z_187 z_188 z_189 z_190 z_191 z_192 z_193 z_194 z_195 z_196 z_197 z_198 z_199 z_200 z_201 z_202 z_203 z_204 z_205 z_206 z_207 z_208 z_209 z_210 z_211 z_212 z_213 z_214 z_215 z_216 z_217 z_218 z_219 z_220 z_221 z_222 z_223 z_224 z_225 z_226 z_227 z_228 z_229 z_230 z_231 z_232 z_233 z_234 z_235 z_236 z_237 z_238 z_239 z_240 z_241 z_242 z_243 z_244 z_245 z_246 z_247 z_248 z_249 z_250 z_251 z_252 z_253 z_254 z_255 z_256 z_257 z_258 z_259 z_260 z_261 z_262 z_263 z_264 z_265 z_266 z_267 z_268 z_269 z_270 z_271 z_272 z_273 z_274 z_275 z_276 z_277 z_278 z_279 z_280 z_281 z_282 z_283 z_284 z_285 z_286 z_287 z_288 z_289 z_290 z_291 z_292 z_293 z_294 z_295 z_296 z_297 z_298 z_299 z_300 z_301 z_302 z_303 z_304 z_305 z_306 z_307 z_308 z_309 z_310 z_311 z_312 z_313 z_314 z_315 z_316 z_317 z_318 z_319 z_320 z_321 z_322 z_323 z_324 z_325 z_326 z_327 z_328 z_329 z_330 z_331 z_332 z_333 z_334 z_335 z_336 z_337 z_338 z_339 z_340 z_341 z_342 z_343 z_344 z_345 z_346 z_347 z_348 z_349 z_350 z_351 z_352 z_353 z_354 z_355 z_356 z_357 z_358 z_359 z_360 z_361 z_362 z_363 z_364 z_365 z_366 z_367 z_368 z_369 z_370 z_371 z_372 z_373 z_374 z_375 z_376 z_377 z_378 z_379 z_380 z_381 z_382 z_383 z_384 z_385 z_386 z_387 z_388 z_389 z_390 z_391 z_392 z_393 z_394 z_395 z_396 z_397 z_398 z_399 z_400 z_401 z_402 z_403 z_404 z_405 z_406 z_407 z_408 z_409 z_410 z_411 z_412 z_413 z_414 z_415 z_416 z_417 z_418 z_419 z_420 z_421 z_422 z_423 z_424 z_425 z_426 z_427 z_428 z_429 z_430 z_431 z_432 z_433 z_434 z_435 z_436 z_437 z_438 z_439 z_440 z_441 z_442 z_443 z_444 z_445 z_446 z_447 z_448 z_449 z_450 z_451 z_452 z_453 z_454 z_455 z_456 z_457 z_458 z_459 z_460 z_461 z_462 z_463 z_464 z_465 z_466 z_467 z_468 z_469 z_470 z_471 z_472 z_473 z_474 z_475 z_476 z_477 z_478 z_479 z_480 z_481 z_482 z_483 z_484 z_485 z_486 z_487 z_488 z_489 z_490 z_491 z_492 z_493 z_494 z_495 z_496 z_497 z_498 z_499 z_500 z_501 z_502 z_503 z_504 z_505 z_506 z_507 z_508 z_509 z_510 z_511 z_512 z_513 z_514 z_515 z_516 z_517 z_518 z_519 z_520 z_521 z_522 z_523 z_524 z_525 z_526 z_527 z_528 z_529 z_530 z_531 z_532 z_533 z_534 z_535 z_536 z_537 z_538 z_539 z_540 z_541 z_542 z_543 z_544 z_545 z_546 z_547 z_548 z_549 z_550 z_551 z_552 z_553 z_554 z_555 z_556 z_557 z_558 z_559 z_560 z_561 z_562 z_563 z_564 z_565 z_566 z_567 z_568 z_569 z_570 z_571 z_572 z_573 z_574 z_575 z_576 z_577 z_578 z_579 z_580 z_581 z_582 z_583 z_584 z_585 z_586 z_587 z_588 z_589 z_590 z_591 z_592 z_593 z_594 z_595 z_596 z_597 z_598 z_599 z_600 z_601 z_602 z_603 z_604 z_605 z_606 z_607 z_608 z_609 z_610 z_611 z_612 z_613 z_614 z_615 z_616 z_617 z_618 z_619 z_620 z_621 z_622 z_623 z_624 z_625 z_626 z_627 z_628 z_629 z_630 z_631 z_632 z_633 z_634 z_635 z_636 z_637 z_638 z_639 z_640 z_641 z_642 z_643 z_644 z_645 z_646 z_647 z_648 z_649 z_650 z_651 z_652 z_653 z_654 z_655 z_656 z_657 z_658 z_659 z_660 z_661 z_662 z_663 z_664 z_665 z_666 z_667 z_668 z_669 z_670 z_671 z_672 z_673 z_674 z_675 z_676 z_677 z_678 z_679 z_680 z_681 z_682 z_683 z_684 z_685 z_686 z_687 z_688 z_689 z_690 z_691 z_692 z_693 z_694 z_695 z_696 z_697 z_698 z_699 z_700 z_701 z_702 z_703 z_704 z_705 z_706 z_707 z_708 z_709 z_710 z_711 z_712 z_713 z_714 z_715 z_716 z_717 z_718 z_719 z_720 z_721 z_722 z_723 z_724 z_725 z_726 z_727 z_728 z_729 z_730 z_731 z_732 z_733 z_734 z_735 z_736 z_737 z_738 z_739 z_740 z_741 z_742 z_743 z_744 z_745 z_746 z_747 z_748 z_749 z_750 z_751 z_752 z_753 z_754 z_755 z_756 z_757 z_758 z_759 z_760 z_761 z_762 z_763 z_764 z_765 z_766 z_767 z_768 z_769 z_770 z_771 z_772 z_773 z_774 z_775 z_776 z_777 z_778 z_779 z_780 z_781 z_782 z_783 z_784 z_785 z_786 z_787 z_788 z_789 z_790 z_791 z_792 z_793 z_794 z_795 z_796 z_797 z_798 z_799 z_800 z_801 z_802 z_803 z_804 z_805 z_806 z_807 z_808 z_809 z_810 z_811 z_812 z_813 z_814 z_815 z_816 z_817 z_818 z_819 z_820 z_821 z_822 z_823 z_824 z_825 z_826 z_827 z_828 z_829 z_830 z_831 z_832 z_833 z_834 z_835 z_836 z_837 z_838 z_839 z_840 z_841 z_842 z_843 z_844 z_845 z_846 z_847 z_848 z_849 z_850 z_851 z_852 z_853 z_854 z_855 z_856 z_857 z_858 z_859 z_860 z_861 z_862 z_863 z_864 z_865 z_866 z_867 z_868 z_869 z_870 z_871 z_872 z_873 z_874 z_875 z_876 z_877 z_878 z_879 z_880 z_881 z_882 z_883 z_884 z_885 z_886 z_887 z_888 z_889 z_890 z_891 z_892 z_893 z_894 z_895 z_896 z_897 z_898 z_899 z_900 z_901 z_902 z_903 z_904 z_905 z_906 z_907 z_908 z_909 z_910 z_911 z_912 z_913 z_914 z_915 z_916 z_917 z_918 z_919 z_920 z_921 z_922 z_923 z_924 z_925 z_926 z_927 z_928 z_929 z_930 z_931 z_932 z_933 z_934 z_935 z_936 z_937 z_938 z_939 z_940 z_941 z_942 z_943 z_944 z_945 z_946 z_947 z_948 z_949 z_950 z_951 z_952 z_953 z_954 z_955 z_956 z_957 z_958 z_959 z_960 z_961 z_962 z_963 z_964 z_965 z_966 z_967 z_968 z_969 z_970 z_971 z_972 z_973 z_974 z_975 z_976 z_977 z_978 z_979 z_980 z_981 z_982 z_983 z_984 z_985 z_986 z_987 z_988 z_989 z_990 z_991 z_992 z_993 z_994 z_995 z_996 z_997 z_998 z_999 z_1000 z_1001 z_1002 z_1003 z_1004 z_1005 z_1006 z_1007 z_1008 z_1009 z_1010 z_1011 z_1012 z_1013 z_1014 z_1015 z_1016 z_1017 z_1018 z_1019 z_1020 z_1021 z_1022 z_1023 z_1024 z_1025 z_1026 z_1027 z_1028 z_1029 z_1030 z_1031 z_1032 z_1033 z_1034 z_1035 z_1036 z_1037 z_1038 z_1039 z_1040 z_1041 z_1042 z_1043 z_1044 z_1045 z_1046 z_1047 z_1048 z_1049 z_1050 z_1051 z_1052 z_1053 z_1054 z_1055 z_1056 z_1057 z_1058 z_1059 z_1060 z_1061 z_1062 z_1063 z_1064 z_1065 z_1066 z_1067 z_1068 z_1069 z_1070 z_1071 z_1072 z_1073 z_1074 z_1075 z_1076 z_1077 z_1078 z_1079 z_1080 z_1081 z_1082 z_1083 z_1084 z_1085 z_1086 z_1087 z_1088 z_1089 z_1090 z_1091 z_1092 z_1093 z_1094 z_1095 z_1096 z_1097 z_1098 z_1099 z_1100 z_1101 z_1102 z_1103 z_1104 z_1105 z_1106 z_1107 z_1108 z_1109 z_1110 z_1111 z_1112 z_1113 z_1114 z_1115 z_1116 z_1117 z_1118 z_1119 z_1120 z_1121 z_1122 z_1123 z_1124 z_1125 z_1126 z_1127 z_1128 z_1129 z_1130 z_1131 z_1132 z_1133 z_1134 z_1135 z_1136 z_1137 z_1138 z_1139 z_1140 z_1141 z_1142 z_1143 z_1144 z_1145 z_1146 z_1147 z_1148 z_1149 z_1150 z_1151 z_1152 z_1153 z_1154 z_1155 z_1156 z_1157 z_1158 z_1159 z_1160 z_1161 z_1162 z_1163 z_1164 z_1165 z_1166 z_1167 z_1168 z_1169 z_1170 z_1171 z_1172 z_1173 z_1174 z_1175 z_1176 z_1177 z_1178 z_1179 z_1180 z_1181 z_1182 z_1183 z_1184 z_1185 z_1186 z_1187 z_1188 z_1189 z_1190 z_1191 z_1192 z_1193 z_1194 z_1195 z_1196 z_1197 z_1198 z_1199 z_1200 z_1201 z_1202 z_1203 z_1204 z_1205 z_1206 z_1207 z_1208 z_1209 z_1210 z_1211 z_1212 z_1213 z_1214 z_1215 End