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