(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES b# b a a b -> b# b a a a a b, b# b a a b -> b# a a a a b, b# b a a b -> b#, b# b a b -> b# b, b# b a b -> b#, b# a a a a b a b -> b# a a a a b a a a b a b a a a a b a a a a b, b# a a a a b a b -> b# a a a b a b a a a a b a a a a b, b# a a a a b a b -> b# a b a a a a b a a a a b, b# a a a a b a b -> b# a a a a b a a a a b, b# a a a a b a b -> b# a a a a b, b# a a a a b a b -> b#, b# a a a a b a a b -> b# a a a a b a a a b a a b a b, b# a a a a b a a b -> b# a a a b a a b a b, b# a a a a b a a b -> b# a a b a b, b# a a a a b a a b -> b# a b, b# a a a a b a a b -> b#, b# a a a a b a a a b -> b#, b b a a b ->= b b a a a a b, b b a b ->= b b, b a a a a b a b ->= b a a a a b a a a b a b a a a a b a a a a b, b a a a a b a a b ->= b a a a a b a a a b a a b a b, b a a a a b a a a b ->= b) by arctic matrix interpretation with dimension 2|) (declare-fun f0 () Arctic) (declare-fun f1 () Arctic) (declare-fun f2 () Arctic) (declare-fun f3 () Arctic) (declare-fun f4 () Arctic) (declare-fun f5 () Arctic) (declare-fun f6 () Arctic) (declare-fun f7 () Arctic) (declare-fun f8 () Arctic) (declare-fun f9 () Arctic) (declare-fun f10 () Arctic) (declare-fun f11 () Arctic) (declare-fun f12 () Arctic) (declare-fun f13 () Arctic) (declare-fun f14 () Arctic) (declare-fun f15 () Arctic) (declare-fun f16 () Arctic) (declare-fun f17 () Arctic) (assert (and (or (finite f12) (finite f16)) (or (finite f6) (finite f10)) (or (finite f0) (finite f4)))) (define-fun f18 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f19 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f20 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f21 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f22 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f23 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f24 () Arctic (+ f16 f22)) (define-fun f25 () Arctic (+ f17 f23)) (define-fun f26 () Arctic (+ (* f12 f18) (* f13 f20))) (define-fun f27 () Arctic (+ (* f12 f19) (* f13 f21))) (define-fun f28 () Arctic (+ (* f14 f18) (* f15 f20))) (define-fun f29 () Arctic (+ (* f14 f19) (* f15 f21))) (define-fun f30 () Arctic (+ (* f12 f24) (* f13 f25))) (define-fun f31 () Arctic (+ (* f14 f24) (* f15 f25))) (define-fun f32 () Arctic (+ f16 f30)) (define-fun f33 () Arctic (+ f17 f31)) (define-fun f34 () Arctic (+ (* f6 f26) (* f7 f28))) (define-fun f35 () Arctic (+ (* f6 f27) (* f7 f29))) (define-fun f36 () Arctic (+ (* f8 f26) (* f9 f28))) (define-fun f37 () Arctic (+ (* f8 f27) (* f9 f29))) (define-fun f38 () Arctic (+ (* f6 f32) (* f7 f33))) (define-fun f39 () Arctic (+ (* f8 f32) (* f9 f33))) (define-fun f40 () Arctic (+ f10 f38)) (define-fun f41 () Arctic (+ f11 f39)) (define-fun f42 () Arctic (+ (* f0 f34) (* f1 f36))) (define-fun f43 () Arctic (+ (* f0 f35) (* f1 f37))) (define-fun f44 () Arctic (+ (* f2 f34) (* f3 f36))) (define-fun f45 () Arctic (+ (* f2 f35) (* f3 f37))) (define-fun f46 () Arctic (+ (* f0 f40) (* f1 f41))) (define-fun f47 () Arctic (+ (* f2 f40) (* f3 f41))) (define-fun f48 () Arctic (+ f4 f46)) (define-fun f49 () Arctic (+ f5 f47)) (define-fun f50 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f51 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f52 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f53 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f54 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f55 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f56 () Arctic (+ f16 f54)) (define-fun f57 () Arctic (+ f17 f55)) (define-fun f58 () Arctic (+ (* f12 f50) (* f13 f52))) (define-fun f59 () Arctic (+ (* f12 f51) (* f13 f53))) (define-fun f60 () Arctic (+ (* f14 f50) (* f15 f52))) (define-fun f61 () Arctic (+ (* f14 f51) (* f15 f53))) (define-fun f62 () Arctic (+ (* f12 f56) (* f13 f57))) (define-fun f63 () Arctic (+ (* f14 f56) (* f15 f57))) (define-fun f64 () Arctic (+ f16 f62)) (define-fun f65 () Arctic (+ f17 f63)) (define-fun f66 () Arctic (+ (* f12 f58) (* f13 f60))) (define-fun f67 () Arctic (+ (* f12 f59) (* f13 f61))) (define-fun f68 () Arctic (+ (* f14 f58) (* f15 f60))) (define-fun f69 () Arctic (+ (* f14 f59) (* f15 f61))) (define-fun f70 () Arctic (+ (* f12 f64) (* f13 f65))) (define-fun f71 () Arctic (+ (* f14 f64) (* f15 f65))) (define-fun f72 () Arctic (+ f16 f70)) (define-fun f73 () Arctic (+ f17 f71)) (define-fun f74 () Arctic (+ (* f12 f66) (* f13 f68))) (define-fun f75 () Arctic (+ (* f12 f67) (* f13 f69))) (define-fun f76 () Arctic (+ (* f14 f66) (* f15 f68))) (define-fun f77 () Arctic (+ (* f14 f67) (* f15 f69))) (define-fun f78 () Arctic (+ (* f12 f72) (* f13 f73))) (define-fun f79 () Arctic (+ (* f14 f72) (* f15 f73))) (define-fun f80 () Arctic (+ f16 f78)) (define-fun f81 () Arctic (+ f17 f79)) (define-fun f82 () Arctic (+ (* f6 f74) (* f7 f76))) (define-fun f83 () Arctic (+ (* f6 f75) (* f7 f77))) (define-fun f84 () Arctic (+ (* f8 f74) (* f9 f76))) (define-fun f85 () Arctic (+ (* f8 f75) (* f9 f77))) (define-fun f86 () Arctic (+ (* f6 f80) (* f7 f81))) (define-fun f87 () Arctic (+ (* f8 f80) (* f9 f81))) (define-fun f88 () Arctic (+ f10 f86)) (define-fun f89 () Arctic (+ f11 f87)) (define-fun f90 () Arctic (+ (* f0 f82) (* f1 f84))) (define-fun f91 () Arctic (+ (* f0 f83) (* f1 f85))) (define-fun f92 () Arctic (+ (* f2 f82) (* f3 f84))) (define-fun f93 () Arctic (+ (* f2 f83) (* f3 f85))) (define-fun f94 () Arctic (+ (* f0 f88) (* f1 f89))) (define-fun f95 () Arctic (+ (* f2 f88) (* f3 f89))) (define-fun f96 () Arctic (+ f4 f94)) (define-fun f97 () Arctic (+ f5 f95)) (define-fun f98 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f99 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f100 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f101 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f102 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f103 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f104 () Arctic (+ f16 f102)) (define-fun f105 () Arctic (+ f17 f103)) (define-fun f106 () Arctic (+ (* f12 f98) (* f13 f100))) (define-fun f107 () Arctic (+ (* f12 f99) (* f13 f101))) (define-fun f108 () Arctic (+ (* f14 f98) (* f15 f100))) (define-fun f109 () Arctic (+ (* f14 f99) (* f15 f101))) (define-fun f110 () Arctic (+ (* f12 f104) (* f13 f105))) (define-fun f111 () Arctic (+ (* f14 f104) (* f15 f105))) (define-fun f112 () Arctic (+ f16 f110)) (define-fun f113 () Arctic (+ f17 f111)) (define-fun f114 () Arctic (+ (* f6 f106) (* f7 f108))) (define-fun f115 () Arctic (+ (* f6 f107) (* f7 f109))) (define-fun f116 () Arctic (+ (* f8 f106) (* f9 f108))) (define-fun f117 () Arctic (+ (* f8 f107) (* f9 f109))) (define-fun f118 () Arctic (+ (* f6 f112) (* f7 f113))) (define-fun f119 () Arctic (+ (* f8 f112) (* f9 f113))) (define-fun f120 () Arctic (+ f10 f118)) (define-fun f121 () Arctic (+ f11 f119)) (define-fun f122 () Arctic (+ (* f0 f114) (* f1 f116))) (define-fun f123 () Arctic (+ (* f0 f115) (* f1 f117))) (define-fun f124 () Arctic (+ (* f2 f114) (* f3 f116))) (define-fun f125 () Arctic (+ (* f2 f115) (* f3 f117))) (define-fun f126 () Arctic (+ (* f0 f120) (* f1 f121))) (define-fun f127 () Arctic (+ (* f2 f120) (* f3 f121))) (define-fun f128 () Arctic (+ f4 f126)) (define-fun f129 () Arctic (+ f5 f127)) (define-fun f130 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f131 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f132 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f133 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f134 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f135 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f136 () Arctic (+ f16 f134)) (define-fun f137 () Arctic (+ f17 f135)) (define-fun f138 () Arctic (+ (* f12 f130) (* f13 f132))) (define-fun f139 () Arctic (+ (* f12 f131) (* f13 f133))) (define-fun f140 () Arctic (+ (* f14 f130) (* f15 f132))) (define-fun f141 () Arctic (+ (* f14 f131) (* f15 f133))) (define-fun f142 () Arctic (+ (* f12 f136) (* f13 f137))) (define-fun f143 () Arctic (+ (* f14 f136) (* f15 f137))) (define-fun f144 () Arctic (+ f16 f142)) (define-fun f145 () Arctic (+ f17 f143)) (define-fun f146 () Arctic (+ (* f12 f138) (* f13 f140))) (define-fun f147 () Arctic (+ (* f12 f139) (* f13 f141))) (define-fun f148 () Arctic (+ (* f14 f138) (* f15 f140))) (define-fun f149 () Arctic (+ (* f14 f139) (* f15 f141))) (define-fun f150 () Arctic (+ (* f12 f144) (* f13 f145))) (define-fun f151 () Arctic (+ (* f14 f144) (* f15 f145))) (define-fun f152 () Arctic (+ f16 f150)) (define-fun f153 () Arctic (+ f17 f151)) (define-fun f154 () Arctic (+ (* f12 f146) (* f13 f148))) (define-fun f155 () Arctic (+ (* f12 f147) (* f13 f149))) (define-fun f156 () Arctic (+ (* f14 f146) (* f15 f148))) (define-fun f157 () Arctic (+ (* f14 f147) (* f15 f149))) (define-fun f158 () Arctic (+ (* f12 f152) (* f13 f153))) (define-fun f159 () Arctic (+ (* f14 f152) (* f15 f153))) (define-fun f160 () Arctic (+ f16 f158)) (define-fun f161 () Arctic (+ f17 f159)) (define-fun f162 () Arctic (+ (* f0 f154) (* f1 f156))) (define-fun f163 () Arctic (+ (* f0 f155) (* f1 f157))) (define-fun f164 () Arctic (+ (* f2 f154) (* f3 f156))) (define-fun f165 () Arctic (+ (* f2 f155) (* f3 f157))) (define-fun f166 () Arctic (+ (* f0 f160) (* f1 f161))) (define-fun f167 () Arctic (+ (* f2 f160) (* f3 f161))) (define-fun f168 () Arctic (+ f4 f166)) (define-fun f169 () Arctic (+ f5 f167)) (define-fun f170 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f171 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f172 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f173 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f174 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f175 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f176 () Arctic (+ f16 f174)) (define-fun f177 () Arctic (+ f17 f175)) (define-fun f178 () Arctic (+ (* f12 f170) (* f13 f172))) (define-fun f179 () Arctic (+ (* f12 f171) (* f13 f173))) (define-fun f180 () Arctic (+ (* f14 f170) (* f15 f172))) (define-fun f181 () Arctic (+ (* f14 f171) (* f15 f173))) (define-fun f182 () Arctic (+ (* f12 f176) (* f13 f177))) (define-fun f183 () Arctic (+ (* f14 f176) (* f15 f177))) (define-fun f184 () Arctic (+ f16 f182)) (define-fun f185 () Arctic (+ f17 f183)) (define-fun f186 () Arctic (+ (* f6 f178) (* f7 f180))) (define-fun f187 () Arctic (+ (* f6 f179) (* f7 f181))) (define-fun f188 () Arctic (+ (* f8 f178) (* f9 f180))) (define-fun f189 () Arctic (+ (* f8 f179) (* f9 f181))) (define-fun f190 () Arctic (+ (* f6 f184) (* f7 f185))) (define-fun f191 () Arctic (+ (* f8 f184) (* f9 f185))) (define-fun f192 () Arctic (+ f10 f190)) (define-fun f193 () Arctic (+ f11 f191)) (define-fun f194 () Arctic (+ (* f0 f186) (* f1 f188))) (define-fun f195 () Arctic (+ (* f0 f187) (* f1 f189))) (define-fun f196 () Arctic (+ (* f2 f186) (* f3 f188))) (define-fun f197 () Arctic (+ (* f2 f187) (* f3 f189))) (define-fun f198 () Arctic (+ (* f0 f192) (* f1 f193))) (define-fun f199 () Arctic (+ (* f2 f192) (* f3 f193))) (define-fun f200 () Arctic (+ f4 f198)) (define-fun f201 () Arctic (+ f5 f199)) (define-fun f202 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f203 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f204 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f205 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f206 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f207 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f208 () Arctic (+ f16 f206)) (define-fun f209 () Arctic (+ f17 f207)) (define-fun f210 () Arctic (+ (* f6 f202) (* f7 f204))) (define-fun f211 () Arctic (+ (* f6 f203) (* f7 f205))) (define-fun f212 () Arctic (+ (* f8 f202) (* f9 f204))) (define-fun f213 () Arctic (+ (* f8 f203) (* f9 f205))) (define-fun f214 () Arctic (+ (* f6 f208) (* f7 f209))) (define-fun f215 () Arctic (+ (* f8 f208) (* f9 f209))) (define-fun f216 () Arctic (+ f10 f214)) (define-fun f217 () Arctic (+ f11 f215)) (define-fun f218 () Arctic (+ (* f0 f210) (* f1 f212))) (define-fun f219 () Arctic (+ (* f0 f211) (* f1 f213))) (define-fun f220 () Arctic (+ (* f2 f210) (* f3 f212))) (define-fun f221 () Arctic (+ (* f2 f211) (* f3 f213))) (define-fun f222 () Arctic (+ (* f0 f216) (* f1 f217))) (define-fun f223 () Arctic (+ (* f2 f216) (* f3 f217))) (define-fun f224 () Arctic (+ f4 f222)) (define-fun f225 () Arctic (+ f5 f223)) (define-fun f226 () Arctic (+ (* f0 f6) (* f1 f8))) (define-fun f227 () Arctic (+ (* f0 f7) (* f1 f9))) (define-fun f228 () Arctic (+ (* f2 f6) (* f3 f8))) (define-fun f229 () Arctic (+ (* f2 f7) (* f3 f9))) (define-fun f230 () Arctic (+ (* f0 f10) (* f1 f11))) (define-fun f231 () Arctic (+ (* f2 f10) (* f3 f11))) (define-fun f232 () Arctic (+ f4 f230)) (define-fun f233 () Arctic (+ f5 f231)) (define-fun f234 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f235 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f236 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f237 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f238 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f239 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f240 () Arctic (+ f16 f238)) (define-fun f241 () Arctic (+ f17 f239)) (define-fun f242 () Arctic (+ (* f6 f234) (* f7 f236))) (define-fun f243 () Arctic (+ (* f6 f235) (* f7 f237))) (define-fun f244 () Arctic (+ (* f8 f234) (* f9 f236))) (define-fun f245 () Arctic (+ (* f8 f235) (* f9 f237))) (define-fun f246 () Arctic (+ (* f6 f240) (* f7 f241))) (define-fun f247 () Arctic (+ (* f8 f240) (* f9 f241))) (define-fun f248 () Arctic (+ f10 f246)) (define-fun f249 () Arctic (+ f11 f247)) (define-fun f250 () Arctic (+ (* f0 f242) (* f1 f244))) (define-fun f251 () Arctic (+ (* f0 f243) (* f1 f245))) (define-fun f252 () Arctic (+ (* f2 f242) (* f3 f244))) (define-fun f253 () Arctic (+ (* f2 f243) (* f3 f245))) (define-fun f254 () Arctic (+ (* f0 f248) (* f1 f249))) (define-fun f255 () Arctic (+ (* f2 f248) (* f3 f249))) (define-fun f256 () Arctic (+ f4 f254)) (define-fun f257 () Arctic (+ f5 f255)) (define-fun f258 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f259 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f260 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f261 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f262 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f263 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f264 () Arctic (+ f16 f262)) (define-fun f265 () Arctic (+ f17 f263)) (define-fun f266 () Arctic (+ (* f6 f258) (* f7 f260))) (define-fun f267 () Arctic (+ (* f6 f259) (* f7 f261))) (define-fun f268 () Arctic (+ (* f8 f258) (* f9 f260))) (define-fun f269 () Arctic (+ (* f8 f259) (* f9 f261))) (define-fun f270 () Arctic (+ (* f6 f264) (* f7 f265))) (define-fun f271 () Arctic (+ (* f8 f264) (* f9 f265))) (define-fun f272 () Arctic (+ f10 f270)) (define-fun f273 () Arctic (+ f11 f271)) (define-fun f274 () Arctic (+ (* f12 f266) (* f13 f268))) (define-fun f275 () Arctic (+ (* f12 f267) (* f13 f269))) (define-fun f276 () Arctic (+ (* f14 f266) (* f15 f268))) (define-fun f277 () Arctic (+ (* f14 f267) (* f15 f269))) (define-fun f278 () Arctic (+ (* f12 f272) (* f13 f273))) (define-fun f279 () Arctic (+ (* f14 f272) (* f15 f273))) (define-fun f280 () Arctic (+ f16 f278)) (define-fun f281 () Arctic (+ f17 f279)) (define-fun f282 () Arctic (+ (* f12 f274) (* f13 f276))) (define-fun f283 () Arctic (+ (* f12 f275) (* f13 f277))) (define-fun f284 () Arctic (+ (* f14 f274) (* f15 f276))) (define-fun f285 () Arctic (+ (* f14 f275) (* f15 f277))) (define-fun f286 () Arctic (+ (* f12 f280) (* f13 f281))) (define-fun f287 () Arctic (+ (* f14 f280) (* f15 f281))) (define-fun f288 () Arctic (+ f16 f286)) (define-fun f289 () Arctic (+ f17 f287)) (define-fun f290 () Arctic (+ (* f12 f282) (* f13 f284))) (define-fun f291 () Arctic (+ (* f12 f283) (* f13 f285))) (define-fun f292 () Arctic (+ (* f14 f282) (* f15 f284))) (define-fun f293 () Arctic (+ (* f14 f283) (* f15 f285))) (define-fun f294 () Arctic (+ (* f12 f288) (* f13 f289))) (define-fun f295 () Arctic (+ (* f14 f288) (* f15 f289))) (define-fun f296 () Arctic (+ f16 f294)) (define-fun f297 () Arctic (+ f17 f295)) (define-fun f298 () Arctic (+ (* f12 f290) (* f13 f292))) (define-fun f299 () Arctic (+ (* f12 f291) (* f13 f293))) (define-fun f300 () Arctic (+ (* f14 f290) (* f15 f292))) (define-fun f301 () Arctic (+ (* f14 f291) (* f15 f293))) (define-fun f302 () Arctic (+ (* f12 f296) (* f13 f297))) (define-fun f303 () Arctic (+ (* f14 f296) (* f15 f297))) (define-fun f304 () Arctic (+ f16 f302)) (define-fun f305 () Arctic (+ f17 f303)) (define-fun f306 () Arctic (+ (* f0 f298) (* f1 f300))) (define-fun f307 () Arctic (+ (* f0 f299) (* f1 f301))) (define-fun f308 () Arctic (+ (* f2 f298) (* f3 f300))) (define-fun f309 () Arctic (+ (* f2 f299) (* f3 f301))) (define-fun f310 () Arctic (+ (* f0 f304) (* f1 f305))) (define-fun f311 () Arctic (+ (* f2 f304) (* f3 f305))) (define-fun f312 () Arctic (+ f4 f310)) (define-fun f313 () Arctic (+ f5 f311)) (define-fun f314 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f315 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f316 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f317 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f318 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f319 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f320 () Arctic (+ f16 f318)) (define-fun f321 () Arctic (+ f17 f319)) (define-fun f322 () Arctic (+ (* f12 f314) (* f13 f316))) (define-fun f323 () Arctic (+ (* f12 f315) (* f13 f317))) (define-fun f324 () Arctic (+ (* f14 f314) (* f15 f316))) (define-fun f325 () Arctic (+ (* f14 f315) (* f15 f317))) (define-fun f326 () Arctic (+ (* f12 f320) (* f13 f321))) (define-fun f327 () Arctic (+ (* f14 f320) (* f15 f321))) (define-fun f328 () Arctic (+ f16 f326)) (define-fun f329 () Arctic (+ f17 f327)) (define-fun f330 () Arctic (+ (* f12 f322) (* f13 f324))) (define-fun f331 () Arctic (+ (* f12 f323) (* f13 f325))) (define-fun f332 () Arctic (+ (* f14 f322) (* f15 f324))) (define-fun f333 () Arctic (+ (* f14 f323) (* f15 f325))) (define-fun f334 () Arctic (+ (* f12 f328) (* f13 f329))) (define-fun f335 () Arctic (+ (* f14 f328) (* f15 f329))) (define-fun f336 () Arctic (+ f16 f334)) (define-fun f337 () Arctic (+ f17 f335)) (define-fun f338 () Arctic (+ (* f12 f330) (* f13 f332))) (define-fun f339 () Arctic (+ (* f12 f331) (* f13 f333))) (define-fun f340 () Arctic (+ (* f14 f330) (* f15 f332))) (define-fun f341 () Arctic (+ (* f14 f331) (* f15 f333))) (define-fun f342 () Arctic (+ (* f12 f336) (* f13 f337))) (define-fun f343 () Arctic (+ (* f14 f336) (* f15 f337))) (define-fun f344 () Arctic (+ f16 f342)) (define-fun f345 () Arctic (+ f17 f343)) (define-fun f346 () Arctic (+ (* f6 f338) (* f7 f340))) (define-fun f347 () Arctic (+ (* f6 f339) (* f7 f341))) (define-fun f348 () Arctic (+ (* f8 f338) (* f9 f340))) (define-fun f349 () Arctic (+ (* f8 f339) (* f9 f341))) (define-fun f350 () Arctic (+ (* f6 f344) (* f7 f345))) (define-fun f351 () Arctic (+ (* f8 f344) (* f9 f345))) (define-fun f352 () Arctic (+ f10 f350)) (define-fun f353 () Arctic (+ f11 f351)) (define-fun f354 () Arctic (+ (* f12 f346) (* f13 f348))) (define-fun f355 () Arctic (+ (* f12 f347) (* f13 f349))) (define-fun f356 () Arctic (+ (* f14 f346) (* f15 f348))) (define-fun f357 () Arctic (+ (* f14 f347) (* f15 f349))) (define-fun f358 () Arctic (+ (* f12 f352) (* f13 f353))) (define-fun f359 () Arctic (+ (* f14 f352) (* f15 f353))) (define-fun f360 () Arctic (+ f16 f358)) (define-fun f361 () Arctic (+ f17 f359)) (define-fun f362 () Arctic (+ (* f12 f354) (* f13 f356))) (define-fun f363 () Arctic (+ (* f12 f355) (* f13 f357))) (define-fun f364 () Arctic (+ (* f14 f354) (* f15 f356))) (define-fun f365 () Arctic (+ (* f14 f355) (* f15 f357))) (define-fun f366 () Arctic (+ (* f12 f360) (* f13 f361))) (define-fun f367 () Arctic (+ (* f14 f360) (* f15 f361))) (define-fun f368 () Arctic (+ f16 f366)) (define-fun f369 () Arctic (+ f17 f367)) (define-fun f370 () Arctic (+ (* f12 f362) (* f13 f364))) (define-fun f371 () Arctic (+ (* f12 f363) (* f13 f365))) (define-fun f372 () Arctic (+ (* f14 f362) (* f15 f364))) (define-fun f373 () Arctic (+ (* f14 f363) (* f15 f365))) (define-fun f374 () Arctic (+ (* f12 f368) (* f13 f369))) (define-fun f375 () Arctic (+ (* f14 f368) (* f15 f369))) (define-fun f376 () Arctic (+ f16 f374)) (define-fun f377 () Arctic (+ f17 f375)) (define-fun f378 () Arctic (+ (* f12 f370) (* f13 f372))) (define-fun f379 () Arctic (+ (* f12 f371) (* f13 f373))) (define-fun f380 () Arctic (+ (* f14 f370) (* f15 f372))) (define-fun f381 () Arctic (+ (* f14 f371) (* f15 f373))) (define-fun f382 () Arctic (+ (* f12 f376) (* f13 f377))) (define-fun f383 () Arctic (+ (* f14 f376) (* f15 f377))) (define-fun f384 () Arctic (+ f16 f382)) (define-fun f385 () Arctic (+ f17 f383)) (define-fun f386 () Arctic (+ (* f6 f378) (* f7 f380))) (define-fun f387 () Arctic (+ (* f6 f379) (* f7 f381))) (define-fun f388 () Arctic (+ (* f8 f378) (* f9 f380))) (define-fun f389 () Arctic (+ (* f8 f379) (* f9 f381))) (define-fun f390 () Arctic (+ (* f6 f384) (* f7 f385))) (define-fun f391 () Arctic (+ (* f8 f384) (* f9 f385))) (define-fun f392 () Arctic (+ f10 f390)) (define-fun f393 () Arctic (+ f11 f391)) (define-fun f394 () Arctic (+ (* f12 f386) (* f13 f388))) (define-fun f395 () Arctic (+ (* f12 f387) (* f13 f389))) (define-fun f396 () Arctic (+ (* f14 f386) (* f15 f388))) (define-fun f397 () Arctic (+ (* f14 f387) (* f15 f389))) (define-fun f398 () Arctic (+ (* f12 f392) (* f13 f393))) (define-fun f399 () Arctic (+ (* f14 f392) (* f15 f393))) (define-fun f400 () Arctic (+ f16 f398)) (define-fun f401 () Arctic (+ f17 f399)) (define-fun f402 () Arctic (+ (* f6 f394) (* f7 f396))) (define-fun f403 () Arctic (+ (* f6 f395) (* f7 f397))) (define-fun f404 () Arctic (+ (* f8 f394) (* f9 f396))) (define-fun f405 () Arctic (+ (* f8 f395) (* f9 f397))) (define-fun f406 () Arctic (+ (* f6 f400) (* f7 f401))) (define-fun f407 () Arctic (+ (* f8 f400) (* f9 f401))) (define-fun f408 () Arctic (+ f10 f406)) (define-fun f409 () Arctic (+ f11 f407)) (define-fun f410 () Arctic (+ (* f12 f402) (* f13 f404))) (define-fun f411 () Arctic (+ (* f12 f403) (* f13 f405))) (define-fun f412 () Arctic (+ (* f14 f402) (* f15 f404))) (define-fun f413 () Arctic (+ (* f14 f403) (* f15 f405))) (define-fun f414 () Arctic (+ (* f12 f408) (* f13 f409))) (define-fun f415 () Arctic (+ (* f14 f408) (* f15 f409))) (define-fun f416 () Arctic (+ f16 f414)) (define-fun f417 () Arctic (+ f17 f415)) (define-fun f418 () Arctic (+ (* f12 f410) (* f13 f412))) (define-fun f419 () Arctic (+ (* f12 f411) (* f13 f413))) (define-fun f420 () Arctic (+ (* f14 f410) (* f15 f412))) (define-fun f421 () Arctic (+ (* f14 f411) (* f15 f413))) (define-fun f422 () Arctic (+ (* f12 f416) (* f13 f417))) (define-fun f423 () Arctic (+ (* f14 f416) (* f15 f417))) (define-fun f424 () Arctic (+ f16 f422)) (define-fun f425 () Arctic (+ f17 f423)) (define-fun f426 () Arctic (+ (* f12 f418) (* f13 f420))) (define-fun f427 () Arctic (+ (* f12 f419) (* f13 f421))) (define-fun f428 () Arctic (+ (* f14 f418) (* f15 f420))) (define-fun f429 () Arctic (+ (* f14 f419) (* f15 f421))) (define-fun f430 () Arctic (+ (* f12 f424) (* f13 f425))) (define-fun f431 () Arctic (+ (* f14 f424) (* f15 f425))) (define-fun f432 () Arctic (+ f16 f430)) (define-fun f433 () Arctic (+ f17 f431)) (define-fun f434 () Arctic (+ (* f6 f426) (* f7 f428))) (define-fun f435 () Arctic (+ (* f6 f427) (* f7 f429))) (define-fun f436 () Arctic (+ (* f8 f426) (* f9 f428))) (define-fun f437 () Arctic (+ (* f8 f427) (* f9 f429))) (define-fun f438 () Arctic (+ (* f6 f432) (* f7 f433))) (define-fun f439 () Arctic (+ (* f8 f432) (* f9 f433))) (define-fun f440 () Arctic (+ f10 f438)) (define-fun f441 () Arctic (+ f11 f439)) (define-fun f442 () Arctic (+ (* f12 f434) (* f13 f436))) (define-fun f443 () Arctic (+ (* f12 f435) (* f13 f437))) (define-fun f444 () Arctic (+ (* f14 f434) (* f15 f436))) (define-fun f445 () Arctic (+ (* f14 f435) (* f15 f437))) (define-fun f446 () Arctic (+ (* f12 f440) (* f13 f441))) (define-fun f447 () Arctic (+ (* f14 f440) (* f15 f441))) (define-fun f448 () Arctic (+ f16 f446)) (define-fun f449 () Arctic (+ f17 f447)) (define-fun f450 () Arctic (+ (* f12 f442) (* f13 f444))) (define-fun f451 () Arctic (+ (* f12 f443) (* f13 f445))) (define-fun f452 () Arctic (+ (* f14 f442) (* f15 f444))) (define-fun f453 () Arctic (+ (* f14 f443) (* f15 f445))) (define-fun f454 () Arctic (+ (* f12 f448) (* f13 f449))) (define-fun f455 () Arctic (+ (* f14 f448) (* f15 f449))) (define-fun f456 () Arctic (+ f16 f454)) (define-fun f457 () Arctic (+ f17 f455)) (define-fun f458 () Arctic (+ (* f12 f450) (* f13 f452))) (define-fun f459 () Arctic (+ (* f12 f451) (* f13 f453))) (define-fun f460 () Arctic (+ (* f14 f450) (* f15 f452))) (define-fun f461 () Arctic (+ (* f14 f451) (* f15 f453))) (define-fun f462 () Arctic (+ (* f12 f456) (* f13 f457))) (define-fun f463 () Arctic (+ (* f14 f456) (* f15 f457))) (define-fun f464 () Arctic (+ f16 f462)) (define-fun f465 () Arctic (+ f17 f463)) (define-fun f466 () Arctic (+ (* f12 f458) (* f13 f460))) (define-fun f467 () Arctic (+ (* f12 f459) (* f13 f461))) (define-fun f468 () Arctic (+ (* f14 f458) (* f15 f460))) (define-fun f469 () Arctic (+ (* f14 f459) (* f15 f461))) (define-fun f470 () Arctic (+ (* f12 f464) (* f13 f465))) (define-fun f471 () Arctic (+ (* f14 f464) (* f15 f465))) (define-fun f472 () Arctic (+ f16 f470)) (define-fun f473 () Arctic (+ f17 f471)) (define-fun f474 () Arctic (+ (* f0 f466) (* f1 f468))) (define-fun f475 () Arctic (+ (* f0 f467) (* f1 f469))) (define-fun f476 () Arctic (+ (* f2 f466) (* f3 f468))) (define-fun f477 () Arctic (+ (* f2 f467) (* f3 f469))) (define-fun f478 () Arctic (+ (* f0 f472) (* f1 f473))) (define-fun f479 () Arctic (+ (* f2 f472) (* f3 f473))) (define-fun f480 () Arctic (+ f4 f478)) (define-fun f481 () Arctic (+ f5 f479)) (define-fun f482 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f483 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f484 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f485 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f486 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f487 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f488 () Arctic (+ f16 f486)) (define-fun f489 () Arctic (+ f17 f487)) (define-fun f490 () Arctic (+ (* f6 f482) (* f7 f484))) (define-fun f491 () Arctic (+ (* f6 f483) (* f7 f485))) (define-fun f492 () Arctic (+ (* f8 f482) (* f9 f484))) (define-fun f493 () Arctic (+ (* f8 f483) (* f9 f485))) (define-fun f494 () Arctic (+ (* f6 f488) (* f7 f489))) (define-fun f495 () Arctic (+ (* f8 f488) (* f9 f489))) (define-fun f496 () Arctic (+ f10 f494)) (define-fun f497 () Arctic (+ f11 f495)) (define-fun f498 () Arctic (+ (* f12 f490) (* f13 f492))) (define-fun f499 () Arctic (+ (* f12 f491) (* f13 f493))) (define-fun f500 () Arctic (+ (* f14 f490) (* f15 f492))) (define-fun f501 () Arctic (+ (* f14 f491) (* f15 f493))) (define-fun f502 () Arctic (+ (* f12 f496) (* f13 f497))) (define-fun f503 () Arctic (+ (* f14 f496) (* f15 f497))) (define-fun f504 () Arctic (+ f16 f502)) (define-fun f505 () Arctic (+ f17 f503)) (define-fun f506 () Arctic (+ (* f12 f498) (* f13 f500))) (define-fun f507 () Arctic (+ (* f12 f499) (* f13 f501))) (define-fun f508 () Arctic (+ (* f14 f498) (* f15 f500))) (define-fun f509 () Arctic (+ (* f14 f499) (* f15 f501))) (define-fun f510 () Arctic (+ (* f12 f504) (* f13 f505))) (define-fun f511 () Arctic (+ (* f14 f504) (* f15 f505))) (define-fun f512 () Arctic (+ f16 f510)) (define-fun f513 () Arctic (+ f17 f511)) (define-fun f514 () Arctic (+ (* f12 f506) (* f13 f508))) (define-fun f515 () Arctic (+ (* f12 f507) (* f13 f509))) (define-fun f516 () Arctic (+ (* f14 f506) (* f15 f508))) (define-fun f517 () Arctic (+ (* f14 f507) (* f15 f509))) (define-fun f518 () Arctic (+ (* f12 f512) (* f13 f513))) (define-fun f519 () Arctic (+ (* f14 f512) (* f15 f513))) (define-fun f520 () Arctic (+ f16 f518)) (define-fun f521 () Arctic (+ f17 f519)) (define-fun f522 () Arctic (+ (* f12 f514) (* f13 f516))) (define-fun f523 () Arctic (+ (* f12 f515) (* f13 f517))) (define-fun f524 () Arctic (+ (* f14 f514) (* f15 f516))) (define-fun f525 () Arctic (+ (* f14 f515) (* f15 f517))) (define-fun f526 () Arctic (+ (* f12 f520) (* f13 f521))) (define-fun f527 () Arctic (+ (* f14 f520) (* f15 f521))) (define-fun f528 () Arctic (+ f16 f526)) (define-fun f529 () Arctic (+ f17 f527)) (define-fun f530 () Arctic (+ (* f0 f522) (* f1 f524))) (define-fun f531 () Arctic (+ (* f0 f523) (* f1 f525))) (define-fun f532 () Arctic (+ (* f2 f522) (* f3 f524))) (define-fun f533 () Arctic (+ (* f2 f523) (* f3 f525))) (define-fun f534 () Arctic (+ (* f0 f528) (* f1 f529))) (define-fun f535 () Arctic (+ (* f2 f528) (* f3 f529))) (define-fun f536 () Arctic (+ f4 f534)) (define-fun f537 () Arctic (+ f5 f535)) (define-fun f538 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f539 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f540 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f541 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f542 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f543 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f544 () Arctic (+ f16 f542)) (define-fun f545 () Arctic (+ f17 f543)) (define-fun f546 () Arctic (+ (* f12 f538) (* f13 f540))) (define-fun f547 () Arctic (+ (* f12 f539) (* f13 f541))) (define-fun f548 () Arctic (+ (* f14 f538) (* f15 f540))) (define-fun f549 () Arctic (+ (* f14 f539) (* f15 f541))) (define-fun f550 () Arctic (+ (* f12 f544) (* f13 f545))) (define-fun f551 () Arctic (+ (* f14 f544) (* f15 f545))) (define-fun f552 () Arctic (+ f16 f550)) (define-fun f553 () Arctic (+ f17 f551)) (define-fun f554 () Arctic (+ (* f12 f546) (* f13 f548))) (define-fun f555 () Arctic (+ (* f12 f547) (* f13 f549))) (define-fun f556 () Arctic (+ (* f14 f546) (* f15 f548))) (define-fun f557 () Arctic (+ (* f14 f547) (* f15 f549))) (define-fun f558 () Arctic (+ (* f12 f552) (* f13 f553))) (define-fun f559 () Arctic (+ (* f14 f552) (* f15 f553))) (define-fun f560 () Arctic (+ f16 f558)) (define-fun f561 () Arctic (+ f17 f559)) (define-fun f562 () Arctic (+ (* f12 f554) (* f13 f556))) (define-fun f563 () Arctic (+ (* f12 f555) (* f13 f557))) (define-fun f564 () Arctic (+ (* f14 f554) (* f15 f556))) (define-fun f565 () Arctic (+ (* f14 f555) (* f15 f557))) (define-fun f566 () Arctic (+ (* f12 f560) (* f13 f561))) (define-fun f567 () Arctic (+ (* f14 f560) (* f15 f561))) (define-fun f568 () Arctic (+ f16 f566)) (define-fun f569 () Arctic (+ f17 f567)) (define-fun f570 () Arctic (+ (* f6 f562) (* f7 f564))) (define-fun f571 () Arctic (+ (* f6 f563) (* f7 f565))) (define-fun f572 () Arctic (+ (* f8 f562) (* f9 f564))) (define-fun f573 () Arctic (+ (* f8 f563) (* f9 f565))) (define-fun f574 () Arctic (+ (* f6 f568) (* f7 f569))) (define-fun f575 () Arctic (+ (* f8 f568) (* f9 f569))) (define-fun f576 () Arctic (+ f10 f574)) (define-fun f577 () Arctic (+ f11 f575)) (define-fun f578 () Arctic (+ (* f12 f570) (* f13 f572))) (define-fun f579 () Arctic (+ (* f12 f571) (* f13 f573))) (define-fun f580 () Arctic (+ (* f14 f570) (* f15 f572))) (define-fun f581 () Arctic (+ (* f14 f571) (* f15 f573))) (define-fun f582 () Arctic (+ (* f12 f576) (* f13 f577))) (define-fun f583 () Arctic (+ (* f14 f576) (* f15 f577))) (define-fun f584 () Arctic (+ f16 f582)) (define-fun f585 () Arctic (+ f17 f583)) (define-fun f586 () Arctic (+ (* f12 f578) (* f13 f580))) (define-fun f587 () Arctic (+ (* f12 f579) (* f13 f581))) (define-fun f588 () Arctic (+ (* f14 f578) (* f15 f580))) (define-fun f589 () Arctic (+ (* f14 f579) (* f15 f581))) (define-fun f590 () Arctic (+ (* f12 f584) (* f13 f585))) (define-fun f591 () Arctic (+ (* f14 f584) (* f15 f585))) (define-fun f592 () Arctic (+ f16 f590)) (define-fun f593 () Arctic (+ f17 f591)) (define-fun f594 () Arctic (+ (* f12 f586) (* f13 f588))) (define-fun f595 () Arctic (+ (* f12 f587) (* f13 f589))) (define-fun f596 () Arctic (+ (* f14 f586) (* f15 f588))) (define-fun f597 () Arctic (+ (* f14 f587) (* f15 f589))) (define-fun f598 () Arctic (+ (* f12 f592) (* f13 f593))) (define-fun f599 () Arctic (+ (* f14 f592) (* f15 f593))) (define-fun f600 () Arctic (+ f16 f598)) (define-fun f601 () Arctic (+ f17 f599)) (define-fun f602 () Arctic (+ (* f12 f594) (* f13 f596))) (define-fun f603 () Arctic (+ (* f12 f595) (* f13 f597))) (define-fun f604 () Arctic (+ (* f14 f594) (* f15 f596))) (define-fun f605 () Arctic (+ (* f14 f595) (* f15 f597))) (define-fun f606 () Arctic (+ (* f12 f600) (* f13 f601))) (define-fun f607 () Arctic (+ (* f14 f600) (* f15 f601))) (define-fun f608 () Arctic (+ f16 f606)) (define-fun f609 () Arctic (+ f17 f607)) (define-fun f610 () Arctic (+ (* f6 f602) (* f7 f604))) (define-fun f611 () Arctic (+ (* f6 f603) (* f7 f605))) (define-fun f612 () Arctic (+ (* f8 f602) (* f9 f604))) (define-fun f613 () Arctic (+ (* f8 f603) (* f9 f605))) (define-fun f614 () Arctic (+ (* f6 f608) (* f7 f609))) (define-fun f615 () Arctic (+ (* f8 f608) (* f9 f609))) (define-fun f616 () Arctic (+ f10 f614)) (define-fun f617 () Arctic (+ f11 f615)) (define-fun f618 () Arctic (+ (* f12 f610) (* f13 f612))) (define-fun f619 () Arctic (+ (* f12 f611) (* f13 f613))) (define-fun f620 () Arctic (+ (* f14 f610) (* f15 f612))) (define-fun f621 () Arctic (+ (* f14 f611) (* f15 f613))) (define-fun f622 () Arctic (+ (* f12 f616) (* f13 f617))) (define-fun f623 () Arctic (+ (* f14 f616) (* f15 f617))) (define-fun f624 () Arctic (+ f16 f622)) (define-fun f625 () Arctic (+ f17 f623)) (define-fun f626 () Arctic (+ (* f6 f618) (* f7 f620))) (define-fun f627 () Arctic (+ (* f6 f619) (* f7 f621))) (define-fun f628 () Arctic (+ (* f8 f618) (* f9 f620))) (define-fun f629 () Arctic (+ (* f8 f619) (* f9 f621))) (define-fun f630 () Arctic (+ (* f6 f624) (* f7 f625))) (define-fun f631 () Arctic (+ (* f8 f624) (* f9 f625))) (define-fun f632 () Arctic (+ f10 f630)) (define-fun f633 () Arctic (+ f11 f631)) (define-fun f634 () Arctic (+ (* f12 f626) (* f13 f628))) (define-fun f635 () Arctic (+ (* f12 f627) (* f13 f629))) (define-fun f636 () Arctic (+ (* f14 f626) (* f15 f628))) (define-fun f637 () Arctic (+ (* f14 f627) (* f15 f629))) (define-fun f638 () Arctic (+ (* f12 f632) (* f13 f633))) (define-fun f639 () Arctic (+ (* f14 f632) (* f15 f633))) (define-fun f640 () Arctic (+ f16 f638)) (define-fun f641 () Arctic (+ f17 f639)) (define-fun f642 () Arctic (+ (* f12 f634) (* f13 f636))) (define-fun f643 () Arctic (+ (* f12 f635) (* f13 f637))) (define-fun f644 () Arctic (+ (* f14 f634) (* f15 f636))) (define-fun f645 () Arctic (+ (* f14 f635) (* f15 f637))) (define-fun f646 () Arctic (+ (* f12 f640) (* f13 f641))) (define-fun f647 () Arctic (+ (* f14 f640) (* f15 f641))) (define-fun f648 () Arctic (+ f16 f646)) (define-fun f649 () Arctic (+ f17 f647)) (define-fun f650 () Arctic (+ (* f12 f642) (* f13 f644))) (define-fun f651 () Arctic (+ (* f12 f643) (* f13 f645))) (define-fun f652 () Arctic (+ (* f14 f642) (* f15 f644))) (define-fun f653 () Arctic (+ (* f14 f643) (* f15 f645))) (define-fun f654 () Arctic (+ (* f12 f648) (* f13 f649))) (define-fun f655 () Arctic (+ (* f14 f648) (* f15 f649))) (define-fun f656 () Arctic (+ f16 f654)) (define-fun f657 () Arctic (+ f17 f655)) (define-fun f658 () Arctic (+ (* f0 f650) (* f1 f652))) (define-fun f659 () Arctic (+ (* f0 f651) (* f1 f653))) (define-fun f660 () Arctic (+ (* f2 f650) (* f3 f652))) (define-fun f661 () Arctic (+ (* f2 f651) (* f3 f653))) (define-fun f662 () Arctic (+ (* f0 f656) (* f1 f657))) (define-fun f663 () Arctic (+ (* f2 f656) (* f3 f657))) (define-fun f664 () Arctic (+ f4 f662)) (define-fun f665 () Arctic (+ f5 f663)) (define-fun f666 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f667 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f668 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f669 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f670 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f671 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f672 () Arctic (+ f16 f670)) (define-fun f673 () Arctic (+ f17 f671)) (define-fun f674 () Arctic (+ (* f6 f666) (* f7 f668))) (define-fun f675 () Arctic (+ (* f6 f667) (* f7 f669))) (define-fun f676 () Arctic (+ (* f8 f666) (* f9 f668))) (define-fun f677 () Arctic (+ (* f8 f667) (* f9 f669))) (define-fun f678 () Arctic (+ (* f6 f672) (* f7 f673))) (define-fun f679 () Arctic (+ (* f8 f672) (* f9 f673))) (define-fun f680 () Arctic (+ f10 f678)) (define-fun f681 () Arctic (+ f11 f679)) (define-fun f682 () Arctic (+ (* f12 f674) (* f13 f676))) (define-fun f683 () Arctic (+ (* f12 f675) (* f13 f677))) (define-fun f684 () Arctic (+ (* f14 f674) (* f15 f676))) (define-fun f685 () Arctic (+ (* f14 f675) (* f15 f677))) (define-fun f686 () Arctic (+ (* f12 f680) (* f13 f681))) (define-fun f687 () Arctic (+ (* f14 f680) (* f15 f681))) (define-fun f688 () Arctic (+ f16 f686)) (define-fun f689 () Arctic (+ f17 f687)) (define-fun f690 () Arctic (+ (* f12 f682) (* f13 f684))) (define-fun f691 () Arctic (+ (* f12 f683) (* f13 f685))) (define-fun f692 () Arctic (+ (* f14 f682) (* f15 f684))) (define-fun f693 () Arctic (+ (* f14 f683) (* f15 f685))) (define-fun f694 () Arctic (+ (* f12 f688) (* f13 f689))) (define-fun f695 () Arctic (+ (* f14 f688) (* f15 f689))) (define-fun f696 () Arctic (+ f16 f694)) (define-fun f697 () Arctic (+ f17 f695)) (define-fun f698 () Arctic (+ (* f12 f690) (* f13 f692))) (define-fun f699 () Arctic (+ (* f12 f691) (* f13 f693))) (define-fun f700 () Arctic (+ (* f14 f690) (* f15 f692))) (define-fun f701 () Arctic (+ (* f14 f691) (* f15 f693))) (define-fun f702 () Arctic (+ (* f12 f696) (* f13 f697))) (define-fun f703 () Arctic (+ (* f14 f696) (* f15 f697))) (define-fun f704 () Arctic (+ f16 f702)) (define-fun f705 () Arctic (+ f17 f703)) (define-fun f706 () Arctic (+ (* f12 f698) (* f13 f700))) (define-fun f707 () Arctic (+ (* f12 f699) (* f13 f701))) (define-fun f708 () Arctic (+ (* f14 f698) (* f15 f700))) (define-fun f709 () Arctic (+ (* f14 f699) (* f15 f701))) (define-fun f710 () Arctic (+ (* f12 f704) (* f13 f705))) (define-fun f711 () Arctic (+ (* f14 f704) (* f15 f705))) (define-fun f712 () Arctic (+ f16 f710)) (define-fun f713 () Arctic (+ f17 f711)) (define-fun f714 () Arctic (+ (* f0 f706) (* f1 f708))) (define-fun f715 () Arctic (+ (* f0 f707) (* f1 f709))) (define-fun f716 () Arctic (+ (* f2 f706) (* f3 f708))) (define-fun f717 () Arctic (+ (* f2 f707) (* f3 f709))) (define-fun f718 () Arctic (+ (* f0 f712) (* f1 f713))) (define-fun f719 () Arctic (+ (* f2 f712) (* f3 f713))) (define-fun f720 () Arctic (+ f4 f718)) (define-fun f721 () Arctic (+ f5 f719)) (define-fun f722 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f723 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f724 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f725 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f726 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f727 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f728 () Arctic (+ f16 f726)) (define-fun f729 () Arctic (+ f17 f727)) (define-fun f730 () Arctic (+ (* f12 f722) (* f13 f724))) (define-fun f731 () Arctic (+ (* f12 f723) (* f13 f725))) (define-fun f732 () Arctic (+ (* f14 f722) (* f15 f724))) (define-fun f733 () Arctic (+ (* f14 f723) (* f15 f725))) (define-fun f734 () Arctic (+ (* f12 f728) (* f13 f729))) (define-fun f735 () Arctic (+ (* f14 f728) (* f15 f729))) (define-fun f736 () Arctic (+ f16 f734)) (define-fun f737 () Arctic (+ f17 f735)) (define-fun f738 () Arctic (+ (* f12 f730) (* f13 f732))) (define-fun f739 () Arctic (+ (* f12 f731) (* f13 f733))) (define-fun f740 () Arctic (+ (* f14 f730) (* f15 f732))) (define-fun f741 () Arctic (+ (* f14 f731) (* f15 f733))) (define-fun f742 () Arctic (+ (* f12 f736) (* f13 f737))) (define-fun f743 () Arctic (+ (* f14 f736) (* f15 f737))) (define-fun f744 () Arctic (+ f16 f742)) (define-fun f745 () Arctic (+ f17 f743)) (define-fun f746 () Arctic (+ (* f12 f738) (* f13 f740))) (define-fun f747 () Arctic (+ (* f12 f739) (* f13 f741))) (define-fun f748 () Arctic (+ (* f14 f738) (* f15 f740))) (define-fun f749 () Arctic (+ (* f14 f739) (* f15 f741))) (define-fun f750 () Arctic (+ (* f12 f744) (* f13 f745))) (define-fun f751 () Arctic (+ (* f14 f744) (* f15 f745))) (define-fun f752 () Arctic (+ f16 f750)) (define-fun f753 () Arctic (+ f17 f751)) (define-fun f754 () Arctic (+ (* f6 f746) (* f7 f748))) (define-fun f755 () Arctic (+ (* f6 f747) (* f7 f749))) (define-fun f756 () Arctic (+ (* f8 f746) (* f9 f748))) (define-fun f757 () Arctic (+ (* f8 f747) (* f9 f749))) (define-fun f758 () Arctic (+ (* f6 f752) (* f7 f753))) (define-fun f759 () Arctic (+ (* f8 f752) (* f9 f753))) (define-fun f760 () Arctic (+ f10 f758)) (define-fun f761 () Arctic (+ f11 f759)) (define-fun f762 () Arctic (+ (* f12 f754) (* f13 f756))) (define-fun f763 () Arctic (+ (* f12 f755) (* f13 f757))) (define-fun f764 () Arctic (+ (* f14 f754) (* f15 f756))) (define-fun f765 () Arctic (+ (* f14 f755) (* f15 f757))) (define-fun f766 () Arctic (+ (* f12 f760) (* f13 f761))) (define-fun f767 () Arctic (+ (* f14 f760) (* f15 f761))) (define-fun f768 () Arctic (+ f16 f766)) (define-fun f769 () Arctic (+ f17 f767)) (define-fun f770 () Arctic (+ (* f12 f762) (* f13 f764))) (define-fun f771 () Arctic (+ (* f12 f763) (* f13 f765))) (define-fun f772 () Arctic (+ (* f14 f762) (* f15 f764))) (define-fun f773 () Arctic (+ (* f14 f763) (* f15 f765))) (define-fun f774 () Arctic (+ (* f12 f768) (* f13 f769))) (define-fun f775 () Arctic (+ (* f14 f768) (* f15 f769))) (define-fun f776 () Arctic (+ f16 f774)) (define-fun f777 () Arctic (+ f17 f775)) (define-fun f778 () Arctic (+ (* f12 f770) (* f13 f772))) (define-fun f779 () Arctic (+ (* f12 f771) (* f13 f773))) (define-fun f780 () Arctic (+ (* f14 f770) (* f15 f772))) (define-fun f781 () Arctic (+ (* f14 f771) (* f15 f773))) (define-fun f782 () Arctic (+ (* f12 f776) (* f13 f777))) (define-fun f783 () Arctic (+ (* f14 f776) (* f15 f777))) (define-fun f784 () Arctic (+ f16 f782)) (define-fun f785 () Arctic (+ f17 f783)) (define-fun f786 () Arctic (+ (* f12 f778) (* f13 f780))) (define-fun f787 () Arctic (+ (* f12 f779) (* f13 f781))) (define-fun f788 () Arctic (+ (* f14 f778) (* f15 f780))) (define-fun f789 () Arctic (+ (* f14 f779) (* f15 f781))) (define-fun f790 () Arctic (+ (* f12 f784) (* f13 f785))) (define-fun f791 () Arctic (+ (* f14 f784) (* f15 f785))) (define-fun f792 () Arctic (+ f16 f790)) (define-fun f793 () Arctic (+ f17 f791)) (define-fun f794 () Arctic (+ (* f6 f786) (* f7 f788))) (define-fun f795 () Arctic (+ (* f6 f787) (* f7 f789))) (define-fun f796 () Arctic (+ (* f8 f786) (* f9 f788))) (define-fun f797 () Arctic (+ (* f8 f787) (* f9 f789))) (define-fun f798 () Arctic (+ (* f6 f792) (* f7 f793))) (define-fun f799 () Arctic (+ (* f8 f792) (* f9 f793))) (define-fun f800 () Arctic (+ f10 f798)) (define-fun f801 () Arctic (+ f11 f799)) (define-fun f802 () Arctic (+ (* f12 f794) (* f13 f796))) (define-fun f803 () Arctic (+ (* f12 f795) (* f13 f797))) (define-fun f804 () Arctic (+ (* f14 f794) (* f15 f796))) (define-fun f805 () Arctic (+ (* f14 f795) (* f15 f797))) (define-fun f806 () Arctic (+ (* f12 f800) (* f13 f801))) (define-fun f807 () Arctic (+ (* f14 f800) (* f15 f801))) (define-fun f808 () Arctic (+ f16 f806)) (define-fun f809 () Arctic (+ f17 f807)) (define-fun f810 () Arctic (+ (* f0 f802) (* f1 f804))) (define-fun f811 () Arctic (+ (* f0 f803) (* f1 f805))) (define-fun f812 () Arctic (+ (* f2 f802) (* f3 f804))) (define-fun f813 () Arctic (+ (* f2 f803) (* f3 f805))) (define-fun f814 () Arctic (+ (* f0 f808) (* f1 f809))) (define-fun f815 () Arctic (+ (* f2 f808) (* f3 f809))) (define-fun f816 () Arctic (+ f4 f814)) (define-fun f817 () Arctic (+ f5 f815)) (define-fun f818 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f819 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f820 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f821 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f822 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f823 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f824 () Arctic (+ f16 f822)) (define-fun f825 () Arctic (+ f17 f823)) (define-fun f826 () Arctic (+ (* f6 f818) (* f7 f820))) (define-fun f827 () Arctic (+ (* f6 f819) (* f7 f821))) (define-fun f828 () Arctic (+ (* f8 f818) (* f9 f820))) (define-fun f829 () Arctic (+ (* f8 f819) (* f9 f821))) (define-fun f830 () Arctic (+ (* f6 f824) (* f7 f825))) (define-fun f831 () Arctic (+ (* f8 f824) (* f9 f825))) (define-fun f832 () Arctic (+ f10 f830)) (define-fun f833 () Arctic (+ f11 f831)) (define-fun f834 () Arctic (+ (* f12 f826) (* f13 f828))) (define-fun f835 () Arctic (+ (* f12 f827) (* f13 f829))) (define-fun f836 () Arctic (+ (* f14 f826) (* f15 f828))) (define-fun f837 () Arctic (+ (* f14 f827) (* f15 f829))) (define-fun f838 () Arctic (+ (* f12 f832) (* f13 f833))) (define-fun f839 () Arctic (+ (* f14 f832) (* f15 f833))) (define-fun f840 () Arctic (+ f16 f838)) (define-fun f841 () Arctic (+ f17 f839)) (define-fun f842 () Arctic (+ (* f12 f834) (* f13 f836))) (define-fun f843 () Arctic (+ (* f12 f835) (* f13 f837))) (define-fun f844 () Arctic (+ (* f14 f834) (* f15 f836))) (define-fun f845 () Arctic (+ (* f14 f835) (* f15 f837))) (define-fun f846 () Arctic (+ (* f12 f840) (* f13 f841))) (define-fun f847 () Arctic (+ (* f14 f840) (* f15 f841))) (define-fun f848 () Arctic (+ f16 f846)) (define-fun f849 () Arctic (+ f17 f847)) (define-fun f850 () Arctic (+ (* f12 f842) (* f13 f844))) (define-fun f851 () Arctic (+ (* f12 f843) (* f13 f845))) (define-fun f852 () Arctic (+ (* f14 f842) (* f15 f844))) (define-fun f853 () Arctic (+ (* f14 f843) (* f15 f845))) (define-fun f854 () Arctic (+ (* f12 f848) (* f13 f849))) (define-fun f855 () Arctic (+ (* f14 f848) (* f15 f849))) (define-fun f856 () Arctic (+ f16 f854)) (define-fun f857 () Arctic (+ f17 f855)) (define-fun f858 () Arctic (+ (* f12 f850) (* f13 f852))) (define-fun f859 () Arctic (+ (* f12 f851) (* f13 f853))) (define-fun f860 () Arctic (+ (* f14 f850) (* f15 f852))) (define-fun f861 () Arctic (+ (* f14 f851) (* f15 f853))) (define-fun f862 () Arctic (+ (* f12 f856) (* f13 f857))) (define-fun f863 () Arctic (+ (* f14 f856) (* f15 f857))) (define-fun f864 () Arctic (+ f16 f862)) (define-fun f865 () Arctic (+ f17 f863)) (define-fun f866 () Arctic (+ (* f0 f858) (* f1 f860))) (define-fun f867 () Arctic (+ (* f0 f859) (* f1 f861))) (define-fun f868 () Arctic (+ (* f2 f858) (* f3 f860))) (define-fun f869 () Arctic (+ (* f2 f859) (* f3 f861))) (define-fun f870 () Arctic (+ (* f0 f864) (* f1 f865))) (define-fun f871 () Arctic (+ (* f2 f864) (* f3 f865))) (define-fun f872 () Arctic (+ f4 f870)) (define-fun f873 () Arctic (+ f5 f871)) (define-fun f874 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f875 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f876 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f877 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f878 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f879 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f880 () Arctic (+ f16 f878)) (define-fun f881 () Arctic (+ f17 f879)) (define-fun f882 () Arctic (+ (* f12 f874) (* f13 f876))) (define-fun f883 () Arctic (+ (* f12 f875) (* f13 f877))) (define-fun f884 () Arctic (+ (* f14 f874) (* f15 f876))) (define-fun f885 () Arctic (+ (* f14 f875) (* f15 f877))) (define-fun f886 () Arctic (+ (* f12 f880) (* f13 f881))) (define-fun f887 () Arctic (+ (* f14 f880) (* f15 f881))) (define-fun f888 () Arctic (+ f16 f886)) (define-fun f889 () Arctic (+ f17 f887)) (define-fun f890 () Arctic (+ (* f12 f882) (* f13 f884))) (define-fun f891 () Arctic (+ (* f12 f883) (* f13 f885))) (define-fun f892 () Arctic (+ (* f14 f882) (* f15 f884))) (define-fun f893 () Arctic (+ (* f14 f883) (* f15 f885))) (define-fun f894 () Arctic (+ (* f12 f888) (* f13 f889))) (define-fun f895 () Arctic (+ (* f14 f888) (* f15 f889))) (define-fun f896 () Arctic (+ f16 f894)) (define-fun f897 () Arctic (+ f17 f895)) (define-fun f898 () Arctic (+ (* f12 f890) (* f13 f892))) (define-fun f899 () Arctic (+ (* f12 f891) (* f13 f893))) (define-fun f900 () Arctic (+ (* f14 f890) (* f15 f892))) (define-fun f901 () Arctic (+ (* f14 f891) (* f15 f893))) (define-fun f902 () Arctic (+ (* f12 f896) (* f13 f897))) (define-fun f903 () Arctic (+ (* f14 f896) (* f15 f897))) (define-fun f904 () Arctic (+ f16 f902)) (define-fun f905 () Arctic (+ f17 f903)) (define-fun f906 () Arctic (+ (* f6 f898) (* f7 f900))) (define-fun f907 () Arctic (+ (* f6 f899) (* f7 f901))) (define-fun f908 () Arctic (+ (* f8 f898) (* f9 f900))) (define-fun f909 () Arctic (+ (* f8 f899) (* f9 f901))) (define-fun f910 () Arctic (+ (* f6 f904) (* f7 f905))) (define-fun f911 () Arctic (+ (* f8 f904) (* f9 f905))) (define-fun f912 () Arctic (+ f10 f910)) (define-fun f913 () Arctic (+ f11 f911)) (define-fun f914 () Arctic (+ (* f12 f906) (* f13 f908))) (define-fun f915 () Arctic (+ (* f12 f907) (* f13 f909))) (define-fun f916 () Arctic (+ (* f14 f906) (* f15 f908))) (define-fun f917 () Arctic (+ (* f14 f907) (* f15 f909))) (define-fun f918 () Arctic (+ (* f12 f912) (* f13 f913))) (define-fun f919 () Arctic (+ (* f14 f912) (* f15 f913))) (define-fun f920 () Arctic (+ f16 f918)) (define-fun f921 () Arctic (+ f17 f919)) (define-fun f922 () Arctic (+ (* f12 f914) (* f13 f916))) (define-fun f923 () Arctic (+ (* f12 f915) (* f13 f917))) (define-fun f924 () Arctic (+ (* f14 f914) (* f15 f916))) (define-fun f925 () Arctic (+ (* f14 f915) (* f15 f917))) (define-fun f926 () Arctic (+ (* f12 f920) (* f13 f921))) (define-fun f927 () Arctic (+ (* f14 f920) (* f15 f921))) (define-fun f928 () Arctic (+ f16 f926)) (define-fun f929 () Arctic (+ f17 f927)) (define-fun f930 () Arctic (+ (* f12 f922) (* f13 f924))) (define-fun f931 () Arctic (+ (* f12 f923) (* f13 f925))) (define-fun f932 () Arctic (+ (* f14 f922) (* f15 f924))) (define-fun f933 () Arctic (+ (* f14 f923) (* f15 f925))) (define-fun f934 () Arctic (+ (* f12 f928) (* f13 f929))) (define-fun f935 () Arctic (+ (* f14 f928) (* f15 f929))) (define-fun f936 () Arctic (+ f16 f934)) (define-fun f937 () Arctic (+ f17 f935)) (define-fun f938 () Arctic (+ (* f12 f930) (* f13 f932))) (define-fun f939 () Arctic (+ (* f12 f931) (* f13 f933))) (define-fun f940 () Arctic (+ (* f14 f930) (* f15 f932))) (define-fun f941 () Arctic (+ (* f14 f931) (* f15 f933))) (define-fun f942 () Arctic (+ (* f12 f936) (* f13 f937))) (define-fun f943 () Arctic (+ (* f14 f936) (* f15 f937))) (define-fun f944 () Arctic (+ f16 f942)) (define-fun f945 () Arctic (+ f17 f943)) (define-fun f946 () Arctic (+ (* f0 f938) (* f1 f940))) (define-fun f947 () Arctic (+ (* f0 f939) (* f1 f941))) (define-fun f948 () Arctic (+ (* f2 f938) (* f3 f940))) (define-fun f949 () Arctic (+ (* f2 f939) (* f3 f941))) (define-fun f950 () Arctic (+ (* f0 f944) (* f1 f945))) (define-fun f951 () Arctic (+ (* f2 f944) (* f3 f945))) (define-fun f952 () Arctic (+ f4 f950)) (define-fun f953 () Arctic (+ f5 f951)) (define-fun f954 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f955 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f956 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f957 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f958 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f959 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f960 () Arctic (+ f16 f958)) (define-fun f961 () Arctic (+ f17 f959)) (define-fun f962 () Arctic (+ (* f6 f954) (* f7 f956))) (define-fun f963 () Arctic (+ (* f6 f955) (* f7 f957))) (define-fun f964 () Arctic (+ (* f8 f954) (* f9 f956))) (define-fun f965 () Arctic (+ (* f8 f955) (* f9 f957))) (define-fun f966 () Arctic (+ (* f6 f960) (* f7 f961))) (define-fun f967 () Arctic (+ (* f8 f960) (* f9 f961))) (define-fun f968 () Arctic (+ f10 f966)) (define-fun f969 () Arctic (+ f11 f967)) (define-fun f970 () Arctic (+ (* f12 f962) (* f13 f964))) (define-fun f971 () Arctic (+ (* f12 f963) (* f13 f965))) (define-fun f972 () Arctic (+ (* f14 f962) (* f15 f964))) (define-fun f973 () Arctic (+ (* f14 f963) (* f15 f965))) (define-fun f974 () Arctic (+ (* f12 f968) (* f13 f969))) (define-fun f975 () Arctic (+ (* f14 f968) (* f15 f969))) (define-fun f976 () Arctic (+ f16 f974)) (define-fun f977 () Arctic (+ f17 f975)) (define-fun f978 () Arctic (+ (* f12 f970) (* f13 f972))) (define-fun f979 () Arctic (+ (* f12 f971) (* f13 f973))) (define-fun f980 () Arctic (+ (* f14 f970) (* f15 f972))) (define-fun f981 () Arctic (+ (* f14 f971) (* f15 f973))) (define-fun f982 () Arctic (+ (* f12 f976) (* f13 f977))) (define-fun f983 () Arctic (+ (* f14 f976) (* f15 f977))) (define-fun f984 () Arctic (+ f16 f982)) (define-fun f985 () Arctic (+ f17 f983)) (define-fun f986 () Arctic (+ (* f12 f978) (* f13 f980))) (define-fun f987 () Arctic (+ (* f12 f979) (* f13 f981))) (define-fun f988 () Arctic (+ (* f14 f978) (* f15 f980))) (define-fun f989 () Arctic (+ (* f14 f979) (* f15 f981))) (define-fun f990 () Arctic (+ (* f12 f984) (* f13 f985))) (define-fun f991 () Arctic (+ (* f14 f984) (* f15 f985))) (define-fun f992 () Arctic (+ f16 f990)) (define-fun f993 () Arctic (+ f17 f991)) (define-fun f994 () Arctic (+ (* f12 f986) (* f13 f988))) (define-fun f995 () Arctic (+ (* f12 f987) (* f13 f989))) (define-fun f996 () Arctic (+ (* f14 f986) (* f15 f988))) (define-fun f997 () Arctic (+ (* f14 f987) (* f15 f989))) (define-fun f998 () Arctic (+ (* f12 f992) (* f13 f993))) (define-fun f999 () Arctic (+ (* f14 f992) (* f15 f993))) (define-fun f1000 () Arctic (+ f16 f998)) (define-fun f1001 () Arctic (+ f17 f999)) (define-fun f1002 () Arctic (+ (* f0 f994) (* f1 f996))) (define-fun f1003 () Arctic (+ (* f0 f995) (* f1 f997))) (define-fun f1004 () Arctic (+ (* f2 f994) (* f3 f996))) (define-fun f1005 () Arctic (+ (* f2 f995) (* f3 f997))) (define-fun f1006 () Arctic (+ (* f0 f1000) (* f1 f1001))) (define-fun f1007 () Arctic (+ (* f2 f1000) (* f3 f1001))) (define-fun f1008 () Arctic (+ f4 f1006)) (define-fun f1009 () Arctic (+ f5 f1007)) (define-fun f1010 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1011 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1012 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1013 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1014 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1015 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1016 () Arctic (+ f16 f1014)) (define-fun f1017 () Arctic (+ f17 f1015)) (define-fun f1018 () Arctic (+ (* f12 f1010) (* f13 f1012))) (define-fun f1019 () Arctic (+ (* f12 f1011) (* f13 f1013))) (define-fun f1020 () Arctic (+ (* f14 f1010) (* f15 f1012))) (define-fun f1021 () Arctic (+ (* f14 f1011) (* f15 f1013))) (define-fun f1022 () Arctic (+ (* f12 f1016) (* f13 f1017))) (define-fun f1023 () Arctic (+ (* f14 f1016) (* f15 f1017))) (define-fun f1024 () Arctic (+ f16 f1022)) (define-fun f1025 () Arctic (+ f17 f1023)) (define-fun f1026 () Arctic (+ (* f12 f1018) (* f13 f1020))) (define-fun f1027 () Arctic (+ (* f12 f1019) (* f13 f1021))) (define-fun f1028 () Arctic (+ (* f14 f1018) (* f15 f1020))) (define-fun f1029 () Arctic (+ (* f14 f1019) (* f15 f1021))) (define-fun f1030 () Arctic (+ (* f12 f1024) (* f13 f1025))) (define-fun f1031 () Arctic (+ (* f14 f1024) (* f15 f1025))) (define-fun f1032 () Arctic (+ f16 f1030)) (define-fun f1033 () Arctic (+ f17 f1031)) (define-fun f1034 () Arctic (+ (* f12 f1026) (* f13 f1028))) (define-fun f1035 () Arctic (+ (* f12 f1027) (* f13 f1029))) (define-fun f1036 () Arctic (+ (* f14 f1026) (* f15 f1028))) (define-fun f1037 () Arctic (+ (* f14 f1027) (* f15 f1029))) (define-fun f1038 () Arctic (+ (* f12 f1032) (* f13 f1033))) (define-fun f1039 () Arctic (+ (* f14 f1032) (* f15 f1033))) (define-fun f1040 () Arctic (+ f16 f1038)) (define-fun f1041 () Arctic (+ f17 f1039)) (define-fun f1042 () Arctic (+ (* f0 f1034) (* f1 f1036))) (define-fun f1043 () Arctic (+ (* f0 f1035) (* f1 f1037))) (define-fun f1044 () Arctic (+ (* f2 f1034) (* f3 f1036))) (define-fun f1045 () Arctic (+ (* f2 f1035) (* f3 f1037))) (define-fun f1046 () Arctic (+ (* f0 f1040) (* f1 f1041))) (define-fun f1047 () Arctic (+ (* f2 f1040) (* f3 f1041))) (define-fun f1048 () Arctic (+ f4 f1046)) (define-fun f1049 () Arctic (+ f5 f1047)) (define-fun f1050 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1051 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1052 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1053 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1054 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1055 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1056 () Arctic (+ f16 f1054)) (define-fun f1057 () Arctic (+ f17 f1055)) (define-fun f1058 () Arctic (+ (* f6 f1050) (* f7 f1052))) (define-fun f1059 () Arctic (+ (* f6 f1051) (* f7 f1053))) (define-fun f1060 () Arctic (+ (* f8 f1050) (* f9 f1052))) (define-fun f1061 () Arctic (+ (* f8 f1051) (* f9 f1053))) (define-fun f1062 () Arctic (+ (* f6 f1056) (* f7 f1057))) (define-fun f1063 () Arctic (+ (* f8 f1056) (* f9 f1057))) (define-fun f1064 () Arctic (+ f10 f1062)) (define-fun f1065 () Arctic (+ f11 f1063)) (define-fun f1066 () Arctic (+ (* f12 f1058) (* f13 f1060))) (define-fun f1067 () Arctic (+ (* f12 f1059) (* f13 f1061))) (define-fun f1068 () Arctic (+ (* f14 f1058) (* f15 f1060))) (define-fun f1069 () Arctic (+ (* f14 f1059) (* f15 f1061))) (define-fun f1070 () Arctic (+ (* f12 f1064) (* f13 f1065))) (define-fun f1071 () Arctic (+ (* f14 f1064) (* f15 f1065))) (define-fun f1072 () Arctic (+ f16 f1070)) (define-fun f1073 () Arctic (+ f17 f1071)) (define-fun f1074 () Arctic (+ (* f12 f1066) (* f13 f1068))) (define-fun f1075 () Arctic (+ (* f12 f1067) (* f13 f1069))) (define-fun f1076 () Arctic (+ (* f14 f1066) (* f15 f1068))) (define-fun f1077 () Arctic (+ (* f14 f1067) (* f15 f1069))) (define-fun f1078 () Arctic (+ (* f12 f1072) (* f13 f1073))) (define-fun f1079 () Arctic (+ (* f14 f1072) (* f15 f1073))) (define-fun f1080 () Arctic (+ f16 f1078)) (define-fun f1081 () Arctic (+ f17 f1079)) (define-fun f1082 () Arctic (+ (* f12 f1074) (* f13 f1076))) (define-fun f1083 () Arctic (+ (* f12 f1075) (* f13 f1077))) (define-fun f1084 () Arctic (+ (* f14 f1074) (* f15 f1076))) (define-fun f1085 () Arctic (+ (* f14 f1075) (* f15 f1077))) (define-fun f1086 () Arctic (+ (* f12 f1080) (* f13 f1081))) (define-fun f1087 () Arctic (+ (* f14 f1080) (* f15 f1081))) (define-fun f1088 () Arctic (+ f16 f1086)) (define-fun f1089 () Arctic (+ f17 f1087)) (define-fun f1090 () Arctic (+ (* f12 f1082) (* f13 f1084))) (define-fun f1091 () Arctic (+ (* f12 f1083) (* f13 f1085))) (define-fun f1092 () Arctic (+ (* f14 f1082) (* f15 f1084))) (define-fun f1093 () Arctic (+ (* f14 f1083) (* f15 f1085))) (define-fun f1094 () Arctic (+ (* f12 f1088) (* f13 f1089))) (define-fun f1095 () Arctic (+ (* f14 f1088) (* f15 f1089))) (define-fun f1096 () Arctic (+ f16 f1094)) (define-fun f1097 () Arctic (+ f17 f1095)) (define-fun f1098 () Arctic (+ (* f0 f1090) (* f1 f1092))) (define-fun f1099 () Arctic (+ (* f0 f1091) (* f1 f1093))) (define-fun f1100 () Arctic (+ (* f2 f1090) (* f3 f1092))) (define-fun f1101 () Arctic (+ (* f2 f1091) (* f3 f1093))) (define-fun f1102 () Arctic (+ (* f0 f1096) (* f1 f1097))) (define-fun f1103 () Arctic (+ (* f2 f1096) (* f3 f1097))) (define-fun f1104 () Arctic (+ f4 f1102)) (define-fun f1105 () Arctic (+ f5 f1103)) (define-fun f1106 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1107 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1108 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1109 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1110 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1111 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1112 () Arctic (+ f16 f1110)) (define-fun f1113 () Arctic (+ f17 f1111)) (define-fun f1114 () Arctic (+ (* f12 f1106) (* f13 f1108))) (define-fun f1115 () Arctic (+ (* f12 f1107) (* f13 f1109))) (define-fun f1116 () Arctic (+ (* f14 f1106) (* f15 f1108))) (define-fun f1117 () Arctic (+ (* f14 f1107) (* f15 f1109))) (define-fun f1118 () Arctic (+ (* f12 f1112) (* f13 f1113))) (define-fun f1119 () Arctic (+ (* f14 f1112) (* f15 f1113))) (define-fun f1120 () Arctic (+ f16 f1118)) (define-fun f1121 () Arctic (+ f17 f1119)) (define-fun f1122 () Arctic (+ (* f6 f1114) (* f7 f1116))) (define-fun f1123 () Arctic (+ (* f6 f1115) (* f7 f1117))) (define-fun f1124 () Arctic (+ (* f8 f1114) (* f9 f1116))) (define-fun f1125 () Arctic (+ (* f8 f1115) (* f9 f1117))) (define-fun f1126 () Arctic (+ (* f6 f1120) (* f7 f1121))) (define-fun f1127 () Arctic (+ (* f8 f1120) (* f9 f1121))) (define-fun f1128 () Arctic (+ f10 f1126)) (define-fun f1129 () Arctic (+ f11 f1127)) (define-fun f1130 () Arctic (+ (* f12 f1122) (* f13 f1124))) (define-fun f1131 () Arctic (+ (* f12 f1123) (* f13 f1125))) (define-fun f1132 () Arctic (+ (* f14 f1122) (* f15 f1124))) (define-fun f1133 () Arctic (+ (* f14 f1123) (* f15 f1125))) (define-fun f1134 () Arctic (+ (* f12 f1128) (* f13 f1129))) (define-fun f1135 () Arctic (+ (* f14 f1128) (* f15 f1129))) (define-fun f1136 () Arctic (+ f16 f1134)) (define-fun f1137 () Arctic (+ f17 f1135)) (define-fun f1138 () Arctic (+ (* f12 f1130) (* f13 f1132))) (define-fun f1139 () Arctic (+ (* f12 f1131) (* f13 f1133))) (define-fun f1140 () Arctic (+ (* f14 f1130) (* f15 f1132))) (define-fun f1141 () Arctic (+ (* f14 f1131) (* f15 f1133))) (define-fun f1142 () Arctic (+ (* f12 f1136) (* f13 f1137))) (define-fun f1143 () Arctic (+ (* f14 f1136) (* f15 f1137))) (define-fun f1144 () Arctic (+ f16 f1142)) (define-fun f1145 () Arctic (+ f17 f1143)) (define-fun f1146 () Arctic (+ (* f12 f1138) (* f13 f1140))) (define-fun f1147 () Arctic (+ (* f12 f1139) (* f13 f1141))) (define-fun f1148 () Arctic (+ (* f14 f1138) (* f15 f1140))) (define-fun f1149 () Arctic (+ (* f14 f1139) (* f15 f1141))) (define-fun f1150 () Arctic (+ (* f12 f1144) (* f13 f1145))) (define-fun f1151 () Arctic (+ (* f14 f1144) (* f15 f1145))) (define-fun f1152 () Arctic (+ f16 f1150)) (define-fun f1153 () Arctic (+ f17 f1151)) (define-fun f1154 () Arctic (+ (* f12 f1146) (* f13 f1148))) (define-fun f1155 () Arctic (+ (* f12 f1147) (* f13 f1149))) (define-fun f1156 () Arctic (+ (* f14 f1146) (* f15 f1148))) (define-fun f1157 () Arctic (+ (* f14 f1147) (* f15 f1149))) (define-fun f1158 () Arctic (+ (* f12 f1152) (* f13 f1153))) (define-fun f1159 () Arctic (+ (* f14 f1152) (* f15 f1153))) (define-fun f1160 () Arctic (+ f16 f1158)) (define-fun f1161 () Arctic (+ f17 f1159)) (define-fun f1162 () Arctic (+ (* f0 f1154) (* f1 f1156))) (define-fun f1163 () Arctic (+ (* f0 f1155) (* f1 f1157))) (define-fun f1164 () Arctic (+ (* f2 f1154) (* f3 f1156))) (define-fun f1165 () Arctic (+ (* f2 f1155) (* f3 f1157))) (define-fun f1166 () Arctic (+ (* f0 f1160) (* f1 f1161))) (define-fun f1167 () Arctic (+ (* f2 f1160) (* f3 f1161))) (define-fun f1168 () Arctic (+ f4 f1166)) (define-fun f1169 () Arctic (+ f5 f1167)) (define-fun f1170 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1171 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1172 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1173 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1174 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1175 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1176 () Arctic (+ f16 f1174)) (define-fun f1177 () Arctic (+ f17 f1175)) (define-fun f1178 () Arctic (+ (* f6 f1170) (* f7 f1172))) (define-fun f1179 () Arctic (+ (* f6 f1171) (* f7 f1173))) (define-fun f1180 () Arctic (+ (* f8 f1170) (* f9 f1172))) (define-fun f1181 () Arctic (+ (* f8 f1171) (* f9 f1173))) (define-fun f1182 () Arctic (+ (* f6 f1176) (* f7 f1177))) (define-fun f1183 () Arctic (+ (* f8 f1176) (* f9 f1177))) (define-fun f1184 () Arctic (+ f10 f1182)) (define-fun f1185 () Arctic (+ f11 f1183)) (define-fun f1186 () Arctic (+ (* f12 f1178) (* f13 f1180))) (define-fun f1187 () Arctic (+ (* f12 f1179) (* f13 f1181))) (define-fun f1188 () Arctic (+ (* f14 f1178) (* f15 f1180))) (define-fun f1189 () Arctic (+ (* f14 f1179) (* f15 f1181))) (define-fun f1190 () Arctic (+ (* f12 f1184) (* f13 f1185))) (define-fun f1191 () Arctic (+ (* f14 f1184) (* f15 f1185))) (define-fun f1192 () Arctic (+ f16 f1190)) (define-fun f1193 () Arctic (+ f17 f1191)) (define-fun f1194 () Arctic (+ (* f12 f1186) (* f13 f1188))) (define-fun f1195 () Arctic (+ (* f12 f1187) (* f13 f1189))) (define-fun f1196 () Arctic (+ (* f14 f1186) (* f15 f1188))) (define-fun f1197 () Arctic (+ (* f14 f1187) (* f15 f1189))) (define-fun f1198 () Arctic (+ (* f12 f1192) (* f13 f1193))) (define-fun f1199 () Arctic (+ (* f14 f1192) (* f15 f1193))) (define-fun f1200 () Arctic (+ f16 f1198)) (define-fun f1201 () Arctic (+ f17 f1199)) (define-fun f1202 () Arctic (+ (* f6 f1194) (* f7 f1196))) (define-fun f1203 () Arctic (+ (* f6 f1195) (* f7 f1197))) (define-fun f1204 () Arctic (+ (* f8 f1194) (* f9 f1196))) (define-fun f1205 () Arctic (+ (* f8 f1195) (* f9 f1197))) (define-fun f1206 () Arctic (+ (* f6 f1200) (* f7 f1201))) (define-fun f1207 () Arctic (+ (* f8 f1200) (* f9 f1201))) (define-fun f1208 () Arctic (+ f10 f1206)) (define-fun f1209 () Arctic (+ f11 f1207)) (define-fun f1210 () Arctic (+ (* f12 f1202) (* f13 f1204))) (define-fun f1211 () Arctic (+ (* f12 f1203) (* f13 f1205))) (define-fun f1212 () Arctic (+ (* f14 f1202) (* f15 f1204))) (define-fun f1213 () Arctic (+ (* f14 f1203) (* f15 f1205))) (define-fun f1214 () Arctic (+ (* f12 f1208) (* f13 f1209))) (define-fun f1215 () Arctic (+ (* f14 f1208) (* f15 f1209))) (define-fun f1216 () Arctic (+ f16 f1214)) (define-fun f1217 () Arctic (+ f17 f1215)) (define-fun f1218 () Arctic (+ (* f12 f1210) (* f13 f1212))) (define-fun f1219 () Arctic (+ (* f12 f1211) (* f13 f1213))) (define-fun f1220 () Arctic (+ (* f14 f1210) (* f15 f1212))) (define-fun f1221 () Arctic (+ (* f14 f1211) (* f15 f1213))) (define-fun f1222 () Arctic (+ (* f12 f1216) (* f13 f1217))) (define-fun f1223 () Arctic (+ (* f14 f1216) (* f15 f1217))) (define-fun f1224 () Arctic (+ f16 f1222)) (define-fun f1225 () Arctic (+ f17 f1223)) (define-fun f1226 () Arctic (+ (* f12 f1218) (* f13 f1220))) (define-fun f1227 () Arctic (+ (* f12 f1219) (* f13 f1221))) (define-fun f1228 () Arctic (+ (* f14 f1218) (* f15 f1220))) (define-fun f1229 () Arctic (+ (* f14 f1219) (* f15 f1221))) (define-fun f1230 () Arctic (+ (* f12 f1224) (* f13 f1225))) (define-fun f1231 () Arctic (+ (* f14 f1224) (* f15 f1225))) (define-fun f1232 () Arctic (+ f16 f1230)) (define-fun f1233 () Arctic (+ f17 f1231)) (define-fun f1234 () Arctic (+ (* f6 f1226) (* f7 f1228))) (define-fun f1235 () Arctic (+ (* f6 f1227) (* f7 f1229))) (define-fun f1236 () Arctic (+ (* f8 f1226) (* f9 f1228))) (define-fun f1237 () Arctic (+ (* f8 f1227) (* f9 f1229))) (define-fun f1238 () Arctic (+ (* f6 f1232) (* f7 f1233))) (define-fun f1239 () Arctic (+ (* f8 f1232) (* f9 f1233))) (define-fun f1240 () Arctic (+ f10 f1238)) (define-fun f1241 () Arctic (+ f11 f1239)) (define-fun f1242 () Arctic (+ (* f12 f1234) (* f13 f1236))) (define-fun f1243 () Arctic (+ (* f12 f1235) (* f13 f1237))) (define-fun f1244 () Arctic (+ (* f14 f1234) (* f15 f1236))) (define-fun f1245 () Arctic (+ (* f14 f1235) (* f15 f1237))) (define-fun f1246 () Arctic (+ (* f12 f1240) (* f13 f1241))) (define-fun f1247 () Arctic (+ (* f14 f1240) (* f15 f1241))) (define-fun f1248 () Arctic (+ f16 f1246)) (define-fun f1249 () Arctic (+ f17 f1247)) (define-fun f1250 () Arctic (+ (* f12 f1242) (* f13 f1244))) (define-fun f1251 () Arctic (+ (* f12 f1243) (* f13 f1245))) (define-fun f1252 () Arctic (+ (* f14 f1242) (* f15 f1244))) (define-fun f1253 () Arctic (+ (* f14 f1243) (* f15 f1245))) (define-fun f1254 () Arctic (+ (* f12 f1248) (* f13 f1249))) (define-fun f1255 () Arctic (+ (* f14 f1248) (* f15 f1249))) (define-fun f1256 () Arctic (+ f16 f1254)) (define-fun f1257 () Arctic (+ f17 f1255)) (define-fun f1258 () Arctic (+ (* f12 f1250) (* f13 f1252))) (define-fun f1259 () Arctic (+ (* f12 f1251) (* f13 f1253))) (define-fun f1260 () Arctic (+ (* f14 f1250) (* f15 f1252))) (define-fun f1261 () Arctic (+ (* f14 f1251) (* f15 f1253))) (define-fun f1262 () Arctic (+ (* f12 f1256) (* f13 f1257))) (define-fun f1263 () Arctic (+ (* f14 f1256) (* f15 f1257))) (define-fun f1264 () Arctic (+ f16 f1262)) (define-fun f1265 () Arctic (+ f17 f1263)) (define-fun f1266 () Arctic (+ (* f12 f1258) (* f13 f1260))) (define-fun f1267 () Arctic (+ (* f12 f1259) (* f13 f1261))) (define-fun f1268 () Arctic (+ (* f14 f1258) (* f15 f1260))) (define-fun f1269 () Arctic (+ (* f14 f1259) (* f15 f1261))) (define-fun f1270 () Arctic (+ (* f12 f1264) (* f13 f1265))) (define-fun f1271 () Arctic (+ (* f14 f1264) (* f15 f1265))) (define-fun f1272 () Arctic (+ f16 f1270)) (define-fun f1273 () Arctic (+ f17 f1271)) (define-fun f1274 () Arctic (+ (* f0 f1266) (* f1 f1268))) (define-fun f1275 () Arctic (+ (* f0 f1267) (* f1 f1269))) (define-fun f1276 () Arctic (+ (* f2 f1266) (* f3 f1268))) (define-fun f1277 () Arctic (+ (* f2 f1267) (* f3 f1269))) (define-fun f1278 () Arctic (+ (* f0 f1272) (* f1 f1273))) (define-fun f1279 () Arctic (+ (* f2 f1272) (* f3 f1273))) (define-fun f1280 () Arctic (+ f4 f1278)) (define-fun f1281 () Arctic (+ f5 f1279)) (define-fun f1282 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1283 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1284 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1285 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1286 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1287 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1288 () Arctic (+ f16 f1286)) (define-fun f1289 () Arctic (+ f17 f1287)) (define-fun f1290 () Arctic (+ (* f12 f1282) (* f13 f1284))) (define-fun f1291 () Arctic (+ (* f12 f1283) (* f13 f1285))) (define-fun f1292 () Arctic (+ (* f14 f1282) (* f15 f1284))) (define-fun f1293 () Arctic (+ (* f14 f1283) (* f15 f1285))) (define-fun f1294 () Arctic (+ (* f12 f1288) (* f13 f1289))) (define-fun f1295 () Arctic (+ (* f14 f1288) (* f15 f1289))) (define-fun f1296 () Arctic (+ f16 f1294)) (define-fun f1297 () Arctic (+ f17 f1295)) (define-fun f1298 () Arctic (+ (* f6 f1290) (* f7 f1292))) (define-fun f1299 () Arctic (+ (* f6 f1291) (* f7 f1293))) (define-fun f1300 () Arctic (+ (* f8 f1290) (* f9 f1292))) (define-fun f1301 () Arctic (+ (* f8 f1291) (* f9 f1293))) (define-fun f1302 () Arctic (+ (* f6 f1296) (* f7 f1297))) (define-fun f1303 () Arctic (+ (* f8 f1296) (* f9 f1297))) (define-fun f1304 () Arctic (+ f10 f1302)) (define-fun f1305 () Arctic (+ f11 f1303)) (define-fun f1306 () Arctic (+ (* f12 f1298) (* f13 f1300))) (define-fun f1307 () Arctic (+ (* f12 f1299) (* f13 f1301))) (define-fun f1308 () Arctic (+ (* f14 f1298) (* f15 f1300))) (define-fun f1309 () Arctic (+ (* f14 f1299) (* f15 f1301))) (define-fun f1310 () Arctic (+ (* f12 f1304) (* f13 f1305))) (define-fun f1311 () Arctic (+ (* f14 f1304) (* f15 f1305))) (define-fun f1312 () Arctic (+ f16 f1310)) (define-fun f1313 () Arctic (+ f17 f1311)) (define-fun f1314 () Arctic (+ (* f12 f1306) (* f13 f1308))) (define-fun f1315 () Arctic (+ (* f12 f1307) (* f13 f1309))) (define-fun f1316 () Arctic (+ (* f14 f1306) (* f15 f1308))) (define-fun f1317 () Arctic (+ (* f14 f1307) (* f15 f1309))) (define-fun f1318 () Arctic (+ (* f12 f1312) (* f13 f1313))) (define-fun f1319 () Arctic (+ (* f14 f1312) (* f15 f1313))) (define-fun f1320 () Arctic (+ f16 f1318)) (define-fun f1321 () Arctic (+ f17 f1319)) (define-fun f1322 () Arctic (+ (* f12 f1314) (* f13 f1316))) (define-fun f1323 () Arctic (+ (* f12 f1315) (* f13 f1317))) (define-fun f1324 () Arctic (+ (* f14 f1314) (* f15 f1316))) (define-fun f1325 () Arctic (+ (* f14 f1315) (* f15 f1317))) (define-fun f1326 () Arctic (+ (* f12 f1320) (* f13 f1321))) (define-fun f1327 () Arctic (+ (* f14 f1320) (* f15 f1321))) (define-fun f1328 () Arctic (+ f16 f1326)) (define-fun f1329 () Arctic (+ f17 f1327)) (define-fun f1330 () Arctic (+ (* f12 f1322) (* f13 f1324))) (define-fun f1331 () Arctic (+ (* f12 f1323) (* f13 f1325))) (define-fun f1332 () Arctic (+ (* f14 f1322) (* f15 f1324))) (define-fun f1333 () Arctic (+ (* f14 f1323) (* f15 f1325))) (define-fun f1334 () Arctic (+ (* f12 f1328) (* f13 f1329))) (define-fun f1335 () Arctic (+ (* f14 f1328) (* f15 f1329))) (define-fun f1336 () Arctic (+ f16 f1334)) (define-fun f1337 () Arctic (+ f17 f1335)) (define-fun f1338 () Arctic (+ (* f0 f1330) (* f1 f1332))) (define-fun f1339 () Arctic (+ (* f0 f1331) (* f1 f1333))) (define-fun f1340 () Arctic (+ (* f2 f1330) (* f3 f1332))) (define-fun f1341 () Arctic (+ (* f2 f1331) (* f3 f1333))) (define-fun f1342 () Arctic (+ (* f0 f1336) (* f1 f1337))) (define-fun f1343 () Arctic (+ (* f2 f1336) (* f3 f1337))) (define-fun f1344 () Arctic (+ f4 f1342)) (define-fun f1345 () Arctic (+ f5 f1343)) (define-fun f1346 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1347 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1348 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1349 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1350 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1351 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1352 () Arctic (+ f16 f1350)) (define-fun f1353 () Arctic (+ f17 f1351)) (define-fun f1354 () Arctic (+ (* f6 f1346) (* f7 f1348))) (define-fun f1355 () Arctic (+ (* f6 f1347) (* f7 f1349))) (define-fun f1356 () Arctic (+ (* f8 f1346) (* f9 f1348))) (define-fun f1357 () Arctic (+ (* f8 f1347) (* f9 f1349))) (define-fun f1358 () Arctic (+ (* f6 f1352) (* f7 f1353))) (define-fun f1359 () Arctic (+ (* f8 f1352) (* f9 f1353))) (define-fun f1360 () Arctic (+ f10 f1358)) (define-fun f1361 () Arctic (+ f11 f1359)) (define-fun f1362 () Arctic (+ (* f12 f1354) (* f13 f1356))) (define-fun f1363 () Arctic (+ (* f12 f1355) (* f13 f1357))) (define-fun f1364 () Arctic (+ (* f14 f1354) (* f15 f1356))) (define-fun f1365 () Arctic (+ (* f14 f1355) (* f15 f1357))) (define-fun f1366 () Arctic (+ (* f12 f1360) (* f13 f1361))) (define-fun f1367 () Arctic (+ (* f14 f1360) (* f15 f1361))) (define-fun f1368 () Arctic (+ f16 f1366)) (define-fun f1369 () Arctic (+ f17 f1367)) (define-fun f1370 () Arctic (+ (* f12 f1362) (* f13 f1364))) (define-fun f1371 () Arctic (+ (* f12 f1363) (* f13 f1365))) (define-fun f1372 () Arctic (+ (* f14 f1362) (* f15 f1364))) (define-fun f1373 () Arctic (+ (* f14 f1363) (* f15 f1365))) (define-fun f1374 () Arctic (+ (* f12 f1368) (* f13 f1369))) (define-fun f1375 () Arctic (+ (* f14 f1368) (* f15 f1369))) (define-fun f1376 () Arctic (+ f16 f1374)) (define-fun f1377 () Arctic (+ f17 f1375)) (define-fun f1378 () Arctic (+ (* f6 f1370) (* f7 f1372))) (define-fun f1379 () Arctic (+ (* f6 f1371) (* f7 f1373))) (define-fun f1380 () Arctic (+ (* f8 f1370) (* f9 f1372))) (define-fun f1381 () Arctic (+ (* f8 f1371) (* f9 f1373))) (define-fun f1382 () Arctic (+ (* f6 f1376) (* f7 f1377))) (define-fun f1383 () Arctic (+ (* f8 f1376) (* f9 f1377))) (define-fun f1384 () Arctic (+ f10 f1382)) (define-fun f1385 () Arctic (+ f11 f1383)) (define-fun f1386 () Arctic (+ (* f12 f1378) (* f13 f1380))) (define-fun f1387 () Arctic (+ (* f12 f1379) (* f13 f1381))) (define-fun f1388 () Arctic (+ (* f14 f1378) (* f15 f1380))) (define-fun f1389 () Arctic (+ (* f14 f1379) (* f15 f1381))) (define-fun f1390 () Arctic (+ (* f12 f1384) (* f13 f1385))) (define-fun f1391 () Arctic (+ (* f14 f1384) (* f15 f1385))) (define-fun f1392 () Arctic (+ f16 f1390)) (define-fun f1393 () Arctic (+ f17 f1391)) (define-fun f1394 () Arctic (+ (* f12 f1386) (* f13 f1388))) (define-fun f1395 () Arctic (+ (* f12 f1387) (* f13 f1389))) (define-fun f1396 () Arctic (+ (* f14 f1386) (* f15 f1388))) (define-fun f1397 () Arctic (+ (* f14 f1387) (* f15 f1389))) (define-fun f1398 () Arctic (+ (* f12 f1392) (* f13 f1393))) (define-fun f1399 () Arctic (+ (* f14 f1392) (* f15 f1393))) (define-fun f1400 () Arctic (+ f16 f1398)) (define-fun f1401 () Arctic (+ f17 f1399)) (define-fun f1402 () Arctic (+ (* f12 f1394) (* f13 f1396))) (define-fun f1403 () Arctic (+ (* f12 f1395) (* f13 f1397))) (define-fun f1404 () Arctic (+ (* f14 f1394) (* f15 f1396))) (define-fun f1405 () Arctic (+ (* f14 f1395) (* f15 f1397))) (define-fun f1406 () Arctic (+ (* f12 f1400) (* f13 f1401))) (define-fun f1407 () Arctic (+ (* f14 f1400) (* f15 f1401))) (define-fun f1408 () Arctic (+ f16 f1406)) (define-fun f1409 () Arctic (+ f17 f1407)) (define-fun f1410 () Arctic (+ (* f0 f1402) (* f1 f1404))) (define-fun f1411 () Arctic (+ (* f0 f1403) (* f1 f1405))) (define-fun f1412 () Arctic (+ (* f2 f1402) (* f3 f1404))) (define-fun f1413 () Arctic (+ (* f2 f1403) (* f3 f1405))) (define-fun f1414 () Arctic (+ (* f0 f1408) (* f1 f1409))) (define-fun f1415 () Arctic (+ (* f2 f1408) (* f3 f1409))) (define-fun f1416 () Arctic (+ f4 f1414)) (define-fun f1417 () Arctic (+ f5 f1415)) (define-fun f1418 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1419 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1420 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1421 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1422 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1423 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1424 () Arctic (+ f16 f1422)) (define-fun f1425 () Arctic (+ f17 f1423)) (define-fun f1426 () Arctic (+ (* f12 f1418) (* f13 f1420))) (define-fun f1427 () Arctic (+ (* f12 f1419) (* f13 f1421))) (define-fun f1428 () Arctic (+ (* f14 f1418) (* f15 f1420))) (define-fun f1429 () Arctic (+ (* f14 f1419) (* f15 f1421))) (define-fun f1430 () Arctic (+ (* f12 f1424) (* f13 f1425))) (define-fun f1431 () Arctic (+ (* f14 f1424) (* f15 f1425))) (define-fun f1432 () Arctic (+ f16 f1430)) (define-fun f1433 () Arctic (+ f17 f1431)) (define-fun f1434 () Arctic (+ (* f6 f1426) (* f7 f1428))) (define-fun f1435 () Arctic (+ (* f6 f1427) (* f7 f1429))) (define-fun f1436 () Arctic (+ (* f8 f1426) (* f9 f1428))) (define-fun f1437 () Arctic (+ (* f8 f1427) (* f9 f1429))) (define-fun f1438 () Arctic (+ (* f6 f1432) (* f7 f1433))) (define-fun f1439 () Arctic (+ (* f8 f1432) (* f9 f1433))) (define-fun f1440 () Arctic (+ f10 f1438)) (define-fun f1441 () Arctic (+ f11 f1439)) (define-fun f1442 () Arctic (+ (* f12 f1434) (* f13 f1436))) (define-fun f1443 () Arctic (+ (* f12 f1435) (* f13 f1437))) (define-fun f1444 () Arctic (+ (* f14 f1434) (* f15 f1436))) (define-fun f1445 () Arctic (+ (* f14 f1435) (* f15 f1437))) (define-fun f1446 () Arctic (+ (* f12 f1440) (* f13 f1441))) (define-fun f1447 () Arctic (+ (* f14 f1440) (* f15 f1441))) (define-fun f1448 () Arctic (+ f16 f1446)) (define-fun f1449 () Arctic (+ f17 f1447)) (define-fun f1450 () Arctic (+ (* f12 f1442) (* f13 f1444))) (define-fun f1451 () Arctic (+ (* f12 f1443) (* f13 f1445))) (define-fun f1452 () Arctic (+ (* f14 f1442) (* f15 f1444))) (define-fun f1453 () Arctic (+ (* f14 f1443) (* f15 f1445))) (define-fun f1454 () Arctic (+ (* f12 f1448) (* f13 f1449))) (define-fun f1455 () Arctic (+ (* f14 f1448) (* f15 f1449))) (define-fun f1456 () Arctic (+ f16 f1454)) (define-fun f1457 () Arctic (+ f17 f1455)) (define-fun f1458 () Arctic (+ (* f12 f1450) (* f13 f1452))) (define-fun f1459 () Arctic (+ (* f12 f1451) (* f13 f1453))) (define-fun f1460 () Arctic (+ (* f14 f1450) (* f15 f1452))) (define-fun f1461 () Arctic (+ (* f14 f1451) (* f15 f1453))) (define-fun f1462 () Arctic (+ (* f12 f1456) (* f13 f1457))) (define-fun f1463 () Arctic (+ (* f14 f1456) (* f15 f1457))) (define-fun f1464 () Arctic (+ f16 f1462)) (define-fun f1465 () Arctic (+ f17 f1463)) (define-fun f1466 () Arctic (+ (* f12 f1458) (* f13 f1460))) (define-fun f1467 () Arctic (+ (* f12 f1459) (* f13 f1461))) (define-fun f1468 () Arctic (+ (* f14 f1458) (* f15 f1460))) (define-fun f1469 () Arctic (+ (* f14 f1459) (* f15 f1461))) (define-fun f1470 () Arctic (+ (* f12 f1464) (* f13 f1465))) (define-fun f1471 () Arctic (+ (* f14 f1464) (* f15 f1465))) (define-fun f1472 () Arctic (+ f16 f1470)) (define-fun f1473 () Arctic (+ f17 f1471)) (define-fun f1474 () Arctic (+ (* f0 f1466) (* f1 f1468))) (define-fun f1475 () Arctic (+ (* f0 f1467) (* f1 f1469))) (define-fun f1476 () Arctic (+ (* f2 f1466) (* f3 f1468))) (define-fun f1477 () Arctic (+ (* f2 f1467) (* f3 f1469))) (define-fun f1478 () Arctic (+ (* f0 f1472) (* f1 f1473))) (define-fun f1479 () Arctic (+ (* f2 f1472) (* f3 f1473))) (define-fun f1480 () Arctic (+ f4 f1478)) (define-fun f1481 () Arctic (+ f5 f1479)) (define-fun f1482 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1483 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1484 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1485 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1486 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1487 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1488 () Arctic (+ f16 f1486)) (define-fun f1489 () Arctic (+ f17 f1487)) (define-fun f1490 () Arctic (+ (* f6 f1482) (* f7 f1484))) (define-fun f1491 () Arctic (+ (* f6 f1483) (* f7 f1485))) (define-fun f1492 () Arctic (+ (* f8 f1482) (* f9 f1484))) (define-fun f1493 () Arctic (+ (* f8 f1483) (* f9 f1485))) (define-fun f1494 () Arctic (+ (* f6 f1488) (* f7 f1489))) (define-fun f1495 () Arctic (+ (* f8 f1488) (* f9 f1489))) (define-fun f1496 () Arctic (+ f10 f1494)) (define-fun f1497 () Arctic (+ f11 f1495)) (define-fun f1498 () Arctic (+ (* f12 f1490) (* f13 f1492))) (define-fun f1499 () Arctic (+ (* f12 f1491) (* f13 f1493))) (define-fun f1500 () Arctic (+ (* f14 f1490) (* f15 f1492))) (define-fun f1501 () Arctic (+ (* f14 f1491) (* f15 f1493))) (define-fun f1502 () Arctic (+ (* f12 f1496) (* f13 f1497))) (define-fun f1503 () Arctic (+ (* f14 f1496) (* f15 f1497))) (define-fun f1504 () Arctic (+ f16 f1502)) (define-fun f1505 () Arctic (+ f17 f1503)) (define-fun f1506 () Arctic (+ (* f12 f1498) (* f13 f1500))) (define-fun f1507 () Arctic (+ (* f12 f1499) (* f13 f1501))) (define-fun f1508 () Arctic (+ (* f14 f1498) (* f15 f1500))) (define-fun f1509 () Arctic (+ (* f14 f1499) (* f15 f1501))) (define-fun f1510 () Arctic (+ (* f12 f1504) (* f13 f1505))) (define-fun f1511 () Arctic (+ (* f14 f1504) (* f15 f1505))) (define-fun f1512 () Arctic (+ f16 f1510)) (define-fun f1513 () Arctic (+ f17 f1511)) (define-fun f1514 () Arctic (+ (* f0 f1506) (* f1 f1508))) (define-fun f1515 () Arctic (+ (* f0 f1507) (* f1 f1509))) (define-fun f1516 () Arctic (+ (* f2 f1506) (* f3 f1508))) (define-fun f1517 () Arctic (+ (* f2 f1507) (* f3 f1509))) (define-fun f1518 () Arctic (+ (* f0 f1512) (* f1 f1513))) (define-fun f1519 () Arctic (+ (* f2 f1512) (* f3 f1513))) (define-fun f1520 () Arctic (+ f4 f1518)) (define-fun f1521 () Arctic (+ f5 f1519)) (define-fun f1522 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1523 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1524 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1525 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1526 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1527 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1528 () Arctic (+ f16 f1526)) (define-fun f1529 () Arctic (+ f17 f1527)) (define-fun f1530 () Arctic (+ (* f12 f1522) (* f13 f1524))) (define-fun f1531 () Arctic (+ (* f12 f1523) (* f13 f1525))) (define-fun f1532 () Arctic (+ (* f14 f1522) (* f15 f1524))) (define-fun f1533 () Arctic (+ (* f14 f1523) (* f15 f1525))) (define-fun f1534 () Arctic (+ (* f12 f1528) (* f13 f1529))) (define-fun f1535 () Arctic (+ (* f14 f1528) (* f15 f1529))) (define-fun f1536 () Arctic (+ f16 f1534)) (define-fun f1537 () Arctic (+ f17 f1535)) (define-fun f1538 () Arctic (+ (* f6 f1530) (* f7 f1532))) (define-fun f1539 () Arctic (+ (* f6 f1531) (* f7 f1533))) (define-fun f1540 () Arctic (+ (* f8 f1530) (* f9 f1532))) (define-fun f1541 () Arctic (+ (* f8 f1531) (* f9 f1533))) (define-fun f1542 () Arctic (+ (* f6 f1536) (* f7 f1537))) (define-fun f1543 () Arctic (+ (* f8 f1536) (* f9 f1537))) (define-fun f1544 () Arctic (+ f10 f1542)) (define-fun f1545 () Arctic (+ f11 f1543)) (define-fun f1546 () Arctic (+ (* f12 f1538) (* f13 f1540))) (define-fun f1547 () Arctic (+ (* f12 f1539) (* f13 f1541))) (define-fun f1548 () Arctic (+ (* f14 f1538) (* f15 f1540))) (define-fun f1549 () Arctic (+ (* f14 f1539) (* f15 f1541))) (define-fun f1550 () Arctic (+ (* f12 f1544) (* f13 f1545))) (define-fun f1551 () Arctic (+ (* f14 f1544) (* f15 f1545))) (define-fun f1552 () Arctic (+ f16 f1550)) (define-fun f1553 () Arctic (+ f17 f1551)) (define-fun f1554 () Arctic (+ (* f12 f1546) (* f13 f1548))) (define-fun f1555 () Arctic (+ (* f12 f1547) (* f13 f1549))) (define-fun f1556 () Arctic (+ (* f14 f1546) (* f15 f1548))) (define-fun f1557 () Arctic (+ (* f14 f1547) (* f15 f1549))) (define-fun f1558 () Arctic (+ (* f12 f1552) (* f13 f1553))) (define-fun f1559 () Arctic (+ (* f14 f1552) (* f15 f1553))) (define-fun f1560 () Arctic (+ f16 f1558)) (define-fun f1561 () Arctic (+ f17 f1559)) (define-fun f1562 () Arctic (+ (* f12 f1554) (* f13 f1556))) (define-fun f1563 () Arctic (+ (* f12 f1555) (* f13 f1557))) (define-fun f1564 () Arctic (+ (* f14 f1554) (* f15 f1556))) (define-fun f1565 () Arctic (+ (* f14 f1555) (* f15 f1557))) (define-fun f1566 () Arctic (+ (* f12 f1560) (* f13 f1561))) (define-fun f1567 () Arctic (+ (* f14 f1560) (* f15 f1561))) (define-fun f1568 () Arctic (+ f16 f1566)) (define-fun f1569 () Arctic (+ f17 f1567)) (define-fun f1570 () Arctic (+ (* f12 f1562) (* f13 f1564))) (define-fun f1571 () Arctic (+ (* f12 f1563) (* f13 f1565))) (define-fun f1572 () Arctic (+ (* f14 f1562) (* f15 f1564))) (define-fun f1573 () Arctic (+ (* f14 f1563) (* f15 f1565))) (define-fun f1574 () Arctic (+ (* f12 f1568) (* f13 f1569))) (define-fun f1575 () Arctic (+ (* f14 f1568) (* f15 f1569))) (define-fun f1576 () Arctic (+ f16 f1574)) (define-fun f1577 () Arctic (+ f17 f1575)) (define-fun f1578 () Arctic (+ (* f0 f1570) (* f1 f1572))) (define-fun f1579 () Arctic (+ (* f0 f1571) (* f1 f1573))) (define-fun f1580 () Arctic (+ (* f2 f1570) (* f3 f1572))) (define-fun f1581 () Arctic (+ (* f2 f1571) (* f3 f1573))) (define-fun f1582 () Arctic (+ (* f0 f1576) (* f1 f1577))) (define-fun f1583 () Arctic (+ (* f2 f1576) (* f3 f1577))) (define-fun f1584 () Arctic (+ f4 f1582)) (define-fun f1585 () Arctic (+ f5 f1583)) (define-fun f1586 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1587 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1588 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1589 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1590 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1591 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1592 () Arctic (+ f16 f1590)) (define-fun f1593 () Arctic (+ f17 f1591)) (define-fun f1594 () Arctic (+ (* f0 f1586) (* f1 f1588))) (define-fun f1595 () Arctic (+ (* f0 f1587) (* f1 f1589))) (define-fun f1596 () Arctic (+ (* f2 f1586) (* f3 f1588))) (define-fun f1597 () Arctic (+ (* f2 f1587) (* f3 f1589))) (define-fun f1598 () Arctic (+ (* f0 f1592) (* f1 f1593))) (define-fun f1599 () Arctic (+ (* f2 f1592) (* f3 f1593))) (define-fun f1600 () Arctic (+ f4 f1598)) (define-fun f1601 () Arctic (+ f5 f1599)) (define-fun f1602 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1603 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1604 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1605 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1606 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1607 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1608 () Arctic (+ f16 f1606)) (define-fun f1609 () Arctic (+ f17 f1607)) (define-fun f1610 () Arctic (+ (* f12 f1602) (* f13 f1604))) (define-fun f1611 () Arctic (+ (* f12 f1603) (* f13 f1605))) (define-fun f1612 () Arctic (+ (* f14 f1602) (* f15 f1604))) (define-fun f1613 () Arctic (+ (* f14 f1603) (* f15 f1605))) (define-fun f1614 () Arctic (+ (* f12 f1608) (* f13 f1609))) (define-fun f1615 () Arctic (+ (* f14 f1608) (* f15 f1609))) (define-fun f1616 () Arctic (+ f16 f1614)) (define-fun f1617 () Arctic (+ f17 f1615)) (define-fun f1618 () Arctic (+ (* f6 f1610) (* f7 f1612))) (define-fun f1619 () Arctic (+ (* f6 f1611) (* f7 f1613))) (define-fun f1620 () Arctic (+ (* f8 f1610) (* f9 f1612))) (define-fun f1621 () Arctic (+ (* f8 f1611) (* f9 f1613))) (define-fun f1622 () Arctic (+ (* f6 f1616) (* f7 f1617))) (define-fun f1623 () Arctic (+ (* f8 f1616) (* f9 f1617))) (define-fun f1624 () Arctic (+ f10 f1622)) (define-fun f1625 () Arctic (+ f11 f1623)) (define-fun f1626 () Arctic (+ (* f12 f1618) (* f13 f1620))) (define-fun f1627 () Arctic (+ (* f12 f1619) (* f13 f1621))) (define-fun f1628 () Arctic (+ (* f14 f1618) (* f15 f1620))) (define-fun f1629 () Arctic (+ (* f14 f1619) (* f15 f1621))) (define-fun f1630 () Arctic (+ (* f12 f1624) (* f13 f1625))) (define-fun f1631 () Arctic (+ (* f14 f1624) (* f15 f1625))) (define-fun f1632 () Arctic (+ f16 f1630)) (define-fun f1633 () Arctic (+ f17 f1631)) (define-fun f1634 () Arctic (+ (* f12 f1626) (* f13 f1628))) (define-fun f1635 () Arctic (+ (* f12 f1627) (* f13 f1629))) (define-fun f1636 () Arctic (+ (* f14 f1626) (* f15 f1628))) (define-fun f1637 () Arctic (+ (* f14 f1627) (* f15 f1629))) (define-fun f1638 () Arctic (+ (* f12 f1632) (* f13 f1633))) (define-fun f1639 () Arctic (+ (* f14 f1632) (* f15 f1633))) (define-fun f1640 () Arctic (+ f16 f1638)) (define-fun f1641 () Arctic (+ f17 f1639)) (define-fun f1642 () Arctic (+ (* f12 f1634) (* f13 f1636))) (define-fun f1643 () Arctic (+ (* f12 f1635) (* f13 f1637))) (define-fun f1644 () Arctic (+ (* f14 f1634) (* f15 f1636))) (define-fun f1645 () Arctic (+ (* f14 f1635) (* f15 f1637))) (define-fun f1646 () Arctic (+ (* f12 f1640) (* f13 f1641))) (define-fun f1647 () Arctic (+ (* f14 f1640) (* f15 f1641))) (define-fun f1648 () Arctic (+ f16 f1646)) (define-fun f1649 () Arctic (+ f17 f1647)) (define-fun f1650 () Arctic (+ (* f12 f1642) (* f13 f1644))) (define-fun f1651 () Arctic (+ (* f12 f1643) (* f13 f1645))) (define-fun f1652 () Arctic (+ (* f14 f1642) (* f15 f1644))) (define-fun f1653 () Arctic (+ (* f14 f1643) (* f15 f1645))) (define-fun f1654 () Arctic (+ (* f12 f1648) (* f13 f1649))) (define-fun f1655 () Arctic (+ (* f14 f1648) (* f15 f1649))) (define-fun f1656 () Arctic (+ f16 f1654)) (define-fun f1657 () Arctic (+ f17 f1655)) (define-fun f1658 () Arctic (+ (* f0 f1650) (* f1 f1652))) (define-fun f1659 () Arctic (+ (* f0 f1651) (* f1 f1653))) (define-fun f1660 () Arctic (+ (* f2 f1650) (* f3 f1652))) (define-fun f1661 () Arctic (+ (* f2 f1651) (* f3 f1653))) (define-fun f1662 () Arctic (+ (* f0 f1656) (* f1 f1657))) (define-fun f1663 () Arctic (+ (* f2 f1656) (* f3 f1657))) (define-fun f1664 () Arctic (+ f4 f1662)) (define-fun f1665 () Arctic (+ f5 f1663)) (define-fun f1666 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1667 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1668 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1669 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1670 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1671 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1672 () Arctic (+ f16 f1670)) (define-fun f1673 () Arctic (+ f17 f1671)) (define-fun f1674 () Arctic (+ (* f12 f1666) (* f13 f1668))) (define-fun f1675 () Arctic (+ (* f12 f1667) (* f13 f1669))) (define-fun f1676 () Arctic (+ (* f14 f1666) (* f15 f1668))) (define-fun f1677 () Arctic (+ (* f14 f1667) (* f15 f1669))) (define-fun f1678 () Arctic (+ (* f12 f1672) (* f13 f1673))) (define-fun f1679 () Arctic (+ (* f14 f1672) (* f15 f1673))) (define-fun f1680 () Arctic (+ f16 f1678)) (define-fun f1681 () Arctic (+ f17 f1679)) (define-fun f1682 () Arctic (+ (* f12 f1674) (* f13 f1676))) (define-fun f1683 () Arctic (+ (* f12 f1675) (* f13 f1677))) (define-fun f1684 () Arctic (+ (* f14 f1674) (* f15 f1676))) (define-fun f1685 () Arctic (+ (* f14 f1675) (* f15 f1677))) (define-fun f1686 () Arctic (+ (* f12 f1680) (* f13 f1681))) (define-fun f1687 () Arctic (+ (* f14 f1680) (* f15 f1681))) (define-fun f1688 () Arctic (+ f16 f1686)) (define-fun f1689 () Arctic (+ f17 f1687)) (define-fun f1690 () Arctic (+ (* f6 f1682) (* f7 f1684))) (define-fun f1691 () Arctic (+ (* f6 f1683) (* f7 f1685))) (define-fun f1692 () Arctic (+ (* f8 f1682) (* f9 f1684))) (define-fun f1693 () Arctic (+ (* f8 f1683) (* f9 f1685))) (define-fun f1694 () Arctic (+ (* f6 f1688) (* f7 f1689))) (define-fun f1695 () Arctic (+ (* f8 f1688) (* f9 f1689))) (define-fun f1696 () Arctic (+ f10 f1694)) (define-fun f1697 () Arctic (+ f11 f1695)) (define-fun f1698 () Arctic (+ (* f12 f1690) (* f13 f1692))) (define-fun f1699 () Arctic (+ (* f12 f1691) (* f13 f1693))) (define-fun f1700 () Arctic (+ (* f14 f1690) (* f15 f1692))) (define-fun f1701 () Arctic (+ (* f14 f1691) (* f15 f1693))) (define-fun f1702 () Arctic (+ (* f12 f1696) (* f13 f1697))) (define-fun f1703 () Arctic (+ (* f14 f1696) (* f15 f1697))) (define-fun f1704 () Arctic (+ f16 f1702)) (define-fun f1705 () Arctic (+ f17 f1703)) (define-fun f1706 () Arctic (+ (* f12 f1698) (* f13 f1700))) (define-fun f1707 () Arctic (+ (* f12 f1699) (* f13 f1701))) (define-fun f1708 () Arctic (+ (* f14 f1698) (* f15 f1700))) (define-fun f1709 () Arctic (+ (* f14 f1699) (* f15 f1701))) (define-fun f1710 () Arctic (+ (* f12 f1704) (* f13 f1705))) (define-fun f1711 () Arctic (+ (* f14 f1704) (* f15 f1705))) (define-fun f1712 () Arctic (+ f16 f1710)) (define-fun f1713 () Arctic (+ f17 f1711)) (define-fun f1714 () Arctic (+ (* f12 f1706) (* f13 f1708))) (define-fun f1715 () Arctic (+ (* f12 f1707) (* f13 f1709))) (define-fun f1716 () Arctic (+ (* f14 f1706) (* f15 f1708))) (define-fun f1717 () Arctic (+ (* f14 f1707) (* f15 f1709))) (define-fun f1718 () Arctic (+ (* f12 f1712) (* f13 f1713))) (define-fun f1719 () Arctic (+ (* f14 f1712) (* f15 f1713))) (define-fun f1720 () Arctic (+ f16 f1718)) (define-fun f1721 () Arctic (+ f17 f1719)) (define-fun f1722 () Arctic (+ (* f12 f1714) (* f13 f1716))) (define-fun f1723 () Arctic (+ (* f12 f1715) (* f13 f1717))) (define-fun f1724 () Arctic (+ (* f14 f1714) (* f15 f1716))) (define-fun f1725 () Arctic (+ (* f14 f1715) (* f15 f1717))) (define-fun f1726 () Arctic (+ (* f12 f1720) (* f13 f1721))) (define-fun f1727 () Arctic (+ (* f14 f1720) (* f15 f1721))) (define-fun f1728 () Arctic (+ f16 f1726)) (define-fun f1729 () Arctic (+ f17 f1727)) (define-fun f1730 () Arctic (+ (* f0 f1722) (* f1 f1724))) (define-fun f1731 () Arctic (+ (* f0 f1723) (* f1 f1725))) (define-fun f1732 () Arctic (+ (* f2 f1722) (* f3 f1724))) (define-fun f1733 () Arctic (+ (* f2 f1723) (* f3 f1725))) (define-fun f1734 () Arctic (+ (* f0 f1728) (* f1 f1729))) (define-fun f1735 () Arctic (+ (* f2 f1728) (* f3 f1729))) (define-fun f1736 () Arctic (+ f4 f1734)) (define-fun f1737 () Arctic (+ f5 f1735)) (define-fun f1738 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1739 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1740 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1741 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1742 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1743 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1744 () Arctic (+ f16 f1742)) (define-fun f1745 () Arctic (+ f17 f1743)) (define-fun f1746 () Arctic (+ (* f12 f1738) (* f13 f1740))) (define-fun f1747 () Arctic (+ (* f12 f1739) (* f13 f1741))) (define-fun f1748 () Arctic (+ (* f14 f1738) (* f15 f1740))) (define-fun f1749 () Arctic (+ (* f14 f1739) (* f15 f1741))) (define-fun f1750 () Arctic (+ (* f12 f1744) (* f13 f1745))) (define-fun f1751 () Arctic (+ (* f14 f1744) (* f15 f1745))) (define-fun f1752 () Arctic (+ f16 f1750)) (define-fun f1753 () Arctic (+ f17 f1751)) (define-fun f1754 () Arctic (+ (* f6 f1746) (* f7 f1748))) (define-fun f1755 () Arctic (+ (* f6 f1747) (* f7 f1749))) (define-fun f1756 () Arctic (+ (* f8 f1746) (* f9 f1748))) (define-fun f1757 () Arctic (+ (* f8 f1747) (* f9 f1749))) (define-fun f1758 () Arctic (+ (* f6 f1752) (* f7 f1753))) (define-fun f1759 () Arctic (+ (* f8 f1752) (* f9 f1753))) (define-fun f1760 () Arctic (+ f10 f1758)) (define-fun f1761 () Arctic (+ f11 f1759)) (define-fun f1762 () Arctic (+ (* f6 f1754) (* f7 f1756))) (define-fun f1763 () Arctic (+ (* f6 f1755) (* f7 f1757))) (define-fun f1764 () Arctic (+ (* f8 f1754) (* f9 f1756))) (define-fun f1765 () Arctic (+ (* f8 f1755) (* f9 f1757))) (define-fun f1766 () Arctic (+ (* f6 f1760) (* f7 f1761))) (define-fun f1767 () Arctic (+ (* f8 f1760) (* f9 f1761))) (define-fun f1768 () Arctic (+ f10 f1766)) (define-fun f1769 () Arctic (+ f11 f1767)) (define-fun f1770 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1771 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1772 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1773 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1774 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1775 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1776 () Arctic (+ f16 f1774)) (define-fun f1777 () Arctic (+ f17 f1775)) (define-fun f1778 () Arctic (+ (* f12 f1770) (* f13 f1772))) (define-fun f1779 () Arctic (+ (* f12 f1771) (* f13 f1773))) (define-fun f1780 () Arctic (+ (* f14 f1770) (* f15 f1772))) (define-fun f1781 () Arctic (+ (* f14 f1771) (* f15 f1773))) (define-fun f1782 () Arctic (+ (* f12 f1776) (* f13 f1777))) (define-fun f1783 () Arctic (+ (* f14 f1776) (* f15 f1777))) (define-fun f1784 () Arctic (+ f16 f1782)) (define-fun f1785 () Arctic (+ f17 f1783)) (define-fun f1786 () Arctic (+ (* f12 f1778) (* f13 f1780))) (define-fun f1787 () Arctic (+ (* f12 f1779) (* f13 f1781))) (define-fun f1788 () Arctic (+ (* f14 f1778) (* f15 f1780))) (define-fun f1789 () Arctic (+ (* f14 f1779) (* f15 f1781))) (define-fun f1790 () Arctic (+ (* f12 f1784) (* f13 f1785))) (define-fun f1791 () Arctic (+ (* f14 f1784) (* f15 f1785))) (define-fun f1792 () Arctic (+ f16 f1790)) (define-fun f1793 () Arctic (+ f17 f1791)) (define-fun f1794 () Arctic (+ (* f12 f1786) (* f13 f1788))) (define-fun f1795 () Arctic (+ (* f12 f1787) (* f13 f1789))) (define-fun f1796 () Arctic (+ (* f14 f1786) (* f15 f1788))) (define-fun f1797 () Arctic (+ (* f14 f1787) (* f15 f1789))) (define-fun f1798 () Arctic (+ (* f12 f1792) (* f13 f1793))) (define-fun f1799 () Arctic (+ (* f14 f1792) (* f15 f1793))) (define-fun f1800 () Arctic (+ f16 f1798)) (define-fun f1801 () Arctic (+ f17 f1799)) (define-fun f1802 () Arctic (+ (* f6 f1794) (* f7 f1796))) (define-fun f1803 () Arctic (+ (* f6 f1795) (* f7 f1797))) (define-fun f1804 () Arctic (+ (* f8 f1794) (* f9 f1796))) (define-fun f1805 () Arctic (+ (* f8 f1795) (* f9 f1797))) (define-fun f1806 () Arctic (+ (* f6 f1800) (* f7 f1801))) (define-fun f1807 () Arctic (+ (* f8 f1800) (* f9 f1801))) (define-fun f1808 () Arctic (+ f10 f1806)) (define-fun f1809 () Arctic (+ f11 f1807)) (define-fun f1810 () Arctic (+ (* f6 f1802) (* f7 f1804))) (define-fun f1811 () Arctic (+ (* f6 f1803) (* f7 f1805))) (define-fun f1812 () Arctic (+ (* f8 f1802) (* f9 f1804))) (define-fun f1813 () Arctic (+ (* f8 f1803) (* f9 f1805))) (define-fun f1814 () Arctic (+ (* f6 f1808) (* f7 f1809))) (define-fun f1815 () Arctic (+ (* f8 f1808) (* f9 f1809))) (define-fun f1816 () Arctic (+ f10 f1814)) (define-fun f1817 () Arctic (+ f11 f1815)) (define-fun f1818 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1819 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1820 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1821 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1822 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1823 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1824 () Arctic (+ f16 f1822)) (define-fun f1825 () Arctic (+ f17 f1823)) (define-fun f1826 () Arctic (+ (* f6 f1818) (* f7 f1820))) (define-fun f1827 () Arctic (+ (* f6 f1819) (* f7 f1821))) (define-fun f1828 () Arctic (+ (* f8 f1818) (* f9 f1820))) (define-fun f1829 () Arctic (+ (* f8 f1819) (* f9 f1821))) (define-fun f1830 () Arctic (+ (* f6 f1824) (* f7 f1825))) (define-fun f1831 () Arctic (+ (* f8 f1824) (* f9 f1825))) (define-fun f1832 () Arctic (+ f10 f1830)) (define-fun f1833 () Arctic (+ f11 f1831)) (define-fun f1834 () Arctic (+ (* f6 f1826) (* f7 f1828))) (define-fun f1835 () Arctic (+ (* f6 f1827) (* f7 f1829))) (define-fun f1836 () Arctic (+ (* f8 f1826) (* f9 f1828))) (define-fun f1837 () Arctic (+ (* f8 f1827) (* f9 f1829))) (define-fun f1838 () Arctic (+ (* f6 f1832) (* f7 f1833))) (define-fun f1839 () Arctic (+ (* f8 f1832) (* f9 f1833))) (define-fun f1840 () Arctic (+ f10 f1838)) (define-fun f1841 () Arctic (+ f11 f1839)) (define-fun f1842 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f1843 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f1844 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f1845 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f1846 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f1847 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f1848 () Arctic (+ f10 f1846)) (define-fun f1849 () Arctic (+ f11 f1847)) (define-fun f1850 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1851 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1852 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1853 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1854 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1855 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1856 () Arctic (+ f16 f1854)) (define-fun f1857 () Arctic (+ f17 f1855)) (define-fun f1858 () Arctic (+ (* f6 f1850) (* f7 f1852))) (define-fun f1859 () Arctic (+ (* f6 f1851) (* f7 f1853))) (define-fun f1860 () Arctic (+ (* f8 f1850) (* f9 f1852))) (define-fun f1861 () Arctic (+ (* f8 f1851) (* f9 f1853))) (define-fun f1862 () Arctic (+ (* f6 f1856) (* f7 f1857))) (define-fun f1863 () Arctic (+ (* f8 f1856) (* f9 f1857))) (define-fun f1864 () Arctic (+ f10 f1862)) (define-fun f1865 () Arctic (+ f11 f1863)) (define-fun f1866 () Arctic (+ (* f12 f1858) (* f13 f1860))) (define-fun f1867 () Arctic (+ (* f12 f1859) (* f13 f1861))) (define-fun f1868 () Arctic (+ (* f14 f1858) (* f15 f1860))) (define-fun f1869 () Arctic (+ (* f14 f1859) (* f15 f1861))) (define-fun f1870 () Arctic (+ (* f12 f1864) (* f13 f1865))) (define-fun f1871 () Arctic (+ (* f14 f1864) (* f15 f1865))) (define-fun f1872 () Arctic (+ f16 f1870)) (define-fun f1873 () Arctic (+ f17 f1871)) (define-fun f1874 () Arctic (+ (* f12 f1866) (* f13 f1868))) (define-fun f1875 () Arctic (+ (* f12 f1867) (* f13 f1869))) (define-fun f1876 () Arctic (+ (* f14 f1866) (* f15 f1868))) (define-fun f1877 () Arctic (+ (* f14 f1867) (* f15 f1869))) (define-fun f1878 () Arctic (+ (* f12 f1872) (* f13 f1873))) (define-fun f1879 () Arctic (+ (* f14 f1872) (* f15 f1873))) (define-fun f1880 () Arctic (+ f16 f1878)) (define-fun f1881 () Arctic (+ f17 f1879)) (define-fun f1882 () Arctic (+ (* f12 f1874) (* f13 f1876))) (define-fun f1883 () Arctic (+ (* f12 f1875) (* f13 f1877))) (define-fun f1884 () Arctic (+ (* f14 f1874) (* f15 f1876))) (define-fun f1885 () Arctic (+ (* f14 f1875) (* f15 f1877))) (define-fun f1886 () Arctic (+ (* f12 f1880) (* f13 f1881))) (define-fun f1887 () Arctic (+ (* f14 f1880) (* f15 f1881))) (define-fun f1888 () Arctic (+ f16 f1886)) (define-fun f1889 () Arctic (+ f17 f1887)) (define-fun f1890 () Arctic (+ (* f12 f1882) (* f13 f1884))) (define-fun f1891 () Arctic (+ (* f12 f1883) (* f13 f1885))) (define-fun f1892 () Arctic (+ (* f14 f1882) (* f15 f1884))) (define-fun f1893 () Arctic (+ (* f14 f1883) (* f15 f1885))) (define-fun f1894 () Arctic (+ (* f12 f1888) (* f13 f1889))) (define-fun f1895 () Arctic (+ (* f14 f1888) (* f15 f1889))) (define-fun f1896 () Arctic (+ f16 f1894)) (define-fun f1897 () Arctic (+ f17 f1895)) (define-fun f1898 () Arctic (+ (* f6 f1890) (* f7 f1892))) (define-fun f1899 () Arctic (+ (* f6 f1891) (* f7 f1893))) (define-fun f1900 () Arctic (+ (* f8 f1890) (* f9 f1892))) (define-fun f1901 () Arctic (+ (* f8 f1891) (* f9 f1893))) (define-fun f1902 () Arctic (+ (* f6 f1896) (* f7 f1897))) (define-fun f1903 () Arctic (+ (* f8 f1896) (* f9 f1897))) (define-fun f1904 () Arctic (+ f10 f1902)) (define-fun f1905 () Arctic (+ f11 f1903)) (define-fun f1906 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1907 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1908 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1909 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1910 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1911 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1912 () Arctic (+ f16 f1910)) (define-fun f1913 () Arctic (+ f17 f1911)) (define-fun f1914 () Arctic (+ (* f12 f1906) (* f13 f1908))) (define-fun f1915 () Arctic (+ (* f12 f1907) (* f13 f1909))) (define-fun f1916 () Arctic (+ (* f14 f1906) (* f15 f1908))) (define-fun f1917 () Arctic (+ (* f14 f1907) (* f15 f1909))) (define-fun f1918 () Arctic (+ (* f12 f1912) (* f13 f1913))) (define-fun f1919 () Arctic (+ (* f14 f1912) (* f15 f1913))) (define-fun f1920 () Arctic (+ f16 f1918)) (define-fun f1921 () Arctic (+ f17 f1919)) (define-fun f1922 () Arctic (+ (* f12 f1914) (* f13 f1916))) (define-fun f1923 () Arctic (+ (* f12 f1915) (* f13 f1917))) (define-fun f1924 () Arctic (+ (* f14 f1914) (* f15 f1916))) (define-fun f1925 () Arctic (+ (* f14 f1915) (* f15 f1917))) (define-fun f1926 () Arctic (+ (* f12 f1920) (* f13 f1921))) (define-fun f1927 () Arctic (+ (* f14 f1920) (* f15 f1921))) (define-fun f1928 () Arctic (+ f16 f1926)) (define-fun f1929 () Arctic (+ f17 f1927)) (define-fun f1930 () Arctic (+ (* f12 f1922) (* f13 f1924))) (define-fun f1931 () Arctic (+ (* f12 f1923) (* f13 f1925))) (define-fun f1932 () Arctic (+ (* f14 f1922) (* f15 f1924))) (define-fun f1933 () Arctic (+ (* f14 f1923) (* f15 f1925))) (define-fun f1934 () Arctic (+ (* f12 f1928) (* f13 f1929))) (define-fun f1935 () Arctic (+ (* f14 f1928) (* f15 f1929))) (define-fun f1936 () Arctic (+ f16 f1934)) (define-fun f1937 () Arctic (+ f17 f1935)) (define-fun f1938 () Arctic (+ (* f6 f1930) (* f7 f1932))) (define-fun f1939 () Arctic (+ (* f6 f1931) (* f7 f1933))) (define-fun f1940 () Arctic (+ (* f8 f1930) (* f9 f1932))) (define-fun f1941 () Arctic (+ (* f8 f1931) (* f9 f1933))) (define-fun f1942 () Arctic (+ (* f6 f1936) (* f7 f1937))) (define-fun f1943 () Arctic (+ (* f8 f1936) (* f9 f1937))) (define-fun f1944 () Arctic (+ f10 f1942)) (define-fun f1945 () Arctic (+ f11 f1943)) (define-fun f1946 () Arctic (+ (* f12 f1938) (* f13 f1940))) (define-fun f1947 () Arctic (+ (* f12 f1939) (* f13 f1941))) (define-fun f1948 () Arctic (+ (* f14 f1938) (* f15 f1940))) (define-fun f1949 () Arctic (+ (* f14 f1939) (* f15 f1941))) (define-fun f1950 () Arctic (+ (* f12 f1944) (* f13 f1945))) (define-fun f1951 () Arctic (+ (* f14 f1944) (* f15 f1945))) (define-fun f1952 () Arctic (+ f16 f1950)) (define-fun f1953 () Arctic (+ f17 f1951)) (define-fun f1954 () Arctic (+ (* f12 f1946) (* f13 f1948))) (define-fun f1955 () Arctic (+ (* f12 f1947) (* f13 f1949))) (define-fun f1956 () Arctic (+ (* f14 f1946) (* f15 f1948))) (define-fun f1957 () Arctic (+ (* f14 f1947) (* f15 f1949))) (define-fun f1958 () Arctic (+ (* f12 f1952) (* f13 f1953))) (define-fun f1959 () Arctic (+ (* f14 f1952) (* f15 f1953))) (define-fun f1960 () Arctic (+ f16 f1958)) (define-fun f1961 () Arctic (+ f17 f1959)) (define-fun f1962 () Arctic (+ (* f12 f1954) (* f13 f1956))) (define-fun f1963 () Arctic (+ (* f12 f1955) (* f13 f1957))) (define-fun f1964 () Arctic (+ (* f14 f1954) (* f15 f1956))) (define-fun f1965 () Arctic (+ (* f14 f1955) (* f15 f1957))) (define-fun f1966 () Arctic (+ (* f12 f1960) (* f13 f1961))) (define-fun f1967 () Arctic (+ (* f14 f1960) (* f15 f1961))) (define-fun f1968 () Arctic (+ f16 f1966)) (define-fun f1969 () Arctic (+ f17 f1967)) (define-fun f1970 () Arctic (+ (* f12 f1962) (* f13 f1964))) (define-fun f1971 () Arctic (+ (* f12 f1963) (* f13 f1965))) (define-fun f1972 () Arctic (+ (* f14 f1962) (* f15 f1964))) (define-fun f1973 () Arctic (+ (* f14 f1963) (* f15 f1965))) (define-fun f1974 () Arctic (+ (* f12 f1968) (* f13 f1969))) (define-fun f1975 () Arctic (+ (* f14 f1968) (* f15 f1969))) (define-fun f1976 () Arctic (+ f16 f1974)) (define-fun f1977 () Arctic (+ f17 f1975)) (define-fun f1978 () Arctic (+ (* f6 f1970) (* f7 f1972))) (define-fun f1979 () Arctic (+ (* f6 f1971) (* f7 f1973))) (define-fun f1980 () Arctic (+ (* f8 f1970) (* f9 f1972))) (define-fun f1981 () Arctic (+ (* f8 f1971) (* f9 f1973))) (define-fun f1982 () Arctic (+ (* f6 f1976) (* f7 f1977))) (define-fun f1983 () Arctic (+ (* f8 f1976) (* f9 f1977))) (define-fun f1984 () Arctic (+ f10 f1982)) (define-fun f1985 () Arctic (+ f11 f1983)) (define-fun f1986 () Arctic (+ (* f12 f1978) (* f13 f1980))) (define-fun f1987 () Arctic (+ (* f12 f1979) (* f13 f1981))) (define-fun f1988 () Arctic (+ (* f14 f1978) (* f15 f1980))) (define-fun f1989 () Arctic (+ (* f14 f1979) (* f15 f1981))) (define-fun f1990 () Arctic (+ (* f12 f1984) (* f13 f1985))) (define-fun f1991 () Arctic (+ (* f14 f1984) (* f15 f1985))) (define-fun f1992 () Arctic (+ f16 f1990)) (define-fun f1993 () Arctic (+ f17 f1991)) (define-fun f1994 () Arctic (+ (* f6 f1986) (* f7 f1988))) (define-fun f1995 () Arctic (+ (* f6 f1987) (* f7 f1989))) (define-fun f1996 () Arctic (+ (* f8 f1986) (* f9 f1988))) (define-fun f1997 () Arctic (+ (* f8 f1987) (* f9 f1989))) (define-fun f1998 () Arctic (+ (* f6 f1992) (* f7 f1993))) (define-fun f1999 () Arctic (+ (* f8 f1992) (* f9 f1993))) (define-fun f2000 () Arctic (+ f10 f1998)) (define-fun f2001 () Arctic (+ f11 f1999)) (define-fun f2002 () Arctic (+ (* f12 f1994) (* f13 f1996))) (define-fun f2003 () Arctic (+ (* f12 f1995) (* f13 f1997))) (define-fun f2004 () Arctic (+ (* f14 f1994) (* f15 f1996))) (define-fun f2005 () Arctic (+ (* f14 f1995) (* f15 f1997))) (define-fun f2006 () Arctic (+ (* f12 f2000) (* f13 f2001))) (define-fun f2007 () Arctic (+ (* f14 f2000) (* f15 f2001))) (define-fun f2008 () Arctic (+ f16 f2006)) (define-fun f2009 () Arctic (+ f17 f2007)) (define-fun f2010 () Arctic (+ (* f12 f2002) (* f13 f2004))) (define-fun f2011 () Arctic (+ (* f12 f2003) (* f13 f2005))) (define-fun f2012 () Arctic (+ (* f14 f2002) (* f15 f2004))) (define-fun f2013 () Arctic (+ (* f14 f2003) (* f15 f2005))) (define-fun f2014 () Arctic (+ (* f12 f2008) (* f13 f2009))) (define-fun f2015 () Arctic (+ (* f14 f2008) (* f15 f2009))) (define-fun f2016 () Arctic (+ f16 f2014)) (define-fun f2017 () Arctic (+ f17 f2015)) (define-fun f2018 () Arctic (+ (* f12 f2010) (* f13 f2012))) (define-fun f2019 () Arctic (+ (* f12 f2011) (* f13 f2013))) (define-fun f2020 () Arctic (+ (* f14 f2010) (* f15 f2012))) (define-fun f2021 () Arctic (+ (* f14 f2011) (* f15 f2013))) (define-fun f2022 () Arctic (+ (* f12 f2016) (* f13 f2017))) (define-fun f2023 () Arctic (+ (* f14 f2016) (* f15 f2017))) (define-fun f2024 () Arctic (+ f16 f2022)) (define-fun f2025 () Arctic (+ f17 f2023)) (define-fun f2026 () Arctic (+ (* f6 f2018) (* f7 f2020))) (define-fun f2027 () Arctic (+ (* f6 f2019) (* f7 f2021))) (define-fun f2028 () Arctic (+ (* f8 f2018) (* f9 f2020))) (define-fun f2029 () Arctic (+ (* f8 f2019) (* f9 f2021))) (define-fun f2030 () Arctic (+ (* f6 f2024) (* f7 f2025))) (define-fun f2031 () Arctic (+ (* f8 f2024) (* f9 f2025))) (define-fun f2032 () Arctic (+ f10 f2030)) (define-fun f2033 () Arctic (+ f11 f2031)) (define-fun f2034 () Arctic (+ (* f12 f2026) (* f13 f2028))) (define-fun f2035 () Arctic (+ (* f12 f2027) (* f13 f2029))) (define-fun f2036 () Arctic (+ (* f14 f2026) (* f15 f2028))) (define-fun f2037 () Arctic (+ (* f14 f2027) (* f15 f2029))) (define-fun f2038 () Arctic (+ (* f12 f2032) (* f13 f2033))) (define-fun f2039 () Arctic (+ (* f14 f2032) (* f15 f2033))) (define-fun f2040 () Arctic (+ f16 f2038)) (define-fun f2041 () Arctic (+ f17 f2039)) (define-fun f2042 () Arctic (+ (* f12 f2034) (* f13 f2036))) (define-fun f2043 () Arctic (+ (* f12 f2035) (* f13 f2037))) (define-fun f2044 () Arctic (+ (* f14 f2034) (* f15 f2036))) (define-fun f2045 () Arctic (+ (* f14 f2035) (* f15 f2037))) (define-fun f2046 () Arctic (+ (* f12 f2040) (* f13 f2041))) (define-fun f2047 () Arctic (+ (* f14 f2040) (* f15 f2041))) (define-fun f2048 () Arctic (+ f16 f2046)) (define-fun f2049 () Arctic (+ f17 f2047)) (define-fun f2050 () Arctic (+ (* f12 f2042) (* f13 f2044))) (define-fun f2051 () Arctic (+ (* f12 f2043) (* f13 f2045))) (define-fun f2052 () Arctic (+ (* f14 f2042) (* f15 f2044))) (define-fun f2053 () Arctic (+ (* f14 f2043) (* f15 f2045))) (define-fun f2054 () Arctic (+ (* f12 f2048) (* f13 f2049))) (define-fun f2055 () Arctic (+ (* f14 f2048) (* f15 f2049))) (define-fun f2056 () Arctic (+ f16 f2054)) (define-fun f2057 () Arctic (+ f17 f2055)) (define-fun f2058 () Arctic (+ (* f12 f2050) (* f13 f2052))) (define-fun f2059 () Arctic (+ (* f12 f2051) (* f13 f2053))) (define-fun f2060 () Arctic (+ (* f14 f2050) (* f15 f2052))) (define-fun f2061 () Arctic (+ (* f14 f2051) (* f15 f2053))) (define-fun f2062 () Arctic (+ (* f12 f2056) (* f13 f2057))) (define-fun f2063 () Arctic (+ (* f14 f2056) (* f15 f2057))) (define-fun f2064 () Arctic (+ f16 f2062)) (define-fun f2065 () Arctic (+ f17 f2063)) (define-fun f2066 () Arctic (+ (* f6 f2058) (* f7 f2060))) (define-fun f2067 () Arctic (+ (* f6 f2059) (* f7 f2061))) (define-fun f2068 () Arctic (+ (* f8 f2058) (* f9 f2060))) (define-fun f2069 () Arctic (+ (* f8 f2059) (* f9 f2061))) (define-fun f2070 () Arctic (+ (* f6 f2064) (* f7 f2065))) (define-fun f2071 () Arctic (+ (* f8 f2064) (* f9 f2065))) (define-fun f2072 () Arctic (+ f10 f2070)) (define-fun f2073 () Arctic (+ f11 f2071)) (define-fun f2074 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f2075 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f2076 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f2077 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f2078 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f2079 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f2080 () Arctic (+ f16 f2078)) (define-fun f2081 () Arctic (+ f17 f2079)) (define-fun f2082 () Arctic (+ (* f12 f2074) (* f13 f2076))) (define-fun f2083 () Arctic (+ (* f12 f2075) (* f13 f2077))) (define-fun f2084 () Arctic (+ (* f14 f2074) (* f15 f2076))) (define-fun f2085 () Arctic (+ (* f14 f2075) (* f15 f2077))) (define-fun f2086 () Arctic (+ (* f12 f2080) (* f13 f2081))) (define-fun f2087 () Arctic (+ (* f14 f2080) (* f15 f2081))) (define-fun f2088 () Arctic (+ f16 f2086)) (define-fun f2089 () Arctic (+ f17 f2087)) (define-fun f2090 () Arctic (+ (* f6 f2082) (* f7 f2084))) (define-fun f2091 () Arctic (+ (* f6 f2083) (* f7 f2085))) (define-fun f2092 () Arctic (+ (* f8 f2082) (* f9 f2084))) (define-fun f2093 () Arctic (+ (* f8 f2083) (* f9 f2085))) (define-fun f2094 () Arctic (+ (* f6 f2088) (* f7 f2089))) (define-fun f2095 () Arctic (+ (* f8 f2088) (* f9 f2089))) (define-fun f2096 () Arctic (+ f10 f2094)) (define-fun f2097 () Arctic (+ f11 f2095)) (define-fun f2098 () Arctic (+ (* f12 f2090) (* f13 f2092))) (define-fun f2099 () Arctic (+ (* f12 f2091) (* f13 f2093))) (define-fun f2100 () Arctic (+ (* f14 f2090) (* f15 f2092))) (define-fun f2101 () Arctic (+ (* f14 f2091) (* f15 f2093))) (define-fun f2102 () Arctic (+ (* f12 f2096) (* f13 f2097))) (define-fun f2103 () Arctic (+ (* f14 f2096) (* f15 f2097))) (define-fun f2104 () Arctic (+ f16 f2102)) (define-fun f2105 () Arctic (+ f17 f2103)) (define-fun f2106 () Arctic (+ (* f12 f2098) (* f13 f2100))) (define-fun f2107 () Arctic (+ (* f12 f2099) (* f13 f2101))) (define-fun f2108 () Arctic (+ (* f14 f2098) (* f15 f2100))) (define-fun f2109 () Arctic (+ (* f14 f2099) (* f15 f2101))) (define-fun f2110 () Arctic (+ (* f12 f2104) (* f13 f2105))) (define-fun f2111 () Arctic (+ (* f14 f2104) (* f15 f2105))) (define-fun f2112 () Arctic (+ f16 f2110)) (define-fun f2113 () Arctic (+ f17 f2111)) (define-fun f2114 () Arctic (+ (* f12 f2106) (* f13 f2108))) (define-fun f2115 () Arctic (+ (* f12 f2107) (* f13 f2109))) (define-fun f2116 () Arctic (+ (* f14 f2106) (* f15 f2108))) (define-fun f2117 () Arctic (+ (* f14 f2107) (* f15 f2109))) (define-fun f2118 () Arctic (+ (* f12 f2112) (* f13 f2113))) (define-fun f2119 () Arctic (+ (* f14 f2112) (* f15 f2113))) (define-fun f2120 () Arctic (+ f16 f2118)) (define-fun f2121 () Arctic (+ f17 f2119)) (define-fun f2122 () Arctic (+ (* f12 f2114) (* f13 f2116))) (define-fun f2123 () Arctic (+ (* f12 f2115) (* f13 f2117))) (define-fun f2124 () Arctic (+ (* f14 f2114) (* f15 f2116))) (define-fun f2125 () Arctic (+ (* f14 f2115) (* f15 f2117))) (define-fun f2126 () Arctic (+ (* f12 f2120) (* f13 f2121))) (define-fun f2127 () Arctic (+ (* f14 f2120) (* f15 f2121))) (define-fun f2128 () Arctic (+ f16 f2126)) (define-fun f2129 () Arctic (+ f17 f2127)) (define-fun f2130 () Arctic (+ (* f6 f2122) (* f7 f2124))) (define-fun f2131 () Arctic (+ (* f6 f2123) (* f7 f2125))) (define-fun f2132 () Arctic (+ (* f8 f2122) (* f9 f2124))) (define-fun f2133 () Arctic (+ (* f8 f2123) (* f9 f2125))) (define-fun f2134 () Arctic (+ (* f6 f2128) (* f7 f2129))) (define-fun f2135 () Arctic (+ (* f8 f2128) (* f9 f2129))) (define-fun f2136 () Arctic (+ f10 f2134)) (define-fun f2137 () Arctic (+ f11 f2135)) (define-fun f2138 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f2139 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f2140 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f2141 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f2142 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f2143 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f2144 () Arctic (+ f16 f2142)) (define-fun f2145 () Arctic (+ f17 f2143)) (define-fun f2146 () Arctic (+ (* f6 f2138) (* f7 f2140))) (define-fun f2147 () Arctic (+ (* f6 f2139) (* f7 f2141))) (define-fun f2148 () Arctic (+ (* f8 f2138) (* f9 f2140))) (define-fun f2149 () Arctic (+ (* f8 f2139) (* f9 f2141))) (define-fun f2150 () Arctic (+ (* f6 f2144) (* f7 f2145))) (define-fun f2151 () Arctic (+ (* f8 f2144) (* f9 f2145))) (define-fun f2152 () Arctic (+ f10 f2150)) (define-fun f2153 () Arctic (+ f11 f2151)) (define-fun f2154 () Arctic (+ (* f12 f2146) (* f13 f2148))) (define-fun f2155 () Arctic (+ (* f12 f2147) (* f13 f2149))) (define-fun f2156 () Arctic (+ (* f14 f2146) (* f15 f2148))) (define-fun f2157 () Arctic (+ (* f14 f2147) (* f15 f2149))) (define-fun f2158 () Arctic (+ (* f12 f2152) (* f13 f2153))) (define-fun f2159 () Arctic (+ (* f14 f2152) (* f15 f2153))) (define-fun f2160 () Arctic (+ f16 f2158)) (define-fun f2161 () Arctic (+ f17 f2159)) (define-fun f2162 () Arctic (+ (* f12 f2154) (* f13 f2156))) (define-fun f2163 () Arctic (+ (* f12 f2155) (* f13 f2157))) (define-fun f2164 () Arctic (+ (* f14 f2154) (* f15 f2156))) (define-fun f2165 () Arctic (+ (* f14 f2155) (* f15 f2157))) (define-fun f2166 () Arctic (+ (* f12 f2160) (* f13 f2161))) (define-fun f2167 () Arctic (+ (* f14 f2160) (* f15 f2161))) (define-fun f2168 () Arctic (+ f16 f2166)) (define-fun f2169 () Arctic (+ f17 f2167)) (define-fun f2170 () Arctic (+ (* f6 f2162) (* f7 f2164))) (define-fun f2171 () Arctic (+ (* f6 f2163) (* f7 f2165))) (define-fun f2172 () Arctic (+ (* f8 f2162) (* f9 f2164))) (define-fun f2173 () Arctic (+ (* f8 f2163) (* f9 f2165))) (define-fun f2174 () Arctic (+ (* f6 f2168) (* f7 f2169))) (define-fun f2175 () Arctic (+ (* f8 f2168) (* f9 f2169))) (define-fun f2176 () Arctic (+ f10 f2174)) (define-fun f2177 () Arctic (+ f11 f2175)) (define-fun f2178 () Arctic (+ (* f12 f2170) (* f13 f2172))) (define-fun f2179 () Arctic (+ (* f12 f2171) (* f13 f2173))) (define-fun f2180 () Arctic (+ (* f14 f2170) (* f15 f2172))) (define-fun f2181 () Arctic (+ (* f14 f2171) (* f15 f2173))) (define-fun f2182 () Arctic (+ (* f12 f2176) (* f13 f2177))) (define-fun f2183 () Arctic (+ (* f14 f2176) (* f15 f2177))) (define-fun f2184 () Arctic (+ f16 f2182)) (define-fun f2185 () Arctic (+ f17 f2183)) (define-fun f2186 () Arctic (+ (* f12 f2178) (* f13 f2180))) (define-fun f2187 () Arctic (+ (* f12 f2179) (* f13 f2181))) (define-fun f2188 () Arctic (+ (* f14 f2178) (* f15 f2180))) (define-fun f2189 () Arctic (+ (* f14 f2179) (* f15 f2181))) (define-fun f2190 () Arctic (+ (* f12 f2184) (* f13 f2185))) (define-fun f2191 () Arctic (+ (* f14 f2184) (* f15 f2185))) (define-fun f2192 () Arctic (+ f16 f2190)) (define-fun f2193 () Arctic (+ f17 f2191)) (define-fun f2194 () Arctic (+ (* f12 f2186) (* f13 f2188))) (define-fun f2195 () Arctic (+ (* f12 f2187) (* f13 f2189))) (define-fun f2196 () Arctic (+ (* f14 f2186) (* f15 f2188))) (define-fun f2197 () Arctic (+ (* f14 f2187) (* f15 f2189))) (define-fun f2198 () Arctic (+ (* f12 f2192) (* f13 f2193))) (define-fun f2199 () Arctic (+ (* f14 f2192) (* f15 f2193))) (define-fun f2200 () Arctic (+ f16 f2198)) (define-fun f2201 () Arctic (+ f17 f2199)) (define-fun f2202 () Arctic (+ (* f6 f2194) (* f7 f2196))) (define-fun f2203 () Arctic (+ (* f6 f2195) (* f7 f2197))) (define-fun f2204 () Arctic (+ (* f8 f2194) (* f9 f2196))) (define-fun f2205 () Arctic (+ (* f8 f2195) (* f9 f2197))) (define-fun f2206 () Arctic (+ (* f6 f2200) (* f7 f2201))) (define-fun f2207 () Arctic (+ (* f8 f2200) (* f9 f2201))) (define-fun f2208 () Arctic (+ f10 f2206)) (define-fun f2209 () Arctic (+ f11 f2207)) (define-fun f2210 () Arctic (+ (* f12 f2202) (* f13 f2204))) (define-fun f2211 () Arctic (+ (* f12 f2203) (* f13 f2205))) (define-fun f2212 () Arctic (+ (* f14 f2202) (* f15 f2204))) (define-fun f2213 () Arctic (+ (* f14 f2203) (* f15 f2205))) (define-fun f2214 () Arctic (+ (* f12 f2208) (* f13 f2209))) (define-fun f2215 () Arctic (+ (* f14 f2208) (* f15 f2209))) (define-fun f2216 () Arctic (+ f16 f2214)) (define-fun f2217 () Arctic (+ f17 f2215)) (define-fun f2218 () Arctic (+ (* f12 f2210) (* f13 f2212))) (define-fun f2219 () Arctic (+ (* f12 f2211) (* f13 f2213))) (define-fun f2220 () Arctic (+ (* f14 f2210) (* f15 f2212))) (define-fun f2221 () Arctic (+ (* f14 f2211) (* f15 f2213))) (define-fun f2222 () Arctic (+ (* f12 f2216) (* f13 f2217))) (define-fun f2223 () Arctic (+ (* f14 f2216) (* f15 f2217))) (define-fun f2224 () Arctic (+ f16 f2222)) (define-fun f2225 () Arctic (+ f17 f2223)) (define-fun f2226 () Arctic (+ (* f12 f2218) (* f13 f2220))) (define-fun f2227 () Arctic (+ (* f12 f2219) (* f13 f2221))) (define-fun f2228 () Arctic (+ (* f14 f2218) (* f15 f2220))) (define-fun f2229 () Arctic (+ (* f14 f2219) (* f15 f2221))) (define-fun f2230 () Arctic (+ (* f12 f2224) (* f13 f2225))) (define-fun f2231 () Arctic (+ (* f14 f2224) (* f15 f2225))) (define-fun f2232 () Arctic (+ f16 f2230)) (define-fun f2233 () Arctic (+ f17 f2231)) (define-fun f2234 () Arctic (+ (* f12 f2226) (* f13 f2228))) (define-fun f2235 () Arctic (+ (* f12 f2227) (* f13 f2229))) (define-fun f2236 () Arctic (+ (* f14 f2226) (* f15 f2228))) (define-fun f2237 () Arctic (+ (* f14 f2227) (* f15 f2229))) (define-fun f2238 () Arctic (+ (* f12 f2232) (* f13 f2233))) (define-fun f2239 () Arctic (+ (* f14 f2232) (* f15 f2233))) (define-fun f2240 () Arctic (+ f16 f2238)) (define-fun f2241 () Arctic (+ f17 f2239)) (define-fun f2242 () Arctic (+ (* f6 f2234) (* f7 f2236))) (define-fun f2243 () Arctic (+ (* f6 f2235) (* f7 f2237))) (define-fun f2244 () Arctic (+ (* f8 f2234) (* f9 f2236))) (define-fun f2245 () Arctic (+ (* f8 f2235) (* f9 f2237))) (define-fun f2246 () Arctic (+ (* f6 f2240) (* f7 f2241))) (define-fun f2247 () Arctic (+ (* f8 f2240) (* f9 f2241))) (define-fun f2248 () Arctic (+ f10 f2246)) (define-fun f2249 () Arctic (+ f11 f2247)) (define-fun f2250 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f2251 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f2252 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f2253 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f2254 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f2255 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f2256 () Arctic (+ f16 f2254)) (define-fun f2257 () Arctic (+ f17 f2255)) (define-fun f2258 () Arctic (+ (* f12 f2250) (* f13 f2252))) (define-fun f2259 () Arctic (+ (* f12 f2251) (* f13 f2253))) (define-fun f2260 () Arctic (+ (* f14 f2250) (* f15 f2252))) (define-fun f2261 () Arctic (+ (* f14 f2251) (* f15 f2253))) (define-fun f2262 () Arctic (+ (* f12 f2256) (* f13 f2257))) (define-fun f2263 () Arctic (+ (* f14 f2256) (* f15 f2257))) (define-fun f2264 () Arctic (+ f16 f2262)) (define-fun f2265 () Arctic (+ f17 f2263)) (define-fun f2266 () Arctic (+ (* f12 f2258) (* f13 f2260))) (define-fun f2267 () Arctic (+ (* f12 f2259) (* f13 f2261))) (define-fun f2268 () Arctic (+ (* f14 f2258) (* f15 f2260))) (define-fun f2269 () Arctic (+ (* f14 f2259) (* f15 f2261))) (define-fun f2270 () Arctic (+ (* f12 f2264) (* f13 f2265))) (define-fun f2271 () Arctic (+ (* f14 f2264) (* f15 f2265))) (define-fun f2272 () Arctic (+ f16 f2270)) (define-fun f2273 () Arctic (+ f17 f2271)) (define-fun f2274 () Arctic (+ (* f6 f2266) (* f7 f2268))) (define-fun f2275 () Arctic (+ (* f6 f2267) (* f7 f2269))) (define-fun f2276 () Arctic (+ (* f8 f2266) (* f9 f2268))) (define-fun f2277 () Arctic (+ (* f8 f2267) (* f9 f2269))) (define-fun f2278 () Arctic (+ (* f6 f2272) (* f7 f2273))) (define-fun f2279 () Arctic (+ (* f8 f2272) (* f9 f2273))) (define-fun f2280 () Arctic (+ f10 f2278)) (define-fun f2281 () Arctic (+ f11 f2279)) (define-fun f2282 () Arctic (+ (* f12 f2274) (* f13 f2276))) (define-fun f2283 () Arctic (+ (* f12 f2275) (* f13 f2277))) (define-fun f2284 () Arctic (+ (* f14 f2274) (* f15 f2276))) (define-fun f2285 () Arctic (+ (* f14 f2275) (* f15 f2277))) (define-fun f2286 () Arctic (+ (* f12 f2280) (* f13 f2281))) (define-fun f2287 () Arctic (+ (* f14 f2280) (* f15 f2281))) (define-fun f2288 () Arctic (+ f16 f2286)) (define-fun f2289 () Arctic (+ f17 f2287)) (define-fun f2290 () Arctic (+ (* f12 f2282) (* f13 f2284))) (define-fun f2291 () Arctic (+ (* f12 f2283) (* f13 f2285))) (define-fun f2292 () Arctic (+ (* f14 f2282) (* f15 f2284))) (define-fun f2293 () Arctic (+ (* f14 f2283) (* f15 f2285))) (define-fun f2294 () Arctic (+ (* f12 f2288) (* f13 f2289))) (define-fun f2295 () Arctic (+ (* f14 f2288) (* f15 f2289))) (define-fun f2296 () Arctic (+ f16 f2294)) (define-fun f2297 () Arctic (+ f17 f2295)) (define-fun f2298 () Arctic (+ (* f12 f2290) (* f13 f2292))) (define-fun f2299 () Arctic (+ (* f12 f2291) (* f13 f2293))) (define-fun f2300 () Arctic (+ (* f14 f2290) (* f15 f2292))) (define-fun f2301 () Arctic (+ (* f14 f2291) (* f15 f2293))) (define-fun f2302 () Arctic (+ (* f12 f2296) (* f13 f2297))) (define-fun f2303 () Arctic (+ (* f14 f2296) (* f15 f2297))) (define-fun f2304 () Arctic (+ f16 f2302)) (define-fun f2305 () Arctic (+ f17 f2303)) (define-fun f2306 () Arctic (+ (* f12 f2298) (* f13 f2300))) (define-fun f2307 () Arctic (+ (* f12 f2299) (* f13 f2301))) (define-fun f2308 () Arctic (+ (* f14 f2298) (* f15 f2300))) (define-fun f2309 () Arctic (+ (* f14 f2299) (* f15 f2301))) (define-fun f2310 () Arctic (+ (* f12 f2304) (* f13 f2305))) (define-fun f2311 () Arctic (+ (* f14 f2304) (* f15 f2305))) (define-fun f2312 () Arctic (+ f16 f2310)) (define-fun f2313 () Arctic (+ f17 f2311)) (define-fun f2314 () Arctic (+ (* f6 f2306) (* f7 f2308))) (define-fun f2315 () Arctic (+ (* f6 f2307) (* f7 f2309))) (define-fun f2316 () Arctic (+ (* f8 f2306) (* f9 f2308))) (define-fun f2317 () Arctic (+ (* f8 f2307) (* f9 f2309))) (define-fun f2318 () Arctic (+ (* f6 f2312) (* f7 f2313))) (define-fun f2319 () Arctic (+ (* f8 f2312) (* f9 f2313))) (define-fun f2320 () Arctic (+ f10 f2318)) (define-fun f2321 () Arctic (+ f11 f2319)) (assert (and (and (and (and (>= f42 f90) (>= f43 f91)) (and (>= f44 f92) (>= f45 f93))) (and (and (>= f48 f96)) (and (>= f49 f97)))) (and (and (and (>= f122 f162) (>= f123 f163)) (and (>= f124 f164) (>= f125 f165))) (and (and (>= f128 f168)) (and (>= f129 f169)))) (and (and (and (>= f194 f0) (>= f195 f1)) (and (>= f196 f2) (>= f197 f3))) (and (and (>= f200 f4)) (and (>= f201 f5)))) (and (and (and (>= f218 f226) (>= f219 f227)) (and (>= f220 f228) (>= f221 f229))) (and (and (>= f224 f232)) (and (>= f225 f233)))) (and (and (and (>= f250 f0) (>= f251 f1)) (and (>= f252 f2) (>= f253 f3))) (and (and (>= f256 f4)) (and (>= f257 f5)))) (and (and (and (>= f306 f474) (>= f307 f475)) (and (>= f308 f476) (>= f309 f477))) (and (and (>= f312 f480)) (and (>= f313 f481)))) (and (and (and (>= f530 f658) (>= f531 f659)) (and (>= f532 f660) (>= f533 f661))) (and (and (>= f536 f664)) (and (>= f537 f665)))) (and (and (and (>= f714 f810) (>= f715 f811)) (and (>= f716 f812) (>= f717 f813))) (and (and (>= f720 f816)) (and (>= f721 f817)))) (and (and (and (>= f866 f946) (>= f867 f947)) (and (>= f868 f948) (>= f869 f949))) (and (and (>= f872 f952)) (and (>= f873 f953)))) (and (and (and (>= f1002 f1042) (>= f1003 f1043)) (and (>= f1004 f1044) (>= f1005 f1045))) (and (and (>= f1008 f1048)) (and (>= f1009 f1049)))) (and (and (and (>= f1098 f0) (>= f1099 f1)) (and (>= f1100 f2) (>= f1101 f3))) (and (and (>= f1104 f4)) (and (>= f1105 f5)))) (and (and (and (>= f1162 f1274) (>= f1163 f1275)) (and (>= f1164 f1276) (>= f1165 f1277))) (and (and (>= f1168 f1280)) (and (>= f1169 f1281)))) (and (and (and (>= f1338 f1410) (>= f1339 f1411)) (and (>= f1340 f1412) (>= f1341 f1413))) (and (and (>= f1344 f1416)) (and (>= f1345 f1417)))) (and (and (and (>= f1474 f1514) (>= f1475 f1515)) (and (>= f1476 f1516) (>= f1477 f1517))) (and (and (>= f1480 f1520)) (and (>= f1481 f1521)))) (and (and (and (>= f1578 f1594) (>= f1579 f1595)) (and (>= f1580 f1596) (>= f1581 f1597))) (and (and (>= f1584 f1600)) (and (>= f1585 f1601)))) (and (and (and (>= f1658 f0) (>= f1659 f1)) (and (>= f1660 f2) (>= f1661 f3))) (and (and (>= f1664 f4)) (and (>= f1665 f5)))) (and (and (and (>= f1730 f0) (>= f1731 f1)) (and (>= f1732 f2) (>= f1733 f3))) (and (and (>= f1736 f4)) (and (>= f1737 f5)))) (and (and (and (>= f1762 f1810) (>= f1763 f1811)) (and (>= f1764 f1812) (>= f1765 f1813))) (and (and (>= f1768 f1816)) (and (>= f1769 f1817)))) (and (and (and (>= f1834 f1842) (>= f1835 f1843)) (and (>= f1836 f1844) (>= f1837 f1845))) (and (and (>= f1840 f1848)) (and (>= f1841 f1849)))) (and (and (and (>= f1898 f2066) (>= f1899 f2067)) (and (>= f1900 f2068) (>= f1901 f2069))) (and (and (>= f1904 f2072)) (and (>= f1905 f2073)))) (and (and (and (>= f2130 f2242) (>= f2131 f2243)) (and (>= f2132 f2244) (>= f2133 f2245))) (and (and (>= f2136 f2248)) (and (>= f2137 f2249)))) (and (and (and (>= f2314 f6) (>= f2315 f7)) (and (>= f2316 f8) (>= f2317 f9))) (and (and (>= f2320 f10)) (and (>= f2321 f11)))))) (assert (or (and (and (and (>> f42 f90) (>> f43 f91)) (and (>> f44 f92) (>> f45 f93))) (and (and (>> f48 f96)) (and (>> f49 f97)))) (and (and (and (>> f122 f162) (>> f123 f163)) (and (>> f124 f164) (>> f125 f165))) (and (and (>> f128 f168)) (and (>> f129 f169)))) (and (and (and (>> f194 f0) (>> f195 f1)) (and (>> f196 f2) (>> f197 f3))) (and (and (>> f200 f4)) (and (>> f201 f5)))) (and (and (and (>> f218 f226) (>> f219 f227)) (and (>> f220 f228) (>> f221 f229))) (and (and (>> f224 f232)) (and (>> f225 f233)))) (and (and (and (>> f250 f0) (>> f251 f1)) (and (>> f252 f2) (>> f253 f3))) (and (and (>> f256 f4)) (and (>> f257 f5)))) (and (and (and (>> f306 f474) (>> f307 f475)) (and (>> f308 f476) (>> f309 f477))) (and (and (>> f312 f480)) (and (>> f313 f481)))) (and (and (and (>> f530 f658) (>> f531 f659)) (and (>> f532 f660) (>> f533 f661))) (and (and (>> f536 f664)) (and (>> f537 f665)))) (and (and (and (>> f714 f810) (>> f715 f811)) (and (>> f716 f812) (>> f717 f813))) (and (and (>> f720 f816)) (and (>> f721 f817)))) (and (and (and (>> f866 f946) (>> f867 f947)) (and (>> f868 f948) (>> f869 f949))) (and (and (>> f872 f952)) (and (>> f873 f953)))) (and (and (and (>> f1002 f1042) (>> f1003 f1043)) (and (>> f1004 f1044) (>> f1005 f1045))) (and (and (>> f1008 f1048)) (and (>> f1009 f1049)))) (and (and (and (>> f1098 f0) (>> f1099 f1)) (and (>> f1100 f2) (>> f1101 f3))) (and (and (>> f1104 f4)) (and (>> f1105 f5)))) (and (and (and (>> f1162 f1274) (>> f1163 f1275)) (and (>> f1164 f1276) (>> f1165 f1277))) (and (and (>> f1168 f1280)) (and (>> f1169 f1281)))) (and (and (and (>> f1338 f1410) (>> f1339 f1411)) (and (>> f1340 f1412) (>> f1341 f1413))) (and (and (>> f1344 f1416)) (and (>> f1345 f1417)))) (and (and (and (>> f1474 f1514) (>> f1475 f1515)) (and (>> f1476 f1516) (>> f1477 f1517))) (and (and (>> f1480 f1520)) (and (>> f1481 f1521)))) (and (and (and (>> f1578 f1594) (>> f1579 f1595)) (and (>> f1580 f1596) (>> f1581 f1597))) (and (and (>> f1584 f1600)) (and (>> f1585 f1601)))) (and (and (and (>> f1658 f0) (>> f1659 f1)) (and (>> f1660 f2) (>> f1661 f3))) (and (and (>> f1664 f4)) (and (>> f1665 f5)))) (and (and (and (>> f1730 f0) (>> f1731 f1)) (and (>> f1732 f2) (>> f1733 f3))) (and (and (>> f1736 f4)) (and (>> f1737 f5)))))) (check-sat) (get-value (f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 f10 f11 f12 f13 f14 f15 f16 f17 f18 f19 f20 f21 f22 f23 f24 f25 f26 f27 f28 f29 f30 f31 f32 f33 f34 f35 f36 f37 f38 f39 f40 f41 f42 f43 f44 f45 f46 f47 f48 f49 f50 f51 f52 f53 f54 f55 f56 f57 f58 f59 f60 f61 f62 f63 f64 f65 f66 f67 f68 f69 f70 f71 f72 f73 f74 f75 f76 f77 f78 f79 f80 f81 f82 f83 f84 f85 f86 f87 f88 f89 f90 f91 f92 f93 f94 f95 f96 f97 f98 f99 f100 f101 f102 f103 f104 f105 f106 f107 f108 f109 f110 f111 f112 f113 f114 f115 f116 f117 f118 f119 f120 f121 f122 f123 f124 f125 f126 f127 f128 f129 f130 f131 f132 f133 f134 f135 f136 f137 f138 f139 f140 f141 f142 f143 f144 f145 f146 f147 f148 f149 f150 f151 f152 f153 f154 f155 f156 f157 f158 f159 f160 f161 f162 f163 f164 f165 f166 f167 f168 f169 f170 f171 f172 f173 f174 f175 f176 f177 f178 f179 f180 f181 f182 f183 f184 f185 f186 f187 f188 f189 f190 f191 f192 f193 f194 f195 f196 f197 f198 f199 f200 f201 f202 f203 f204 f205 f206 f207 f208 f209 f210 f211 f212 f213 f214 f215 f216 f217 f218 f219 f220 f221 f222 f223 f224 f225 f226 f227 f228 f229 f230 f231 f232 f233 f234 f235 f236 f237 f238 f239 f240 f241 f242 f243 f244 f245 f246 f247 f248 f249 f250 f251 f252 f253 f254 f255 f256 f257 f258 f259 f260 f261 f262 f263 f264 f265 f266 f267 f268 f269 f270 f271 f272 f273 f274 f275 f276 f277 f278 f279 f280 f281 f282 f283 f284 f285 f286 f287 f288 f289 f290 f291 f292 f293 f294 f295 f296 f297 f298 f299 f300 f301 f302 f303 f304 f305 f306 f307 f308 f309 f310 f311 f312 f313 f314 f315 f316 f317 f318 f319 f320 f321 f322 f323 f324 f325 f326 f327 f328 f329 f330 f331 f332 f333 f334 f335 f336 f337 f338 f339 f340 f341 f342 f343 f344 f345 f346 f347 f348 f349 f350 f351 f352 f353 f354 f355 f356 f357 f358 f359 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 f960 f961 f962 f963 f964 f965 f966 f967 f968 f969 f970 f971 f972 f973 f974 f975 f976 f977 f978 f979 f980 f981 f982 f983 f984 f985 f986 f987 f988 f989 f990 f991 f992 f993 f994 f995 f996 f997 f998 f999 f1000 f1001 f1002 f1003 f1004 f1005 f1006 f1007 f1008 f1009 f1010 f1011 f1012 f1013 f1014 f1015 f1016 f1017 f1018 f1019 f1020 f1021 f1022 f1023 f1024 f1025 f1026 f1027 f1028 f1029 f1030 f1031 f1032 f1033 f1034 f1035 f1036 f1037 f1038 f1039 f1040 f1041 f1042 f1043 f1044 f1045 f1046 f1047 f1048 f1049 f1050 f1051 f1052 f1053 f1054 f1055 f1056 f1057 f1058 f1059 f1060 f1061 f1062 f1063 f1064 f1065 f1066 f1067 f1068 f1069 f1070 f1071 f1072 f1073 f1074 f1075 f1076 f1077 f1078 f1079 f1080 f1081 f1082 f1083 f1084 f1085 f1086 f1087 f1088 f1089 f1090 f1091 f1092 f1093 f1094 f1095 f1096 f1097 f1098 f1099 f1100 f1101 f1102 f1103 f1104 f1105 f1106 f1107 f1108 f1109 f1110 f1111 f1112 f1113 f1114 f1115 f1116 f1117 f1118 f1119 f1120 f1121 f1122 f1123 f1124 f1125 f1126 f1127 f1128 f1129 f1130 f1131 f1132 f1133 f1134 f1135 f1136 f1137 f1138 f1139 f1140 f1141 f1142 f1143 f1144 f1145 f1146 f1147 f1148 f1149 f1150 f1151 f1152 f1153 f1154 f1155 f1156 f1157 f1158 f1159 f1160 f1161 f1162 f1163 f1164 f1165 f1166 f1167 f1168 f1169 f1170 f1171 f1172 f1173 f1174 f1175 f1176 f1177 f1178 f1179 f1180 f1181 f1182 f1183 f1184 f1185 f1186 f1187 f1188 f1189 f1190 f1191 f1192 f1193 f1194 f1195 f1196 f1197 f1198 f1199 f1200 f1201 f1202 f1203 f1204 f1205 f1206 f1207 f1208 f1209 f1210 f1211 f1212 f1213 f1214 f1215 f1216 f1217 f1218 f1219 f1220 f1221 f1222 f1223 f1224 f1225 f1226 f1227 f1228 f1229 f1230 f1231 f1232 f1233 f1234 f1235 f1236 f1237 f1238 f1239 f1240 f1241 f1242 f1243 f1244 f1245 f1246 f1247 f1248 f1249 f1250 f1251 f1252 f1253 f1254 f1255 f1256 f1257 f1258 f1259 f1260 f1261 f1262 f1263 f1264 f1265 f1266 f1267 f1268 f1269 f1270 f1271 f1272 f1273 f1274 f1275 f1276 f1277 f1278 f1279 f1280 f1281 f1282 f1283 f1284 f1285 f1286 f1287 f1288 f1289 f1290 f1291 f1292 f1293 f1294 f1295 f1296 f1297 f1298 f1299 f1300 f1301 f1302 f1303 f1304 f1305 f1306 f1307 f1308 f1309 f1310 f1311 f1312 f1313 f1314 f1315 f1316 f1317 f1318 f1319 f1320 f1321 f1322 f1323 f1324 f1325 f1326 f1327 f1328 f1329 f1330 f1331 f1332 f1333 f1334 f1335 f1336 f1337 f1338 f1339 f1340 f1341 f1342 f1343 f1344 f1345 f1346 f1347 f1348 f1349 f1350 f1351 f1352 f1353 f1354 f1355 f1356 f1357 f1358 f1359 f1360 f1361 f1362 f1363 f1364 f1365 f1366 f1367 f1368 f1369 f1370 f1371 f1372 f1373 f1374 f1375 f1376 f1377 f1378 f1379 f1380 f1381 f1382 f1383 f1384 f1385 f1386 f1387 f1388 f1389 f1390 f1391 f1392 f1393 f1394 f1395 f1396 f1397 f1398 f1399 f1400 f1401 f1402 f1403 f1404 f1405 f1406 f1407 f1408 f1409 f1410 f1411 f1412 f1413 f1414 f1415 f1416 f1417 f1418 f1419 f1420 f1421 f1422 f1423 f1424 f1425 f1426 f1427 f1428 f1429 f1430 f1431 f1432 f1433 f1434 f1435 f1436 f1437 f1438 f1439 f1440 f1441 f1442 f1443 f1444 f1445 f1446 f1447 f1448 f1449 f1450 f1451 f1452 f1453 f1454 f1455 f1456 f1457 f1458 f1459 f1460 f1461 f1462 f1463 f1464 f1465 f1466 f1467 f1468 f1469 f1470 f1471 f1472 f1473 f1474 f1475 f1476 f1477 f1478 f1479 f1480 f1481 f1482 f1483 f1484 f1485 f1486 f1487 f1488 f1489 f1490 f1491 f1492 f1493 f1494 f1495 f1496 f1497 f1498 f1499 f1500 f1501 f1502 f1503 f1504 f1505 f1506 f1507 f1508 f1509 f1510 f1511 f1512 f1513 f1514 f1515 f1516 f1517 f1518 f1519 f1520 f1521 f1522 f1523 f1524 f1525 f1526 f1527 f1528 f1529 f1530 f1531 f1532 f1533 f1534 f1535 f1536 f1537 f1538 f1539 f1540 f1541 f1542 f1543 f1544 f1545 f1546 f1547 f1548 f1549 f1550 f1551 f1552 f1553 f1554 f1555 f1556 f1557 f1558 f1559 f1560 f1561 f1562 f1563 f1564 f1565 f1566 f1567 f1568 f1569 f1570 f1571 f1572 f1573 f1574 f1575 f1576 f1577 f1578 f1579 f1580 f1581 f1582 f1583 f1584 f1585 f1586 f1587 f1588 f1589 f1590 f1591 f1592 f1593 f1594 f1595 f1596 f1597 f1598 f1599 f1600 f1601 f1602 f1603 f1604 f1605 f1606 f1607 f1608 f1609 f1610 f1611 f1612 f1613 f1614 f1615 f1616 f1617 f1618 f1619 f1620 f1621 f1622 f1623 f1624 f1625 f1626 f1627 f1628 f1629 f1630 f1631 f1632 f1633 f1634 f1635 f1636 f1637 f1638 f1639 f1640 f1641 f1642 f1643 f1644 f1645 f1646 f1647 f1648 f1649 f1650 f1651 f1652 f1653 f1654 f1655 f1656 f1657 f1658 f1659 f1660 f1661 f1662 f1663 f1664 f1665 f1666 f1667 f1668 f1669 f1670 f1671 f1672 f1673 f1674 f1675 f1676 f1677 f1678 f1679 f1680 f1681 f1682 f1683 f1684 f1685 f1686 f1687 f1688 f1689 f1690 f1691 f1692 f1693 f1694 f1695 f1696 f1697 f1698 f1699 f1700 f1701 f1702 f1703 f1704 f1705 f1706 f1707 f1708 f1709 f1710 f1711 f1712 f1713 f1714 f1715 f1716 f1717 f1718 f1719 f1720 f1721 f1722 f1723 f1724 f1725 f1726 f1727 f1728 f1729 f1730 f1731 f1732 f1733 f1734 f1735 f1736 f1737 f1738 f1739 f1740 f1741 f1742 f1743 f1744 f1745 f1746 f1747 f1748 f1749 f1750 f1751 f1752 f1753 f1754 f1755 f1756 f1757 f1758 f1759 f1760 f1761 f1762 f1763 f1764 f1765 f1766 f1767 f1768 f1769 f1770 f1771 f1772 f1773 f1774 f1775 f1776 f1777 f1778 f1779 f1780 f1781 f1782 f1783 f1784 f1785 f1786 f1787 f1788 f1789 f1790 f1791 f1792 f1793 f1794 f1795 f1796 f1797 f1798 f1799 f1800 f1801 f1802 f1803 f1804 f1805 f1806 f1807 f1808 f1809 f1810 f1811 f1812 f1813 f1814 f1815 f1816 f1817 f1818 f1819 f1820 f1821 f1822 f1823 f1824 f1825 f1826 f1827 f1828 f1829 f1830 f1831 f1832 f1833 f1834 f1835 f1836 f1837 f1838 f1839 f1840 f1841 f1842 f1843 f1844 f1845 f1846 f1847 f1848 f1849 f1850 f1851 f1852 f1853 f1854 f1855 f1856 f1857 f1858 f1859 f1860 f1861 f1862 f1863 f1864 f1865 f1866 f1867 f1868 f1869 f1870 f1871 f1872 f1873 f1874 f1875 f1876 f1877 f1878 f1879 f1880 f1881 f1882 f1883 f1884 f1885 f1886 f1887 f1888 f1889 f1890 f1891 f1892 f1893 f1894 f1895 f1896 f1897 f1898 f1899 f1900 f1901 f1902 f1903 f1904 f1905 f1906 f1907 f1908 f1909 f1910 f1911 f1912 f1913 f1914 f1915 f1916 f1917 f1918 f1919 f1920 f1921 f1922 f1923 f1924 f1925 f1926 f1927 f1928 f1929 f1930 f1931 f1932 f1933 f1934 f1935 f1936 f1937 f1938 f1939 f1940 f1941 f1942 f1943 f1944 f1945 f1946 f1947 f1948 f1949 f1950 f1951 f1952 f1953 f1954 f1955 f1956 f1957 f1958 f1959 f1960 f1961 f1962 f1963 f1964 f1965 f1966 f1967 f1968 f1969 f1970 f1971 f1972 f1973 f1974 f1975 f1976 f1977 f1978 f1979 f1980 f1981 f1982 f1983 f1984 f1985 f1986 f1987 f1988 f1989 f1990 f1991 f1992 f1993 f1994 f1995 f1996 f1997 f1998 f1999 f2000 f2001 f2002 f2003 f2004 f2005 f2006 f2007 f2008 f2009 f2010 f2011 f2012 f2013 f2014 f2015 f2016 f2017 f2018 f2019 f2020 f2021 f2022 f2023 f2024 f2025 f2026 f2027 f2028 f2029 f2030 f2031 f2032 f2033 f2034 f2035 f2036 f2037 f2038 f2039 f2040 f2041 f2042 f2043 f2044 f2045 f2046 f2047 f2048 f2049 f2050 f2051 f2052 f2053 f2054 f2055 f2056 f2057 f2058 f2059 f2060 f2061 f2062 f2063 f2064 f2065 f2066 f2067 f2068 f2069 f2070 f2071 f2072 f2073 f2074 f2075 f2076 f2077 f2078 f2079 f2080 f2081 f2082 f2083 f2084 f2085 f2086 f2087 f2088 f2089 f2090 f2091 f2092 f2093 f2094 f2095 f2096 f2097 f2098 f2099 f2100 f2101 f2102 f2103 f2104 f2105 f2106 f2107 f2108 f2109 f2110 f2111 f2112 f2113 f2114 f2115 f2116 f2117 f2118 f2119 f2120 f2121 f2122 f2123 f2124 f2125 f2126 f2127 f2128 f2129 f2130 f2131 f2132 f2133 f2134 f2135 f2136 f2137 f2138 f2139 f2140 f2141 f2142 f2143 f2144 f2145 f2146 f2147 f2148 f2149 f2150 f2151 f2152 f2153 f2154 f2155 f2156 f2157 f2158 f2159 f2160 f2161 f2162 f2163 f2164 f2165 f2166 f2167 f2168 f2169 f2170 f2171 f2172 f2173 f2174 f2175 f2176 f2177 f2178 f2179 f2180 f2181 f2182 f2183 f2184 f2185 f2186 f2187 f2188 f2189 f2190 f2191 f2192 f2193 f2194 f2195 f2196 f2197 f2198 f2199 f2200 f2201 f2202 f2203 f2204 f2205 f2206 f2207 f2208 f2209 f2210 f2211 f2212 f2213 f2214 f2215 f2216 f2217 f2218 f2219 f2220 f2221 f2222 f2223 f2224 f2225 f2226 f2227 f2228 f2229 f2230 f2231 f2232 f2233 f2234 f2235 f2236 f2237 f2238 f2239 f2240 f2241 f2242 f2243 f2244 f2245 f2246 f2247 f2248 f2249 f2250 f2251 f2252 f2253 f2254 f2255 f2256 f2257 f2258 f2259 f2260 f2261 f2262 f2263 f2264 f2265 f2266 f2267 f2268 f2269 f2270 f2271 f2272 f2273 f2274 f2275 f2276 f2277 f2278 f2279 f2280 f2281 f2282 f2283 f2284 f2285 f2286 f2287 f2288 f2289 f2290 f2291 f2292 f2293 f2294 f2295 f2296 f2297 f2298 f2299 f2300 f2301 f2302 f2303 f2304 f2305 f2306 f2307 f2308 f2309 f2310 f2311 f2312 f2313 f2314 f2315 f2316 f2317 f2318 f2319 f2320 f2321))