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