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