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