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