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