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