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