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