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