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