(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES a# a -> b# b b, a# -> d# c, b# b -> c# c c, c# c -> d# d d, d# d c -> a#, a a ->= b b b, a ->= d c, b b ->= c c c, c c ->= d d d, d e ->= e d c b a, b ->= d d, c e ->= e a a b, d d c ->= a) by arctic matrix interpretation with dimension 3|) (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) (declare-fun f24 () Arctic) (declare-fun f25 () Arctic) (declare-fun f26 () Arctic) (declare-fun f27 () Arctic) (declare-fun f28 () Arctic) (declare-fun f29 () Arctic) (declare-fun f30 () Arctic) (declare-fun f31 () Arctic) (declare-fun f32 () Arctic) (declare-fun f33 () Arctic) (declare-fun f34 () Arctic) (declare-fun f35 () Arctic) (declare-fun f36 () Arctic) (declare-fun f37 () Arctic) (declare-fun f38 () Arctic) (declare-fun f39 () Arctic) (declare-fun f40 () Arctic) (declare-fun f41 () Arctic) (declare-fun f42 () Arctic) (declare-fun f43 () Arctic) (declare-fun f44 () Arctic) (declare-fun f45 () Arctic) (declare-fun f46 () Arctic) (declare-fun f47 () Arctic) (declare-fun f48 () Arctic) (declare-fun f49 () Arctic) (declare-fun f50 () Arctic) (declare-fun f51 () Arctic) (declare-fun f52 () Arctic) (declare-fun f53 () Arctic) (declare-fun f54 () Arctic) (declare-fun f55 () Arctic) (declare-fun f56 () Arctic) (declare-fun f57 () Arctic) (declare-fun f58 () Arctic) (declare-fun f59 () Arctic) (declare-fun f60 () Arctic) (declare-fun f61 () Arctic) (declare-fun f62 () Arctic) (declare-fun f63 () Arctic) (declare-fun f64 () Arctic) (declare-fun f65 () Arctic) (declare-fun f66 () Arctic) (declare-fun f67 () Arctic) (declare-fun f68 () Arctic) (declare-fun f69 () Arctic) (declare-fun f70 () Arctic) (declare-fun f71 () Arctic) (declare-fun f72 () Arctic) (declare-fun f73 () Arctic) (declare-fun f74 () Arctic) (declare-fun f75 () Arctic) (declare-fun f76 () Arctic) (declare-fun f77 () Arctic) (declare-fun f78 () Arctic) (declare-fun f79 () Arctic) (declare-fun f80 () Arctic) (declare-fun f81 () Arctic) (declare-fun f82 () Arctic) (declare-fun f83 () Arctic) (declare-fun f84 () Arctic) (declare-fun f85 () Arctic) (declare-fun f86 () Arctic) (declare-fun f87 () Arctic) (declare-fun f88 () Arctic) (declare-fun f89 () Arctic) (declare-fun f90 () Arctic) (declare-fun f91 () Arctic) (declare-fun f92 () Arctic) (declare-fun f93 () Arctic) (declare-fun f94 () Arctic) (declare-fun f95 () Arctic) (declare-fun f96 () Arctic) (declare-fun f97 () Arctic) (declare-fun f98 () Arctic) (declare-fun f99 () Arctic) (declare-fun f100 () Arctic) (declare-fun f101 () Arctic) (declare-fun f102 () Arctic) (declare-fun f103 () Arctic) (declare-fun f104 () Arctic) (declare-fun f105 () Arctic) (declare-fun f106 () Arctic) (declare-fun f107 () Arctic) (assert (and (or (finite f12) (finite f21)) (or (finite f36) (finite f45)) (or (finite f60) (finite f69)) (or (finite f84) (finite f93)) (or (finite f96) (finite f105)) (or (finite f0) (finite f9)) (or (finite f24) (finite f33)) (or (finite f72) (finite f81)) (or (finite f48) (finite f57)))) (define-fun f108 () Arctic (+ (* f0 f12) (* f1 f15) (* f2 f18))) (define-fun f109 () Arctic (+ (* f0 f13) (* f1 f16) (* f2 f19))) (define-fun f110 () Arctic (+ (* f0 f14) (* f1 f17) (* f2 f20))) (define-fun f111 () Arctic (+ (* f3 f12) (* f4 f15) (* f5 f18))) (define-fun f112 () Arctic (+ (* f3 f13) (* f4 f16) (* f5 f19))) (define-fun f113 () Arctic (+ (* f3 f14) (* f4 f17) (* f5 f20))) (define-fun f114 () Arctic (+ (* f6 f12) (* f7 f15) (* f8 f18))) (define-fun f115 () Arctic (+ (* f6 f13) (* f7 f16) (* f8 f19))) (define-fun f116 () Arctic (+ (* f6 f14) (* f7 f17) (* f8 f20))) (define-fun f117 () Arctic (+ (* f0 f21) (* f1 f22) (* f2 f23))) (define-fun f118 () Arctic (+ (* f3 f21) (* f4 f22) (* f5 f23))) (define-fun f119 () Arctic (+ (* f6 f21) (* f7 f22) (* f8 f23))) (define-fun f120 () Arctic (+ f9 f117)) (define-fun f121 () Arctic (+ f10 f118)) (define-fun f122 () Arctic (+ f11 f119)) (define-fun f123 () Arctic (+ (* f36 f36) (* f37 f39) (* f38 f42))) (define-fun f124 () Arctic (+ (* f36 f37) (* f37 f40) (* f38 f43))) (define-fun f125 () Arctic (+ (* f36 f38) (* f37 f41) (* f38 f44))) (define-fun f126 () Arctic (+ (* f39 f36) (* f40 f39) (* f41 f42))) (define-fun f127 () Arctic (+ (* f39 f37) (* f40 f40) (* f41 f43))) (define-fun f128 () Arctic (+ (* f39 f38) (* f40 f41) (* f41 f44))) (define-fun f129 () Arctic (+ (* f42 f36) (* f43 f39) (* f44 f42))) (define-fun f130 () Arctic (+ (* f42 f37) (* f43 f40) (* f44 f43))) (define-fun f131 () Arctic (+ (* f42 f38) (* f43 f41) (* f44 f44))) (define-fun f132 () Arctic (+ (* f36 f45) (* f37 f46) (* f38 f47))) (define-fun f133 () Arctic (+ (* f39 f45) (* f40 f46) (* f41 f47))) (define-fun f134 () Arctic (+ (* f42 f45) (* f43 f46) (* f44 f47))) (define-fun f135 () Arctic (+ f45 f132)) (define-fun f136 () Arctic (+ f46 f133)) (define-fun f137 () Arctic (+ f47 f134)) (define-fun f138 () Arctic (+ (* f24 f123) (* f25 f126) (* f26 f129))) (define-fun f139 () Arctic (+ (* f24 f124) (* f25 f127) (* f26 f130))) (define-fun f140 () Arctic (+ (* f24 f125) (* f25 f128) (* f26 f131))) (define-fun f141 () Arctic (+ (* f27 f123) (* f28 f126) (* f29 f129))) (define-fun f142 () Arctic (+ (* f27 f124) (* f28 f127) (* f29 f130))) (define-fun f143 () Arctic (+ (* f27 f125) (* f28 f128) (* f29 f131))) (define-fun f144 () Arctic (+ (* f30 f123) (* f31 f126) (* f32 f129))) (define-fun f145 () Arctic (+ (* f30 f124) (* f31 f127) (* f32 f130))) (define-fun f146 () Arctic (+ (* f30 f125) (* f31 f128) (* f32 f131))) (define-fun f147 () Arctic (+ (* f24 f135) (* f25 f136) (* f26 f137))) (define-fun f148 () Arctic (+ (* f27 f135) (* f28 f136) (* f29 f137))) (define-fun f149 () Arctic (+ (* f30 f135) (* f31 f136) (* f32 f137))) (define-fun f150 () Arctic (+ f33 f147)) (define-fun f151 () Arctic (+ f34 f148)) (define-fun f152 () Arctic (+ f35 f149)) (define-fun f153 () Arctic (+ (* f48 f60) (* f49 f63) (* f50 f66))) (define-fun f154 () Arctic (+ (* f48 f61) (* f49 f64) (* f50 f67))) (define-fun f155 () Arctic (+ (* f48 f62) (* f49 f65) (* f50 f68))) (define-fun f156 () Arctic (+ (* f51 f60) (* f52 f63) (* f53 f66))) (define-fun f157 () Arctic (+ (* f51 f61) (* f52 f64) (* f53 f67))) (define-fun f158 () Arctic (+ (* f51 f62) (* f52 f65) (* f53 f68))) (define-fun f159 () Arctic (+ (* f54 f60) (* f55 f63) (* f56 f66))) (define-fun f160 () Arctic (+ (* f54 f61) (* f55 f64) (* f56 f67))) (define-fun f161 () Arctic (+ (* f54 f62) (* f55 f65) (* f56 f68))) (define-fun f162 () Arctic (+ (* f48 f69) (* f49 f70) (* f50 f71))) (define-fun f163 () Arctic (+ (* f51 f69) (* f52 f70) (* f53 f71))) (define-fun f164 () Arctic (+ (* f54 f69) (* f55 f70) (* f56 f71))) (define-fun f165 () Arctic (+ f57 f162)) (define-fun f166 () Arctic (+ f58 f163)) (define-fun f167 () Arctic (+ f59 f164)) (define-fun f168 () Arctic (+ (* f24 f36) (* f25 f39) (* f26 f42))) (define-fun f169 () Arctic (+ (* f24 f37) (* f25 f40) (* f26 f43))) (define-fun f170 () Arctic (+ (* f24 f38) (* f25 f41) (* f26 f44))) (define-fun f171 () Arctic (+ (* f27 f36) (* f28 f39) (* f29 f42))) (define-fun f172 () Arctic (+ (* f27 f37) (* f28 f40) (* f29 f43))) (define-fun f173 () Arctic (+ (* f27 f38) (* f28 f41) (* f29 f44))) (define-fun f174 () Arctic (+ (* f30 f36) (* f31 f39) (* f32 f42))) (define-fun f175 () Arctic (+ (* f30 f37) (* f31 f40) (* f32 f43))) (define-fun f176 () Arctic (+ (* f30 f38) (* f31 f41) (* f32 f44))) (define-fun f177 () Arctic (+ (* f24 f45) (* f25 f46) (* f26 f47))) (define-fun f178 () Arctic (+ (* f27 f45) (* f28 f46) (* f29 f47))) (define-fun f179 () Arctic (+ (* f30 f45) (* f31 f46) (* f32 f47))) (define-fun f180 () Arctic (+ f33 f177)) (define-fun f181 () Arctic (+ f34 f178)) (define-fun f182 () Arctic (+ f35 f179)) (define-fun f183 () Arctic (+ (* f60 f60) (* f61 f63) (* f62 f66))) (define-fun f184 () Arctic (+ (* f60 f61) (* f61 f64) (* f62 f67))) (define-fun f185 () Arctic (+ (* f60 f62) (* f61 f65) (* f62 f68))) (define-fun f186 () Arctic (+ (* f63 f60) (* f64 f63) (* f65 f66))) (define-fun f187 () Arctic (+ (* f63 f61) (* f64 f64) (* f65 f67))) (define-fun f188 () Arctic (+ (* f63 f62) (* f64 f65) (* f65 f68))) (define-fun f189 () Arctic (+ (* f66 f60) (* f67 f63) (* f68 f66))) (define-fun f190 () Arctic (+ (* f66 f61) (* f67 f64) (* f68 f67))) (define-fun f191 () Arctic (+ (* f66 f62) (* f67 f65) (* f68 f68))) (define-fun f192 () Arctic (+ (* f60 f69) (* f61 f70) (* f62 f71))) (define-fun f193 () Arctic (+ (* f63 f69) (* f64 f70) (* f65 f71))) (define-fun f194 () Arctic (+ (* f66 f69) (* f67 f70) (* f68 f71))) (define-fun f195 () Arctic (+ f69 f192)) (define-fun f196 () Arctic (+ f70 f193)) (define-fun f197 () Arctic (+ f71 f194)) (define-fun f198 () Arctic (+ (* f72 f183) (* f73 f186) (* f74 f189))) (define-fun f199 () Arctic (+ (* f72 f184) (* f73 f187) (* f74 f190))) (define-fun f200 () Arctic (+ (* f72 f185) (* f73 f188) (* f74 f191))) (define-fun f201 () Arctic (+ (* f75 f183) (* f76 f186) (* f77 f189))) (define-fun f202 () Arctic (+ (* f75 f184) (* f76 f187) (* f77 f190))) (define-fun f203 () Arctic (+ (* f75 f185) (* f76 f188) (* f77 f191))) (define-fun f204 () Arctic (+ (* f78 f183) (* f79 f186) (* f80 f189))) (define-fun f205 () Arctic (+ (* f78 f184) (* f79 f187) (* f80 f190))) (define-fun f206 () Arctic (+ (* f78 f185) (* f79 f188) (* f80 f191))) (define-fun f207 () Arctic (+ (* f72 f195) (* f73 f196) (* f74 f197))) (define-fun f208 () Arctic (+ (* f75 f195) (* f76 f196) (* f77 f197))) (define-fun f209 () Arctic (+ (* f78 f195) (* f79 f196) (* f80 f197))) (define-fun f210 () Arctic (+ f81 f207)) (define-fun f211 () Arctic (+ f82 f208)) (define-fun f212 () Arctic (+ f83 f209)) (define-fun f213 () Arctic (+ (* f72 f60) (* f73 f63) (* f74 f66))) (define-fun f214 () Arctic (+ (* f72 f61) (* f73 f64) (* f74 f67))) (define-fun f215 () Arctic (+ (* f72 f62) (* f73 f65) (* f74 f68))) (define-fun f216 () Arctic (+ (* f75 f60) (* f76 f63) (* f77 f66))) (define-fun f217 () Arctic (+ (* f75 f61) (* f76 f64) (* f77 f67))) (define-fun f218 () Arctic (+ (* f75 f62) (* f76 f65) (* f77 f68))) (define-fun f219 () Arctic (+ (* f78 f60) (* f79 f63) (* f80 f66))) (define-fun f220 () Arctic (+ (* f78 f61) (* f79 f64) (* f80 f67))) (define-fun f221 () Arctic (+ (* f78 f62) (* f79 f65) (* f80 f68))) (define-fun f222 () Arctic (+ (* f72 f69) (* f73 f70) (* f74 f71))) (define-fun f223 () Arctic (+ (* f75 f69) (* f76 f70) (* f77 f71))) (define-fun f224 () Arctic (+ (* f78 f69) (* f79 f70) (* f80 f71))) (define-fun f225 () Arctic (+ f81 f222)) (define-fun f226 () Arctic (+ f82 f223)) (define-fun f227 () Arctic (+ f83 f224)) (define-fun f228 () Arctic (+ (* f84 f84) (* f85 f87) (* f86 f90))) (define-fun f229 () Arctic (+ (* f84 f85) (* f85 f88) (* f86 f91))) (define-fun f230 () Arctic (+ (* f84 f86) (* f85 f89) (* f86 f92))) (define-fun f231 () Arctic (+ (* f87 f84) (* f88 f87) (* f89 f90))) (define-fun f232 () Arctic (+ (* f87 f85) (* f88 f88) (* f89 f91))) (define-fun f233 () Arctic (+ (* f87 f86) (* f88 f89) (* f89 f92))) (define-fun f234 () Arctic (+ (* f90 f84) (* f91 f87) (* f92 f90))) (define-fun f235 () Arctic (+ (* f90 f85) (* f91 f88) (* f92 f91))) (define-fun f236 () Arctic (+ (* f90 f86) (* f91 f89) (* f92 f92))) (define-fun f237 () Arctic (+ (* f84 f93) (* f85 f94) (* f86 f95))) (define-fun f238 () Arctic (+ (* f87 f93) (* f88 f94) (* f89 f95))) (define-fun f239 () Arctic (+ (* f90 f93) (* f91 f94) (* f92 f95))) (define-fun f240 () Arctic (+ f93 f237)) (define-fun f241 () Arctic (+ f94 f238)) (define-fun f242 () Arctic (+ f95 f239)) (define-fun f243 () Arctic (+ (* f48 f228) (* f49 f231) (* f50 f234))) (define-fun f244 () Arctic (+ (* f48 f229) (* f49 f232) (* f50 f235))) (define-fun f245 () Arctic (+ (* f48 f230) (* f49 f233) (* f50 f236))) (define-fun f246 () Arctic (+ (* f51 f228) (* f52 f231) (* f53 f234))) (define-fun f247 () Arctic (+ (* f51 f229) (* f52 f232) (* f53 f235))) (define-fun f248 () Arctic (+ (* f51 f230) (* f52 f233) (* f53 f236))) (define-fun f249 () Arctic (+ (* f54 f228) (* f55 f231) (* f56 f234))) (define-fun f250 () Arctic (+ (* f54 f229) (* f55 f232) (* f56 f235))) (define-fun f251 () Arctic (+ (* f54 f230) (* f55 f233) (* f56 f236))) (define-fun f252 () Arctic (+ (* f48 f240) (* f49 f241) (* f50 f242))) (define-fun f253 () Arctic (+ (* f51 f240) (* f52 f241) (* f53 f242))) (define-fun f254 () Arctic (+ (* f54 f240) (* f55 f241) (* f56 f242))) (define-fun f255 () Arctic (+ f57 f252)) (define-fun f256 () Arctic (+ f58 f253)) (define-fun f257 () Arctic (+ f59 f254)) (define-fun f258 () Arctic (+ (* f84 f60) (* f85 f63) (* f86 f66))) (define-fun f259 () Arctic (+ (* f84 f61) (* f85 f64) (* f86 f67))) (define-fun f260 () Arctic (+ (* f84 f62) (* f85 f65) (* f86 f68))) (define-fun f261 () Arctic (+ (* f87 f60) (* f88 f63) (* f89 f66))) (define-fun f262 () Arctic (+ (* f87 f61) (* f88 f64) (* f89 f67))) (define-fun f263 () Arctic (+ (* f87 f62) (* f88 f65) (* f89 f68))) (define-fun f264 () Arctic (+ (* f90 f60) (* f91 f63) (* f92 f66))) (define-fun f265 () Arctic (+ (* f90 f61) (* f91 f64) (* f92 f67))) (define-fun f266 () Arctic (+ (* f90 f62) (* f91 f65) (* f92 f68))) (define-fun f267 () Arctic (+ (* f84 f69) (* f85 f70) (* f86 f71))) (define-fun f268 () Arctic (+ (* f87 f69) (* f88 f70) (* f89 f71))) (define-fun f269 () Arctic (+ (* f90 f69) (* f91 f70) (* f92 f71))) (define-fun f270 () Arctic (+ f93 f267)) (define-fun f271 () Arctic (+ f94 f268)) (define-fun f272 () Arctic (+ f95 f269)) (define-fun f273 () Arctic (+ (* f48 f258) (* f49 f261) (* f50 f264))) (define-fun f274 () Arctic (+ (* f48 f259) (* f49 f262) (* f50 f265))) (define-fun f275 () Arctic (+ (* f48 f260) (* f49 f263) (* f50 f266))) (define-fun f276 () Arctic (+ (* f51 f258) (* f52 f261) (* f53 f264))) (define-fun f277 () Arctic (+ (* f51 f259) (* f52 f262) (* f53 f265))) (define-fun f278 () Arctic (+ (* f51 f260) (* f52 f263) (* f53 f266))) (define-fun f279 () Arctic (+ (* f54 f258) (* f55 f261) (* f56 f264))) (define-fun f280 () Arctic (+ (* f54 f259) (* f55 f262) (* f56 f265))) (define-fun f281 () Arctic (+ (* f54 f260) (* f55 f263) (* f56 f266))) (define-fun f282 () Arctic (+ (* f48 f270) (* f49 f271) (* f50 f272))) (define-fun f283 () Arctic (+ (* f51 f270) (* f52 f271) (* f53 f272))) (define-fun f284 () Arctic (+ (* f54 f270) (* f55 f271) (* f56 f272))) (define-fun f285 () Arctic (+ f57 f282)) (define-fun f286 () Arctic (+ f58 f283)) (define-fun f287 () Arctic (+ f59 f284)) (define-fun f288 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f289 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f290 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f291 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f292 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f293 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f294 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f295 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f296 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f297 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f298 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f299 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f300 () Arctic (+ f21 f297)) (define-fun f301 () Arctic (+ f22 f298)) (define-fun f302 () Arctic (+ f23 f299)) (define-fun f303 () Arctic (+ (* f36 f36) (* f37 f39) (* f38 f42))) (define-fun f304 () Arctic (+ (* f36 f37) (* f37 f40) (* f38 f43))) (define-fun f305 () Arctic (+ (* f36 f38) (* f37 f41) (* f38 f44))) (define-fun f306 () Arctic (+ (* f39 f36) (* f40 f39) (* f41 f42))) (define-fun f307 () Arctic (+ (* f39 f37) (* f40 f40) (* f41 f43))) (define-fun f308 () Arctic (+ (* f39 f38) (* f40 f41) (* f41 f44))) (define-fun f309 () Arctic (+ (* f42 f36) (* f43 f39) (* f44 f42))) (define-fun f310 () Arctic (+ (* f42 f37) (* f43 f40) (* f44 f43))) (define-fun f311 () Arctic (+ (* f42 f38) (* f43 f41) (* f44 f44))) (define-fun f312 () Arctic (+ (* f36 f45) (* f37 f46) (* f38 f47))) (define-fun f313 () Arctic (+ (* f39 f45) (* f40 f46) (* f41 f47))) (define-fun f314 () Arctic (+ (* f42 f45) (* f43 f46) (* f44 f47))) (define-fun f315 () Arctic (+ f45 f312)) (define-fun f316 () Arctic (+ f46 f313)) (define-fun f317 () Arctic (+ f47 f314)) (define-fun f318 () Arctic (+ (* f36 f303) (* f37 f306) (* f38 f309))) (define-fun f319 () Arctic (+ (* f36 f304) (* f37 f307) (* f38 f310))) (define-fun f320 () Arctic (+ (* f36 f305) (* f37 f308) (* f38 f311))) (define-fun f321 () Arctic (+ (* f39 f303) (* f40 f306) (* f41 f309))) (define-fun f322 () Arctic (+ (* f39 f304) (* f40 f307) (* f41 f310))) (define-fun f323 () Arctic (+ (* f39 f305) (* f40 f308) (* f41 f311))) (define-fun f324 () Arctic (+ (* f42 f303) (* f43 f306) (* f44 f309))) (define-fun f325 () Arctic (+ (* f42 f304) (* f43 f307) (* f44 f310))) (define-fun f326 () Arctic (+ (* f42 f305) (* f43 f308) (* f44 f311))) (define-fun f327 () Arctic (+ (* f36 f315) (* f37 f316) (* f38 f317))) (define-fun f328 () Arctic (+ (* f39 f315) (* f40 f316) (* f41 f317))) (define-fun f329 () Arctic (+ (* f42 f315) (* f43 f316) (* f44 f317))) (define-fun f330 () Arctic (+ f45 f327)) (define-fun f331 () Arctic (+ f46 f328)) (define-fun f332 () Arctic (+ f47 f329)) (define-fun f333 () Arctic (+ (* f84 f60) (* f85 f63) (* f86 f66))) (define-fun f334 () Arctic (+ (* f84 f61) (* f85 f64) (* f86 f67))) (define-fun f335 () Arctic (+ (* f84 f62) (* f85 f65) (* f86 f68))) (define-fun f336 () Arctic (+ (* f87 f60) (* f88 f63) (* f89 f66))) (define-fun f337 () Arctic (+ (* f87 f61) (* f88 f64) (* f89 f67))) (define-fun f338 () Arctic (+ (* f87 f62) (* f88 f65) (* f89 f68))) (define-fun f339 () Arctic (+ (* f90 f60) (* f91 f63) (* f92 f66))) (define-fun f340 () Arctic (+ (* f90 f61) (* f91 f64) (* f92 f67))) (define-fun f341 () Arctic (+ (* f90 f62) (* f91 f65) (* f92 f68))) (define-fun f342 () Arctic (+ (* f84 f69) (* f85 f70) (* f86 f71))) (define-fun f343 () Arctic (+ (* f87 f69) (* f88 f70) (* f89 f71))) (define-fun f344 () Arctic (+ (* f90 f69) (* f91 f70) (* f92 f71))) (define-fun f345 () Arctic (+ f93 f342)) (define-fun f346 () Arctic (+ f94 f343)) (define-fun f347 () Arctic (+ f95 f344)) (define-fun f348 () Arctic (+ (* f36 f36) (* f37 f39) (* f38 f42))) (define-fun f349 () Arctic (+ (* f36 f37) (* f37 f40) (* f38 f43))) (define-fun f350 () Arctic (+ (* f36 f38) (* f37 f41) (* f38 f44))) (define-fun f351 () Arctic (+ (* f39 f36) (* f40 f39) (* f41 f42))) (define-fun f352 () Arctic (+ (* f39 f37) (* f40 f40) (* f41 f43))) (define-fun f353 () Arctic (+ (* f39 f38) (* f40 f41) (* f41 f44))) (define-fun f354 () Arctic (+ (* f42 f36) (* f43 f39) (* f44 f42))) (define-fun f355 () Arctic (+ (* f42 f37) (* f43 f40) (* f44 f43))) (define-fun f356 () Arctic (+ (* f42 f38) (* f43 f41) (* f44 f44))) (define-fun f357 () Arctic (+ (* f36 f45) (* f37 f46) (* f38 f47))) (define-fun f358 () Arctic (+ (* f39 f45) (* f40 f46) (* f41 f47))) (define-fun f359 () Arctic (+ (* f42 f45) (* f43 f46) (* f44 f47))) (define-fun f360 () Arctic (+ f45 f357)) (define-fun f361 () Arctic (+ f46 f358)) (define-fun f362 () Arctic (+ f47 f359)) (define-fun f363 () Arctic (+ (* f60 f60) (* f61 f63) (* f62 f66))) (define-fun f364 () Arctic (+ (* f60 f61) (* f61 f64) (* f62 f67))) (define-fun f365 () Arctic (+ (* f60 f62) (* f61 f65) (* f62 f68))) (define-fun f366 () Arctic (+ (* f63 f60) (* f64 f63) (* f65 f66))) (define-fun f367 () Arctic (+ (* f63 f61) (* f64 f64) (* f65 f67))) (define-fun f368 () Arctic (+ (* f63 f62) (* f64 f65) (* f65 f68))) (define-fun f369 () Arctic (+ (* f66 f60) (* f67 f63) (* f68 f66))) (define-fun f370 () Arctic (+ (* f66 f61) (* f67 f64) (* f68 f67))) (define-fun f371 () Arctic (+ (* f66 f62) (* f67 f65) (* f68 f68))) (define-fun f372 () Arctic (+ (* f60 f69) (* f61 f70) (* f62 f71))) (define-fun f373 () Arctic (+ (* f63 f69) (* f64 f70) (* f65 f71))) (define-fun f374 () Arctic (+ (* f66 f69) (* f67 f70) (* f68 f71))) (define-fun f375 () Arctic (+ f69 f372)) (define-fun f376 () Arctic (+ f70 f373)) (define-fun f377 () Arctic (+ f71 f374)) (define-fun f378 () Arctic (+ (* f60 f363) (* f61 f366) (* f62 f369))) (define-fun f379 () Arctic (+ (* f60 f364) (* f61 f367) (* f62 f370))) (define-fun f380 () Arctic (+ (* f60 f365) (* f61 f368) (* f62 f371))) (define-fun f381 () Arctic (+ (* f63 f363) (* f64 f366) (* f65 f369))) (define-fun f382 () Arctic (+ (* f63 f364) (* f64 f367) (* f65 f370))) (define-fun f383 () Arctic (+ (* f63 f365) (* f64 f368) (* f65 f371))) (define-fun f384 () Arctic (+ (* f66 f363) (* f67 f366) (* f68 f369))) (define-fun f385 () Arctic (+ (* f66 f364) (* f67 f367) (* f68 f370))) (define-fun f386 () Arctic (+ (* f66 f365) (* f67 f368) (* f68 f371))) (define-fun f387 () Arctic (+ (* f60 f375) (* f61 f376) (* f62 f377))) (define-fun f388 () Arctic (+ (* f63 f375) (* f64 f376) (* f65 f377))) (define-fun f389 () Arctic (+ (* f66 f375) (* f67 f376) (* f68 f377))) (define-fun f390 () Arctic (+ f69 f387)) (define-fun f391 () Arctic (+ f70 f388)) (define-fun f392 () Arctic (+ f71 f389)) (define-fun f393 () Arctic (+ (* f60 f60) (* f61 f63) (* f62 f66))) (define-fun f394 () Arctic (+ (* f60 f61) (* f61 f64) (* f62 f67))) (define-fun f395 () Arctic (+ (* f60 f62) (* f61 f65) (* f62 f68))) (define-fun f396 () Arctic (+ (* f63 f60) (* f64 f63) (* f65 f66))) (define-fun f397 () Arctic (+ (* f63 f61) (* f64 f64) (* f65 f67))) (define-fun f398 () Arctic (+ (* f63 f62) (* f64 f65) (* f65 f68))) (define-fun f399 () Arctic (+ (* f66 f60) (* f67 f63) (* f68 f66))) (define-fun f400 () Arctic (+ (* f66 f61) (* f67 f64) (* f68 f67))) (define-fun f401 () Arctic (+ (* f66 f62) (* f67 f65) (* f68 f68))) (define-fun f402 () Arctic (+ (* f60 f69) (* f61 f70) (* f62 f71))) (define-fun f403 () Arctic (+ (* f63 f69) (* f64 f70) (* f65 f71))) (define-fun f404 () Arctic (+ (* f66 f69) (* f67 f70) (* f68 f71))) (define-fun f405 () Arctic (+ f69 f402)) (define-fun f406 () Arctic (+ f70 f403)) (define-fun f407 () Arctic (+ f71 f404)) (define-fun f408 () Arctic (+ (* f84 f84) (* f85 f87) (* f86 f90))) (define-fun f409 () Arctic (+ (* f84 f85) (* f85 f88) (* f86 f91))) (define-fun f410 () Arctic (+ (* f84 f86) (* f85 f89) (* f86 f92))) (define-fun f411 () Arctic (+ (* f87 f84) (* f88 f87) (* f89 f90))) (define-fun f412 () Arctic (+ (* f87 f85) (* f88 f88) (* f89 f91))) (define-fun f413 () Arctic (+ (* f87 f86) (* f88 f89) (* f89 f92))) (define-fun f414 () Arctic (+ (* f90 f84) (* f91 f87) (* f92 f90))) (define-fun f415 () Arctic (+ (* f90 f85) (* f91 f88) (* f92 f91))) (define-fun f416 () Arctic (+ (* f90 f86) (* f91 f89) (* f92 f92))) (define-fun f417 () Arctic (+ (* f84 f93) (* f85 f94) (* f86 f95))) (define-fun f418 () Arctic (+ (* f87 f93) (* f88 f94) (* f89 f95))) (define-fun f419 () Arctic (+ (* f90 f93) (* f91 f94) (* f92 f95))) (define-fun f420 () Arctic (+ f93 f417)) (define-fun f421 () Arctic (+ f94 f418)) (define-fun f422 () Arctic (+ f95 f419)) (define-fun f423 () Arctic (+ (* f84 f408) (* f85 f411) (* f86 f414))) (define-fun f424 () Arctic (+ (* f84 f409) (* f85 f412) (* f86 f415))) (define-fun f425 () Arctic (+ (* f84 f410) (* f85 f413) (* f86 f416))) (define-fun f426 () Arctic (+ (* f87 f408) (* f88 f411) (* f89 f414))) (define-fun f427 () Arctic (+ (* f87 f409) (* f88 f412) (* f89 f415))) (define-fun f428 () Arctic (+ (* f87 f410) (* f88 f413) (* f89 f416))) (define-fun f429 () Arctic (+ (* f90 f408) (* f91 f411) (* f92 f414))) (define-fun f430 () Arctic (+ (* f90 f409) (* f91 f412) (* f92 f415))) (define-fun f431 () Arctic (+ (* f90 f410) (* f91 f413) (* f92 f416))) (define-fun f432 () Arctic (+ (* f84 f420) (* f85 f421) (* f86 f422))) (define-fun f433 () Arctic (+ (* f87 f420) (* f88 f421) (* f89 f422))) (define-fun f434 () Arctic (+ (* f90 f420) (* f91 f421) (* f92 f422))) (define-fun f435 () Arctic (+ f93 f432)) (define-fun f436 () Arctic (+ f94 f433)) (define-fun f437 () Arctic (+ f95 f434)) (define-fun f438 () Arctic (+ (* f84 f96) (* f85 f99) (* f86 f102))) (define-fun f439 () Arctic (+ (* f84 f97) (* f85 f100) (* f86 f103))) (define-fun f440 () Arctic (+ (* f84 f98) (* f85 f101) (* f86 f104))) (define-fun f441 () Arctic (+ (* f87 f96) (* f88 f99) (* f89 f102))) (define-fun f442 () Arctic (+ (* f87 f97) (* f88 f100) (* f89 f103))) (define-fun f443 () Arctic (+ (* f87 f98) (* f88 f101) (* f89 f104))) (define-fun f444 () Arctic (+ (* f90 f96) (* f91 f99) (* f92 f102))) (define-fun f445 () Arctic (+ (* f90 f97) (* f91 f100) (* f92 f103))) (define-fun f446 () Arctic (+ (* f90 f98) (* f91 f101) (* f92 f104))) (define-fun f447 () Arctic (+ (* f84 f105) (* f85 f106) (* f86 f107))) (define-fun f448 () Arctic (+ (* f87 f105) (* f88 f106) (* f89 f107))) (define-fun f449 () Arctic (+ (* f90 f105) (* f91 f106) (* f92 f107))) (define-fun f450 () Arctic (+ f93 f447)) (define-fun f451 () Arctic (+ f94 f448)) (define-fun f452 () Arctic (+ f95 f449)) (define-fun f453 () Arctic (+ (* f36 f12) (* f37 f15) (* f38 f18))) (define-fun f454 () Arctic (+ (* f36 f13) (* f37 f16) (* f38 f19))) (define-fun f455 () Arctic (+ (* f36 f14) (* f37 f17) (* f38 f20))) (define-fun f456 () Arctic (+ (* f39 f12) (* f40 f15) (* f41 f18))) (define-fun f457 () Arctic (+ (* f39 f13) (* f40 f16) (* f41 f19))) (define-fun f458 () Arctic (+ (* f39 f14) (* f40 f17) (* f41 f20))) (define-fun f459 () Arctic (+ (* f42 f12) (* f43 f15) (* f44 f18))) (define-fun f460 () Arctic (+ (* f42 f13) (* f43 f16) (* f44 f19))) (define-fun f461 () Arctic (+ (* f42 f14) (* f43 f17) (* f44 f20))) (define-fun f462 () Arctic (+ (* f36 f21) (* f37 f22) (* f38 f23))) (define-fun f463 () Arctic (+ (* f39 f21) (* f40 f22) (* f41 f23))) (define-fun f464 () Arctic (+ (* f42 f21) (* f43 f22) (* f44 f23))) (define-fun f465 () Arctic (+ f45 f462)) (define-fun f466 () Arctic (+ f46 f463)) (define-fun f467 () Arctic (+ f47 f464)) (define-fun f468 () Arctic (+ (* f60 f453) (* f61 f456) (* f62 f459))) (define-fun f469 () Arctic (+ (* f60 f454) (* f61 f457) (* f62 f460))) (define-fun f470 () Arctic (+ (* f60 f455) (* f61 f458) (* f62 f461))) (define-fun f471 () Arctic (+ (* f63 f453) (* f64 f456) (* f65 f459))) (define-fun f472 () Arctic (+ (* f63 f454) (* f64 f457) (* f65 f460))) (define-fun f473 () Arctic (+ (* f63 f455) (* f64 f458) (* f65 f461))) (define-fun f474 () Arctic (+ (* f66 f453) (* f67 f456) (* f68 f459))) (define-fun f475 () Arctic (+ (* f66 f454) (* f67 f457) (* f68 f460))) (define-fun f476 () Arctic (+ (* f66 f455) (* f67 f458) (* f68 f461))) (define-fun f477 () Arctic (+ (* f60 f465) (* f61 f466) (* f62 f467))) (define-fun f478 () Arctic (+ (* f63 f465) (* f64 f466) (* f65 f467))) (define-fun f479 () Arctic (+ (* f66 f465) (* f67 f466) (* f68 f467))) (define-fun f480 () Arctic (+ f69 f477)) (define-fun f481 () Arctic (+ f70 f478)) (define-fun f482 () Arctic (+ f71 f479)) (define-fun f483 () Arctic (+ (* f84 f468) (* f85 f471) (* f86 f474))) (define-fun f484 () Arctic (+ (* f84 f469) (* f85 f472) (* f86 f475))) (define-fun f485 () Arctic (+ (* f84 f470) (* f85 f473) (* f86 f476))) (define-fun f486 () Arctic (+ (* f87 f468) (* f88 f471) (* f89 f474))) (define-fun f487 () Arctic (+ (* f87 f469) (* f88 f472) (* f89 f475))) (define-fun f488 () Arctic (+ (* f87 f470) (* f88 f473) (* f89 f476))) (define-fun f489 () Arctic (+ (* f90 f468) (* f91 f471) (* f92 f474))) (define-fun f490 () Arctic (+ (* f90 f469) (* f91 f472) (* f92 f475))) (define-fun f491 () Arctic (+ (* f90 f470) (* f91 f473) (* f92 f476))) (define-fun f492 () Arctic (+ (* f84 f480) (* f85 f481) (* f86 f482))) (define-fun f493 () Arctic (+ (* f87 f480) (* f88 f481) (* f89 f482))) (define-fun f494 () Arctic (+ (* f90 f480) (* f91 f481) (* f92 f482))) (define-fun f495 () Arctic (+ f93 f492)) (define-fun f496 () Arctic (+ f94 f493)) (define-fun f497 () Arctic (+ f95 f494)) (define-fun f498 () Arctic (+ (* f96 f483) (* f97 f486) (* f98 f489))) (define-fun f499 () Arctic (+ (* f96 f484) (* f97 f487) (* f98 f490))) (define-fun f500 () Arctic (+ (* f96 f485) (* f97 f488) (* f98 f491))) (define-fun f501 () Arctic (+ (* f99 f483) (* f100 f486) (* f101 f489))) (define-fun f502 () Arctic (+ (* f99 f484) (* f100 f487) (* f101 f490))) (define-fun f503 () Arctic (+ (* f99 f485) (* f100 f488) (* f101 f491))) (define-fun f504 () Arctic (+ (* f102 f483) (* f103 f486) (* f104 f489))) (define-fun f505 () Arctic (+ (* f102 f484) (* f103 f487) (* f104 f490))) (define-fun f506 () Arctic (+ (* f102 f485) (* f103 f488) (* f104 f491))) (define-fun f507 () Arctic (+ (* f96 f495) (* f97 f496) (* f98 f497))) (define-fun f508 () Arctic (+ (* f99 f495) (* f100 f496) (* f101 f497))) (define-fun f509 () Arctic (+ (* f102 f495) (* f103 f496) (* f104 f497))) (define-fun f510 () Arctic (+ f105 f507)) (define-fun f511 () Arctic (+ f106 f508)) (define-fun f512 () Arctic (+ f107 f509)) (define-fun f513 () Arctic (+ (* f84 f84) (* f85 f87) (* f86 f90))) (define-fun f514 () Arctic (+ (* f84 f85) (* f85 f88) (* f86 f91))) (define-fun f515 () Arctic (+ (* f84 f86) (* f85 f89) (* f86 f92))) (define-fun f516 () Arctic (+ (* f87 f84) (* f88 f87) (* f89 f90))) (define-fun f517 () Arctic (+ (* f87 f85) (* f88 f88) (* f89 f91))) (define-fun f518 () Arctic (+ (* f87 f86) (* f88 f89) (* f89 f92))) (define-fun f519 () Arctic (+ (* f90 f84) (* f91 f87) (* f92 f90))) (define-fun f520 () Arctic (+ (* f90 f85) (* f91 f88) (* f92 f91))) (define-fun f521 () Arctic (+ (* f90 f86) (* f91 f89) (* f92 f92))) (define-fun f522 () Arctic (+ (* f84 f93) (* f85 f94) (* f86 f95))) (define-fun f523 () Arctic (+ (* f87 f93) (* f88 f94) (* f89 f95))) (define-fun f524 () Arctic (+ (* f90 f93) (* f91 f94) (* f92 f95))) (define-fun f525 () Arctic (+ f93 f522)) (define-fun f526 () Arctic (+ f94 f523)) (define-fun f527 () Arctic (+ f95 f524)) (define-fun f528 () Arctic (+ (* f60 f96) (* f61 f99) (* f62 f102))) (define-fun f529 () Arctic (+ (* f60 f97) (* f61 f100) (* f62 f103))) (define-fun f530 () Arctic (+ (* f60 f98) (* f61 f101) (* f62 f104))) (define-fun f531 () Arctic (+ (* f63 f96) (* f64 f99) (* f65 f102))) (define-fun f532 () Arctic (+ (* f63 f97) (* f64 f100) (* f65 f103))) (define-fun f533 () Arctic (+ (* f63 f98) (* f64 f101) (* f65 f104))) (define-fun f534 () Arctic (+ (* f66 f96) (* f67 f99) (* f68 f102))) (define-fun f535 () Arctic (+ (* f66 f97) (* f67 f100) (* f68 f103))) (define-fun f536 () Arctic (+ (* f66 f98) (* f67 f101) (* f68 f104))) (define-fun f537 () Arctic (+ (* f60 f105) (* f61 f106) (* f62 f107))) (define-fun f538 () Arctic (+ (* f63 f105) (* f64 f106) (* f65 f107))) (define-fun f539 () Arctic (+ (* f66 f105) (* f67 f106) (* f68 f107))) (define-fun f540 () Arctic (+ f69 f537)) (define-fun f541 () Arctic (+ f70 f538)) (define-fun f542 () Arctic (+ f71 f539)) (define-fun f543 () Arctic (+ (* f12 f36) (* f13 f39) (* f14 f42))) (define-fun f544 () Arctic (+ (* f12 f37) (* f13 f40) (* f14 f43))) (define-fun f545 () Arctic (+ (* f12 f38) (* f13 f41) (* f14 f44))) (define-fun f546 () Arctic (+ (* f15 f36) (* f16 f39) (* f17 f42))) (define-fun f547 () Arctic (+ (* f15 f37) (* f16 f40) (* f17 f43))) (define-fun f548 () Arctic (+ (* f15 f38) (* f16 f41) (* f17 f44))) (define-fun f549 () Arctic (+ (* f18 f36) (* f19 f39) (* f20 f42))) (define-fun f550 () Arctic (+ (* f18 f37) (* f19 f40) (* f20 f43))) (define-fun f551 () Arctic (+ (* f18 f38) (* f19 f41) (* f20 f44))) (define-fun f552 () Arctic (+ (* f12 f45) (* f13 f46) (* f14 f47))) (define-fun f553 () Arctic (+ (* f15 f45) (* f16 f46) (* f17 f47))) (define-fun f554 () Arctic (+ (* f18 f45) (* f19 f46) (* f20 f47))) (define-fun f555 () Arctic (+ f21 f552)) (define-fun f556 () Arctic (+ f22 f553)) (define-fun f557 () Arctic (+ f23 f554)) (define-fun f558 () Arctic (+ (* f12 f543) (* f13 f546) (* f14 f549))) (define-fun f559 () Arctic (+ (* f12 f544) (* f13 f547) (* f14 f550))) (define-fun f560 () Arctic (+ (* f12 f545) (* f13 f548) (* f14 f551))) (define-fun f561 () Arctic (+ (* f15 f543) (* f16 f546) (* f17 f549))) (define-fun f562 () Arctic (+ (* f15 f544) (* f16 f547) (* f17 f550))) (define-fun f563 () Arctic (+ (* f15 f545) (* f16 f548) (* f17 f551))) (define-fun f564 () Arctic (+ (* f18 f543) (* f19 f546) (* f20 f549))) (define-fun f565 () Arctic (+ (* f18 f544) (* f19 f547) (* f20 f550))) (define-fun f566 () Arctic (+ (* f18 f545) (* f19 f548) (* f20 f551))) (define-fun f567 () Arctic (+ (* f12 f555) (* f13 f556) (* f14 f557))) (define-fun f568 () Arctic (+ (* f15 f555) (* f16 f556) (* f17 f557))) (define-fun f569 () Arctic (+ (* f18 f555) (* f19 f556) (* f20 f557))) (define-fun f570 () Arctic (+ f21 f567)) (define-fun f571 () Arctic (+ f22 f568)) (define-fun f572 () Arctic (+ f23 f569)) (define-fun f573 () Arctic (+ (* f96 f558) (* f97 f561) (* f98 f564))) (define-fun f574 () Arctic (+ (* f96 f559) (* f97 f562) (* f98 f565))) (define-fun f575 () Arctic (+ (* f96 f560) (* f97 f563) (* f98 f566))) (define-fun f576 () Arctic (+ (* f99 f558) (* f100 f561) (* f101 f564))) (define-fun f577 () Arctic (+ (* f99 f559) (* f100 f562) (* f101 f565))) (define-fun f578 () Arctic (+ (* f99 f560) (* f100 f563) (* f101 f566))) (define-fun f579 () Arctic (+ (* f102 f558) (* f103 f561) (* f104 f564))) (define-fun f580 () Arctic (+ (* f102 f559) (* f103 f562) (* f104 f565))) (define-fun f581 () Arctic (+ (* f102 f560) (* f103 f563) (* f104 f566))) (define-fun f582 () Arctic (+ (* f96 f570) (* f97 f571) (* f98 f572))) (define-fun f583 () Arctic (+ (* f99 f570) (* f100 f571) (* f101 f572))) (define-fun f584 () Arctic (+ (* f102 f570) (* f103 f571) (* f104 f572))) (define-fun f585 () Arctic (+ f105 f582)) (define-fun f586 () Arctic (+ f106 f583)) (define-fun f587 () Arctic (+ f107 f584)) (define-fun f588 () Arctic (+ (* f84 f60) (* f85 f63) (* f86 f66))) (define-fun f589 () Arctic (+ (* f84 f61) (* f85 f64) (* f86 f67))) (define-fun f590 () Arctic (+ (* f84 f62) (* f85 f65) (* f86 f68))) (define-fun f591 () Arctic (+ (* f87 f60) (* f88 f63) (* f89 f66))) (define-fun f592 () Arctic (+ (* f87 f61) (* f88 f64) (* f89 f67))) (define-fun f593 () Arctic (+ (* f87 f62) (* f88 f65) (* f89 f68))) (define-fun f594 () Arctic (+ (* f90 f60) (* f91 f63) (* f92 f66))) (define-fun f595 () Arctic (+ (* f90 f61) (* f91 f64) (* f92 f67))) (define-fun f596 () Arctic (+ (* f90 f62) (* f91 f65) (* f92 f68))) (define-fun f597 () Arctic (+ (* f84 f69) (* f85 f70) (* f86 f71))) (define-fun f598 () Arctic (+ (* f87 f69) (* f88 f70) (* f89 f71))) (define-fun f599 () Arctic (+ (* f90 f69) (* f91 f70) (* f92 f71))) (define-fun f600 () Arctic (+ f93 f597)) (define-fun f601 () Arctic (+ f94 f598)) (define-fun f602 () Arctic (+ f95 f599)) (define-fun f603 () Arctic (+ (* f84 f588) (* f85 f591) (* f86 f594))) (define-fun f604 () Arctic (+ (* f84 f589) (* f85 f592) (* f86 f595))) (define-fun f605 () Arctic (+ (* f84 f590) (* f85 f593) (* f86 f596))) (define-fun f606 () Arctic (+ (* f87 f588) (* f88 f591) (* f89 f594))) (define-fun f607 () Arctic (+ (* f87 f589) (* f88 f592) (* f89 f595))) (define-fun f608 () Arctic (+ (* f87 f590) (* f88 f593) (* f89 f596))) (define-fun f609 () Arctic (+ (* f90 f588) (* f91 f591) (* f92 f594))) (define-fun f610 () Arctic (+ (* f90 f589) (* f91 f592) (* f92 f595))) (define-fun f611 () Arctic (+ (* f90 f590) (* f91 f593) (* f92 f596))) (define-fun f612 () Arctic (+ (* f84 f600) (* f85 f601) (* f86 f602))) (define-fun f613 () Arctic (+ (* f87 f600) (* f88 f601) (* f89 f602))) (define-fun f614 () Arctic (+ (* f90 f600) (* f91 f601) (* f92 f602))) (define-fun f615 () Arctic (+ f93 f612)) (define-fun f616 () Arctic (+ f94 f613)) (define-fun f617 () Arctic (+ f95 f614)) (assert (and (and (and (and (>= f108 f138) (>= f109 f139) (>= f110 f140)) (and (>= f111 f141) (>= f112 f142) (>= f113 f143)) (and (>= f114 f144) (>= f115 f145) (>= f116 f146))) (and (and (>= f120 f150)) (and (>= f121 f151)) (and (>= f122 f152)))) (and (and (and (>= f0 f153) (>= f1 f154) (>= f2 f155)) (and (>= f3 f156) (>= f4 f157) (>= f5 f158)) (and (>= f6 f159) (>= f7 f160) (>= f8 f161))) (and (and (>= f9 f165)) (and (>= f10 f166)) (and (>= f11 f167)))) (and (and (and (>= f168 f198) (>= f169 f199) (>= f170 f200)) (and (>= f171 f201) (>= f172 f202) (>= f173 f203)) (and (>= f174 f204) (>= f175 f205) (>= f176 f206))) (and (and (>= f180 f210)) (and (>= f181 f211)) (and (>= f182 f212)))) (and (and (and (>= f213 f243) (>= f214 f244) (>= f215 f245)) (and (>= f216 f246) (>= f217 f247) (>= f218 f248)) (and (>= f219 f249) (>= f220 f250) (>= f221 f251))) (and (and (>= f225 f255)) (and (>= f226 f256)) (and (>= f227 f257)))) (and (and (and (>= f273 f0) (>= f274 f1) (>= f275 f2)) (and (>= f276 f3) (>= f277 f4) (>= f278 f5)) (and (>= f279 f6) (>= f280 f7) (>= f281 f8))) (and (and (>= f285 f9)) (and (>= f286 f10)) (and (>= f287 f11)))) (and (and (and (>= f288 f318) (>= f289 f319) (>= f290 f320)) (and (>= f291 f321) (>= f292 f322) (>= f293 f323)) (and (>= f294 f324) (>= f295 f325) (>= f296 f326))) (and (and (>= f300 f330)) (and (>= f301 f331)) (and (>= f302 f332)))) (and (and (and (>= f12 f333) (>= f13 f334) (>= f14 f335)) (and (>= f15 f336) (>= f16 f337) (>= f17 f338)) (and (>= f18 f339) (>= f19 f340) (>= f20 f341))) (and (and (>= f21 f345)) (and (>= f22 f346)) (and (>= f23 f347)))) (and (and (and (>= f348 f378) (>= f349 f379) (>= f350 f380)) (and (>= f351 f381) (>= f352 f382) (>= f353 f383)) (and (>= f354 f384) (>= f355 f385) (>= f356 f386))) (and (and (>= f360 f390)) (and (>= f361 f391)) (and (>= f362 f392)))) (and (and (and (>= f393 f423) (>= f394 f424) (>= f395 f425)) (and (>= f396 f426) (>= f397 f427) (>= f398 f428)) (and (>= f399 f429) (>= f400 f430) (>= f401 f431))) (and (and (>= f405 f435)) (and (>= f406 f436)) (and (>= f407 f437)))) (and (and (and (>= f438 f498) (>= f439 f499) (>= f440 f500)) (and (>= f441 f501) (>= f442 f502) (>= f443 f503)) (and (>= f444 f504) (>= f445 f505) (>= f446 f506))) (and (and (>= f450 f510)) (and (>= f451 f511)) (and (>= f452 f512)))) (and (and (and (>= f36 f513) (>= f37 f514) (>= f38 f515)) (and (>= f39 f516) (>= f40 f517) (>= f41 f518)) (and (>= f42 f519) (>= f43 f520) (>= f44 f521))) (and (and (>= f45 f525)) (and (>= f46 f526)) (and (>= f47 f527)))) (and (and (and (>= f528 f573) (>= f529 f574) (>= f530 f575)) (and (>= f531 f576) (>= f532 f577) (>= f533 f578)) (and (>= f534 f579) (>= f535 f580) (>= f536 f581))) (and (and (>= f540 f585)) (and (>= f541 f586)) (and (>= f542 f587)))) (and (and (and (>= f603 f12) (>= f604 f13) (>= f605 f14)) (and (>= f606 f15) (>= f607 f16) (>= f608 f17)) (and (>= f609 f18) (>= f610 f19) (>= f611 f20))) (and (and (>= f615 f21)) (and (>= f616 f22)) (and (>= f617 f23)))))) (assert (or (and (and (and (>> f108 f138) (>> f109 f139) (>> f110 f140)) (and (>> f111 f141) (>> f112 f142) (>> f113 f143)) (and (>> f114 f144) (>> f115 f145) (>> f116 f146))) (and (and (>> f120 f150)) (and (>> f121 f151)) (and (>> f122 f152)))) (and (and (and (>> f0 f153) (>> f1 f154) (>> f2 f155)) (and (>> f3 f156) (>> f4 f157) (>> f5 f158)) (and (>> f6 f159) (>> f7 f160) (>> f8 f161))) (and (and (>> f9 f165)) (and (>> f10 f166)) (and (>> f11 f167)))) (and (and (and (>> f168 f198) (>> f169 f199) (>> f170 f200)) (and (>> f171 f201) (>> f172 f202) (>> f173 f203)) (and (>> f174 f204) (>> f175 f205) (>> f176 f206))) (and (and (>> f180 f210)) (and (>> f181 f211)) (and (>> f182 f212)))) (and (and (and (>> f213 f243) (>> f214 f244) (>> f215 f245)) (and (>> f216 f246) (>> f217 f247) (>> f218 f248)) (and (>> f219 f249) (>> f220 f250) (>> f221 f251))) (and (and (>> f225 f255)) (and (>> f226 f256)) (and (>> f227 f257)))) (and (and (and (>> f273 f0) (>> f274 f1) (>> f275 f2)) (and (>> f276 f3) (>> f277 f4) (>> f278 f5)) (and (>> f279 f6) (>> f280 f7) (>> f281 f8))) (and (and (>> f285 f9)) (and (>> f286 f10)) (and (>> f287 f11)))))) (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 f360 f361 f362 f363 f364 f365 f366 f367 f368 f369 f370 f371 f372 f373 f374 f375 f376 f377 f378 f379 f380 f381 f382 f383 f384 f385 f386 f387 f388 f389 f390 f391 f392 f393 f394 f395 f396 f397 f398 f399 f400 f401 f402 f403 f404 f405 f406 f407 f408 f409 f410 f411 f412 f413 f414 f415 f416 f417 f418 f419 f420 f421 f422 f423 f424 f425 f426 f427 f428 f429 f430 f431 f432 f433 f434 f435 f436 f437 f438 f439 f440 f441 f442 f443 f444 f445 f446 f447 f448 f449 f450 f451 f452 f453 f454 f455 f456 f457 f458 f459 f460 f461 f462 f463 f464 f465 f466 f467 f468 f469 f470 f471 f472 f473 f474 f475 f476 f477 f478 f479 f480 f481 f482 f483 f484 f485 f486 f487 f488 f489 f490 f491 f492 f493 f494 f495 f496 f497 f498 f499 f500 f501 f502 f503 f504 f505 f506 f507 f508 f509 f510 f511 f512 f513 f514 f515 f516 f517 f518 f519 f520 f521 f522 f523 f524 f525 f526 f527 f528 f529 f530 f531 f532 f533 f534 f535 f536 f537 f538 f539 f540 f541 f542 f543 f544 f545 f546 f547 f548 f549 f550 f551 f552 f553 f554 f555 f556 f557 f558 f559 f560 f561 f562 f563 f564 f565 f566 f567 f568 f569 f570 f571 f572 f573 f574 f575 f576 f577 f578 f579 f580 f581 f582 f583 f584 f585 f586 f587 f588 f589 f590 f591 f592 f593 f594 f595 f596 f597 f598 f599 f600 f601 f602 f603 f604 f605 f606 f607 f608 f609 f610 f611 f612 f613 f614 f615 f616 f617))