(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES a# a b -> b# a a a, b# a b a -> a# b b, b# a b a -> b# b, a a b ->= b a a a, b a b a ->= a b b) by arctic matrix interpretation with dimension 5|) (declare-fun f0 () Arctic) (declare-fun f1 () Arctic) (declare-fun f2 () Arctic) (declare-fun f3 () Arctic) (declare-fun f4 () Arctic) (declare-fun f5 () Arctic) (declare-fun f6 () Arctic) (declare-fun f7 () Arctic) (declare-fun f8 () Arctic) (declare-fun f9 () Arctic) (declare-fun f10 () Arctic) (declare-fun f11 () Arctic) (declare-fun f12 () Arctic) (declare-fun f13 () Arctic) (declare-fun f14 () Arctic) (declare-fun f15 () Arctic) (declare-fun f16 () Arctic) (declare-fun f17 () Arctic) (declare-fun f18 () Arctic) (declare-fun f19 () Arctic) (declare-fun f20 () Arctic) (declare-fun f21 () Arctic) (declare-fun f22 () Arctic) (declare-fun f23 () Arctic) (declare-fun f24 () Arctic) (declare-fun f25 () Arctic) (declare-fun f26 () Arctic) (declare-fun f27 () Arctic) (declare-fun f28 () Arctic) (declare-fun f29 () Arctic) (declare-fun f30 () Arctic) (declare-fun f31 () Arctic) (declare-fun f32 () Arctic) (declare-fun f33 () Arctic) (declare-fun f34 () Arctic) (declare-fun f35 () Arctic) (declare-fun f36 () Arctic) (declare-fun f37 () Arctic) (declare-fun f38 () Arctic) (declare-fun f39 () Arctic) (declare-fun f40 () Arctic) (declare-fun f41 () Arctic) (declare-fun f42 () Arctic) (declare-fun f43 () Arctic) (declare-fun f44 () Arctic) (declare-fun f45 () Arctic) (declare-fun f46 () Arctic) (declare-fun f47 () Arctic) (declare-fun f48 () Arctic) (declare-fun f49 () Arctic) (declare-fun f50 () Arctic) (declare-fun f51 () Arctic) (declare-fun f52 () Arctic) (declare-fun f53 () Arctic) (declare-fun f54 () Arctic) (declare-fun f55 () Arctic) (declare-fun f56 () Arctic) (declare-fun f57 () Arctic) (declare-fun f58 () Arctic) (declare-fun f59 () Arctic) (declare-fun f60 () Arctic) (declare-fun f61 () Arctic) (declare-fun f62 () Arctic) (declare-fun f63 () Arctic) (declare-fun f64 () Arctic) (declare-fun f65 () Arctic) (declare-fun f66 () Arctic) (declare-fun f67 () Arctic) (declare-fun f68 () Arctic) (declare-fun f69 () Arctic) (declare-fun f70 () Arctic) (declare-fun f71 () Arctic) (declare-fun f72 () Arctic) (declare-fun f73 () Arctic) (declare-fun f74 () Arctic) (declare-fun f75 () Arctic) (declare-fun f76 () Arctic) (declare-fun f77 () Arctic) (declare-fun f78 () Arctic) (declare-fun f79 () Arctic) (declare-fun f80 () Arctic) (declare-fun f81 () Arctic) (declare-fun f82 () Arctic) (declare-fun f83 () Arctic) (declare-fun f84 () Arctic) (declare-fun f85 () Arctic) (declare-fun f86 () Arctic) (declare-fun f87 () Arctic) (declare-fun f88 () Arctic) (declare-fun f89 () Arctic) (declare-fun f90 () Arctic) (declare-fun f91 () Arctic) (declare-fun f92 () Arctic) (declare-fun f93 () Arctic) (declare-fun f94 () Arctic) (declare-fun f95 () Arctic) (declare-fun f96 () Arctic) (declare-fun f97 () Arctic) (declare-fun f98 () Arctic) (declare-fun f99 () Arctic) (declare-fun f100 () Arctic) (declare-fun f101 () Arctic) (declare-fun f102 () Arctic) (declare-fun f103 () Arctic) (declare-fun f104 () Arctic) (declare-fun f105 () Arctic) (declare-fun f106 () Arctic) (declare-fun f107 () Arctic) (declare-fun f108 () Arctic) (declare-fun f109 () Arctic) (declare-fun f110 () Arctic) (declare-fun f111 () Arctic) (declare-fun f112 () Arctic) (declare-fun f113 () Arctic) (declare-fun f114 () Arctic) (declare-fun f115 () Arctic) (declare-fun f116 () Arctic) (declare-fun f117 () Arctic) (declare-fun f118 () Arctic) (declare-fun f119 () Arctic) (assert (and (or (finite f30) (finite f55)) (or (finite f60) (finite f85)) (or (finite f0) (finite f25)) (or (finite f90) (finite f115)))) (define-fun f120 () Arctic (+ (* f30 f60) (* f31 f65) (* f32 f70) (* f33 f75) (* f34 f80))) (define-fun f121 () Arctic (+ (* f30 f61) (* f31 f66) (* f32 f71) (* f33 f76) (* f34 f81))) (define-fun f122 () Arctic (+ (* f30 f62) (* f31 f67) (* f32 f72) (* f33 f77) (* f34 f82))) (define-fun f123 () Arctic (+ (* f30 f63) (* f31 f68) (* f32 f73) (* f33 f78) (* f34 f83))) (define-fun f124 () Arctic (+ (* f30 f64) (* f31 f69) (* f32 f74) (* f33 f79) (* f34 f84))) (define-fun f125 () Arctic (+ (* f35 f60) (* f36 f65) (* f37 f70) (* f38 f75) (* f39 f80))) (define-fun f126 () Arctic (+ (* f35 f61) (* f36 f66) (* f37 f71) (* f38 f76) (* f39 f81))) (define-fun f127 () Arctic (+ (* f35 f62) (* f36 f67) (* f37 f72) (* f38 f77) (* f39 f82))) (define-fun f128 () Arctic (+ (* f35 f63) (* f36 f68) (* f37 f73) (* f38 f78) (* f39 f83))) (define-fun f129 () Arctic (+ (* f35 f64) (* f36 f69) (* f37 f74) (* f38 f79) (* f39 f84))) (define-fun f130 () Arctic (+ (* f40 f60) (* f41 f65) (* f42 f70) (* f43 f75) (* f44 f80))) (define-fun f131 () Arctic (+ (* f40 f61) (* f41 f66) (* f42 f71) (* f43 f76) (* f44 f81))) (define-fun f132 () Arctic (+ (* f40 f62) (* f41 f67) (* f42 f72) (* f43 f77) (* f44 f82))) (define-fun f133 () Arctic (+ (* f40 f63) (* f41 f68) (* f42 f73) (* f43 f78) (* f44 f83))) (define-fun f134 () Arctic (+ (* f40 f64) (* f41 f69) (* f42 f74) (* f43 f79) (* f44 f84))) (define-fun f135 () Arctic (+ (* f45 f60) (* f46 f65) (* f47 f70) (* f48 f75) (* f49 f80))) (define-fun f136 () Arctic (+ (* f45 f61) (* f46 f66) (* f47 f71) (* f48 f76) (* f49 f81))) (define-fun f137 () Arctic (+ (* f45 f62) (* f46 f67) (* f47 f72) (* f48 f77) (* f49 f82))) (define-fun f138 () Arctic (+ (* f45 f63) (* f46 f68) (* f47 f73) (* f48 f78) (* f49 f83))) (define-fun f139 () Arctic (+ (* f45 f64) (* f46 f69) (* f47 f74) (* f48 f79) (* f49 f84))) (define-fun f140 () Arctic (+ (* f50 f60) (* f51 f65) (* f52 f70) (* f53 f75) (* f54 f80))) (define-fun f141 () Arctic (+ (* f50 f61) (* f51 f66) (* f52 f71) (* f53 f76) (* f54 f81))) (define-fun f142 () Arctic (+ (* f50 f62) (* f51 f67) (* f52 f72) (* f53 f77) (* f54 f82))) (define-fun f143 () Arctic (+ (* f50 f63) (* f51 f68) (* f52 f73) (* f53 f78) (* f54 f83))) (define-fun f144 () Arctic (+ (* f50 f64) (* f51 f69) (* f52 f74) (* f53 f79) (* f54 f84))) (define-fun f145 () Arctic (+ (* f30 f85) (* f31 f86) (* f32 f87) (* f33 f88) (* f34 f89))) (define-fun f146 () Arctic (+ (* f35 f85) (* f36 f86) (* f37 f87) (* f38 f88) (* f39 f89))) (define-fun f147 () Arctic (+ (* f40 f85) (* f41 f86) (* f42 f87) (* f43 f88) (* f44 f89))) (define-fun f148 () Arctic (+ (* f45 f85) (* f46 f86) (* f47 f87) (* f48 f88) (* f49 f89))) (define-fun f149 () Arctic (+ (* f50 f85) (* f51 f86) (* f52 f87) (* f53 f88) (* f54 f89))) (define-fun f150 () Arctic (+ f55 f145)) (define-fun f151 () Arctic (+ f56 f146)) (define-fun f152 () Arctic (+ f57 f147)) (define-fun f153 () Arctic (+ f58 f148)) (define-fun f154 () Arctic (+ f59 f149)) (define-fun f155 () Arctic (+ (* f0 f120) (* f1 f125) (* f2 f130) (* f3 f135) (* f4 f140))) (define-fun f156 () Arctic (+ (* f0 f121) (* f1 f126) (* f2 f131) (* f3 f136) (* f4 f141))) (define-fun f157 () Arctic (+ (* f0 f122) (* f1 f127) (* f2 f132) (* f3 f137) (* f4 f142))) (define-fun f158 () Arctic (+ (* f0 f123) (* f1 f128) (* f2 f133) (* f3 f138) (* f4 f143))) (define-fun f159 () Arctic (+ (* f0 f124) (* f1 f129) (* f2 f134) (* f3 f139) (* f4 f144))) (define-fun f160 () Arctic (+ (* f5 f120) (* f6 f125) (* f7 f130) (* f8 f135) (* f9 f140))) (define-fun f161 () Arctic (+ (* f5 f121) (* f6 f126) (* f7 f131) (* f8 f136) (* f9 f141))) (define-fun f162 () Arctic (+ (* f5 f122) (* f6 f127) (* f7 f132) (* f8 f137) (* f9 f142))) (define-fun f163 () Arctic (+ (* f5 f123) (* f6 f128) (* f7 f133) (* f8 f138) (* f9 f143))) (define-fun f164 () Arctic (+ (* f5 f124) (* f6 f129) (* f7 f134) (* f8 f139) (* f9 f144))) (define-fun f165 () Arctic (+ (* f10 f120) (* f11 f125) (* f12 f130) (* f13 f135) (* f14 f140))) (define-fun f166 () Arctic (+ (* f10 f121) (* f11 f126) (* f12 f131) (* f13 f136) (* f14 f141))) (define-fun f167 () Arctic (+ (* f10 f122) (* f11 f127) (* f12 f132) (* f13 f137) (* f14 f142))) (define-fun f168 () Arctic (+ (* f10 f123) (* f11 f128) (* f12 f133) (* f13 f138) (* f14 f143))) (define-fun f169 () Arctic (+ (* f10 f124) (* f11 f129) (* f12 f134) (* f13 f139) (* f14 f144))) (define-fun f170 () Arctic (+ (* f15 f120) (* f16 f125) (* f17 f130) (* f18 f135) (* f19 f140))) (define-fun f171 () Arctic (+ (* f15 f121) (* f16 f126) (* f17 f131) (* f18 f136) (* f19 f141))) (define-fun f172 () Arctic (+ (* f15 f122) (* f16 f127) (* f17 f132) (* f18 f137) (* f19 f142))) (define-fun f173 () Arctic (+ (* f15 f123) (* f16 f128) (* f17 f133) (* f18 f138) (* f19 f143))) (define-fun f174 () Arctic (+ (* f15 f124) (* f16 f129) (* f17 f134) (* f18 f139) (* f19 f144))) (define-fun f175 () Arctic (+ (* f20 f120) (* f21 f125) (* f22 f130) (* f23 f135) (* f24 f140))) (define-fun f176 () Arctic (+ (* f20 f121) (* f21 f126) (* f22 f131) (* f23 f136) (* f24 f141))) (define-fun f177 () Arctic (+ (* f20 f122) (* f21 f127) (* f22 f132) (* f23 f137) (* f24 f142))) (define-fun f178 () Arctic (+ (* f20 f123) (* f21 f128) (* f22 f133) (* f23 f138) (* f24 f143))) (define-fun f179 () Arctic (+ (* f20 f124) (* f21 f129) (* f22 f134) (* f23 f139) (* f24 f144))) (define-fun f180 () Arctic (+ (* f0 f150) (* f1 f151) (* f2 f152) (* f3 f153) (* f4 f154))) (define-fun f181 () Arctic (+ (* f5 f150) (* f6 f151) (* f7 f152) (* f8 f153) (* f9 f154))) (define-fun f182 () Arctic (+ (* f10 f150) (* f11 f151) (* f12 f152) (* f13 f153) (* f14 f154))) (define-fun f183 () Arctic (+ (* f15 f150) (* f16 f151) (* f17 f152) (* f18 f153) (* f19 f154))) (define-fun f184 () Arctic (+ (* f20 f150) (* f21 f151) (* f22 f152) (* f23 f153) (* f24 f154))) (define-fun f185 () Arctic (+ f25 f180)) (define-fun f186 () Arctic (+ f26 f181)) (define-fun f187 () Arctic (+ f27 f182)) (define-fun f188 () Arctic (+ f28 f183)) (define-fun f189 () Arctic (+ f29 f184)) (define-fun f190 () Arctic (+ (* f30 f30) (* f31 f35) (* f32 f40) (* f33 f45) (* f34 f50))) (define-fun f191 () Arctic (+ (* f30 f31) (* f31 f36) (* f32 f41) (* f33 f46) (* f34 f51))) (define-fun f192 () Arctic (+ (* f30 f32) (* f31 f37) (* f32 f42) (* f33 f47) (* f34 f52))) (define-fun f193 () Arctic (+ (* f30 f33) (* f31 f38) (* f32 f43) (* f33 f48) (* f34 f53))) (define-fun f194 () Arctic (+ (* f30 f34) (* f31 f39) (* f32 f44) (* f33 f49) (* f34 f54))) (define-fun f195 () Arctic (+ (* f35 f30) (* f36 f35) (* f37 f40) (* f38 f45) (* f39 f50))) (define-fun f196 () Arctic (+ (* f35 f31) (* f36 f36) (* f37 f41) (* f38 f46) (* f39 f51))) (define-fun f197 () Arctic (+ (* f35 f32) (* f36 f37) (* f37 f42) (* f38 f47) (* f39 f52))) (define-fun f198 () Arctic (+ (* f35 f33) (* f36 f38) (* f37 f43) (* f38 f48) (* f39 f53))) (define-fun f199 () Arctic (+ (* f35 f34) (* f36 f39) (* f37 f44) (* f38 f49) (* f39 f54))) (define-fun f200 () Arctic (+ (* f40 f30) (* f41 f35) (* f42 f40) (* f43 f45) (* f44 f50))) (define-fun f201 () Arctic (+ (* f40 f31) (* f41 f36) (* f42 f41) (* f43 f46) (* f44 f51))) (define-fun f202 () Arctic (+ (* f40 f32) (* f41 f37) (* f42 f42) (* f43 f47) (* f44 f52))) (define-fun f203 () Arctic (+ (* f40 f33) (* f41 f38) (* f42 f43) (* f43 f48) (* f44 f53))) (define-fun f204 () Arctic (+ (* f40 f34) (* f41 f39) (* f42 f44) (* f43 f49) (* f44 f54))) (define-fun f205 () Arctic (+ (* f45 f30) (* f46 f35) (* f47 f40) (* f48 f45) (* f49 f50))) (define-fun f206 () Arctic (+ (* f45 f31) (* f46 f36) (* f47 f41) (* f48 f46) (* f49 f51))) (define-fun f207 () Arctic (+ (* f45 f32) (* f46 f37) (* f47 f42) (* f48 f47) (* f49 f52))) (define-fun f208 () Arctic (+ (* f45 f33) (* f46 f38) (* f47 f43) (* f48 f48) (* f49 f53))) (define-fun f209 () Arctic (+ (* f45 f34) (* f46 f39) (* f47 f44) (* f48 f49) (* f49 f54))) (define-fun f210 () Arctic (+ (* f50 f30) (* f51 f35) (* f52 f40) (* f53 f45) (* f54 f50))) (define-fun f211 () Arctic (+ (* f50 f31) (* f51 f36) (* f52 f41) (* f53 f46) (* f54 f51))) (define-fun f212 () Arctic (+ (* f50 f32) (* f51 f37) (* f52 f42) (* f53 f47) (* f54 f52))) (define-fun f213 () Arctic (+ (* f50 f33) (* f51 f38) (* f52 f43) (* f53 f48) (* f54 f53))) (define-fun f214 () Arctic (+ (* f50 f34) (* f51 f39) (* f52 f44) (* f53 f49) (* f54 f54))) (define-fun f215 () Arctic (+ (* f30 f55) (* f31 f56) (* f32 f57) (* f33 f58) (* f34 f59))) (define-fun f216 () Arctic (+ (* f35 f55) (* f36 f56) (* f37 f57) (* f38 f58) (* f39 f59))) (define-fun f217 () Arctic (+ (* f40 f55) (* f41 f56) (* f42 f57) (* f43 f58) (* f44 f59))) (define-fun f218 () Arctic (+ (* f45 f55) (* f46 f56) (* f47 f57) (* f48 f58) (* f49 f59))) (define-fun f219 () Arctic (+ (* f50 f55) (* f51 f56) (* f52 f57) (* f53 f58) (* f54 f59))) (define-fun f220 () Arctic (+ f55 f215)) (define-fun f221 () Arctic (+ f56 f216)) (define-fun f222 () Arctic (+ f57 f217)) (define-fun f223 () Arctic (+ f58 f218)) (define-fun f224 () Arctic (+ f59 f219)) (define-fun f225 () Arctic (+ (* f30 f190) (* f31 f195) (* f32 f200) (* f33 f205) (* f34 f210))) (define-fun f226 () Arctic (+ (* f30 f191) (* f31 f196) (* f32 f201) (* f33 f206) (* f34 f211))) (define-fun f227 () Arctic (+ (* f30 f192) (* f31 f197) (* f32 f202) (* f33 f207) (* f34 f212))) (define-fun f228 () Arctic (+ (* f30 f193) (* f31 f198) (* f32 f203) (* f33 f208) (* f34 f213))) (define-fun f229 () Arctic (+ (* f30 f194) (* f31 f199) (* f32 f204) (* f33 f209) (* f34 f214))) (define-fun f230 () Arctic (+ (* f35 f190) (* f36 f195) (* f37 f200) (* f38 f205) (* f39 f210))) (define-fun f231 () Arctic (+ (* f35 f191) (* f36 f196) (* f37 f201) (* f38 f206) (* f39 f211))) (define-fun f232 () Arctic (+ (* f35 f192) (* f36 f197) (* f37 f202) (* f38 f207) (* f39 f212))) (define-fun f233 () Arctic (+ (* f35 f193) (* f36 f198) (* f37 f203) (* f38 f208) (* f39 f213))) (define-fun f234 () Arctic (+ (* f35 f194) (* f36 f199) (* f37 f204) (* f38 f209) (* f39 f214))) (define-fun f235 () Arctic (+ (* f40 f190) (* f41 f195) (* f42 f200) (* f43 f205) (* f44 f210))) (define-fun f236 () Arctic (+ (* f40 f191) (* f41 f196) (* f42 f201) (* f43 f206) (* f44 f211))) (define-fun f237 () Arctic (+ (* f40 f192) (* f41 f197) (* f42 f202) (* f43 f207) (* f44 f212))) (define-fun f238 () Arctic (+ (* f40 f193) (* f41 f198) (* f42 f203) (* f43 f208) (* f44 f213))) (define-fun f239 () Arctic (+ (* f40 f194) (* f41 f199) (* f42 f204) (* f43 f209) (* f44 f214))) (define-fun f240 () Arctic (+ (* f45 f190) (* f46 f195) (* f47 f200) (* f48 f205) (* f49 f210))) (define-fun f241 () Arctic (+ (* f45 f191) (* f46 f196) (* f47 f201) (* f48 f206) (* f49 f211))) (define-fun f242 () Arctic (+ (* f45 f192) (* f46 f197) (* f47 f202) (* f48 f207) (* f49 f212))) (define-fun f243 () Arctic (+ (* f45 f193) (* f46 f198) (* f47 f203) (* f48 f208) (* f49 f213))) (define-fun f244 () Arctic (+ (* f45 f194) (* f46 f199) (* f47 f204) (* f48 f209) (* f49 f214))) (define-fun f245 () Arctic (+ (* f50 f190) (* f51 f195) (* f52 f200) (* f53 f205) (* f54 f210))) (define-fun f246 () Arctic (+ (* f50 f191) (* f51 f196) (* f52 f201) (* f53 f206) (* f54 f211))) (define-fun f247 () Arctic (+ (* f50 f192) (* f51 f197) (* f52 f202) (* f53 f207) (* f54 f212))) (define-fun f248 () Arctic (+ (* f50 f193) (* f51 f198) (* f52 f203) (* f53 f208) (* f54 f213))) (define-fun f249 () Arctic (+ (* f50 f194) (* f51 f199) (* f52 f204) (* f53 f209) (* f54 f214))) (define-fun f250 () Arctic (+ (* f30 f220) (* f31 f221) (* f32 f222) (* f33 f223) (* f34 f224))) (define-fun f251 () Arctic (+ (* f35 f220) (* f36 f221) (* f37 f222) (* f38 f223) (* f39 f224))) (define-fun f252 () Arctic (+ (* f40 f220) (* f41 f221) (* f42 f222) (* f43 f223) (* f44 f224))) (define-fun f253 () Arctic (+ (* f45 f220) (* f46 f221) (* f47 f222) (* f48 f223) (* f49 f224))) (define-fun f254 () Arctic (+ (* f50 f220) (* f51 f221) (* f52 f222) (* f53 f223) (* f54 f224))) (define-fun f255 () Arctic (+ f55 f250)) (define-fun f256 () Arctic (+ f56 f251)) (define-fun f257 () Arctic (+ f57 f252)) (define-fun f258 () Arctic (+ f58 f253)) (define-fun f259 () Arctic (+ f59 f254)) (define-fun f260 () Arctic (+ (* f90 f225) (* f91 f230) (* f92 f235) (* f93 f240) (* f94 f245))) (define-fun f261 () Arctic (+ (* f90 f226) (* f91 f231) (* f92 f236) (* f93 f241) (* f94 f246))) (define-fun f262 () Arctic (+ (* f90 f227) (* f91 f232) (* f92 f237) (* f93 f242) (* f94 f247))) (define-fun f263 () Arctic (+ (* f90 f228) (* f91 f233) (* f92 f238) (* f93 f243) (* f94 f248))) (define-fun f264 () Arctic (+ (* f90 f229) (* f91 f234) (* f92 f239) (* f93 f244) (* f94 f249))) (define-fun f265 () Arctic (+ (* f95 f225) (* f96 f230) (* f97 f235) (* f98 f240) (* f99 f245))) (define-fun f266 () Arctic (+ (* f95 f226) (* f96 f231) (* f97 f236) (* f98 f241) (* f99 f246))) (define-fun f267 () Arctic (+ (* f95 f227) (* f96 f232) (* f97 f237) (* f98 f242) (* f99 f247))) (define-fun f268 () Arctic (+ (* f95 f228) (* f96 f233) (* f97 f238) (* f98 f243) (* f99 f248))) (define-fun f269 () Arctic (+ (* f95 f229) (* f96 f234) (* f97 f239) (* f98 f244) (* f99 f249))) (define-fun f270 () Arctic (+ (* f100 f225) (* f101 f230) (* f102 f235) (* f103 f240) (* f104 f245))) (define-fun f271 () Arctic (+ (* f100 f226) (* f101 f231) (* f102 f236) (* f103 f241) (* f104 f246))) (define-fun f272 () Arctic (+ (* f100 f227) (* f101 f232) (* f102 f237) (* f103 f242) (* f104 f247))) (define-fun f273 () Arctic (+ (* f100 f228) (* f101 f233) (* f102 f238) (* f103 f243) (* f104 f248))) (define-fun f274 () Arctic (+ (* f100 f229) (* f101 f234) (* f102 f239) (* f103 f244) (* f104 f249))) (define-fun f275 () Arctic (+ (* f105 f225) (* f106 f230) (* f107 f235) (* f108 f240) (* f109 f245))) (define-fun f276 () Arctic (+ (* f105 f226) (* f106 f231) (* f107 f236) (* f108 f241) (* f109 f246))) (define-fun f277 () Arctic (+ (* f105 f227) (* f106 f232) (* f107 f237) (* f108 f242) (* f109 f247))) (define-fun f278 () Arctic (+ (* f105 f228) (* f106 f233) (* f107 f238) (* f108 f243) (* f109 f248))) (define-fun f279 () Arctic (+ (* f105 f229) (* f106 f234) (* f107 f239) (* f108 f244) (* f109 f249))) (define-fun f280 () Arctic (+ (* f110 f225) (* f111 f230) (* f112 f235) (* f113 f240) (* f114 f245))) (define-fun f281 () Arctic (+ (* f110 f226) (* f111 f231) (* f112 f236) (* f113 f241) (* f114 f246))) (define-fun f282 () Arctic (+ (* f110 f227) (* f111 f232) (* f112 f237) (* f113 f242) (* f114 f247))) (define-fun f283 () Arctic (+ (* f110 f228) (* f111 f233) (* f112 f238) (* f113 f243) (* f114 f248))) (define-fun f284 () Arctic (+ (* f110 f229) (* f111 f234) (* f112 f239) (* f113 f244) (* f114 f249))) (define-fun f285 () Arctic (+ (* f90 f255) (* f91 f256) (* f92 f257) (* f93 f258) (* f94 f259))) (define-fun f286 () Arctic (+ (* f95 f255) (* f96 f256) (* f97 f257) (* f98 f258) (* f99 f259))) (define-fun f287 () Arctic (+ (* f100 f255) (* f101 f256) (* f102 f257) (* f103 f258) (* f104 f259))) (define-fun f288 () Arctic (+ (* f105 f255) (* f106 f256) (* f107 f257) (* f108 f258) (* f109 f259))) (define-fun f289 () Arctic (+ (* f110 f255) (* f111 f256) (* f112 f257) (* f113 f258) (* f114 f259))) (define-fun f290 () Arctic (+ f115 f285)) (define-fun f291 () Arctic (+ f116 f286)) (define-fun f292 () Arctic (+ f117 f287)) (define-fun f293 () Arctic (+ f118 f288)) (define-fun f294 () Arctic (+ f119 f289)) (define-fun f295 () Arctic (+ (* f60 f30) (* f61 f35) (* f62 f40) (* f63 f45) (* f64 f50))) (define-fun f296 () Arctic (+ (* f60 f31) (* f61 f36) (* f62 f41) (* f63 f46) (* f64 f51))) (define-fun f297 () Arctic (+ (* f60 f32) (* f61 f37) (* f62 f42) (* f63 f47) (* f64 f52))) (define-fun f298 () Arctic (+ (* f60 f33) (* f61 f38) (* f62 f43) (* f63 f48) (* f64 f53))) (define-fun f299 () Arctic (+ (* f60 f34) (* f61 f39) (* f62 f44) (* f63 f49) (* f64 f54))) (define-fun f300 () Arctic (+ (* f65 f30) (* f66 f35) (* f67 f40) (* f68 f45) (* f69 f50))) (define-fun f301 () Arctic (+ (* f65 f31) (* f66 f36) (* f67 f41) (* f68 f46) (* f69 f51))) (define-fun f302 () Arctic (+ (* f65 f32) (* f66 f37) (* f67 f42) (* f68 f47) (* f69 f52))) (define-fun f303 () Arctic (+ (* f65 f33) (* f66 f38) (* f67 f43) (* f68 f48) (* f69 f53))) (define-fun f304 () Arctic (+ (* f65 f34) (* f66 f39) (* f67 f44) (* f68 f49) (* f69 f54))) (define-fun f305 () Arctic (+ (* f70 f30) (* f71 f35) (* f72 f40) (* f73 f45) (* f74 f50))) (define-fun f306 () Arctic (+ (* f70 f31) (* f71 f36) (* f72 f41) (* f73 f46) (* f74 f51))) (define-fun f307 () Arctic (+ (* f70 f32) (* f71 f37) (* f72 f42) (* f73 f47) (* f74 f52))) (define-fun f308 () Arctic (+ (* f70 f33) (* f71 f38) (* f72 f43) (* f73 f48) (* f74 f53))) (define-fun f309 () Arctic (+ (* f70 f34) (* f71 f39) (* f72 f44) (* f73 f49) (* f74 f54))) (define-fun f310 () Arctic (+ (* f75 f30) (* f76 f35) (* f77 f40) (* f78 f45) (* f79 f50))) (define-fun f311 () Arctic (+ (* f75 f31) (* f76 f36) (* f77 f41) (* f78 f46) (* f79 f51))) (define-fun f312 () Arctic (+ (* f75 f32) (* f76 f37) (* f77 f42) (* f78 f47) (* f79 f52))) (define-fun f313 () Arctic (+ (* f75 f33) (* f76 f38) (* f77 f43) (* f78 f48) (* f79 f53))) (define-fun f314 () Arctic (+ (* f75 f34) (* f76 f39) (* f77 f44) (* f78 f49) (* f79 f54))) (define-fun f315 () Arctic (+ (* f80 f30) (* f81 f35) (* f82 f40) (* f83 f45) (* f84 f50))) (define-fun f316 () Arctic (+ (* f80 f31) (* f81 f36) (* f82 f41) (* f83 f46) (* f84 f51))) (define-fun f317 () Arctic (+ (* f80 f32) (* f81 f37) (* f82 f42) (* f83 f47) (* f84 f52))) (define-fun f318 () Arctic (+ (* f80 f33) (* f81 f38) (* f82 f43) (* f83 f48) (* f84 f53))) (define-fun f319 () Arctic (+ (* f80 f34) (* f81 f39) (* f82 f44) (* f83 f49) (* f84 f54))) (define-fun f320 () Arctic (+ (* f60 f55) (* f61 f56) (* f62 f57) (* f63 f58) (* f64 f59))) (define-fun f321 () Arctic (+ (* f65 f55) (* f66 f56) (* f67 f57) (* f68 f58) (* f69 f59))) (define-fun f322 () Arctic (+ (* f70 f55) (* f71 f56) (* f72 f57) (* f73 f58) (* f74 f59))) (define-fun f323 () Arctic (+ (* f75 f55) (* f76 f56) (* f77 f57) (* f78 f58) (* f79 f59))) (define-fun f324 () Arctic (+ (* f80 f55) (* f81 f56) (* f82 f57) (* f83 f58) (* f84 f59))) (define-fun f325 () Arctic (+ f85 f320)) (define-fun f326 () Arctic (+ f86 f321)) (define-fun f327 () Arctic (+ f87 f322)) (define-fun f328 () Arctic (+ f88 f323)) (define-fun f329 () Arctic (+ f89 f324)) (define-fun f330 () Arctic (+ (* f30 f295) (* f31 f300) (* f32 f305) (* f33 f310) (* f34 f315))) (define-fun f331 () Arctic (+ (* f30 f296) (* f31 f301) (* f32 f306) (* f33 f311) (* f34 f316))) (define-fun f332 () Arctic (+ (* f30 f297) (* f31 f302) (* f32 f307) (* f33 f312) (* f34 f317))) (define-fun f333 () Arctic (+ (* f30 f298) (* f31 f303) (* f32 f308) (* f33 f313) (* f34 f318))) (define-fun f334 () Arctic (+ (* f30 f299) (* f31 f304) (* f32 f309) (* f33 f314) (* f34 f319))) (define-fun f335 () Arctic (+ (* f35 f295) (* f36 f300) (* f37 f305) (* f38 f310) (* f39 f315))) (define-fun f336 () Arctic (+ (* f35 f296) (* f36 f301) (* f37 f306) (* f38 f311) (* f39 f316))) (define-fun f337 () Arctic (+ (* f35 f297) (* f36 f302) (* f37 f307) (* f38 f312) (* f39 f317))) (define-fun f338 () Arctic (+ (* f35 f298) (* f36 f303) (* f37 f308) (* f38 f313) (* f39 f318))) (define-fun f339 () Arctic (+ (* f35 f299) (* f36 f304) (* f37 f309) (* f38 f314) (* f39 f319))) (define-fun f340 () Arctic (+ (* f40 f295) (* f41 f300) (* f42 f305) (* f43 f310) (* f44 f315))) (define-fun f341 () Arctic (+ (* f40 f296) (* f41 f301) (* f42 f306) (* f43 f311) (* f44 f316))) (define-fun f342 () Arctic (+ (* f40 f297) (* f41 f302) (* f42 f307) (* f43 f312) (* f44 f317))) (define-fun f343 () Arctic (+ (* f40 f298) (* f41 f303) (* f42 f308) (* f43 f313) (* f44 f318))) (define-fun f344 () Arctic (+ (* f40 f299) (* f41 f304) (* f42 f309) (* f43 f314) (* f44 f319))) (define-fun f345 () Arctic (+ (* f45 f295) (* f46 f300) (* f47 f305) (* f48 f310) (* f49 f315))) (define-fun f346 () Arctic (+ (* f45 f296) (* f46 f301) (* f47 f306) (* f48 f311) (* f49 f316))) (define-fun f347 () Arctic (+ (* f45 f297) (* f46 f302) (* f47 f307) (* f48 f312) (* f49 f317))) (define-fun f348 () Arctic (+ (* f45 f298) (* f46 f303) (* f47 f308) (* f48 f313) (* f49 f318))) (define-fun f349 () Arctic (+ (* f45 f299) (* f46 f304) (* f47 f309) (* f48 f314) (* f49 f319))) (define-fun f350 () Arctic (+ (* f50 f295) (* f51 f300) (* f52 f305) (* f53 f310) (* f54 f315))) (define-fun f351 () Arctic (+ (* f50 f296) (* f51 f301) (* f52 f306) (* f53 f311) (* f54 f316))) (define-fun f352 () Arctic (+ (* f50 f297) (* f51 f302) (* f52 f307) (* f53 f312) (* f54 f317))) (define-fun f353 () Arctic (+ (* f50 f298) (* f51 f303) (* f52 f308) (* f53 f313) (* f54 f318))) (define-fun f354 () Arctic (+ (* f50 f299) (* f51 f304) (* f52 f309) (* f53 f314) (* f54 f319))) (define-fun f355 () Arctic (+ (* f30 f325) (* f31 f326) (* f32 f327) (* f33 f328) (* f34 f329))) (define-fun f356 () Arctic (+ (* f35 f325) (* f36 f326) (* f37 f327) (* f38 f328) (* f39 f329))) (define-fun f357 () Arctic (+ (* f40 f325) (* f41 f326) (* f42 f327) (* f43 f328) (* f44 f329))) (define-fun f358 () Arctic (+ (* f45 f325) (* f46 f326) (* f47 f327) (* f48 f328) (* f49 f329))) (define-fun f359 () Arctic (+ (* f50 f325) (* f51 f326) (* f52 f327) (* f53 f328) (* f54 f329))) (define-fun f360 () Arctic (+ f55 f355)) (define-fun f361 () Arctic (+ f56 f356)) (define-fun f362 () Arctic (+ f57 f357)) (define-fun f363 () Arctic (+ f58 f358)) (define-fun f364 () Arctic (+ f59 f359)) (define-fun f365 () Arctic (+ (* f90 f330) (* f91 f335) (* f92 f340) (* f93 f345) (* f94 f350))) (define-fun f366 () Arctic (+ (* f90 f331) (* f91 f336) (* f92 f341) (* f93 f346) (* f94 f351))) (define-fun f367 () Arctic (+ (* f90 f332) (* f91 f337) (* f92 f342) (* f93 f347) (* f94 f352))) (define-fun f368 () Arctic (+ (* f90 f333) (* f91 f338) (* f92 f343) (* f93 f348) (* f94 f353))) (define-fun f369 () Arctic (+ (* f90 f334) (* f91 f339) (* f92 f344) (* f93 f349) (* f94 f354))) (define-fun f370 () Arctic (+ (* f95 f330) (* f96 f335) (* f97 f340) (* f98 f345) (* f99 f350))) (define-fun f371 () Arctic (+ (* f95 f331) (* f96 f336) (* f97 f341) (* f98 f346) (* f99 f351))) (define-fun f372 () Arctic (+ (* f95 f332) (* f96 f337) (* f97 f342) (* f98 f347) (* f99 f352))) (define-fun f373 () Arctic (+ (* f95 f333) (* f96 f338) (* f97 f343) (* f98 f348) (* f99 f353))) (define-fun f374 () Arctic (+ (* f95 f334) (* f96 f339) (* f97 f344) (* f98 f349) (* f99 f354))) (define-fun f375 () Arctic (+ (* f100 f330) (* f101 f335) (* f102 f340) (* f103 f345) (* f104 f350))) (define-fun f376 () Arctic (+ (* f100 f331) (* f101 f336) (* f102 f341) (* f103 f346) (* f104 f351))) (define-fun f377 () Arctic (+ (* f100 f332) (* f101 f337) (* f102 f342) (* f103 f347) (* f104 f352))) (define-fun f378 () Arctic (+ (* f100 f333) (* f101 f338) (* f102 f343) (* f103 f348) (* f104 f353))) (define-fun f379 () Arctic (+ (* f100 f334) (* f101 f339) (* f102 f344) (* f103 f349) (* f104 f354))) (define-fun f380 () Arctic (+ (* f105 f330) (* f106 f335) (* f107 f340) (* f108 f345) (* f109 f350))) (define-fun f381 () Arctic (+ (* f105 f331) (* f106 f336) (* f107 f341) (* f108 f346) (* f109 f351))) (define-fun f382 () Arctic (+ (* f105 f332) (* f106 f337) (* f107 f342) (* f108 f347) (* f109 f352))) (define-fun f383 () Arctic (+ (* f105 f333) (* f106 f338) (* f107 f343) (* f108 f348) (* f109 f353))) (define-fun f384 () Arctic (+ (* f105 f334) (* f106 f339) (* f107 f344) (* f108 f349) (* f109 f354))) (define-fun f385 () Arctic (+ (* f110 f330) (* f111 f335) (* f112 f340) (* f113 f345) (* f114 f350))) (define-fun f386 () Arctic (+ (* f110 f331) (* f111 f336) (* f112 f341) (* f113 f346) (* f114 f351))) (define-fun f387 () Arctic (+ (* f110 f332) (* f111 f337) (* f112 f342) (* f113 f347) (* f114 f352))) (define-fun f388 () Arctic (+ (* f110 f333) (* f111 f338) (* f112 f343) (* f113 f348) (* f114 f353))) (define-fun f389 () Arctic (+ (* f110 f334) (* f111 f339) (* f112 f344) (* f113 f349) (* f114 f354))) (define-fun f390 () Arctic (+ (* f90 f360) (* f91 f361) (* f92 f362) (* f93 f363) (* f94 f364))) (define-fun f391 () Arctic (+ (* f95 f360) (* f96 f361) (* f97 f362) (* f98 f363) (* f99 f364))) (define-fun f392 () Arctic (+ (* f100 f360) (* f101 f361) (* f102 f362) (* f103 f363) (* f104 f364))) (define-fun f393 () Arctic (+ (* f105 f360) (* f106 f361) (* f107 f362) (* f108 f363) (* f109 f364))) (define-fun f394 () Arctic (+ (* f110 f360) (* f111 f361) (* f112 f362) (* f113 f363) (* f114 f364))) (define-fun f395 () Arctic (+ f115 f390)) (define-fun f396 () Arctic (+ f116 f391)) (define-fun f397 () Arctic (+ f117 f392)) (define-fun f398 () Arctic (+ f118 f393)) (define-fun f399 () Arctic (+ f119 f394)) (define-fun f400 () Arctic (+ (* f60 f60) (* f61 f65) (* f62 f70) (* f63 f75) (* f64 f80))) (define-fun f401 () Arctic (+ (* f60 f61) (* f61 f66) (* f62 f71) (* f63 f76) (* f64 f81))) (define-fun f402 () Arctic (+ (* f60 f62) (* f61 f67) (* f62 f72) (* f63 f77) (* f64 f82))) (define-fun f403 () Arctic (+ (* f60 f63) (* f61 f68) (* f62 f73) (* f63 f78) (* f64 f83))) (define-fun f404 () Arctic (+ (* f60 f64) (* f61 f69) (* f62 f74) (* f63 f79) (* f64 f84))) (define-fun f405 () Arctic (+ (* f65 f60) (* f66 f65) (* f67 f70) (* f68 f75) (* f69 f80))) (define-fun f406 () Arctic (+ (* f65 f61) (* f66 f66) (* f67 f71) (* f68 f76) (* f69 f81))) (define-fun f407 () Arctic (+ (* f65 f62) (* f66 f67) (* f67 f72) (* f68 f77) (* f69 f82))) (define-fun f408 () Arctic (+ (* f65 f63) (* f66 f68) (* f67 f73) (* f68 f78) (* f69 f83))) (define-fun f409 () Arctic (+ (* f65 f64) (* f66 f69) (* f67 f74) (* f68 f79) (* f69 f84))) (define-fun f410 () Arctic (+ (* f70 f60) (* f71 f65) (* f72 f70) (* f73 f75) (* f74 f80))) (define-fun f411 () Arctic (+ (* f70 f61) (* f71 f66) (* f72 f71) (* f73 f76) (* f74 f81))) (define-fun f412 () Arctic (+ (* f70 f62) (* f71 f67) (* f72 f72) (* f73 f77) (* f74 f82))) (define-fun f413 () Arctic (+ (* f70 f63) (* f71 f68) (* f72 f73) (* f73 f78) (* f74 f83))) (define-fun f414 () Arctic (+ (* f70 f64) (* f71 f69) (* f72 f74) (* f73 f79) (* f74 f84))) (define-fun f415 () Arctic (+ (* f75 f60) (* f76 f65) (* f77 f70) (* f78 f75) (* f79 f80))) (define-fun f416 () Arctic (+ (* f75 f61) (* f76 f66) (* f77 f71) (* f78 f76) (* f79 f81))) (define-fun f417 () Arctic (+ (* f75 f62) (* f76 f67) (* f77 f72) (* f78 f77) (* f79 f82))) (define-fun f418 () Arctic (+ (* f75 f63) (* f76 f68) (* f77 f73) (* f78 f78) (* f79 f83))) (define-fun f419 () Arctic (+ (* f75 f64) (* f76 f69) (* f77 f74) (* f78 f79) (* f79 f84))) (define-fun f420 () Arctic (+ (* f80 f60) (* f81 f65) (* f82 f70) (* f83 f75) (* f84 f80))) (define-fun f421 () Arctic (+ (* f80 f61) (* f81 f66) (* f82 f71) (* f83 f76) (* f84 f81))) (define-fun f422 () Arctic (+ (* f80 f62) (* f81 f67) (* f82 f72) (* f83 f77) (* f84 f82))) (define-fun f423 () Arctic (+ (* f80 f63) (* f81 f68) (* f82 f73) (* f83 f78) (* f84 f83))) (define-fun f424 () Arctic (+ (* f80 f64) (* f81 f69) (* f82 f74) (* f83 f79) (* f84 f84))) (define-fun f425 () Arctic (+ (* f60 f85) (* f61 f86) (* f62 f87) (* f63 f88) (* f64 f89))) (define-fun f426 () Arctic (+ (* f65 f85) (* f66 f86) (* f67 f87) (* f68 f88) (* f69 f89))) (define-fun f427 () Arctic (+ (* f70 f85) (* f71 f86) (* f72 f87) (* f73 f88) (* f74 f89))) (define-fun f428 () Arctic (+ (* f75 f85) (* f76 f86) (* f77 f87) (* f78 f88) (* f79 f89))) (define-fun f429 () Arctic (+ (* f80 f85) (* f81 f86) (* f82 f87) (* f83 f88) (* f84 f89))) (define-fun f430 () Arctic (+ f85 f425)) (define-fun f431 () Arctic (+ f86 f426)) (define-fun f432 () Arctic (+ f87 f427)) (define-fun f433 () Arctic (+ f88 f428)) (define-fun f434 () Arctic (+ f89 f429)) (define-fun f435 () Arctic (+ (* f0 f400) (* f1 f405) (* f2 f410) (* f3 f415) (* f4 f420))) (define-fun f436 () Arctic (+ (* f0 f401) (* f1 f406) (* f2 f411) (* f3 f416) (* f4 f421))) (define-fun f437 () Arctic (+ (* f0 f402) (* f1 f407) (* f2 f412) (* f3 f417) (* f4 f422))) (define-fun f438 () Arctic (+ (* f0 f403) (* f1 f408) (* f2 f413) (* f3 f418) (* f4 f423))) (define-fun f439 () Arctic (+ (* f0 f404) (* f1 f409) (* f2 f414) (* f3 f419) (* f4 f424))) (define-fun f440 () Arctic (+ (* f5 f400) (* f6 f405) (* f7 f410) (* f8 f415) (* f9 f420))) (define-fun f441 () Arctic (+ (* f5 f401) (* f6 f406) (* f7 f411) (* f8 f416) (* f9 f421))) (define-fun f442 () Arctic (+ (* f5 f402) (* f6 f407) (* f7 f412) (* f8 f417) (* f9 f422))) (define-fun f443 () Arctic (+ (* f5 f403) (* f6 f408) (* f7 f413) (* f8 f418) (* f9 f423))) (define-fun f444 () Arctic (+ (* f5 f404) (* f6 f409) (* f7 f414) (* f8 f419) (* f9 f424))) (define-fun f445 () Arctic (+ (* f10 f400) (* f11 f405) (* f12 f410) (* f13 f415) (* f14 f420))) (define-fun f446 () Arctic (+ (* f10 f401) (* f11 f406) (* f12 f411) (* f13 f416) (* f14 f421))) (define-fun f447 () Arctic (+ (* f10 f402) (* f11 f407) (* f12 f412) (* f13 f417) (* f14 f422))) (define-fun f448 () Arctic (+ (* f10 f403) (* f11 f408) (* f12 f413) (* f13 f418) (* f14 f423))) (define-fun f449 () Arctic (+ (* f10 f404) (* f11 f409) (* f12 f414) (* f13 f419) (* f14 f424))) (define-fun f450 () Arctic (+ (* f15 f400) (* f16 f405) (* f17 f410) (* f18 f415) (* f19 f420))) (define-fun f451 () Arctic (+ (* f15 f401) (* f16 f406) (* f17 f411) (* f18 f416) (* f19 f421))) (define-fun f452 () Arctic (+ (* f15 f402) (* f16 f407) (* f17 f412) (* f18 f417) (* f19 f422))) (define-fun f453 () Arctic (+ (* f15 f403) (* f16 f408) (* f17 f413) (* f18 f418) (* f19 f423))) (define-fun f454 () Arctic (+ (* f15 f404) (* f16 f409) (* f17 f414) (* f18 f419) (* f19 f424))) (define-fun f455 () Arctic (+ (* f20 f400) (* f21 f405) (* f22 f410) (* f23 f415) (* f24 f420))) (define-fun f456 () Arctic (+ (* f20 f401) (* f21 f406) (* f22 f411) (* f23 f416) (* f24 f421))) (define-fun f457 () Arctic (+ (* f20 f402) (* f21 f407) (* f22 f412) (* f23 f417) (* f24 f422))) (define-fun f458 () Arctic (+ (* f20 f403) (* f21 f408) (* f22 f413) (* f23 f418) (* f24 f423))) (define-fun f459 () Arctic (+ (* f20 f404) (* f21 f409) (* f22 f414) (* f23 f419) (* f24 f424))) (define-fun f460 () Arctic (+ (* f0 f430) (* f1 f431) (* f2 f432) (* f3 f433) (* f4 f434))) (define-fun f461 () Arctic (+ (* f5 f430) (* f6 f431) (* f7 f432) (* f8 f433) (* f9 f434))) (define-fun f462 () Arctic (+ (* f10 f430) (* f11 f431) (* f12 f432) (* f13 f433) (* f14 f434))) (define-fun f463 () Arctic (+ (* f15 f430) (* f16 f431) (* f17 f432) (* f18 f433) (* f19 f434))) (define-fun f464 () Arctic (+ (* f20 f430) (* f21 f431) (* f22 f432) (* f23 f433) (* f24 f434))) (define-fun f465 () Arctic (+ f25 f460)) (define-fun f466 () Arctic (+ f26 f461)) (define-fun f467 () Arctic (+ f27 f462)) (define-fun f468 () Arctic (+ f28 f463)) (define-fun f469 () Arctic (+ f29 f464)) (define-fun f470 () Arctic (+ (* f60 f30) (* f61 f35) (* f62 f40) (* f63 f45) (* f64 f50))) (define-fun f471 () Arctic (+ (* f60 f31) (* f61 f36) (* f62 f41) (* f63 f46) (* f64 f51))) (define-fun f472 () Arctic (+ (* f60 f32) (* f61 f37) (* f62 f42) (* f63 f47) (* f64 f52))) (define-fun f473 () Arctic (+ (* f60 f33) (* f61 f38) (* f62 f43) (* f63 f48) (* f64 f53))) (define-fun f474 () Arctic (+ (* f60 f34) (* f61 f39) (* f62 f44) (* f63 f49) (* f64 f54))) (define-fun f475 () Arctic (+ (* f65 f30) (* f66 f35) (* f67 f40) (* f68 f45) (* f69 f50))) (define-fun f476 () Arctic (+ (* f65 f31) (* f66 f36) (* f67 f41) (* f68 f46) (* f69 f51))) (define-fun f477 () Arctic (+ (* f65 f32) (* f66 f37) (* f67 f42) (* f68 f47) (* f69 f52))) (define-fun f478 () Arctic (+ (* f65 f33) (* f66 f38) (* f67 f43) (* f68 f48) (* f69 f53))) (define-fun f479 () Arctic (+ (* f65 f34) (* f66 f39) (* f67 f44) (* f68 f49) (* f69 f54))) (define-fun f480 () Arctic (+ (* f70 f30) (* f71 f35) (* f72 f40) (* f73 f45) (* f74 f50))) (define-fun f481 () Arctic (+ (* f70 f31) (* f71 f36) (* f72 f41) (* f73 f46) (* f74 f51))) (define-fun f482 () Arctic (+ (* f70 f32) (* f71 f37) (* f72 f42) (* f73 f47) (* f74 f52))) (define-fun f483 () Arctic (+ (* f70 f33) (* f71 f38) (* f72 f43) (* f73 f48) (* f74 f53))) (define-fun f484 () Arctic (+ (* f70 f34) (* f71 f39) (* f72 f44) (* f73 f49) (* f74 f54))) (define-fun f485 () Arctic (+ (* f75 f30) (* f76 f35) (* f77 f40) (* f78 f45) (* f79 f50))) (define-fun f486 () Arctic (+ (* f75 f31) (* f76 f36) (* f77 f41) (* f78 f46) (* f79 f51))) (define-fun f487 () Arctic (+ (* f75 f32) (* f76 f37) (* f77 f42) (* f78 f47) (* f79 f52))) (define-fun f488 () Arctic (+ (* f75 f33) (* f76 f38) (* f77 f43) (* f78 f48) (* f79 f53))) (define-fun f489 () Arctic (+ (* f75 f34) (* f76 f39) (* f77 f44) (* f78 f49) (* f79 f54))) (define-fun f490 () Arctic (+ (* f80 f30) (* f81 f35) (* f82 f40) (* f83 f45) (* f84 f50))) (define-fun f491 () Arctic (+ (* f80 f31) (* f81 f36) (* f82 f41) (* f83 f46) (* f84 f51))) (define-fun f492 () Arctic (+ (* f80 f32) (* f81 f37) (* f82 f42) (* f83 f47) (* f84 f52))) (define-fun f493 () Arctic (+ (* f80 f33) (* f81 f38) (* f82 f43) (* f83 f48) (* f84 f53))) (define-fun f494 () Arctic (+ (* f80 f34) (* f81 f39) (* f82 f44) (* f83 f49) (* f84 f54))) (define-fun f495 () Arctic (+ (* f60 f55) (* f61 f56) (* f62 f57) (* f63 f58) (* f64 f59))) (define-fun f496 () Arctic (+ (* f65 f55) (* f66 f56) (* f67 f57) (* f68 f58) (* f69 f59))) (define-fun f497 () Arctic (+ (* f70 f55) (* f71 f56) (* f72 f57) (* f73 f58) (* f74 f59))) (define-fun f498 () Arctic (+ (* f75 f55) (* f76 f56) (* f77 f57) (* f78 f58) (* f79 f59))) (define-fun f499 () Arctic (+ (* f80 f55) (* f81 f56) (* f82 f57) (* f83 f58) (* f84 f59))) (define-fun f500 () Arctic (+ f85 f495)) (define-fun f501 () Arctic (+ f86 f496)) (define-fun f502 () Arctic (+ f87 f497)) (define-fun f503 () Arctic (+ f88 f498)) (define-fun f504 () Arctic (+ f89 f499)) (define-fun f505 () Arctic (+ (* f30 f470) (* f31 f475) (* f32 f480) (* f33 f485) (* f34 f490))) (define-fun f506 () Arctic (+ (* f30 f471) (* f31 f476) (* f32 f481) (* f33 f486) (* f34 f491))) (define-fun f507 () Arctic (+ (* f30 f472) (* f31 f477) (* f32 f482) (* f33 f487) (* f34 f492))) (define-fun f508 () Arctic (+ (* f30 f473) (* f31 f478) (* f32 f483) (* f33 f488) (* f34 f493))) (define-fun f509 () Arctic (+ (* f30 f474) (* f31 f479) (* f32 f484) (* f33 f489) (* f34 f494))) (define-fun f510 () Arctic (+ (* f35 f470) (* f36 f475) (* f37 f480) (* f38 f485) (* f39 f490))) (define-fun f511 () Arctic (+ (* f35 f471) (* f36 f476) (* f37 f481) (* f38 f486) (* f39 f491))) (define-fun f512 () Arctic (+ (* f35 f472) (* f36 f477) (* f37 f482) (* f38 f487) (* f39 f492))) (define-fun f513 () Arctic (+ (* f35 f473) (* f36 f478) (* f37 f483) (* f38 f488) (* f39 f493))) (define-fun f514 () Arctic (+ (* f35 f474) (* f36 f479) (* f37 f484) (* f38 f489) (* f39 f494))) (define-fun f515 () Arctic (+ (* f40 f470) (* f41 f475) (* f42 f480) (* f43 f485) (* f44 f490))) (define-fun f516 () Arctic (+ (* f40 f471) (* f41 f476) (* f42 f481) (* f43 f486) (* f44 f491))) (define-fun f517 () Arctic (+ (* f40 f472) (* f41 f477) (* f42 f482) (* f43 f487) (* f44 f492))) (define-fun f518 () Arctic (+ (* f40 f473) (* f41 f478) (* f42 f483) (* f43 f488) (* f44 f493))) (define-fun f519 () Arctic (+ (* f40 f474) (* f41 f479) (* f42 f484) (* f43 f489) (* f44 f494))) (define-fun f520 () Arctic (+ (* f45 f470) (* f46 f475) (* f47 f480) (* f48 f485) (* f49 f490))) (define-fun f521 () Arctic (+ (* f45 f471) (* f46 f476) (* f47 f481) (* f48 f486) (* f49 f491))) (define-fun f522 () Arctic (+ (* f45 f472) (* f46 f477) (* f47 f482) (* f48 f487) (* f49 f492))) (define-fun f523 () Arctic (+ (* f45 f473) (* f46 f478) (* f47 f483) (* f48 f488) (* f49 f493))) (define-fun f524 () Arctic (+ (* f45 f474) (* f46 f479) (* f47 f484) (* f48 f489) (* f49 f494))) (define-fun f525 () Arctic (+ (* f50 f470) (* f51 f475) (* f52 f480) (* f53 f485) (* f54 f490))) (define-fun f526 () Arctic (+ (* f50 f471) (* f51 f476) (* f52 f481) (* f53 f486) (* f54 f491))) (define-fun f527 () Arctic (+ (* f50 f472) (* f51 f477) (* f52 f482) (* f53 f487) (* f54 f492))) (define-fun f528 () Arctic (+ (* f50 f473) (* f51 f478) (* f52 f483) (* f53 f488) (* f54 f493))) (define-fun f529 () Arctic (+ (* f50 f474) (* f51 f479) (* f52 f484) (* f53 f489) (* f54 f494))) (define-fun f530 () Arctic (+ (* f30 f500) (* f31 f501) (* f32 f502) (* f33 f503) (* f34 f504))) (define-fun f531 () Arctic (+ (* f35 f500) (* f36 f501) (* f37 f502) (* f38 f503) (* f39 f504))) (define-fun f532 () Arctic (+ (* f40 f500) (* f41 f501) (* f42 f502) (* f43 f503) (* f44 f504))) (define-fun f533 () Arctic (+ (* f45 f500) (* f46 f501) (* f47 f502) (* f48 f503) (* f49 f504))) (define-fun f534 () Arctic (+ (* f50 f500) (* f51 f501) (* f52 f502) (* f53 f503) (* f54 f504))) (define-fun f535 () Arctic (+ f55 f530)) (define-fun f536 () Arctic (+ f56 f531)) (define-fun f537 () Arctic (+ f57 f532)) (define-fun f538 () Arctic (+ f58 f533)) (define-fun f539 () Arctic (+ f59 f534)) (define-fun f540 () Arctic (+ (* f90 f505) (* f91 f510) (* f92 f515) (* f93 f520) (* f94 f525))) (define-fun f541 () Arctic (+ (* f90 f506) (* f91 f511) (* f92 f516) (* f93 f521) (* f94 f526))) (define-fun f542 () Arctic (+ (* f90 f507) (* f91 f512) (* f92 f517) (* f93 f522) (* f94 f527))) (define-fun f543 () Arctic (+ (* f90 f508) (* f91 f513) (* f92 f518) (* f93 f523) (* f94 f528))) (define-fun f544 () Arctic (+ (* f90 f509) (* f91 f514) (* f92 f519) (* f93 f524) (* f94 f529))) (define-fun f545 () Arctic (+ (* f95 f505) (* f96 f510) (* f97 f515) (* f98 f520) (* f99 f525))) (define-fun f546 () Arctic (+ (* f95 f506) (* f96 f511) (* f97 f516) (* f98 f521) (* f99 f526))) (define-fun f547 () Arctic (+ (* f95 f507) (* f96 f512) (* f97 f517) (* f98 f522) (* f99 f527))) (define-fun f548 () Arctic (+ (* f95 f508) (* f96 f513) (* f97 f518) (* f98 f523) (* f99 f528))) (define-fun f549 () Arctic (+ (* f95 f509) (* f96 f514) (* f97 f519) (* f98 f524) (* f99 f529))) (define-fun f550 () Arctic (+ (* f100 f505) (* f101 f510) (* f102 f515) (* f103 f520) (* f104 f525))) (define-fun f551 () Arctic (+ (* f100 f506) (* f101 f511) (* f102 f516) (* f103 f521) (* f104 f526))) (define-fun f552 () Arctic (+ (* f100 f507) (* f101 f512) (* f102 f517) (* f103 f522) (* f104 f527))) (define-fun f553 () Arctic (+ (* f100 f508) (* f101 f513) (* f102 f518) (* f103 f523) (* f104 f528))) (define-fun f554 () Arctic (+ (* f100 f509) (* f101 f514) (* f102 f519) (* f103 f524) (* f104 f529))) (define-fun f555 () Arctic (+ (* f105 f505) (* f106 f510) (* f107 f515) (* f108 f520) (* f109 f525))) (define-fun f556 () Arctic (+ (* f105 f506) (* f106 f511) (* f107 f516) (* f108 f521) (* f109 f526))) (define-fun f557 () Arctic (+ (* f105 f507) (* f106 f512) (* f107 f517) (* f108 f522) (* f109 f527))) (define-fun f558 () Arctic (+ (* f105 f508) (* f106 f513) (* f107 f518) (* f108 f523) (* f109 f528))) (define-fun f559 () Arctic (+ (* f105 f509) (* f106 f514) (* f107 f519) (* f108 f524) (* f109 f529))) (define-fun f560 () Arctic (+ (* f110 f505) (* f111 f510) (* f112 f515) (* f113 f520) (* f114 f525))) (define-fun f561 () Arctic (+ (* f110 f506) (* f111 f511) (* f112 f516) (* f113 f521) (* f114 f526))) (define-fun f562 () Arctic (+ (* f110 f507) (* f111 f512) (* f112 f517) (* f113 f522) (* f114 f527))) (define-fun f563 () Arctic (+ (* f110 f508) (* f111 f513) (* f112 f518) (* f113 f523) (* f114 f528))) (define-fun f564 () Arctic (+ (* f110 f509) (* f111 f514) (* f112 f519) (* f113 f524) (* f114 f529))) (define-fun f565 () Arctic (+ (* f90 f535) (* f91 f536) (* f92 f537) (* f93 f538) (* f94 f539))) (define-fun f566 () Arctic (+ (* f95 f535) (* f96 f536) (* f97 f537) (* f98 f538) (* f99 f539))) (define-fun f567 () Arctic (+ (* f100 f535) (* f101 f536) (* f102 f537) (* f103 f538) (* f104 f539))) (define-fun f568 () Arctic (+ (* f105 f535) (* f106 f536) (* f107 f537) (* f108 f538) (* f109 f539))) (define-fun f569 () Arctic (+ (* f110 f535) (* f111 f536) (* f112 f537) (* f113 f538) (* f114 f539))) (define-fun f570 () Arctic (+ f115 f565)) (define-fun f571 () Arctic (+ f116 f566)) (define-fun f572 () Arctic (+ f117 f567)) (define-fun f573 () Arctic (+ f118 f568)) (define-fun f574 () Arctic (+ f119 f569)) (define-fun f575 () Arctic (+ (* f90 f60) (* f91 f65) (* f92 f70) (* f93 f75) (* f94 f80))) (define-fun f576 () Arctic (+ (* f90 f61) (* f91 f66) (* f92 f71) (* f93 f76) (* f94 f81))) (define-fun f577 () Arctic (+ (* f90 f62) (* f91 f67) (* f92 f72) (* f93 f77) (* f94 f82))) (define-fun f578 () Arctic (+ (* f90 f63) (* f91 f68) (* f92 f73) (* f93 f78) (* f94 f83))) (define-fun f579 () Arctic (+ (* f90 f64) (* f91 f69) (* f92 f74) (* f93 f79) (* f94 f84))) (define-fun f580 () Arctic (+ (* f95 f60) (* f96 f65) (* f97 f70) (* f98 f75) (* f99 f80))) (define-fun f581 () Arctic (+ (* f95 f61) (* f96 f66) (* f97 f71) (* f98 f76) (* f99 f81))) (define-fun f582 () Arctic (+ (* f95 f62) (* f96 f67) (* f97 f72) (* f98 f77) (* f99 f82))) (define-fun f583 () Arctic (+ (* f95 f63) (* f96 f68) (* f97 f73) (* f98 f78) (* f99 f83))) (define-fun f584 () Arctic (+ (* f95 f64) (* f96 f69) (* f97 f74) (* f98 f79) (* f99 f84))) (define-fun f585 () Arctic (+ (* f100 f60) (* f101 f65) (* f102 f70) (* f103 f75) (* f104 f80))) (define-fun f586 () Arctic (+ (* f100 f61) (* f101 f66) (* f102 f71) (* f103 f76) (* f104 f81))) (define-fun f587 () Arctic (+ (* f100 f62) (* f101 f67) (* f102 f72) (* f103 f77) (* f104 f82))) (define-fun f588 () Arctic (+ (* f100 f63) (* f101 f68) (* f102 f73) (* f103 f78) (* f104 f83))) (define-fun f589 () Arctic (+ (* f100 f64) (* f101 f69) (* f102 f74) (* f103 f79) (* f104 f84))) (define-fun f590 () Arctic (+ (* f105 f60) (* f106 f65) (* f107 f70) (* f108 f75) (* f109 f80))) (define-fun f591 () Arctic (+ (* f105 f61) (* f106 f66) (* f107 f71) (* f108 f76) (* f109 f81))) (define-fun f592 () Arctic (+ (* f105 f62) (* f106 f67) (* f107 f72) (* f108 f77) (* f109 f82))) (define-fun f593 () Arctic (+ (* f105 f63) (* f106 f68) (* f107 f73) (* f108 f78) (* f109 f83))) (define-fun f594 () Arctic (+ (* f105 f64) (* f106 f69) (* f107 f74) (* f108 f79) (* f109 f84))) (define-fun f595 () Arctic (+ (* f110 f60) (* f111 f65) (* f112 f70) (* f113 f75) (* f114 f80))) (define-fun f596 () Arctic (+ (* f110 f61) (* f111 f66) (* f112 f71) (* f113 f76) (* f114 f81))) (define-fun f597 () Arctic (+ (* f110 f62) (* f111 f67) (* f112 f72) (* f113 f77) (* f114 f82))) (define-fun f598 () Arctic (+ (* f110 f63) (* f111 f68) (* f112 f73) (* f113 f78) (* f114 f83))) (define-fun f599 () Arctic (+ (* f110 f64) (* f111 f69) (* f112 f74) (* f113 f79) (* f114 f84))) (define-fun f600 () Arctic (+ (* f90 f85) (* f91 f86) (* f92 f87) (* f93 f88) (* f94 f89))) (define-fun f601 () Arctic (+ (* f95 f85) (* f96 f86) (* f97 f87) (* f98 f88) (* f99 f89))) (define-fun f602 () Arctic (+ (* f100 f85) (* f101 f86) (* f102 f87) (* f103 f88) (* f104 f89))) (define-fun f603 () Arctic (+ (* f105 f85) (* f106 f86) (* f107 f87) (* f108 f88) (* f109 f89))) (define-fun f604 () Arctic (+ (* f110 f85) (* f111 f86) (* f112 f87) (* f113 f88) (* f114 f89))) (define-fun f605 () Arctic (+ f115 f600)) (define-fun f606 () Arctic (+ f116 f601)) (define-fun f607 () Arctic (+ f117 f602)) (define-fun f608 () Arctic (+ f118 f603)) (define-fun f609 () Arctic (+ f119 f604)) (define-fun f610 () Arctic (+ (* f30 f60) (* f31 f65) (* f32 f70) (* f33 f75) (* f34 f80))) (define-fun f611 () Arctic (+ (* f30 f61) (* f31 f66) (* f32 f71) (* f33 f76) (* f34 f81))) (define-fun f612 () Arctic (+ (* f30 f62) (* f31 f67) (* f32 f72) (* f33 f77) (* f34 f82))) (define-fun f613 () Arctic (+ (* f30 f63) (* f31 f68) (* f32 f73) (* f33 f78) (* f34 f83))) (define-fun f614 () Arctic (+ (* f30 f64) (* f31 f69) (* f32 f74) (* f33 f79) (* f34 f84))) (define-fun f615 () Arctic (+ (* f35 f60) (* f36 f65) (* f37 f70) (* f38 f75) (* f39 f80))) (define-fun f616 () Arctic (+ (* f35 f61) (* f36 f66) (* f37 f71) (* f38 f76) (* f39 f81))) (define-fun f617 () Arctic (+ (* f35 f62) (* f36 f67) (* f37 f72) (* f38 f77) (* f39 f82))) (define-fun f618 () Arctic (+ (* f35 f63) (* f36 f68) (* f37 f73) (* f38 f78) (* f39 f83))) (define-fun f619 () Arctic (+ (* f35 f64) (* f36 f69) (* f37 f74) (* f38 f79) (* f39 f84))) (define-fun f620 () Arctic (+ (* f40 f60) (* f41 f65) (* f42 f70) (* f43 f75) (* f44 f80))) (define-fun f621 () Arctic (+ (* f40 f61) (* f41 f66) (* f42 f71) (* f43 f76) (* f44 f81))) (define-fun f622 () Arctic (+ (* f40 f62) (* f41 f67) (* f42 f72) (* f43 f77) (* f44 f82))) (define-fun f623 () Arctic (+ (* f40 f63) (* f41 f68) (* f42 f73) (* f43 f78) (* f44 f83))) (define-fun f624 () Arctic (+ (* f40 f64) (* f41 f69) (* f42 f74) (* f43 f79) (* f44 f84))) (define-fun f625 () Arctic (+ (* f45 f60) (* f46 f65) (* f47 f70) (* f48 f75) (* f49 f80))) (define-fun f626 () Arctic (+ (* f45 f61) (* f46 f66) (* f47 f71) (* f48 f76) (* f49 f81))) (define-fun f627 () Arctic (+ (* f45 f62) (* f46 f67) (* f47 f72) (* f48 f77) (* f49 f82))) (define-fun f628 () Arctic (+ (* f45 f63) (* f46 f68) (* f47 f73) (* f48 f78) (* f49 f83))) (define-fun f629 () Arctic (+ (* f45 f64) (* f46 f69) (* f47 f74) (* f48 f79) (* f49 f84))) (define-fun f630 () Arctic (+ (* f50 f60) (* f51 f65) (* f52 f70) (* f53 f75) (* f54 f80))) (define-fun f631 () Arctic (+ (* f50 f61) (* f51 f66) (* f52 f71) (* f53 f76) (* f54 f81))) (define-fun f632 () Arctic (+ (* f50 f62) (* f51 f67) (* f52 f72) (* f53 f77) (* f54 f82))) (define-fun f633 () Arctic (+ (* f50 f63) (* f51 f68) (* f52 f73) (* f53 f78) (* f54 f83))) (define-fun f634 () Arctic (+ (* f50 f64) (* f51 f69) (* f52 f74) (* f53 f79) (* f54 f84))) (define-fun f635 () Arctic (+ (* f30 f85) (* f31 f86) (* f32 f87) (* f33 f88) (* f34 f89))) (define-fun f636 () Arctic (+ (* f35 f85) (* f36 f86) (* f37 f87) (* f38 f88) (* f39 f89))) (define-fun f637 () Arctic (+ (* f40 f85) (* f41 f86) (* f42 f87) (* f43 f88) (* f44 f89))) (define-fun f638 () Arctic (+ (* f45 f85) (* f46 f86) (* f47 f87) (* f48 f88) (* f49 f89))) (define-fun f639 () Arctic (+ (* f50 f85) (* f51 f86) (* f52 f87) (* f53 f88) (* f54 f89))) (define-fun f640 () Arctic (+ f55 f635)) (define-fun f641 () Arctic (+ f56 f636)) (define-fun f642 () Arctic (+ f57 f637)) (define-fun f643 () Arctic (+ f58 f638)) (define-fun f644 () Arctic (+ f59 f639)) (define-fun f645 () Arctic (+ (* f30 f610) (* f31 f615) (* f32 f620) (* f33 f625) (* f34 f630))) (define-fun f646 () Arctic (+ (* f30 f611) (* f31 f616) (* f32 f621) (* f33 f626) (* f34 f631))) (define-fun f647 () Arctic (+ (* f30 f612) (* f31 f617) (* f32 f622) (* f33 f627) (* f34 f632))) (define-fun f648 () Arctic (+ (* f30 f613) (* f31 f618) (* f32 f623) (* f33 f628) (* f34 f633))) (define-fun f649 () Arctic (+ (* f30 f614) (* f31 f619) (* f32 f624) (* f33 f629) (* f34 f634))) (define-fun f650 () Arctic (+ (* f35 f610) (* f36 f615) (* f37 f620) (* f38 f625) (* f39 f630))) (define-fun f651 () Arctic (+ (* f35 f611) (* f36 f616) (* f37 f621) (* f38 f626) (* f39 f631))) (define-fun f652 () Arctic (+ (* f35 f612) (* f36 f617) (* f37 f622) (* f38 f627) (* f39 f632))) (define-fun f653 () Arctic (+ (* f35 f613) (* f36 f618) (* f37 f623) (* f38 f628) (* f39 f633))) (define-fun f654 () Arctic (+ (* f35 f614) (* f36 f619) (* f37 f624) (* f38 f629) (* f39 f634))) (define-fun f655 () Arctic (+ (* f40 f610) (* f41 f615) (* f42 f620) (* f43 f625) (* f44 f630))) (define-fun f656 () Arctic (+ (* f40 f611) (* f41 f616) (* f42 f621) (* f43 f626) (* f44 f631))) (define-fun f657 () Arctic (+ (* f40 f612) (* f41 f617) (* f42 f622) (* f43 f627) (* f44 f632))) (define-fun f658 () Arctic (+ (* f40 f613) (* f41 f618) (* f42 f623) (* f43 f628) (* f44 f633))) (define-fun f659 () Arctic (+ (* f40 f614) (* f41 f619) (* f42 f624) (* f43 f629) (* f44 f634))) (define-fun f660 () Arctic (+ (* f45 f610) (* f46 f615) (* f47 f620) (* f48 f625) (* f49 f630))) (define-fun f661 () Arctic (+ (* f45 f611) (* f46 f616) (* f47 f621) (* f48 f626) (* f49 f631))) (define-fun f662 () Arctic (+ (* f45 f612) (* f46 f617) (* f47 f622) (* f48 f627) (* f49 f632))) (define-fun f663 () Arctic (+ (* f45 f613) (* f46 f618) (* f47 f623) (* f48 f628) (* f49 f633))) (define-fun f664 () Arctic (+ (* f45 f614) (* f46 f619) (* f47 f624) (* f48 f629) (* f49 f634))) (define-fun f665 () Arctic (+ (* f50 f610) (* f51 f615) (* f52 f620) (* f53 f625) (* f54 f630))) (define-fun f666 () Arctic (+ (* f50 f611) (* f51 f616) (* f52 f621) (* f53 f626) (* f54 f631))) (define-fun f667 () Arctic (+ (* f50 f612) (* f51 f617) (* f52 f622) (* f53 f627) (* f54 f632))) (define-fun f668 () Arctic (+ (* f50 f613) (* f51 f618) (* f52 f623) (* f53 f628) (* f54 f633))) (define-fun f669 () Arctic (+ (* f50 f614) (* f51 f619) (* f52 f624) (* f53 f629) (* f54 f634))) (define-fun f670 () Arctic (+ (* f30 f640) (* f31 f641) (* f32 f642) (* f33 f643) (* f34 f644))) (define-fun f671 () Arctic (+ (* f35 f640) (* f36 f641) (* f37 f642) (* f38 f643) (* f39 f644))) (define-fun f672 () Arctic (+ (* f40 f640) (* f41 f641) (* f42 f642) (* f43 f643) (* f44 f644))) (define-fun f673 () Arctic (+ (* f45 f640) (* f46 f641) (* f47 f642) (* f48 f643) (* f49 f644))) (define-fun f674 () Arctic (+ (* f50 f640) (* f51 f641) (* f52 f642) (* f53 f643) (* f54 f644))) (define-fun f675 () Arctic (+ f55 f670)) (define-fun f676 () Arctic (+ f56 f671)) (define-fun f677 () Arctic (+ f57 f672)) (define-fun f678 () Arctic (+ f58 f673)) (define-fun f679 () Arctic (+ f59 f674)) (define-fun f680 () Arctic (+ (* f30 f30) (* f31 f35) (* f32 f40) (* f33 f45) (* f34 f50))) (define-fun f681 () Arctic (+ (* f30 f31) (* f31 f36) (* f32 f41) (* f33 f46) (* f34 f51))) (define-fun f682 () Arctic (+ (* f30 f32) (* f31 f37) (* f32 f42) (* f33 f47) (* f34 f52))) (define-fun f683 () Arctic (+ (* f30 f33) (* f31 f38) (* f32 f43) (* f33 f48) (* f34 f53))) (define-fun f684 () Arctic (+ (* f30 f34) (* f31 f39) (* f32 f44) (* f33 f49) (* f34 f54))) (define-fun f685 () Arctic (+ (* f35 f30) (* f36 f35) (* f37 f40) (* f38 f45) (* f39 f50))) (define-fun f686 () Arctic (+ (* f35 f31) (* f36 f36) (* f37 f41) (* f38 f46) (* f39 f51))) (define-fun f687 () Arctic (+ (* f35 f32) (* f36 f37) (* f37 f42) (* f38 f47) (* f39 f52))) (define-fun f688 () Arctic (+ (* f35 f33) (* f36 f38) (* f37 f43) (* f38 f48) (* f39 f53))) (define-fun f689 () Arctic (+ (* f35 f34) (* f36 f39) (* f37 f44) (* f38 f49) (* f39 f54))) (define-fun f690 () Arctic (+ (* f40 f30) (* f41 f35) (* f42 f40) (* f43 f45) (* f44 f50))) (define-fun f691 () Arctic (+ (* f40 f31) (* f41 f36) (* f42 f41) (* f43 f46) (* f44 f51))) (define-fun f692 () Arctic (+ (* f40 f32) (* f41 f37) (* f42 f42) (* f43 f47) (* f44 f52))) (define-fun f693 () Arctic (+ (* f40 f33) (* f41 f38) (* f42 f43) (* f43 f48) (* f44 f53))) (define-fun f694 () Arctic (+ (* f40 f34) (* f41 f39) (* f42 f44) (* f43 f49) (* f44 f54))) (define-fun f695 () Arctic (+ (* f45 f30) (* f46 f35) (* f47 f40) (* f48 f45) (* f49 f50))) (define-fun f696 () Arctic (+ (* f45 f31) (* f46 f36) (* f47 f41) (* f48 f46) (* f49 f51))) (define-fun f697 () Arctic (+ (* f45 f32) (* f46 f37) (* f47 f42) (* f48 f47) (* f49 f52))) (define-fun f698 () Arctic (+ (* f45 f33) (* f46 f38) (* f47 f43) (* f48 f48) (* f49 f53))) (define-fun f699 () Arctic (+ (* f45 f34) (* f46 f39) (* f47 f44) (* f48 f49) (* f49 f54))) (define-fun f700 () Arctic (+ (* f50 f30) (* f51 f35) (* f52 f40) (* f53 f45) (* f54 f50))) (define-fun f701 () Arctic (+ (* f50 f31) (* f51 f36) (* f52 f41) (* f53 f46) (* f54 f51))) (define-fun f702 () Arctic (+ (* f50 f32) (* f51 f37) (* f52 f42) (* f53 f47) (* f54 f52))) (define-fun f703 () Arctic (+ (* f50 f33) (* f51 f38) (* f52 f43) (* f53 f48) (* f54 f53))) (define-fun f704 () Arctic (+ (* f50 f34) (* f51 f39) (* f52 f44) (* f53 f49) (* f54 f54))) (define-fun f705 () Arctic (+ (* f30 f55) (* f31 f56) (* f32 f57) (* f33 f58) (* f34 f59))) (define-fun f706 () Arctic (+ (* f35 f55) (* f36 f56) (* f37 f57) (* f38 f58) (* f39 f59))) (define-fun f707 () Arctic (+ (* f40 f55) (* f41 f56) (* f42 f57) (* f43 f58) (* f44 f59))) (define-fun f708 () Arctic (+ (* f45 f55) (* f46 f56) (* f47 f57) (* f48 f58) (* f49 f59))) (define-fun f709 () Arctic (+ (* f50 f55) (* f51 f56) (* f52 f57) (* f53 f58) (* f54 f59))) (define-fun f710 () Arctic (+ f55 f705)) (define-fun f711 () Arctic (+ f56 f706)) (define-fun f712 () Arctic (+ f57 f707)) (define-fun f713 () Arctic (+ f58 f708)) (define-fun f714 () Arctic (+ f59 f709)) (define-fun f715 () Arctic (+ (* f30 f680) (* f31 f685) (* f32 f690) (* f33 f695) (* f34 f700))) (define-fun f716 () Arctic (+ (* f30 f681) (* f31 f686) (* f32 f691) (* f33 f696) (* f34 f701))) (define-fun f717 () Arctic (+ (* f30 f682) (* f31 f687) (* f32 f692) (* f33 f697) (* f34 f702))) (define-fun f718 () Arctic (+ (* f30 f683) (* f31 f688) (* f32 f693) (* f33 f698) (* f34 f703))) (define-fun f719 () Arctic (+ (* f30 f684) (* f31 f689) (* f32 f694) (* f33 f699) (* f34 f704))) (define-fun f720 () Arctic (+ (* f35 f680) (* f36 f685) (* f37 f690) (* f38 f695) (* f39 f700))) (define-fun f721 () Arctic (+ (* f35 f681) (* f36 f686) (* f37 f691) (* f38 f696) (* f39 f701))) (define-fun f722 () Arctic (+ (* f35 f682) (* f36 f687) (* f37 f692) (* f38 f697) (* f39 f702))) (define-fun f723 () Arctic (+ (* f35 f683) (* f36 f688) (* f37 f693) (* f38 f698) (* f39 f703))) (define-fun f724 () Arctic (+ (* f35 f684) (* f36 f689) (* f37 f694) (* f38 f699) (* f39 f704))) (define-fun f725 () Arctic (+ (* f40 f680) (* f41 f685) (* f42 f690) (* f43 f695) (* f44 f700))) (define-fun f726 () Arctic (+ (* f40 f681) (* f41 f686) (* f42 f691) (* f43 f696) (* f44 f701))) (define-fun f727 () Arctic (+ (* f40 f682) (* f41 f687) (* f42 f692) (* f43 f697) (* f44 f702))) (define-fun f728 () Arctic (+ (* f40 f683) (* f41 f688) (* f42 f693) (* f43 f698) (* f44 f703))) (define-fun f729 () Arctic (+ (* f40 f684) (* f41 f689) (* f42 f694) (* f43 f699) (* f44 f704))) (define-fun f730 () Arctic (+ (* f45 f680) (* f46 f685) (* f47 f690) (* f48 f695) (* f49 f700))) (define-fun f731 () Arctic (+ (* f45 f681) (* f46 f686) (* f47 f691) (* f48 f696) (* f49 f701))) (define-fun f732 () Arctic (+ (* f45 f682) (* f46 f687) (* f47 f692) (* f48 f697) (* f49 f702))) (define-fun f733 () Arctic (+ (* f45 f683) (* f46 f688) (* f47 f693) (* f48 f698) (* f49 f703))) (define-fun f734 () Arctic (+ (* f45 f684) (* f46 f689) (* f47 f694) (* f48 f699) (* f49 f704))) (define-fun f735 () Arctic (+ (* f50 f680) (* f51 f685) (* f52 f690) (* f53 f695) (* f54 f700))) (define-fun f736 () Arctic (+ (* f50 f681) (* f51 f686) (* f52 f691) (* f53 f696) (* f54 f701))) (define-fun f737 () Arctic (+ (* f50 f682) (* f51 f687) (* f52 f692) (* f53 f697) (* f54 f702))) (define-fun f738 () Arctic (+ (* f50 f683) (* f51 f688) (* f52 f693) (* f53 f698) (* f54 f703))) (define-fun f739 () Arctic (+ (* f50 f684) (* f51 f689) (* f52 f694) (* f53 f699) (* f54 f704))) (define-fun f740 () Arctic (+ (* f30 f710) (* f31 f711) (* f32 f712) (* f33 f713) (* f34 f714))) (define-fun f741 () Arctic (+ (* f35 f710) (* f36 f711) (* f37 f712) (* f38 f713) (* f39 f714))) (define-fun f742 () Arctic (+ (* f40 f710) (* f41 f711) (* f42 f712) (* f43 f713) (* f44 f714))) (define-fun f743 () Arctic (+ (* f45 f710) (* f46 f711) (* f47 f712) (* f48 f713) (* f49 f714))) (define-fun f744 () Arctic (+ (* f50 f710) (* f51 f711) (* f52 f712) (* f53 f713) (* f54 f714))) (define-fun f745 () Arctic (+ f55 f740)) (define-fun f746 () Arctic (+ f56 f741)) (define-fun f747 () Arctic (+ f57 f742)) (define-fun f748 () Arctic (+ f58 f743)) (define-fun f749 () Arctic (+ f59 f744)) (define-fun f750 () Arctic (+ (* f60 f715) (* f61 f720) (* f62 f725) (* f63 f730) (* f64 f735))) (define-fun f751 () Arctic (+ (* f60 f716) (* f61 f721) (* f62 f726) (* f63 f731) (* f64 f736))) (define-fun f752 () Arctic (+ (* f60 f717) (* f61 f722) (* f62 f727) (* f63 f732) (* f64 f737))) (define-fun f753 () Arctic (+ (* f60 f718) (* f61 f723) (* f62 f728) (* f63 f733) (* f64 f738))) (define-fun f754 () Arctic (+ (* f60 f719) (* f61 f724) (* f62 f729) (* f63 f734) (* f64 f739))) (define-fun f755 () Arctic (+ (* f65 f715) (* f66 f720) (* f67 f725) (* f68 f730) (* f69 f735))) (define-fun f756 () Arctic (+ (* f65 f716) (* f66 f721) (* f67 f726) (* f68 f731) (* f69 f736))) (define-fun f757 () Arctic (+ (* f65 f717) (* f66 f722) (* f67 f727) (* f68 f732) (* f69 f737))) (define-fun f758 () Arctic (+ (* f65 f718) (* f66 f723) (* f67 f728) (* f68 f733) (* f69 f738))) (define-fun f759 () Arctic (+ (* f65 f719) (* f66 f724) (* f67 f729) (* f68 f734) (* f69 f739))) (define-fun f760 () Arctic (+ (* f70 f715) (* f71 f720) (* f72 f725) (* f73 f730) (* f74 f735))) (define-fun f761 () Arctic (+ (* f70 f716) (* f71 f721) (* f72 f726) (* f73 f731) (* f74 f736))) (define-fun f762 () Arctic (+ (* f70 f717) (* f71 f722) (* f72 f727) (* f73 f732) (* f74 f737))) (define-fun f763 () Arctic (+ (* f70 f718) (* f71 f723) (* f72 f728) (* f73 f733) (* f74 f738))) (define-fun f764 () Arctic (+ (* f70 f719) (* f71 f724) (* f72 f729) (* f73 f734) (* f74 f739))) (define-fun f765 () Arctic (+ (* f75 f715) (* f76 f720) (* f77 f725) (* f78 f730) (* f79 f735))) (define-fun f766 () Arctic (+ (* f75 f716) (* f76 f721) (* f77 f726) (* f78 f731) (* f79 f736))) (define-fun f767 () Arctic (+ (* f75 f717) (* f76 f722) (* f77 f727) (* f78 f732) (* f79 f737))) (define-fun f768 () Arctic (+ (* f75 f718) (* f76 f723) (* f77 f728) (* f78 f733) (* f79 f738))) (define-fun f769 () Arctic (+ (* f75 f719) (* f76 f724) (* f77 f729) (* f78 f734) (* f79 f739))) (define-fun f770 () Arctic (+ (* f80 f715) (* f81 f720) (* f82 f725) (* f83 f730) (* f84 f735))) (define-fun f771 () Arctic (+ (* f80 f716) (* f81 f721) (* f82 f726) (* f83 f731) (* f84 f736))) (define-fun f772 () Arctic (+ (* f80 f717) (* f81 f722) (* f82 f727) (* f83 f732) (* f84 f737))) (define-fun f773 () Arctic (+ (* f80 f718) (* f81 f723) (* f82 f728) (* f83 f733) (* f84 f738))) (define-fun f774 () Arctic (+ (* f80 f719) (* f81 f724) (* f82 f729) (* f83 f734) (* f84 f739))) (define-fun f775 () Arctic (+ (* f60 f745) (* f61 f746) (* f62 f747) (* f63 f748) (* f64 f749))) (define-fun f776 () Arctic (+ (* f65 f745) (* f66 f746) (* f67 f747) (* f68 f748) (* f69 f749))) (define-fun f777 () Arctic (+ (* f70 f745) (* f71 f746) (* f72 f747) (* f73 f748) (* f74 f749))) (define-fun f778 () Arctic (+ (* f75 f745) (* f76 f746) (* f77 f747) (* f78 f748) (* f79 f749))) (define-fun f779 () Arctic (+ (* f80 f745) (* f81 f746) (* f82 f747) (* f83 f748) (* f84 f749))) (define-fun f780 () Arctic (+ f85 f775)) (define-fun f781 () Arctic (+ f86 f776)) (define-fun f782 () Arctic (+ f87 f777)) (define-fun f783 () Arctic (+ f88 f778)) (define-fun f784 () Arctic (+ f89 f779)) (define-fun f785 () Arctic (+ (* f60 f30) (* f61 f35) (* f62 f40) (* f63 f45) (* f64 f50))) (define-fun f786 () Arctic (+ (* f60 f31) (* f61 f36) (* f62 f41) (* f63 f46) (* f64 f51))) (define-fun f787 () Arctic (+ (* f60 f32) (* f61 f37) (* f62 f42) (* f63 f47) (* f64 f52))) (define-fun f788 () Arctic (+ (* f60 f33) (* f61 f38) (* f62 f43) (* f63 f48) (* f64 f53))) (define-fun f789 () Arctic (+ (* f60 f34) (* f61 f39) (* f62 f44) (* f63 f49) (* f64 f54))) (define-fun f790 () Arctic (+ (* f65 f30) (* f66 f35) (* f67 f40) (* f68 f45) (* f69 f50))) (define-fun f791 () Arctic (+ (* f65 f31) (* f66 f36) (* f67 f41) (* f68 f46) (* f69 f51))) (define-fun f792 () Arctic (+ (* f65 f32) (* f66 f37) (* f67 f42) (* f68 f47) (* f69 f52))) (define-fun f793 () Arctic (+ (* f65 f33) (* f66 f38) (* f67 f43) (* f68 f48) (* f69 f53))) (define-fun f794 () Arctic (+ (* f65 f34) (* f66 f39) (* f67 f44) (* f68 f49) (* f69 f54))) (define-fun f795 () Arctic (+ (* f70 f30) (* f71 f35) (* f72 f40) (* f73 f45) (* f74 f50))) (define-fun f796 () Arctic (+ (* f70 f31) (* f71 f36) (* f72 f41) (* f73 f46) (* f74 f51))) (define-fun f797 () Arctic (+ (* f70 f32) (* f71 f37) (* f72 f42) (* f73 f47) (* f74 f52))) (define-fun f798 () Arctic (+ (* f70 f33) (* f71 f38) (* f72 f43) (* f73 f48) (* f74 f53))) (define-fun f799 () Arctic (+ (* f70 f34) (* f71 f39) (* f72 f44) (* f73 f49) (* f74 f54))) (define-fun f800 () Arctic (+ (* f75 f30) (* f76 f35) (* f77 f40) (* f78 f45) (* f79 f50))) (define-fun f801 () Arctic (+ (* f75 f31) (* f76 f36) (* f77 f41) (* f78 f46) (* f79 f51))) (define-fun f802 () Arctic (+ (* f75 f32) (* f76 f37) (* f77 f42) (* f78 f47) (* f79 f52))) (define-fun f803 () Arctic (+ (* f75 f33) (* f76 f38) (* f77 f43) (* f78 f48) (* f79 f53))) (define-fun f804 () Arctic (+ (* f75 f34) (* f76 f39) (* f77 f44) (* f78 f49) (* f79 f54))) (define-fun f805 () Arctic (+ (* f80 f30) (* f81 f35) (* f82 f40) (* f83 f45) (* f84 f50))) (define-fun f806 () Arctic (+ (* f80 f31) (* f81 f36) (* f82 f41) (* f83 f46) (* f84 f51))) (define-fun f807 () Arctic (+ (* f80 f32) (* f81 f37) (* f82 f42) (* f83 f47) (* f84 f52))) (define-fun f808 () Arctic (+ (* f80 f33) (* f81 f38) (* f82 f43) (* f83 f48) (* f84 f53))) (define-fun f809 () Arctic (+ (* f80 f34) (* f81 f39) (* f82 f44) (* f83 f49) (* f84 f54))) (define-fun f810 () Arctic (+ (* f60 f55) (* f61 f56) (* f62 f57) (* f63 f58) (* f64 f59))) (define-fun f811 () Arctic (+ (* f65 f55) (* f66 f56) (* f67 f57) (* f68 f58) (* f69 f59))) (define-fun f812 () Arctic (+ (* f70 f55) (* f71 f56) (* f72 f57) (* f73 f58) (* f74 f59))) (define-fun f813 () Arctic (+ (* f75 f55) (* f76 f56) (* f77 f57) (* f78 f58) (* f79 f59))) (define-fun f814 () Arctic (+ (* f80 f55) (* f81 f56) (* f82 f57) (* f83 f58) (* f84 f59))) (define-fun f815 () Arctic (+ f85 f810)) (define-fun f816 () Arctic (+ f86 f811)) (define-fun f817 () Arctic (+ f87 f812)) (define-fun f818 () Arctic (+ f88 f813)) (define-fun f819 () Arctic (+ f89 f814)) (define-fun f820 () Arctic (+ (* f30 f785) (* f31 f790) (* f32 f795) (* f33 f800) (* f34 f805))) (define-fun f821 () Arctic (+ (* f30 f786) (* f31 f791) (* f32 f796) (* f33 f801) (* f34 f806))) (define-fun f822 () Arctic (+ (* f30 f787) (* f31 f792) (* f32 f797) (* f33 f802) (* f34 f807))) (define-fun f823 () Arctic (+ (* f30 f788) (* f31 f793) (* f32 f798) (* f33 f803) (* f34 f808))) (define-fun f824 () Arctic (+ (* f30 f789) (* f31 f794) (* f32 f799) (* f33 f804) (* f34 f809))) (define-fun f825 () Arctic (+ (* f35 f785) (* f36 f790) (* f37 f795) (* f38 f800) (* f39 f805))) (define-fun f826 () Arctic (+ (* f35 f786) (* f36 f791) (* f37 f796) (* f38 f801) (* f39 f806))) (define-fun f827 () Arctic (+ (* f35 f787) (* f36 f792) (* f37 f797) (* f38 f802) (* f39 f807))) (define-fun f828 () Arctic (+ (* f35 f788) (* f36 f793) (* f37 f798) (* f38 f803) (* f39 f808))) (define-fun f829 () Arctic (+ (* f35 f789) (* f36 f794) (* f37 f799) (* f38 f804) (* f39 f809))) (define-fun f830 () Arctic (+ (* f40 f785) (* f41 f790) (* f42 f795) (* f43 f800) (* f44 f805))) (define-fun f831 () Arctic (+ (* f40 f786) (* f41 f791) (* f42 f796) (* f43 f801) (* f44 f806))) (define-fun f832 () Arctic (+ (* f40 f787) (* f41 f792) (* f42 f797) (* f43 f802) (* f44 f807))) (define-fun f833 () Arctic (+ (* f40 f788) (* f41 f793) (* f42 f798) (* f43 f803) (* f44 f808))) (define-fun f834 () Arctic (+ (* f40 f789) (* f41 f794) (* f42 f799) (* f43 f804) (* f44 f809))) (define-fun f835 () Arctic (+ (* f45 f785) (* f46 f790) (* f47 f795) (* f48 f800) (* f49 f805))) (define-fun f836 () Arctic (+ (* f45 f786) (* f46 f791) (* f47 f796) (* f48 f801) (* f49 f806))) (define-fun f837 () Arctic (+ (* f45 f787) (* f46 f792) (* f47 f797) (* f48 f802) (* f49 f807))) (define-fun f838 () Arctic (+ (* f45 f788) (* f46 f793) (* f47 f798) (* f48 f803) (* f49 f808))) (define-fun f839 () Arctic (+ (* f45 f789) (* f46 f794) (* f47 f799) (* f48 f804) (* f49 f809))) (define-fun f840 () Arctic (+ (* f50 f785) (* f51 f790) (* f52 f795) (* f53 f800) (* f54 f805))) (define-fun f841 () Arctic (+ (* f50 f786) (* f51 f791) (* f52 f796) (* f53 f801) (* f54 f806))) (define-fun f842 () Arctic (+ (* f50 f787) (* f51 f792) (* f52 f797) (* f53 f802) (* f54 f807))) (define-fun f843 () Arctic (+ (* f50 f788) (* f51 f793) (* f52 f798) (* f53 f803) (* f54 f808))) (define-fun f844 () Arctic (+ (* f50 f789) (* f51 f794) (* f52 f799) (* f53 f804) (* f54 f809))) (define-fun f845 () Arctic (+ (* f30 f815) (* f31 f816) (* f32 f817) (* f33 f818) (* f34 f819))) (define-fun f846 () Arctic (+ (* f35 f815) (* f36 f816) (* f37 f817) (* f38 f818) (* f39 f819))) (define-fun f847 () Arctic (+ (* f40 f815) (* f41 f816) (* f42 f817) (* f43 f818) (* f44 f819))) (define-fun f848 () Arctic (+ (* f45 f815) (* f46 f816) (* f47 f817) (* f48 f818) (* f49 f819))) (define-fun f849 () Arctic (+ (* f50 f815) (* f51 f816) (* f52 f817) (* f53 f818) (* f54 f819))) (define-fun f850 () Arctic (+ f55 f845)) (define-fun f851 () Arctic (+ f56 f846)) (define-fun f852 () Arctic (+ f57 f847)) (define-fun f853 () Arctic (+ f58 f848)) (define-fun f854 () Arctic (+ f59 f849)) (define-fun f855 () Arctic (+ (* f60 f820) (* f61 f825) (* f62 f830) (* f63 f835) (* f64 f840))) (define-fun f856 () Arctic (+ (* f60 f821) (* f61 f826) (* f62 f831) (* f63 f836) (* f64 f841))) (define-fun f857 () Arctic (+ (* f60 f822) (* f61 f827) (* f62 f832) (* f63 f837) (* f64 f842))) (define-fun f858 () Arctic (+ (* f60 f823) (* f61 f828) (* f62 f833) (* f63 f838) (* f64 f843))) (define-fun f859 () Arctic (+ (* f60 f824) (* f61 f829) (* f62 f834) (* f63 f839) (* f64 f844))) (define-fun f860 () Arctic (+ (* f65 f820) (* f66 f825) (* f67 f830) (* f68 f835) (* f69 f840))) (define-fun f861 () Arctic (+ (* f65 f821) (* f66 f826) (* f67 f831) (* f68 f836) (* f69 f841))) (define-fun f862 () Arctic (+ (* f65 f822) (* f66 f827) (* f67 f832) (* f68 f837) (* f69 f842))) (define-fun f863 () Arctic (+ (* f65 f823) (* f66 f828) (* f67 f833) (* f68 f838) (* f69 f843))) (define-fun f864 () Arctic (+ (* f65 f824) (* f66 f829) (* f67 f834) (* f68 f839) (* f69 f844))) (define-fun f865 () Arctic (+ (* f70 f820) (* f71 f825) (* f72 f830) (* f73 f835) (* f74 f840))) (define-fun f866 () Arctic (+ (* f70 f821) (* f71 f826) (* f72 f831) (* f73 f836) (* f74 f841))) (define-fun f867 () Arctic (+ (* f70 f822) (* f71 f827) (* f72 f832) (* f73 f837) (* f74 f842))) (define-fun f868 () Arctic (+ (* f70 f823) (* f71 f828) (* f72 f833) (* f73 f838) (* f74 f843))) (define-fun f869 () Arctic (+ (* f70 f824) (* f71 f829) (* f72 f834) (* f73 f839) (* f74 f844))) (define-fun f870 () Arctic (+ (* f75 f820) (* f76 f825) (* f77 f830) (* f78 f835) (* f79 f840))) (define-fun f871 () Arctic (+ (* f75 f821) (* f76 f826) (* f77 f831) (* f78 f836) (* f79 f841))) (define-fun f872 () Arctic (+ (* f75 f822) (* f76 f827) (* f77 f832) (* f78 f837) (* f79 f842))) (define-fun f873 () Arctic (+ (* f75 f823) (* f76 f828) (* f77 f833) (* f78 f838) (* f79 f843))) (define-fun f874 () Arctic (+ (* f75 f824) (* f76 f829) (* f77 f834) (* f78 f839) (* f79 f844))) (define-fun f875 () Arctic (+ (* f80 f820) (* f81 f825) (* f82 f830) (* f83 f835) (* f84 f840))) (define-fun f876 () Arctic (+ (* f80 f821) (* f81 f826) (* f82 f831) (* f83 f836) (* f84 f841))) (define-fun f877 () Arctic (+ (* f80 f822) (* f81 f827) (* f82 f832) (* f83 f837) (* f84 f842))) (define-fun f878 () Arctic (+ (* f80 f823) (* f81 f828) (* f82 f833) (* f83 f838) (* f84 f843))) (define-fun f879 () Arctic (+ (* f80 f824) (* f81 f829) (* f82 f834) (* f83 f839) (* f84 f844))) (define-fun f880 () Arctic (+ (* f60 f850) (* f61 f851) (* f62 f852) (* f63 f853) (* f64 f854))) (define-fun f881 () Arctic (+ (* f65 f850) (* f66 f851) (* f67 f852) (* f68 f853) (* f69 f854))) (define-fun f882 () Arctic (+ (* f70 f850) (* f71 f851) (* f72 f852) (* f73 f853) (* f74 f854))) (define-fun f883 () Arctic (+ (* f75 f850) (* f76 f851) (* f77 f852) (* f78 f853) (* f79 f854))) (define-fun f884 () Arctic (+ (* f80 f850) (* f81 f851) (* f82 f852) (* f83 f853) (* f84 f854))) (define-fun f885 () Arctic (+ f85 f880)) (define-fun f886 () Arctic (+ f86 f881)) (define-fun f887 () Arctic (+ f87 f882)) (define-fun f888 () Arctic (+ f88 f883)) (define-fun f889 () Arctic (+ f89 f884)) (define-fun f890 () Arctic (+ (* f60 f60) (* f61 f65) (* f62 f70) (* f63 f75) (* f64 f80))) (define-fun f891 () Arctic (+ (* f60 f61) (* f61 f66) (* f62 f71) (* f63 f76) (* f64 f81))) (define-fun f892 () Arctic (+ (* f60 f62) (* f61 f67) (* f62 f72) (* f63 f77) (* f64 f82))) (define-fun f893 () Arctic (+ (* f60 f63) (* f61 f68) (* f62 f73) (* f63 f78) (* f64 f83))) (define-fun f894 () Arctic (+ (* f60 f64) (* f61 f69) (* f62 f74) (* f63 f79) (* f64 f84))) (define-fun f895 () Arctic (+ (* f65 f60) (* f66 f65) (* f67 f70) (* f68 f75) (* f69 f80))) (define-fun f896 () Arctic (+ (* f65 f61) (* f66 f66) (* f67 f71) (* f68 f76) (* f69 f81))) (define-fun f897 () Arctic (+ (* f65 f62) (* f66 f67) (* f67 f72) (* f68 f77) (* f69 f82))) (define-fun f898 () Arctic (+ (* f65 f63) (* f66 f68) (* f67 f73) (* f68 f78) (* f69 f83))) (define-fun f899 () Arctic (+ (* f65 f64) (* f66 f69) (* f67 f74) (* f68 f79) (* f69 f84))) (define-fun f900 () Arctic (+ (* f70 f60) (* f71 f65) (* f72 f70) (* f73 f75) (* f74 f80))) (define-fun f901 () Arctic (+ (* f70 f61) (* f71 f66) (* f72 f71) (* f73 f76) (* f74 f81))) (define-fun f902 () Arctic (+ (* f70 f62) (* f71 f67) (* f72 f72) (* f73 f77) (* f74 f82))) (define-fun f903 () Arctic (+ (* f70 f63) (* f71 f68) (* f72 f73) (* f73 f78) (* f74 f83))) (define-fun f904 () Arctic (+ (* f70 f64) (* f71 f69) (* f72 f74) (* f73 f79) (* f74 f84))) (define-fun f905 () Arctic (+ (* f75 f60) (* f76 f65) (* f77 f70) (* f78 f75) (* f79 f80))) (define-fun f906 () Arctic (+ (* f75 f61) (* f76 f66) (* f77 f71) (* f78 f76) (* f79 f81))) (define-fun f907 () Arctic (+ (* f75 f62) (* f76 f67) (* f77 f72) (* f78 f77) (* f79 f82))) (define-fun f908 () Arctic (+ (* f75 f63) (* f76 f68) (* f77 f73) (* f78 f78) (* f79 f83))) (define-fun f909 () Arctic (+ (* f75 f64) (* f76 f69) (* f77 f74) (* f78 f79) (* f79 f84))) (define-fun f910 () Arctic (+ (* f80 f60) (* f81 f65) (* f82 f70) (* f83 f75) (* f84 f80))) (define-fun f911 () Arctic (+ (* f80 f61) (* f81 f66) (* f82 f71) (* f83 f76) (* f84 f81))) (define-fun f912 () Arctic (+ (* f80 f62) (* f81 f67) (* f82 f72) (* f83 f77) (* f84 f82))) (define-fun f913 () Arctic (+ (* f80 f63) (* f81 f68) (* f82 f73) (* f83 f78) (* f84 f83))) (define-fun f914 () Arctic (+ (* f80 f64) (* f81 f69) (* f82 f74) (* f83 f79) (* f84 f84))) (define-fun f915 () Arctic (+ (* f60 f85) (* f61 f86) (* f62 f87) (* f63 f88) (* f64 f89))) (define-fun f916 () Arctic (+ (* f65 f85) (* f66 f86) (* f67 f87) (* f68 f88) (* f69 f89))) (define-fun f917 () Arctic (+ (* f70 f85) (* f71 f86) (* f72 f87) (* f73 f88) (* f74 f89))) (define-fun f918 () Arctic (+ (* f75 f85) (* f76 f86) (* f77 f87) (* f78 f88) (* f79 f89))) (define-fun f919 () Arctic (+ (* f80 f85) (* f81 f86) (* f82 f87) (* f83 f88) (* f84 f89))) (define-fun f920 () Arctic (+ f85 f915)) (define-fun f921 () Arctic (+ f86 f916)) (define-fun f922 () Arctic (+ f87 f917)) (define-fun f923 () Arctic (+ f88 f918)) (define-fun f924 () Arctic (+ f89 f919)) (define-fun f925 () Arctic (+ (* f30 f890) (* f31 f895) (* f32 f900) (* f33 f905) (* f34 f910))) (define-fun f926 () Arctic (+ (* f30 f891) (* f31 f896) (* f32 f901) (* f33 f906) (* f34 f911))) (define-fun f927 () Arctic (+ (* f30 f892) (* f31 f897) (* f32 f902) (* f33 f907) (* f34 f912))) (define-fun f928 () Arctic (+ (* f30 f893) (* f31 f898) (* f32 f903) (* f33 f908) (* f34 f913))) (define-fun f929 () Arctic (+ (* f30 f894) (* f31 f899) (* f32 f904) (* f33 f909) (* f34 f914))) (define-fun f930 () Arctic (+ (* f35 f890) (* f36 f895) (* f37 f900) (* f38 f905) (* f39 f910))) (define-fun f931 () Arctic (+ (* f35 f891) (* f36 f896) (* f37 f901) (* f38 f906) (* f39 f911))) (define-fun f932 () Arctic (+ (* f35 f892) (* f36 f897) (* f37 f902) (* f38 f907) (* f39 f912))) (define-fun f933 () Arctic (+ (* f35 f893) (* f36 f898) (* f37 f903) (* f38 f908) (* f39 f913))) (define-fun f934 () Arctic (+ (* f35 f894) (* f36 f899) (* f37 f904) (* f38 f909) (* f39 f914))) (define-fun f935 () Arctic (+ (* f40 f890) (* f41 f895) (* f42 f900) (* f43 f905) (* f44 f910))) (define-fun f936 () Arctic (+ (* f40 f891) (* f41 f896) (* f42 f901) (* f43 f906) (* f44 f911))) (define-fun f937 () Arctic (+ (* f40 f892) (* f41 f897) (* f42 f902) (* f43 f907) (* f44 f912))) (define-fun f938 () Arctic (+ (* f40 f893) (* f41 f898) (* f42 f903) (* f43 f908) (* f44 f913))) (define-fun f939 () Arctic (+ (* f40 f894) (* f41 f899) (* f42 f904) (* f43 f909) (* f44 f914))) (define-fun f940 () Arctic (+ (* f45 f890) (* f46 f895) (* f47 f900) (* f48 f905) (* f49 f910))) (define-fun f941 () Arctic (+ (* f45 f891) (* f46 f896) (* f47 f901) (* f48 f906) (* f49 f911))) (define-fun f942 () Arctic (+ (* f45 f892) (* f46 f897) (* f47 f902) (* f48 f907) (* f49 f912))) (define-fun f943 () Arctic (+ (* f45 f893) (* f46 f898) (* f47 f903) (* f48 f908) (* f49 f913))) (define-fun f944 () Arctic (+ (* f45 f894) (* f46 f899) (* f47 f904) (* f48 f909) (* f49 f914))) (define-fun f945 () Arctic (+ (* f50 f890) (* f51 f895) (* f52 f900) (* f53 f905) (* f54 f910))) (define-fun f946 () Arctic (+ (* f50 f891) (* f51 f896) (* f52 f901) (* f53 f906) (* f54 f911))) (define-fun f947 () Arctic (+ (* f50 f892) (* f51 f897) (* f52 f902) (* f53 f907) (* f54 f912))) (define-fun f948 () Arctic (+ (* f50 f893) (* f51 f898) (* f52 f903) (* f53 f908) (* f54 f913))) (define-fun f949 () Arctic (+ (* f50 f894) (* f51 f899) (* f52 f904) (* f53 f909) (* f54 f914))) (define-fun f950 () Arctic (+ (* f30 f920) (* f31 f921) (* f32 f922) (* f33 f923) (* f34 f924))) (define-fun f951 () Arctic (+ (* f35 f920) (* f36 f921) (* f37 f922) (* f38 f923) (* f39 f924))) (define-fun f952 () Arctic (+ (* f40 f920) (* f41 f921) (* f42 f922) (* f43 f923) (* f44 f924))) (define-fun f953 () Arctic (+ (* f45 f920) (* f46 f921) (* f47 f922) (* f48 f923) (* f49 f924))) (define-fun f954 () Arctic (+ (* f50 f920) (* f51 f921) (* f52 f922) (* f53 f923) (* f54 f924))) (define-fun f955 () Arctic (+ f55 f950)) (define-fun f956 () Arctic (+ f56 f951)) (define-fun f957 () Arctic (+ f57 f952)) (define-fun f958 () Arctic (+ f58 f953)) (define-fun f959 () Arctic (+ f59 f954)) (assert (and (and (and (and (>= f155 f260) (>= f156 f261) (>= f157 f262) (>= f158 f263) (>= f159 f264)) (and (>= f160 f265) (>= f161 f266) (>= f162 f267) (>= f163 f268) (>= f164 f269)) (and (>= f165 f270) (>= f166 f271) (>= f167 f272) (>= f168 f273) (>= f169 f274)) (and (>= f170 f275) (>= f171 f276) (>= f172 f277) (>= f173 f278) (>= f174 f279)) (and (>= f175 f280) (>= f176 f281) (>= f177 f282) (>= f178 f283) (>= f179 f284))) (and (and (>= f185 f290)) (and (>= f186 f291)) (and (>= f187 f292)) (and (>= f188 f293)) (and (>= f189 f294)))) (and (and (and (>= f365 f435) (>= f366 f436) (>= f367 f437) (>= f368 f438) (>= f369 f439)) (and (>= f370 f440) (>= f371 f441) (>= f372 f442) (>= f373 f443) (>= f374 f444)) (and (>= f375 f445) (>= f376 f446) (>= f377 f447) (>= f378 f448) (>= f379 f449)) (and (>= f380 f450) (>= f381 f451) (>= f382 f452) (>= f383 f453) (>= f384 f454)) (and (>= f385 f455) (>= f386 f456) (>= f387 f457) (>= f388 f458) (>= f389 f459))) (and (and (>= f395 f465)) (and (>= f396 f466)) (and (>= f397 f467)) (and (>= f398 f468)) (and (>= f399 f469)))) (and (and (and (>= f540 f575) (>= f541 f576) (>= f542 f577) (>= f543 f578) (>= f544 f579)) (and (>= f545 f580) (>= f546 f581) (>= f547 f582) (>= f548 f583) (>= f549 f584)) (and (>= f550 f585) (>= f551 f586) (>= f552 f587) (>= f553 f588) (>= f554 f589)) (and (>= f555 f590) (>= f556 f591) (>= f557 f592) (>= f558 f593) (>= f559 f594)) (and (>= f560 f595) (>= f561 f596) (>= f562 f597) (>= f563 f598) (>= f564 f599))) (and (and (>= f570 f605)) (and (>= f571 f606)) (and (>= f572 f607)) (and (>= f573 f608)) (and (>= f574 f609)))) (and (and (and (>= f645 f750) (>= f646 f751) (>= f647 f752) (>= f648 f753) (>= f649 f754)) (and (>= f650 f755) (>= f651 f756) (>= f652 f757) (>= f653 f758) (>= f654 f759)) (and (>= f655 f760) (>= f656 f761) (>= f657 f762) (>= f658 f763) (>= f659 f764)) (and (>= f660 f765) (>= f661 f766) (>= f662 f767) (>= f663 f768) (>= f664 f769)) (and (>= f665 f770) (>= f666 f771) (>= f667 f772) (>= f668 f773) (>= f669 f774))) (and (and (>= f675 f780)) (and (>= f676 f781)) (and (>= f677 f782)) (and (>= f678 f783)) (and (>= f679 f784)))) (and (and (and (>= f855 f925) (>= f856 f926) (>= f857 f927) (>= f858 f928) (>= f859 f929)) (and (>= f860 f930) (>= f861 f931) (>= f862 f932) (>= f863 f933) (>= f864 f934)) (and (>= f865 f935) (>= f866 f936) (>= f867 f937) (>= f868 f938) (>= f869 f939)) (and (>= f870 f940) (>= f871 f941) (>= f872 f942) (>= f873 f943) (>= f874 f944)) (and (>= f875 f945) (>= f876 f946) (>= f877 f947) (>= f878 f948) (>= f879 f949))) (and (and (>= f885 f955)) (and (>= f886 f956)) (and (>= f887 f957)) (and (>= f888 f958)) (and (>= f889 f959)))))) (assert (or (and (and (and (>> f155 f260) (>> f156 f261) (>> f157 f262) (>> f158 f263) (>> f159 f264)) (and (>> f160 f265) (>> f161 f266) (>> f162 f267) (>> f163 f268) (>> f164 f269)) (and (>> f165 f270) (>> f166 f271) (>> f167 f272) (>> f168 f273) (>> f169 f274)) (and (>> f170 f275) (>> f171 f276) (>> f172 f277) (>> f173 f278) (>> f174 f279)) (and (>> f175 f280) (>> f176 f281) (>> f177 f282) (>> f178 f283) (>> f179 f284))) (and (and (>> f185 f290)) (and (>> f186 f291)) (and (>> f187 f292)) (and (>> f188 f293)) (and (>> f189 f294)))) (and (and (and (>> f365 f435) (>> f366 f436) (>> f367 f437) (>> f368 f438) (>> f369 f439)) (and (>> f370 f440) (>> f371 f441) (>> f372 f442) (>> f373 f443) (>> f374 f444)) (and (>> f375 f445) (>> f376 f446) (>> f377 f447) (>> f378 f448) (>> f379 f449)) (and (>> f380 f450) (>> f381 f451) (>> f382 f452) (>> f383 f453) (>> f384 f454)) (and (>> f385 f455) (>> f386 f456) (>> f387 f457) (>> f388 f458) (>> f389 f459))) (and (and (>> f395 f465)) (and (>> f396 f466)) (and (>> f397 f467)) (and (>> f398 f468)) (and (>> f399 f469)))) (and (and (and (>> f540 f575) (>> f541 f576) (>> f542 f577) (>> f543 f578) (>> f544 f579)) (and (>> f545 f580) (>> f546 f581) (>> f547 f582) (>> f548 f583) (>> f549 f584)) (and (>> f550 f585) (>> f551 f586) (>> f552 f587) (>> f553 f588) (>> f554 f589)) (and (>> f555 f590) (>> f556 f591) (>> f557 f592) (>> f558 f593) (>> f559 f594)) (and (>> f560 f595) (>> f561 f596) (>> f562 f597) (>> f563 f598) (>> f564 f599))) (and (and (>> f570 f605)) (and (>> f571 f606)) (and (>> f572 f607)) (and (>> f573 f608)) (and (>> f574 f609)))))) (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 f693 f694 f695 f696 f697 f698 f699 f700 f701 f702 f703 f704 f705 f706 f707 f708 f709 f710 f711 f712 f713 f714 f715 f716 f717 f718 f719 f720 f721 f722 f723 f724 f725 f726 f727 f728 f729 f730 f731 f732 f733 f734 f735 f736 f737 f738 f739 f740 f741 f742 f743 f744 f745 f746 f747 f748 f749 f750 f751 f752 f753 f754 f755 f756 f757 f758 f759 f760 f761 f762 f763 f764 f765 f766 f767 f768 f769 f770 f771 f772 f773 f774 f775 f776 f777 f778 f779 f780 f781 f782 f783 f784 f785 f786 f787 f788 f789 f790 f791 f792 f793 f794 f795 f796 f797 f798 f799 f800 f801 f802 f803 f804 f805 f806 f807 f808 f809 f810 f811 f812 f813 f814 f815 f816 f817 f818 f819 f820 f821 f822 f823 f824 f825 f826 f827 f828 f829 f830 f831 f832 f833 f834 f835 f836 f837 f838 f839 f840 f841 f842 f843 f844 f845 f846 f847 f848 f849 f850 f851 f852 f853 f854 f855 f856 f857 f858 f859 f860 f861 f862 f863 f864 f865 f866 f867 f868 f869 f870 f871 f872 f873 f874 f875 f876 f877 f878 f879 f880 f881 f882 f883 f884 f885 f886 f887 f888 f889 f890 f891 f892 f893 f894 f895 f896 f897 f898 f899 f900 f901 f902 f903 f904 f905 f906 f907 f908 f909 f910 f911 f912 f913 f914 f915 f916 f917 f918 f919 f920 f921 f922 f923 f924 f925 f926 f927 f928 f929 f930 f931 f932 f933 f934 f935 f936 f937 f938 f939 f940 f941 f942 f943 f944 f945 f946 f947 f948 f949 f950 f951 f952 f953 f954 f955 f956 f957 f958 f959))