f169 = -inf; f168 = -inf; f602 = -inf; f603 = -inf; f604 = -inf; f605 = -inf; f606 = 0; f601 = -inf; f161 = 2; f160 = 0; f163 = 0; f162 = 1; f165 = -inf; f164 = 2; f167 = -inf; f166 = -inf; f749 = 2; f769 = -inf; f768 = -inf; f767 = -inf; f766 = -inf; f765 = -inf; f764 = 1; f763 = -inf; f762 = 0; f761 = 0; f760 = -inf; f607 = 0; f748 = 1; f608 = 1; f651 = 1; f913 = 2; f609 = 1; f1026 = 0; f1027 = 0; f1024 = -inf; f799 = -inf; f886 = -inf; f1023 = -inf; f1020 = -inf; f1021 = -inf; f932 = -inf; f933 = -inf; f930 = -inf; f931 = -inf; f936 = 0; f937 = 0; f934 = -inf; f935 = -inf; f938 = 1; f939 = 1; f310 = 0; f509 = 1; f258 = -inf; f118 = 1; f119 = 2; f114 = 0; f115 = 0; f116 = 1; f117 = 1; f110 = -inf; f111 = 1; f112 = 1; f113 = 2; f699 = 1; f698 = 1; f693 = -inf; f692 = -inf; f691 = -inf; f690 = -inf; f697 = 0; f696 = 0; f695 = -inf; f694 = -inf; f590 = -inf; f591 = 0; f592 = 0; f593 = 1; f594 = 0; f595 = 0; f596 = 1; f597 = 0; f598 = -inf; f599 = 0; f985 = 0; f984 = 1; f983 = 1; f251 = 1; f981 = 0; f980 = -inf; f730 = 0; f250 = 0; f902 = -inf; f978 = -inf; f731 = 1; f790 = 1; f884 = 1; f871 = -inf; f341 = 2; f340 = 0; f343 = 0; f342 = 1; f345 = -inf; f344 = 2; f347 = -inf; f346 = -inf; f349 = -inf; f348 = -inf; f439 = -inf; f438 = -inf; f187 = 0; f186 = 1; f185 = -inf; f184 = -inf; f183 = -inf; f182 = -inf; f181 = -inf; f180 = -inf; f881 = 2; f813 = -inf; f189 = 1; f188 = 2; f928 = -inf; f738 = -inf; f882 = 0; f739 = -inf; f894 = 1; f883 = 0; f888 = -inf; f889 = -inf; f334 = -inf; f335 = -inf; f336 = 2; f337 = 1; f239 = 2; f331 = -inf; f332 = -inf; f333 = -inf; f235 = 1; f234 = 1; f237 = 1; f236 = 2; f338 = 3; f230 = -inf; f233 = 1; f232 = 0; f880 = 0; f891 = 1; f723 = -inf; f385 = 1; f721 = -inf; f720 = -inf; f727 = 1; f726 = 2; f725 = -inf; f384 = 1; f899 = 2; f898 = 1; f729 = 1; f728 = 2; f387 = 1; f386 = 2; f381 = 2; f874 = -inf; f380 = -inf; f1062 = 2; f1063 = 1; f711 = 1; f1061 = 2; f870 = -inf; f383 = 3; f1064 = 2; f1065 = -inf; f1068 = -inf; f382 = 2; f877 = 0; f808 = 1; f700 = 0; f806 = 1; f807 = 1; f804 = 0; f805 = 0; f802 = 1; f803 = 2; f800 = -inf; f801 = 1; f150 = -inf; f151 = -inf; f152 = -inf; f153 = -inf; f154 = -inf; f155 = -inf; f156 = 0; f157 = 0; f158 = 1; f159 = 1; f1029 = 1; f872 = -inf; f796 = -inf; f797 = -inf; f794 = 2; f795 = -inf; f792 = 1; f793 = 1; f659 = 1; f658 = 0; f657 = 0; f656 = 1; f655 = 0; f654 = 0; f653 = 2; f652 = 1; f578 = 1; f650 = -inf; f1025 = -inf; f1022 = -inf; f570 = -inf; f912 = 2; f571 = -inf; f1078 = 1; f1083 = -inf; f0 = 1; f1 = 1; f2 = 1; f3 = 0; f4 = -inf; f5 = 0; f6 = 0; f7 = 0; f8 = 0; f9 = -inf; f389 = 2; f388 = 1; f572 = -inf; f573 = -inf; f479 = 1; f478 = -inf; f576 = 0; f577 = 0; f574 = -inf; f575 = -inf; f473 = 1; f472 = 0; f471 = 0; f470 = -inf; f477 = 0; f476 = 0; f475 = -inf; f474 = 0; f833 = 1; f579 = 0; f832 = 0; f831 = 0; f900 = -inf; f977 = -inf; f974 = 0; f830 = -inf; f972 = 0; f973 = -inf; f970 = 0; f971 = 1; f837 = 0; f454 = -inf; f836 = 0; f1048 = 0; f434 = 2; f835 = -inf; f834 = 0; f271 = -inf; f270 = -inf; f273 = -inf; f272 = -inf; f275 = -inf; f274 = -inf; f277 = 0; f276 = 0; f279 = 0; f278 = 1; f922 = 0; f378 = -inf; f379 = -inf; f433 = 1; f370 = 0; f371 = 1; f372 = 1; f373 = 1; f374 = 2; f375 = -inf; f376 = -inf; f377 = -inf; f887 = -inf; f508 = -inf; f722 = -inf; f432 = 1; f1043 = 1; f1044 = 0; f949 = -inf; f503 = 1; f948 = -inf; f502 = 0; f501 = 0; f431 = 2; f41 = 1; f40 = 0; f43 = 0; f42 = 0; f45 = -inf; f44 = 1; f47 = -inf; f46 = -inf; f49 = -inf; f48 = -inf; f208 = 1; f209 = 2; f506 = 0; f500 = -inf; f975 = -inf; f505 = -inf; f504 = 0; f430 = 1; f613 = 0; f217 = 2; f611 = 1; f610 = 0; f617 = -inf; f616 = -inf; f615 = -inf; f216 = 2; f1084 = -inf; f947 = -inf; f619 = -inf; f618 = -inf; f1080 = -inf; f54 = 0; f1082 = -inf; f742 = 0; f507 = 0; f758 = 1; f55 = -inf; f752 = -inf; f213 = -inf; f750 = -inf; f751 = -inf; f756 = 0; f757 = 0; f754 = -inf; f212 = -inf; f997 = 0; f211 = -inf; f210 = -inf; f855 = -inf; f854 = 2; f857 = -inf; f856 = -inf; f851 = 2; f850 = 0; f853 = 0; f852 = 1; f1013 = 1; f1012 = 0; f1011 = 0; f979 = -inf; f859 = -inf; f858 = -inf; f783 = -inf; f1014 = 0; f536 = 1; f537 = 0; f534 = 0; f535 = 0; f532 = 1; f533 = 2; f530 = -inf; f531 = 1; f925 = -inf; f924 = 0; f927 = 0; f926 = 0; f921 = 0; f920 = -inf; f538 = 0; f539 = 1; f219 = 1; f109 = -inf; f108 = -inf; f107 = -inf; f106 = -inf; f105 = -inf; f104 = 2; f103 = 1; f102 = 1; f101 = 2; f100 = 1; f724 = -inf; f673 = -inf; f672 = 0; f583 = -inf; f582 = 0; f581 = 0; f580 = -inf; f587 = -inf; f586 = -inf; f585 = -inf; f584 = 1; f589 = -inf; f588 = -inf; f248 = 2; f989 = 1; f249 = 0; f679 = -inf; f988 = 0; f678 = -inf; f402 = 0; f403 = -inf; f400 = -inf; f401 = 0; f406 = -inf; f407 = -inf; f404 = 1; f405 = -inf; f1069 = -inf; f323 = 2; f408 = -inf; f409 = -inf; f88 = 0; f982 = 0; f85 = 0; f241 = -inf; f87 = 0; f243 = -inf; f600 = -inf; f953 = 1; f81 = 1; f80 = -inf; f246 = 1; f82 = 1; f529 = -inf; f327 = 0; f326 = 2; f325 = 0; f324 = 1; f89 = 1; f322 = 0; f321 = 1; f320 = -inf; f240 = -inf; f84 = 0; f242 = -inf; f86 = 1; f244 = -inf; f245 = -inf; f329 = 1; f247 = 1; f487 = 1; f528 = -inf; f868 = 0; f869 = 2; f718 = 0; f719 = 1; f716 = 1; f622 = 0; f714 = 0; f715 = 0; f462 = 1; f713 = 1; f710 = -inf; f623 = 1; f759 = 0; f437 = -inf; f1059 = 2; f436 = -inf; f1057 = 0; f1056 = 1; f463 = 1; f1054 = -inf; f1053 = -inf; f435 = -inf; f1051 = -inf; f1050 = -inf; f819 = 2; f818 = 2; f18 = 0; f19 = 0; f12 = 0; f13 = -inf; f10 = -inf; f11 = -inf; f16 = -inf; f17 = 1; f14 = 0; f15 = 0; f143 = 1; f142 = 0; f141 = 0; f140 = -inf; f147 = 0; f146 = 0; f145 = -inf; f144 = 0; f464 = 2; f149 = 1; f148 = -inf; f781 = -inf; f780 = -inf; f668 = 1; f669 = 0; f785 = -inf; f784 = -inf; f787 = 0; f786 = 0; f662 = -inf; f663 = -inf; f660 = -inf; f661 = -inf; f666 = 0; f667 = 0; f664 = -inf; f665 = -inf; f465 = -inf; f1052 = -inf; f864 = 0; f717 = 1; f866 = 1; f1038 = -inf; f446 = 1; f447 = 1; f444 = 0; f445 = 0; f442 = 1; f443 = 2; f440 = -inf; f441 = 1; f712 = 0; f918 = -inf; f919 = -inf; f448 = 1; f449 = 2; f569 = 1; f568 = 0; f1034 = 1; f565 = 0; f564 = 0; f567 = 0; f566 = 1; f561 = 1; f560 = -inf; f563 = 2; f562 = 1; f547 = 0; f546 = 0; f1003 = -inf; f545 = -inf; f961 = -inf; f960 = -inf; f963 = -inf; f544 = -inf; f965 = -inf; f964 = -inf; f967 = 0; f966 = 0; f969 = 0; f687 = 0; f1032 = 1; f907 = 1; f906 = 1; f905 = -inf; f460 = 1; f904 = -inf; f288 = -inf; f289 = -inf; f461 = 2; f284 = 1; f285 = -inf; f286 = -inf; f287 = -inf; f280 = -inf; f281 = 0; f282 = 0; f283 = -inf; f820 = 2; f369 = 0; f368 = 2; f901 = -inf; f821 = 3; f363 = -inf; f362 = -inf; f361 = -inf; f360 = -inf; f367 = 1; f366 = 1; f365 = -inf; f364 = -inf; f823 = 2; f466 = -inf; f824 = 3; f467 = -inf; f825 = -inf; f549 = 0; f826 = -inf; f827 = -inf; f909 = 2; f56 = 0; f57 = 0; f215 = -inf; f214 = -inf; f52 = 0; f53 = 1; f50 = -inf; f51 = 0; f1058 = 1; f58 = -inf; f59 = 1; f878 = 2; f1055 = -inf; f745 = 1; f744 = 1; f747 = 1; f746 = 2; f741 = 0; f740 = -inf; f628 = 0; f520 = 0; f626 = 1; f627 = 1; f624 = 0; f625 = 0; f422 = -inf; f523 = -inf; f620 = -inf; f621 = 1; f522 = 0; f1004 = 1; f1005 = -inf; f1006 = -inf; f1007 = -inf; f1000 = -inf; f1001 = 0; f1002 = 0; f494 = 1; f423 = -inf; f526 = -inf; f1008 = -inf; f1009 = -inf; f23 = -inf; f22 = -inf; f21 = -inf; f20 = 1; f27 = 0; f26 = 0; f25 = -inf; f24 = 0; f828 = -inf; f829 = -inf; f29 = -inf; f28 = -inf; f952 = 0; f923 = 1; f521 = 1; f204 = 1; f488 = 2; f489 = 0; f525 = -inf; f524 = 0; f527 = -inf; f205 = 1; f482 = -inf; f483 = -inf; f480 = -inf; f481 = -inf; f486 = 1; f206 = 2; f484 = -inf; f485 = -inf; f811 = -inf; f138 = -inf; f139 = -inf; f956 = 0; f810 = -inf; f132 = 1; f133 = 1; f130 = 1; f131 = 2; f136 = -inf; f137 = -inf; f134 = 2; f135 = -inf; f812 = -inf; f548 = 1; f202 = 0; f861 = 1; f815 = -inf; f203 = 2; f814 = -inf; f817 = 1; f681 = 0; f816 = 1; f862 = 0; f554 = 1; f555 = -inf; f556 = -inf; f557 = -inf; f419 = 1; f418 = 0; f552 = 0; f553 = -inf; f415 = 0; f414 = 0; f417 = 0; f416 = 1; f411 = 1; f410 = -inf; f413 = 2; f412 = 1; f863 = 2; f959 = 1; f986 = 1; f999 = 0; f1060 = 1; f798 = -inf; f92 = -inf; f93 = -inf; f90 = -inf; f91 = -inf; f96 = 0; f97 = 0; f94 = -inf; f95 = -inf; f954 = 0; f330 = -inf; f98 = 1; f99 = 1; f238 = 1; f312 = 1; f313 = 0; f259 = -inf; f311 = 1; f316 = -inf; f317 = -inf; f314 = 2; f315 = -inf; f253 = 1; f252 = 1; f318 = -inf; f319 = -inf; f257 = -inf; f256 = -inf; f255 = -inf; f254 = 2; f782 = -inf; f896 = 2; f709 = -inf; f708 = -inf; f791 = 2; f879 = 1; f612 = 1; f701 = 1; f231 = 0; f703 = 0; f702 = 1; f705 = -inf; f704 = 1; f707 = -inf; f339 = 1; f789 = 1; f743 = 1; f788 = 1; f976 = -inf; f201 = 1; f876 = 1; f1049 = 1; f1040 = -inf; f1041 = 1; f1042 = 0; f614 = 1; f958 = -inf; f1045 = 0; f1046 = 1; f1047 = 1; f69 = 0; f68 = 2; f67 = 1; f66 = 1; f65 = -inf; f64 = -inf; f63 = -inf; f62 = -inf; f61 = -inf; f60 = -inf; f675 = -inf; f674 = 1; f677 = -inf; f676 = -inf; f671 = 0; f670 = -inf; f178 = 0; f179 = 2; f176 = 1; f177 = 1; f174 = 0; f175 = 0; f172 = 0; f173 = 2; f170 = -inf; f171 = 1; f778 = 0; f779 = 2; f774 = 1; f775 = 0; f776 = 2; f777 = 1; f770 = -inf; f771 = 0; f772 = 0; f773 = 1; f424 = -inf; f425 = -inf; f890 = -inf; f426 = 0; f427 = 0; f1039 = -inf; f865 = 0; f1035 = -inf; f420 = -inf; f1037 = -inf; f1036 = -inf; f1031 = 1; f1030 = 0; f1033 = 0; f421 = -inf; f451 = -inf; f450 = -inf; f453 = -inf; f452 = -inf; f455 = -inf; f350 = -inf; f457 = 2; f456 = 2; f459 = 1; f458 = 3; f351 = 0; f893 = 2; f885 = -inf; f908 = 2; f518 = 1; f519 = 0; f892 = 0; f753 = -inf; f510 = -inf; f511 = -inf; f512 = -inf; f513 = -inf; f514 = -inf; f515 = -inf; f516 = 0; f517 = 0; f688 = -inf; f689 = 0; f897 = 1; f680 = -inf; f428 = 1; f682 = 0; f683 = 1; f684 = 0; f685 = 0; f686 = 1; f429 = 1; f998 = 1; f358 = 1; f875 = -inf; f994 = -inf; f995 = -inf; f996 = 0; f359 = 2; f990 = -inf; f991 = -inf; f992 = -inf; f993 = -inf; f1028 = 1; f895 = 1; f356 = 2; f357 = 1; f354 = 1; f355 = 1; f352 = 0; f353 = 1; f299 = 2; f298 = 0; f297 = 1; f296 = 2; f295 = 0; f294 = 1; f293 = 1; f292 = 0; f291 = 0; f290 = -inf; f194 = 1; f195 = -inf; f196 = -inf; f197 = -inf; f190 = 0; f191 = 2; f192 = 0; f193 = 0; f218 = 3; f198 = -inf; f199 = -inf; f1019 = 0; f550 = -inf; f1072 = 0; f551 = 0; f914 = 3; f915 = -inf; f916 = -inf; f849 = 1; f910 = 2; f950 = -inf; f911 = 3; f222 = 1; f223 = 1; f220 = 1; f221 = 2; f226 = -inf; f227 = -inf; f224 = 2; f225 = -inf; f558 = -inf; f228 = -inf; f229 = -inf; f755 = -inf; f559 = -inf; f1018 = -inf; f706 = -inf; f946 = -inf; f951 = 0; f639 = 1; f638 = 2; f732 = 1; f733 = 0; f734 = 1; f735 = -inf; f736 = -inf; f737 = -inf; f631 = -inf; f630 = -inf; f633 = -inf; f632 = -inf; f635 = -inf; f634 = -inf; f637 = 1; f636 = 2; f1081 = -inf; f1066 = -inf; f1067 = -inf; f1071 = 0; f1070 = -inf; f1073 = 1; f1010 = -inf; f1075 = 1; f1074 = 1; f1077 = 1; f1076 = 2; f1079 = 2; f1017 = 0; f1016 = 1; f30 = -inf; f31 = 0; f32 = -inf; f33 = -inf; f34 = -inf; f35 = -inf; f36 = 1; f37 = 1; f38 = 2; f39 = 0; f839 = 1; f838 = -inf; f629 = 1; f125 = -inf; f124 = -inf; f127 = 2; f126 = 2; f121 = -inf; f120 = -inf; f123 = -inf; f122 = -inf; f943 = 0; f942 = 1; f941 = 2; f940 = 0; f129 = 1; f128 = 3; f945 = -inf; f944 = 2; f648 = -inf; f649 = -inf; f644 = 1; f645 = -inf; f646 = -inf; f647 = -inf; f640 = 0; f641 = 1; f642 = 1; f643 = 0; f867 = 1; f955 = -inf; f929 = 1; f809 = 2; f468 = -inf; f469 = -inf; f398 = 1; f399 = 0; f543 = -inf; f542 = -inf; f541 = -inf; f540 = -inf; f392 = -inf; f393 = -inf; f390 = -inf; f391 = -inf; f396 = 0; f397 = 0; f394 = -inf; f395 = -inf; f873 = -inf; f957 = 0; f495 = -inf; f207 = 1; f497 = -inf; f496 = -inf; f491 = 1; f490 = 0; f493 = 0; f492 = 0; f499 = -inf; f498 = -inf; f822 = 2; f200 = -inf; f266 = 2; f267 = 1; f264 = 1; f265 = 1; f262 = 2; f263 = 3; f260 = -inf; f261 = 2; f987 = 1; f268 = 1; f269 = 2; f328 = 0; f309 = 0; f308 = 2; f305 = -inf; f304 = -inf; f307 = 0; f306 = 1; f301 = -inf; f300 = -inf; f303 = -inf; f302 = -inf; f962 = -inf; f860 = -inf; f917 = -inf; f848 = 1; f83 = 2; f842 = -inf; f843 = -inf; f840 = -inf; f841 = -inf; f846 = 0; f847 = 0; f844 = -inf; f845 = -inf; f968 = 1; f1015 = 0; f1085 = -inf; f903 = -inf; f78 = -inf; f79 = -inf; f74 = 1; f75 = -inf; f76 = -inf; f77 = -inf; f70 = 0; f71 = 1; f72 = 0; f73 = 0; ---------- ./Problems/SMT/arctic/slice-4/arctic-017e4db2261082851a01497cad14ecd6.smt2 ; Sat ; 2.37600302696 ; 0.18701505661 ; None