From a9281777ccc1ec6085c68373fe68e64480cb7d1f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 19 Mar 2014 15:48:05 -0700 Subject: [PATCH] test for SLS Signed-off-by: Nikolaj Bjorner --- tests/wmax1.smt2 | 5842 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 5842 insertions(+) create mode 100644 tests/wmax1.smt2 diff --git a/tests/wmax1.smt2 b/tests/wmax1.smt2 new file mode 100644 index 000000000..602309e95 --- /dev/null +++ b/tests/wmax1.smt2 @@ -0,0 +1,5842 @@ +(declare-fun x_354 () Int) +(declare-fun x_522 () Int) +(declare-fun x_464 () Int) +(declare-fun x_644 () Int) +(declare-fun x_174 () Int) +(declare-fun x_397 () Int) +(declare-fun x_432 () Int) +(declare-fun x_557 () Int) +(declare-fun x_926 () Int) +(declare-fun x_582 () Int) +(declare-fun x_779 () Int) +(declare-fun x_759 () Int) +(declare-fun x_912 () Int) +(declare-fun x_868 () Int) +(declare-fun x_384 () Int) +(declare-fun x_963 () Int) +(declare-fun x_658 () Int) +(declare-fun x_362 () Int) +(declare-fun x_984 () Int) +(declare-fun x_308 () Int) +(declare-fun x_456 () Int) +(declare-fun x_17 () Int) +(declare-fun x_816 () Int) +(declare-fun x_833 () Int) +(declare-fun x_463 () Int) +(declare-fun x_211 () Int) +(declare-fun x_607 () Int) +(declare-fun x_139 () Int) +(declare-fun x_124 () Int) +(declare-fun x_291 () Int) +(declare-fun x_859 () Int) +(declare-fun x_888 () Int) +(declare-fun x_31 () Int) +(declare-fun x_472 () Int) +(declare-fun x_434 () Int) +(declare-fun x_154 () Int) +(declare-fun x_347 () Int) +(declare-fun x_88 () Int) +(declare-fun x_769 () Int) +(declare-fun x_986 () Int) +(declare-fun x_8 () Int) +(declare-fun x_196 () Int) +(declare-fun x_882 () Int) +(declare-fun x_711 () Int) +(declare-fun x_167 () Int) +(declare-fun x_119 () Int) +(declare-fun x_4 () Int) +(declare-fun x_33 () Int) +(declare-fun x_178 () Int) +(declare-fun x_893 () Int) +(declare-fun x_429 () Int) +(declare-fun x_527 () Int) +(declare-fun x_194 () Int) +(declare-fun x_498 () Int) +(declare-fun x_346 () Int) +(declare-fun x_712 () Int) +(declare-fun x_691 () Int) +(declare-fun x_294 () Int) +(declare-fun x_402 () Int) +(declare-fun x_213 () Int) +(declare-fun x_239 () Int) +(declare-fun x_297 () Int) +(declare-fun x_427 () Int) +(declare-fun x_489 () Int) +(declare-fun x_841 () Int) +(declare-fun x_186 () Int) +(declare-fun x_149 () Int) +(declare-fun x_586 () Int) +(declare-fun x_932 () Int) +(declare-fun x_367 () Int) +(declare-fun x_77 () Int) +(declare-fun x_123 () Int) +(declare-fun x_884 () Int) +(declare-fun x_989 () Int) +(declare-fun x_242 () Int) +(declare-fun x_614 () Int) +(declare-fun x_381 () Int) +(declare-fun x_388 () Int) +(declare-fun x_306 () Int) +(declare-fun x_737 () Int) +(declare-fun x_277 () Int) +(declare-fun x_966 () Int) +(declare-fun x_67 () Int) +(declare-fun x_678 () Int) +(declare-fun x_87 () Int) +(declare-fun x_496 () Int) +(declare-fun x_919 () Int) +(declare-fun x_439 () Int) +(declare-fun x_854 () Int) +(declare-fun x_961 () Int) +(declare-fun x_697 () Int) +(declare-fun x_19 () Int) +(declare-fun x_818 () Int) +(declare-fun x_158 () Int) +(declare-fun x_26 () Int) +(declare-fun x_436 () Int) +(declare-fun x_798 () Int) +(declare-fun x_457 () Int) +(declare-fun x_838 () Int) +(declare-fun x_953 () Int) +(declare-fun x_524 () Int) +(declare-fun x_574 () Int) +(declare-fun x_212 () Int) +(declare-fun x_486 () Int) +(declare-fun x_3 () Int) +(declare-fun x_256 () Int) +(declare-fun x_22 () Int) +(declare-fun x_676 () Int) +(declare-fun x_789 () Int) +(declare-fun x_892 () Int) +(declare-fun x_682 () Int) +(declare-fun x_84 () Int) +(declare-fun x_819 () Int) +(declare-fun x_454 () Int) +(declare-fun x_59 () Int) +(declare-fun x_227 () Int) +(declare-fun x_572 () Int) +(declare-fun x_914 () Int) +(declare-fun x_39 () Int) +(declare-fun x_679 () Int) +(declare-fun x_824 () Int) +(declare-fun x_684 () Int) +(declare-fun x_221 () Int) +(declare-fun x_274 () Int) +(declare-fun x_32 () Int) +(declare-fun x_348 () Int) +(declare-fun x_877 () Int) +(declare-fun x_701 () Int) +(declare-fun x_231 () Int) +(declare-fun x_549 () Int) +(declare-fun x_889 () Int) +(declare-fun x_879 () Int) +(declare-fun x_662 () Int) +(declare-fun x_302 () Int) +(declare-fun x_979 () Int) +(declare-fun x_861 () Int) +(declare-fun x_973 () Int) +(declare-fun x_401 () Int) +(declare-fun x_537 () Int) +(declare-fun x_972 () Int) +(declare-fun x_269 () Int) +(declare-fun x_957 () Int) +(declare-fun x_271 () Int) +(declare-fun x_363 () Int) +(declare-fun x_181 () Int) +(declare-fun x_357 () Int) +(declare-fun x_591 () Int) +(declare-fun x_559 () Int) +(declare-fun x_51 () Int) +(declare-fun x_916 () Int) +(declare-fun x_389 () Int) +(declare-fun x_512 () Int) +(declare-fun x_988 () Int) +(declare-fun x_667 () Int) +(declare-fun x_511 () Int) +(declare-fun x_733 () Int) +(declare-fun x_821 () Int) +(declare-fun x_671 () Int) +(declare-fun x_707 () Int) +(declare-fun x_826 () Int) +(declare-fun x_319 () Int) +(declare-fun x_399 () Int) +(declare-fun x_852 () Int) +(declare-fun x_442 () Int) +(declare-fun x_108 () Int) +(declare-fun x_392 () Int) +(declare-fun x_776 () Int) +(declare-fun x_993 () Int) +(declare-fun x_459 () Int) +(declare-fun x_913 () Int) +(declare-fun x_107 () Int) +(declare-fun x_994 () Int) +(declare-fun x_61 () Int) +(declare-fun x_802 () Int) +(declare-fun x_677 () Int) +(declare-fun x_857 () Int) +(declare-fun x_706 () Int) +(declare-fun x_278 () Int) +(declare-fun x_443 () Int) +(declare-fun x_813 () Int) +(declare-fun x_971 () Int) +(declare-fun x_173 () Int) +(declare-fun x_91 () Int) +(declare-fun x_396 () Int) +(declare-fun x_551 () Int) +(declare-fun x_846 () Int) +(declare-fun x_417 () Int) +(declare-fun x_54 () Int) +(declare-fun x_721 () Int) +(declare-fun x_331 () Int) +(declare-fun x_467 () Int) +(declare-fun x_553 () Int) +(declare-fun x_959 () Int) +(declare-fun x_871 () Int) +(declare-fun x_692 () Int) +(declare-fun x_792 () Int) +(declare-fun x_593 () Int) +(declare-fun x_412 () Int) +(declare-fun x_531 () Int) +(declare-fun x_352 () Int) +(declare-fun x_333 () Int) +(declare-fun x_596 () Int) +(declare-fun x_229 () Int) +(declare-fun x_447 () Int) +(declare-fun x_53 () Int) +(declare-fun x_548 () Int) +(declare-fun x_43 () Int) +(declare-fun x_13 () Int) +(declare-fun x_198 () Int) +(declare-fun x_47 () Int) +(declare-fun x_626 () Int) +(declare-fun x_648 () Int) +(declare-fun x_902 () Int) +(declare-fun x_594 () Int) +(declare-fun x_113 () Int) +(declare-fun x_286 () Int) +(declare-fun x_163 () Int) +(declare-fun x_157 () Int) +(declare-fun x_659 () Int) +(declare-fun x_24 () Int) +(declare-fun x_631 () Int) +(declare-fun x_699 () Int) +(declare-fun x_366 () Int) +(declare-fun x_6 () Int) +(declare-fun x_156 () Int) +(declare-fun x_876 () Int) +(declare-fun x_598 () Int) +(declare-fun x_974 () Int) +(declare-fun x_372 () Int) +(declare-fun x_538 () Int) +(declare-fun x_287 () Int) +(declare-fun x_71 () Int) +(declare-fun x_371 () Int) +(declare-fun x_646 () Int) +(declare-fun x_519 () Int) +(declare-fun x_121 () Int) +(declare-fun x_268 () Int) +(declare-fun x_746 () Int) +(declare-fun x_562 () Int) +(declare-fun x_799 () Int) +(declare-fun x_423 () Int) +(declare-fun x_808 () Int) +(declare-fun x_303 () Int) +(declare-fun x_536 () Int) +(declare-fun x_344 () Int) +(declare-fun x_322 () Int) +(declare-fun x_299 () Int) +(declare-fun x_976 () Int) +(declare-fun x_279 () Int) +(declare-fun x_482 () Int) +(declare-fun x_246 () Int) +(declare-fun x_763 () Int) +(declare-fun x_111 () Int) +(declare-fun x_226 () Int) +(declare-fun x_741 () Int) +(declare-fun x_188 () Int) +(declare-fun x_873 () Int) +(declare-fun x_767 () Int) +(declare-fun x_766 () Int) +(declare-fun x_7 () Int) +(declare-fun x_377 () Int) +(declare-fun x_719 () Int) +(declare-fun x_704 () Int) +(declare-fun x_72 () Int) +(declare-fun x_27 () Int) +(declare-fun x_284 () Int) +(declare-fun x_943 () Int) +(declare-fun x_42 () Int) +(declare-fun x_881 () Int) +(declare-fun x_693 () Int) +(declare-fun x_422 () Int) +(declare-fun x_218 () Int) +(declare-fun x_736 () Int) +(declare-fun x_817 () Int) +(declare-fun x_168 () Int) +(declare-fun x_359 () Int) +(declare-fun x_16 () Int) +(declare-fun x_469 () Int) +(declare-fun x_814 () Int) +(declare-fun x_62 () Int) +(declare-fun x_461 () Int) +(declare-fun x_483 () Int) +(declare-fun x_68 () Int) +(declare-fun x_786 () Int) +(declare-fun x_938 () Int) +(declare-fun x_204 () Int) +(declare-fun x_718 () Int) +(declare-fun x_197 () Int) +(declare-fun x_603 () Int) +(declare-fun x_616 () Int) +(declare-fun x_117 () Int) +(declare-fun x_567 () Int) +(declare-fun x_729 () Int) +(declare-fun x_942 () Int) +(declare-fun x_748 () Int) +(declare-fun x_992 () Int) +(declare-fun x_713 () Int) +(declare-fun x_326 () Int) +(declare-fun x_689 () Int) +(declare-fun x_948 () Int) +(declare-fun x_717 () Int) +(declare-fun x_403 () Int) +(declare-fun x_872 () Int) +(declare-fun x_73 () Int) +(declare-fun x_639 () Int) +(declare-fun x_137 () Int) +(declare-fun x_373 () Int) +(declare-fun x_364 () Int) +(declare-fun x_576 () Int) +(declare-fun x_358 () Int) +(declare-fun x_466 () Int) +(declare-fun x_122 () Int) +(declare-fun x_637 () Int) +(declare-fun x_202 () Int) +(declare-fun x_476 () Int) +(declare-fun x_44 () Int) +(declare-fun x_151 () Int) +(declare-fun x_253 () Int) +(declare-fun x_696 () Int) +(declare-fun x_822 () Int) +(declare-fun x_641 () Int) +(declare-fun x_924 () Int) +(declare-fun x_233 () Int) +(declare-fun x_136 () Int) +(declare-fun x_222 () Int) +(declare-fun x_318 () Int) +(declare-fun x_694 () Int) +(declare-fun x_543 () Int) +(declare-fun x_141 () Int) +(declare-fun x_418 () Int) +(declare-fun x_409 () Int) +(declare-fun x_601 () Int) +(declare-fun x_339 () Int) +(declare-fun x_958 () Int) +(declare-fun x_773 () Int) +(declare-fun x_448 () Int) +(declare-fun x_508 () Int) +(declare-fun x_104 () Int) +(declare-fun x_674 () Int) +(declare-fun x_991 () Int) +(declare-fun x_406 () Int) +(declare-fun x_283 () Int) +(declare-fun x_552 () Int) +(declare-fun x_907 () Int) +(declare-fun x_408 () Int) +(declare-fun x_451 () Int) +(declare-fun x_897 () Int) +(declare-fun x_503 () Int) +(declare-fun x_672 () Int) +(declare-fun x_264 () Int) +(declare-fun x_382 () Int) +(declare-fun x_554 () Int) +(declare-fun x_561 () Int) +(declare-fun x_11 () Int) +(declare-fun x_329 () Int) +(declare-fun x_727 () Int) +(declare-fun x_97 () Int) +(declare-fun x_343 () Int) +(declare-fun x_918 () Int) +(declare-fun x_289 () Int) +(declare-fun x_803 () Int) +(declare-fun x_812 () Int) +(declare-fun x_547 () Int) +(declare-fun x_806 () Int) +(declare-fun x_252 () Int) +(declare-fun x_273 () Int) +(declare-fun x_618 () Int) +(declare-fun x_301 () Int) +(declare-fun x_688 () Int) +(declare-fun x_224 () Int) +(declare-fun x_449 () Int) +(declare-fun x_327 () Int) +(declare-fun x_387 () Int) +(declare-fun x_86 () Int) +(declare-fun x_89 () Int) +(declare-fun x_404 () Int) +(declare-fun x_507 () Int) +(declare-fun x_312 () Int) +(declare-fun x_578 () Int) +(declare-fun x_722 () Int) +(declare-fun x_762 () Int) +(declare-fun x_169 () Int) +(declare-fun x_206 () Int) +(declare-fun x_383 () Int) +(declare-fun x_867 () Int) +(declare-fun x_627 () Int) +(declare-fun x_638 () Int) +(declare-fun x_184 () Int) +(declare-fun x_479 () Int) +(declare-fun x_292 () Int) +(declare-fun x_844 () Int) +(declare-fun x_421 () Int) +(declare-fun x_911 () Int) +(declare-fun x_419 () Int) +(declare-fun x_612 () Int) +(declare-fun x_192 () Int) +(declare-fun x_656 () Int) +(declare-fun x_702 () Int) +(declare-fun x_778 () Int) +(declare-fun x_281 () Int) +(declare-fun x_834 () Int) +(declare-fun x_63 () Int) +(declare-fun x_836 () Int) +(declare-fun x_793 () Int) +(declare-fun x_622 () Int) +(declare-fun x_899 () Int) +(declare-fun x_944 () Int) +(declare-fun x_369 () Int) +(declare-fun x_336 () Int) +(declare-fun x_869 () Int) +(declare-fun x_257 () Int) +(declare-fun x_1001 () Int) +(declare-fun x_904 () Int) +(declare-fun x_528 () Int) +(declare-fun x_997 () Int) +(declare-fun x_414 () Int) +(declare-fun x_223 () Int) +(declare-fun x_642 () Int) +(declare-fun x_76 () Int) +(declare-fun x_29 () Int) +(declare-fun x_533 () Int) +(declare-fun x_41 () Int) +(declare-fun x_581 () Int) +(declare-fun x_791 () Int) +(declare-fun x_809 () Int) +(declare-fun x_321 () Int) +(declare-fun x_939 () Int) +(declare-fun x_541 () Int) +(declare-fun x_652 () Int) +(declare-fun x_569 () Int) +(declare-fun x_934 () Int) +(declare-fun x_207 () Int) +(declare-fun x_376 () Int) +(declare-fun x_109 () Int) +(declare-fun x_761 () Int) +(declare-fun x_446 () Int) +(declare-fun x_657 () Int) +(declare-fun x_171 () Int) +(declare-fun x_558 () Int) +(declare-fun x_276 () Int) +(declare-fun x_46 () Int) +(declare-fun x_668 () Int) +(declare-fun x_57 () Int) +(declare-fun x_374 () Int) +(declare-fun x_209 () Int) +(declare-fun x_739 () Int) +(declare-fun x_909 () Int) +(declare-fun x_468 () Int) +(declare-fun x_14 () Int) +(declare-fun x_832 () Int) +(declare-fun x_391 () Int) +(declare-fun x_517 () Int) +(declare-fun x_12 () Int) +(declare-fun x_244 () Int) +(declare-fun x_628 () Int) +(declare-fun x_334 () Int) +(declare-fun x_502 () Int) +(declare-fun x_883 () Int) +(declare-fun x_379 () Int) +(declare-fun x_307 () Int) +(declare-fun x_182 () Int) +(declare-fun x_293 () Int) +(declare-fun x_288 () Int) +(declare-fun x_633 () Int) +(declare-fun x_866 () Int) +(declare-fun x_571 () Int) +(declare-fun x_842 () Int) +(declare-fun x_921 () Int) +(declare-fun x_797 () Int) +(declare-fun x_153 () Int) +(declare-fun x_398 () Int) +(declare-fun x_583 () Int) +(declare-fun x_683 () Int) +(declare-fun x_189 () Int) +(declare-fun x_964 () Int) +(declare-fun x_164 () Int) +(declare-fun x_474 () Int) +(declare-fun x_521 () Int) +(declare-fun x_21 () Int) +(declare-fun x_518 () Int) +(declare-fun x_473 () Int) +(declare-fun x_896 () Int) +(declare-fun x_796 () Int) +(declare-fun x_477 () Int) +(declare-fun x_74 () Int) +(declare-fun x_116 () Int) +(declare-fun x_837 () Int) +(declare-fun x_673 () Int) +(declare-fun x_309 () Int) +(declare-fun x_58 () Int) +(declare-fun x_428 () Int) +(declare-fun x_589 () Int) +(declare-fun x_747 () Int) +(declare-fun x_929 () Int) +(declare-fun x_529 () Int) +(declare-fun x_413 () Int) +(declare-fun x_847 () Int) +(declare-fun x_262 () Int) +(declare-fun x_801 () Int) +(declare-fun x_952 () Int) +(declare-fun x_632 () Int) +(declare-fun x_142 () Int) +(declare-fun x_491 () Int) +(declare-fun x_546 () Int) +(declare-fun x_839 () Int) +(declare-fun x_588 () Int) +(declare-fun x_393 () Int) +(declare-fun x_118 () Int) +(declare-fun x_901 () Int) +(declare-fun x_962 () Int) +(declare-fun x_968 () Int) +(declare-fun x_886 () Int) +(declare-fun x_774 () Int) +(declare-fun x_487 () Int) +(declare-fun x_127 () Int) +(declare-fun x_237 () Int) +(declare-fun x_723 () Int) +(declare-fun x_542 () Int) +(declare-fun x_753 () Int) +(declare-fun x_129 () Int) +(declare-fun x_864 () Int) +(declare-fun x_611 () Int) +(declare-fun x_416 () Int) +(declare-fun x_947 () Int) +(declare-fun x_1202 () Int) +(declare-fun x_563 () Int) +(declare-fun x_337 () Int) +(declare-fun x_544 () Int) +(declare-fun x_654 () Int) +(declare-fun x_756 () Int) +(declare-fun x_744 () Int) +(declare-fun x_891 () Int) +(declare-fun x_378 () Int) +(declare-fun x_134 () Int) +(declare-fun x_208 () Int) +(declare-fun x_758 () Int) +(declare-fun x_848 () Int) +(declare-fun x_927 () Int) +(declare-fun x_937 () Int) +(declare-fun x_602 () Int) +(declare-fun x_349 () Int) +(declare-fun x_96 () Int) +(declare-fun x_162 () Int) +(declare-fun x_37 () Int) +(declare-fun x_941 () Int) +(declare-fun x_906 () Int) +(declare-fun x_811 () Int) +(declare-fun x_138 () Int) +(declare-fun x_621 () Int) +(declare-fun x_492 () Int) +(declare-fun x_764 () Int) +(declare-fun x_452 () Int) +(declare-fun x_851 () Int) +(declare-fun x_98 () Int) +(declare-fun x_236 () Int) +(declare-fun x_453 () Int) +(declare-fun x_978 () Int) +(declare-fun x_499 () Int) +(declare-fun x_494 () Int) +(declare-fun x_316 () Int) +(declare-fun x_587 () Int) +(declare-fun x_103 () Int) +(declare-fun x_734 () Int) +(declare-fun x_923 () Int) +(declare-fun x_228 () Int) +(declare-fun x_504 () Int) +(declare-fun x_564 () Int) +(declare-fun x_592 () Int) +(declare-fun x_2 () Int) +(declare-fun x_539 () Int) +(declare-fun x_247 () Int) +(declare-fun x_931 () Int) +(declare-fun x_903 () Int) +(declare-fun x_64 () Int) +(declare-fun x_232 () Int) +(declare-fun x_298 () Int) +(declare-fun x_126 () Int) +(declare-fun x_787 () Int) +(declare-fun x_243 () Int) +(declare-fun x_356 () Int) +(declare-fun x_709 () Int) +(declare-fun x_823 () Int) +(declare-fun x_338 () Int) +(declare-fun x_201 () Int) +(declare-fun x_304 () Int) +(declare-fun x_101 () Int) +(declare-fun x_568 () Int) +(declare-fun x_573 () Int) +(declare-fun x_28 () Int) +(declare-fun x_516 () Int) +(declare-fun x_619 () Int) +(declare-fun x_102 () Int) +(declare-fun x_92 () Int) +(declare-fun x_604 () Int) +(declare-fun x_597 () Int) +(declare-fun x_663 () Int) +(declare-fun x_731 () Int) +(declare-fun x_328 () Int) +(declare-fun x_143 () Int) +(declare-fun x_849 () Int) +(declare-fun x_128 () Int) +(declare-fun x_266 () Int) +(declare-fun x_203 () Int) +(declare-fun x_661 () Int) +(declare-fun x_996 () Int) +(declare-fun x_462 () Int) +(declare-fun x_977 () Int) +(declare-fun x_458 () Int) +(declare-fun x_933 () Int) +(declare-fun x_94 () Int) +(declare-fun x_332 () Int) +(declare-fun x_514 () Int) +(declare-fun x_969 () Int) +(declare-fun x_987 () Int) +(declare-fun x_497 () Int) +(declare-fun x_666 () Int) +(declare-fun x_858 () Int) +(declare-fun x_643 () Int) +(declare-fun x_523 () Int) +(declare-fun x_609 () Int) +(declare-fun x_263 () Int) +(declare-fun x_878 () Int) +(declare-fun x_981 () Int) +(declare-fun x_863 () Int) +(declare-fun x_324 () Int) +(declare-fun x_783 () Int) +(declare-fun x_241 () Int) +(declare-fun x_407 () Int) +(declare-fun x_708 () Int) +(declare-fun x_862 () Int) +(declare-fun x_757 () Int) +(declare-fun x_251 () Int) +(declare-fun x_771 () Int) +(declare-fun x_478 () Int) +(declare-fun x_437 () Int) +(declare-fun x_267 () Int) +(declare-fun x_599 () Int) +(declare-fun x_234 () Int) +(declare-fun x_177 () Int) +(declare-fun x_726 () Int) +(declare-fun x_261 () Int) +(declare-fun x_353 () Int) +(declare-fun x_732 () Int) +(declare-fun x_908 () Int) +(declare-fun x_361 () Int) +(declare-fun x_887 () Int) +(declare-fun x_488 () Int) +(declare-fun x_917 () Int) +(declare-fun x_716 () Int) +(declare-fun x_166 () Int) +(declare-fun x_112 () Int) +(declare-fun x_629 () Int) +(declare-fun x_52 () Int) +(declare-fun x_34 () Int) +(declare-fun x_183 () Int) +(declare-fun x_999 () Int) +(declare-fun x_99 () Int) +(declare-fun x_444 () Int) +(declare-fun x_424 () Int) +(declare-fun x_317 () Int) +(declare-fun x_784 () Int) +(declare-fun x_584 () Int) +(declare-fun x_282 () Int) +(declare-fun x_743 () Int) +(declare-fun x_56 () Int) +(declare-fun x_749 () Int) +(declare-fun x_411 () Int) +(declare-fun x_647 () Int) +(declare-fun x_219 () Int) +(declare-fun x_946 () Int) +(declare-fun x_433 () Int) +(declare-fun x_106 () Int) +(declare-fun x_38 () Int) +(declare-fun x_314 () Int) +(declare-fun x_481 () Int) +(declare-fun x_768 () Int) +(declare-fun x_579 () Int) +(declare-fun x_114 () Int) +(declare-fun x_894 () Int) +(declare-fun x_146 () Int) +(declare-fun x_577 () Int) +(declare-fun x_394 () Int) +(declare-fun x_566 () Int) +(declare-fun x_738 () Int) +(declare-fun x_506 () Int) +(declare-fun x_351 () Int) +(declare-fun x_493 () Int) +(declare-fun x_624 () Int) +(declare-fun x_653 () Int) +(declare-fun x_386 () Int) +(declare-fun x_526 () Int) +(declare-fun x_148 () Int) +(declare-fun x_131 () Int) +(declare-fun x_669 () Int) +(declare-fun x_982 () Int) +(declare-fun x_664 () Int) +(declare-fun x_501 () Int) +(declare-fun x_856 () Int) +(declare-fun x_828 () Int) +(declare-fun x_161 () Int) +(declare-fun x_772 () Int) +(declare-fun x_147 () Int) +(declare-fun x_967 () Int) +(declare-fun x_313 () Int) +(declare-fun x_681 () Int) +(declare-fun x_724 () Int) +(declare-fun x_636 () Int) +(declare-fun x_83 () Int) +(declare-fun x_754 () Int) +(declare-fun x_484 () Int) +(declare-fun x_49 () Int) +(declare-fun x_703 () Int) +(declare-fun x_36 () Int) +(declare-fun x_152 () Int) +(declare-fun x_187 () Int) +(declare-fun x_752 () Int) +(declare-fun x_191 () Int) +(declare-fun x_634 () Int) +(declare-fun x_788 () Int) +(declare-fun x_259 () Int) +(declare-fun x_431 () Int) +(declare-fun x_509 () Int) +(declare-fun x_93 () Int) +(declare-fun x_9 () Int) +(declare-fun x_513 () Int) +(declare-fun x_248 () Int) +(declare-fun x_272 () Int) +(declare-fun x_751 () Int) +(declare-fun x_686 () Int) +(declare-fun x_714 () Int) +(declare-fun x_807 () Int) +(declare-fun x_922 () Int) +(declare-fun x_81 () Int) +(declare-fun x_613 () Int) +(declare-fun x_928 () Int) +(declare-fun x_1604 () Int) +(declare-fun x_78 () Int) +(declare-fun x_249 () Int) +(declare-fun x_79 () Int) +(declare-fun x_649 () Int) +(declare-fun x_781 () Int) +(declare-fun x_687 () Int) +(declare-fun x_82 () Int) +(declare-fun x_804 () Int) +(declare-fun x_441 () Int) +(declare-fun x_651 () Int) +(declare-fun x_936 () Int) +(declare-fun x_1 () Int) +(declare-fun x_179 () Int) +(declare-fun x_199 () Int) +(declare-fun x_623 () Int) +(declare-fun x_794 () Int) +(declare-fun x_777 () Int) +(declare-fun x_214 () Int) +(declare-fun x_296 () Int) +(declare-fun x_949 () Int) +(declare-fun x_133 () Int) +(declare-fun x_829 () Int) +(declare-fun x_556 () Int) +(declare-fun x_617 () Int) +(declare-fun x_18 () Int) +(declare-fun x_728 () Int) +(declare-fun x_426 () Int) +(declare-fun x_898 () Int) +(declare-fun x_23 () Int) +(declare-fun x_843 () Int) +(declare-fun x_827 () Int) +(declare-fun x_831 () Int) +(declare-fun x_954 () Int) +(declare-fun x_341 () Int) +(declare-fun x_956 () Int) +(declare-fun x_983 () Int) +(declare-fun x_606 () Int) +(declare-fun x_874 () Int) +(declare-fun x_698 () Int) +(declare-fun x_782 () Int) +(declare-fun x_48 () Int) +(declare-fun x_172 () Int) +(declare-fun x_342 () Int) +(declare-fun x_238 () Int) +(declare-fun x_323 () Int) +(declare-fun x_608 () Int) +(declare-fun x_471 () Int) +(declare-fun x_216 () Int) +(declare-fun x_69 () Int) +(declare-fun x_438 () Int) +(declare-fun x_534 () Int) +(declare-fun x_368 () Int) +(declare-fun x_193 () Int) +(declare-fun x_532 () Int) +(declare-fun x_951 () Int) +(declare-fun x_258 () Int) +(declare-fun x_853 () Int) +(declare-fun x_132 () Int) +(declare-fun x_159 () Int) +(declare-fun x_217 () Int) +(declare-fun x_742 () Int) +(declare-fun x_311 () Int) +(declare-fun x_1403 () Int) +(declare-fun x_176 () Int) +(declare-fun x_254 () Int) +(declare-fun x_66 () Int) +(declare-fun x_144 () Int) +(declare-fun x_998 () Int) +(assert (<= 0 x_1)) +(assert (>= 1 x_1)) +(assert (<= 0 x_2)) +(assert (>= 1 x_2)) +(assert (<= 0 x_3)) +(assert (>= 1 x_3)) +(assert (<= 0 x_4)) +(assert (>= 1 x_4)) +(assert (<= 0 x_6)) +(assert (>= 1 x_6)) +(assert (<= 0 x_7)) +(assert (>= 1 x_7)) +(assert (<= 0 x_8)) +(assert (>= 1 x_8)) +(assert (<= 0 x_9)) +(assert (>= 1 x_9)) +(assert (<= 0 x_11)) +(assert (>= 1 x_11)) +(assert (<= 0 x_12)) +(assert (>= 1 x_12)) +(assert (<= 0 x_13)) +(assert (>= 1 x_13)) +(assert (<= 0 x_14)) +(assert (>= 1 x_14)) +(assert (<= 0 x_16)) +(assert (>= 1 x_16)) +(assert (<= 0 x_17)) +(assert (>= 1 x_17)) +(assert (<= 0 x_18)) +(assert (>= 1 x_18)) +(assert (<= 0 x_19)) +(assert (>= 1 x_19)) +(assert (<= 0 x_21)) +(assert (>= 1 x_21)) +(assert (<= 0 x_22)) +(assert (>= 1 x_22)) +(assert (<= 0 x_23)) +(assert (>= 1 x_23)) +(assert (<= 0 x_24)) +(assert (>= 1 x_24)) +(assert (<= 0 x_26)) +(assert (>= 1 x_26)) +(assert (<= 0 x_27)) +(assert (>= 1 x_27)) +(assert (<= 0 x_28)) +(assert (>= 1 x_28)) +(assert (<= 0 x_29)) +(assert (>= 1 x_29)) +(assert (<= 0 x_31)) +(assert (>= 1 x_31)) +(assert (<= 0 x_32)) +(assert (>= 1 x_32)) +(assert (<= 0 x_33)) +(assert (>= 1 x_33)) +(assert (<= 0 x_34)) +(assert (>= 1 x_34)) +(assert (<= 0 x_36)) +(assert (>= 1 x_36)) +(assert (<= 0 x_37)) +(assert (>= 1 x_37)) +(assert (<= 0 x_38)) +(assert (>= 1 x_38)) +(assert (<= 0 x_39)) +(assert (>= 1 x_39)) +(assert (<= 0 x_41)) +(assert (>= 1 x_41)) +(assert (<= 0 x_42)) +(assert (>= 1 x_42)) +(assert (<= 0 x_43)) +(assert (>= 1 x_43)) +(assert (<= 0 x_44)) +(assert (>= 1 x_44)) +(assert (<= 0 x_46)) +(assert (>= 1 x_46)) +(assert (<= 0 x_47)) +(assert (>= 1 x_47)) +(assert (<= 0 x_48)) +(assert (>= 1 x_48)) +(assert (<= 0 x_49)) +(assert (>= 1 x_49)) +(assert (<= 0 x_51)) +(assert (>= 1 x_51)) +(assert (<= 0 x_52)) +(assert (>= 1 x_52)) +(assert (<= 0 x_53)) +(assert (>= 1 x_53)) +(assert (<= 0 x_54)) +(assert (>= 1 x_54)) +(assert (<= 0 x_56)) +(assert (>= 1 x_56)) +(assert (<= 0 x_57)) +(assert (>= 1 x_57)) +(assert (<= 0 x_58)) +(assert (>= 1 x_58)) +(assert (<= 0 x_59)) +(assert (>= 1 x_59)) +(assert (<= 0 x_61)) +(assert (>= 1 x_61)) +(assert (<= 0 x_62)) +(assert (>= 1 x_62)) +(assert (<= 0 x_63)) +(assert (>= 1 x_63)) +(assert (<= 0 x_64)) +(assert (>= 1 x_64)) +(assert (<= 0 x_66)) +(assert (>= 1 x_66)) +(assert (<= 0 x_67)) +(assert (>= 1 x_67)) +(assert (<= 0 x_68)) +(assert (>= 1 x_68)) +(assert (<= 0 x_69)) +(assert (>= 1 x_69)) +(assert (<= 0 x_71)) +(assert (>= 1 x_71)) +(assert (<= 0 x_72)) +(assert (>= 1 x_72)) +(assert (<= 0 x_73)) +(assert (>= 1 x_73)) +(assert (<= 0 x_74)) +(assert (>= 1 x_74)) +(assert (<= 0 x_76)) +(assert (>= 1 x_76)) +(assert (<= 0 x_77)) +(assert (>= 1 x_77)) +(assert (<= 0 x_78)) +(assert (>= 1 x_78)) +(assert (<= 0 x_79)) +(assert (>= 1 x_79)) +(assert (<= 0 x_81)) +(assert (>= 1 x_81)) +(assert (<= 0 x_82)) +(assert (>= 1 x_82)) +(assert (<= 0 x_83)) +(assert (>= 1 x_83)) +(assert (<= 0 x_84)) +(assert (>= 1 x_84)) +(assert (<= 0 x_86)) +(assert (>= 1 x_86)) +(assert (<= 0 x_87)) +(assert (>= 1 x_87)) +(assert (<= 0 x_88)) +(assert (>= 1 x_88)) +(assert (<= 0 x_89)) +(assert (>= 1 x_89)) +(assert (<= 0 x_91)) +(assert (>= 1 x_91)) +(assert (<= 0 x_92)) +(assert (>= 1 x_92)) +(assert (<= 0 x_93)) +(assert (>= 1 x_93)) +(assert (<= 0 x_94)) +(assert (>= 1 x_94)) +(assert (<= 0 x_96)) +(assert (>= 1 x_96)) +(assert (<= 0 x_97)) +(assert (>= 1 x_97)) +(assert (<= 0 x_98)) +(assert (>= 1 x_98)) +(assert (<= 0 x_99)) +(assert (>= 1 x_99)) +(assert (<= 0 x_101)) +(assert (>= 1 x_101)) +(assert (<= 0 x_102)) +(assert (>= 1 x_102)) +(assert (<= 0 x_103)) +(assert (>= 1 x_103)) +(assert (<= 0 x_104)) +(assert (>= 1 x_104)) +(assert (<= 0 x_106)) +(assert (>= 1 x_106)) +(assert (<= 0 x_107)) +(assert (>= 1 x_107)) +(assert (<= 0 x_108)) +(assert (>= 1 x_108)) +(assert (<= 0 x_109)) +(assert (>= 1 x_109)) +(assert (<= 0 x_111)) +(assert (>= 1 x_111)) +(assert (<= 0 x_112)) +(assert (>= 1 x_112)) +(assert (<= 0 x_113)) +(assert (>= 1 x_113)) +(assert (<= 0 x_114)) +(assert (>= 1 x_114)) +(assert (<= 0 x_116)) +(assert (>= 1 x_116)) +(assert (<= 0 x_117)) +(assert (>= 1 x_117)) +(assert (<= 0 x_118)) +(assert (>= 1 x_118)) +(assert (<= 0 x_119)) +(assert (>= 1 x_119)) +(assert (<= 0 x_121)) +(assert (>= 1 x_121)) +(assert (<= 0 x_122)) +(assert (>= 1 x_122)) +(assert (<= 0 x_123)) +(assert (>= 1 x_123)) +(assert (<= 0 x_124)) +(assert (>= 1 x_124)) +(assert (<= 0 x_126)) +(assert (>= 1 x_126)) +(assert (<= 0 x_127)) +(assert (>= 1 x_127)) +(assert (<= 0 x_128)) +(assert (>= 1 x_128)) +(assert (<= 0 x_129)) +(assert (>= 1 x_129)) +(assert (<= 0 x_131)) +(assert (>= 1 x_131)) +(assert (<= 0 x_132)) +(assert (>= 1 x_132)) +(assert (<= 0 x_133)) +(assert (>= 1 x_133)) +(assert (<= 0 x_134)) +(assert (>= 1 x_134)) +(assert (<= 0 x_136)) +(assert (>= 1 x_136)) +(assert (<= 0 x_137)) +(assert (>= 1 x_137)) +(assert (<= 0 x_138)) +(assert (>= 1 x_138)) +(assert (<= 0 x_139)) +(assert (>= 1 x_139)) +(assert (<= 0 x_141)) +(assert (>= 1 x_141)) +(assert (<= 0 x_142)) +(assert (>= 1 x_142)) +(assert (<= 0 x_143)) +(assert (>= 1 x_143)) +(assert (<= 0 x_144)) +(assert (>= 1 x_144)) +(assert (<= 0 x_146)) +(assert (>= 1 x_146)) +(assert (<= 0 x_147)) +(assert (>= 1 x_147)) +(assert (<= 0 x_148)) +(assert (>= 1 x_148)) +(assert (<= 0 x_149)) +(assert (>= 1 x_149)) +(assert (<= 0 x_151)) +(assert (>= 1 x_151)) +(assert (<= 0 x_152)) +(assert (>= 1 x_152)) +(assert (<= 0 x_153)) +(assert (>= 1 x_153)) +(assert (<= 0 x_154)) +(assert (>= 1 x_154)) +(assert (<= 0 x_156)) +(assert (>= 1 x_156)) +(assert (<= 0 x_157)) +(assert (>= 1 x_157)) +(assert (<= 0 x_158)) +(assert (>= 1 x_158)) +(assert (<= 0 x_159)) +(assert (>= 1 x_159)) +(assert (<= 0 x_161)) +(assert (>= 1 x_161)) +(assert (<= 0 x_162)) +(assert (>= 1 x_162)) +(assert (<= 0 x_163)) +(assert (>= 1 x_163)) +(assert (<= 0 x_164)) +(assert (>= 1 x_164)) +(assert (<= 0 x_166)) +(assert (>= 1 x_166)) +(assert (<= 0 x_167)) +(assert (>= 1 x_167)) +(assert (<= 0 x_168)) +(assert (>= 1 x_168)) +(assert (<= 0 x_169)) +(assert (>= 1 x_169)) +(assert (<= 0 x_171)) +(assert (>= 1 x_171)) +(assert (<= 0 x_172)) +(assert (>= 1 x_172)) +(assert (<= 0 x_173)) +(assert (>= 1 x_173)) +(assert (<= 0 x_174)) +(assert (>= 1 x_174)) +(assert (<= 0 x_176)) +(assert (>= 1 x_176)) +(assert (<= 0 x_177)) +(assert (>= 1 x_177)) +(assert (<= 0 x_178)) +(assert (>= 1 x_178)) +(assert (<= 0 x_179)) +(assert (>= 1 x_179)) +(assert (<= 0 x_181)) +(assert (>= 1 x_181)) +(assert (<= 0 x_182)) +(assert (>= 1 x_182)) +(assert (<= 0 x_183)) +(assert (>= 1 x_183)) +(assert (<= 0 x_184)) +(assert (>= 1 x_184)) +(assert (<= 0 x_186)) +(assert (>= 1 x_186)) +(assert (<= 0 x_187)) +(assert (>= 1 x_187)) +(assert (<= 0 x_188)) +(assert (>= 1 x_188)) +(assert (<= 0 x_189)) +(assert (>= 1 x_189)) +(assert (<= 0 x_191)) +(assert (>= 1 x_191)) +(assert (<= 0 x_192)) +(assert (>= 1 x_192)) +(assert (<= 0 x_193)) +(assert (>= 1 x_193)) +(assert (<= 0 x_194)) +(assert (>= 1 x_194)) +(assert (<= 0 x_196)) +(assert (>= 1 x_196)) +(assert (<= 0 x_197)) +(assert (>= 1 x_197)) +(assert (<= 0 x_198)) +(assert (>= 1 x_198)) +(assert (<= 0 x_199)) +(assert (>= 1 x_199)) +(assert (<= 0 x_201)) +(assert (>= 1 x_201)) +(assert (<= 0 x_202)) +(assert (>= 1 x_202)) +(assert (<= 0 x_203)) +(assert (>= 1 x_203)) +(assert (<= 0 x_204)) +(assert (>= 1 x_204)) +(assert (<= 0 x_206)) +(assert (>= 1 x_206)) +(assert (<= 0 x_207)) +(assert (>= 1 x_207)) +(assert (<= 0 x_208)) +(assert (>= 1 x_208)) +(assert (<= 0 x_209)) +(assert (>= 1 x_209)) +(assert (<= 0 x_211)) +(assert (>= 1 x_211)) +(assert (<= 0 x_212)) +(assert (>= 1 x_212)) +(assert (<= 0 x_213)) +(assert (>= 1 x_213)) +(assert (<= 0 x_214)) +(assert (>= 1 x_214)) +(assert (<= 0 x_216)) +(assert (>= 1 x_216)) +(assert (<= 0 x_217)) +(assert (>= 1 x_217)) +(assert (<= 0 x_218)) +(assert (>= 1 x_218)) +(assert (<= 0 x_219)) +(assert (>= 1 x_219)) +(assert (<= 0 x_221)) +(assert (>= 1 x_221)) +(assert (<= 0 x_222)) +(assert (>= 1 x_222)) +(assert (<= 0 x_223)) +(assert (>= 1 x_223)) +(assert (<= 0 x_224)) +(assert (>= 1 x_224)) +(assert (<= 0 x_226)) +(assert (>= 1 x_226)) +(assert (<= 0 x_227)) +(assert (>= 1 x_227)) +(assert (<= 0 x_228)) +(assert (>= 1 x_228)) +(assert (<= 0 x_229)) +(assert (>= 1 x_229)) +(assert (<= 0 x_231)) +(assert (>= 1 x_231)) +(assert (<= 0 x_232)) +(assert (>= 1 x_232)) +(assert (<= 0 x_233)) +(assert (>= 1 x_233)) +(assert (<= 0 x_234)) +(assert (>= 1 x_234)) +(assert (<= 0 x_236)) +(assert (>= 1 x_236)) +(assert (<= 0 x_237)) +(assert (>= 1 x_237)) +(assert (<= 0 x_238)) +(assert (>= 1 x_238)) +(assert (<= 0 x_239)) +(assert (>= 1 x_239)) +(assert (<= 0 x_241)) +(assert (>= 1 x_241)) +(assert (<= 0 x_242)) +(assert (>= 1 x_242)) +(assert (<= 0 x_243)) +(assert (>= 1 x_243)) +(assert (<= 0 x_244)) +(assert (>= 1 x_244)) +(assert (<= 0 x_246)) +(assert (>= 1 x_246)) +(assert (<= 0 x_247)) +(assert (>= 1 x_247)) +(assert (<= 0 x_248)) +(assert (>= 1 x_248)) +(assert (<= 0 x_249)) +(assert (>= 1 x_249)) +(assert (<= 0 x_251)) +(assert (>= 1 x_251)) +(assert (<= 0 x_252)) +(assert (>= 1 x_252)) +(assert (<= 0 x_253)) +(assert (>= 1 x_253)) +(assert (<= 0 x_254)) +(assert (>= 1 x_254)) +(assert (<= 0 x_256)) +(assert (>= 1 x_256)) +(assert (<= 0 x_257)) +(assert (>= 1 x_257)) +(assert (<= 0 x_258)) +(assert (>= 1 x_258)) +(assert (<= 0 x_259)) +(assert (>= 1 x_259)) +(assert (<= 0 x_261)) +(assert (>= 1 x_261)) +(assert (<= 0 x_262)) +(assert (>= 1 x_262)) +(assert (<= 0 x_263)) +(assert (>= 1 x_263)) +(assert (<= 0 x_264)) +(assert (>= 1 x_264)) +(assert (<= 0 x_266)) +(assert (>= 1 x_266)) +(assert (<= 0 x_267)) +(assert (>= 1 x_267)) +(assert (<= 0 x_268)) +(assert (>= 1 x_268)) +(assert (<= 0 x_269)) +(assert (>= 1 x_269)) +(assert (<= 0 x_271)) +(assert (>= 1 x_271)) +(assert (<= 0 x_272)) +(assert (>= 1 x_272)) +(assert (<= 0 x_273)) +(assert (>= 1 x_273)) +(assert (<= 0 x_274)) +(assert (>= 1 x_274)) +(assert (<= 0 x_276)) +(assert (>= 1 x_276)) +(assert (<= 0 x_277)) +(assert (>= 1 x_277)) +(assert (<= 0 x_278)) +(assert (>= 1 x_278)) +(assert (<= 0 x_279)) +(assert (>= 1 x_279)) +(assert (<= 0 x_281)) +(assert (>= 1 x_281)) +(assert (<= 0 x_282)) +(assert (>= 1 x_282)) +(assert (<= 0 x_283)) +(assert (>= 1 x_283)) +(assert (<= 0 x_284)) +(assert (>= 1 x_284)) +(assert (<= 0 x_286)) +(assert (>= 1 x_286)) +(assert (<= 0 x_287)) +(assert (>= 1 x_287)) +(assert (<= 0 x_288)) +(assert (>= 1 x_288)) +(assert (<= 0 x_289)) +(assert (>= 1 x_289)) +(assert (<= 0 x_291)) +(assert (>= 1 x_291)) +(assert (<= 0 x_292)) +(assert (>= 1 x_292)) +(assert (<= 0 x_293)) +(assert (>= 1 x_293)) +(assert (<= 0 x_294)) +(assert (>= 1 x_294)) +(assert (<= 0 x_296)) +(assert (>= 1 x_296)) +(assert (<= 0 x_297)) +(assert (>= 1 x_297)) +(assert (<= 0 x_298)) +(assert (>= 1 x_298)) +(assert (<= 0 x_299)) +(assert (>= 1 x_299)) +(assert (<= 0 x_301)) +(assert (>= 1 x_301)) +(assert (<= 0 x_302)) +(assert (>= 1 x_302)) +(assert (<= 0 x_303)) +(assert (>= 1 x_303)) +(assert (<= 0 x_304)) +(assert (>= 1 x_304)) +(assert (<= 0 x_306)) +(assert (>= 1 x_306)) +(assert (<= 0 x_307)) +(assert (>= 1 x_307)) +(assert (<= 0 x_308)) +(assert (>= 1 x_308)) +(assert (<= 0 x_309)) +(assert (>= 1 x_309)) +(assert (<= 0 x_311)) +(assert (>= 1 x_311)) +(assert (<= 0 x_312)) +(assert (>= 1 x_312)) +(assert (<= 0 x_313)) +(assert (>= 1 x_313)) +(assert (<= 0 x_314)) +(assert (>= 1 x_314)) +(assert (<= 0 x_316)) +(assert (>= 1 x_316)) +(assert (<= 0 x_317)) +(assert (>= 1 x_317)) +(assert (<= 0 x_318)) +(assert (>= 1 x_318)) +(assert (<= 0 x_319)) +(assert (>= 1 x_319)) +(assert (<= 0 x_321)) +(assert (>= 1 x_321)) +(assert (<= 0 x_322)) +(assert (>= 1 x_322)) +(assert (<= 0 x_323)) +(assert (>= 1 x_323)) +(assert (<= 0 x_324)) +(assert (>= 1 x_324)) +(assert (<= 0 x_326)) +(assert (>= 1 x_326)) +(assert (<= 0 x_327)) +(assert (>= 1 x_327)) +(assert (<= 0 x_328)) +(assert (>= 1 x_328)) +(assert (<= 0 x_329)) +(assert (>= 1 x_329)) +(assert (<= 0 x_331)) +(assert (>= 1 x_331)) +(assert (<= 0 x_332)) +(assert (>= 1 x_332)) +(assert (<= 0 x_333)) +(assert (>= 1 x_333)) +(assert (<= 0 x_334)) +(assert (>= 1 x_334)) +(assert (<= 0 x_336)) +(assert (>= 1 x_336)) +(assert (<= 0 x_337)) +(assert (>= 1 x_337)) +(assert (<= 0 x_338)) +(assert (>= 1 x_338)) +(assert (<= 0 x_339)) +(assert (>= 1 x_339)) +(assert (<= 0 x_341)) +(assert (>= 1 x_341)) +(assert (<= 0 x_342)) +(assert (>= 1 x_342)) +(assert (<= 0 x_343)) +(assert (>= 1 x_343)) +(assert (<= 0 x_344)) +(assert (>= 1 x_344)) +(assert (<= 0 x_346)) +(assert (>= 1 x_346)) +(assert (<= 0 x_347)) +(assert (>= 1 x_347)) +(assert (<= 0 x_348)) +(assert (>= 1 x_348)) +(assert (<= 0 x_349)) +(assert (>= 1 x_349)) +(assert (<= 0 x_351)) +(assert (>= 1 x_351)) +(assert (<= 0 x_352)) +(assert (>= 1 x_352)) +(assert (<= 0 x_353)) +(assert (>= 1 x_353)) +(assert (<= 0 x_354)) +(assert (>= 1 x_354)) +(assert (<= 0 x_356)) +(assert (>= 1 x_356)) +(assert (<= 0 x_357)) +(assert (>= 1 x_357)) +(assert (<= 0 x_358)) +(assert (>= 1 x_358)) +(assert (<= 0 x_359)) +(assert (>= 1 x_359)) +(assert (<= 0 x_361)) +(assert (>= 1 x_361)) +(assert (<= 0 x_362)) +(assert (>= 1 x_362)) +(assert (<= 0 x_363)) +(assert (>= 1 x_363)) +(assert (<= 0 x_364)) +(assert (>= 1 x_364)) +(assert (<= 0 x_366)) +(assert (>= 1 x_366)) +(assert (<= 0 x_367)) +(assert (>= 1 x_367)) +(assert (<= 0 x_368)) +(assert (>= 1 x_368)) +(assert (<= 0 x_369)) +(assert (>= 1 x_369)) +(assert (<= 0 x_371)) +(assert (>= 1 x_371)) +(assert (<= 0 x_372)) +(assert (>= 1 x_372)) +(assert (<= 0 x_373)) +(assert (>= 1 x_373)) +(assert (<= 0 x_374)) +(assert (>= 1 x_374)) +(assert (<= 0 x_376)) +(assert (>= 1 x_376)) +(assert (<= 0 x_377)) +(assert (>= 1 x_377)) +(assert (<= 0 x_378)) +(assert (>= 1 x_378)) +(assert (<= 0 x_379)) +(assert (>= 1 x_379)) +(assert (<= 0 x_381)) +(assert (>= 1 x_381)) +(assert (<= 0 x_382)) +(assert (>= 1 x_382)) +(assert (<= 0 x_383)) +(assert (>= 1 x_383)) +(assert (<= 0 x_384)) +(assert (>= 1 x_384)) +(assert (<= 0 x_386)) +(assert (>= 1 x_386)) +(assert (<= 0 x_387)) +(assert (>= 1 x_387)) +(assert (<= 0 x_388)) +(assert (>= 1 x_388)) +(assert (<= 0 x_389)) +(assert (>= 1 x_389)) +(assert (<= 0 x_391)) +(assert (>= 1 x_391)) +(assert (<= 0 x_392)) +(assert (>= 1 x_392)) +(assert (<= 0 x_393)) +(assert (>= 1 x_393)) +(assert (<= 0 x_394)) +(assert (>= 1 x_394)) +(assert (<= 0 x_396)) +(assert (>= 1 x_396)) +(assert (<= 0 x_397)) +(assert (>= 1 x_397)) +(assert (<= 0 x_398)) +(assert (>= 1 x_398)) +(assert (<= 0 x_399)) +(assert (>= 1 x_399)) +(assert (<= 0 x_401)) +(assert (>= 1 x_401)) +(assert (<= 0 x_402)) +(assert (>= 1 x_402)) +(assert (<= 0 x_403)) +(assert (>= 1 x_403)) +(assert (<= 0 x_404)) +(assert (>= 1 x_404)) +(assert (<= 0 x_406)) +(assert (>= 1 x_406)) +(assert (<= 0 x_407)) +(assert (>= 1 x_407)) +(assert (<= 0 x_408)) +(assert (>= 1 x_408)) +(assert (<= 0 x_409)) +(assert (>= 1 x_409)) +(assert (<= 0 x_411)) +(assert (>= 1 x_411)) +(assert (<= 0 x_412)) +(assert (>= 1 x_412)) +(assert (<= 0 x_413)) +(assert (>= 1 x_413)) +(assert (<= 0 x_414)) +(assert (>= 1 x_414)) +(assert (<= 0 x_416)) +(assert (>= 1 x_416)) +(assert (<= 0 x_417)) +(assert (>= 1 x_417)) +(assert (<= 0 x_418)) +(assert (>= 1 x_418)) +(assert (<= 0 x_419)) +(assert (>= 1 x_419)) +(assert (<= 0 x_421)) +(assert (>= 1 x_421)) +(assert (<= 0 x_422)) +(assert (>= 1 x_422)) +(assert (<= 0 x_423)) +(assert (>= 1 x_423)) +(assert (<= 0 x_424)) +(assert (>= 1 x_424)) +(assert (<= 0 x_426)) +(assert (>= 1 x_426)) +(assert (<= 0 x_427)) +(assert (>= 1 x_427)) +(assert (<= 0 x_428)) +(assert (>= 1 x_428)) +(assert (<= 0 x_429)) +(assert (>= 1 x_429)) +(assert (<= 0 x_431)) +(assert (>= 1 x_431)) +(assert (<= 0 x_432)) +(assert (>= 1 x_432)) +(assert (<= 0 x_433)) +(assert (>= 1 x_433)) +(assert (<= 0 x_434)) +(assert (>= 1 x_434)) +(assert (<= 0 x_436)) +(assert (>= 1 x_436)) +(assert (<= 0 x_437)) +(assert (>= 1 x_437)) +(assert (<= 0 x_438)) +(assert (>= 1 x_438)) +(assert (<= 0 x_439)) +(assert (>= 1 x_439)) +(assert (<= 0 x_441)) +(assert (>= 1 x_441)) +(assert (<= 0 x_442)) +(assert (>= 1 x_442)) +(assert (<= 0 x_443)) +(assert (>= 1 x_443)) +(assert (<= 0 x_444)) +(assert (>= 1 x_444)) +(assert (<= 0 x_446)) +(assert (>= 1 x_446)) +(assert (<= 0 x_447)) +(assert (>= 1 x_447)) +(assert (<= 0 x_448)) +(assert (>= 1 x_448)) +(assert (<= 0 x_449)) +(assert (>= 1 x_449)) +(assert (<= 0 x_451)) +(assert (>= 1 x_451)) +(assert (<= 0 x_452)) +(assert (>= 1 x_452)) +(assert (<= 0 x_453)) +(assert (>= 1 x_453)) +(assert (<= 0 x_454)) +(assert (>= 1 x_454)) +(assert (<= 0 x_456)) +(assert (>= 1 x_456)) +(assert (<= 0 x_457)) +(assert (>= 1 x_457)) +(assert (<= 0 x_458)) +(assert (>= 1 x_458)) +(assert (<= 0 x_459)) +(assert (>= 1 x_459)) +(assert (<= 0 x_461)) +(assert (>= 1 x_461)) +(assert (<= 0 x_462)) +(assert (>= 1 x_462)) +(assert (<= 0 x_463)) +(assert (>= 1 x_463)) +(assert (<= 0 x_464)) +(assert (>= 1 x_464)) +(assert (<= 0 x_466)) +(assert (>= 1 x_466)) +(assert (<= 0 x_467)) +(assert (>= 1 x_467)) +(assert (<= 0 x_468)) +(assert (>= 1 x_468)) +(assert (<= 0 x_469)) +(assert (>= 1 x_469)) +(assert (<= 0 x_471)) +(assert (>= 1 x_471)) +(assert (<= 0 x_472)) +(assert (>= 1 x_472)) +(assert (<= 0 x_473)) +(assert (>= 1 x_473)) +(assert (<= 0 x_474)) +(assert (>= 1 x_474)) +(assert (<= 0 x_476)) +(assert (>= 1 x_476)) +(assert (<= 0 x_477)) +(assert (>= 1 x_477)) +(assert (<= 0 x_478)) +(assert (>= 1 x_478)) +(assert (<= 0 x_479)) +(assert (>= 1 x_479)) +(assert (<= 0 x_481)) +(assert (>= 1 x_481)) +(assert (<= 0 x_482)) +(assert (>= 1 x_482)) +(assert (<= 0 x_483)) +(assert (>= 1 x_483)) +(assert (<= 0 x_484)) +(assert (>= 1 x_484)) +(assert (<= 0 x_486)) +(assert (>= 1 x_486)) +(assert (<= 0 x_487)) +(assert (>= 1 x_487)) +(assert (<= 0 x_488)) +(assert (>= 1 x_488)) +(assert (<= 0 x_489)) +(assert (>= 1 x_489)) +(assert (<= 0 x_491)) +(assert (>= 1 x_491)) +(assert (<= 0 x_492)) +(assert (>= 1 x_492)) +(assert (<= 0 x_493)) +(assert (>= 1 x_493)) +(assert (<= 0 x_494)) +(assert (>= 1 x_494)) +(assert (<= 0 x_496)) +(assert (>= 1 x_496)) +(assert (<= 0 x_497)) +(assert (>= 1 x_497)) +(assert (<= 0 x_498)) +(assert (>= 1 x_498)) +(assert (<= 0 x_499)) +(assert (>= 1 x_499)) +(assert (<= 0 x_501)) +(assert (>= 1 x_501)) +(assert (<= 0 x_502)) +(assert (>= 1 x_502)) +(assert (<= 0 x_503)) +(assert (>= 1 x_503)) +(assert (<= 0 x_504)) +(assert (>= 1 x_504)) +(assert (<= 0 x_506)) +(assert (>= 1 x_506)) +(assert (<= 0 x_507)) +(assert (>= 1 x_507)) +(assert (<= 0 x_508)) +(assert (>= 1 x_508)) +(assert (<= 0 x_509)) +(assert (>= 1 x_509)) +(assert (<= 0 x_511)) +(assert (>= 1 x_511)) +(assert (<= 0 x_512)) +(assert (>= 1 x_512)) +(assert (<= 0 x_513)) +(assert (>= 1 x_513)) +(assert (<= 0 x_514)) +(assert (>= 1 x_514)) +(assert (<= 0 x_516)) +(assert (>= 1 x_516)) +(assert (<= 0 x_517)) +(assert (>= 1 x_517)) +(assert (<= 0 x_518)) +(assert (>= 1 x_518)) +(assert (<= 0 x_519)) +(assert (>= 1 x_519)) +(assert (<= 0 x_521)) +(assert (>= 1 x_521)) +(assert (<= 0 x_522)) +(assert (>= 1 x_522)) +(assert (<= 0 x_523)) +(assert (>= 1 x_523)) +(assert (<= 0 x_524)) +(assert (>= 1 x_524)) +(assert (<= 0 x_526)) +(assert (>= 1 x_526)) +(assert (<= 0 x_527)) +(assert (>= 1 x_527)) +(assert (<= 0 x_528)) +(assert (>= 1 x_528)) +(assert (<= 0 x_529)) +(assert (>= 1 x_529)) +(assert (<= 0 x_531)) +(assert (>= 1 x_531)) +(assert (<= 0 x_532)) +(assert (>= 1 x_532)) +(assert (<= 0 x_533)) +(assert (>= 1 x_533)) +(assert (<= 0 x_534)) +(assert (>= 1 x_534)) +(assert (<= 0 x_536)) +(assert (>= 1 x_536)) +(assert (<= 0 x_537)) +(assert (>= 1 x_537)) +(assert (<= 0 x_538)) +(assert (>= 1 x_538)) +(assert (<= 0 x_539)) +(assert (>= 1 x_539)) +(assert (<= 0 x_541)) +(assert (>= 1 x_541)) +(assert (<= 0 x_542)) +(assert (>= 1 x_542)) +(assert (<= 0 x_543)) +(assert (>= 1 x_543)) +(assert (<= 0 x_544)) +(assert (>= 1 x_544)) +(assert (<= 0 x_546)) +(assert (>= 1 x_546)) +(assert (<= 0 x_547)) +(assert (>= 1 x_547)) +(assert (<= 0 x_548)) +(assert (>= 1 x_548)) +(assert (<= 0 x_549)) +(assert (>= 1 x_549)) +(assert (<= 0 x_551)) +(assert (>= 1 x_551)) +(assert (<= 0 x_552)) +(assert (>= 1 x_552)) +(assert (<= 0 x_553)) +(assert (>= 1 x_553)) +(assert (<= 0 x_554)) +(assert (>= 1 x_554)) +(assert (<= 0 x_556)) +(assert (>= 1 x_556)) +(assert (<= 0 x_557)) +(assert (>= 1 x_557)) +(assert (<= 0 x_558)) +(assert (>= 1 x_558)) +(assert (<= 0 x_559)) +(assert (>= 1 x_559)) +(assert (<= 0 x_561)) +(assert (>= 1 x_561)) +(assert (<= 0 x_562)) +(assert (>= 1 x_562)) +(assert (<= 0 x_563)) +(assert (>= 1 x_563)) +(assert (<= 0 x_564)) +(assert (>= 1 x_564)) +(assert (<= 0 x_566)) +(assert (>= 1 x_566)) +(assert (<= 0 x_567)) +(assert (>= 1 x_567)) +(assert (<= 0 x_568)) +(assert (>= 1 x_568)) +(assert (<= 0 x_569)) +(assert (>= 1 x_569)) +(assert (<= 0 x_571)) +(assert (>= 1 x_571)) +(assert (<= 0 x_572)) +(assert (>= 1 x_572)) +(assert (<= 0 x_573)) +(assert (>= 1 x_573)) +(assert (<= 0 x_574)) +(assert (>= 1 x_574)) +(assert (<= 0 x_576)) +(assert (>= 1 x_576)) +(assert (<= 0 x_577)) +(assert (>= 1 x_577)) +(assert (<= 0 x_578)) +(assert (>= 1 x_578)) +(assert (<= 0 x_579)) +(assert (>= 1 x_579)) +(assert (<= 0 x_581)) +(assert (>= 1 x_581)) +(assert (<= 0 x_582)) +(assert (>= 1 x_582)) +(assert (<= 0 x_583)) +(assert (>= 1 x_583)) +(assert (<= 0 x_584)) +(assert (>= 1 x_584)) +(assert (<= 0 x_586)) +(assert (>= 1 x_586)) +(assert (<= 0 x_587)) +(assert (>= 1 x_587)) +(assert (<= 0 x_588)) +(assert (>= 1 x_588)) +(assert (<= 0 x_589)) +(assert (>= 1 x_589)) +(assert (<= 0 x_591)) +(assert (>= 1 x_591)) +(assert (<= 0 x_592)) +(assert (>= 1 x_592)) +(assert (<= 0 x_593)) +(assert (>= 1 x_593)) +(assert (<= 0 x_594)) +(assert (>= 1 x_594)) +(assert (<= 0 x_596)) +(assert (>= 1 x_596)) +(assert (<= 0 x_597)) +(assert (>= 1 x_597)) +(assert (<= 0 x_598)) +(assert (>= 1 x_598)) +(assert (<= 0 x_599)) +(assert (>= 1 x_599)) +(assert (<= 0 x_601)) +(assert (>= 1 x_601)) +(assert (<= 0 x_602)) +(assert (>= 1 x_602)) +(assert (<= 0 x_603)) +(assert (>= 1 x_603)) +(assert (<= 0 x_604)) +(assert (>= 1 x_604)) +(assert (<= 0 x_606)) +(assert (>= 1 x_606)) +(assert (<= 0 x_607)) +(assert (>= 1 x_607)) +(assert (<= 0 x_608)) +(assert (>= 1 x_608)) +(assert (<= 0 x_609)) +(assert (>= 1 x_609)) +(assert (<= 0 x_611)) +(assert (>= 1 x_611)) +(assert (<= 0 x_612)) +(assert (>= 1 x_612)) +(assert (<= 0 x_613)) +(assert (>= 1 x_613)) +(assert (<= 0 x_614)) +(assert (>= 1 x_614)) +(assert (<= 0 x_616)) +(assert (>= 1 x_616)) +(assert (<= 0 x_617)) +(assert (>= 1 x_617)) +(assert (<= 0 x_618)) +(assert (>= 1 x_618)) +(assert (<= 0 x_619)) +(assert (>= 1 x_619)) +(assert (<= 0 x_621)) +(assert (>= 1 x_621)) +(assert (<= 0 x_622)) +(assert (>= 1 x_622)) +(assert (<= 0 x_623)) +(assert (>= 1 x_623)) +(assert (<= 0 x_624)) +(assert (>= 1 x_624)) +(assert (<= 0 x_626)) +(assert (>= 1 x_626)) +(assert (<= 0 x_627)) +(assert (>= 1 x_627)) +(assert (<= 0 x_628)) +(assert (>= 1 x_628)) +(assert (<= 0 x_629)) +(assert (>= 1 x_629)) +(assert (<= 0 x_631)) +(assert (>= 1 x_631)) +(assert (<= 0 x_632)) +(assert (>= 1 x_632)) +(assert (<= 0 x_633)) +(assert (>= 1 x_633)) +(assert (<= 0 x_634)) +(assert (>= 1 x_634)) +(assert (<= 0 x_636)) +(assert (>= 1 x_636)) +(assert (<= 0 x_637)) +(assert (>= 1 x_637)) +(assert (<= 0 x_638)) +(assert (>= 1 x_638)) +(assert (<= 0 x_639)) +(assert (>= 1 x_639)) +(assert (<= 0 x_641)) +(assert (>= 1 x_641)) +(assert (<= 0 x_642)) +(assert (>= 1 x_642)) +(assert (<= 0 x_643)) +(assert (>= 1 x_643)) +(assert (<= 0 x_644)) +(assert (>= 1 x_644)) +(assert (<= 0 x_646)) +(assert (>= 1 x_646)) +(assert (<= 0 x_647)) +(assert (>= 1 x_647)) +(assert (<= 0 x_648)) +(assert (>= 1 x_648)) +(assert (<= 0 x_649)) +(assert (>= 1 x_649)) +(assert (<= 0 x_651)) +(assert (>= 1 x_651)) +(assert (<= 0 x_652)) +(assert (>= 1 x_652)) +(assert (<= 0 x_653)) +(assert (>= 1 x_653)) +(assert (<= 0 x_654)) +(assert (>= 1 x_654)) +(assert (<= 0 x_656)) +(assert (>= 1 x_656)) +(assert (<= 0 x_657)) +(assert (>= 1 x_657)) +(assert (<= 0 x_658)) +(assert (>= 1 x_658)) +(assert (<= 0 x_659)) +(assert (>= 1 x_659)) +(assert (<= 0 x_661)) +(assert (>= 1 x_661)) +(assert (<= 0 x_662)) +(assert (>= 1 x_662)) +(assert (<= 0 x_663)) +(assert (>= 1 x_663)) +(assert (<= 0 x_664)) +(assert (>= 1 x_664)) +(assert (<= 0 x_666)) +(assert (>= 1 x_666)) +(assert (<= 0 x_667)) +(assert (>= 1 x_667)) +(assert (<= 0 x_668)) +(assert (>= 1 x_668)) +(assert (<= 0 x_669)) +(assert (>= 1 x_669)) +(assert (<= 0 x_671)) +(assert (>= 1 x_671)) +(assert (<= 0 x_672)) +(assert (>= 1 x_672)) +(assert (<= 0 x_673)) +(assert (>= 1 x_673)) +(assert (<= 0 x_674)) +(assert (>= 1 x_674)) +(assert (<= 0 x_676)) +(assert (>= 1 x_676)) +(assert (<= 0 x_677)) +(assert (>= 1 x_677)) +(assert (<= 0 x_678)) +(assert (>= 1 x_678)) +(assert (<= 0 x_679)) +(assert (>= 1 x_679)) +(assert (<= 0 x_681)) +(assert (>= 1 x_681)) +(assert (<= 0 x_682)) +(assert (>= 1 x_682)) +(assert (<= 0 x_683)) +(assert (>= 1 x_683)) +(assert (<= 0 x_684)) +(assert (>= 1 x_684)) +(assert (<= 0 x_686)) +(assert (>= 1 x_686)) +(assert (<= 0 x_687)) +(assert (>= 1 x_687)) +(assert (<= 0 x_688)) +(assert (>= 1 x_688)) +(assert (<= 0 x_689)) +(assert (>= 1 x_689)) +(assert (<= 0 x_691)) +(assert (>= 1 x_691)) +(assert (<= 0 x_692)) +(assert (>= 1 x_692)) +(assert (<= 0 x_693)) +(assert (>= 1 x_693)) +(assert (<= 0 x_694)) +(assert (>= 1 x_694)) +(assert (<= 0 x_696)) +(assert (>= 1 x_696)) +(assert (<= 0 x_697)) +(assert (>= 1 x_697)) +(assert (<= 0 x_698)) +(assert (>= 1 x_698)) +(assert (<= 0 x_699)) +(assert (>= 1 x_699)) +(assert (<= 0 x_701)) +(assert (>= 1 x_701)) +(assert (<= 0 x_702)) +(assert (>= 1 x_702)) +(assert (<= 0 x_703)) +(assert (>= 1 x_703)) +(assert (<= 0 x_704)) +(assert (>= 1 x_704)) +(assert (<= 0 x_706)) +(assert (>= 1 x_706)) +(assert (<= 0 x_707)) +(assert (>= 1 x_707)) +(assert (<= 0 x_708)) +(assert (>= 1 x_708)) +(assert (<= 0 x_709)) +(assert (>= 1 x_709)) +(assert (<= 0 x_711)) +(assert (>= 1 x_711)) +(assert (<= 0 x_712)) +(assert (>= 1 x_712)) +(assert (<= 0 x_713)) +(assert (>= 1 x_713)) +(assert (<= 0 x_714)) +(assert (>= 1 x_714)) +(assert (<= 0 x_716)) +(assert (>= 1 x_716)) +(assert (<= 0 x_717)) +(assert (>= 1 x_717)) +(assert (<= 0 x_718)) +(assert (>= 1 x_718)) +(assert (<= 0 x_719)) +(assert (>= 1 x_719)) +(assert (<= 0 x_721)) +(assert (>= 1 x_721)) +(assert (<= 0 x_722)) +(assert (>= 1 x_722)) +(assert (<= 0 x_723)) +(assert (>= 1 x_723)) +(assert (<= 0 x_724)) +(assert (>= 1 x_724)) +(assert (<= 0 x_726)) +(assert (>= 1 x_726)) +(assert (<= 0 x_727)) +(assert (>= 1 x_727)) +(assert (<= 0 x_728)) +(assert (>= 1 x_728)) +(assert (<= 0 x_729)) +(assert (>= 1 x_729)) +(assert (<= 0 x_731)) +(assert (>= 1 x_731)) +(assert (<= 0 x_732)) +(assert (>= 1 x_732)) +(assert (<= 0 x_733)) +(assert (>= 1 x_733)) +(assert (<= 0 x_734)) +(assert (>= 1 x_734)) +(assert (<= 0 x_736)) +(assert (>= 1 x_736)) +(assert (<= 0 x_737)) +(assert (>= 1 x_737)) +(assert (<= 0 x_738)) +(assert (>= 1 x_738)) +(assert (<= 0 x_739)) +(assert (>= 1 x_739)) +(assert (<= 0 x_741)) +(assert (>= 1 x_741)) +(assert (<= 0 x_742)) +(assert (>= 1 x_742)) +(assert (<= 0 x_743)) +(assert (>= 1 x_743)) +(assert (<= 0 x_744)) +(assert (>= 1 x_744)) +(assert (<= 0 x_746)) +(assert (>= 1 x_746)) +(assert (<= 0 x_747)) +(assert (>= 1 x_747)) +(assert (<= 0 x_748)) +(assert (>= 1 x_748)) +(assert (<= 0 x_749)) +(assert (>= 1 x_749)) +(assert (<= 0 x_751)) +(assert (>= 1 x_751)) +(assert (<= 0 x_752)) +(assert (>= 1 x_752)) +(assert (<= 0 x_753)) +(assert (>= 1 x_753)) +(assert (<= 0 x_754)) +(assert (>= 1 x_754)) +(assert (<= 0 x_756)) +(assert (>= 1 x_756)) +(assert (<= 0 x_757)) +(assert (>= 1 x_757)) +(assert (<= 0 x_758)) +(assert (>= 1 x_758)) +(assert (<= 0 x_759)) +(assert (>= 1 x_759)) +(assert (<= 0 x_761)) +(assert (>= 1 x_761)) +(assert (<= 0 x_762)) +(assert (>= 1 x_762)) +(assert (<= 0 x_763)) +(assert (>= 1 x_763)) +(assert (<= 0 x_764)) +(assert (>= 1 x_764)) +(assert (<= 0 x_766)) +(assert (>= 1 x_766)) +(assert (<= 0 x_767)) +(assert (>= 1 x_767)) +(assert (<= 0 x_768)) +(assert (>= 1 x_768)) +(assert (<= 0 x_769)) +(assert (>= 1 x_769)) +(assert (<= 0 x_771)) +(assert (>= 1 x_771)) +(assert (<= 0 x_772)) +(assert (>= 1 x_772)) +(assert (<= 0 x_773)) +(assert (>= 1 x_773)) +(assert (<= 0 x_774)) +(assert (>= 1 x_774)) +(assert (<= 0 x_776)) +(assert (>= 1 x_776)) +(assert (<= 0 x_777)) +(assert (>= 1 x_777)) +(assert (<= 0 x_778)) +(assert (>= 1 x_778)) +(assert (<= 0 x_779)) +(assert (>= 1 x_779)) +(assert (<= 0 x_781)) +(assert (>= 1 x_781)) +(assert (<= 0 x_782)) +(assert (>= 1 x_782)) +(assert (<= 0 x_783)) +(assert (>= 1 x_783)) +(assert (<= 0 x_784)) +(assert (>= 1 x_784)) +(assert (<= 0 x_786)) +(assert (>= 1 x_786)) +(assert (<= 0 x_787)) +(assert (>= 1 x_787)) +(assert (<= 0 x_788)) +(assert (>= 1 x_788)) +(assert (<= 0 x_789)) +(assert (>= 1 x_789)) +(assert (<= 0 x_791)) +(assert (>= 1 x_791)) +(assert (<= 0 x_792)) +(assert (>= 1 x_792)) +(assert (<= 0 x_793)) +(assert (>= 1 x_793)) +(assert (<= 0 x_794)) +(assert (>= 1 x_794)) +(assert (<= 0 x_796)) +(assert (>= 1 x_796)) +(assert (<= 0 x_797)) +(assert (>= 1 x_797)) +(assert (<= 0 x_798)) +(assert (>= 1 x_798)) +(assert (<= 0 x_799)) +(assert (>= 1 x_799)) +(assert (<= 0 x_801)) +(assert (>= 1 x_801)) +(assert (<= 0 x_802)) +(assert (>= 1 x_802)) +(assert (<= 0 x_803)) +(assert (>= 1 x_803)) +(assert (<= 0 x_804)) +(assert (>= 1 x_804)) +(assert (<= 0 x_806)) +(assert (>= 1 x_806)) +(assert (<= 0 x_807)) +(assert (>= 1 x_807)) +(assert (<= 0 x_808)) +(assert (>= 1 x_808)) +(assert (<= 0 x_809)) +(assert (>= 1 x_809)) +(assert (<= 0 x_811)) +(assert (>= 1 x_811)) +(assert (<= 0 x_812)) +(assert (>= 1 x_812)) +(assert (<= 0 x_813)) +(assert (>= 1 x_813)) +(assert (<= 0 x_814)) +(assert (>= 1 x_814)) +(assert (<= 0 x_816)) +(assert (>= 1 x_816)) +(assert (<= 0 x_817)) +(assert (>= 1 x_817)) +(assert (<= 0 x_818)) +(assert (>= 1 x_818)) +(assert (<= 0 x_819)) +(assert (>= 1 x_819)) +(assert (<= 0 x_821)) +(assert (>= 1 x_821)) +(assert (<= 0 x_822)) +(assert (>= 1 x_822)) +(assert (<= 0 x_823)) +(assert (>= 1 x_823)) +(assert (<= 0 x_824)) +(assert (>= 1 x_824)) +(assert (<= 0 x_826)) +(assert (>= 1 x_826)) +(assert (<= 0 x_827)) +(assert (>= 1 x_827)) +(assert (<= 0 x_828)) +(assert (>= 1 x_828)) +(assert (<= 0 x_829)) +(assert (>= 1 x_829)) +(assert (<= 0 x_831)) +(assert (>= 1 x_831)) +(assert (<= 0 x_832)) +(assert (>= 1 x_832)) +(assert (<= 0 x_833)) +(assert (>= 1 x_833)) +(assert (<= 0 x_834)) +(assert (>= 1 x_834)) +(assert (<= 0 x_836)) +(assert (>= 1 x_836)) +(assert (<= 0 x_837)) +(assert (>= 1 x_837)) +(assert (<= 0 x_838)) +(assert (>= 1 x_838)) +(assert (<= 0 x_839)) +(assert (>= 1 x_839)) +(assert (<= 0 x_841)) +(assert (>= 1 x_841)) +(assert (<= 0 x_842)) +(assert (>= 1 x_842)) +(assert (<= 0 x_843)) +(assert (>= 1 x_843)) +(assert (<= 0 x_844)) +(assert (>= 1 x_844)) +(assert (<= 0 x_846)) +(assert (>= 1 x_846)) +(assert (<= 0 x_847)) +(assert (>= 1 x_847)) +(assert (<= 0 x_848)) +(assert (>= 1 x_848)) +(assert (<= 0 x_849)) +(assert (>= 1 x_849)) +(assert (<= 0 x_851)) +(assert (>= 1 x_851)) +(assert (<= 0 x_852)) +(assert (>= 1 x_852)) +(assert (<= 0 x_853)) +(assert (>= 1 x_853)) +(assert (<= 0 x_854)) +(assert (>= 1 x_854)) +(assert (<= 0 x_856)) +(assert (>= 1 x_856)) +(assert (<= 0 x_857)) +(assert (>= 1 x_857)) +(assert (<= 0 x_858)) +(assert (>= 1 x_858)) +(assert (<= 0 x_859)) +(assert (>= 1 x_859)) +(assert (<= 0 x_861)) +(assert (>= 1 x_861)) +(assert (<= 0 x_862)) +(assert (>= 1 x_862)) +(assert (<= 0 x_863)) +(assert (>= 1 x_863)) +(assert (<= 0 x_864)) +(assert (>= 1 x_864)) +(assert (<= 0 x_866)) +(assert (>= 1 x_866)) +(assert (<= 0 x_867)) +(assert (>= 1 x_867)) +(assert (<= 0 x_868)) +(assert (>= 1 x_868)) +(assert (<= 0 x_869)) +(assert (>= 1 x_869)) +(assert (<= 0 x_871)) +(assert (>= 1 x_871)) +(assert (<= 0 x_872)) +(assert (>= 1 x_872)) +(assert (<= 0 x_873)) +(assert (>= 1 x_873)) +(assert (<= 0 x_874)) +(assert (>= 1 x_874)) +(assert (<= 0 x_876)) +(assert (>= 1 x_876)) +(assert (<= 0 x_877)) +(assert (>= 1 x_877)) +(assert (<= 0 x_878)) +(assert (>= 1 x_878)) +(assert (<= 0 x_879)) +(assert (>= 1 x_879)) +(assert (<= 0 x_881)) +(assert (>= 1 x_881)) +(assert (<= 0 x_882)) +(assert (>= 1 x_882)) +(assert (<= 0 x_883)) +(assert (>= 1 x_883)) +(assert (<= 0 x_884)) +(assert (>= 1 x_884)) +(assert (<= 0 x_886)) +(assert (>= 1 x_886)) +(assert (<= 0 x_887)) +(assert (>= 1 x_887)) +(assert (<= 0 x_888)) +(assert (>= 1 x_888)) +(assert (<= 0 x_889)) +(assert (>= 1 x_889)) +(assert (<= 0 x_891)) +(assert (>= 1 x_891)) +(assert (<= 0 x_892)) +(assert (>= 1 x_892)) +(assert (<= 0 x_893)) +(assert (>= 1 x_893)) +(assert (<= 0 x_894)) +(assert (>= 1 x_894)) +(assert (<= 0 x_896)) +(assert (>= 1 x_896)) +(assert (<= 0 x_897)) +(assert (>= 1 x_897)) +(assert (<= 0 x_898)) +(assert (>= 1 x_898)) +(assert (<= 0 x_899)) +(assert (>= 1 x_899)) +(assert (<= 0 x_901)) +(assert (>= 1 x_901)) +(assert (<= 0 x_902)) +(assert (>= 1 x_902)) +(assert (<= 0 x_903)) +(assert (>= 1 x_903)) +(assert (<= 0 x_904)) +(assert (>= 1 x_904)) +(assert (<= 0 x_906)) +(assert (>= 1 x_906)) +(assert (<= 0 x_907)) +(assert (>= 1 x_907)) +(assert (<= 0 x_908)) +(assert (>= 1 x_908)) +(assert (<= 0 x_909)) +(assert (>= 1 x_909)) +(assert (<= 0 x_911)) +(assert (>= 1 x_911)) +(assert (<= 0 x_912)) +(assert (>= 1 x_912)) +(assert (<= 0 x_913)) +(assert (>= 1 x_913)) +(assert (<= 0 x_914)) +(assert (>= 1 x_914)) +(assert (<= 0 x_916)) +(assert (>= 1 x_916)) +(assert (<= 0 x_917)) +(assert (>= 1 x_917)) +(assert (<= 0 x_918)) +(assert (>= 1 x_918)) +(assert (<= 0 x_919)) +(assert (>= 1 x_919)) +(assert (<= 0 x_921)) +(assert (>= 1 x_921)) +(assert (<= 0 x_922)) +(assert (>= 1 x_922)) +(assert (<= 0 x_923)) +(assert (>= 1 x_923)) +(assert (<= 0 x_924)) +(assert (>= 1 x_924)) +(assert (<= 0 x_926)) +(assert (>= 1 x_926)) +(assert (<= 0 x_927)) +(assert (>= 1 x_927)) +(assert (<= 0 x_928)) +(assert (>= 1 x_928)) +(assert (<= 0 x_929)) +(assert (>= 1 x_929)) +(assert (<= 0 x_931)) +(assert (>= 1 x_931)) +(assert (<= 0 x_932)) +(assert (>= 1 x_932)) +(assert (<= 0 x_933)) +(assert (>= 1 x_933)) +(assert (<= 0 x_934)) +(assert (>= 1 x_934)) +(assert (<= 0 x_936)) +(assert (>= 1 x_936)) +(assert (<= 0 x_937)) +(assert (>= 1 x_937)) +(assert (<= 0 x_938)) +(assert (>= 1 x_938)) +(assert (<= 0 x_939)) +(assert (>= 1 x_939)) +(assert (<= 0 x_941)) +(assert (>= 1 x_941)) +(assert (<= 0 x_942)) +(assert (>= 1 x_942)) +(assert (<= 0 x_943)) +(assert (>= 1 x_943)) +(assert (<= 0 x_944)) +(assert (>= 1 x_944)) +(assert (<= 0 x_946)) +(assert (>= 1 x_946)) +(assert (<= 0 x_947)) +(assert (>= 1 x_947)) +(assert (<= 0 x_948)) +(assert (>= 1 x_948)) +(assert (<= 0 x_949)) +(assert (>= 1 x_949)) +(assert (<= 0 x_951)) +(assert (>= 1 x_951)) +(assert (<= 0 x_952)) +(assert (>= 1 x_952)) +(assert (<= 0 x_953)) +(assert (>= 1 x_953)) +(assert (<= 0 x_954)) +(assert (>= 1 x_954)) +(assert (<= 0 x_956)) +(assert (>= 1 x_956)) +(assert (<= 0 x_957)) +(assert (>= 1 x_957)) +(assert (<= 0 x_958)) +(assert (>= 1 x_958)) +(assert (<= 0 x_959)) +(assert (>= 1 x_959)) +(assert (<= 0 x_961)) +(assert (>= 1 x_961)) +(assert (<= 0 x_962)) +(assert (>= 1 x_962)) +(assert (<= 0 x_963)) +(assert (>= 1 x_963)) +(assert (<= 0 x_964)) +(assert (>= 1 x_964)) +(assert (<= 0 x_966)) +(assert (>= 1 x_966)) +(assert (<= 0 x_967)) +(assert (>= 1 x_967)) +(assert (<= 0 x_968)) +(assert (>= 1 x_968)) +(assert (<= 0 x_969)) +(assert (>= 1 x_969)) +(assert (<= 0 x_971)) +(assert (>= 1 x_971)) +(assert (<= 0 x_972)) +(assert (>= 1 x_972)) +(assert (<= 0 x_973)) +(assert (>= 1 x_973)) +(assert (<= 0 x_974)) +(assert (>= 1 x_974)) +(assert (<= 0 x_976)) +(assert (>= 1 x_976)) +(assert (<= 0 x_977)) +(assert (>= 1 x_977)) +(assert (<= 0 x_978)) +(assert (>= 1 x_978)) +(assert (<= 0 x_979)) +(assert (>= 1 x_979)) +(assert (<= 0 x_981)) +(assert (>= 1 x_981)) +(assert (<= 0 x_982)) +(assert (>= 1 x_982)) +(assert (<= 0 x_983)) +(assert (>= 1 x_983)) +(assert (<= 0 x_984)) +(assert (>= 1 x_984)) +(assert (<= 0 x_986)) +(assert (>= 1 x_986)) +(assert (<= 0 x_987)) +(assert (>= 1 x_987)) +(assert (<= 0 x_988)) +(assert (>= 1 x_988)) +(assert (<= 0 x_989)) +(assert (>= 1 x_989)) +(assert (<= 0 x_991)) +(assert (>= 1 x_991)) +(assert (<= 0 x_992)) +(assert (>= 1 x_992)) +(assert (<= 0 x_993)) +(assert (>= 1 x_993)) +(assert (<= 0 x_994)) +(assert (>= 1 x_994)) +(assert (<= 0 x_996)) +(assert (>= 1 x_996)) +(assert (<= 0 x_997)) +(assert (>= 1 x_997)) +(assert (<= 0 x_998)) +(assert (>= 1 x_998)) +(assert (<= 0 x_999)) +(assert (>= 1 x_999)) +(assert (<= 0 x_1001)) +(assert (>= 1 x_1001)) +(assert (<= 0 x_1202)) +(assert (>= 1 x_1202)) +(assert (<= 0 x_1403)) +(assert (>= 1 x_1403)) +(assert (<= 0 x_1604)) +(assert (>= 1 x_1604)) +(assert (= 1 (+ x_1 x_2 x_3 x_4))) +(assert (= 1 (+ x_6 x_7 x_8 x_9))) +(assert (= 1 (+ x_11 x_12 x_13 x_14))) +(assert (= 1 (+ x_16 x_17 x_18 x_19))) +(assert (= 1 (+ x_21 x_22 x_23 x_24))) +(assert (= 1 (+ x_26 x_27 x_28 x_29))) +(assert (= 1 (+ x_31 x_32 x_33 x_34))) +(assert (= 1 (+ x_36 x_37 x_38 x_39))) +(assert (= 1 (+ x_41 x_42 x_43 x_44))) +(assert (= 1 (+ x_46 x_47 x_48 x_49))) +(assert (= 1 (+ x_51 x_52 x_53 x_54))) +(assert (= 1 (+ x_56 x_57 x_58 x_59))) +(assert (= 1 (+ x_61 x_62 x_63 x_64))) +(assert (= 1 (+ x_66 x_67 x_68 x_69))) +(assert (= 1 (+ x_71 x_72 x_73 x_74))) +(assert (= 1 (+ x_76 x_77 x_78 x_79))) +(assert (= 1 (+ x_81 x_82 x_83 x_84))) +(assert (= 1 (+ x_86 x_87 x_88 x_89))) +(assert (= 1 (+ x_91 x_92 x_93 x_94))) +(assert (= 1 (+ x_96 x_97 x_98 x_99))) +(assert (= 1 (+ x_101 x_102 x_103 x_104))) +(assert (= 1 (+ x_106 x_107 x_108 x_109))) +(assert (= 1 (+ x_111 x_112 x_113 x_114))) +(assert (= 1 (+ x_116 x_117 x_118 x_119))) +(assert (= 1 (+ x_121 x_122 x_123 x_124))) +(assert (= 1 (+ x_126 x_127 x_128 x_129))) +(assert (= 1 (+ x_131 x_132 x_133 x_134))) +(assert (= 1 (+ x_136 x_137 x_138 x_139))) +(assert (= 1 (+ x_141 x_142 x_143 x_144))) +(assert (= 1 (+ x_146 x_147 x_148 x_149))) +(assert (= 1 (+ x_151 x_152 x_153 x_154))) +(assert (= 1 (+ x_156 x_157 x_158 x_159))) +(assert (= 1 (+ x_161 x_162 x_163 x_164))) +(assert (= 1 (+ x_166 x_167 x_168 x_169))) +(assert (= 1 (+ x_171 x_172 x_173 x_174))) +(assert (= 1 (+ x_176 x_177 x_178 x_179))) +(assert (= 1 (+ x_181 x_182 x_183 x_184))) +(assert (= 1 (+ x_186 x_187 x_188 x_189))) +(assert (= 1 (+ x_191 x_192 x_193 x_194))) +(assert (= 1 (+ x_196 x_197 x_198 x_199))) +(assert (= 1 (+ x_201 x_202 x_203 x_204))) +(assert (= 1 (+ x_206 x_207 x_208 x_209))) +(assert (= 1 (+ x_211 x_212 x_213 x_214))) +(assert (= 1 (+ x_216 x_217 x_218 x_219))) +(assert (= 1 (+ x_221 x_222 x_223 x_224))) +(assert (= 1 (+ x_226 x_227 x_228 x_229))) +(assert (= 1 (+ x_231 x_232 x_233 x_234))) +(assert (= 1 (+ x_236 x_237 x_238 x_239))) +(assert (= 1 (+ x_241 x_242 x_243 x_244))) +(assert (= 1 (+ x_246 x_247 x_248 x_249))) +(assert (= 1 (+ x_251 x_252 x_253 x_254))) +(assert (= 1 (+ x_256 x_257 x_258 x_259))) +(assert (= 1 (+ x_261 x_262 x_263 x_264))) +(assert (= 1 (+ x_266 x_267 x_268 x_269))) +(assert (= 1 (+ x_271 x_272 x_273 x_274))) +(assert (= 1 (+ x_276 x_277 x_278 x_279))) +(assert (= 1 (+ x_281 x_282 x_283 x_284))) +(assert (= 1 (+ x_286 x_287 x_288 x_289))) +(assert (= 1 (+ x_291 x_292 x_293 x_294))) +(assert (= 1 (+ x_296 x_297 x_298 x_299))) +(assert (= 1 (+ x_301 x_302 x_303 x_304))) +(assert (= 1 (+ x_306 x_307 x_308 x_309))) +(assert (= 1 (+ x_311 x_312 x_313 x_314))) +(assert (= 1 (+ x_316 x_317 x_318 x_319))) +(assert (= 1 (+ x_321 x_322 x_323 x_324))) +(assert (= 1 (+ x_326 x_327 x_328 x_329))) +(assert (= 1 (+ x_331 x_332 x_333 x_334))) +(assert (= 1 (+ x_336 x_337 x_338 x_339))) +(assert (= 1 (+ x_341 x_342 x_343 x_344))) +(assert (= 1 (+ x_346 x_347 x_348 x_349))) +(assert (= 1 (+ x_351 x_352 x_353 x_354))) +(assert (= 1 (+ x_356 x_357 x_358 x_359))) +(assert (= 1 (+ x_361 x_362 x_363 x_364))) +(assert (= 1 (+ x_366 x_367 x_368 x_369))) +(assert (= 1 (+ x_371 x_372 x_373 x_374))) +(assert (= 1 (+ x_376 x_377 x_378 x_379))) +(assert (= 1 (+ x_381 x_382 x_383 x_384))) +(assert (= 1 (+ x_386 x_387 x_388 x_389))) +(assert (= 1 (+ x_391 x_392 x_393 x_394))) +(assert (= 1 (+ x_396 x_397 x_398 x_399))) +(assert (= 1 (+ x_401 x_402 x_403 x_404))) +(assert (= 1 (+ x_406 x_407 x_408 x_409))) +(assert (= 1 (+ x_411 x_412 x_413 x_414))) +(assert (= 1 (+ x_416 x_417 x_418 x_419))) +(assert (= 1 (+ x_421 x_422 x_423 x_424))) +(assert (= 1 (+ x_426 x_427 x_428 x_429))) +(assert (= 1 (+ x_431 x_432 x_433 x_434))) +(assert (= 1 (+ x_436 x_437 x_438 x_439))) +(assert (= 1 (+ x_441 x_442 x_443 x_444))) +(assert (= 1 (+ x_446 x_447 x_448 x_449))) +(assert (= 1 (+ x_451 x_452 x_453 x_454))) +(assert (= 1 (+ x_456 x_457 x_458 x_459))) +(assert (= 1 (+ x_461 x_462 x_463 x_464))) +(assert (= 1 (+ x_466 x_467 x_468 x_469))) +(assert (= 1 (+ x_471 x_472 x_473 x_474))) +(assert (= 1 (+ x_476 x_477 x_478 x_479))) +(assert (= 1 (+ x_481 x_482 x_483 x_484))) +(assert (= 1 (+ x_486 x_487 x_488 x_489))) +(assert (= 1 (+ x_491 x_492 x_493 x_494))) +(assert (= 1 (+ x_496 x_497 x_498 x_499))) +(assert (= 1 (+ x_501 x_502 x_503 x_504))) +(assert (= 1 (+ x_506 x_507 x_508 x_509))) +(assert (= 1 (+ x_511 x_512 x_513 x_514))) +(assert (= 1 (+ x_516 x_517 x_518 x_519))) +(assert (= 1 (+ x_521 x_522 x_523 x_524))) +(assert (= 1 (+ x_526 x_527 x_528 x_529))) +(assert (= 1 (+ x_531 x_532 x_533 x_534))) +(assert (= 1 (+ x_536 x_537 x_538 x_539))) +(assert (= 1 (+ x_541 x_542 x_543 x_544))) +(assert (= 1 (+ x_546 x_547 x_548 x_549))) +(assert (= 1 (+ x_551 x_552 x_553 x_554))) +(assert (= 1 (+ x_556 x_557 x_558 x_559))) +(assert (= 1 (+ x_561 x_562 x_563 x_564))) +(assert (= 1 (+ x_566 x_567 x_568 x_569))) +(assert (= 1 (+ x_571 x_572 x_573 x_574))) +(assert (= 1 (+ x_576 x_577 x_578 x_579))) +(assert (= 1 (+ x_581 x_582 x_583 x_584))) +(assert (= 1 (+ x_586 x_587 x_588 x_589))) +(assert (= 1 (+ x_591 x_592 x_593 x_594))) +(assert (= 1 (+ x_596 x_597 x_598 x_599))) +(assert (= 1 (+ x_601 x_602 x_603 x_604))) +(assert (= 1 (+ x_606 x_607 x_608 x_609))) +(assert (= 1 (+ x_611 x_612 x_613 x_614))) +(assert (= 1 (+ x_616 x_617 x_618 x_619))) +(assert (= 1 (+ x_621 x_622 x_623 x_624))) +(assert (= 1 (+ x_626 x_627 x_628 x_629))) +(assert (= 1 (+ x_631 x_632 x_633 x_634))) +(assert (= 1 (+ x_636 x_637 x_638 x_639))) +(assert (= 1 (+ x_641 x_642 x_643 x_644))) +(assert (= 1 (+ x_646 x_647 x_648 x_649))) +(assert (= 1 (+ x_651 x_652 x_653 x_654))) +(assert (= 1 (+ x_656 x_657 x_658 x_659))) +(assert (= 1 (+ x_661 x_662 x_663 x_664))) +(assert (= 1 (+ x_666 x_667 x_668 x_669))) +(assert (= 1 (+ x_671 x_672 x_673 x_674))) +(assert (= 1 (+ x_676 x_677 x_678 x_679))) +(assert (= 1 (+ x_681 x_682 x_683 x_684))) +(assert (= 1 (+ x_686 x_687 x_688 x_689))) +(assert (= 1 (+ x_691 x_692 x_693 x_694))) +(assert (= 1 (+ x_696 x_697 x_698 x_699))) +(assert (= 1 (+ x_701 x_702 x_703 x_704))) +(assert (= 1 (+ x_706 x_707 x_708 x_709))) +(assert (= 1 (+ x_711 x_712 x_713 x_714))) +(assert (= 1 (+ x_716 x_717 x_718 x_719))) +(assert (= 1 (+ x_721 x_722 x_723 x_724))) +(assert (= 1 (+ x_726 x_727 x_728 x_729))) +(assert (= 1 (+ x_731 x_732 x_733 x_734))) +(assert (= 1 (+ x_736 x_737 x_738 x_739))) +(assert (= 1 (+ x_741 x_742 x_743 x_744))) +(assert (= 1 (+ x_746 x_747 x_748 x_749))) +(assert (= 1 (+ x_751 x_752 x_753 x_754))) +(assert (= 1 (+ x_756 x_757 x_758 x_759))) +(assert (= 1 (+ x_761 x_762 x_763 x_764))) +(assert (= 1 (+ x_766 x_767 x_768 x_769))) +(assert (= 1 (+ x_771 x_772 x_773 x_774))) +(assert (= 1 (+ x_776 x_777 x_778 x_779))) +(assert (= 1 (+ x_781 x_782 x_783 x_784))) +(assert (= 1 (+ x_786 x_787 x_788 x_789))) +(assert (= 1 (+ x_791 x_792 x_793 x_794))) +(assert (= 1 (+ x_796 x_797 x_798 x_799))) +(assert (= 1 (+ x_801 x_802 x_803 x_804))) +(assert (= 1 (+ x_806 x_807 x_808 x_809))) +(assert (= 1 (+ x_811 x_812 x_813 x_814))) +(assert (= 1 (+ x_816 x_817 x_818 x_819))) +(assert (= 1 (+ x_821 x_822 x_823 x_824))) +(assert (= 1 (+ x_826 x_827 x_828 x_829))) +(assert (= 1 (+ x_831 x_832 x_833 x_834))) +(assert (= 1 (+ x_836 x_837 x_838 x_839))) +(assert (= 1 (+ x_841 x_842 x_843 x_844))) +(assert (= 1 (+ x_846 x_847 x_848 x_849))) +(assert (= 1 (+ x_851 x_852 x_853 x_854))) +(assert (= 1 (+ x_856 x_857 x_858 x_859))) +(assert (= 1 (+ x_861 x_862 x_863 x_864))) +(assert (= 1 (+ x_866 x_867 x_868 x_869))) +(assert (= 1 (+ x_871 x_872 x_873 x_874))) +(assert (= 1 (+ x_876 x_877 x_878 x_879))) +(assert (= 1 (+ x_881 x_882 x_883 x_884))) +(assert (= 1 (+ x_886 x_887 x_888 x_889))) +(assert (= 1 (+ x_891 x_892 x_893 x_894))) +(assert (= 1 (+ x_896 x_897 x_898 x_899))) +(assert (= 1 (+ x_901 x_902 x_903 x_904))) +(assert (= 1 (+ x_906 x_907 x_908 x_909))) +(assert (= 1 (+ x_911 x_912 x_913 x_914))) +(assert (= 1 (+ x_916 x_917 x_918 x_919))) +(assert (= 1 (+ x_921 x_922 x_923 x_924))) +(assert (= 1 (+ x_926 x_927 x_928 x_929))) +(assert (= 1 (+ x_931 x_932 x_933 x_934))) +(assert (= 1 (+ x_936 x_937 x_938 x_939))) +(assert (= 1 (+ x_941 x_942 x_943 x_944))) +(assert (= 1 (+ x_946 x_947 x_948 x_949))) +(assert (= 1 (+ x_951 x_952 x_953 x_954))) +(assert (= 1 (+ x_956 x_957 x_958 x_959))) +(assert (= 1 (+ x_961 x_962 x_963 x_964))) +(assert (= 1 (+ x_966 x_967 x_968 x_969))) +(assert (= 1 (+ x_971 x_972 x_973 x_974))) +(assert (= 1 (+ x_976 x_977 x_978 x_979))) +(assert (= 1 (+ x_981 x_982 x_983 x_984))) +(assert (= 1 (+ x_986 x_987 x_988 x_989))) +(assert (= 1 (+ x_991 x_992 x_993 x_994))) +(assert (= 1 (+ x_996 x_997 x_998 x_999))) +(assert (<= 0 (+ x_1001 (* (- 1) x_4)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_9)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_14)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_19)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_24)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_29)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_34)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_39)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_44)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_49)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_54)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_59)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_64)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_69)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_74)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_79)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_84)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_89)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_94)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_99)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_104)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_109)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_114)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_119)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_124)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_129)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_134)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_139)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_144)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_149)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_154)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_159)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_164)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_169)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_174)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_179)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_184)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_189)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_194)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_199)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_204)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_209)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_214)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_219)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_224)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_229)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_234)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_239)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_244)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_249)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_254)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_259)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_264)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_269)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_274)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_279)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_284)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_289)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_294)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_299)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_304)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_309)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_314)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_319)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_324)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_329)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_334)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_339)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_344)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_349)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_354)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_359)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_364)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_369)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_374)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_379)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_384)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_389)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_394)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_399)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_404)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_409)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_414)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_419)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_424)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_429)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_434)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_439)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_444)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_449)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_454)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_459)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_464)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_469)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_474)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_479)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_484)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_489)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_494)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_499)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_504)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_509)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_514)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_519)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_524)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_529)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_534)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_539)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_544)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_549)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_554)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_559)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_564)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_569)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_574)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_579)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_584)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_589)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_594)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_599)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_604)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_609)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_614)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_619)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_624)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_629)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_634)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_639)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_644)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_649)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_654)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_659)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_664)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_669)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_674)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_679)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_684)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_689)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_694)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_699)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_704)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_709)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_714)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_719)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_724)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_729)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_734)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_739)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_744)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_749)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_754)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_759)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_764)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_769)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_774)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_779)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_784)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_789)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_794)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_799)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_804)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_809)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_814)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_819)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_824)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_829)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_834)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_839)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_844)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_849)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_854)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_859)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_864)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_869)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_874)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_879)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_884)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_889)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_894)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_899)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_904)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_909)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_914)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_919)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_924)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_929)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_934)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_939)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_944)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_949)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_954)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_959)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_964)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_969)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_974)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_979)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_984)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_989)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_994)))) +(assert (<= 0 (+ x_1001 (* (- 1) x_999)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_1)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_6)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_11)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_16)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_21)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_26)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_31)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_36)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_41)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_46)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_51)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_56)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_61)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_66)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_71)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_76)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_81)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_86)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_91)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_96)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_101)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_106)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_111)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_116)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_121)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_126)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_131)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_136)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_141)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_146)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_151)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_156)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_161)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_166)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_171)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_176)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_181)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_186)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_191)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_196)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_201)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_206)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_211)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_216)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_221)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_226)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_231)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_236)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_241)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_246)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_251)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_256)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_261)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_266)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_271)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_276)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_281)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_286)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_291)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_296)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_301)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_306)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_311)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_316)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_321)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_326)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_331)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_336)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_341)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_346)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_351)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_356)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_361)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_366)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_371)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_376)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_381)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_386)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_391)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_396)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_401)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_406)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_411)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_416)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_421)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_426)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_431)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_436)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_441)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_446)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_451)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_456)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_461)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_466)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_471)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_476)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_481)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_486)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_491)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_496)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_501)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_506)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_511)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_516)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_521)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_526)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_531)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_536)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_541)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_546)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_551)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_556)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_561)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_566)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_571)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_576)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_581)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_586)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_591)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_596)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_601)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_606)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_611)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_616)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_621)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_626)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_631)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_636)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_641)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_646)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_651)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_656)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_661)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_666)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_671)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_676)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_681)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_686)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_691)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_696)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_701)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_706)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_711)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_716)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_721)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_726)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_731)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_736)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_741)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_746)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_751)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_756)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_761)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_766)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_771)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_776)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_781)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_786)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_791)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_796)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_801)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_806)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_811)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_816)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_821)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_826)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_831)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_836)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_841)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_846)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_851)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_856)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_861)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_866)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_871)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_876)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_881)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_886)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_891)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_896)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_901)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_906)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_911)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_916)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_921)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_926)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_931)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_936)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_941)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_946)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_951)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_956)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_961)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_966)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_971)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_976)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_981)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_986)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_991)))) +(assert (<= 0 (+ x_1202 (* (- 1) x_996)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_2)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_7)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_12)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_17)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_22)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_27)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_32)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_37)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_42)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_47)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_52)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_57)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_62)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_67)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_72)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_77)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_82)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_87)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_92)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_97)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_102)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_107)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_112)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_117)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_122)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_127)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_132)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_137)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_142)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_147)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_152)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_157)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_162)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_167)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_172)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_177)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_182)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_187)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_192)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_197)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_202)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_207)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_212)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_217)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_222)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_227)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_232)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_237)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_242)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_247)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_252)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_257)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_262)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_267)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_272)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_277)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_282)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_287)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_292)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_297)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_302)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_307)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_312)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_317)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_322)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_327)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_332)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_337)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_342)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_347)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_352)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_357)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_362)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_367)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_372)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_377)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_382)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_387)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_392)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_397)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_402)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_407)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_412)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_417)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_422)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_427)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_432)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_437)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_442)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_447)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_452)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_457)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_462)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_467)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_472)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_477)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_482)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_487)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_492)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_497)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_502)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_507)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_512)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_517)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_522)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_527)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_532)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_537)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_542)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_547)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_552)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_557)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_562)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_567)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_572)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_577)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_582)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_587)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_592)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_597)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_602)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_607)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_612)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_617)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_622)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_627)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_632)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_637)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_642)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_647)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_652)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_657)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_662)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_667)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_672)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_677)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_682)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_687)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_692)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_697)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_702)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_707)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_712)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_717)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_722)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_727)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_732)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_737)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_742)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_747)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_752)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_757)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_762)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_767)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_772)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_777)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_782)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_787)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_792)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_797)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_802)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_807)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_812)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_817)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_822)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_827)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_832)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_837)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_842)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_847)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_852)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_857)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_862)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_867)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_872)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_877)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_882)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_887)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_892)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_897)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_902)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_907)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_912)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_917)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_922)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_927)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_932)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_937)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_942)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_947)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_952)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_957)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_962)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_967)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_972)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_977)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_982)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_987)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_992)))) +(assert (<= 0 (+ x_1403 (* (- 1) x_997)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_3)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_8)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_13)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_18)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_23)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_28)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_33)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_38)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_43)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_48)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_53)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_58)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_63)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_68)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_73)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_78)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_83)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_88)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_93)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_98)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_103)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_108)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_113)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_118)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_123)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_128)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_133)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_138)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_143)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_148)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_153)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_158)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_163)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_168)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_173)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_178)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_183)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_188)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_193)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_198)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_203)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_208)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_213)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_218)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_223)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_228)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_233)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_238)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_243)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_248)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_253)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_258)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_263)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_268)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_273)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_278)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_283)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_288)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_293)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_298)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_303)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_308)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_313)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_318)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_323)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_328)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_333)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_338)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_343)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_348)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_353)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_358)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_363)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_368)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_373)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_378)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_383)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_388)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_393)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_398)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_403)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_408)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_413)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_418)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_423)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_428)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_433)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_438)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_443)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_448)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_453)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_458)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_463)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_468)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_473)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_478)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_483)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_488)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_493)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_498)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_503)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_508)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_513)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_518)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_523)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_528)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_533)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_538)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_543)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_548)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_553)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_558)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_563)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_568)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_573)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_578)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_583)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_588)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_593)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_598)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_603)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_608)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_613)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_618)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_623)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_628)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_633)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_638)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_643)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_648)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_653)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_658)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_663)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_668)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_673)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_678)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_683)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_688)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_693)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_698)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_703)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_708)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_713)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_718)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_723)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_728)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_733)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_738)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_743)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_748)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_753)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_758)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_763)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_768)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_773)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_778)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_783)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_788)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_793)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_798)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_803)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_808)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_813)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_818)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_823)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_828)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_833)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_838)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_843)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_848)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_853)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_858)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_863)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_868)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_873)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_878)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_883)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_888)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_893)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_898)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_903)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_908)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_913)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_918)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_923)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_928)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_933)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_938)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_943)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_948)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_953)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_958)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_963)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_968)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_973)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_978)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_983)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_988)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_993)))) +(assert (<= 0 (+ x_1604 (* (- 1) x_998)))) +(assert (<= 0 + (+ (* 21600 x_1001) + (* (- 50) x_9) + (* (- 40) x_14) + (* (- 50) x_19) + (* (- 60) x_24) + (* (- 40) x_29) + (* (- 40) x_34) + (* (- 50) x_39) + (* (- 40) x_44) + (* (- 40) x_49) + (* (- 40) x_54) + (* (- 50) x_59) + (* (- 40) x_64) + (* (- 40) x_69) + (* (- 50) x_74) + (* (- 60) x_79) + (* (- 70) x_84) + (* (- 80) x_89) + (* (- 90) x_94) + (* (- 100) x_99) + (* (- 40) x_104) + (* (- 50) x_109) + (* (- 60) x_114) + (* (- 70) x_119) + (* (- 40) x_124) + (* (- 50) x_129) + (* (- 60) x_134) + (* (- 70) x_139) + (* (- 80) x_144) + (* (- 90) x_149) + (* (- 100) x_154) + (* (- 110) x_159) + (* (- 120) x_164) + (* (- 40) x_169) + (* (- 50) x_174) + (* (- 60) x_179) + (* (- 70) x_184) + (* (- 40) x_189) + (* (- 50) x_194) + (* (- 60) x_199) + (* (- 40) x_204) + (* (- 50) x_209) + (* (- 40) x_214) + (* (- 50) x_219) + (* (- 60) x_224) + (* (- 70) x_229) + (* (- 80) x_234) + (* (- 90) x_239) + (* (- 100) x_244) + (* (- 110) x_249) + (* (- 40) x_254) + (* (- 50) x_259) + (* (- 60) x_264) + (* (- 70) x_269) + (* (- 80) x_274) + (* (- 90) x_279) + (* (- 100) x_284) + (* (- 40) x_289) + (* (- 50) x_294) + (* (- 60) x_299) + (* (- 70) x_304) + (* (- 80) x_309) + (* (- 90) x_314) + (* (- 100) x_319) + (* (- 110) x_324) + (* (- 40) x_329) + (* (- 50) x_334) + (* (- 60) x_339) + (* (- 70) x_344) + (* (- 80) x_349) + (* (- 90) x_354) + (* (- 100) x_359) + (* (- 40) x_364) + (* (- 50) x_369) + (* (- 60) x_374) + (* (- 70) x_379) + (* (- 80) x_384) + (* (- 90) x_389) + (* (- 100) x_394) + (* (- 40) x_399) + (* (- 50) x_404) + (* (- 60) x_409) + (* (- 40) x_414) + (* (- 50) x_419) + (* (- 60) x_424) + (* (- 70) x_429) + (* (- 80) x_434) + (* (- 90) x_439) + (* (- 100) x_444) + (* (- 110) x_449) + (* (- 120) x_454) + (* (- 130) x_459) + (* (- 40) x_464) + (* (- 50) x_469) + (* (- 60) x_474) + (* (- 70) x_479) + (* (- 80) x_484) + (* (- 90) x_489) + (* (- 40) x_494) + (* (- 40) x_499) + (* (- 50) x_504) + (* (- 60) x_509) + (* (- 70) x_514) + (* (- 80) x_519) + (* (- 90) x_524) + (* (- 40) x_529) + (* (- 50) x_534) + (* (- 60) x_539) + (* (- 40) x_544) + (* (- 50) x_549) + (* (- 60) x_554) + (* (- 70) x_559) + (* (- 40) x_564) + (* (- 50) x_569) + (* (- 60) x_574) + (* (- 70) x_579) + (* (- 80) x_584) + (* (- 90) x_589) + (* (- 40) x_594) + (* (- 40) x_599) + (* (- 50) x_604) + (* (- 60) x_609) + (* (- 70) x_614) + (* (- 80) x_619) + (* (- 40) x_624) + (* (- 50) x_629) + (* (- 60) x_634) + (* (- 70) x_639) + (* (- 80) x_644) + (* (- 90) x_649) + (* (- 100) x_654) + (* (- 110) x_659) + (* (- 40) x_664) + (* (- 50) x_669) + (* (- 60) x_674) + (* (- 70) x_679) + (* (- 40) x_684) + (* (- 50) x_689) + (* (- 60) x_694) + (* (- 70) x_699) + (* (- 80) x_704) + (* (- 90) x_709) + (* (- 100) x_714) + (* (- 110) x_719) + (* (- 120) x_724) + (* (- 40) x_729) + (* (- 50) x_734) + (* (- 60) x_739) + (* (- 70) x_744) + (* (- 80) x_749) + (* (- 90) x_754) + (* (- 100) x_759) + (* (- 110) x_764) + (* (- 40) x_769) + (* (- 50) x_774) + (* (- 40) x_779) + (* (- 50) x_784) + (* (- 40) x_789) + (* (- 50) x_794) + (* (- 60) x_799) + (* (- 70) x_804) + (* (- 80) x_809) + (* (- 90) x_814) + (* (- 100) x_819) + (* (- 40) x_824) + (* (- 50) x_829) + (* (- 60) x_834) + (* (- 70) x_839) + (* (- 80) x_844) + (* (- 90) x_849) + (* (- 100) x_854) + (* (- 110) x_859) + (* (- 40) x_864) + (* (- 50) x_869) + (* (- 60) x_874) + (* (- 70) x_879) + (* (- 80) x_884) + (* (- 90) x_889) + (* (- 40) x_894) + (* (- 50) x_899) + (* (- 60) x_904) + (* (- 70) x_909) + (* (- 80) x_914) + (* (- 90) x_919) + (* (- 100) x_924) + (* (- 52) x_929) + (* (- 52) x_934) + (* (- 65) x_939) + (* (- 52) x_944) + (* (- 52) x_949) + (* (- 65) x_954) + (* (- 52) x_959) + (* (- 65) x_964) + (* (- 52) x_969) + (* (- 65) x_974) + (* (- 78) x_979) + (* (- 91) x_984) + (* (- 104) x_989) + (* (- 117) x_994) + (* (- 130) x_999) + (* (- 40) x_4)))) +(assert (<= 0 + (+ (* 7400 x_1202) + (* (- 50) x_6) + (* (- 40) x_11) + (* (- 50) x_16) + (* (- 60) x_21) + (* (- 40) x_26) + (* (- 40) x_31) + (* (- 50) x_36) + (* (- 40) x_41) + (* (- 40) x_46) + (* (- 40) x_51) + (* (- 50) x_56) + (* (- 40) x_61) + (* (- 40) x_66) + (* (- 50) x_71) + (* (- 60) x_76) + (* (- 70) x_81) + (* (- 80) x_86) + (* (- 90) x_91) + (* (- 100) x_96) + (* (- 40) x_101) + (* (- 50) x_106) + (* (- 60) x_111) + (* (- 70) x_116) + (* (- 40) x_121) + (* (- 50) x_126) + (* (- 60) x_131) + (* (- 70) x_136) + (* (- 80) x_141) + (* (- 90) x_146) + (* (- 100) x_151) + (* (- 110) x_156) + (* (- 120) x_161) + (* (- 40) x_166) + (* (- 50) x_171) + (* (- 60) x_176) + (* (- 70) x_181) + (* (- 40) x_186) + (* (- 50) x_191) + (* (- 60) x_196) + (* (- 40) x_201) + (* (- 50) x_206) + (* (- 40) x_211) + (* (- 50) x_216) + (* (- 60) x_221) + (* (- 70) x_226) + (* (- 80) x_231) + (* (- 90) x_236) + (* (- 100) x_241) + (* (- 110) x_246) + (* (- 40) x_251) + (* (- 50) x_256) + (* (- 60) x_261) + (* (- 70) x_266) + (* (- 80) x_271) + (* (- 90) x_276) + (* (- 100) x_281) + (* (- 40) x_286) + (* (- 50) x_291) + (* (- 60) x_296) + (* (- 70) x_301) + (* (- 80) x_306) + (* (- 90) x_311) + (* (- 100) x_316) + (* (- 110) x_321) + (* (- 40) x_326) + (* (- 50) x_331) + (* (- 60) x_336) + (* (- 70) x_341) + (* (- 80) x_346) + (* (- 90) x_351) + (* (- 100) x_356) + (* (- 40) x_361) + (* (- 50) x_366) + (* (- 60) x_371) + (* (- 70) x_376) + (* (- 80) x_381) + (* (- 90) x_386) + (* (- 100) x_391) + (* (- 40) x_396) + (* (- 50) x_401) + (* (- 60) x_406) + (* (- 40) x_411) + (* (- 50) x_416) + (* (- 60) x_421) + (* (- 70) x_426) + (* (- 80) x_431) + (* (- 90) x_436) + (* (- 100) x_441) + (* (- 110) x_446) + (* (- 120) x_451) + (* (- 130) x_456) + (* (- 40) x_461) + (* (- 50) x_466) + (* (- 60) x_471) + (* (- 70) x_476) + (* (- 80) x_481) + (* (- 90) x_486) + (* (- 40) x_491) + (* (- 40) x_496) + (* (- 50) x_501) + (* (- 60) x_506) + (* (- 70) x_511) + (* (- 80) x_516) + (* (- 90) x_521) + (* (- 40) x_526) + (* (- 50) x_531) + (* (- 60) x_536) + (* (- 40) x_541) + (* (- 50) x_546) + (* (- 60) x_551) + (* (- 70) x_556) + (* (- 40) x_561) + (* (- 50) x_566) + (* (- 60) x_571) + (* (- 70) x_576) + (* (- 80) x_581) + (* (- 90) x_586) + (* (- 40) x_591) + (* (- 40) x_596) + (* (- 50) x_601) + (* (- 60) x_606) + (* (- 70) x_611) + (* (- 80) x_616) + (* (- 40) x_621) + (* (- 50) x_626) + (* (- 60) x_631) + (* (- 70) x_636) + (* (- 80) x_641) + (* (- 90) x_646) + (* (- 100) x_651) + (* (- 110) x_656) + (* (- 40) x_661) + (* (- 50) x_666) + (* (- 60) x_671) + (* (- 70) x_676) + (* (- 40) x_681) + (* (- 50) x_686) + (* (- 60) x_691) + (* (- 70) x_696) + (* (- 80) x_701) + (* (- 90) x_706) + (* (- 100) x_711) + (* (- 110) x_716) + (* (- 120) x_721) + (* (- 40) x_726) + (* (- 50) x_731) + (* (- 60) x_736) + (* (- 70) x_741) + (* (- 80) x_746) + (* (- 90) x_751) + (* (- 100) x_756) + (* (- 110) x_761) + (* (- 40) x_766) + (* (- 50) x_771) + (* (- 40) x_776) + (* (- 50) x_781) + (* (- 40) x_786) + (* (- 50) x_791) + (* (- 60) x_796) + (* (- 70) x_801) + (* (- 80) x_806) + (* (- 90) x_811) + (* (- 100) x_816) + (* (- 40) x_821) + (* (- 50) x_826) + (* (- 60) x_831) + (* (- 70) x_836) + (* (- 80) x_841) + (* (- 90) x_846) + (* (- 100) x_851) + (* (- 110) x_856) + (* (- 40) x_861) + (* (- 50) x_866) + (* (- 60) x_871) + (* (- 70) x_876) + (* (- 80) x_881) + (* (- 90) x_886) + (* (- 40) x_891) + (* (- 50) x_896) + (* (- 60) x_901) + (* (- 70) x_906) + (* (- 80) x_911) + (* (- 90) x_916) + (* (- 100) x_921) + (* (- 52) x_926) + (* (- 52) x_931) + (* (- 65) x_936) + (* (- 52) x_941) + (* (- 52) x_946) + (* (- 65) x_951) + (* (- 52) x_956) + (* (- 65) x_961) + (* (- 52) x_966) + (* (- 65) x_971) + (* (- 78) x_976) + (* (- 91) x_981) + (* (- 104) x_986) + (* (- 117) x_991) + (* (- 130) x_996) + (* (- 40) x_1)))) +(assert (<= 0 + (+ (* 26500 x_1403) + (* (- 50) x_7) + (* (- 40) x_12) + (* (- 50) x_17) + (* (- 60) x_22) + (* (- 40) x_27) + (* (- 40) x_32) + (* (- 50) x_37) + (* (- 40) x_42) + (* (- 40) x_47) + (* (- 40) x_52) + (* (- 50) x_57) + (* (- 40) x_62) + (* (- 40) x_67) + (* (- 50) x_72) + (* (- 60) x_77) + (* (- 70) x_82) + (* (- 80) x_87) + (* (- 90) x_92) + (* (- 100) x_97) + (* (- 40) x_102) + (* (- 50) x_107) + (* (- 60) x_112) + (* (- 70) x_117) + (* (- 40) x_122) + (* (- 50) x_127) + (* (- 60) x_132) + (* (- 70) x_137) + (* (- 80) x_142) + (* (- 90) x_147) + (* (- 100) x_152) + (* (- 110) x_157) + (* (- 120) x_162) + (* (- 40) x_167) + (* (- 50) x_172) + (* (- 60) x_177) + (* (- 70) x_182) + (* (- 40) x_187) + (* (- 50) x_192) + (* (- 60) x_197) + (* (- 40) x_202) + (* (- 50) x_207) + (* (- 40) x_212) + (* (- 50) x_217) + (* (- 60) x_222) + (* (- 70) x_227) + (* (- 80) x_232) + (* (- 90) x_237) + (* (- 100) x_242) + (* (- 110) x_247) + (* (- 40) x_252) + (* (- 50) x_257) + (* (- 60) x_262) + (* (- 70) x_267) + (* (- 80) x_272) + (* (- 90) x_277) + (* (- 100) x_282) + (* (- 40) x_287) + (* (- 50) x_292) + (* (- 60) x_297) + (* (- 70) x_302) + (* (- 80) x_307) + (* (- 90) x_312) + (* (- 100) x_317) + (* (- 110) x_322) + (* (- 40) x_327) + (* (- 50) x_332) + (* (- 60) x_337) + (* (- 70) x_342) + (* (- 80) x_347) + (* (- 90) x_352) + (* (- 100) x_357) + (* (- 40) x_362) + (* (- 50) x_367) + (* (- 60) x_372) + (* (- 70) x_377) + (* (- 80) x_382) + (* (- 90) x_387) + (* (- 100) x_392) + (* (- 40) x_397) + (* (- 50) x_402) + (* (- 60) x_407) + (* (- 40) x_412) + (* (- 50) x_417) + (* (- 60) x_422) + (* (- 70) x_427) + (* (- 80) x_432) + (* (- 90) x_437) + (* (- 100) x_442) + (* (- 110) x_447) + (* (- 120) x_452) + (* (- 130) x_457) + (* (- 40) x_462) + (* (- 50) x_467) + (* (- 60) x_472) + (* (- 70) x_477) + (* (- 80) x_482) + (* (- 90) x_487) + (* (- 40) x_492) + (* (- 40) x_497) + (* (- 50) x_502) + (* (- 60) x_507) + (* (- 70) x_512) + (* (- 80) x_517) + (* (- 90) x_522) + (* (- 40) x_527) + (* (- 50) x_532) + (* (- 60) x_537) + (* (- 40) x_542) + (* (- 50) x_547) + (* (- 60) x_552) + (* (- 70) x_557) + (* (- 40) x_562) + (* (- 50) x_567) + (* (- 60) x_572) + (* (- 70) x_577) + (* (- 80) x_582) + (* (- 90) x_587) + (* (- 40) x_592) + (* (- 40) x_597) + (* (- 50) x_602) + (* (- 60) x_607) + (* (- 70) x_612) + (* (- 80) x_617) + (* (- 40) x_622) + (* (- 50) x_627) + (* (- 60) x_632) + (* (- 70) x_637) + (* (- 80) x_642) + (* (- 90) x_647) + (* (- 100) x_652) + (* (- 110) x_657) + (* (- 40) x_662) + (* (- 50) x_667) + (* (- 60) x_672) + (* (- 70) x_677) + (* (- 40) x_682) + (* (- 50) x_687) + (* (- 60) x_692) + (* (- 70) x_697) + (* (- 80) x_702) + (* (- 90) x_707) + (* (- 100) x_712) + (* (- 110) x_717) + (* (- 120) x_722) + (* (- 40) x_727) + (* (- 50) x_732) + (* (- 60) x_737) + (* (- 70) x_742) + (* (- 80) x_747) + (* (- 90) x_752) + (* (- 100) x_757) + (* (- 110) x_762) + (* (- 40) x_767) + (* (- 50) x_772) + (* (- 40) x_777) + (* (- 50) x_782) + (* (- 40) x_787) + (* (- 50) x_792) + (* (- 60) x_797) + (* (- 70) x_802) + (* (- 80) x_807) + (* (- 90) x_812) + (* (- 100) x_817) + (* (- 40) x_822) + (* (- 50) x_827) + (* (- 60) x_832) + (* (- 70) x_837) + (* (- 80) x_842) + (* (- 90) x_847) + (* (- 100) x_852) + (* (- 110) x_857) + (* (- 40) x_862) + (* (- 50) x_867) + (* (- 60) x_872) + (* (- 70) x_877) + (* (- 80) x_882) + (* (- 90) x_887) + (* (- 40) x_892) + (* (- 50) x_897) + (* (- 60) x_902) + (* (- 70) x_907) + (* (- 80) x_912) + (* (- 90) x_917) + (* (- 100) x_922) + (* (- 52) x_927) + (* (- 52) x_932) + (* (- 65) x_937) + (* (- 52) x_942) + (* (- 52) x_947) + (* (- 65) x_952) + (* (- 52) x_957) + (* (- 65) x_962) + (* (- 52) x_967) + (* (- 65) x_972) + (* (- 78) x_977) + (* (- 91) x_982) + (* (- 104) x_987) + (* (- 117) x_992) + (* (- 130) x_997) + (* (- 40) x_2)))) +(assert (<= 0 + (+ (* 4500 x_1604) + (* (- 50) x_8) + (* (- 40) x_13) + (* (- 50) x_18) + (* (- 60) x_23) + (* (- 40) x_28) + (* (- 40) x_33) + (* (- 50) x_38) + (* (- 40) x_43) + (* (- 40) x_48) + (* (- 40) x_53) + (* (- 50) x_58) + (* (- 40) x_63) + (* (- 40) x_68) + (* (- 50) x_73) + (* (- 60) x_78) + (* (- 70) x_83) + (* (- 80) x_88) + (* (- 90) x_93) + (* (- 100) x_98) + (* (- 40) x_103) + (* (- 50) x_108) + (* (- 60) x_113) + (* (- 70) x_118) + (* (- 40) x_123) + (* (- 50) x_128) + (* (- 60) x_133) + (* (- 70) x_138) + (* (- 80) x_143) + (* (- 90) x_148) + (* (- 100) x_153) + (* (- 110) x_158) + (* (- 120) x_163) + (* (- 40) x_168) + (* (- 50) x_173) + (* (- 60) x_178) + (* (- 70) x_183) + (* (- 40) x_188) + (* (- 50) x_193) + (* (- 60) x_198) + (* (- 40) x_203) + (* (- 50) x_208) + (* (- 40) x_213) + (* (- 50) x_218) + (* (- 60) x_223) + (* (- 70) x_228) + (* (- 80) x_233) + (* (- 90) x_238) + (* (- 100) x_243) + (* (- 110) x_248) + (* (- 40) x_253) + (* (- 50) x_258) + (* (- 60) x_263) + (* (- 70) x_268) + (* (- 80) x_273) + (* (- 90) x_278) + (* (- 100) x_283) + (* (- 40) x_288) + (* (- 50) x_293) + (* (- 60) x_298) + (* (- 70) x_303) + (* (- 80) x_308) + (* (- 90) x_313) + (* (- 100) x_318) + (* (- 110) x_323) + (* (- 40) x_328) + (* (- 50) x_333) + (* (- 60) x_338) + (* (- 70) x_343) + (* (- 80) x_348) + (* (- 90) x_353) + (* (- 100) x_358) + (* (- 40) x_363) + (* (- 50) x_368) + (* (- 60) x_373) + (* (- 70) x_378) + (* (- 80) x_383) + (* (- 90) x_388) + (* (- 100) x_393) + (* (- 40) x_398) + (* (- 50) x_403) + (* (- 60) x_408) + (* (- 40) x_413) + (* (- 50) x_418) + (* (- 60) x_423) + (* (- 70) x_428) + (* (- 80) x_433) + (* (- 90) x_438) + (* (- 100) x_443) + (* (- 110) x_448) + (* (- 120) x_453) + (* (- 130) x_458) + (* (- 40) x_463) + (* (- 50) x_468) + (* (- 60) x_473) + (* (- 70) x_478) + (* (- 80) x_483) + (* (- 90) x_488) + (* (- 40) x_493) + (* (- 40) x_498) + (* (- 50) x_503) + (* (- 60) x_508) + (* (- 70) x_513) + (* (- 80) x_518) + (* (- 90) x_523) + (* (- 40) x_528) + (* (- 50) x_533) + (* (- 60) x_538) + (* (- 40) x_543) + (* (- 50) x_548) + (* (- 60) x_553) + (* (- 70) x_558) + (* (- 40) x_563) + (* (- 50) x_568) + (* (- 60) x_573) + (* (- 70) x_578) + (* (- 80) x_583) + (* (- 90) x_588) + (* (- 40) x_593) + (* (- 40) x_598) + (* (- 50) x_603) + (* (- 60) x_608) + (* (- 70) x_613) + (* (- 80) x_618) + (* (- 40) x_623) + (* (- 50) x_628) + (* (- 60) x_633) + (* (- 70) x_638) + (* (- 80) x_643) + (* (- 90) x_648) + (* (- 100) x_653) + (* (- 110) x_658) + (* (- 40) x_663) + (* (- 50) x_668) + (* (- 60) x_673) + (* (- 70) x_678) + (* (- 40) x_683) + (* (- 50) x_688) + (* (- 60) x_693) + (* (- 70) x_698) + (* (- 80) x_703) + (* (- 90) x_708) + (* (- 100) x_713) + (* (- 110) x_718) + (* (- 120) x_723) + (* (- 40) x_728) + (* (- 50) x_733) + (* (- 60) x_738) + (* (- 70) x_743) + (* (- 80) x_748) + (* (- 90) x_753) + (* (- 100) x_758) + (* (- 110) x_763) + (* (- 40) x_768) + (* (- 50) x_773) + (* (- 40) x_778) + (* (- 50) x_783) + (* (- 40) x_788) + (* (- 50) x_793) + (* (- 60) x_798) + (* (- 70) x_803) + (* (- 80) x_808) + (* (- 90) x_813) + (* (- 100) x_818) + (* (- 40) x_823) + (* (- 50) x_828) + (* (- 60) x_833) + (* (- 70) x_838) + (* (- 80) x_843) + (* (- 90) x_848) + (* (- 100) x_853) + (* (- 110) x_858) + (* (- 40) x_863) + (* (- 50) x_868) + (* (- 60) x_873) + (* (- 70) x_878) + (* (- 80) x_883) + (* (- 90) x_888) + (* (- 40) x_893) + (* (- 50) x_898) + (* (- 60) x_903) + (* (- 70) x_908) + (* (- 80) x_913) + (* (- 90) x_918) + (* (- 100) x_923) + (* (- 52) x_928) + (* (- 52) x_933) + (* (- 65) x_938) + (* (- 52) x_943) + (* (- 52) x_948) + (* (- 65) x_953) + (* (- 52) x_958) + (* (- 65) x_963) + (* (- 52) x_968) + (* (- 65) x_973) + (* (- 78) x_978) + (* (- 91) x_983) + (* (- 104) x_988) + (* (- 117) x_993) + (* (- 130) x_998) + (* (- 40) x_3)))) +(assert (<= 0 + (+ (* 3850 x_1001) + (* (- 30) x_9) + (* (- 24) x_14) + (* (- 30) x_19) + (* (- 36) x_24) + (* (- 24) x_29) + (* (- 24) x_34) + (* (- 30) x_39) + (* (- 24) x_44) + (* (- 24) x_49) + (* (- 24) x_54) + (* (- 30) x_59) + (* (- 24) x_64) + (* (- 24) x_69) + (* (- 30) x_74) + (* (- 36) x_79) + (* (- 42) x_84) + (* (- 48) x_89) + (* (- 54) x_94) + (* (- 60) x_99) + (* (- 24) x_104) + (* (- 30) x_109) + (* (- 36) x_114) + (* (- 42) x_119) + (* (- 24) x_124) + (* (- 30) x_129) + (* (- 36) x_134) + (* (- 42) x_139) + (* (- 48) x_144) + (* (- 54) x_149) + (* (- 60) x_154) + (* (- 66) x_159) + (* (- 72) x_164) + (* (- 24) x_169) + (* (- 30) x_174) + (* (- 36) x_179) + (* (- 42) x_184) + (* (- 24) x_189) + (* (- 30) x_194) + (* (- 36) x_199) + (* (- 24) x_204) + (* (- 30) x_209) + (* (- 24) x_214) + (* (- 30) x_219) + (* (- 36) x_224) + (* (- 42) x_229) + (* (- 48) x_234) + (* (- 54) x_239) + (* (- 60) x_244) + (* (- 66) x_249) + (* (- 24) x_254) + (* (- 30) x_259) + (* (- 36) x_264) + (* (- 42) x_269) + (* (- 48) x_274) + (* (- 54) x_279) + (* (- 60) x_284) + (* (- 24) x_289) + (* (- 30) x_294) + (* (- 36) x_299) + (* (- 42) x_304) + (* (- 48) x_309) + (* (- 54) x_314) + (* (- 60) x_319) + (* (- 66) x_324) + (* (- 24) x_329) + (* (- 30) x_334) + (* (- 36) x_339) + (* (- 42) x_344) + (* (- 48) x_349) + (* (- 54) x_354) + (* (- 60) x_359) + (* (- 24) x_364) + (* (- 30) x_369) + (* (- 36) x_374) + (* (- 42) x_379) + (* (- 48) x_384) + (* (- 54) x_389) + (* (- 60) x_394) + (* (- 24) x_399) + (* (- 30) x_404) + (* (- 36) x_409) + (* (- 24) x_414) + (* (- 30) x_419) + (* (- 36) x_424) + (* (- 42) x_429) + (* (- 48) x_434) + (* (- 54) x_439) + (* (- 60) x_444) + (* (- 66) x_449) + (* (- 72) x_454) + (* (- 78) x_459) + (* (- 24) x_464) + (* (- 30) x_469) + (* (- 36) x_474) + (* (- 42) x_479) + (* (- 48) x_484) + (* (- 54) x_489) + (* (- 24) x_494) + (* (- 24) x_499) + (* (- 30) x_504) + (* (- 36) x_509) + (* (- 42) x_514) + (* (- 48) x_519) + (* (- 54) x_524) + (* (- 24) x_529) + (* (- 30) x_534) + (* (- 36) x_539) + (* (- 24) x_544) + (* (- 30) x_549) + (* (- 36) x_554) + (* (- 42) x_559) + (* (- 24) x_564) + (* (- 30) x_569) + (* (- 36) x_574) + (* (- 42) x_579) + (* (- 48) x_584) + (* (- 54) x_589) + (* (- 24) x_594) + (* (- 24) x_599) + (* (- 30) x_604) + (* (- 36) x_609) + (* (- 42) x_614) + (* (- 48) x_619) + (* (- 24) x_624) + (* (- 30) x_629) + (* (- 36) x_634) + (* (- 42) x_639) + (* (- 48) x_644) + (* (- 54) x_649) + (* (- 60) x_654) + (* (- 66) x_659) + (* (- 24) x_664) + (* (- 30) x_669) + (* (- 36) x_674) + (* (- 42) x_679) + (* (- 24) x_684) + (* (- 30) x_689) + (* (- 36) x_694) + (* (- 42) x_699) + (* (- 48) x_704) + (* (- 54) x_709) + (* (- 60) x_714) + (* (- 66) x_719) + (* (- 72) x_724) + (* (- 24) x_729) + (* (- 30) x_734) + (* (- 36) x_739) + (* (- 42) x_744) + (* (- 48) x_749) + (* (- 54) x_754) + (* (- 60) x_759) + (* (- 66) x_764) + (* (- 24) x_769) + (* (- 30) x_774) + (* (- 24) x_779) + (* (- 30) x_784) + (* (- 24) x_789) + (* (- 30) x_794) + (* (- 36) x_799) + (* (- 42) x_804) + (* (- 48) x_809) + (* (- 54) x_814) + (* (- 60) x_819) + (* (- 24) x_824) + (* (- 30) x_829) + (* (- 36) x_834) + (* (- 42) x_839) + (* (- 48) x_844) + (* (- 54) x_849) + (* (- 60) x_854) + (* (- 66) x_859) + (* (- 24) x_864) + (* (- 30) x_869) + (* (- 36) x_874) + (* (- 42) x_879) + (* (- 48) x_884) + (* (- 54) x_889) + (* (- 24) x_894) + (* (- 30) x_899) + (* (- 36) x_904) + (* (- 42) x_909) + (* (- 48) x_914) + (* (- 54) x_919) + (* (- 60) x_924) + (* (- 36) x_929) + (* (- 36) x_934) + (* (- 45) x_939) + (* (- 36) x_944) + (* (- 36) x_949) + (* (- 45) x_954) + (* (- 36) x_959) + (* (- 45) x_964) + (* (- 36) x_969) + (* (- 45) x_974) + (* (- 54) x_979) + (* (- 63) x_984) + (* (- 72) x_989) + (* (- 81) x_994) + (* (- 90) x_999) + (* (- 24) x_4)))) +(assert (<= 0 + (+ (* 3000 x_1202) + (* (- 30) x_6) + (* (- 24) x_11) + (* (- 30) x_16) + (* (- 36) x_21) + (* (- 24) x_26) + (* (- 24) x_31) + (* (- 30) x_36) + (* (- 24) x_41) + (* (- 24) x_46) + (* (- 24) x_51) + (* (- 30) x_56) + (* (- 24) x_61) + (* (- 24) x_66) + (* (- 30) x_71) + (* (- 36) x_76) + (* (- 42) x_81) + (* (- 48) x_86) + (* (- 54) x_91) + (* (- 60) x_96) + (* (- 24) x_101) + (* (- 30) x_106) + (* (- 36) x_111) + (* (- 42) x_116) + (* (- 24) x_121) + (* (- 30) x_126) + (* (- 36) x_131) + (* (- 42) x_136) + (* (- 48) x_141) + (* (- 54) x_146) + (* (- 60) x_151) + (* (- 66) x_156) + (* (- 72) x_161) + (* (- 24) x_166) + (* (- 30) x_171) + (* (- 36) x_176) + (* (- 42) x_181) + (* (- 24) x_186) + (* (- 30) x_191) + (* (- 36) x_196) + (* (- 24) x_201) + (* (- 30) x_206) + (* (- 24) x_211) + (* (- 30) x_216) + (* (- 36) x_221) + (* (- 42) x_226) + (* (- 48) x_231) + (* (- 54) x_236) + (* (- 60) x_241) + (* (- 66) x_246) + (* (- 24) x_251) + (* (- 30) x_256) + (* (- 36) x_261) + (* (- 42) x_266) + (* (- 48) x_271) + (* (- 54) x_276) + (* (- 60) x_281) + (* (- 24) x_286) + (* (- 30) x_291) + (* (- 36) x_296) + (* (- 42) x_301) + (* (- 48) x_306) + (* (- 54) x_311) + (* (- 60) x_316) + (* (- 66) x_321) + (* (- 24) x_326) + (* (- 30) x_331) + (* (- 36) x_336) + (* (- 42) x_341) + (* (- 48) x_346) + (* (- 54) x_351) + (* (- 60) x_356) + (* (- 24) x_361) + (* (- 30) x_366) + (* (- 36) x_371) + (* (- 42) x_376) + (* (- 48) x_381) + (* (- 54) x_386) + (* (- 60) x_391) + (* (- 24) x_396) + (* (- 30) x_401) + (* (- 36) x_406) + (* (- 24) x_411) + (* (- 30) x_416) + (* (- 36) x_421) + (* (- 42) x_426) + (* (- 48) x_431) + (* (- 54) x_436) + (* (- 60) x_441) + (* (- 66) x_446) + (* (- 72) x_451) + (* (- 78) x_456) + (* (- 24) x_461) + (* (- 30) x_466) + (* (- 36) x_471) + (* (- 42) x_476) + (* (- 48) x_481) + (* (- 54) x_486) + (* (- 24) x_491) + (* (- 24) x_496) + (* (- 30) x_501) + (* (- 36) x_506) + (* (- 42) x_511) + (* (- 48) x_516) + (* (- 54) x_521) + (* (- 24) x_526) + (* (- 30) x_531) + (* (- 36) x_536) + (* (- 24) x_541) + (* (- 30) x_546) + (* (- 36) x_551) + (* (- 42) x_556) + (* (- 24) x_561) + (* (- 30) x_566) + (* (- 36) x_571) + (* (- 42) x_576) + (* (- 48) x_581) + (* (- 54) x_586) + (* (- 24) x_591) + (* (- 24) x_596) + (* (- 30) x_601) + (* (- 36) x_606) + (* (- 42) x_611) + (* (- 48) x_616) + (* (- 24) x_621) + (* (- 30) x_626) + (* (- 36) x_631) + (* (- 42) x_636) + (* (- 48) x_641) + (* (- 54) x_646) + (* (- 60) x_651) + (* (- 66) x_656) + (* (- 24) x_661) + (* (- 30) x_666) + (* (- 36) x_671) + (* (- 42) x_676) + (* (- 24) x_681) + (* (- 30) x_686) + (* (- 36) x_691) + (* (- 42) x_696) + (* (- 48) x_701) + (* (- 54) x_706) + (* (- 60) x_711) + (* (- 66) x_716) + (* (- 72) x_721) + (* (- 24) x_726) + (* (- 30) x_731) + (* (- 36) x_736) + (* (- 42) x_741) + (* (- 48) x_746) + (* (- 54) x_751) + (* (- 60) x_756) + (* (- 66) x_761) + (* (- 24) x_766) + (* (- 30) x_771) + (* (- 24) x_776) + (* (- 30) x_781) + (* (- 24) x_786) + (* (- 30) x_791) + (* (- 36) x_796) + (* (- 42) x_801) + (* (- 48) x_806) + (* (- 54) x_811) + (* (- 60) x_816) + (* (- 24) x_821) + (* (- 30) x_826) + (* (- 36) x_831) + (* (- 42) x_836) + (* (- 48) x_841) + (* (- 54) x_846) + (* (- 60) x_851) + (* (- 66) x_856) + (* (- 24) x_861) + (* (- 30) x_866) + (* (- 36) x_871) + (* (- 42) x_876) + (* (- 48) x_881) + (* (- 54) x_886) + (* (- 24) x_891) + (* (- 30) x_896) + (* (- 36) x_901) + (* (- 42) x_906) + (* (- 48) x_911) + (* (- 54) x_916) + (* (- 60) x_921) + (* (- 36) x_926) + (* (- 36) x_931) + (* (- 45) x_936) + (* (- 36) x_941) + (* (- 36) x_946) + (* (- 45) x_951) + (* (- 36) x_956) + (* (- 45) x_961) + (* (- 36) x_966) + (* (- 45) x_971) + (* (- 54) x_976) + (* (- 63) x_981) + (* (- 72) x_986) + (* (- 81) x_991) + (* (- 90) x_996) + (* (- 24) x_1)))) +(assert (<= 0 + (+ (* 7700 x_1403) + (* (- 30) x_7) + (* (- 24) x_12) + (* (- 30) x_17) + (* (- 36) x_22) + (* (- 24) x_27) + (* (- 24) x_32) + (* (- 30) x_37) + (* (- 24) x_42) + (* (- 24) x_47) + (* (- 24) x_52) + (* (- 30) x_57) + (* (- 24) x_62) + (* (- 24) x_67) + (* (- 30) x_72) + (* (- 36) x_77) + (* (- 42) x_82) + (* (- 48) x_87) + (* (- 54) x_92) + (* (- 60) x_97) + (* (- 24) x_102) + (* (- 30) x_107) + (* (- 36) x_112) + (* (- 42) x_117) + (* (- 24) x_122) + (* (- 30) x_127) + (* (- 36) x_132) + (* (- 42) x_137) + (* (- 48) x_142) + (* (- 54) x_147) + (* (- 60) x_152) + (* (- 66) x_157) + (* (- 72) x_162) + (* (- 24) x_167) + (* (- 30) x_172) + (* (- 36) x_177) + (* (- 42) x_182) + (* (- 24) x_187) + (* (- 30) x_192) + (* (- 36) x_197) + (* (- 24) x_202) + (* (- 30) x_207) + (* (- 24) x_212) + (* (- 30) x_217) + (* (- 36) x_222) + (* (- 42) x_227) + (* (- 48) x_232) + (* (- 54) x_237) + (* (- 60) x_242) + (* (- 66) x_247) + (* (- 24) x_252) + (* (- 30) x_257) + (* (- 36) x_262) + (* (- 42) x_267) + (* (- 48) x_272) + (* (- 54) x_277) + (* (- 60) x_282) + (* (- 24) x_287) + (* (- 30) x_292) + (* (- 36) x_297) + (* (- 42) x_302) + (* (- 48) x_307) + (* (- 54) x_312) + (* (- 60) x_317) + (* (- 66) x_322) + (* (- 24) x_327) + (* (- 30) x_332) + (* (- 36) x_337) + (* (- 42) x_342) + (* (- 48) x_347) + (* (- 54) x_352) + (* (- 60) x_357) + (* (- 24) x_362) + (* (- 30) x_367) + (* (- 36) x_372) + (* (- 42) x_377) + (* (- 48) x_382) + (* (- 54) x_387) + (* (- 60) x_392) + (* (- 24) x_397) + (* (- 30) x_402) + (* (- 36) x_407) + (* (- 24) x_412) + (* (- 30) x_417) + (* (- 36) x_422) + (* (- 42) x_427) + (* (- 48) x_432) + (* (- 54) x_437) + (* (- 60) x_442) + (* (- 66) x_447) + (* (- 72) x_452) + (* (- 78) x_457) + (* (- 24) x_462) + (* (- 30) x_467) + (* (- 36) x_472) + (* (- 42) x_477) + (* (- 48) x_482) + (* (- 54) x_487) + (* (- 24) x_492) + (* (- 24) x_497) + (* (- 30) x_502) + (* (- 36) x_507) + (* (- 42) x_512) + (* (- 48) x_517) + (* (- 54) x_522) + (* (- 24) x_527) + (* (- 30) x_532) + (* (- 36) x_537) + (* (- 24) x_542) + (* (- 30) x_547) + (* (- 36) x_552) + (* (- 42) x_557) + (* (- 24) x_562) + (* (- 30) x_567) + (* (- 36) x_572) + (* (- 42) x_577) + (* (- 48) x_582) + (* (- 54) x_587) + (* (- 24) x_592) + (* (- 24) x_597) + (* (- 30) x_602) + (* (- 36) x_607) + (* (- 42) x_612) + (* (- 48) x_617) + (* (- 24) x_622) + (* (- 30) x_627) + (* (- 36) x_632) + (* (- 42) x_637) + (* (- 48) x_642) + (* (- 54) x_647) + (* (- 60) x_652) + (* (- 66) x_657) + (* (- 24) x_662) + (* (- 30) x_667) + (* (- 36) x_672) + (* (- 42) x_677) + (* (- 24) x_682) + (* (- 30) x_687) + (* (- 36) x_692) + (* (- 42) x_697) + (* (- 48) x_702) + (* (- 54) x_707) + (* (- 60) x_712) + (* (- 66) x_717) + (* (- 72) x_722) + (* (- 24) x_727) + (* (- 30) x_732) + (* (- 36) x_737) + (* (- 42) x_742) + (* (- 48) x_747) + (* (- 54) x_752) + (* (- 60) x_757) + (* (- 66) x_762) + (* (- 24) x_767) + (* (- 30) x_772) + (* (- 24) x_777) + (* (- 30) x_782) + (* (- 24) x_787) + (* (- 30) x_792) + (* (- 36) x_797) + (* (- 42) x_802) + (* (- 48) x_807) + (* (- 54) x_812) + (* (- 60) x_817) + (* (- 24) x_822) + (* (- 30) x_827) + (* (- 36) x_832) + (* (- 42) x_837) + (* (- 48) x_842) + (* (- 54) x_847) + (* (- 60) x_852) + (* (- 66) x_857) + (* (- 24) x_862) + (* (- 30) x_867) + (* (- 36) x_872) + (* (- 42) x_877) + (* (- 48) x_882) + (* (- 54) x_887) + (* (- 24) x_892) + (* (- 30) x_897) + (* (- 36) x_902) + (* (- 42) x_907) + (* (- 48) x_912) + (* (- 54) x_917) + (* (- 60) x_922) + (* (- 36) x_927) + (* (- 36) x_932) + (* (- 45) x_937) + (* (- 36) x_942) + (* (- 36) x_947) + (* (- 45) x_952) + (* (- 36) x_957) + (* (- 45) x_962) + (* (- 36) x_967) + (* (- 45) x_972) + (* (- 54) x_977) + (* (- 63) x_982) + (* (- 72) x_987) + (* (- 81) x_992) + (* (- 90) x_997) + (* (- 24) x_2)))) +(assert (<= 0 + (+ (* 3960 x_1604) + (* (- 30) x_8) + (* (- 24) x_13) + (* (- 30) x_18) + (* (- 36) x_23) + (* (- 24) x_28) + (* (- 24) x_33) + (* (- 30) x_38) + (* (- 24) x_43) + (* (- 24) x_48) + (* (- 24) x_53) + (* (- 30) x_58) + (* (- 24) x_63) + (* (- 24) x_68) + (* (- 30) x_73) + (* (- 36) x_78) + (* (- 42) x_83) + (* (- 48) x_88) + (* (- 54) x_93) + (* (- 60) x_98) + (* (- 24) x_103) + (* (- 30) x_108) + (* (- 36) x_113) + (* (- 42) x_118) + (* (- 24) x_123) + (* (- 30) x_128) + (* (- 36) x_133) + (* (- 42) x_138) + (* (- 48) x_143) + (* (- 54) x_148) + (* (- 60) x_153) + (* (- 66) x_158) + (* (- 72) x_163) + (* (- 24) x_168) + (* (- 30) x_173) + (* (- 36) x_178) + (* (- 42) x_183) + (* (- 24) x_188) + (* (- 30) x_193) + (* (- 36) x_198) + (* (- 24) x_203) + (* (- 30) x_208) + (* (- 24) x_213) + (* (- 30) x_218) + (* (- 36) x_223) + (* (- 42) x_228) + (* (- 48) x_233) + (* (- 54) x_238) + (* (- 60) x_243) + (* (- 66) x_248) + (* (- 24) x_253) + (* (- 30) x_258) + (* (- 36) x_263) + (* (- 42) x_268) + (* (- 48) x_273) + (* (- 54) x_278) + (* (- 60) x_283) + (* (- 24) x_288) + (* (- 30) x_293) + (* (- 36) x_298) + (* (- 42) x_303) + (* (- 48) x_308) + (* (- 54) x_313) + (* (- 60) x_318) + (* (- 66) x_323) + (* (- 24) x_328) + (* (- 30) x_333) + (* (- 36) x_338) + (* (- 42) x_343) + (* (- 48) x_348) + (* (- 54) x_353) + (* (- 60) x_358) + (* (- 24) x_363) + (* (- 30) x_368) + (* (- 36) x_373) + (* (- 42) x_378) + (* (- 48) x_383) + (* (- 54) x_388) + (* (- 60) x_393) + (* (- 24) x_398) + (* (- 30) x_403) + (* (- 36) x_408) + (* (- 24) x_413) + (* (- 30) x_418) + (* (- 36) x_423) + (* (- 42) x_428) + (* (- 48) x_433) + (* (- 54) x_438) + (* (- 60) x_443) + (* (- 66) x_448) + (* (- 72) x_453) + (* (- 78) x_458) + (* (- 24) x_463) + (* (- 30) x_468) + (* (- 36) x_473) + (* (- 42) x_478) + (* (- 48) x_483) + (* (- 54) x_488) + (* (- 24) x_493) + (* (- 24) x_498) + (* (- 30) x_503) + (* (- 36) x_508) + (* (- 42) x_513) + (* (- 48) x_518) + (* (- 54) x_523) + (* (- 24) x_528) + (* (- 30) x_533) + (* (- 36) x_538) + (* (- 24) x_543) + (* (- 30) x_548) + (* (- 36) x_553) + (* (- 42) x_558) + (* (- 24) x_563) + (* (- 30) x_568) + (* (- 36) x_573) + (* (- 42) x_578) + (* (- 48) x_583) + (* (- 54) x_588) + (* (- 24) x_593) + (* (- 24) x_598) + (* (- 30) x_603) + (* (- 36) x_608) + (* (- 42) x_613) + (* (- 48) x_618) + (* (- 24) x_623) + (* (- 30) x_628) + (* (- 36) x_633) + (* (- 42) x_638) + (* (- 48) x_643) + (* (- 54) x_648) + (* (- 60) x_653) + (* (- 66) x_658) + (* (- 24) x_663) + (* (- 30) x_668) + (* (- 36) x_673) + (* (- 42) x_678) + (* (- 24) x_683) + (* (- 30) x_688) + (* (- 36) x_693) + (* (- 42) x_698) + (* (- 48) x_703) + (* (- 54) x_708) + (* (- 60) x_713) + (* (- 66) x_718) + (* (- 72) x_723) + (* (- 24) x_728) + (* (- 30) x_733) + (* (- 36) x_738) + (* (- 42) x_743) + (* (- 48) x_748) + (* (- 54) x_753) + (* (- 60) x_758) + (* (- 66) x_763) + (* (- 24) x_768) + (* (- 30) x_773) + (* (- 24) x_778) + (* (- 30) x_783) + (* (- 24) x_788) + (* (- 30) x_793) + (* (- 36) x_798) + (* (- 42) x_803) + (* (- 48) x_808) + (* (- 54) x_813) + (* (- 60) x_818) + (* (- 24) x_823) + (* (- 30) x_828) + (* (- 36) x_833) + (* (- 42) x_838) + (* (- 48) x_843) + (* (- 54) x_848) + (* (- 60) x_853) + (* (- 66) x_858) + (* (- 24) x_863) + (* (- 30) x_868) + (* (- 36) x_873) + (* (- 42) x_878) + (* (- 48) x_883) + (* (- 54) x_888) + (* (- 24) x_893) + (* (- 30) x_898) + (* (- 36) x_903) + (* (- 42) x_908) + (* (- 48) x_913) + (* (- 54) x_918) + (* (- 60) x_923) + (* (- 36) x_928) + (* (- 36) x_933) + (* (- 45) x_938) + (* (- 36) x_943) + (* (- 36) x_948) + (* (- 45) x_953) + (* (- 36) x_958) + (* (- 45) x_963) + (* (- 36) x_968) + (* (- 45) x_973) + (* (- 54) x_978) + (* (- 63) x_983) + (* (- 72) x_988) + (* (- 81) x_993) + (* (- 90) x_998) + (* (- 24) x_3)))) + +(assert (= x_1202 1)) +(assert (= x_1403 1)) +(assert (= x_1604 0)) +(assert (= x_1001 0)) + +;(minimize (+ x_1202 x_1403 x_1604 x_1001)) +(minimize (+ (* 2 x_1) + (* 3 x_2) + (* 4 x_3) + x_9 + (* 2 x_6) + (* 3 x_7) + (* 4 x_8) + x_14 + (* 2 x_11) + (* 3 x_12) + (* 4 x_13) + x_19 + (* 2 x_16) + (* 3 x_17) + (* 4 x_18) + x_24 + (* 2 x_21) + (* 3 x_22) + (* 4 x_23) + x_29 + (* 2 x_26) + (* 3 x_27) + (* 4 x_28) + x_34 + (* 2 x_31) + (* 3 x_32) + (* 4 x_33) + x_39 + (* 2 x_36) + (* 3 x_37) + (* 4 x_38) + x_44 + (* 2 x_41) + (* 3 x_42) + (* 4 x_43) + x_49 + (* 2 x_46) + (* 3 x_47) + (* 4 x_48) + x_54 + (* 2 x_51) + (* 3 x_52) + (* 4 x_53) + x_59 + (* 2 x_56) + (* 3 x_57) + (* 4 x_58) + x_64 + (* 2 x_61) + (* 3 x_62) + (* 4 x_63) + x_69 + (* 2 x_66) + (* 3 x_67) + (* 4 x_68) + x_74 + (* 2 x_71) + (* 3 x_72) + (* 4 x_73) + x_79 + (* 2 x_76) + (* 3 x_77) + (* 4 x_78) + x_84 + (* 2 x_81) + (* 3 x_82) + (* 4 x_83) + x_89 + (* 2 x_86) + (* 3 x_87) + (* 4 x_88) + x_94 + (* 2 x_91) + (* 3 x_92) + (* 4 x_93) + x_99 + (* 2 x_96) + (* 3 x_97) + (* 4 x_98) + x_104 + (* 2 x_101) + (* 3 x_102) + (* 4 x_103) + x_109 + (* 2 x_106) + (* 3 x_107) + (* 4 x_108) + x_114 + (* 2 x_111) + (* 3 x_112) + (* 4 x_113) + x_119 + (* 2 x_116) + (* 3 x_117) + (* 4 x_118) + x_124 + (* 2 x_121) + (* 3 x_122) + (* 4 x_123) + x_129 + (* 2 x_126) + (* 3 x_127) + (* 4 x_128) + x_134 + (* 2 x_131) + (* 3 x_132) + (* 4 x_133) + x_139 + (* 2 x_136) + (* 3 x_137) + (* 4 x_138) + x_144 + (* 2 x_141) + (* 3 x_142) + (* 4 x_143) + x_149 + (* 2 x_146) + (* 3 x_147) + (* 4 x_148) + x_154 + (* 2 x_151) + (* 3 x_152) + (* 4 x_153) + x_159 + (* 2 x_156) + (* 3 x_157) + (* 4 x_158) + x_164 + (* 2 x_161) + (* 3 x_162) + (* 4 x_163) + x_169 + (* 2 x_166) + (* 3 x_167) + (* 4 x_168) + x_174 + (* 2 x_171) + (* 3 x_172) + (* 4 x_173) + x_179 + (* 2 x_176) + (* 3 x_177) + (* 4 x_178) + x_184 + (* 2 x_181) + (* 3 x_182) + (* 4 x_183) + x_189 + (* 2 x_186) + (* 3 x_187) + (* 4 x_188) + x_194 + (* 2 x_191) + (* 3 x_192) + (* 4 x_193) + x_199 + (* 2 x_196) + (* 3 x_197) + (* 4 x_198) + x_204 + (* 2 x_201) + (* 3 x_202) + (* 4 x_203) + x_209 + (* 2 x_206) + (* 3 x_207) + (* 4 x_208) + x_214 + (* 2 x_211) + (* 3 x_212) + (* 4 x_213) + x_219 + (* 2 x_216) + (* 3 x_217) + (* 4 x_218) + x_224 + (* 2 x_221) + (* 3 x_222) + (* 4 x_223) + x_229 + (* 2 x_226) + (* 3 x_227) + (* 4 x_228) + x_234 + (* 2 x_231) + (* 3 x_232) + (* 4 x_233) + x_239 + (* 2 x_236) + (* 3 x_237) + (* 4 x_238) + x_244 + (* 2 x_241) + (* 3 x_242) + (* 4 x_243) + x_249 + (* 2 x_246) + (* 3 x_247) + (* 4 x_248) + x_254 + (* 2 x_251) + (* 3 x_252) + (* 4 x_253) + x_259 + (* 2 x_256) + (* 3 x_257) + (* 4 x_258) + x_264 + (* 2 x_261) + (* 3 x_262) + (* 4 x_263) + x_269 + (* 2 x_266) + (* 3 x_267) + (* 4 x_268) + x_274 + (* 2 x_271) + (* 3 x_272) + (* 4 x_273) + x_279 + (* 2 x_276) + (* 3 x_277) + (* 4 x_278) + x_284 + (* 2 x_281) + (* 3 x_282) + (* 4 x_283) + x_289 + (* 2 x_286) + (* 3 x_287) + (* 4 x_288) + x_294 + (* 2 x_291) + (* 3 x_292) + (* 4 x_293) + x_299 + (* 2 x_296) + (* 3 x_297) + (* 4 x_298) + x_304 + (* 2 x_301) + (* 3 x_302) + (* 4 x_303) + x_309 + (* 2 x_306) + (* 3 x_307) + (* 4 x_308) + x_314 + (* 2 x_311) + (* 3 x_312) + (* 4 x_313) + x_319 + (* 2 x_316) + (* 3 x_317) + (* 4 x_318) + x_324 + (* 2 x_321) + (* 3 x_322) + (* 4 x_323) + x_329 + (* 2 x_326) + (* 3 x_327) + (* 4 x_328) + x_334 + (* 2 x_331) + (* 3 x_332) + (* 4 x_333) + x_339 + (* 2 x_336) + (* 3 x_337) + (* 4 x_338) + x_344 + (* 2 x_341) + (* 3 x_342) + (* 4 x_343) + x_349 + (* 2 x_346) + (* 3 x_347) + (* 4 x_348) + x_354 + (* 2 x_351) + (* 3 x_352) + (* 4 x_353) + x_359 + (* 2 x_356) + (* 3 x_357) + (* 4 x_358) + x_364 + (* 2 x_361) + (* 3 x_362) + (* 4 x_363) + x_369 + (* 2 x_366) + (* 3 x_367) + (* 4 x_368) + x_374 + (* 2 x_371) + (* 3 x_372) + (* 4 x_373) + x_379 + (* 2 x_376) + (* 3 x_377) + (* 4 x_378) + x_384 + (* 2 x_381) + (* 3 x_382) + (* 4 x_383) + x_389 + (* 2 x_386) + (* 3 x_387) + (* 4 x_388) + x_394 + (* 2 x_391) + (* 3 x_392) + (* 4 x_393) + x_399 + (* 2 x_396) + (* 3 x_397) + (* 4 x_398) + x_404 + (* 2 x_401) + (* 3 x_402) + (* 4 x_403) + x_409 + (* 2 x_406) + (* 3 x_407) + (* 4 x_408) + x_414 + (* 2 x_411) + (* 3 x_412) + (* 4 x_413) + x_419 + (* 2 x_416) + (* 3 x_417) + (* 4 x_418) + x_424 + (* 2 x_421) + (* 3 x_422) + (* 4 x_423) + x_429 + (* 2 x_426) + (* 3 x_427) + (* 4 x_428) + x_434 + (* 2 x_431) + (* 3 x_432) + (* 4 x_433) + x_439 + (* 2 x_436) + (* 3 x_437) + (* 4 x_438) + x_444 + (* 2 x_441) + (* 3 x_442) + (* 4 x_443) + x_449 + (* 2 x_446) + (* 3 x_447) + (* 4 x_448) + x_454 + (* 2 x_451) + (* 3 x_452) + (* 4 x_453) + x_459 + (* 2 x_456) + (* 3 x_457) + (* 4 x_458) + x_464 + (* 2 x_461) + (* 3 x_462) + (* 4 x_463) + x_469 + (* 2 x_466) + (* 3 x_467) + (* 4 x_468) + x_474 + (* 2 x_471) + (* 3 x_472) + (* 4 x_473) + x_479 + (* 2 x_476) + (* 3 x_477) + (* 4 x_478) + x_484 + (* 2 x_481) + (* 3 x_482) + (* 4 x_483) + x_489 + (* 2 x_486) + (* 3 x_487) + (* 4 x_488) + x_494 + (* 2 x_491) + (* 3 x_492) + (* 4 x_493) + x_499 + (* 2 x_496) + (* 3 x_497) + (* 4 x_498) + x_504 + (* 2 x_501) + (* 3 x_502) + (* 4 x_503) + x_509 + (* 2 x_506) + (* 3 x_507) + (* 4 x_508) + x_514 + (* 2 x_511) + (* 3 x_512) + (* 4 x_513) + x_519 + (* 2 x_516) + (* 3 x_517) + (* 4 x_518) + x_524 + (* 2 x_521) + (* 3 x_522) + (* 4 x_523) + x_529 + (* 2 x_526) + (* 3 x_527) + (* 4 x_528) + x_534 + (* 2 x_531) + (* 3 x_532) + (* 4 x_533) + x_539 + (* 2 x_536) + (* 3 x_537) + (* 4 x_538) + x_544 + (* 2 x_541) + (* 3 x_542) + (* 4 x_543) + x_549 + (* 2 x_546) + (* 3 x_547) + (* 4 x_548) + x_554 + (* 2 x_551) + (* 3 x_552) + (* 4 x_553) + x_559 + (* 2 x_556) + (* 3 x_557) + (* 4 x_558) + x_564 + (* 2 x_561) + (* 3 x_562) + (* 4 x_563) + x_569 + (* 2 x_566) + (* 3 x_567) + (* 4 x_568) + x_574 + (* 2 x_571) + (* 3 x_572) + (* 4 x_573) + x_579 + (* 2 x_576) + (* 3 x_577) + (* 4 x_578) + x_584 + (* 2 x_581) + (* 3 x_582) + (* 4 x_583) + x_589 + (* 2 x_586) + (* 3 x_587) + (* 4 x_588) + x_594 + (* 2 x_591) + (* 3 x_592) + (* 4 x_593) + x_599 + (* 2 x_596) + (* 3 x_597) + (* 4 x_598) + x_604 + (* 2 x_601) + (* 3 x_602) + (* 4 x_603) + x_609 + (* 2 x_606) + (* 3 x_607) + (* 4 x_608) + x_614 + (* 2 x_611) + (* 3 x_612) + (* 4 x_613) + x_619 + (* 2 x_616) + (* 3 x_617) + (* 4 x_618) + x_624 + (* 2 x_621) + (* 3 x_622) + (* 4 x_623) + x_629 + (* 2 x_626) + (* 3 x_627) + (* 4 x_628) + x_634 + (* 2 x_631) + (* 3 x_632) + (* 4 x_633) + x_639 + (* 2 x_636) + (* 3 x_637) + (* 4 x_638) + x_644 + (* 2 x_641) + (* 3 x_642) + (* 4 x_643) + x_649 + (* 2 x_646) + (* 3 x_647) + (* 4 x_648) + x_654 + (* 2 x_651) + (* 3 x_652) + (* 4 x_653) + x_659 + (* 2 x_656) + (* 3 x_657) + (* 4 x_658) + x_664 + (* 2 x_661) + (* 3 x_662) + (* 4 x_663) + x_669 + (* 2 x_666) + (* 3 x_667) + (* 4 x_668) + x_674 + (* 2 x_671) + (* 3 x_672) + (* 4 x_673) + x_679 + (* 2 x_676) + (* 3 x_677) + (* 4 x_678) + x_684 + (* 2 x_681) + (* 3 x_682) + (* 4 x_683) + x_689 + (* 2 x_686) + (* 3 x_687) + (* 4 x_688) + x_694 + (* 2 x_691) + (* 3 x_692) + (* 4 x_693) + x_699 + (* 2 x_696) + (* 3 x_697) + (* 4 x_698) + x_704 + (* 2 x_701) + (* 3 x_702) + (* 4 x_703) + x_709 + (* 2 x_706) + (* 3 x_707) + (* 4 x_708) + x_714 + (* 2 x_711) + (* 3 x_712) + (* 4 x_713) + x_719 + (* 2 x_716) + (* 3 x_717) + (* 4 x_718) + x_724 + (* 2 x_721) + (* 3 x_722) + (* 4 x_723) + x_729 + (* 2 x_726) + (* 3 x_727) + (* 4 x_728) + x_734 + (* 2 x_731) + (* 3 x_732) + (* 4 x_733) + x_739 + (* 2 x_736) + (* 3 x_737) + (* 4 x_738) + x_744 + (* 2 x_741) + (* 3 x_742) + (* 4 x_743) + x_749 + (* 2 x_746) + (* 3 x_747) + (* 4 x_748) + x_754 + (* 2 x_751) + (* 3 x_752) + (* 4 x_753) + x_759 + (* 2 x_756) + (* 3 x_757) + (* 4 x_758) + x_764 + (* 2 x_761) + (* 3 x_762) + (* 4 x_763) + x_769 + (* 2 x_766) + (* 3 x_767) + (* 4 x_768) + x_774 + (* 2 x_771) + (* 3 x_772) + (* 4 x_773) + x_779 + (* 2 x_776) + (* 3 x_777) + (* 4 x_778) + x_784 + (* 2 x_781) + (* 3 x_782) + (* 4 x_783) + x_789 + (* 2 x_786) + (* 3 x_787) + (* 4 x_788) + x_794 + (* 2 x_791) + (* 3 x_792) + (* 4 x_793) + x_799 + (* 2 x_796) + (* 3 x_797) + (* 4 x_798) + x_804 + (* 2 x_801) + (* 3 x_802) + (* 4 x_803) + x_809 + (* 2 x_806) + (* 3 x_807) + (* 4 x_808) + x_814 + (* 2 x_811) + (* 3 x_812) + (* 4 x_813) + x_819 + (* 2 x_816) + (* 3 x_817) + (* 4 x_818) + x_824 + (* 2 x_821) + (* 3 x_822) + (* 4 x_823) + x_829 + (* 2 x_826) + (* 3 x_827) + (* 4 x_828) + x_834 + (* 2 x_831) + (* 3 x_832) + (* 4 x_833) + x_839 + (* 2 x_836) + (* 3 x_837) + (* 4 x_838) + x_844 + (* 2 x_841) + (* 3 x_842) + (* 4 x_843) + x_849 + (* 2 x_846) + (* 3 x_847) + (* 4 x_848) + x_854 + (* 2 x_851) + (* 3 x_852) + (* 4 x_853) + x_859 + (* 2 x_856) + (* 3 x_857) + (* 4 x_858) + x_864 + (* 2 x_861) + (* 3 x_862) + (* 4 x_863) + x_869 + (* 2 x_866) + (* 3 x_867) + (* 4 x_868) + x_874 + (* 2 x_871) + (* 3 x_872) + (* 4 x_873) + x_879 + (* 2 x_876) + (* 3 x_877) + (* 4 x_878) + x_884 + (* 2 x_881) + (* 3 x_882) + (* 4 x_883) + x_889 + (* 2 x_886) + (* 3 x_887) + (* 4 x_888) + x_894 + (* 2 x_891) + (* 3 x_892) + (* 4 x_893) + x_899 + (* 2 x_896) + (* 3 x_897) + (* 4 x_898) + x_904 + (* 2 x_901) + (* 3 x_902) + (* 4 x_903) + x_909 + (* 2 x_906) + (* 3 x_907) + (* 4 x_908) + x_914 + (* 2 x_911) + (* 3 x_912) + (* 4 x_913) + x_919 + (* 2 x_916) + (* 3 x_917) + (* 4 x_918) + x_924 + (* 2 x_921) + (* 3 x_922) + (* 4 x_923) + x_929 + (* 2 x_926) + (* 3 x_927) + (* 4 x_928) + x_934 + (* 2 x_931) + (* 3 x_932) + (* 4 x_933) + x_939 + (* 2 x_936) + (* 3 x_937) + (* 4 x_938) + x_944 + (* 2 x_941) + (* 3 x_942) + (* 4 x_943) + x_949 + (* 2 x_946) + (* 3 x_947) + (* 4 x_948) + x_954 + (* 2 x_951) + (* 3 x_952) + (* 4 x_953) + x_959 + (* 2 x_956) + (* 3 x_957) + (* 4 x_958) + x_964 + (* 2 x_961) + (* 3 x_962) + (* 4 x_963) + x_969 + (* 2 x_966) + (* 3 x_967) + (* 4 x_968) + x_974 + (* 2 x_971) + (* 3 x_972) + (* 4 x_973) + x_979 + (* 2 x_976) + (* 3 x_977) + (* 4 x_978) + x_984 + (* 2 x_981) + (* 3 x_982) + (* 4 x_983) + x_989 + (* 2 x_986) + (* 3 x_987) + (* 4 x_988) + x_994 + (* 2 x_991) + (* 3 x_992) + (* 4 x_993) + x_999 + (* 2 x_996) + (* 3 x_997) + (* 4 x_998) + x_4 + (* 100 x_1202) + (* 100 x_1403) + (* 100 x_1604) + (* 100 x_1001))) +(optimize :print_statistics true + :wmaxsat_engine wmax + :maxsat_engine weighted_maxsat)