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