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