(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES b# b c c -> b# b b b, b# b c c -> b# b b, b# b c c -> b# b, b# b c c -> b#, a a b b ->= b b c c a a, b b c c ->= c c b b b b, b b a a ->= a a c c b b) by arctic matrix interpretation with dimension 2|) (declare-fun f0 () Arctic) (declare-fun f1 () Arctic) (declare-fun f2 () Arctic) (declare-fun f3 () Arctic) (declare-fun f4 () Arctic) (declare-fun f5 () Arctic) (declare-fun f6 () Arctic) (declare-fun f7 () Arctic) (declare-fun f8 () Arctic) (declare-fun f9 () Arctic) (declare-fun f10 () Arctic) (declare-fun f11 () Arctic) (declare-fun f12 () Arctic) (declare-fun f13 () Arctic) (declare-fun f14 () Arctic) (declare-fun f15 () Arctic) (declare-fun f16 () Arctic) (declare-fun f17 () Arctic) (declare-fun f18 () Arctic) (declare-fun f19 () Arctic) (declare-fun f20 () Arctic) (declare-fun f21 () Arctic) (declare-fun f22 () Arctic) (declare-fun f23 () Arctic) (assert (and (or (finite f18) (finite f22)) (or (finite f6) (finite f10)) (or (finite f12) (finite f16)) (or (finite f0) (finite f4)))) (define-fun f24 () Arctic (+ (* f12 f12) (* f13 f14))) (define-fun f25 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f26 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f27 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f28 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f29 () Arctic (+ (* f14 f16) (* f15 f17))) (define-fun f30 () Arctic (+ f16 f28)) (define-fun f31 () Arctic (+ f17 f29)) (define-fun f32 () Arctic (+ (* f6 f24) (* f7 f26))) (define-fun f33 () Arctic (+ (* f6 f25) (* f7 f27))) (define-fun f34 () Arctic (+ (* f8 f24) (* f9 f26))) (define-fun f35 () Arctic (+ (* f8 f25) (* f9 f27))) (define-fun f36 () Arctic (+ (* f6 f30) (* f7 f31))) (define-fun f37 () Arctic (+ (* f8 f30) (* f9 f31))) (define-fun f38 () Arctic (+ f10 f36)) (define-fun f39 () Arctic (+ f11 f37)) (define-fun f40 () Arctic (+ (* f0 f32) (* f1 f34))) (define-fun f41 () Arctic (+ (* f0 f33) (* f1 f35))) (define-fun f42 () Arctic (+ (* f2 f32) (* f3 f34))) (define-fun f43 () Arctic (+ (* f2 f33) (* f3 f35))) (define-fun f44 () Arctic (+ (* f0 f38) (* f1 f39))) (define-fun f45 () Arctic (+ (* f2 f38) (* f3 f39))) (define-fun f46 () Arctic (+ f4 f44)) (define-fun f47 () Arctic (+ f5 f45)) (define-fun f48 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f49 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f50 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f51 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f52 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f53 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f54 () Arctic (+ f10 f52)) (define-fun f55 () Arctic (+ f11 f53)) (define-fun f56 () Arctic (+ (* f6 f48) (* f7 f50))) (define-fun f57 () Arctic (+ (* f6 f49) (* f7 f51))) (define-fun f58 () Arctic (+ (* f8 f48) (* f9 f50))) (define-fun f59 () Arctic (+ (* f8 f49) (* f9 f51))) (define-fun f60 () Arctic (+ (* f6 f54) (* f7 f55))) (define-fun f61 () Arctic (+ (* f8 f54) (* f9 f55))) (define-fun f62 () Arctic (+ f10 f60)) (define-fun f63 () Arctic (+ f11 f61)) (define-fun f64 () Arctic (+ (* f0 f56) (* f1 f58))) (define-fun f65 () Arctic (+ (* f0 f57) (* f1 f59))) (define-fun f66 () Arctic (+ (* f2 f56) (* f3 f58))) (define-fun f67 () Arctic (+ (* f2 f57) (* f3 f59))) (define-fun f68 () Arctic (+ (* f0 f62) (* f1 f63))) (define-fun f69 () Arctic (+ (* f2 f62) (* f3 f63))) (define-fun f70 () Arctic (+ f4 f68)) (define-fun f71 () Arctic (+ f5 f69)) (define-fun f72 () Arctic (+ (* f12 f12) (* f13 f14))) (define-fun f73 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f74 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f75 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f76 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f77 () Arctic (+ (* f14 f16) (* f15 f17))) (define-fun f78 () Arctic (+ f16 f76)) (define-fun f79 () Arctic (+ f17 f77)) (define-fun f80 () Arctic (+ (* f6 f72) (* f7 f74))) (define-fun f81 () Arctic (+ (* f6 f73) (* f7 f75))) (define-fun f82 () Arctic (+ (* f8 f72) (* f9 f74))) (define-fun f83 () Arctic (+ (* f8 f73) (* f9 f75))) (define-fun f84 () Arctic (+ (* f6 f78) (* f7 f79))) (define-fun f85 () Arctic (+ (* f8 f78) (* f9 f79))) (define-fun f86 () Arctic (+ f10 f84)) (define-fun f87 () Arctic (+ f11 f85)) (define-fun f88 () Arctic (+ (* f0 f80) (* f1 f82))) (define-fun f89 () Arctic (+ (* f0 f81) (* f1 f83))) (define-fun f90 () Arctic (+ (* f2 f80) (* f3 f82))) (define-fun f91 () Arctic (+ (* f2 f81) (* f3 f83))) (define-fun f92 () Arctic (+ (* f0 f86) (* f1 f87))) (define-fun f93 () Arctic (+ (* f2 f86) (* f3 f87))) (define-fun f94 () Arctic (+ f4 f92)) (define-fun f95 () Arctic (+ f5 f93)) (define-fun f96 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f97 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f98 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f99 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f100 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f101 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f102 () Arctic (+ f10 f100)) (define-fun f103 () Arctic (+ f11 f101)) (define-fun f104 () Arctic (+ (* f0 f96) (* f1 f98))) (define-fun f105 () Arctic (+ (* f0 f97) (* f1 f99))) (define-fun f106 () Arctic (+ (* f2 f96) (* f3 f98))) (define-fun f107 () Arctic (+ (* f2 f97) (* f3 f99))) (define-fun f108 () Arctic (+ (* f0 f102) (* f1 f103))) (define-fun f109 () Arctic (+ (* f2 f102) (* f3 f103))) (define-fun f110 () Arctic (+ f4 f108)) (define-fun f111 () Arctic (+ f5 f109)) (define-fun f112 () Arctic (+ (* f12 f12) (* f13 f14))) (define-fun f113 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f114 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f115 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f116 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f117 () Arctic (+ (* f14 f16) (* f15 f17))) (define-fun f118 () Arctic (+ f16 f116)) (define-fun f119 () Arctic (+ f17 f117)) (define-fun f120 () Arctic (+ (* f6 f112) (* f7 f114))) (define-fun f121 () Arctic (+ (* f6 f113) (* f7 f115))) (define-fun f122 () Arctic (+ (* f8 f112) (* f9 f114))) (define-fun f123 () Arctic (+ (* f8 f113) (* f9 f115))) (define-fun f124 () Arctic (+ (* f6 f118) (* f7 f119))) (define-fun f125 () Arctic (+ (* f8 f118) (* f9 f119))) (define-fun f126 () Arctic (+ f10 f124)) (define-fun f127 () Arctic (+ f11 f125)) (define-fun f128 () Arctic (+ (* f0 f120) (* f1 f122))) (define-fun f129 () Arctic (+ (* f0 f121) (* f1 f123))) (define-fun f130 () Arctic (+ (* f2 f120) (* f3 f122))) (define-fun f131 () Arctic (+ (* f2 f121) (* f3 f123))) (define-fun f132 () Arctic (+ (* f0 f126) (* f1 f127))) (define-fun f133 () Arctic (+ (* f2 f126) (* f3 f127))) (define-fun f134 () Arctic (+ f4 f132)) (define-fun f135 () Arctic (+ f5 f133)) (define-fun f136 () Arctic (+ (* f0 f6) (* f1 f8))) (define-fun f137 () Arctic (+ (* f0 f7) (* f1 f9))) (define-fun f138 () Arctic (+ (* f2 f6) (* f3 f8))) (define-fun f139 () Arctic (+ (* f2 f7) (* f3 f9))) (define-fun f140 () Arctic (+ (* f0 f10) (* f1 f11))) (define-fun f141 () Arctic (+ (* f2 f10) (* f3 f11))) (define-fun f142 () Arctic (+ f4 f140)) (define-fun f143 () Arctic (+ f5 f141)) (define-fun f144 () Arctic (+ (* f12 f12) (* f13 f14))) (define-fun f145 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f146 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f147 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f148 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f149 () Arctic (+ (* f14 f16) (* f15 f17))) (define-fun f150 () Arctic (+ f16 f148)) (define-fun f151 () Arctic (+ f17 f149)) (define-fun f152 () Arctic (+ (* f6 f144) (* f7 f146))) (define-fun f153 () Arctic (+ (* f6 f145) (* f7 f147))) (define-fun f154 () Arctic (+ (* f8 f144) (* f9 f146))) (define-fun f155 () Arctic (+ (* f8 f145) (* f9 f147))) (define-fun f156 () Arctic (+ (* f6 f150) (* f7 f151))) (define-fun f157 () Arctic (+ (* f8 f150) (* f9 f151))) (define-fun f158 () Arctic (+ f10 f156)) (define-fun f159 () Arctic (+ f11 f157)) (define-fun f160 () Arctic (+ (* f0 f152) (* f1 f154))) (define-fun f161 () Arctic (+ (* f0 f153) (* f1 f155))) (define-fun f162 () Arctic (+ (* f2 f152) (* f3 f154))) (define-fun f163 () Arctic (+ (* f2 f153) (* f3 f155))) (define-fun f164 () Arctic (+ (* f0 f158) (* f1 f159))) (define-fun f165 () Arctic (+ (* f2 f158) (* f3 f159))) (define-fun f166 () Arctic (+ f4 f164)) (define-fun f167 () Arctic (+ f5 f165)) (define-fun f168 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f169 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f170 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f171 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f172 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f173 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f174 () Arctic (+ f10 f172)) (define-fun f175 () Arctic (+ f11 f173)) (define-fun f176 () Arctic (+ (* f18 f168) (* f19 f170))) (define-fun f177 () Arctic (+ (* f18 f169) (* f19 f171))) (define-fun f178 () Arctic (+ (* f20 f168) (* f21 f170))) (define-fun f179 () Arctic (+ (* f20 f169) (* f21 f171))) (define-fun f180 () Arctic (+ (* f18 f174) (* f19 f175))) (define-fun f181 () Arctic (+ (* f20 f174) (* f21 f175))) (define-fun f182 () Arctic (+ f22 f180)) (define-fun f183 () Arctic (+ f23 f181)) (define-fun f184 () Arctic (+ (* f18 f176) (* f19 f178))) (define-fun f185 () Arctic (+ (* f18 f177) (* f19 f179))) (define-fun f186 () Arctic (+ (* f20 f176) (* f21 f178))) (define-fun f187 () Arctic (+ (* f20 f177) (* f21 f179))) (define-fun f188 () Arctic (+ (* f18 f182) (* f19 f183))) (define-fun f189 () Arctic (+ (* f20 f182) (* f21 f183))) (define-fun f190 () Arctic (+ f22 f188)) (define-fun f191 () Arctic (+ f23 f189)) (define-fun f192 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f193 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f194 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f195 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f196 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f197 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f198 () Arctic (+ f22 f196)) (define-fun f199 () Arctic (+ f23 f197)) (define-fun f200 () Arctic (+ (* f12 f192) (* f13 f194))) (define-fun f201 () Arctic (+ (* f12 f193) (* f13 f195))) (define-fun f202 () Arctic (+ (* f14 f192) (* f15 f194))) (define-fun f203 () Arctic (+ (* f14 f193) (* f15 f195))) (define-fun f204 () Arctic (+ (* f12 f198) (* f13 f199))) (define-fun f205 () Arctic (+ (* f14 f198) (* f15 f199))) (define-fun f206 () Arctic (+ f16 f204)) (define-fun f207 () Arctic (+ f17 f205)) (define-fun f208 () Arctic (+ (* f12 f200) (* f13 f202))) (define-fun f209 () Arctic (+ (* f12 f201) (* f13 f203))) (define-fun f210 () Arctic (+ (* f14 f200) (* f15 f202))) (define-fun f211 () Arctic (+ (* f14 f201) (* f15 f203))) (define-fun f212 () Arctic (+ (* f12 f206) (* f13 f207))) (define-fun f213 () Arctic (+ (* f14 f206) (* f15 f207))) (define-fun f214 () Arctic (+ f16 f212)) (define-fun f215 () Arctic (+ f17 f213)) (define-fun f216 () Arctic (+ (* f6 f208) (* f7 f210))) (define-fun f217 () Arctic (+ (* f6 f209) (* f7 f211))) (define-fun f218 () Arctic (+ (* f8 f208) (* f9 f210))) (define-fun f219 () Arctic (+ (* f8 f209) (* f9 f211))) (define-fun f220 () Arctic (+ (* f6 f214) (* f7 f215))) (define-fun f221 () Arctic (+ (* f8 f214) (* f9 f215))) (define-fun f222 () Arctic (+ f10 f220)) (define-fun f223 () Arctic (+ f11 f221)) (define-fun f224 () Arctic (+ (* f6 f216) (* f7 f218))) (define-fun f225 () Arctic (+ (* f6 f217) (* f7 f219))) (define-fun f226 () Arctic (+ (* f8 f216) (* f9 f218))) (define-fun f227 () Arctic (+ (* f8 f217) (* f9 f219))) (define-fun f228 () Arctic (+ (* f6 f222) (* f7 f223))) (define-fun f229 () Arctic (+ (* f8 f222) (* f9 f223))) (define-fun f230 () Arctic (+ f10 f228)) (define-fun f231 () Arctic (+ f11 f229)) (define-fun f232 () Arctic (+ (* f12 f12) (* f13 f14))) (define-fun f233 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f234 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f235 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f236 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f237 () Arctic (+ (* f14 f16) (* f15 f17))) (define-fun f238 () Arctic (+ f16 f236)) (define-fun f239 () Arctic (+ f17 f237)) (define-fun f240 () Arctic (+ (* f6 f232) (* f7 f234))) (define-fun f241 () Arctic (+ (* f6 f233) (* f7 f235))) (define-fun f242 () Arctic (+ (* f8 f232) (* f9 f234))) (define-fun f243 () Arctic (+ (* f8 f233) (* f9 f235))) (define-fun f244 () Arctic (+ (* f6 f238) (* f7 f239))) (define-fun f245 () Arctic (+ (* f8 f238) (* f9 f239))) (define-fun f246 () Arctic (+ f10 f244)) (define-fun f247 () Arctic (+ f11 f245)) (define-fun f248 () Arctic (+ (* f6 f240) (* f7 f242))) (define-fun f249 () Arctic (+ (* f6 f241) (* f7 f243))) (define-fun f250 () Arctic (+ (* f8 f240) (* f9 f242))) (define-fun f251 () Arctic (+ (* f8 f241) (* f9 f243))) (define-fun f252 () Arctic (+ (* f6 f246) (* f7 f247))) (define-fun f253 () Arctic (+ (* f8 f246) (* f9 f247))) (define-fun f254 () Arctic (+ f10 f252)) (define-fun f255 () Arctic (+ f11 f253)) (define-fun f256 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f257 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f258 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f259 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f260 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f261 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f262 () Arctic (+ f10 f260)) (define-fun f263 () Arctic (+ f11 f261)) (define-fun f264 () Arctic (+ (* f6 f256) (* f7 f258))) (define-fun f265 () Arctic (+ (* f6 f257) (* f7 f259))) (define-fun f266 () Arctic (+ (* f8 f256) (* f9 f258))) (define-fun f267 () Arctic (+ (* f8 f257) (* f9 f259))) (define-fun f268 () Arctic (+ (* f6 f262) (* f7 f263))) (define-fun f269 () Arctic (+ (* f8 f262) (* f9 f263))) (define-fun f270 () Arctic (+ f10 f268)) (define-fun f271 () Arctic (+ f11 f269)) (define-fun f272 () Arctic (+ (* f6 f264) (* f7 f266))) (define-fun f273 () Arctic (+ (* f6 f265) (* f7 f267))) (define-fun f274 () Arctic (+ (* f8 f264) (* f9 f266))) (define-fun f275 () Arctic (+ (* f8 f265) (* f9 f267))) (define-fun f276 () Arctic (+ (* f6 f270) (* f7 f271))) (define-fun f277 () Arctic (+ (* f8 f270) (* f9 f271))) (define-fun f278 () Arctic (+ f10 f276)) (define-fun f279 () Arctic (+ f11 f277)) (define-fun f280 () Arctic (+ (* f12 f272) (* f13 f274))) (define-fun f281 () Arctic (+ (* f12 f273) (* f13 f275))) (define-fun f282 () Arctic (+ (* f14 f272) (* f15 f274))) (define-fun f283 () Arctic (+ (* f14 f273) (* f15 f275))) (define-fun f284 () Arctic (+ (* f12 f278) (* f13 f279))) (define-fun f285 () Arctic (+ (* f14 f278) (* f15 f279))) (define-fun f286 () Arctic (+ f16 f284)) (define-fun f287 () Arctic (+ f17 f285)) (define-fun f288 () Arctic (+ (* f12 f280) (* f13 f282))) (define-fun f289 () Arctic (+ (* f12 f281) (* f13 f283))) (define-fun f290 () Arctic (+ (* f14 f280) (* f15 f282))) (define-fun f291 () Arctic (+ (* f14 f281) (* f15 f283))) (define-fun f292 () Arctic (+ (* f12 f286) (* f13 f287))) (define-fun f293 () Arctic (+ (* f14 f286) (* f15 f287))) (define-fun f294 () Arctic (+ f16 f292)) (define-fun f295 () Arctic (+ f17 f293)) (define-fun f296 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f297 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f298 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f299 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f300 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f301 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f302 () Arctic (+ f22 f300)) (define-fun f303 () Arctic (+ f23 f301)) (define-fun f304 () Arctic (+ (* f6 f296) (* f7 f298))) (define-fun f305 () Arctic (+ (* f6 f297) (* f7 f299))) (define-fun f306 () Arctic (+ (* f8 f296) (* f9 f298))) (define-fun f307 () Arctic (+ (* f8 f297) (* f9 f299))) (define-fun f308 () Arctic (+ (* f6 f302) (* f7 f303))) (define-fun f309 () Arctic (+ (* f8 f302) (* f9 f303))) (define-fun f310 () Arctic (+ f10 f308)) (define-fun f311 () Arctic (+ f11 f309)) (define-fun f312 () Arctic (+ (* f6 f304) (* f7 f306))) (define-fun f313 () Arctic (+ (* f6 f305) (* f7 f307))) (define-fun f314 () Arctic (+ (* f8 f304) (* f9 f306))) (define-fun f315 () Arctic (+ (* f8 f305) (* f9 f307))) (define-fun f316 () Arctic (+ (* f6 f310) (* f7 f311))) (define-fun f317 () Arctic (+ (* f8 f310) (* f9 f311))) (define-fun f318 () Arctic (+ f10 f316)) (define-fun f319 () Arctic (+ f11 f317)) (define-fun f320 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f321 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f322 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f323 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f324 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f325 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f326 () Arctic (+ f10 f324)) (define-fun f327 () Arctic (+ f11 f325)) (define-fun f328 () Arctic (+ (* f12 f320) (* f13 f322))) (define-fun f329 () Arctic (+ (* f12 f321) (* f13 f323))) (define-fun f330 () Arctic (+ (* f14 f320) (* f15 f322))) (define-fun f331 () Arctic (+ (* f14 f321) (* f15 f323))) (define-fun f332 () Arctic (+ (* f12 f326) (* f13 f327))) (define-fun f333 () Arctic (+ (* f14 f326) (* f15 f327))) (define-fun f334 () Arctic (+ f16 f332)) (define-fun f335 () Arctic (+ f17 f333)) (define-fun f336 () Arctic (+ (* f12 f328) (* f13 f330))) (define-fun f337 () Arctic (+ (* f12 f329) (* f13 f331))) (define-fun f338 () Arctic (+ (* f14 f328) (* f15 f330))) (define-fun f339 () Arctic (+ (* f14 f329) (* f15 f331))) (define-fun f340 () Arctic (+ (* f12 f334) (* f13 f335))) (define-fun f341 () Arctic (+ (* f14 f334) (* f15 f335))) (define-fun f342 () Arctic (+ f16 f340)) (define-fun f343 () Arctic (+ f17 f341)) (define-fun f344 () Arctic (+ (* f18 f336) (* f19 f338))) (define-fun f345 () Arctic (+ (* f18 f337) (* f19 f339))) (define-fun f346 () Arctic (+ (* f20 f336) (* f21 f338))) (define-fun f347 () Arctic (+ (* f20 f337) (* f21 f339))) (define-fun f348 () Arctic (+ (* f18 f342) (* f19 f343))) (define-fun f349 () Arctic (+ (* f20 f342) (* f21 f343))) (define-fun f350 () Arctic (+ f22 f348)) (define-fun f351 () Arctic (+ f23 f349)) (define-fun f352 () Arctic (+ (* f18 f344) (* f19 f346))) (define-fun f353 () Arctic (+ (* f18 f345) (* f19 f347))) (define-fun f354 () Arctic (+ (* f20 f344) (* f21 f346))) (define-fun f355 () Arctic (+ (* f20 f345) (* f21 f347))) (define-fun f356 () Arctic (+ (* f18 f350) (* f19 f351))) (define-fun f357 () Arctic (+ (* f20 f350) (* f21 f351))) (define-fun f358 () Arctic (+ f22 f356)) (define-fun f359 () Arctic (+ f23 f357)) (assert (and (and (and (and (>= f40 f64) (>= f41 f65)) (and (>= f42 f66) (>= f43 f67))) (and (and (>= f46 f70)) (and (>= f47 f71)))) (and (and (and (>= f88 f104) (>= f89 f105)) (and (>= f90 f106) (>= f91 f107))) (and (and (>= f94 f110)) (and (>= f95 f111)))) (and (and (and (>= f128 f136) (>= f129 f137)) (and (>= f130 f138) (>= f131 f139))) (and (and (>= f134 f142)) (and (>= f135 f143)))) (and (and (and (>= f160 f0) (>= f161 f1)) (and (>= f162 f2) (>= f163 f3))) (and (and (>= f166 f4)) (and (>= f167 f5)))) (and (and (and (>= f184 f224) (>= f185 f225)) (and (>= f186 f226) (>= f187 f227))) (and (and (>= f190 f230)) (and (>= f191 f231)))) (and (and (and (>= f248 f288) (>= f249 f289)) (and (>= f250 f290) (>= f251 f291))) (and (and (>= f254 f294)) (and (>= f255 f295)))) (and (and (and (>= f312 f352) (>= f313 f353)) (and (>= f314 f354) (>= f315 f355))) (and (and (>= f318 f358)) (and (>= f319 f359)))))) (assert (or (and (and (and (>> f40 f64) (>> f41 f65)) (and (>> f42 f66) (>> f43 f67))) (and (and (>> f46 f70)) (and (>> f47 f71)))) (and (and (and (>> f88 f104) (>> f89 f105)) (and (>> f90 f106) (>> f91 f107))) (and (and (>> f94 f110)) (and (>> f95 f111)))) (and (and (and (>> f128 f136) (>> f129 f137)) (and (>> f130 f138) (>> f131 f139))) (and (and (>> f134 f142)) (and (>> f135 f143)))) (and (and (and (>> f160 f0) (>> f161 f1)) (and (>> f162 f2) (>> f163 f3))) (and (and (>> f166 f4)) (and (>> f167 f5)))))) (check-sat) (get-value (f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 f41 f42 f43 f44 f45 f46 f47 f48 f49 f50 f51 f52 f53 f54 f55 f56 f57 f58 f59 f60 f61 f62 f63 f64 f65 f66 f67 f68 f69 f70 f71 f72 f73 f74 f75 f76 f77 f78 f79 f80 f81 f82 f83 f84 f85 f86 f87 f88 f89 f90 f91 f92 f93 f94 f95 f96 f97 f98 f99 f100 f101 f102 f103 f104 f105 f106 f107 f108 f109 f110 f111 f112 f113 f114 f115 f116 f117 f118 f119 f120 f121 f122 f123 f124 f125 f126 f127 f128 f129 f130 f131 f132 f133 f134 f135 f136 f137 f138 f139 f140 f141 f142 f143 f144 f145 f146 f147 f148 f149 f150 f151 f152 f153 f154 f155 f156 f157 f158 f159 f160 f161 f162 f163 f164 f165 f166 f167 f168 f169 f170 f171 f172 f173 f174 f175 f176 f177 f178 f179 f180 f181 f182 f183 f184 f185 f186 f187 f188 f189 f190 f191 f192 f193 f194 f195 f196 f197 f198 f199 f200 f201 f202 f203 f204 f205 f206 f207 f208 f209 f210 f211 f212 f213 f214 f215 f216 f217 f218 f219 f220 f221 f222 f223 f224 f225 f226 f227 f228 f229 f230 f231 f232 f233 f234 f235 f236 f237 f238 f239 f240 f241 f242 f243 f244 f245 f246 f247 f248 f249 f250 f251 f252 f253 f254 f255 f256 f257 f258 f259 f260 f261 f262 f263 f264 f265 f266 f267 f268 f269 f270 f271 f272 f273 f274 f275 f276 f277 f278 f279 f280 f281 f282 f283 f284 f285 f286 f287 f288 f289 f290 f291 f292 f293 f294 f295 f296 f297 f298 f299 f300 f301 f302 f303 f304 f305 f306 f307 f308 f309 f310 f311 f312 f313 f314 f315 f316 f317 f318 f319 f320 f321 f322 f323 f324 f325 f326 f327 f328 f329 f330 f331 f332 f333 f334 f335 f336 f337 f338 f339 f340 f341 f342 f343 f344 f345 f346 f347 f348 f349 f350 f351 f352 f353 f354 f355 f356 f357 f358 f359))