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