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