(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES b# a b -> b# a a a b, b# a b -> b#, b# a a b a a a b -> b# b a a a b a a b a a b, b# a a b a a a b -> b# a a a b a a b a a b, b# a a b a a a b -> b# a a b a a b, b# a a b a a a b -> b# a a b, b# a a b a a a b -> b#, b# b b a a a b -> b# a a a b b b, b# b b a a a b -> b# b b, b# b b a a a b -> b# b, b# b b a a a b -> b#, b# b a a b -> b#, b# a a b b -> b#, b a b ->= b a a a b, b a a b a a a b ->= b b a a a b a a b a a b, b a a a b a a a b ->= b, b b b a a a b ->= b a a a b b b, b b a a b ->= b, b a a b b ->= b, b a b a a a b ->= b, b a a a b 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 f6) (finite f10)) (or (finite f12) (finite f16)) (or (finite f0) (finite f4)))) (define-fun f18 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f19 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f20 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f21 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f22 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f23 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f24 () Arctic (+ f10 f22)) (define-fun f25 () Arctic (+ f11 f23)) (define-fun f26 () Arctic (+ (* f0 f18) (* f1 f20))) (define-fun f27 () Arctic (+ (* f0 f19) (* f1 f21))) (define-fun f28 () Arctic (+ (* f2 f18) (* f3 f20))) (define-fun f29 () Arctic (+ (* f2 f19) (* f3 f21))) (define-fun f30 () Arctic (+ (* f0 f24) (* f1 f25))) (define-fun f31 () Arctic (+ (* f2 f24) (* f3 f25))) (define-fun f32 () Arctic (+ f4 f30)) (define-fun f33 () Arctic (+ f5 f31)) (define-fun f34 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f35 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f36 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f37 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f38 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f39 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f40 () Arctic (+ f10 f38)) (define-fun f41 () Arctic (+ f11 f39)) (define-fun f42 () Arctic (+ (* f6 f34) (* f7 f36))) (define-fun f43 () Arctic (+ (* f6 f35) (* f7 f37))) (define-fun f44 () Arctic (+ (* f8 f34) (* f9 f36))) (define-fun f45 () Arctic (+ (* f8 f35) (* f9 f37))) (define-fun f46 () Arctic (+ (* f6 f40) (* f7 f41))) (define-fun f47 () Arctic (+ (* f8 f40) (* f9 f41))) (define-fun f48 () Arctic (+ f10 f46)) (define-fun f49 () Arctic (+ f11 f47)) (define-fun f50 () Arctic (+ (* f6 f42) (* f7 f44))) (define-fun f51 () Arctic (+ (* f6 f43) (* f7 f45))) (define-fun f52 () Arctic (+ (* f8 f42) (* f9 f44))) (define-fun f53 () Arctic (+ (* f8 f43) (* f9 f45))) (define-fun f54 () Arctic (+ (* f6 f48) (* f7 f49))) (define-fun f55 () Arctic (+ (* f8 f48) (* f9 f49))) (define-fun f56 () Arctic (+ f10 f54)) (define-fun f57 () Arctic (+ f11 f55)) (define-fun f58 () Arctic (+ (* f0 f50) (* f1 f52))) (define-fun f59 () Arctic (+ (* f0 f51) (* f1 f53))) (define-fun f60 () Arctic (+ (* f2 f50) (* f3 f52))) (define-fun f61 () Arctic (+ (* f2 f51) (* f3 f53))) (define-fun f62 () Arctic (+ (* f0 f56) (* f1 f57))) (define-fun f63 () Arctic (+ (* f2 f56) (* f3 f57))) (define-fun f64 () Arctic (+ f4 f62)) (define-fun f65 () Arctic (+ f5 f63)) (define-fun f66 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f67 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f68 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f69 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f70 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f71 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f72 () Arctic (+ f10 f70)) (define-fun f73 () Arctic (+ f11 f71)) (define-fun f74 () Arctic (+ (* f0 f66) (* f1 f68))) (define-fun f75 () Arctic (+ (* f0 f67) (* f1 f69))) (define-fun f76 () Arctic (+ (* f2 f66) (* f3 f68))) (define-fun f77 () Arctic (+ (* f2 f67) (* f3 f69))) (define-fun f78 () Arctic (+ (* f0 f72) (* f1 f73))) (define-fun f79 () Arctic (+ (* f2 f72) (* f3 f73))) (define-fun f80 () Arctic (+ f4 f78)) (define-fun f81 () Arctic (+ f5 f79)) (define-fun f82 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f83 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f84 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f85 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f86 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f87 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f88 () Arctic (+ f10 f86)) (define-fun f89 () Arctic (+ f11 f87)) (define-fun f90 () Arctic (+ (* f6 f82) (* f7 f84))) (define-fun f91 () Arctic (+ (* f6 f83) (* f7 f85))) (define-fun f92 () Arctic (+ (* f8 f82) (* f9 f84))) (define-fun f93 () Arctic (+ (* f8 f83) (* f9 f85))) (define-fun f94 () Arctic (+ (* f6 f88) (* f7 f89))) (define-fun f95 () Arctic (+ (* f8 f88) (* f9 f89))) (define-fun f96 () Arctic (+ f10 f94)) (define-fun f97 () Arctic (+ f11 f95)) (define-fun f98 () Arctic (+ (* f6 f90) (* f7 f92))) (define-fun f99 () Arctic (+ (* f6 f91) (* f7 f93))) (define-fun f100 () Arctic (+ (* f8 f90) (* f9 f92))) (define-fun f101 () Arctic (+ (* f8 f91) (* f9 f93))) (define-fun f102 () Arctic (+ (* f6 f96) (* f7 f97))) (define-fun f103 () Arctic (+ (* f8 f96) (* f9 f97))) (define-fun f104 () Arctic (+ f10 f102)) (define-fun f105 () Arctic (+ f11 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 (+ (* f6 f114) (* f7 f116))) (define-fun f123 () Arctic (+ (* f6 f115) (* f7 f117))) (define-fun f124 () Arctic (+ (* f8 f114) (* f9 f116))) (define-fun f125 () Arctic (+ (* f8 f115) (* f9 f117))) (define-fun f126 () Arctic (+ (* f6 f120) (* f7 f121))) (define-fun f127 () Arctic (+ (* f8 f120) (* f9 f121))) (define-fun f128 () Arctic (+ f10 f126)) (define-fun f129 () Arctic (+ f11 f127)) (define-fun f130 () Arctic (+ (* f0 f122) (* f1 f124))) (define-fun f131 () Arctic (+ (* f0 f123) (* f1 f125))) (define-fun f132 () Arctic (+ (* f2 f122) (* f3 f124))) (define-fun f133 () Arctic (+ (* f2 f123) (* f3 f125))) (define-fun f134 () Arctic (+ (* f0 f128) (* f1 f129))) (define-fun f135 () Arctic (+ (* f2 f128) (* f3 f129))) (define-fun f136 () Arctic (+ f4 f134)) (define-fun f137 () Arctic (+ f5 f135)) (define-fun f138 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f139 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f140 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f141 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f142 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f143 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f144 () Arctic (+ f10 f142)) (define-fun f145 () Arctic (+ f11 f143)) (define-fun f146 () Arctic (+ (* f6 f138) (* f7 f140))) (define-fun f147 () Arctic (+ (* f6 f139) (* f7 f141))) (define-fun f148 () Arctic (+ (* f8 f138) (* f9 f140))) (define-fun f149 () Arctic (+ (* f8 f139) (* f9 f141))) (define-fun f150 () Arctic (+ (* f6 f144) (* f7 f145))) (define-fun f151 () Arctic (+ (* f8 f144) (* f9 f145))) (define-fun f152 () Arctic (+ f10 f150)) (define-fun f153 () Arctic (+ f11 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 (+ (* f6 f154) (* f7 f156))) (define-fun f163 () Arctic (+ (* f6 f155) (* f7 f157))) (define-fun f164 () Arctic (+ (* f8 f154) (* f9 f156))) (define-fun f165 () Arctic (+ (* f8 f155) (* f9 f157))) (define-fun f166 () Arctic (+ (* f6 f160) (* f7 f161))) (define-fun f167 () Arctic (+ (* f8 f160) (* f9 f161))) (define-fun f168 () Arctic (+ f10 f166)) (define-fun f169 () Arctic (+ f11 f167)) (define-fun f170 () Arctic (+ (* f6 f162) (* f7 f164))) (define-fun f171 () Arctic (+ (* f6 f163) (* f7 f165))) (define-fun f172 () Arctic (+ (* f8 f162) (* f9 f164))) (define-fun f173 () Arctic (+ (* f8 f163) (* f9 f165))) (define-fun f174 () Arctic (+ (* f6 f168) (* f7 f169))) (define-fun f175 () Arctic (+ (* f8 f168) (* f9 f169))) (define-fun f176 () Arctic (+ f10 f174)) (define-fun f177 () Arctic (+ f11 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 (+ (* f6 f186) (* f7 f188))) (define-fun f195 () Arctic (+ (* f6 f187) (* f7 f189))) (define-fun f196 () Arctic (+ (* f8 f186) (* f9 f188))) (define-fun f197 () Arctic (+ (* f8 f187) (* f9 f189))) (define-fun f198 () Arctic (+ (* f6 f192) (* f7 f193))) (define-fun f199 () Arctic (+ (* f8 f192) (* f9 f193))) (define-fun f200 () Arctic (+ f10 f198)) (define-fun f201 () Arctic (+ f11 f199)) (define-fun f202 () Arctic (+ (* f6 f194) (* f7 f196))) (define-fun f203 () Arctic (+ (* f6 f195) (* f7 f197))) (define-fun f204 () Arctic (+ (* f8 f194) (* f9 f196))) (define-fun f205 () Arctic (+ (* f8 f195) (* f9 f197))) (define-fun f206 () Arctic (+ (* f6 f200) (* f7 f201))) (define-fun f207 () Arctic (+ (* f8 f200) (* f9 f201))) (define-fun f208 () Arctic (+ f10 f206)) (define-fun f209 () Arctic (+ f11 f207)) (define-fun f210 () Arctic (+ (* f12 f202) (* f13 f204))) (define-fun f211 () Arctic (+ (* f12 f203) (* f13 f205))) (define-fun f212 () Arctic (+ (* f14 f202) (* f15 f204))) (define-fun f213 () Arctic (+ (* f14 f203) (* f15 f205))) (define-fun f214 () Arctic (+ (* f12 f208) (* f13 f209))) (define-fun f215 () Arctic (+ (* f14 f208) (* f15 f209))) (define-fun f216 () Arctic (+ f16 f214)) (define-fun f217 () Arctic (+ f17 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 (+ (* f6 f12) (* f7 f14))) (define-fun f227 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f228 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f229 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f230 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f231 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f232 () Arctic (+ f10 f230)) (define-fun f233 () Arctic (+ f11 f231)) (define-fun f234 () Arctic (+ (* f6 f226) (* f7 f228))) (define-fun f235 () Arctic (+ (* f6 f227) (* f7 f229))) (define-fun f236 () Arctic (+ (* f8 f226) (* f9 f228))) (define-fun f237 () Arctic (+ (* f8 f227) (* f9 f229))) (define-fun f238 () Arctic (+ (* f6 f232) (* f7 f233))) (define-fun f239 () Arctic (+ (* f8 f232) (* f9 f233))) (define-fun f240 () Arctic (+ f10 f238)) (define-fun f241 () Arctic (+ f11 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 (+ (* f12 f242) (* f13 f244))) (define-fun f251 () Arctic (+ (* f12 f243) (* f13 f245))) (define-fun f252 () Arctic (+ (* f14 f242) (* f15 f244))) (define-fun f253 () Arctic (+ (* f14 f243) (* f15 f245))) (define-fun f254 () Arctic (+ (* f12 f248) (* f13 f249))) (define-fun f255 () Arctic (+ (* f14 f248) (* f15 f249))) (define-fun f256 () Arctic (+ f16 f254)) (define-fun f257 () Arctic (+ f17 f255)) (define-fun f258 () Arctic (+ (* f6 f250) (* f7 f252))) (define-fun f259 () Arctic (+ (* f6 f251) (* f7 f253))) (define-fun f260 () Arctic (+ (* f8 f250) (* f9 f252))) (define-fun f261 () Arctic (+ (* f8 f251) (* f9 f253))) (define-fun f262 () Arctic (+ (* f6 f256) (* f7 f257))) (define-fun f263 () Arctic (+ (* f8 f256) (* f9 f257))) (define-fun f264 () Arctic (+ f10 f262)) (define-fun f265 () Arctic (+ f11 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 (+ (* f0 f266) (* f1 f268))) (define-fun f275 () Arctic (+ (* f0 f267) (* f1 f269))) (define-fun f276 () Arctic (+ (* f2 f266) (* f3 f268))) (define-fun f277 () Arctic (+ (* f2 f267) (* f3 f269))) (define-fun f278 () Arctic (+ (* f0 f272) (* f1 f273))) (define-fun f279 () Arctic (+ (* f2 f272) (* f3 f273))) (define-fun f280 () Arctic (+ f4 f278)) (define-fun f281 () Arctic (+ f5 f279)) (define-fun f282 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f283 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f284 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f285 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f286 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f287 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f288 () Arctic (+ f10 f286)) (define-fun f289 () Arctic (+ f11 f287)) (define-fun f290 () Arctic (+ (* f6 f282) (* f7 f284))) (define-fun f291 () Arctic (+ (* f6 f283) (* f7 f285))) (define-fun f292 () Arctic (+ (* f8 f282) (* f9 f284))) (define-fun f293 () Arctic (+ (* f8 f283) (* f9 f285))) (define-fun f294 () Arctic (+ (* f6 f288) (* f7 f289))) (define-fun f295 () Arctic (+ (* f8 f288) (* f9 f289))) (define-fun f296 () Arctic (+ f10 f294)) (define-fun f297 () Arctic (+ f11 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 (+ (* f6 f298) (* f7 f300))) (define-fun f307 () Arctic (+ (* f6 f299) (* f7 f301))) (define-fun f308 () Arctic (+ (* f8 f298) (* f9 f300))) (define-fun f309 () Arctic (+ (* f8 f299) (* f9 f301))) (define-fun f310 () Arctic (+ (* f6 f304) (* f7 f305))) (define-fun f311 () Arctic (+ (* f8 f304) (* f9 f305))) (define-fun f312 () Arctic (+ f10 f310)) (define-fun f313 () Arctic (+ f11 f311)) (define-fun f314 () Arctic (+ (* f6 f306) (* f7 f308))) (define-fun f315 () Arctic (+ (* f6 f307) (* f7 f309))) (define-fun f316 () Arctic (+ (* f8 f306) (* f9 f308))) (define-fun f317 () Arctic (+ (* f8 f307) (* f9 f309))) (define-fun f318 () Arctic (+ (* f6 f312) (* f7 f313))) (define-fun f319 () Arctic (+ (* f8 f312) (* f9 f313))) (define-fun f320 () Arctic (+ f10 f318)) (define-fun f321 () Arctic (+ f11 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 (+ (* f6 f322) (* f7 f324))) (define-fun f331 () Arctic (+ (* f6 f323) (* f7 f325))) (define-fun f332 () Arctic (+ (* f8 f322) (* f9 f324))) (define-fun f333 () Arctic (+ (* f8 f323) (* f9 f325))) (define-fun f334 () Arctic (+ (* f6 f328) (* f7 f329))) (define-fun f335 () Arctic (+ (* f8 f328) (* f9 f329))) (define-fun f336 () Arctic (+ f10 f334)) (define-fun f337 () Arctic (+ f11 f335)) (define-fun f338 () Arctic (+ (* f6 f330) (* f7 f332))) (define-fun f339 () Arctic (+ (* f6 f331) (* f7 f333))) (define-fun f340 () Arctic (+ (* f8 f330) (* f9 f332))) (define-fun f341 () Arctic (+ (* f8 f331) (* f9 f333))) (define-fun f342 () Arctic (+ (* f6 f336) (* f7 f337))) (define-fun f343 () Arctic (+ (* f8 f336) (* f9 f337))) (define-fun f344 () Arctic (+ f10 f342)) (define-fun f345 () Arctic (+ f11 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 (+ (* f0 f346) (* f1 f348))) (define-fun f355 () Arctic (+ (* f0 f347) (* f1 f349))) (define-fun f356 () Arctic (+ (* f2 f346) (* f3 f348))) (define-fun f357 () Arctic (+ (* f2 f347) (* f3 f349))) (define-fun f358 () Arctic (+ (* f0 f352) (* f1 f353))) (define-fun f359 () Arctic (+ (* f2 f352) (* f3 f353))) (define-fun f360 () Arctic (+ f4 f358)) (define-fun f361 () Arctic (+ f5 f359)) (define-fun f362 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f363 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f364 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f365 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f366 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f367 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f368 () Arctic (+ f10 f366)) (define-fun f369 () Arctic (+ f11 f367)) (define-fun f370 () Arctic (+ (* f6 f362) (* f7 f364))) (define-fun f371 () Arctic (+ (* f6 f363) (* f7 f365))) (define-fun f372 () Arctic (+ (* f8 f362) (* f9 f364))) (define-fun f373 () Arctic (+ (* f8 f363) (* f9 f365))) (define-fun f374 () Arctic (+ (* f6 f368) (* f7 f369))) (define-fun f375 () Arctic (+ (* f8 f368) (* f9 f369))) (define-fun f376 () Arctic (+ f10 f374)) (define-fun f377 () Arctic (+ f11 f375)) (define-fun f378 () Arctic (+ (* f6 f370) (* f7 f372))) (define-fun f379 () Arctic (+ (* f6 f371) (* f7 f373))) (define-fun f380 () Arctic (+ (* f8 f370) (* f9 f372))) (define-fun f381 () Arctic (+ (* f8 f371) (* f9 f373))) (define-fun f382 () Arctic (+ (* f6 f376) (* f7 f377))) (define-fun f383 () Arctic (+ (* f8 f376) (* f9 f377))) (define-fun f384 () Arctic (+ f10 f382)) (define-fun f385 () Arctic (+ f11 f383)) (define-fun f386 () Arctic (+ (* f12 f378) (* f13 f380))) (define-fun f387 () Arctic (+ (* f12 f379) (* f13 f381))) (define-fun f388 () Arctic (+ (* f14 f378) (* f15 f380))) (define-fun f389 () Arctic (+ (* f14 f379) (* f15 f381))) (define-fun f390 () Arctic (+ (* f12 f384) (* f13 f385))) (define-fun f391 () Arctic (+ (* f14 f384) (* f15 f385))) (define-fun f392 () Arctic (+ f16 f390)) (define-fun f393 () Arctic (+ f17 f391)) (define-fun f394 () Arctic (+ (* f6 f386) (* f7 f388))) (define-fun f395 () Arctic (+ (* f6 f387) (* f7 f389))) (define-fun f396 () Arctic (+ (* f8 f386) (* f9 f388))) (define-fun f397 () Arctic (+ (* f8 f387) (* f9 f389))) (define-fun f398 () Arctic (+ (* f6 f392) (* f7 f393))) (define-fun f399 () Arctic (+ (* f8 f392) (* f9 f393))) (define-fun f400 () Arctic (+ f10 f398)) (define-fun f401 () Arctic (+ f11 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 (+ (* f0 f402) (* f1 f404))) (define-fun f411 () Arctic (+ (* f0 f403) (* f1 f405))) (define-fun f412 () Arctic (+ (* f2 f402) (* f3 f404))) (define-fun f413 () Arctic (+ (* f2 f403) (* f3 f405))) (define-fun f414 () Arctic (+ (* f0 f408) (* f1 f409))) (define-fun f415 () Arctic (+ (* f2 f408) (* f3 f409))) (define-fun f416 () Arctic (+ f4 f414)) (define-fun f417 () Arctic (+ f5 f415)) (define-fun f418 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f419 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f420 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f421 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f422 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f423 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f424 () Arctic (+ f10 f422)) (define-fun f425 () Arctic (+ f11 f423)) (define-fun f426 () Arctic (+ (* f6 f418) (* f7 f420))) (define-fun f427 () Arctic (+ (* f6 f419) (* f7 f421))) (define-fun f428 () Arctic (+ (* f8 f418) (* f9 f420))) (define-fun f429 () Arctic (+ (* f8 f419) (* f9 f421))) (define-fun f430 () Arctic (+ (* f6 f424) (* f7 f425))) (define-fun f431 () Arctic (+ (* f8 f424) (* f9 f425))) (define-fun f432 () Arctic (+ f10 f430)) (define-fun f433 () Arctic (+ f11 f431)) (define-fun f434 () Arctic (+ (* f12 f426) (* f13 f428))) (define-fun f435 () Arctic (+ (* f12 f427) (* f13 f429))) (define-fun f436 () Arctic (+ (* f14 f426) (* f15 f428))) (define-fun f437 () Arctic (+ (* f14 f427) (* f15 f429))) (define-fun f438 () Arctic (+ (* f12 f432) (* f13 f433))) (define-fun f439 () Arctic (+ (* f14 f432) (* f15 f433))) (define-fun f440 () Arctic (+ f16 f438)) (define-fun f441 () Arctic (+ f17 f439)) (define-fun f442 () Arctic (+ (* f6 f434) (* f7 f436))) (define-fun f443 () Arctic (+ (* f6 f435) (* f7 f437))) (define-fun f444 () Arctic (+ (* f8 f434) (* f9 f436))) (define-fun f445 () Arctic (+ (* f8 f435) (* f9 f437))) (define-fun f446 () Arctic (+ (* f6 f440) (* f7 f441))) (define-fun f447 () Arctic (+ (* f8 f440) (* f9 f441))) (define-fun f448 () Arctic (+ f10 f446)) (define-fun f449 () Arctic (+ f11 f447)) (define-fun f450 () Arctic (+ (* f6 f442) (* f7 f444))) (define-fun f451 () Arctic (+ (* f6 f443) (* f7 f445))) (define-fun f452 () Arctic (+ (* f8 f442) (* f9 f444))) (define-fun f453 () Arctic (+ (* f8 f443) (* f9 f445))) (define-fun f454 () Arctic (+ (* f6 f448) (* f7 f449))) (define-fun f455 () Arctic (+ (* f8 f448) (* f9 f449))) (define-fun f456 () Arctic (+ f10 f454)) (define-fun f457 () Arctic (+ f11 f455)) (define-fun f458 () Arctic (+ (* f0 f450) (* f1 f452))) (define-fun f459 () Arctic (+ (* f0 f451) (* f1 f453))) (define-fun f460 () Arctic (+ (* f2 f450) (* f3 f452))) (define-fun f461 () Arctic (+ (* f2 f451) (* f3 f453))) (define-fun f462 () Arctic (+ (* f0 f456) (* f1 f457))) (define-fun f463 () Arctic (+ (* f2 f456) (* f3 f457))) (define-fun f464 () Arctic (+ f4 f462)) (define-fun f465 () Arctic (+ f5 f463)) (define-fun f466 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f467 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f468 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f469 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f470 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f471 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f472 () Arctic (+ f10 f470)) (define-fun f473 () Arctic (+ f11 f471)) (define-fun f474 () Arctic (+ (* f6 f466) (* f7 f468))) (define-fun f475 () Arctic (+ (* f6 f467) (* f7 f469))) (define-fun f476 () Arctic (+ (* f8 f466) (* f9 f468))) (define-fun f477 () Arctic (+ (* f8 f467) (* f9 f469))) (define-fun f478 () Arctic (+ (* f6 f472) (* f7 f473))) (define-fun f479 () Arctic (+ (* f8 f472) (* f9 f473))) (define-fun f480 () Arctic (+ f10 f478)) (define-fun f481 () Arctic (+ f11 f479)) (define-fun f482 () Arctic (+ (* f6 f474) (* f7 f476))) (define-fun f483 () Arctic (+ (* f6 f475) (* f7 f477))) (define-fun f484 () Arctic (+ (* f8 f474) (* f9 f476))) (define-fun f485 () Arctic (+ (* f8 f475) (* f9 f477))) (define-fun f486 () Arctic (+ (* f6 f480) (* f7 f481))) (define-fun f487 () Arctic (+ (* f8 f480) (* f9 f481))) (define-fun f488 () Arctic (+ f10 f486)) (define-fun f489 () Arctic (+ f11 f487)) (define-fun f490 () Arctic (+ (* f12 f482) (* f13 f484))) (define-fun f491 () Arctic (+ (* f12 f483) (* f13 f485))) (define-fun f492 () Arctic (+ (* f14 f482) (* f15 f484))) (define-fun f493 () Arctic (+ (* f14 f483) (* f15 f485))) (define-fun f494 () Arctic (+ (* f12 f488) (* f13 f489))) (define-fun f495 () Arctic (+ (* f14 f488) (* f15 f489))) (define-fun f496 () Arctic (+ f16 f494)) (define-fun f497 () Arctic (+ f17 f495)) (define-fun f498 () Arctic (+ (* f6 f490) (* f7 f492))) (define-fun f499 () Arctic (+ (* f6 f491) (* f7 f493))) (define-fun f500 () Arctic (+ (* f8 f490) (* f9 f492))) (define-fun f501 () Arctic (+ (* f8 f491) (* f9 f493))) (define-fun f502 () Arctic (+ (* f6 f496) (* f7 f497))) (define-fun f503 () Arctic (+ (* f8 f496) (* f9 f497))) (define-fun f504 () Arctic (+ f10 f502)) (define-fun f505 () Arctic (+ f11 f503)) (define-fun f506 () Arctic (+ (* f6 f498) (* f7 f500))) (define-fun f507 () Arctic (+ (* f6 f499) (* f7 f501))) (define-fun f508 () Arctic (+ (* f8 f498) (* f9 f500))) (define-fun f509 () Arctic (+ (* f8 f499) (* f9 f501))) (define-fun f510 () Arctic (+ (* f6 f504) (* f7 f505))) (define-fun f511 () Arctic (+ (* f8 f504) (* f9 f505))) (define-fun f512 () Arctic (+ f10 f510)) (define-fun f513 () Arctic (+ f11 f511)) (define-fun f514 () Arctic (+ (* f0 f506) (* f1 f508))) (define-fun f515 () Arctic (+ (* f0 f507) (* f1 f509))) (define-fun f516 () Arctic (+ (* f2 f506) (* f3 f508))) (define-fun f517 () Arctic (+ (* f2 f507) (* f3 f509))) (define-fun f518 () Arctic (+ (* f0 f512) (* f1 f513))) (define-fun f519 () Arctic (+ (* f2 f512) (* f3 f513))) (define-fun f520 () Arctic (+ f4 f518)) (define-fun f521 () Arctic (+ f5 f519)) (define-fun f522 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f523 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f524 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f525 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f526 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f527 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f528 () Arctic (+ f10 f526)) (define-fun f529 () Arctic (+ f11 f527)) (define-fun f530 () Arctic (+ (* f6 f522) (* f7 f524))) (define-fun f531 () Arctic (+ (* f6 f523) (* f7 f525))) (define-fun f532 () Arctic (+ (* f8 f522) (* f9 f524))) (define-fun f533 () Arctic (+ (* f8 f523) (* f9 f525))) (define-fun f534 () Arctic (+ (* f6 f528) (* f7 f529))) (define-fun f535 () Arctic (+ (* f8 f528) (* f9 f529))) (define-fun f536 () Arctic (+ f10 f534)) (define-fun f537 () Arctic (+ f11 f535)) (define-fun f538 () Arctic (+ (* f0 f530) (* f1 f532))) (define-fun f539 () Arctic (+ (* f0 f531) (* f1 f533))) (define-fun f540 () Arctic (+ (* f2 f530) (* f3 f532))) (define-fun f541 () Arctic (+ (* f2 f531) (* f3 f533))) (define-fun f542 () Arctic (+ (* f0 f536) (* f1 f537))) (define-fun f543 () Arctic (+ (* f2 f536) (* f3 f537))) (define-fun f544 () Arctic (+ f4 f542)) (define-fun f545 () Arctic (+ f5 f543)) (define-fun f546 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f547 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f548 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f549 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f550 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f551 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f552 () Arctic (+ f10 f550)) (define-fun f553 () Arctic (+ f11 f551)) (define-fun f554 () Arctic (+ (* f6 f546) (* f7 f548))) (define-fun f555 () Arctic (+ (* f6 f547) (* f7 f549))) (define-fun f556 () Arctic (+ (* f8 f546) (* f9 f548))) (define-fun f557 () Arctic (+ (* f8 f547) (* f9 f549))) (define-fun f558 () Arctic (+ (* f6 f552) (* f7 f553))) (define-fun f559 () Arctic (+ (* f8 f552) (* f9 f553))) (define-fun f560 () Arctic (+ f10 f558)) (define-fun f561 () Arctic (+ f11 f559)) (define-fun f562 () Arctic (+ (* f6 f554) (* f7 f556))) (define-fun f563 () Arctic (+ (* f6 f555) (* f7 f557))) (define-fun f564 () Arctic (+ (* f8 f554) (* f9 f556))) (define-fun f565 () Arctic (+ (* f8 f555) (* f9 f557))) (define-fun f566 () Arctic (+ (* f6 f560) (* f7 f561))) (define-fun f567 () Arctic (+ (* f8 f560) (* f9 f561))) (define-fun f568 () Arctic (+ f10 f566)) (define-fun f569 () Arctic (+ f11 f567)) (define-fun f570 () Arctic (+ (* f12 f562) (* f13 f564))) (define-fun f571 () Arctic (+ (* f12 f563) (* f13 f565))) (define-fun f572 () Arctic (+ (* f14 f562) (* f15 f564))) (define-fun f573 () Arctic (+ (* f14 f563) (* f15 f565))) (define-fun f574 () Arctic (+ (* f12 f568) (* f13 f569))) (define-fun f575 () Arctic (+ (* f14 f568) (* f15 f569))) (define-fun f576 () Arctic (+ f16 f574)) (define-fun f577 () Arctic (+ f17 f575)) (define-fun f578 () Arctic (+ (* f6 f570) (* f7 f572))) (define-fun f579 () Arctic (+ (* f6 f571) (* f7 f573))) (define-fun f580 () Arctic (+ (* f8 f570) (* f9 f572))) (define-fun f581 () Arctic (+ (* f8 f571) (* f9 f573))) (define-fun f582 () Arctic (+ (* f6 f576) (* f7 f577))) (define-fun f583 () Arctic (+ (* f8 f576) (* f9 f577))) (define-fun f584 () Arctic (+ f10 f582)) (define-fun f585 () Arctic (+ f11 f583)) (define-fun f586 () Arctic (+ (* f6 f578) (* f7 f580))) (define-fun f587 () Arctic (+ (* f6 f579) (* f7 f581))) (define-fun f588 () Arctic (+ (* f8 f578) (* f9 f580))) (define-fun f589 () Arctic (+ (* f8 f579) (* f9 f581))) (define-fun f590 () Arctic (+ (* f6 f584) (* f7 f585))) (define-fun f591 () Arctic (+ (* f8 f584) (* f9 f585))) (define-fun f592 () Arctic (+ f10 f590)) (define-fun f593 () Arctic (+ f11 f591)) (define-fun f594 () Arctic (+ (* f0 f586) (* f1 f588))) (define-fun f595 () Arctic (+ (* f0 f587) (* f1 f589))) (define-fun f596 () Arctic (+ (* f2 f586) (* f3 f588))) (define-fun f597 () Arctic (+ (* f2 f587) (* f3 f589))) (define-fun f598 () Arctic (+ (* f0 f592) (* f1 f593))) (define-fun f599 () Arctic (+ (* f2 f592) (* f3 f593))) (define-fun f600 () Arctic (+ f4 f598)) (define-fun f601 () Arctic (+ f5 f599)) (define-fun f602 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f603 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f604 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f605 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f606 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f607 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f608 () Arctic (+ f10 f606)) (define-fun f609 () Arctic (+ f11 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 (+ (* f6 f610) (* f7 f612))) (define-fun f619 () Arctic (+ (* f6 f611) (* f7 f613))) (define-fun f620 () Arctic (+ (* f8 f610) (* f9 f612))) (define-fun f621 () Arctic (+ (* f8 f611) (* f9 f613))) (define-fun f622 () Arctic (+ (* f6 f616) (* f7 f617))) (define-fun f623 () Arctic (+ (* f8 f616) (* f9 f617))) (define-fun f624 () Arctic (+ f10 f622)) (define-fun f625 () Arctic (+ f11 f623)) (define-fun f626 () Arctic (+ (* f12 f618) (* f13 f620))) (define-fun f627 () Arctic (+ (* f12 f619) (* f13 f621))) (define-fun f628 () Arctic (+ (* f14 f618) (* f15 f620))) (define-fun f629 () Arctic (+ (* f14 f619) (* f15 f621))) (define-fun f630 () Arctic (+ (* f12 f624) (* f13 f625))) (define-fun f631 () Arctic (+ (* f14 f624) (* f15 f625))) (define-fun f632 () Arctic (+ f16 f630)) (define-fun f633 () Arctic (+ f17 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 (+ (* f0 f634) (* f1 f636))) (define-fun f643 () Arctic (+ (* f0 f635) (* f1 f637))) (define-fun f644 () Arctic (+ (* f2 f634) (* f3 f636))) (define-fun f645 () Arctic (+ (* f2 f635) (* f3 f637))) (define-fun f646 () Arctic (+ (* f0 f640) (* f1 f641))) (define-fun f647 () Arctic (+ (* f2 f640) (* f3 f641))) (define-fun f648 () Arctic (+ f4 f646)) (define-fun f649 () Arctic (+ f5 f647)) (define-fun f650 () Arctic (+ (* f12 f12) (* f13 f14))) (define-fun f651 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f652 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f653 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f654 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f655 () Arctic (+ (* f14 f16) (* f15 f17))) (define-fun f656 () Arctic (+ f16 f654)) (define-fun f657 () Arctic (+ f17 f655)) (define-fun f658 () Arctic (+ (* f12 f650) (* f13 f652))) (define-fun f659 () Arctic (+ (* f12 f651) (* f13 f653))) (define-fun f660 () Arctic (+ (* f14 f650) (* f15 f652))) (define-fun f661 () Arctic (+ (* f14 f651) (* f15 f653))) (define-fun f662 () Arctic (+ (* f12 f656) (* f13 f657))) (define-fun f663 () Arctic (+ (* f14 f656) (* f15 f657))) (define-fun f664 () Arctic (+ f16 f662)) (define-fun f665 () Arctic (+ f17 f663)) (define-fun f666 () Arctic (+ (* f6 f658) (* f7 f660))) (define-fun f667 () Arctic (+ (* f6 f659) (* f7 f661))) (define-fun f668 () Arctic (+ (* f8 f658) (* f9 f660))) (define-fun f669 () Arctic (+ (* f8 f659) (* f9 f661))) (define-fun f670 () Arctic (+ (* f6 f664) (* f7 f665))) (define-fun f671 () Arctic (+ (* f8 f664) (* f9 f665))) (define-fun f672 () Arctic (+ f10 f670)) (define-fun f673 () Arctic (+ f11 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 (+ (* f6 f674) (* f7 f676))) (define-fun f683 () Arctic (+ (* f6 f675) (* f7 f677))) (define-fun f684 () Arctic (+ (* f8 f674) (* f9 f676))) (define-fun f685 () Arctic (+ (* f8 f675) (* f9 f677))) (define-fun f686 () Arctic (+ (* f6 f680) (* f7 f681))) (define-fun f687 () Arctic (+ (* f8 f680) (* f9 f681))) (define-fun f688 () Arctic (+ f10 f686)) (define-fun f689 () Arctic (+ f11 f687)) (define-fun f690 () Arctic (+ (* f0 f682) (* f1 f684))) (define-fun f691 () Arctic (+ (* f0 f683) (* f1 f685))) (define-fun f692 () Arctic (+ (* f2 f682) (* f3 f684))) (define-fun f693 () Arctic (+ (* f2 f683) (* f3 f685))) (define-fun f694 () Arctic (+ (* f0 f688) (* f1 f689))) (define-fun f695 () Arctic (+ (* f2 f688) (* f3 f689))) (define-fun f696 () Arctic (+ f4 f694)) (define-fun f697 () Arctic (+ f5 f695)) (define-fun f698 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f699 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f700 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f701 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f702 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f703 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f704 () Arctic (+ f10 f702)) (define-fun f705 () Arctic (+ f11 f703)) (define-fun f706 () Arctic (+ (* f6 f698) (* f7 f700))) (define-fun f707 () Arctic (+ (* f6 f699) (* f7 f701))) (define-fun f708 () Arctic (+ (* f8 f698) (* f9 f700))) (define-fun f709 () Arctic (+ (* f8 f699) (* f9 f701))) (define-fun f710 () Arctic (+ (* f6 f704) (* f7 f705))) (define-fun f711 () Arctic (+ (* f8 f704) (* f9 f705))) (define-fun f712 () Arctic (+ f10 f710)) (define-fun f713 () Arctic (+ f11 f711)) (define-fun f714 () Arctic (+ (* f6 f706) (* f7 f708))) (define-fun f715 () Arctic (+ (* f6 f707) (* f7 f709))) (define-fun f716 () Arctic (+ (* f8 f706) (* f9 f708))) (define-fun f717 () Arctic (+ (* f8 f707) (* f9 f709))) (define-fun f718 () Arctic (+ (* f6 f712) (* f7 f713))) (define-fun f719 () Arctic (+ (* f8 f712) (* f9 f713))) (define-fun f720 () Arctic (+ f10 f718)) (define-fun f721 () Arctic (+ f11 f719)) (define-fun f722 () Arctic (+ (* f12 f714) (* f13 f716))) (define-fun f723 () Arctic (+ (* f12 f715) (* f13 f717))) (define-fun f724 () Arctic (+ (* f14 f714) (* f15 f716))) (define-fun f725 () Arctic (+ (* f14 f715) (* f15 f717))) (define-fun f726 () Arctic (+ (* f12 f720) (* f13 f721))) (define-fun f727 () Arctic (+ (* f14 f720) (* f15 f721))) (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 (+ (* f0 f730) (* f1 f732))) (define-fun f739 () Arctic (+ (* f0 f731) (* f1 f733))) (define-fun f740 () Arctic (+ (* f2 f730) (* f3 f732))) (define-fun f741 () Arctic (+ (* f2 f731) (* f3 f733))) (define-fun f742 () Arctic (+ (* f0 f736) (* f1 f737))) (define-fun f743 () Arctic (+ (* f2 f736) (* f3 f737))) (define-fun f744 () Arctic (+ f4 f742)) (define-fun f745 () Arctic (+ f5 f743)) (define-fun f746 () Arctic (+ (* f12 f12) (* f13 f14))) (define-fun f747 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f748 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f749 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f750 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f751 () Arctic (+ (* f14 f16) (* f15 f17))) (define-fun f752 () Arctic (+ f16 f750)) (define-fun f753 () Arctic (+ f17 f751)) (define-fun f754 () Arctic (+ (* f0 f746) (* f1 f748))) (define-fun f755 () Arctic (+ (* f0 f747) (* f1 f749))) (define-fun f756 () Arctic (+ (* f2 f746) (* f3 f748))) (define-fun f757 () Arctic (+ (* f2 f747) (* f3 f749))) (define-fun f758 () Arctic (+ (* f0 f752) (* f1 f753))) (define-fun f759 () Arctic (+ (* f2 f752) (* f3 f753))) (define-fun f760 () Arctic (+ f4 f758)) (define-fun f761 () Arctic (+ f5 f759)) (define-fun f762 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f763 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f764 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f765 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f766 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f767 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f768 () Arctic (+ f10 f766)) (define-fun f769 () Arctic (+ f11 f767)) (define-fun f770 () Arctic (+ (* f6 f762) (* f7 f764))) (define-fun f771 () Arctic (+ (* f6 f763) (* f7 f765))) (define-fun f772 () Arctic (+ (* f8 f762) (* f9 f764))) (define-fun f773 () Arctic (+ (* f8 f763) (* f9 f765))) (define-fun f774 () Arctic (+ (* f6 f768) (* f7 f769))) (define-fun f775 () Arctic (+ (* f8 f768) (* f9 f769))) (define-fun f776 () Arctic (+ f10 f774)) (define-fun f777 () Arctic (+ f11 f775)) (define-fun f778 () Arctic (+ (* f6 f770) (* f7 f772))) (define-fun f779 () Arctic (+ (* f6 f771) (* f7 f773))) (define-fun f780 () Arctic (+ (* f8 f770) (* f9 f772))) (define-fun f781 () Arctic (+ (* f8 f771) (* f9 f773))) (define-fun f782 () Arctic (+ (* f6 f776) (* f7 f777))) (define-fun f783 () Arctic (+ (* f8 f776) (* f9 f777))) (define-fun f784 () Arctic (+ f10 f782)) (define-fun f785 () Arctic (+ f11 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 (+ (* f12 f786) (* f13 f788))) (define-fun f795 () Arctic (+ (* f12 f787) (* f13 f789))) (define-fun f796 () Arctic (+ (* f14 f786) (* f15 f788))) (define-fun f797 () Arctic (+ (* f14 f787) (* f15 f789))) (define-fun f798 () Arctic (+ (* f12 f792) (* f13 f793))) (define-fun f799 () Arctic (+ (* f14 f792) (* f15 f793))) (define-fun f800 () Arctic (+ f16 f798)) (define-fun f801 () Arctic (+ f17 f799)) (define-fun f802 () Arctic (+ (* f0 f794) (* f1 f796))) (define-fun f803 () Arctic (+ (* f0 f795) (* f1 f797))) (define-fun f804 () Arctic (+ (* f2 f794) (* f3 f796))) (define-fun f805 () Arctic (+ (* f2 f795) (* f3 f797))) (define-fun f806 () Arctic (+ (* f0 f800) (* f1 f801))) (define-fun f807 () Arctic (+ (* f2 f800) (* f3 f801))) (define-fun f808 () Arctic (+ f4 f806)) (define-fun f809 () Arctic (+ f5 f807)) (define-fun f810 () Arctic (+ (* f0 f12) (* f1 f14))) (define-fun f811 () Arctic (+ (* f0 f13) (* f1 f15))) (define-fun f812 () Arctic (+ (* f2 f12) (* f3 f14))) (define-fun f813 () Arctic (+ (* f2 f13) (* f3 f15))) (define-fun f814 () Arctic (+ (* f0 f16) (* f1 f17))) (define-fun f815 () Arctic (+ (* f2 f16) (* f3 f17))) (define-fun f816 () Arctic (+ f4 f814)) (define-fun f817 () Arctic (+ f5 f815)) (define-fun f818 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f819 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f820 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f821 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f822 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f823 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f824 () Arctic (+ f10 f822)) (define-fun f825 () Arctic (+ f11 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 (+ (* f6 f826) (* f7 f828))) (define-fun f835 () Arctic (+ (* f6 f827) (* f7 f829))) (define-fun f836 () Arctic (+ (* f8 f826) (* f9 f828))) (define-fun f837 () Arctic (+ (* f8 f827) (* f9 f829))) (define-fun f838 () Arctic (+ (* f6 f832) (* f7 f833))) (define-fun f839 () Arctic (+ (* f8 f832) (* f9 f833))) (define-fun f840 () Arctic (+ f10 f838)) (define-fun f841 () Arctic (+ f11 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 (+ (* f0 f850) (* f1 f852))) (define-fun f859 () Arctic (+ (* f0 f851) (* f1 f853))) (define-fun f860 () Arctic (+ (* f2 f850) (* f3 f852))) (define-fun f861 () Arctic (+ (* f2 f851) (* f3 f853))) (define-fun f862 () Arctic (+ (* f0 f856) (* f1 f857))) (define-fun f863 () Arctic (+ (* f2 f856) (* f3 f857))) (define-fun f864 () Arctic (+ f4 f862)) (define-fun f865 () Arctic (+ f5 f863)) (define-fun f866 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f867 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f868 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f869 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f870 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f871 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f872 () Arctic (+ f10 f870)) (define-fun f873 () Arctic (+ f11 f871)) (define-fun f874 () Arctic (+ (* f6 f866) (* f7 f868))) (define-fun f875 () Arctic (+ (* f6 f867) (* f7 f869))) (define-fun f876 () Arctic (+ (* f8 f866) (* f9 f868))) (define-fun f877 () Arctic (+ (* f8 f867) (* f9 f869))) (define-fun f878 () Arctic (+ (* f6 f872) (* f7 f873))) (define-fun f879 () Arctic (+ (* f8 f872) (* f9 f873))) (define-fun f880 () Arctic (+ f10 f878)) (define-fun f881 () Arctic (+ f11 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 (+ (* f0 f882) (* f1 f884))) (define-fun f891 () Arctic (+ (* f0 f883) (* f1 f885))) (define-fun f892 () Arctic (+ (* f2 f882) (* f3 f884))) (define-fun f893 () Arctic (+ (* f2 f883) (* f3 f885))) (define-fun f894 () Arctic (+ (* f0 f888) (* f1 f889))) (define-fun f895 () Arctic (+ (* f2 f888) (* f3 f889))) (define-fun f896 () Arctic (+ f4 f894)) (define-fun f897 () Arctic (+ f5 f895)) (define-fun f898 () Arctic (+ (* f12 f12) (* f13 f14))) (define-fun f899 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f900 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f901 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f902 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f903 () Arctic (+ (* f14 f16) (* f15 f17))) (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 (+ (* f6 f906) (* f7 f908))) (define-fun f915 () Arctic (+ (* f6 f907) (* f7 f909))) (define-fun f916 () Arctic (+ (* f8 f906) (* f9 f908))) (define-fun f917 () Arctic (+ (* f8 f907) (* f9 f909))) (define-fun f918 () Arctic (+ (* f6 f912) (* f7 f913))) (define-fun f919 () Arctic (+ (* f8 f912) (* f9 f913))) (define-fun f920 () Arctic (+ f10 f918)) (define-fun f921 () Arctic (+ f11 f919)) (define-fun f922 () Arctic (+ (* f0 f914) (* f1 f916))) (define-fun f923 () Arctic (+ (* f0 f915) (* f1 f917))) (define-fun f924 () Arctic (+ (* f2 f914) (* f3 f916))) (define-fun f925 () Arctic (+ (* f2 f915) (* f3 f917))) (define-fun f926 () Arctic (+ (* f0 f920) (* f1 f921))) (define-fun f927 () Arctic (+ (* f2 f920) (* f3 f921))) (define-fun f928 () Arctic (+ f4 f926)) (define-fun f929 () Arctic (+ f5 f927)) (define-fun f930 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f931 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f932 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f933 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f934 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f935 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f936 () Arctic (+ f10 f934)) (define-fun f937 () Arctic (+ f11 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 (+ (* f6 f12) (* f7 f14))) (define-fun f947 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f948 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f949 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f950 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f951 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f952 () Arctic (+ f10 f950)) (define-fun f953 () Arctic (+ f11 f951)) (define-fun f954 () Arctic (+ (* f6 f946) (* f7 f948))) (define-fun f955 () Arctic (+ (* f6 f947) (* f7 f949))) (define-fun f956 () Arctic (+ (* f8 f946) (* f9 f948))) (define-fun f957 () Arctic (+ (* f8 f947) (* f9 f949))) (define-fun f958 () Arctic (+ (* f6 f952) (* f7 f953))) (define-fun f959 () Arctic (+ (* f8 f952) (* f9 f953))) (define-fun f960 () Arctic (+ f10 f958)) (define-fun f961 () Arctic (+ f11 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 (+ (* f6 f12) (* f7 f14))) (define-fun f979 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f980 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f981 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f982 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f983 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f984 () Arctic (+ f10 f982)) (define-fun f985 () Arctic (+ f11 f983)) (define-fun f986 () Arctic (+ (* f6 f978) (* f7 f980))) (define-fun f987 () Arctic (+ (* f6 f979) (* f7 f981))) (define-fun f988 () Arctic (+ (* f8 f978) (* f9 f980))) (define-fun f989 () Arctic (+ (* f8 f979) (* f9 f981))) (define-fun f990 () Arctic (+ (* f6 f984) (* f7 f985))) (define-fun f991 () Arctic (+ (* f8 f984) (* f9 f985))) (define-fun f992 () Arctic (+ f10 f990)) (define-fun f993 () Arctic (+ f11 f991)) (define-fun f994 () Arctic (+ (* f6 f986) (* f7 f988))) (define-fun f995 () Arctic (+ (* f6 f987) (* f7 f989))) (define-fun f996 () Arctic (+ (* f8 f986) (* f9 f988))) (define-fun f997 () Arctic (+ (* f8 f987) (* f9 f989))) (define-fun f998 () Arctic (+ (* f6 f992) (* f7 f993))) (define-fun f999 () Arctic (+ (* f8 f992) (* f9 f993))) (define-fun f1000 () Arctic (+ f10 f998)) (define-fun f1001 () Arctic (+ f11 f999)) (define-fun f1002 () Arctic (+ (* f12 f994) (* f13 f996))) (define-fun f1003 () Arctic (+ (* f12 f995) (* f13 f997))) (define-fun f1004 () Arctic (+ (* f14 f994) (* f15 f996))) (define-fun f1005 () Arctic (+ (* f14 f995) (* f15 f997))) (define-fun f1006 () Arctic (+ (* f12 f1000) (* f13 f1001))) (define-fun f1007 () Arctic (+ (* f14 f1000) (* f15 f1001))) (define-fun f1008 () Arctic (+ f16 f1006)) (define-fun f1009 () Arctic (+ f17 f1007)) (define-fun f1010 () Arctic (+ (* f6 f1002) (* f7 f1004))) (define-fun f1011 () Arctic (+ (* f6 f1003) (* f7 f1005))) (define-fun f1012 () Arctic (+ (* f8 f1002) (* f9 f1004))) (define-fun f1013 () Arctic (+ (* f8 f1003) (* f9 f1005))) (define-fun f1014 () Arctic (+ (* f6 f1008) (* f7 f1009))) (define-fun f1015 () Arctic (+ (* f8 f1008) (* f9 f1009))) (define-fun f1016 () Arctic (+ f10 f1014)) (define-fun f1017 () Arctic (+ f11 f1015)) (define-fun f1018 () Arctic (+ (* f6 f1010) (* f7 f1012))) (define-fun f1019 () Arctic (+ (* f6 f1011) (* f7 f1013))) (define-fun f1020 () Arctic (+ (* f8 f1010) (* f9 f1012))) (define-fun f1021 () Arctic (+ (* f8 f1011) (* f9 f1013))) (define-fun f1022 () Arctic (+ (* f6 f1016) (* f7 f1017))) (define-fun f1023 () Arctic (+ (* f8 f1016) (* f9 f1017))) (define-fun f1024 () Arctic (+ f10 f1022)) (define-fun f1025 () Arctic (+ f11 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 (+ (* f6 f12) (* f7 f14))) (define-fun f1035 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f1036 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f1037 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f1038 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f1039 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f1040 () Arctic (+ f10 f1038)) (define-fun f1041 () Arctic (+ f11 f1039)) (define-fun f1042 () Arctic (+ (* f6 f1034) (* f7 f1036))) (define-fun f1043 () Arctic (+ (* f6 f1035) (* f7 f1037))) (define-fun f1044 () Arctic (+ (* f8 f1034) (* f9 f1036))) (define-fun f1045 () Arctic (+ (* f8 f1035) (* f9 f1037))) (define-fun f1046 () Arctic (+ (* f6 f1040) (* f7 f1041))) (define-fun f1047 () Arctic (+ (* f8 f1040) (* f9 f1041))) (define-fun f1048 () Arctic (+ f10 f1046)) (define-fun f1049 () Arctic (+ f11 f1047)) (define-fun f1050 () Arctic (+ (* f12 f1042) (* f13 f1044))) (define-fun f1051 () Arctic (+ (* f12 f1043) (* f13 f1045))) (define-fun f1052 () Arctic (+ (* f14 f1042) (* f15 f1044))) (define-fun f1053 () Arctic (+ (* f14 f1043) (* f15 f1045))) (define-fun f1054 () Arctic (+ (* f12 f1048) (* f13 f1049))) (define-fun f1055 () Arctic (+ (* f14 f1048) (* f15 f1049))) (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 (+ (* f6 f1058) (* f7 f1060))) (define-fun f1067 () Arctic (+ (* f6 f1059) (* f7 f1061))) (define-fun f1068 () Arctic (+ (* f8 f1058) (* f9 f1060))) (define-fun f1069 () Arctic (+ (* f8 f1059) (* f9 f1061))) (define-fun f1070 () Arctic (+ (* f6 f1064) (* f7 f1065))) (define-fun f1071 () Arctic (+ (* f8 f1064) (* f9 f1065))) (define-fun f1072 () Arctic (+ f10 f1070)) (define-fun f1073 () Arctic (+ f11 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 (+ (* f6 f1074) (* f7 f1076))) (define-fun f1083 () Arctic (+ (* f6 f1075) (* f7 f1077))) (define-fun f1084 () Arctic (+ (* f8 f1074) (* f9 f1076))) (define-fun f1085 () Arctic (+ (* f8 f1075) (* f9 f1077))) (define-fun f1086 () Arctic (+ (* f6 f1080) (* f7 f1081))) (define-fun f1087 () Arctic (+ (* f8 f1080) (* f9 f1081))) (define-fun f1088 () Arctic (+ f10 f1086)) (define-fun f1089 () Arctic (+ f11 f1087)) (define-fun f1090 () Arctic (+ (* f6 f1082) (* f7 f1084))) (define-fun f1091 () Arctic (+ (* f6 f1083) (* f7 f1085))) (define-fun f1092 () Arctic (+ (* f8 f1082) (* f9 f1084))) (define-fun f1093 () Arctic (+ (* f8 f1083) (* f9 f1085))) (define-fun f1094 () Arctic (+ (* f6 f1088) (* f7 f1089))) (define-fun f1095 () Arctic (+ (* f8 f1088) (* f9 f1089))) (define-fun f1096 () Arctic (+ f10 f1094)) (define-fun f1097 () Arctic (+ f11 f1095)) (define-fun f1098 () Arctic (+ (* f6 f1090) (* f7 f1092))) (define-fun f1099 () Arctic (+ (* f6 f1091) (* f7 f1093))) (define-fun f1100 () Arctic (+ (* f8 f1090) (* f9 f1092))) (define-fun f1101 () Arctic (+ (* f8 f1091) (* f9 f1093))) (define-fun f1102 () Arctic (+ (* f6 f1096) (* f7 f1097))) (define-fun f1103 () Arctic (+ (* f8 f1096) (* f9 f1097))) (define-fun f1104 () Arctic (+ f10 f1102)) (define-fun f1105 () Arctic (+ f11 f1103)) (define-fun f1106 () Arctic (+ (* f12 f1098) (* f13 f1100))) (define-fun f1107 () Arctic (+ (* f12 f1099) (* f13 f1101))) (define-fun f1108 () Arctic (+ (* f14 f1098) (* f15 f1100))) (define-fun f1109 () Arctic (+ (* f14 f1099) (* f15 f1101))) (define-fun f1110 () Arctic (+ (* f12 f1104) (* f13 f1105))) (define-fun f1111 () Arctic (+ (* f14 f1104) (* f15 f1105))) (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 f12) (* f7 f14))) (define-fun f1123 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f1124 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f1125 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f1126 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f1127 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f1128 () Arctic (+ f10 f1126)) (define-fun f1129 () Arctic (+ f11 f1127)) (define-fun f1130 () Arctic (+ (* f6 f1122) (* f7 f1124))) (define-fun f1131 () Arctic (+ (* f6 f1123) (* f7 f1125))) (define-fun f1132 () Arctic (+ (* f8 f1122) (* f9 f1124))) (define-fun f1133 () Arctic (+ (* f8 f1123) (* f9 f1125))) (define-fun f1134 () Arctic (+ (* f6 f1128) (* f7 f1129))) (define-fun f1135 () Arctic (+ (* f8 f1128) (* f9 f1129))) (define-fun f1136 () Arctic (+ f10 f1134)) (define-fun f1137 () Arctic (+ f11 f1135)) (define-fun f1138 () Arctic (+ (* f6 f1130) (* f7 f1132))) (define-fun f1139 () Arctic (+ (* f6 f1131) (* f7 f1133))) (define-fun f1140 () Arctic (+ (* f8 f1130) (* f9 f1132))) (define-fun f1141 () Arctic (+ (* f8 f1131) (* f9 f1133))) (define-fun f1142 () Arctic (+ (* f6 f1136) (* f7 f1137))) (define-fun f1143 () Arctic (+ (* f8 f1136) (* f9 f1137))) (define-fun f1144 () Arctic (+ f10 f1142)) (define-fun f1145 () Arctic (+ f11 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 (+ (* f6 f1146) (* f7 f1148))) (define-fun f1155 () Arctic (+ (* f6 f1147) (* f7 f1149))) (define-fun f1156 () Arctic (+ (* f8 f1146) (* f9 f1148))) (define-fun f1157 () Arctic (+ (* f8 f1147) (* f9 f1149))) (define-fun f1158 () Arctic (+ (* f6 f1152) (* f7 f1153))) (define-fun f1159 () Arctic (+ (* f8 f1152) (* f9 f1153))) (define-fun f1160 () Arctic (+ f10 f1158)) (define-fun f1161 () Arctic (+ f11 f1159)) (define-fun f1162 () Arctic (+ (* f6 f1154) (* f7 f1156))) (define-fun f1163 () Arctic (+ (* f6 f1155) (* f7 f1157))) (define-fun f1164 () Arctic (+ (* f8 f1154) (* f9 f1156))) (define-fun f1165 () Arctic (+ (* f8 f1155) (* f9 f1157))) (define-fun f1166 () Arctic (+ (* f6 f1160) (* f7 f1161))) (define-fun f1167 () Arctic (+ (* f8 f1160) (* f9 f1161))) (define-fun f1168 () Arctic (+ f10 f1166)) (define-fun f1169 () Arctic (+ f11 f1167)) (define-fun f1170 () Arctic (+ (* f6 f1162) (* f7 f1164))) (define-fun f1171 () Arctic (+ (* f6 f1163) (* f7 f1165))) (define-fun f1172 () Arctic (+ (* f8 f1162) (* f9 f1164))) (define-fun f1173 () Arctic (+ (* f8 f1163) (* f9 f1165))) (define-fun f1174 () Arctic (+ (* f6 f1168) (* f7 f1169))) (define-fun f1175 () Arctic (+ (* f8 f1168) (* f9 f1169))) (define-fun f1176 () Arctic (+ f10 f1174)) (define-fun f1177 () Arctic (+ f11 f1175)) (define-fun f1178 () Arctic (+ (* f12 f1170) (* f13 f1172))) (define-fun f1179 () Arctic (+ (* f12 f1171) (* f13 f1173))) (define-fun f1180 () Arctic (+ (* f14 f1170) (* f15 f1172))) (define-fun f1181 () Arctic (+ (* f14 f1171) (* f15 f1173))) (define-fun f1182 () Arctic (+ (* f12 f1176) (* f13 f1177))) (define-fun f1183 () Arctic (+ (* f14 f1176) (* f15 f1177))) (define-fun f1184 () Arctic (+ f16 f1182)) (define-fun f1185 () Arctic (+ f17 f1183)) (define-fun f1186 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f1187 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f1188 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f1189 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f1190 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f1191 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f1192 () Arctic (+ f10 f1190)) (define-fun f1193 () Arctic (+ f11 f1191)) (define-fun f1194 () Arctic (+ (* f6 f1186) (* f7 f1188))) (define-fun f1195 () Arctic (+ (* f6 f1187) (* f7 f1189))) (define-fun f1196 () Arctic (+ (* f8 f1186) (* f9 f1188))) (define-fun f1197 () Arctic (+ (* f8 f1187) (* f9 f1189))) (define-fun f1198 () Arctic (+ (* f6 f1192) (* f7 f1193))) (define-fun f1199 () Arctic (+ (* f8 f1192) (* f9 f1193))) (define-fun f1200 () Arctic (+ f10 f1198)) (define-fun f1201 () Arctic (+ f11 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 (+ (* f12 f12) (* f13 f14))) (define-fun f1235 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f1236 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f1237 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f1238 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f1239 () Arctic (+ (* f14 f16) (* f15 f17))) (define-fun f1240 () Arctic (+ f16 f1238)) (define-fun f1241 () Arctic (+ f17 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 (+ (* f6 f1242) (* f7 f1244))) (define-fun f1251 () Arctic (+ (* f6 f1243) (* f7 f1245))) (define-fun f1252 () Arctic (+ (* f8 f1242) (* f9 f1244))) (define-fun f1253 () Arctic (+ (* f8 f1243) (* f9 f1245))) (define-fun f1254 () Arctic (+ (* f6 f1248) (* f7 f1249))) (define-fun f1255 () Arctic (+ (* f8 f1248) (* f9 f1249))) (define-fun f1256 () Arctic (+ f10 f1254)) (define-fun f1257 () Arctic (+ f11 f1255)) (define-fun f1258 () Arctic (+ (* f6 f1250) (* f7 f1252))) (define-fun f1259 () Arctic (+ (* f6 f1251) (* f7 f1253))) (define-fun f1260 () Arctic (+ (* f8 f1250) (* f9 f1252))) (define-fun f1261 () Arctic (+ (* f8 f1251) (* f9 f1253))) (define-fun f1262 () Arctic (+ (* f6 f1256) (* f7 f1257))) (define-fun f1263 () Arctic (+ (* f8 f1256) (* f9 f1257))) (define-fun f1264 () Arctic (+ f10 f1262)) (define-fun f1265 () Arctic (+ f11 f1263)) (define-fun f1266 () Arctic (+ (* f6 f1258) (* f7 f1260))) (define-fun f1267 () Arctic (+ (* f6 f1259) (* f7 f1261))) (define-fun f1268 () Arctic (+ (* f8 f1258) (* f9 f1260))) (define-fun f1269 () Arctic (+ (* f8 f1259) (* f9 f1261))) (define-fun f1270 () Arctic (+ (* f6 f1264) (* f7 f1265))) (define-fun f1271 () Arctic (+ (* f8 f1264) (* f9 f1265))) (define-fun f1272 () Arctic (+ f10 f1270)) (define-fun f1273 () Arctic (+ f11 f1271)) (define-fun f1274 () Arctic (+ (* f12 f1266) (* f13 f1268))) (define-fun f1275 () Arctic (+ (* f12 f1267) (* f13 f1269))) (define-fun f1276 () Arctic (+ (* f14 f1266) (* f15 f1268))) (define-fun f1277 () Arctic (+ (* f14 f1267) (* f15 f1269))) (define-fun f1278 () Arctic (+ (* f12 f1272) (* f13 f1273))) (define-fun f1279 () Arctic (+ (* f14 f1272) (* f15 f1273))) (define-fun f1280 () Arctic (+ f16 f1278)) (define-fun f1281 () Arctic (+ f17 f1279)) (define-fun f1282 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f1283 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f1284 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f1285 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f1286 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f1287 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f1288 () Arctic (+ f10 f1286)) (define-fun f1289 () Arctic (+ f11 f1287)) (define-fun f1290 () Arctic (+ (* f6 f1282) (* f7 f1284))) (define-fun f1291 () Arctic (+ (* f6 f1283) (* f7 f1285))) (define-fun f1292 () Arctic (+ (* f8 f1282) (* f9 f1284))) (define-fun f1293 () Arctic (+ (* f8 f1283) (* f9 f1285))) (define-fun f1294 () Arctic (+ (* f6 f1288) (* f7 f1289))) (define-fun f1295 () Arctic (+ (* f8 f1288) (* f9 f1289))) (define-fun f1296 () Arctic (+ f10 f1294)) (define-fun f1297 () Arctic (+ f11 f1295)) (define-fun f1298 () Arctic (+ (* f12 f1290) (* f13 f1292))) (define-fun f1299 () Arctic (+ (* f12 f1291) (* f13 f1293))) (define-fun f1300 () Arctic (+ (* f14 f1290) (* f15 f1292))) (define-fun f1301 () Arctic (+ (* f14 f1291) (* f15 f1293))) (define-fun f1302 () Arctic (+ (* f12 f1296) (* f13 f1297))) (define-fun f1303 () Arctic (+ (* f14 f1296) (* f15 f1297))) (define-fun f1304 () Arctic (+ f16 f1302)) (define-fun f1305 () Arctic (+ f17 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 f12) (* f13 f14))) (define-fun f1315 () Arctic (+ (* f12 f13) (* f13 f15))) (define-fun f1316 () Arctic (+ (* f14 f12) (* f15 f14))) (define-fun f1317 () Arctic (+ (* f14 f13) (* f15 f15))) (define-fun f1318 () Arctic (+ (* f12 f16) (* f13 f17))) (define-fun f1319 () Arctic (+ (* f14 f16) (* f15 f17))) (define-fun f1320 () Arctic (+ f16 f1318)) (define-fun f1321 () Arctic (+ f17 f1319)) (define-fun f1322 () Arctic (+ (* f6 f1314) (* f7 f1316))) (define-fun f1323 () Arctic (+ (* f6 f1315) (* f7 f1317))) (define-fun f1324 () Arctic (+ (* f8 f1314) (* f9 f1316))) (define-fun f1325 () Arctic (+ (* f8 f1315) (* f9 f1317))) (define-fun f1326 () Arctic (+ (* f6 f1320) (* f7 f1321))) (define-fun f1327 () Arctic (+ (* f8 f1320) (* f9 f1321))) (define-fun f1328 () Arctic (+ f10 f1326)) (define-fun f1329 () Arctic (+ f11 f1327)) (define-fun f1330 () Arctic (+ (* f6 f1322) (* f7 f1324))) (define-fun f1331 () Arctic (+ (* f6 f1323) (* f7 f1325))) (define-fun f1332 () Arctic (+ (* f8 f1322) (* f9 f1324))) (define-fun f1333 () Arctic (+ (* f8 f1323) (* f9 f1325))) (define-fun f1334 () Arctic (+ (* f6 f1328) (* f7 f1329))) (define-fun f1335 () Arctic (+ (* f8 f1328) (* f9 f1329))) (define-fun f1336 () Arctic (+ f10 f1334)) (define-fun f1337 () Arctic (+ f11 f1335)) (define-fun f1338 () Arctic (+ (* f12 f1330) (* f13 f1332))) (define-fun f1339 () Arctic (+ (* f12 f1331) (* f13 f1333))) (define-fun f1340 () Arctic (+ (* f14 f1330) (* f15 f1332))) (define-fun f1341 () Arctic (+ (* f14 f1331) (* f15 f1333))) (define-fun f1342 () Arctic (+ (* f12 f1336) (* f13 f1337))) (define-fun f1343 () Arctic (+ (* f14 f1336) (* f15 f1337))) (define-fun f1344 () Arctic (+ f16 f1342)) (define-fun f1345 () Arctic (+ f17 f1343)) (define-fun f1346 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f1347 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f1348 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f1349 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f1350 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f1351 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f1352 () Arctic (+ f10 f1350)) (define-fun f1353 () Arctic (+ f11 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 (+ (* f6 f1354) (* f7 f1356))) (define-fun f1363 () Arctic (+ (* f6 f1355) (* f7 f1357))) (define-fun f1364 () Arctic (+ (* f8 f1354) (* f9 f1356))) (define-fun f1365 () Arctic (+ (* f8 f1355) (* f9 f1357))) (define-fun f1366 () Arctic (+ (* f6 f1360) (* f7 f1361))) (define-fun f1367 () Arctic (+ (* f8 f1360) (* f9 f1361))) (define-fun f1368 () Arctic (+ f10 f1366)) (define-fun f1369 () Arctic (+ f11 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 (+ (* f6 f12) (* f7 f14))) (define-fun f1395 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f1396 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f1397 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f1398 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f1399 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f1400 () Arctic (+ f10 f1398)) (define-fun f1401 () Arctic (+ f11 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 (+ (* f6 f1402) (* f7 f1404))) (define-fun f1411 () Arctic (+ (* f6 f1403) (* f7 f1405))) (define-fun f1412 () Arctic (+ (* f8 f1402) (* f9 f1404))) (define-fun f1413 () Arctic (+ (* f8 f1403) (* f9 f1405))) (define-fun f1414 () Arctic (+ (* f6 f1408) (* f7 f1409))) (define-fun f1415 () Arctic (+ (* f8 f1408) (* f9 f1409))) (define-fun f1416 () Arctic (+ f10 f1414)) (define-fun f1417 () Arctic (+ f11 f1415)) (define-fun f1418 () Arctic (+ (* f6 f1410) (* f7 f1412))) (define-fun f1419 () Arctic (+ (* f6 f1411) (* f7 f1413))) (define-fun f1420 () Arctic (+ (* f8 f1410) (* f9 f1412))) (define-fun f1421 () Arctic (+ (* f8 f1411) (* f9 f1413))) (define-fun f1422 () Arctic (+ (* f6 f1416) (* f7 f1417))) (define-fun f1423 () Arctic (+ (* f8 f1416) (* f9 f1417))) (define-fun f1424 () Arctic (+ f10 f1422)) (define-fun f1425 () Arctic (+ f11 f1423)) (define-fun f1426 () Arctic (+ (* f6 f1418) (* f7 f1420))) (define-fun f1427 () Arctic (+ (* f6 f1419) (* f7 f1421))) (define-fun f1428 () Arctic (+ (* f8 f1418) (* f9 f1420))) (define-fun f1429 () Arctic (+ (* f8 f1419) (* f9 f1421))) (define-fun f1430 () Arctic (+ (* f6 f1424) (* f7 f1425))) (define-fun f1431 () Arctic (+ (* f8 f1424) (* f9 f1425))) (define-fun f1432 () Arctic (+ f10 f1430)) (define-fun f1433 () Arctic (+ f11 f1431)) (define-fun f1434 () Arctic (+ (* f12 f1426) (* f13 f1428))) (define-fun f1435 () Arctic (+ (* f12 f1427) (* f13 f1429))) (define-fun f1436 () Arctic (+ (* f14 f1426) (* f15 f1428))) (define-fun f1437 () Arctic (+ (* f14 f1427) (* f15 f1429))) (define-fun f1438 () Arctic (+ (* f12 f1432) (* f13 f1433))) (define-fun f1439 () Arctic (+ (* f14 f1432) (* f15 f1433))) (define-fun f1440 () Arctic (+ f16 f1438)) (define-fun f1441 () Arctic (+ f17 f1439)) (assert (and (and (and (and (>= f26 f58) (>= f27 f59)) (and (>= f28 f60) (>= f29 f61))) (and (and (>= f32 f64)) (and (>= f33 f65)))) (and (and (and (>= f74 f0) (>= f75 f1)) (and (>= f76 f2) (>= f77 f3))) (and (and (>= f80 f4)) (and (>= f81 f5)))) (and (and (and (>= f130 f218) (>= f131 f219)) (and (>= f132 f220) (>= f133 f221))) (and (and (>= f136 f224)) (and (>= f137 f225)))) (and (and (and (>= f274 f354) (>= f275 f355)) (and (>= f276 f356) (>= f277 f357))) (and (and (>= f280 f360)) (and (>= f281 f361)))) (and (and (and (>= f410 f458) (>= f411 f459)) (and (>= f412 f460) (>= f413 f461))) (and (and (>= f416 f464)) (and (>= f417 f465)))) (and (and (and (>= f514 f538) (>= f515 f539)) (and (>= f516 f540) (>= f517 f541))) (and (and (>= f520 f544)) (and (>= f521 f545)))) (and (and (and (>= f594 f0) (>= f595 f1)) (and (>= f596 f2) (>= f597 f3))) (and (and (>= f600 f4)) (and (>= f601 f5)))) (and (and (and (>= f642 f690) (>= f643 f691)) (and (>= f644 f692) (>= f645 f693))) (and (and (>= f648 f696)) (and (>= f649 f697)))) (and (and (and (>= f738 f754) (>= f739 f755)) (and (>= f740 f756) (>= f741 f757))) (and (and (>= f744 f760)) (and (>= f745 f761)))) (and (and (and (>= f802 f810) (>= f803 f811)) (and (>= f804 f812) (>= f805 f813))) (and (and (>= f808 f816)) (and (>= f809 f817)))) (and (and (and (>= f858 f0) (>= f859 f1)) (and (>= f860 f2) (>= f861 f3))) (and (and (>= f864 f4)) (and (>= f865 f5)))) (and (and (and (>= f890 f0) (>= f891 f1)) (and (>= f892 f2) (>= f893 f3))) (and (and (>= f896 f4)) (and (>= f897 f5)))) (and (and (and (>= f922 f0) (>= f923 f1)) (and (>= f924 f2) (>= f925 f3))) (and (and (>= f928 f4)) (and (>= f929 f5)))) (and (and (and (>= f938 f970) (>= f939 f971)) (and (>= f940 f972) (>= f941 f973))) (and (and (>= f944 f976)) (and (>= f945 f977)))) (and (and (and (>= f1026 f1114) (>= f1027 f1115)) (and (>= f1028 f1116) (>= f1029 f1117))) (and (and (>= f1032 f1120)) (and (>= f1033 f1121)))) (and (and (and (>= f1178 f12) (>= f1179 f13)) (and (>= f1180 f14) (>= f1181 f15))) (and (and (>= f1184 f16)) (and (>= f1185 f17)))) (and (and (and (>= f1226 f1274) (>= f1227 f1275)) (and (>= f1228 f1276) (>= f1229 f1277))) (and (and (>= f1232 f1280)) (and (>= f1233 f1281)))) (and (and (and (>= f1306 f12) (>= f1307 f13)) (and (>= f1308 f14) (>= f1309 f15))) (and (and (>= f1312 f16)) (and (>= f1313 f17)))) (and (and (and (>= f1338 f12) (>= f1339 f13)) (and (>= f1340 f14) (>= f1341 f15))) (and (and (>= f1344 f16)) (and (>= f1345 f17)))) (and (and (and (>= f1386 f12) (>= f1387 f13)) (and (>= f1388 f14) (>= f1389 f15))) (and (and (>= f1392 f16)) (and (>= f1393 f17)))) (and (and (and (>= f1434 f12) (>= f1435 f13)) (and (>= f1436 f14) (>= f1437 f15))) (and (and (>= f1440 f16)) (and (>= f1441 f17)))))) (assert (or (and (and (and (>> f26 f58) (>> f27 f59)) (and (>> f28 f60) (>> f29 f61))) (and (and (>> f32 f64)) (and (>> f33 f65)))) (and (and (and (>> f74 f0) (>> f75 f1)) (and (>> f76 f2) (>> f77 f3))) (and (and (>> f80 f4)) (and (>> f81 f5)))) (and (and (and (>> f130 f218) (>> f131 f219)) (and (>> f132 f220) (>> f133 f221))) (and (and (>> f136 f224)) (and (>> f137 f225)))) (and (and (and (>> f274 f354) (>> f275 f355)) (and (>> f276 f356) (>> f277 f357))) (and (and (>> f280 f360)) (and (>> f281 f361)))) (and (and (and (>> f410 f458) (>> f411 f459)) (and (>> f412 f460) (>> f413 f461))) (and (and (>> f416 f464)) (and (>> f417 f465)))) (and (and (and (>> f514 f538) (>> f515 f539)) (and (>> f516 f540) (>> f517 f541))) (and (and (>> f520 f544)) (and (>> f521 f545)))) (and (and (and (>> f594 f0) (>> f595 f1)) (and (>> f596 f2) (>> f597 f3))) (and (and (>> f600 f4)) (and (>> f601 f5)))) (and (and (and (>> f642 f690) (>> f643 f691)) (and (>> f644 f692) (>> f645 f693))) (and (and (>> f648 f696)) (and (>> f649 f697)))) (and (and (and (>> f738 f754) (>> f739 f755)) (and (>> f740 f756) (>> f741 f757))) (and (and (>> f744 f760)) (and (>> f745 f761)))) (and (and (and (>> f802 f810) (>> f803 f811)) (and (>> f804 f812) (>> f805 f813))) (and (and (>> f808 f816)) (and (>> f809 f817)))) (and (and (and (>> f858 f0) (>> f859 f1)) (and (>> f860 f2) (>> f861 f3))) (and (and (>> f864 f4)) (and (>> f865 f5)))) (and (and (and (>> f890 f0) (>> f891 f1)) (and (>> f892 f2) (>> f893 f3))) (and (and (>> f896 f4)) (and (>> f897 f5)))) (and (and (and (>> f922 f0) (>> f923 f1)) (and (>> f924 f2) (>> f925 f3))) (and (and (>> f928 f4)) (and (>> f929 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))