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