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