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