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