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