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