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