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