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