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