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