(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES b# b b b a b b a b b -> b# b a b b a b b b b b, b# b b b a b b a b b -> b# b a b b b b b, b# b b b a b b a b b -> b# b b b b, b# b b b a b b a b b -> b# b b b, b# b b b a b b a b b -> b# b b, b# b b b a b b a b b -> b# b, b# b b b a b b a b b -> b#, b b b b a b b a b b ->= b a b b a b b a b b b 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 (+ (* f6 f6) (* f7 f8))) (define-fun f19 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f20 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f21 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f22 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f23 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f24 () Arctic (+ f10 f22)) (define-fun f25 () Arctic (+ f11 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 (+ (* 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 (+ (* f12 f42) (* f13 f44))) (define-fun f51 () Arctic (+ (* f12 f43) (* f13 f45))) (define-fun f52 () Arctic (+ (* f14 f42) (* f15 f44))) (define-fun f53 () Arctic (+ (* f14 f43) (* f15 f45))) (define-fun f54 () Arctic (+ (* f12 f48) (* f13 f49))) (define-fun f55 () Arctic (+ (* f14 f48) (* f15 f49))) (define-fun f56 () Arctic (+ f16 f54)) (define-fun f57 () Arctic (+ f17 f55)) (define-fun f58 () Arctic (+ (* f6 f50) (* f7 f52))) (define-fun f59 () Arctic (+ (* f6 f51) (* f7 f53))) (define-fun f60 () Arctic (+ (* f8 f50) (* f9 f52))) (define-fun f61 () Arctic (+ (* f8 f51) (* f9 f53))) (define-fun f62 () Arctic (+ (* f6 f56) (* f7 f57))) (define-fun f63 () Arctic (+ (* f8 f56) (* f9 f57))) (define-fun f64 () Arctic (+ f10 f62)) (define-fun f65 () Arctic (+ f11 f63)) (define-fun f66 () Arctic (+ (* f6 f58) (* f7 f60))) (define-fun f67 () Arctic (+ (* f6 f59) (* f7 f61))) (define-fun f68 () Arctic (+ (* f8 f58) (* f9 f60))) (define-fun f69 () Arctic (+ (* f8 f59) (* f9 f61))) (define-fun f70 () Arctic (+ (* f6 f64) (* f7 f65))) (define-fun f71 () Arctic (+ (* f8 f64) (* f9 f65))) (define-fun f72 () Arctic (+ f10 f70)) (define-fun f73 () Arctic (+ f11 f71)) (define-fun f74 () Arctic (+ (* f6 f66) (* f7 f68))) (define-fun f75 () Arctic (+ (* f6 f67) (* f7 f69))) (define-fun f76 () Arctic (+ (* f8 f66) (* f9 f68))) (define-fun f77 () Arctic (+ (* f8 f67) (* f9 f69))) (define-fun f78 () Arctic (+ (* f6 f72) (* f7 f73))) (define-fun f79 () Arctic (+ (* f8 f72) (* f9 f73))) (define-fun f80 () Arctic (+ f10 f78)) (define-fun f81 () Arctic (+ f11 f79)) (define-fun f82 () Arctic (+ (* f0 f74) (* f1 f76))) (define-fun f83 () Arctic (+ (* f0 f75) (* f1 f77))) (define-fun f84 () Arctic (+ (* f2 f74) (* f3 f76))) (define-fun f85 () Arctic (+ (* f2 f75) (* f3 f77))) (define-fun f86 () Arctic (+ (* f0 f80) (* f1 f81))) (define-fun f87 () Arctic (+ (* f2 f80) (* f3 f81))) (define-fun f88 () Arctic (+ f4 f86)) (define-fun f89 () Arctic (+ f5 f87)) (define-fun f90 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f91 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f92 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f93 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f94 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f95 () Arctic (+ (* f8 f10) (* f9 f11))) (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 (+ (* f6 f98) (* f7 f100))) (define-fun f107 () Arctic (+ (* f6 f99) (* f7 f101))) (define-fun f108 () Arctic (+ (* f8 f98) (* f9 f100))) (define-fun f109 () Arctic (+ (* f8 f99) (* f9 f101))) (define-fun f110 () Arctic (+ (* f6 f104) (* f7 f105))) (define-fun f111 () Arctic (+ (* f8 f104) (* f9 f105))) (define-fun f112 () Arctic (+ f10 f110)) (define-fun f113 () Arctic (+ f11 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 (+ (* f12 f114) (* f13 f116))) (define-fun f123 () Arctic (+ (* f12 f115) (* f13 f117))) (define-fun f124 () Arctic (+ (* f14 f114) (* f15 f116))) (define-fun f125 () Arctic (+ (* f14 f115) (* f15 f117))) (define-fun f126 () Arctic (+ (* f12 f120) (* f13 f121))) (define-fun f127 () Arctic (+ (* f14 f120) (* f15 f121))) (define-fun f128 () Arctic (+ f16 f126)) (define-fun f129 () Arctic (+ f17 f127)) (define-fun f130 () Arctic (+ (* f6 f122) (* f7 f124))) (define-fun f131 () Arctic (+ (* f6 f123) (* f7 f125))) (define-fun f132 () Arctic (+ (* f8 f122) (* f9 f124))) (define-fun f133 () Arctic (+ (* f8 f123) (* f9 f125))) (define-fun f134 () Arctic (+ (* f6 f128) (* f7 f129))) (define-fun f135 () Arctic (+ (* f8 f128) (* f9 f129))) (define-fun f136 () Arctic (+ f10 f134)) (define-fun f137 () Arctic (+ f11 f135)) (define-fun f138 () Arctic (+ (* f6 f130) (* f7 f132))) (define-fun f139 () Arctic (+ (* f6 f131) (* f7 f133))) (define-fun f140 () Arctic (+ (* f8 f130) (* f9 f132))) (define-fun f141 () Arctic (+ (* f8 f131) (* f9 f133))) (define-fun f142 () Arctic (+ (* f6 f136) (* f7 f137))) (define-fun f143 () Arctic (+ (* f8 f136) (* f9 f137))) (define-fun f144 () Arctic (+ f10 f142)) (define-fun f145 () Arctic (+ f11 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 (+ (* f6 f146) (* f7 f148))) (define-fun f155 () Arctic (+ (* f6 f147) (* f7 f149))) (define-fun f156 () Arctic (+ (* f8 f146) (* f9 f148))) (define-fun f157 () Arctic (+ (* f8 f147) (* f9 f149))) (define-fun f158 () Arctic (+ (* f6 f152) (* f7 f153))) (define-fun f159 () Arctic (+ (* f8 f152) (* f9 f153))) (define-fun f160 () Arctic (+ f10 f158)) (define-fun f161 () Arctic (+ f11 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 (+ (* f6 f6) (* f7 f8))) (define-fun f171 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f172 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f173 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f174 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f175 () Arctic (+ (* f8 f10) (* f9 f11))) (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 (+ (* f12 f194) (* f13 f196))) (define-fun f203 () Arctic (+ (* f12 f195) (* f13 f197))) (define-fun f204 () Arctic (+ (* f14 f194) (* f15 f196))) (define-fun f205 () Arctic (+ (* f14 f195) (* f15 f197))) (define-fun f206 () Arctic (+ (* f12 f200) (* f13 f201))) (define-fun f207 () Arctic (+ (* f14 f200) (* f15 f201))) (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 (+ (* f6 f210) (* f7 f212))) (define-fun f219 () Arctic (+ (* f6 f211) (* f7 f213))) (define-fun f220 () Arctic (+ (* f8 f210) (* f9 f212))) (define-fun f221 () Arctic (+ (* f8 f211) (* f9 f213))) (define-fun f222 () Arctic (+ (* f6 f216) (* f7 f217))) (define-fun f223 () Arctic (+ (* f8 f216) (* f9 f217))) (define-fun f224 () Arctic (+ f10 f222)) (define-fun f225 () Arctic (+ f11 f223)) (define-fun f226 () Arctic (+ (* f6 f218) (* f7 f220))) (define-fun f227 () Arctic (+ (* f6 f219) (* f7 f221))) (define-fun f228 () Arctic (+ (* f8 f218) (* f9 f220))) (define-fun f229 () Arctic (+ (* f8 f219) (* f9 f221))) (define-fun f230 () Arctic (+ (* f6 f224) (* f7 f225))) (define-fun f231 () Arctic (+ (* f8 f224) (* f9 f225))) (define-fun f232 () Arctic (+ f10 f230)) (define-fun f233 () Arctic (+ f11 f231)) (define-fun f234 () Arctic (+ (* f0 f226) (* f1 f228))) (define-fun f235 () Arctic (+ (* f0 f227) (* f1 f229))) (define-fun f236 () Arctic (+ (* f2 f226) (* f3 f228))) (define-fun f237 () Arctic (+ (* f2 f227) (* f3 f229))) (define-fun f238 () Arctic (+ (* f0 f232) (* f1 f233))) (define-fun f239 () Arctic (+ (* f2 f232) (* f3 f233))) (define-fun f240 () Arctic (+ f4 f238)) (define-fun f241 () Arctic (+ f5 f239)) (define-fun f242 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f243 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f244 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f245 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f246 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f247 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f248 () Arctic (+ f10 f246)) (define-fun f249 () Arctic (+ f11 f247)) (define-fun f250 () Arctic (+ (* f6 f242) (* f7 f244))) (define-fun f251 () Arctic (+ (* f6 f243) (* f7 f245))) (define-fun f252 () Arctic (+ (* f8 f242) (* f9 f244))) (define-fun f253 () Arctic (+ (* f8 f243) (* f9 f245))) (define-fun f254 () Arctic (+ (* f6 f248) (* f7 f249))) (define-fun f255 () Arctic (+ (* f8 f248) (* f9 f249))) (define-fun f256 () Arctic (+ f10 f254)) (define-fun f257 () Arctic (+ f11 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 (+ (* 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 (+ (* f6 f274) (* f7 f276))) (define-fun f283 () Arctic (+ (* f6 f275) (* f7 f277))) (define-fun f284 () Arctic (+ (* f8 f274) (* f9 f276))) (define-fun f285 () Arctic (+ (* f8 f275) (* f9 f277))) (define-fun f286 () Arctic (+ (* f6 f280) (* f7 f281))) (define-fun f287 () Arctic (+ (* f8 f280) (* f9 f281))) (define-fun f288 () Arctic (+ f10 f286)) (define-fun f289 () Arctic (+ f11 f287)) (define-fun f290 () Arctic (+ (* f0 f282) (* f1 f284))) (define-fun f291 () Arctic (+ (* f0 f283) (* f1 f285))) (define-fun f292 () Arctic (+ (* f2 f282) (* f3 f284))) (define-fun f293 () Arctic (+ (* f2 f283) (* f3 f285))) (define-fun f294 () Arctic (+ (* f0 f288) (* f1 f289))) (define-fun f295 () Arctic (+ (* f2 f288) (* f3 f289))) (define-fun f296 () Arctic (+ f4 f294)) (define-fun f297 () Arctic (+ f5 f295)) (define-fun f298 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f299 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f300 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f301 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f302 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f303 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f304 () Arctic (+ f10 f302)) (define-fun f305 () Arctic (+ f11 f303)) (define-fun f306 () Arctic (+ (* f12 f298) (* f13 f300))) (define-fun f307 () Arctic (+ (* f12 f299) (* f13 f301))) (define-fun f308 () Arctic (+ (* f14 f298) (* f15 f300))) (define-fun f309 () Arctic (+ (* f14 f299) (* f15 f301))) (define-fun f310 () Arctic (+ (* f12 f304) (* f13 f305))) (define-fun f311 () Arctic (+ (* f14 f304) (* f15 f305))) (define-fun f312 () Arctic (+ f16 f310)) (define-fun f313 () Arctic (+ f17 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 (+ (* f6 f314) (* f7 f316))) (define-fun f323 () Arctic (+ (* f6 f315) (* f7 f317))) (define-fun f324 () Arctic (+ (* f8 f314) (* f9 f316))) (define-fun f325 () Arctic (+ (* f8 f315) (* f9 f317))) (define-fun f326 () Arctic (+ (* f6 f320) (* f7 f321))) (define-fun f327 () Arctic (+ (* f8 f320) (* f9 f321))) (define-fun f328 () Arctic (+ f10 f326)) (define-fun f329 () Arctic (+ f11 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 (+ (* 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 (+ (* f6 f346) (* f7 f348))) (define-fun f355 () Arctic (+ (* f6 f347) (* f7 f349))) (define-fun f356 () Arctic (+ (* f8 f346) (* f9 f348))) (define-fun f357 () Arctic (+ (* f8 f347) (* f9 f349))) (define-fun f358 () Arctic (+ (* f6 f352) (* f7 f353))) (define-fun f359 () Arctic (+ (* f8 f352) (* f9 f353))) (define-fun f360 () Arctic (+ f10 f358)) (define-fun f361 () Arctic (+ f11 f359)) (define-fun f362 () Arctic (+ (* f0 f354) (* f1 f356))) (define-fun f363 () Arctic (+ (* f0 f355) (* f1 f357))) (define-fun f364 () Arctic (+ (* f2 f354) (* f3 f356))) (define-fun f365 () Arctic (+ (* f2 f355) (* f3 f357))) (define-fun f366 () Arctic (+ (* f0 f360) (* f1 f361))) (define-fun f367 () Arctic (+ (* f2 f360) (* f3 f361))) (define-fun f368 () Arctic (+ f4 f366)) (define-fun f369 () Arctic (+ f5 f367)) (define-fun f370 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f371 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f372 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f373 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f374 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f375 () Arctic (+ (* f8 f10) (* f9 f11))) (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 (+ (* 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 (+ (* f0 f386) (* f1 f388))) (define-fun f395 () Arctic (+ (* f0 f387) (* f1 f389))) (define-fun f396 () Arctic (+ (* f2 f386) (* f3 f388))) (define-fun f397 () Arctic (+ (* f2 f387) (* f3 f389))) (define-fun f398 () Arctic (+ (* f0 f392) (* f1 f393))) (define-fun f399 () Arctic (+ (* f2 f392) (* f3 f393))) (define-fun f400 () Arctic (+ f4 f398)) (define-fun f401 () Arctic (+ f5 f399)) (define-fun f402 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f403 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f404 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f405 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f406 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f407 () Arctic (+ (* f8 f10) (* f9 f11))) (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 (+ (* f6 f410) (* f7 f412))) (define-fun f419 () Arctic (+ (* f6 f411) (* f7 f413))) (define-fun f420 () Arctic (+ (* f8 f410) (* f9 f412))) (define-fun f421 () Arctic (+ (* f8 f411) (* f9 f413))) (define-fun f422 () Arctic (+ (* f6 f416) (* f7 f417))) (define-fun f423 () Arctic (+ (* f8 f416) (* f9 f417))) (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 (+ (* f6 f450) (* f7 f452))) (define-fun f459 () Arctic (+ (* f6 f451) (* f7 f453))) (define-fun f460 () Arctic (+ (* f8 f450) (* f9 f452))) (define-fun f461 () Arctic (+ (* f8 f451) (* f9 f453))) (define-fun f462 () Arctic (+ (* f6 f456) (* f7 f457))) (define-fun f463 () Arctic (+ (* f8 f456) (* f9 f457))) (define-fun f464 () Arctic (+ f10 f462)) (define-fun f465 () Arctic (+ f11 f463)) (define-fun f466 () Arctic (+ (* f0 f458) (* f1 f460))) (define-fun f467 () Arctic (+ (* f0 f459) (* f1 f461))) (define-fun f468 () Arctic (+ (* f2 f458) (* f3 f460))) (define-fun f469 () Arctic (+ (* f2 f459) (* f3 f461))) (define-fun f470 () Arctic (+ (* f0 f464) (* f1 f465))) (define-fun f471 () Arctic (+ (* f2 f464) (* f3 f465))) (define-fun f472 () Arctic (+ f4 f470)) (define-fun f473 () Arctic (+ f5 f471)) (define-fun f474 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f475 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f476 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f477 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f478 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f479 () Arctic (+ (* f8 f10) (* f9 f11))) (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 (+ (* f0 f482) (* f1 f484))) (define-fun f491 () Arctic (+ (* f0 f483) (* f1 f485))) (define-fun f492 () Arctic (+ (* f2 f482) (* f3 f484))) (define-fun f493 () Arctic (+ (* f2 f483) (* f3 f485))) (define-fun f494 () Arctic (+ (* f0 f488) (* f1 f489))) (define-fun f495 () Arctic (+ (* f2 f488) (* f3 f489))) (define-fun f496 () Arctic (+ f4 f494)) (define-fun f497 () Arctic (+ f5 f495)) (define-fun f498 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f499 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f500 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f501 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f502 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f503 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f504 () Arctic (+ f10 f502)) (define-fun f505 () Arctic (+ f11 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 (+ (* f6 f506) (* f7 f508))) (define-fun f515 () Arctic (+ (* f6 f507) (* f7 f509))) (define-fun f516 () Arctic (+ (* f8 f506) (* f9 f508))) (define-fun f517 () Arctic (+ (* f8 f507) (* f9 f509))) (define-fun f518 () Arctic (+ (* f6 f512) (* f7 f513))) (define-fun f519 () Arctic (+ (* f8 f512) (* f9 f513))) (define-fun f520 () Arctic (+ f10 f518)) (define-fun f521 () Arctic (+ f11 f519)) (define-fun f522 () Arctic (+ (* f6 f514) (* f7 f516))) (define-fun f523 () Arctic (+ (* f6 f515) (* f7 f517))) (define-fun f524 () Arctic (+ (* f8 f514) (* f9 f516))) (define-fun f525 () Arctic (+ (* f8 f515) (* f9 f517))) (define-fun f526 () Arctic (+ (* f6 f520) (* f7 f521))) (define-fun f527 () Arctic (+ (* f8 f520) (* f9 f521))) (define-fun f528 () Arctic (+ f10 f526)) (define-fun f529 () Arctic (+ f11 f527)) (define-fun f530 () Arctic (+ (* f12 f522) (* f13 f524))) (define-fun f531 () Arctic (+ (* f12 f523) (* f13 f525))) (define-fun f532 () Arctic (+ (* f14 f522) (* f15 f524))) (define-fun f533 () Arctic (+ (* f14 f523) (* f15 f525))) (define-fun f534 () Arctic (+ (* f12 f528) (* f13 f529))) (define-fun f535 () Arctic (+ (* f14 f528) (* f15 f529))) (define-fun f536 () Arctic (+ f16 f534)) (define-fun f537 () Arctic (+ f17 f535)) (define-fun f538 () Arctic (+ (* f6 f530) (* f7 f532))) (define-fun f539 () Arctic (+ (* f6 f531) (* f7 f533))) (define-fun f540 () Arctic (+ (* f8 f530) (* f9 f532))) (define-fun f541 () Arctic (+ (* f8 f531) (* f9 f533))) (define-fun f542 () Arctic (+ (* f6 f536) (* f7 f537))) (define-fun f543 () Arctic (+ (* f8 f536) (* f9 f537))) (define-fun f544 () Arctic (+ f10 f542)) (define-fun f545 () Arctic (+ f11 f543)) (define-fun f546 () Arctic (+ (* f6 f538) (* f7 f540))) (define-fun f547 () Arctic (+ (* f6 f539) (* f7 f541))) (define-fun f548 () Arctic (+ (* f8 f538) (* f9 f540))) (define-fun f549 () Arctic (+ (* f8 f539) (* f9 f541))) (define-fun f550 () Arctic (+ (* f6 f544) (* f7 f545))) (define-fun f551 () Arctic (+ (* f8 f544) (* f9 f545))) (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 (+ (* f0 f554) (* f1 f556))) (define-fun f563 () Arctic (+ (* f0 f555) (* f1 f557))) (define-fun f564 () Arctic (+ (* f2 f554) (* f3 f556))) (define-fun f565 () Arctic (+ (* f2 f555) (* f3 f557))) (define-fun f566 () Arctic (+ (* f0 f560) (* f1 f561))) (define-fun f567 () Arctic (+ (* f2 f560) (* f3 f561))) (define-fun f568 () Arctic (+ f4 f566)) (define-fun f569 () Arctic (+ f5 f567)) (define-fun f570 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f571 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f572 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f573 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f574 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f575 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f576 () Arctic (+ f10 f574)) (define-fun f577 () Arctic (+ f11 f575)) (define-fun f578 () Arctic (+ (* f0 f570) (* f1 f572))) (define-fun f579 () Arctic (+ (* f0 f571) (* f1 f573))) (define-fun f580 () Arctic (+ (* f2 f570) (* f3 f572))) (define-fun f581 () Arctic (+ (* f2 f571) (* f3 f573))) (define-fun f582 () Arctic (+ (* f0 f576) (* f1 f577))) (define-fun f583 () Arctic (+ (* f2 f576) (* f3 f577))) (define-fun f584 () Arctic (+ f4 f582)) (define-fun f585 () Arctic (+ f5 f583)) (define-fun f586 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f587 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f588 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f589 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f590 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f591 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f592 () Arctic (+ f10 f590)) (define-fun f593 () Arctic (+ f11 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 (+ (* f6 f594) (* f7 f596))) (define-fun f603 () Arctic (+ (* f6 f595) (* f7 f597))) (define-fun f604 () Arctic (+ (* f8 f594) (* f9 f596))) (define-fun f605 () Arctic (+ (* f8 f595) (* f9 f597))) (define-fun f606 () Arctic (+ (* f6 f600) (* f7 f601))) (define-fun f607 () Arctic (+ (* f8 f600) (* f9 f601))) (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 (+ (* 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 (+ (* f6 f626) (* f7 f628))) (define-fun f635 () Arctic (+ (* f6 f627) (* f7 f629))) (define-fun f636 () Arctic (+ (* f8 f626) (* f9 f628))) (define-fun f637 () Arctic (+ (* f8 f627) (* f9 f629))) (define-fun f638 () Arctic (+ (* f6 f632) (* f7 f633))) (define-fun f639 () Arctic (+ (* f8 f632) (* f9 f633))) (define-fun f640 () Arctic (+ f10 f638)) (define-fun f641 () Arctic (+ f11 f639)) (define-fun f642 () Arctic (+ (* f6 f634) (* f7 f636))) (define-fun f643 () Arctic (+ (* f6 f635) (* f7 f637))) (define-fun f644 () Arctic (+ (* f8 f634) (* f9 f636))) (define-fun f645 () Arctic (+ (* f8 f635) (* f9 f637))) (define-fun f646 () Arctic (+ (* f6 f640) (* f7 f641))) (define-fun f647 () Arctic (+ (* f8 f640) (* f9 f641))) (define-fun f648 () Arctic (+ f10 f646)) (define-fun f649 () Arctic (+ f11 f647)) (define-fun f650 () Arctic (+ (* f0 f642) (* f1 f644))) (define-fun f651 () Arctic (+ (* f0 f643) (* f1 f645))) (define-fun f652 () Arctic (+ (* f2 f642) (* f3 f644))) (define-fun f653 () Arctic (+ (* f2 f643) (* f3 f645))) (define-fun f654 () Arctic (+ (* f0 f648) (* f1 f649))) (define-fun f655 () Arctic (+ (* f2 f648) (* f3 f649))) (define-fun f656 () Arctic (+ f4 f654)) (define-fun f657 () Arctic (+ f5 f655)) (define-fun f658 () Arctic (+ (* f0 f6) (* f1 f8))) (define-fun f659 () Arctic (+ (* f0 f7) (* f1 f9))) (define-fun f660 () Arctic (+ (* f2 f6) (* f3 f8))) (define-fun f661 () Arctic (+ (* f2 f7) (* f3 f9))) (define-fun f662 () Arctic (+ (* f0 f10) (* f1 f11))) (define-fun f663 () Arctic (+ (* f2 f10) (* f3 f11))) (define-fun f664 () Arctic (+ f4 f662)) (define-fun f665 () Arctic (+ f5 f663)) (define-fun f666 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f667 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f668 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f669 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f670 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f671 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f672 () Arctic (+ f10 f670)) (define-fun f673 () Arctic (+ f11 f671)) (define-fun f674 () Arctic (+ (* f12 f666) (* f13 f668))) (define-fun f675 () Arctic (+ (* f12 f667) (* f13 f669))) (define-fun f676 () Arctic (+ (* f14 f666) (* f15 f668))) (define-fun f677 () Arctic (+ (* f14 f667) (* f15 f669))) (define-fun f678 () Arctic (+ (* f12 f672) (* f13 f673))) (define-fun f679 () Arctic (+ (* f14 f672) (* f15 f673))) (define-fun f680 () Arctic (+ f16 f678)) (define-fun f681 () Arctic (+ f17 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 (+ (* f6 f682) (* f7 f684))) (define-fun f691 () Arctic (+ (* f6 f683) (* f7 f685))) (define-fun f692 () Arctic (+ (* f8 f682) (* f9 f684))) (define-fun f693 () Arctic (+ (* f8 f683) (* f9 f685))) (define-fun f694 () Arctic (+ (* f6 f688) (* f7 f689))) (define-fun f695 () Arctic (+ (* f8 f688) (* f9 f689))) (define-fun f696 () Arctic (+ f10 f694)) (define-fun f697 () Arctic (+ f11 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 (+ (* 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 (+ (* f6 f714) (* f7 f716))) (define-fun f723 () Arctic (+ (* f6 f715) (* f7 f717))) (define-fun f724 () Arctic (+ (* f8 f714) (* f9 f716))) (define-fun f725 () Arctic (+ (* f8 f715) (* f9 f717))) (define-fun f726 () Arctic (+ (* f6 f720) (* f7 f721))) (define-fun f727 () Arctic (+ (* f8 f720) (* f9 f721))) (define-fun f728 () Arctic (+ f10 f726)) (define-fun f729 () Arctic (+ f11 f727)) (define-fun f730 () Arctic (+ (* f0 f722) (* f1 f724))) (define-fun f731 () Arctic (+ (* f0 f723) (* f1 f725))) (define-fun f732 () Arctic (+ (* f2 f722) (* f3 f724))) (define-fun f733 () Arctic (+ (* f2 f723) (* f3 f725))) (define-fun f734 () Arctic (+ (* f0 f728) (* f1 f729))) (define-fun f735 () Arctic (+ (* f2 f728) (* f3 f729))) (define-fun f736 () Arctic (+ f4 f734)) (define-fun f737 () Arctic (+ f5 f735)) (define-fun f738 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f739 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f740 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f741 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f742 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f743 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f744 () Arctic (+ f10 f742)) (define-fun f745 () Arctic (+ f11 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 (+ (* f6 f754) (* f7 f756))) (define-fun f763 () Arctic (+ (* f6 f755) (* f7 f757))) (define-fun f764 () Arctic (+ (* f8 f754) (* f9 f756))) (define-fun f765 () Arctic (+ (* f8 f755) (* f9 f757))) (define-fun f766 () Arctic (+ (* f6 f760) (* f7 f761))) (define-fun f767 () Arctic (+ (* f8 f760) (* f9 f761))) (define-fun f768 () Arctic (+ f10 f766)) (define-fun f769 () Arctic (+ f11 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 (+ (* 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 (+ (* f6 f778) (* f7 f780))) (define-fun f787 () Arctic (+ (* f6 f779) (* f7 f781))) (define-fun f788 () Arctic (+ (* f8 f778) (* f9 f780))) (define-fun f789 () Arctic (+ (* f8 f779) (* f9 f781))) (define-fun f790 () Arctic (+ (* f6 f784) (* f7 f785))) (define-fun f791 () Arctic (+ (* f8 f784) (* f9 f785))) (define-fun f792 () Arctic (+ f10 f790)) (define-fun f793 () Arctic (+ f11 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 (+ (* f6 f794) (* f7 f796))) (define-fun f803 () Arctic (+ (* f6 f795) (* f7 f797))) (define-fun f804 () Arctic (+ (* f8 f794) (* f9 f796))) (define-fun f805 () Arctic (+ (* f8 f795) (* f9 f797))) (define-fun f806 () Arctic (+ (* f6 f800) (* f7 f801))) (define-fun f807 () Arctic (+ (* f8 f800) (* f9 f801))) (define-fun f808 () Arctic (+ f10 f806)) (define-fun f809 () Arctic (+ f11 f807)) (define-fun f810 () Arctic (+ (* f6 f6) (* f7 f8))) (define-fun f811 () Arctic (+ (* f6 f7) (* f7 f9))) (define-fun f812 () Arctic (+ (* f8 f6) (* f9 f8))) (define-fun f813 () Arctic (+ (* f8 f7) (* f9 f9))) (define-fun f814 () Arctic (+ (* f6 f10) (* f7 f11))) (define-fun f815 () Arctic (+ (* f8 f10) (* f9 f11))) (define-fun f816 () Arctic (+ f10 f814)) (define-fun f817 () Arctic (+ f11 f815)) (define-fun f818 () Arctic (+ (* f6 f810) (* f7 f812))) (define-fun f819 () Arctic (+ (* f6 f811) (* f7 f813))) (define-fun f820 () Arctic (+ (* f8 f810) (* f9 f812))) (define-fun f821 () Arctic (+ (* f8 f811) (* f9 f813))) (define-fun f822 () Arctic (+ (* f6 f816) (* f7 f817))) (define-fun f823 () Arctic (+ (* f8 f816) (* f9 f817))) (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 (+ (* f6 f842) (* f7 f844))) (define-fun f851 () Arctic (+ (* f6 f843) (* f7 f845))) (define-fun f852 () Arctic (+ (* f8 f842) (* f9 f844))) (define-fun f853 () Arctic (+ (* f8 f843) (* f9 f845))) (define-fun f854 () Arctic (+ (* f6 f848) (* f7 f849))) (define-fun f855 () Arctic (+ (* f8 f848) (* f9 f849))) (define-fun f856 () Arctic (+ f10 f854)) (define-fun f857 () Arctic (+ f11 f855)) (define-fun f858 () Arctic (+ (* f6 f850) (* f7 f852))) (define-fun f859 () Arctic (+ (* f6 f851) (* f7 f853))) (define-fun f860 () Arctic (+ (* f8 f850) (* f9 f852))) (define-fun f861 () Arctic (+ (* f8 f851) (* f9 f853))) (define-fun f862 () Arctic (+ (* f6 f856) (* f7 f857))) (define-fun f863 () Arctic (+ (* f8 f856) (* f9 f857))) (define-fun f864 () Arctic (+ f10 f862)) (define-fun f865 () Arctic (+ f11 f863)) (define-fun f866 () Arctic (+ (* f12 f858) (* f13 f860))) (define-fun f867 () Arctic (+ (* f12 f859) (* f13 f861))) (define-fun f868 () Arctic (+ (* f14 f858) (* f15 f860))) (define-fun f869 () Arctic (+ (* f14 f859) (* f15 f861))) (define-fun f870 () Arctic (+ (* f12 f864) (* f13 f865))) (define-fun f871 () Arctic (+ (* f14 f864) (* f15 f865))) (define-fun f872 () Arctic (+ f16 f870)) (define-fun f873 () Arctic (+ f17 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 (+ (* f6 f874) (* f7 f876))) (define-fun f883 () Arctic (+ (* f6 f875) (* f7 f877))) (define-fun f884 () Arctic (+ (* f8 f874) (* f9 f876))) (define-fun f885 () Arctic (+ (* f8 f875) (* f9 f877))) (define-fun f886 () Arctic (+ (* f6 f880) (* f7 f881))) (define-fun f887 () Arctic (+ (* f8 f880) (* f9 f881))) (define-fun f888 () Arctic (+ f10 f886)) (define-fun f889 () Arctic (+ f11 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 (+ (* f6 f890) (* f7 f892))) (define-fun f899 () Arctic (+ (* f6 f891) (* f7 f893))) (define-fun f900 () Arctic (+ (* f8 f890) (* f9 f892))) (define-fun f901 () Arctic (+ (* f8 f891) (* f9 f893))) (define-fun f902 () Arctic (+ (* f6 f896) (* f7 f897))) (define-fun f903 () Arctic (+ (* f8 f896) (* f9 f897))) (define-fun f904 () Arctic (+ f10 f902)) (define-fun f905 () Arctic (+ f11 f903)) (assert (and (and (and (and (>= f82 f162) (>= f83 f163)) (and (>= f84 f164) (>= f85 f165))) (and (and (>= f88 f168)) (and (>= f89 f169)))) (and (and (and (>= f234 f290) (>= f235 f291)) (and (>= f236 f292) (>= f237 f293))) (and (and (>= f240 f296)) (and (>= f241 f297)))) (and (and (and (>= f362 f394) (>= f363 f395)) (and (>= f364 f396) (>= f365 f397))) (and (and (>= f368 f400)) (and (>= f369 f401)))) (and (and (and (>= f466 f490) (>= f467 f491)) (and (>= f468 f492) (>= f469 f493))) (and (and (>= f472 f496)) (and (>= f473 f497)))) (and (and (and (>= f562 f578) (>= f563 f579)) (and (>= f564 f580) (>= f565 f581))) (and (and (>= f568 f584)) (and (>= f569 f585)))) (and (and (and (>= f650 f658) (>= f651 f659)) (and (>= f652 f660) (>= f653 f661))) (and (and (>= f656 f664)) (and (>= f657 f665)))) (and (and (and (>= f730 f0) (>= f731 f1)) (and (>= f732 f2) (>= f733 f3))) (and (and (>= f736 f4)) (and (>= f737 f5)))) (and (and (and (>= f802 f898) (>= f803 f899)) (and (>= f804 f900) (>= f805 f901))) (and (and (>= f808 f904)) (and (>= f809 f905)))))) (assert (or (and (and (and (>> f82 f162) (>> f83 f163)) (and (>> f84 f164) (>> f85 f165))) (and (and (>> f88 f168)) (and (>> f89 f169)))) (and (and (and (>> f234 f290) (>> f235 f291)) (and (>> f236 f292) (>> f237 f293))) (and (and (>> f240 f296)) (and (>> f241 f297)))) (and (and (and (>> f362 f394) (>> f363 f395)) (and (>> f364 f396) (>> f365 f397))) (and (and (>> f368 f400)) (and (>> f369 f401)))) (and (and (and (>> f466 f490) (>> f467 f491)) (and (>> f468 f492) (>> f469 f493))) (and (and (>> f472 f496)) (and (>> f473 f497)))) (and (and (and (>> f562 f578) (>> f563 f579)) (and (>> f564 f580) (>> f565 f581))) (and (and (>> f568 f584)) (and (>> f569 f585)))) (and (and (and (>> f650 f658) (>> f651 f659)) (and (>> f652 f660) (>> f653 f661))) (and (and (>> f656 f664)) (and (>> f657 f665)))) (and (and (and (>> f730 f0) (>> f731 f1)) (and (>> f732 f2) (>> f733 f3))) (and (and (>> f736 f4)) (and (>> f737 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))