f169 = -inf; f168 = -inf; f161 = 1; f160 = 1; f163 = 1; f162 = 1; f165 = -inf; f164 = 1; f167 = -inf; f166 = -inf; f297 = 1; f288 = -inf; f289 = -inf; f145 = 1; f296 = 0; f284 = 0; f285 = -inf; f286 = -inf; f214 = -inf; f280 = 1; f281 = -inf; f282 = 0; f283 = 1; f41 = -inf; f40 = 0; f43 = 1; f42 = 0; f45 = -inf; f44 = 0; f47 = -inf; f46 = -inf; f49 = -inf; f48 = -inf; f208 = 1; f209 = -inf; f259 = -inf; f215 = -inf; f144 = 0; f291 = 1; f278 = 1; f290 = -inf; f194 = 0; f195 = -inf; f196 = -inf; f240 = -inf; f197 = -inf; f118 = -inf; f119 = -inf; f299 = 1; f298 = 2; f114 = -inf; f115 = -inf; f116 = -inf; f117 = -inf; f110 = -inf; f111 = 0; f112 = 1; f113 = -inf; f56 = 0; f57 = 0; f54 = 0; f55 = 1; f52 = 1; f53 = 1; f50 = -inf; f51 = 1; f193 = 1; f198 = -inf; f199 = -inf; f58 = 1; f59 = 1; f142 = 1; f220 = 0; f295 = 1; f300 = -inf; f272 = -inf; f256 = -inf; f219 = -inf; f109 = -inf; f108 = -inf; f107 = -inf; f106 = -inf; f105 = -inf; f104 = 0; f103 = 1; f102 = 0; f101 = -inf; f100 = 0; f187 = 1; f186 = 0; f185 = -inf; f184 = -inf; f183 = -inf; f182 = -inf; f181 = -inf; f180 = -inf; f217 = 1; f228 = -inf; f229 = -inf; f189 = -inf; f188 = -inf; f23 = -inf; f22 = -inf; f21 = -inf; f20 = -inf; f27 = -inf; f26 = -inf; f25 = 1; f24 = 0; f29 = -inf; f28 = 0; f293 = 1; f204 = 0; f205 = 1; f206 = 0; f138 = -inf; f139 = -inf; f132 = 0; f133 = 1; f130 = 0; f131 = -inf; f136 = -inf; f137 = -inf; f134 = 0; f135 = -inf; f239 = -inf; f202 = 1; f235 = 1; f234 = 0; f237 = 0; f203 = -inf; f231 = 0; f230 = -inf; f233 = -inf; f216 = 0; f30 = 0; f31 = 1; f32 = 0; f33 = -inf; f34 = -inf; f35 = -inf; f36 = 0; f37 = 1; f38 = 1; f39 = 0; f242 = -inf; f125 = -inf; f124 = -inf; f127 = 1; f126 = 0; f121 = -inf; f120 = -inf; f123 = -inf; f122 = -inf; f244 = -inf; f292 = 2; f129 = 0; f128 = 1; f245 = -inf; f287 = -inf; f140 = -inf; f246 = 1; f236 = 0; f147 = 0; f247 = 2; f146 = 0; f248 = 1; f213 = -inf; f218 = -inf; f89 = 0; f88 = 1; f85 = 0; f84 = -inf; f87 = 0; f86 = -inf; f81 = 0; f80 = -inf; f83 = -inf; f82 = 1; f190 = 0; f212 = -inf; f150 = -inf; f151 = -inf; f152 = -inf; f153 = -inf; f154 = -inf; f155 = -inf; f156 = 1; f157 = 2; f158 = 1; f159 = 0; f191 = -inf; f92 = -inf; f93 = -inf; f90 = -inf; f91 = -inf; f96 = 0; f97 = 1; f94 = -inf; f95 = -inf; f98 = -inf; f99 = -inf; f211 = -inf; f238 = 1; f143 = 1; f258 = -inf; f253 = 2; f252 = 1; f251 = 0; f250 = 1; f257 = -inf; f192 = 0; f255 = -inf; f254 = 1; f207 = 0; f18 = 0; f19 = 0; f12 = 0; f13 = 1; f10 = -inf; f11 = -inf; f16 = -inf; f17 = 0; f14 = -inf; f15 = -inf; f0 = 0; f1 = 1; f2 = -inf; f3 = -inf; f4 = -inf; f5 = -inf; f6 = -inf; f7 = -inf; f8 = -inf; f9 = -inf; f149 = 1; f148 = 1; f200 = -inf; f266 = 0; f267 = 0; f264 = 0; f265 = 1; f262 = 1; f263 = -inf; f260 = -inf; f261 = 0; f294 = 0; f232 = 1; f141 = 1; f269 = -inf; f305 = -inf; f304 = -inf; f301 = -inf; f201 = 0; f303 = -inf; f302 = -inf; f223 = 1; f268 = 1; f69 = -inf; f68 = 1; f67 = 2; f66 = 1; f65 = -inf; f64 = -inf; f63 = -inf; f62 = -inf; f61 = -inf; f60 = -inf; f222 = 0; f178 = 1; f179 = 0; f176 = -inf; f177 = 0; f174 = -inf; f175 = 0; f172 = 1; f173 = -inf; f170 = -inf; f171 = 0; f271 = -inf; f270 = -inf; f273 = -inf; f221 = -inf; f275 = -inf; f274 = -inf; f277 = 2; f276 = 1; f279 = 0; f226 = -inf; f241 = -inf; f210 = -inf; f227 = -inf; f224 = 0; f243 = -inf; f225 = -inf; f249 = 0; f78 = -inf; f79 = -inf; f74 = -inf; f75 = -inf; f76 = -inf; f77 = -inf; f70 = -inf; f71 = -inf; f72 = -inf; f73 = -inf; ---------- ./Problems/SMT/arctic/slice-2/arctic-7d7a62550bc344d4bd9030357a2ee218.smt2 ; Sat ; 0.526477098465 ; 0.160094022751 ; None