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