(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 h -> 0# 0 q0 h, 0# q0 h -> 0# q0 h, 0# q0 1 -> 0# 1 q0, 0# q0 1 -> 1# q0, 1# q1 0 -> 1# 0 q1, 1# q1 0 -> 0# q1, 1# q1 h -> 1# 0 q1 h, 1# q1 h -> 0# q1 h, 1# q1 1 -> 1# 1 q1, 1# q1 1 -> 1# q1, 0# q1 0 -> 0# 0 q2, 0# q1 0 -> 0# q2, 0# q1 h -> 0# 0 q2 h, 0# q1 h -> 0# q2 h, 0# q1 1 -> 0# 1 q2, 0# q1 1 -> 1# q2, 1# q2 0 -> 1# 0 q2, 1# q2 0 -> 0# q2, 1# q2 h -> 1# 0 q2 h, 1# q2 h -> 0# q2 h, 1# q2 1 -> 1# 1 q2, 1# q2 1 -> 1# q2, 0# q4 0 -> 1# 0 q5, 0# q4 0 -> 0# q5, 0# q4 h -> 0# q5 h, 0# q4 1 -> 1# 1 q5, 0# q4 1 -> 1# q5, 1# q5 0 -> 0# 0 q1, 1# q5 0 -> 0# q1, 1# q5 h -> 0# 0 q1 h, 1# q5 h -> 0# q1 h, 1# q5 1 -> 0# 1 q1, 1# q5 1 -> 1# q1, h# q3 -> h# 0 q3, h# q4 -> h# 0 q4, 0 q0 0 ->= 0 0 q0, 0 q0 h ->= 0 0 q0 h, 0 q0 1 ->= 0 1 q0, 1 q1 0 ->= 1 0 q1, 1 q1 h ->= 1 0 q1 h, 1 q1 1 ->= 1 1 q1, 0 q1 0 ->= 0 0 q2, 0 q1 h ->= 0 0 q2 h, 0 q1 1 ->= 0 1 q2, 1 q2 0 ->= 1 0 q2, 1 q2 h ->= 1 0 q2 h, 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 h ->= 1 0 q5 h, 0 q4 1 ->= 1 1 q5, 1 q5 0 ->= 0 0 q1, 1 q5 h ->= 0 0 q1 h, 1 q5 1 ->= 0 1 q1, h q0 ->= h 0 q0, h q1 ->= h 0 q1, h q2 ->= h 0 q2, h q3 ->= h 0 q3, h q4 ->= h 0 q4, h q5 ->= h 0 q5) 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) (assert (and (or (finite f12) (finite f16)) (or (finite f24) (finite f28)) (or (finite f18) (finite f22)) (or (finite f6) (finite f10)) (or (finite f36) (finite f40)) (or (finite f42) (finite f46)) (or (finite f66) (finite f70)) (or (finite f48) (finite f52)) (or (finite f54) (finite f58)) (or (finite f0) (finite f4)) (or (finite f30) (finite f34)) (or (finite f60) (finite f64)))) (define-fun f72 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f73 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f74 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f75 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f76 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f77 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f78 () Arctic (+ f10 f76)) (define-fun f79 () Arctic (+ f11 f77)) (define-fun f80 () Arctic (+ (* f0 f72) (* f1 f74))) (define-fun f81 () Arctic (+ (* f0 f73) (* f1 f75))) (define-fun f82 () Arctic (+ (* f2 f72) (* f3 f74))) (define-fun f83 () Arctic (+ (* f2 f73) (* f3 f75))) (define-fun f84 () Arctic (+ (* f0 f78) (* f1 f79))) (define-fun f85 () Arctic (+ (* f2 f78) (* f3 f79))) (define-fun f86 () Arctic (+ f4 f84)) (define-fun f87 () Arctic (+ f5 f85)) (define-fun f88 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f89 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f90 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f91 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f92 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f93 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f94 () Arctic (+ f16 f92)) (define-fun f95 () Arctic (+ f17 f93)) (define-fun f96 () Arctic (+ (* f0 f88) (* f1 f90))) (define-fun f97 () Arctic (+ (* f0 f89) (* f1 f91))) (define-fun f98 () Arctic (+ (* f2 f88) (* f3 f90))) (define-fun f99 () Arctic (+ (* f2 f89) (* f3 f91))) (define-fun f100 () Arctic (+ (* f0 f94) (* f1 f95))) (define-fun f101 () Arctic (+ (* f2 f94) (* f3 f95))) (define-fun f102 () Arctic (+ f4 f100)) (define-fun f103 () Arctic (+ f5 f101)) (define-fun f104 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f105 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f106 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f107 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f108 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f109 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f110 () Arctic (+ f10 f108)) (define-fun f111 () Arctic (+ f11 f109)) (define-fun f112 () Arctic (+ (* f0 f104) (* f1 f106))) (define-fun f113 () Arctic (+ (* f0 f105) (* f1 f107))) (define-fun f114 () Arctic (+ (* f2 f104) (* f3 f106))) (define-fun f115 () Arctic (+ (* f2 f105) (* f3 f107))) (define-fun f116 () Arctic (+ (* f0 f110) (* f1 f111))) (define-fun f117 () Arctic (+ (* f2 f110) (* f3 f111))) (define-fun f118 () Arctic (+ f4 f116)) (define-fun f119 () Arctic (+ f5 f117)) (define-fun f120 () Arctic (+ (* f0 f6) (* f1 f8))) (define-fun f121 () Arctic (+ (* f0 f7) (* f1 f9))) (define-fun f122 () Arctic (+ (* f2 f6) (* f3 f8))) (define-fun f123 () Arctic (+ (* f2 f7) (* f3 f9))) (define-fun f124 () Arctic (+ (* f0 f10) (* f1 f11))) (define-fun f125 () Arctic (+ (* f2 f10) (* f3 f11))) (define-fun f126 () Arctic (+ f4 f124)) (define-fun f127 () Arctic (+ f5 f125)) (define-fun f128 () Arctic (+ (* f6 f18) (* f7 f20))) (define-fun f129 () Arctic (+ (* f6 f19) (* f7 f21))) (define-fun f130 () Arctic (+ (* f8 f18) (* f9 f20))) (define-fun f131 () Arctic (+ (* f8 f19) (* f9 f21))) (define-fun f132 () Arctic (+ (* f6 f22) (* f7 f23))) (define-fun f133 () Arctic (+ (* f8 f22) (* f9 f23))) (define-fun f134 () Arctic (+ f10 f132)) (define-fun f135 () Arctic (+ f11 f133)) (define-fun f136 () Arctic (+ (* f0 f128) (* f1 f130))) (define-fun f137 () Arctic (+ (* f0 f129) (* f1 f131))) (define-fun f138 () Arctic (+ (* f2 f128) (* f3 f130))) (define-fun f139 () Arctic (+ (* f2 f129) (* f3 f131))) (define-fun f140 () Arctic (+ (* f0 f134) (* f1 f135))) (define-fun f141 () Arctic (+ (* f2 f134) (* f3 f135))) (define-fun f142 () Arctic (+ f4 f140)) (define-fun f143 () Arctic (+ f5 f141)) (define-fun f144 () Arctic (+ (* f6 f18) (* f7 f20))) (define-fun f145 () Arctic (+ (* f6 f19) (* f7 f21))) (define-fun f146 () Arctic (+ (* f8 f18) (* f9 f20))) (define-fun f147 () Arctic (+ (* f8 f19) (* f9 f21))) (define-fun f148 () Arctic (+ (* f6 f22) (* f7 f23))) (define-fun f149 () Arctic (+ (* f8 f22) (* f9 f23))) (define-fun f150 () Arctic (+ f10 f148)) (define-fun f151 () Arctic (+ f11 f149)) (define-fun f152 () Arctic (+ (* f12 f144) (* f13 f146))) (define-fun f153 () Arctic (+ (* f12 f145) (* f13 f147))) (define-fun f154 () Arctic (+ (* f14 f144) (* f15 f146))) (define-fun f155 () Arctic (+ (* f14 f145) (* f15 f147))) (define-fun f156 () Arctic (+ (* f12 f150) (* f13 f151))) (define-fun f157 () Arctic (+ (* f14 f150) (* f15 f151))) (define-fun f158 () Arctic (+ f16 f156)) (define-fun f159 () Arctic (+ f17 f157)) (define-fun f160 () Arctic (+ (* f0 f152) (* f1 f154))) (define-fun f161 () Arctic (+ (* f0 f153) (* f1 f155))) (define-fun f162 () Arctic (+ (* f2 f152) (* f3 f154))) (define-fun f163 () Arctic (+ (* f2 f153) (* f3 f155))) (define-fun f164 () Arctic (+ (* f0 f158) (* f1 f159))) (define-fun f165 () Arctic (+ (* f2 f158) (* f3 f159))) (define-fun f166 () Arctic (+ f4 f164)) (define-fun f167 () Arctic (+ f5 f165)) (define-fun f168 () Arctic (+ (* f6 f18) (* f7 f20))) (define-fun f169 () Arctic (+ (* f6 f19) (* f7 f21))) (define-fun f170 () Arctic (+ (* f8 f18) (* f9 f20))) (define-fun f171 () Arctic (+ (* f8 f19) (* f9 f21))) (define-fun f172 () Arctic (+ (* f6 f22) (* f7 f23))) (define-fun f173 () Arctic (+ (* f8 f22) (* f9 f23))) (define-fun f174 () Arctic (+ f10 f172)) (define-fun f175 () Arctic (+ f11 f173)) (define-fun f176 () Arctic (+ (* f0 f168) (* f1 f170))) (define-fun f177 () Arctic (+ (* f0 f169) (* f1 f171))) (define-fun f178 () Arctic (+ (* f2 f168) (* f3 f170))) (define-fun f179 () Arctic (+ (* f2 f169) (* f3 f171))) (define-fun f180 () Arctic (+ (* f0 f174) (* f1 f175))) (define-fun f181 () Arctic (+ (* f2 f174) (* f3 f175))) (define-fun f182 () Arctic (+ f4 f180)) (define-fun f183 () Arctic (+ f5 f181)) (define-fun f184 () Arctic (+ (* f6 f18) (* f7 f20))) (define-fun f185 () Arctic (+ (* f6 f19) (* f7 f21))) (define-fun f186 () Arctic (+ (* f8 f18) (* f9 f20))) (define-fun f187 () Arctic (+ (* f8 f19) (* f9 f21))) (define-fun f188 () Arctic (+ (* f6 f22) (* f7 f23))) (define-fun f189 () Arctic (+ (* f8 f22) (* f9 f23))) (define-fun f190 () Arctic (+ f10 f188)) (define-fun f191 () Arctic (+ f11 f189)) (define-fun f192 () Arctic (+ (* f0 f184) (* f1 f186))) (define-fun f193 () Arctic (+ (* f0 f185) (* f1 f187))) (define-fun f194 () Arctic (+ (* f2 f184) (* f3 f186))) (define-fun f195 () Arctic (+ (* f2 f185) (* f3 f187))) (define-fun f196 () Arctic (+ (* f0 f190) (* f1 f191))) (define-fun f197 () Arctic (+ (* f2 f190) (* f3 f191))) (define-fun f198 () Arctic (+ f4 f196)) (define-fun f199 () Arctic (+ f5 f197)) (define-fun f200 () Arctic (+ (* f6 f24) (* f7 f26))) (define-fun f201 () Arctic (+ (* f6 f25) (* f7 f27))) (define-fun f202 () Arctic (+ (* f8 f24) (* f9 f26))) (define-fun f203 () Arctic (+ (* f8 f25) (* f9 f27))) (define-fun f204 () Arctic (+ (* f6 f28) (* f7 f29))) (define-fun f205 () Arctic (+ (* f8 f28) (* f9 f29))) (define-fun f206 () Arctic (+ f10 f204)) (define-fun f207 () Arctic (+ f11 f205)) (define-fun f208 () Arctic (+ (* f0 f200) (* f1 f202))) (define-fun f209 () Arctic (+ (* f0 f201) (* f1 f203))) (define-fun f210 () Arctic (+ (* f2 f200) (* f3 f202))) (define-fun f211 () Arctic (+ (* f2 f201) (* f3 f203))) (define-fun f212 () Arctic (+ (* f0 f206) (* f1 f207))) (define-fun f213 () Arctic (+ (* f2 f206) (* f3 f207))) (define-fun f214 () Arctic (+ f4 f212)) (define-fun f215 () Arctic (+ f5 f213)) (define-fun f216 () Arctic (+ (* f24 f6) (* f25 f8))) (define-fun f217 () Arctic (+ (* f24 f7) (* f25 f9))) (define-fun f218 () Arctic (+ (* f26 f6) (* f27 f8))) (define-fun f219 () Arctic (+ (* f26 f7) (* f27 f9))) (define-fun f220 () Arctic (+ (* f24 f10) (* f25 f11))) (define-fun f221 () Arctic (+ (* f26 f10) (* f27 f11))) (define-fun f222 () Arctic (+ f28 f220)) (define-fun f223 () Arctic (+ f29 f221)) (define-fun f224 () Arctic (+ (* f0 f216) (* f1 f218))) (define-fun f225 () Arctic (+ (* f0 f217) (* f1 f219))) (define-fun f226 () Arctic (+ (* f2 f216) (* f3 f218))) (define-fun f227 () Arctic (+ (* f2 f217) (* f3 f219))) (define-fun f228 () Arctic (+ (* f0 f222) (* f1 f223))) (define-fun f229 () Arctic (+ (* f2 f222) (* f3 f223))) (define-fun f230 () Arctic (+ f4 f228)) (define-fun f231 () Arctic (+ f5 f229)) (define-fun f232 () Arctic (+ (* f6 f24) (* f7 f26))) (define-fun f233 () Arctic (+ (* f6 f25) (* f7 f27))) (define-fun f234 () Arctic (+ (* f8 f24) (* f9 f26))) (define-fun f235 () Arctic (+ (* f8 f25) (* f9 f27))) (define-fun f236 () Arctic (+ (* f6 f28) (* f7 f29))) (define-fun f237 () Arctic (+ (* f8 f28) (* f9 f29))) (define-fun f238 () Arctic (+ f10 f236)) (define-fun f239 () Arctic (+ f11 f237)) (define-fun f240 () Arctic (+ (* f0 f232) (* f1 f234))) (define-fun f241 () Arctic (+ (* f0 f233) (* f1 f235))) (define-fun f242 () Arctic (+ (* f2 f232) (* f3 f234))) (define-fun f243 () Arctic (+ (* f2 f233) (* f3 f235))) (define-fun f244 () Arctic (+ (* f0 f238) (* f1 f239))) (define-fun f245 () Arctic (+ (* f2 f238) (* f3 f239))) (define-fun f246 () Arctic (+ f4 f244)) (define-fun f247 () Arctic (+ f5 f245)) (define-fun f248 () Arctic (+ (* f30 f6) (* f31 f8))) (define-fun f249 () Arctic (+ (* f30 f7) (* f31 f9))) (define-fun f250 () Arctic (+ (* f32 f6) (* f33 f8))) (define-fun f251 () Arctic (+ (* f32 f7) (* f33 f9))) (define-fun f252 () Arctic (+ (* f30 f10) (* f31 f11))) (define-fun f253 () Arctic (+ (* f32 f10) (* f33 f11))) (define-fun f254 () Arctic (+ f34 f252)) (define-fun f255 () Arctic (+ f35 f253)) (define-fun f256 () Arctic (+ (* f36 f12) (* f37 f14))) (define-fun f257 () Arctic (+ (* f36 f13) (* f37 f15))) (define-fun f258 () Arctic (+ (* f38 f12) (* f39 f14))) (define-fun f259 () Arctic (+ (* f38 f13) (* f39 f15))) (define-fun f260 () Arctic (+ (* f36 f16) (* f37 f17))) (define-fun f261 () Arctic (+ (* f38 f16) (* f39 f17))) (define-fun f262 () Arctic (+ f40 f260)) (define-fun f263 () Arctic (+ f41 f261)) (define-fun f264 () Arctic (+ (* f30 f256) (* f31 f258))) (define-fun f265 () Arctic (+ (* f30 f257) (* f31 f259))) (define-fun f266 () Arctic (+ (* f32 f256) (* f33 f258))) (define-fun f267 () Arctic (+ (* f32 f257) (* f33 f259))) (define-fun f268 () Arctic (+ (* f30 f262) (* f31 f263))) (define-fun f269 () Arctic (+ (* f32 f262) (* f33 f263))) (define-fun f270 () Arctic (+ f34 f268)) (define-fun f271 () Arctic (+ f35 f269)) (define-fun f272 () Arctic (+ (* f12 f36) (* f13 f38))) (define-fun f273 () Arctic (+ (* f12 f37) (* f13 f39))) (define-fun f274 () Arctic (+ (* f14 f36) (* f15 f38))) (define-fun f275 () Arctic (+ (* f14 f37) (* f15 f39))) (define-fun f276 () Arctic (+ (* f12 f40) (* f13 f41))) (define-fun f277 () Arctic (+ (* f14 f40) (* f15 f41))) (define-fun f278 () Arctic (+ f16 f276)) (define-fun f279 () Arctic (+ f17 f277)) (define-fun f280 () Arctic (+ (* f30 f272) (* f31 f274))) (define-fun f281 () Arctic (+ (* f30 f273) (* f31 f275))) (define-fun f282 () Arctic (+ (* f32 f272) (* f33 f274))) (define-fun f283 () Arctic (+ (* f32 f273) (* f33 f275))) (define-fun f284 () Arctic (+ (* f30 f278) (* f31 f279))) (define-fun f285 () Arctic (+ (* f32 f278) (* f33 f279))) (define-fun f286 () Arctic (+ f34 f284)) (define-fun f287 () Arctic (+ f35 f285)) (define-fun f288 () Arctic (+ (* f36 f12) (* f37 f14))) (define-fun f289 () Arctic (+ (* f36 f13) (* f37 f15))) (define-fun f290 () Arctic (+ (* f38 f12) (* f39 f14))) (define-fun f291 () Arctic (+ (* f38 f13) (* f39 f15))) (define-fun f292 () Arctic (+ (* f36 f16) (* f37 f17))) (define-fun f293 () Arctic (+ (* f38 f16) (* f39 f17))) (define-fun f294 () Arctic (+ f40 f292)) (define-fun f295 () Arctic (+ f41 f293)) (define-fun f296 () Arctic (+ (* f30 f288) (* f31 f290))) (define-fun f297 () Arctic (+ (* f30 f289) (* f31 f291))) (define-fun f298 () Arctic (+ (* f32 f288) (* f33 f290))) (define-fun f299 () Arctic (+ (* f32 f289) (* f33 f291))) (define-fun f300 () Arctic (+ (* f30 f294) (* f31 f295))) (define-fun f301 () Arctic (+ (* f32 f294) (* f33 f295))) (define-fun f302 () Arctic (+ f34 f300)) (define-fun f303 () Arctic (+ f35 f301)) (define-fun f304 () Arctic (+ (* f0 f36) (* f1 f38))) (define-fun f305 () Arctic (+ (* f0 f37) (* f1 f39))) (define-fun f306 () Arctic (+ (* f2 f36) (* f3 f38))) (define-fun f307 () Arctic (+ (* f2 f37) (* f3 f39))) (define-fun f308 () Arctic (+ (* f0 f40) (* f1 f41))) (define-fun f309 () Arctic (+ (* f2 f40) (* f3 f41))) (define-fun f310 () Arctic (+ f4 f308)) (define-fun f311 () Arctic (+ f5 f309)) (define-fun f312 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f313 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f314 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f315 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f316 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f317 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f318 () Arctic (+ f40 f316)) (define-fun f319 () Arctic (+ f41 f317)) (define-fun f320 () Arctic (+ (* f30 f312) (* f31 f314))) (define-fun f321 () Arctic (+ (* f30 f313) (* f31 f315))) (define-fun f322 () Arctic (+ (* f32 f312) (* f33 f314))) (define-fun f323 () Arctic (+ (* f32 f313) (* f33 f315))) (define-fun f324 () Arctic (+ (* f30 f318) (* f31 f319))) (define-fun f325 () Arctic (+ (* f32 f318) (* f33 f319))) (define-fun f326 () Arctic (+ f34 f324)) (define-fun f327 () Arctic (+ f35 f325)) (define-fun f328 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f329 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f330 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f331 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f332 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f333 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f334 () Arctic (+ f40 f332)) (define-fun f335 () Arctic (+ f41 f333)) (define-fun f336 () Arctic (+ (* f12 f328) (* f13 f330))) (define-fun f337 () Arctic (+ (* f12 f329) (* f13 f331))) (define-fun f338 () Arctic (+ (* f14 f328) (* f15 f330))) (define-fun f339 () Arctic (+ (* f14 f329) (* f15 f331))) (define-fun f340 () Arctic (+ (* f12 f334) (* f13 f335))) (define-fun f341 () Arctic (+ (* f14 f334) (* f15 f335))) (define-fun f342 () Arctic (+ f16 f340)) (define-fun f343 () Arctic (+ f17 f341)) (define-fun f344 () Arctic (+ (* f30 f336) (* f31 f338))) (define-fun f345 () Arctic (+ (* f30 f337) (* f31 f339))) (define-fun f346 () Arctic (+ (* f32 f336) (* f33 f338))) (define-fun f347 () Arctic (+ (* f32 f337) (* f33 f339))) (define-fun f348 () Arctic (+ (* f30 f342) (* f31 f343))) (define-fun f349 () Arctic (+ (* f32 f342) (* f33 f343))) (define-fun f350 () Arctic (+ f34 f348)) (define-fun f351 () Arctic (+ f35 f349)) (define-fun f352 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f353 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f354 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f355 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f356 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f357 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f358 () Arctic (+ f40 f356)) (define-fun f359 () Arctic (+ f41 f357)) (define-fun f360 () Arctic (+ (* f30 f352) (* f31 f354))) (define-fun f361 () Arctic (+ (* f30 f353) (* f31 f355))) (define-fun f362 () Arctic (+ (* f32 f352) (* f33 f354))) (define-fun f363 () Arctic (+ (* f32 f353) (* f33 f355))) (define-fun f364 () Arctic (+ (* f30 f358) (* f31 f359))) (define-fun f365 () Arctic (+ (* f32 f358) (* f33 f359))) (define-fun f366 () Arctic (+ f34 f364)) (define-fun f367 () Arctic (+ f35 f365)) (define-fun f368 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f369 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f370 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f371 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f372 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f373 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f374 () Arctic (+ f40 f372)) (define-fun f375 () Arctic (+ f41 f373)) (define-fun f376 () Arctic (+ (* f0 f368) (* f1 f370))) (define-fun f377 () Arctic (+ (* f0 f369) (* f1 f371))) (define-fun f378 () Arctic (+ (* f2 f368) (* f3 f370))) (define-fun f379 () Arctic (+ (* f2 f369) (* f3 f371))) (define-fun f380 () Arctic (+ (* f0 f374) (* f1 f375))) (define-fun f381 () Arctic (+ (* f2 f374) (* f3 f375))) (define-fun f382 () Arctic (+ f4 f380)) (define-fun f383 () Arctic (+ f5 f381)) (define-fun f384 () Arctic (+ (* f36 f24) (* f37 f26))) (define-fun f385 () Arctic (+ (* f36 f25) (* f37 f27))) (define-fun f386 () Arctic (+ (* f38 f24) (* f39 f26))) (define-fun f387 () Arctic (+ (* f38 f25) (* f39 f27))) (define-fun f388 () Arctic (+ (* f36 f28) (* f37 f29))) (define-fun f389 () Arctic (+ (* f38 f28) (* f39 f29))) (define-fun f390 () Arctic (+ f40 f388)) (define-fun f391 () Arctic (+ f41 f389)) (define-fun f392 () Arctic (+ (* f30 f384) (* f31 f386))) (define-fun f393 () Arctic (+ (* f30 f385) (* f31 f387))) (define-fun f394 () Arctic (+ (* f32 f384) (* f33 f386))) (define-fun f395 () Arctic (+ (* f32 f385) (* f33 f387))) (define-fun f396 () Arctic (+ (* f30 f390) (* f31 f391))) (define-fun f397 () Arctic (+ (* f32 f390) (* f33 f391))) (define-fun f398 () Arctic (+ f34 f396)) (define-fun f399 () Arctic (+ f35 f397)) (define-fun f400 () Arctic (+ (* f24 f36) (* f25 f38))) (define-fun f401 () Arctic (+ (* f24 f37) (* f25 f39))) (define-fun f402 () Arctic (+ (* f26 f36) (* f27 f38))) (define-fun f403 () Arctic (+ (* f26 f37) (* f27 f39))) (define-fun f404 () Arctic (+ (* f24 f40) (* f25 f41))) (define-fun f405 () Arctic (+ (* f26 f40) (* f27 f41))) (define-fun f406 () Arctic (+ f28 f404)) (define-fun f407 () Arctic (+ f29 f405)) (define-fun f408 () Arctic (+ (* f30 f400) (* f31 f402))) (define-fun f409 () Arctic (+ (* f30 f401) (* f31 f403))) (define-fun f410 () Arctic (+ (* f32 f400) (* f33 f402))) (define-fun f411 () Arctic (+ (* f32 f401) (* f33 f403))) (define-fun f412 () Arctic (+ (* f30 f406) (* f31 f407))) (define-fun f413 () Arctic (+ (* f32 f406) (* f33 f407))) (define-fun f414 () Arctic (+ f34 f412)) (define-fun f415 () Arctic (+ f35 f413)) (define-fun f416 () Arctic (+ (* f36 f24) (* f37 f26))) (define-fun f417 () Arctic (+ (* f36 f25) (* f37 f27))) (define-fun f418 () Arctic (+ (* f38 f24) (* f39 f26))) (define-fun f419 () Arctic (+ (* f38 f25) (* f39 f27))) (define-fun f420 () Arctic (+ (* f36 f28) (* f37 f29))) (define-fun f421 () Arctic (+ (* f38 f28) (* f39 f29))) (define-fun f422 () Arctic (+ f40 f420)) (define-fun f423 () Arctic (+ f41 f421)) (define-fun f424 () Arctic (+ (* f30 f416) (* f31 f418))) (define-fun f425 () Arctic (+ (* f30 f417) (* f31 f419))) (define-fun f426 () Arctic (+ (* f32 f416) (* f33 f418))) (define-fun f427 () Arctic (+ (* f32 f417) (* f33 f419))) (define-fun f428 () Arctic (+ (* f30 f422) (* f31 f423))) (define-fun f429 () Arctic (+ (* f32 f422) (* f33 f423))) (define-fun f430 () Arctic (+ f34 f428)) (define-fun f431 () Arctic (+ f35 f429)) (define-fun f432 () Arctic (+ (* f30 f36) (* f31 f38))) (define-fun f433 () Arctic (+ (* f30 f37) (* f31 f39))) (define-fun f434 () Arctic (+ (* f32 f36) (* f33 f38))) (define-fun f435 () Arctic (+ (* f32 f37) (* f33 f39))) (define-fun f436 () Arctic (+ (* f30 f40) (* f31 f41))) (define-fun f437 () Arctic (+ (* f32 f40) (* f33 f41))) (define-fun f438 () Arctic (+ f34 f436)) (define-fun f439 () Arctic (+ f35 f437)) (define-fun f440 () Arctic (+ (* f36 f12) (* f37 f14))) (define-fun f441 () Arctic (+ (* f36 f13) (* f37 f15))) (define-fun f442 () Arctic (+ (* f38 f12) (* f39 f14))) (define-fun f443 () Arctic (+ (* f38 f13) (* f39 f15))) (define-fun f444 () Arctic (+ (* f36 f16) (* f37 f17))) (define-fun f445 () Arctic (+ (* f38 f16) (* f39 f17))) (define-fun f446 () Arctic (+ f40 f444)) (define-fun f447 () Arctic (+ f41 f445)) (define-fun f448 () Arctic (+ (* f0 f440) (* f1 f442))) (define-fun f449 () Arctic (+ (* f0 f441) (* f1 f443))) (define-fun f450 () Arctic (+ (* f2 f440) (* f3 f442))) (define-fun f451 () Arctic (+ (* f2 f441) (* f3 f443))) (define-fun f452 () Arctic (+ (* f0 f446) (* f1 f447))) (define-fun f453 () Arctic (+ (* f2 f446) (* f3 f447))) (define-fun f454 () Arctic (+ f4 f452)) (define-fun f455 () Arctic (+ f5 f453)) (define-fun f456 () Arctic (+ (* f12 f42) (* f13 f44))) (define-fun f457 () Arctic (+ (* f12 f43) (* f13 f45))) (define-fun f458 () Arctic (+ (* f14 f42) (* f15 f44))) (define-fun f459 () Arctic (+ (* f14 f43) (* f15 f45))) (define-fun f460 () Arctic (+ (* f12 f46) (* f13 f47))) (define-fun f461 () Arctic (+ (* f14 f46) (* f15 f47))) (define-fun f462 () Arctic (+ f16 f460)) (define-fun f463 () Arctic (+ f17 f461)) (define-fun f464 () Arctic (+ (* f0 f456) (* f1 f458))) (define-fun f465 () Arctic (+ (* f0 f457) (* f1 f459))) (define-fun f466 () Arctic (+ (* f2 f456) (* f3 f458))) (define-fun f467 () Arctic (+ (* f2 f457) (* f3 f459))) (define-fun f468 () Arctic (+ (* f0 f462) (* f1 f463))) (define-fun f469 () Arctic (+ (* f2 f462) (* f3 f463))) (define-fun f470 () Arctic (+ f4 f468)) (define-fun f471 () Arctic (+ f5 f469)) (define-fun f472 () Arctic (+ (* f36 f12) (* f37 f14))) (define-fun f473 () Arctic (+ (* f36 f13) (* f37 f15))) (define-fun f474 () Arctic (+ (* f38 f12) (* f39 f14))) (define-fun f475 () Arctic (+ (* f38 f13) (* f39 f15))) (define-fun f476 () Arctic (+ (* f36 f16) (* f37 f17))) (define-fun f477 () Arctic (+ (* f38 f16) (* f39 f17))) (define-fun f478 () Arctic (+ f40 f476)) (define-fun f479 () Arctic (+ f41 f477)) (define-fun f480 () Arctic (+ (* f0 f472) (* f1 f474))) (define-fun f481 () Arctic (+ (* f0 f473) (* f1 f475))) (define-fun f482 () Arctic (+ (* f2 f472) (* f3 f474))) (define-fun f483 () Arctic (+ (* f2 f473) (* f3 f475))) (define-fun f484 () Arctic (+ (* f0 f478) (* f1 f479))) (define-fun f485 () Arctic (+ (* f2 f478) (* f3 f479))) (define-fun f486 () Arctic (+ f4 f484)) (define-fun f487 () Arctic (+ f5 f485)) (define-fun f488 () Arctic (+ (* f0 f42) (* f1 f44))) (define-fun f489 () Arctic (+ (* f0 f43) (* f1 f45))) (define-fun f490 () Arctic (+ (* f2 f42) (* f3 f44))) (define-fun f491 () Arctic (+ (* f2 f43) (* f3 f45))) (define-fun f492 () Arctic (+ (* f0 f46) (* f1 f47))) (define-fun f493 () Arctic (+ (* f2 f46) (* f3 f47))) (define-fun f494 () Arctic (+ f4 f492)) (define-fun f495 () Arctic (+ f5 f493)) (define-fun f496 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f497 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f498 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f499 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f500 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f501 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f502 () Arctic (+ f40 f500)) (define-fun f503 () Arctic (+ f41 f501)) (define-fun f504 () Arctic (+ (* f0 f496) (* f1 f498))) (define-fun f505 () Arctic (+ (* f0 f497) (* f1 f499))) (define-fun f506 () Arctic (+ (* f2 f496) (* f3 f498))) (define-fun f507 () Arctic (+ (* f2 f497) (* f3 f499))) (define-fun f508 () Arctic (+ (* f0 f502) (* f1 f503))) (define-fun f509 () Arctic (+ (* f2 f502) (* f3 f503))) (define-fun f510 () Arctic (+ f4 f508)) (define-fun f511 () Arctic (+ f5 f509)) (define-fun f512 () Arctic (+ (* f42 f18) (* f43 f20))) (define-fun f513 () Arctic (+ (* f42 f19) (* f43 f21))) (define-fun f514 () Arctic (+ (* f44 f18) (* f45 f20))) (define-fun f515 () Arctic (+ (* f44 f19) (* f45 f21))) (define-fun f516 () Arctic (+ (* f42 f22) (* f43 f23))) (define-fun f517 () Arctic (+ (* f44 f22) (* f45 f23))) (define-fun f518 () Arctic (+ f46 f516)) (define-fun f519 () Arctic (+ f47 f517)) (define-fun f520 () Arctic (+ (* f12 f512) (* f13 f514))) (define-fun f521 () Arctic (+ (* f12 f513) (* f13 f515))) (define-fun f522 () Arctic (+ (* f14 f512) (* f15 f514))) (define-fun f523 () Arctic (+ (* f14 f513) (* f15 f515))) (define-fun f524 () Arctic (+ (* f12 f518) (* f13 f519))) (define-fun f525 () Arctic (+ (* f14 f518) (* f15 f519))) (define-fun f526 () Arctic (+ f16 f524)) (define-fun f527 () Arctic (+ f17 f525)) (define-fun f528 () Arctic (+ (* f0 f520) (* f1 f522))) (define-fun f529 () Arctic (+ (* f0 f521) (* f1 f523))) (define-fun f530 () Arctic (+ (* f2 f520) (* f3 f522))) (define-fun f531 () Arctic (+ (* f2 f521) (* f3 f523))) (define-fun f532 () Arctic (+ (* f0 f526) (* f1 f527))) (define-fun f533 () Arctic (+ (* f2 f526) (* f3 f527))) (define-fun f534 () Arctic (+ f4 f532)) (define-fun f535 () Arctic (+ f5 f533)) (define-fun f536 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f537 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f538 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f539 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f540 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f541 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f542 () Arctic (+ f40 f540)) (define-fun f543 () Arctic (+ f41 f541)) (define-fun f544 () Arctic (+ (* f0 f536) (* f1 f538))) (define-fun f545 () Arctic (+ (* f0 f537) (* f1 f539))) (define-fun f546 () Arctic (+ (* f2 f536) (* f3 f538))) (define-fun f547 () Arctic (+ (* f2 f537) (* f3 f539))) (define-fun f548 () Arctic (+ (* f0 f542) (* f1 f543))) (define-fun f549 () Arctic (+ (* f2 f542) (* f3 f543))) (define-fun f550 () Arctic (+ f4 f548)) (define-fun f551 () Arctic (+ f5 f549)) (define-fun f552 () Arctic (+ (* f42 f18) (* f43 f20))) (define-fun f553 () Arctic (+ (* f42 f19) (* f43 f21))) (define-fun f554 () Arctic (+ (* f44 f18) (* f45 f20))) (define-fun f555 () Arctic (+ (* f44 f19) (* f45 f21))) (define-fun f556 () Arctic (+ (* f42 f22) (* f43 f23))) (define-fun f557 () Arctic (+ (* f44 f22) (* f45 f23))) (define-fun f558 () Arctic (+ f46 f556)) (define-fun f559 () Arctic (+ f47 f557)) (define-fun f560 () Arctic (+ (* f0 f552) (* f1 f554))) (define-fun f561 () Arctic (+ (* f0 f553) (* f1 f555))) (define-fun f562 () Arctic (+ (* f2 f552) (* f3 f554))) (define-fun f563 () Arctic (+ (* f2 f553) (* f3 f555))) (define-fun f564 () Arctic (+ (* f0 f558) (* f1 f559))) (define-fun f565 () Arctic (+ (* f2 f558) (* f3 f559))) (define-fun f566 () Arctic (+ f4 f564)) (define-fun f567 () Arctic (+ f5 f565)) (define-fun f568 () Arctic (+ (* f36 f24) (* f37 f26))) (define-fun f569 () Arctic (+ (* f36 f25) (* f37 f27))) (define-fun f570 () Arctic (+ (* f38 f24) (* f39 f26))) (define-fun f571 () Arctic (+ (* f38 f25) (* f39 f27))) (define-fun f572 () Arctic (+ (* f36 f28) (* f37 f29))) (define-fun f573 () Arctic (+ (* f38 f28) (* f39 f29))) (define-fun f574 () Arctic (+ f40 f572)) (define-fun f575 () Arctic (+ f41 f573)) (define-fun f576 () Arctic (+ (* f0 f568) (* f1 f570))) (define-fun f577 () Arctic (+ (* f0 f569) (* f1 f571))) (define-fun f578 () Arctic (+ (* f2 f568) (* f3 f570))) (define-fun f579 () Arctic (+ (* f2 f569) (* f3 f571))) (define-fun f580 () Arctic (+ (* f0 f574) (* f1 f575))) (define-fun f581 () Arctic (+ (* f2 f574) (* f3 f575))) (define-fun f582 () Arctic (+ f4 f580)) (define-fun f583 () Arctic (+ f5 f581)) (define-fun f584 () Arctic (+ (* f24 f42) (* f25 f44))) (define-fun f585 () Arctic (+ (* f24 f43) (* f25 f45))) (define-fun f586 () Arctic (+ (* f26 f42) (* f27 f44))) (define-fun f587 () Arctic (+ (* f26 f43) (* f27 f45))) (define-fun f588 () Arctic (+ (* f24 f46) (* f25 f47))) (define-fun f589 () Arctic (+ (* f26 f46) (* f27 f47))) (define-fun f590 () Arctic (+ f28 f588)) (define-fun f591 () Arctic (+ f29 f589)) (define-fun f592 () Arctic (+ (* f0 f584) (* f1 f586))) (define-fun f593 () Arctic (+ (* f0 f585) (* f1 f587))) (define-fun f594 () Arctic (+ (* f2 f584) (* f3 f586))) (define-fun f595 () Arctic (+ (* f2 f585) (* f3 f587))) (define-fun f596 () Arctic (+ (* f0 f590) (* f1 f591))) (define-fun f597 () Arctic (+ (* f2 f590) (* f3 f591))) (define-fun f598 () Arctic (+ f4 f596)) (define-fun f599 () Arctic (+ f5 f597)) (define-fun f600 () Arctic (+ (* f36 f24) (* f37 f26))) (define-fun f601 () Arctic (+ (* f36 f25) (* f37 f27))) (define-fun f602 () Arctic (+ (* f38 f24) (* f39 f26))) (define-fun f603 () Arctic (+ (* f38 f25) (* f39 f27))) (define-fun f604 () Arctic (+ (* f36 f28) (* f37 f29))) (define-fun f605 () Arctic (+ (* f38 f28) (* f39 f29))) (define-fun f606 () Arctic (+ f40 f604)) (define-fun f607 () Arctic (+ f41 f605)) (define-fun f608 () Arctic (+ (* f0 f600) (* f1 f602))) (define-fun f609 () Arctic (+ (* f0 f601) (* f1 f603))) (define-fun f610 () Arctic (+ (* f2 f600) (* f3 f602))) (define-fun f611 () Arctic (+ (* f2 f601) (* f3 f603))) (define-fun f612 () Arctic (+ (* f0 f606) (* f1 f607))) (define-fun f613 () Arctic (+ (* f2 f606) (* f3 f607))) (define-fun f614 () Arctic (+ f4 f612)) (define-fun f615 () Arctic (+ f5 f613)) (define-fun f616 () Arctic (+ (* f30 f42) (* f31 f44))) (define-fun f617 () Arctic (+ (* f30 f43) (* f31 f45))) (define-fun f618 () Arctic (+ (* f32 f42) (* f33 f44))) (define-fun f619 () Arctic (+ (* f32 f43) (* f33 f45))) (define-fun f620 () Arctic (+ (* f30 f46) (* f31 f47))) (define-fun f621 () Arctic (+ (* f32 f46) (* f33 f47))) (define-fun f622 () Arctic (+ f34 f620)) (define-fun f623 () Arctic (+ f35 f621)) (define-fun f624 () Arctic (+ (* f42 f12) (* f43 f14))) (define-fun f625 () Arctic (+ (* f42 f13) (* f43 f15))) (define-fun f626 () Arctic (+ (* f44 f12) (* f45 f14))) (define-fun f627 () Arctic (+ (* f44 f13) (* f45 f15))) (define-fun f628 () Arctic (+ (* f42 f16) (* f43 f17))) (define-fun f629 () Arctic (+ (* f44 f16) (* f45 f17))) (define-fun f630 () Arctic (+ f46 f628)) (define-fun f631 () Arctic (+ f47 f629)) (define-fun f632 () Arctic (+ (* f30 f624) (* f31 f626))) (define-fun f633 () Arctic (+ (* f30 f625) (* f31 f627))) (define-fun f634 () Arctic (+ (* f32 f624) (* f33 f626))) (define-fun f635 () Arctic (+ (* f32 f625) (* f33 f627))) (define-fun f636 () Arctic (+ (* f30 f630) (* f31 f631))) (define-fun f637 () Arctic (+ (* f32 f630) (* f33 f631))) (define-fun f638 () Arctic (+ f34 f636)) (define-fun f639 () Arctic (+ f35 f637)) (define-fun f640 () Arctic (+ (* f12 f42) (* f13 f44))) (define-fun f641 () Arctic (+ (* f12 f43) (* f13 f45))) (define-fun f642 () Arctic (+ (* f14 f42) (* f15 f44))) (define-fun f643 () Arctic (+ (* f14 f43) (* f15 f45))) (define-fun f644 () Arctic (+ (* f12 f46) (* f13 f47))) (define-fun f645 () Arctic (+ (* f14 f46) (* f15 f47))) (define-fun f646 () Arctic (+ f16 f644)) (define-fun f647 () Arctic (+ f17 f645)) (define-fun f648 () Arctic (+ (* f30 f640) (* f31 f642))) (define-fun f649 () Arctic (+ (* f30 f641) (* f31 f643))) (define-fun f650 () Arctic (+ (* f32 f640) (* f33 f642))) (define-fun f651 () Arctic (+ (* f32 f641) (* f33 f643))) (define-fun f652 () Arctic (+ (* f30 f646) (* f31 f647))) (define-fun f653 () Arctic (+ (* f32 f646) (* f33 f647))) (define-fun f654 () Arctic (+ f34 f652)) (define-fun f655 () Arctic (+ f35 f653)) (define-fun f656 () Arctic (+ (* f42 f12) (* f43 f14))) (define-fun f657 () Arctic (+ (* f42 f13) (* f43 f15))) (define-fun f658 () Arctic (+ (* f44 f12) (* f45 f14))) (define-fun f659 () Arctic (+ (* f44 f13) (* f45 f15))) (define-fun f660 () Arctic (+ (* f42 f16) (* f43 f17))) (define-fun f661 () Arctic (+ (* f44 f16) (* f45 f17))) (define-fun f662 () Arctic (+ f46 f660)) (define-fun f663 () Arctic (+ f47 f661)) (define-fun f664 () Arctic (+ (* f30 f656) (* f31 f658))) (define-fun f665 () Arctic (+ (* f30 f657) (* f31 f659))) (define-fun f666 () Arctic (+ (* f32 f656) (* f33 f658))) (define-fun f667 () Arctic (+ (* f32 f657) (* f33 f659))) (define-fun f668 () Arctic (+ (* f30 f662) (* f31 f663))) (define-fun f669 () Arctic (+ (* f32 f662) (* f33 f663))) (define-fun f670 () Arctic (+ f34 f668)) (define-fun f671 () Arctic (+ f35 f669)) (define-fun f672 () Arctic (+ (* f0 f42) (* f1 f44))) (define-fun f673 () Arctic (+ (* f0 f43) (* f1 f45))) (define-fun f674 () Arctic (+ (* f2 f42) (* f3 f44))) (define-fun f675 () Arctic (+ (* f2 f43) (* f3 f45))) (define-fun f676 () Arctic (+ (* f0 f46) (* f1 f47))) (define-fun f677 () Arctic (+ (* f2 f46) (* f3 f47))) (define-fun f678 () Arctic (+ f4 f676)) (define-fun f679 () Arctic (+ f5 f677)) (define-fun f680 () Arctic (+ (* f42 f18) (* f43 f20))) (define-fun f681 () Arctic (+ (* f42 f19) (* f43 f21))) (define-fun f682 () Arctic (+ (* f44 f18) (* f45 f20))) (define-fun f683 () Arctic (+ (* f44 f19) (* f45 f21))) (define-fun f684 () Arctic (+ (* f42 f22) (* f43 f23))) (define-fun f685 () Arctic (+ (* f44 f22) (* f45 f23))) (define-fun f686 () Arctic (+ f46 f684)) (define-fun f687 () Arctic (+ f47 f685)) (define-fun f688 () Arctic (+ (* f30 f680) (* f31 f682))) (define-fun f689 () Arctic (+ (* f30 f681) (* f31 f683))) (define-fun f690 () Arctic (+ (* f32 f680) (* f33 f682))) (define-fun f691 () Arctic (+ (* f32 f681) (* f33 f683))) (define-fun f692 () Arctic (+ (* f30 f686) (* f31 f687))) (define-fun f693 () Arctic (+ (* f32 f686) (* f33 f687))) (define-fun f694 () Arctic (+ f34 f692)) (define-fun f695 () Arctic (+ f35 f693)) (define-fun f696 () Arctic (+ (* f42 f18) (* f43 f20))) (define-fun f697 () Arctic (+ (* f42 f19) (* f43 f21))) (define-fun f698 () Arctic (+ (* f44 f18) (* f45 f20))) (define-fun f699 () Arctic (+ (* f44 f19) (* f45 f21))) (define-fun f700 () Arctic (+ (* f42 f22) (* f43 f23))) (define-fun f701 () Arctic (+ (* f44 f22) (* f45 f23))) (define-fun f702 () Arctic (+ f46 f700)) (define-fun f703 () Arctic (+ f47 f701)) (define-fun f704 () Arctic (+ (* f12 f696) (* f13 f698))) (define-fun f705 () Arctic (+ (* f12 f697) (* f13 f699))) (define-fun f706 () Arctic (+ (* f14 f696) (* f15 f698))) (define-fun f707 () Arctic (+ (* f14 f697) (* f15 f699))) (define-fun f708 () Arctic (+ (* f12 f702) (* f13 f703))) (define-fun f709 () Arctic (+ (* f14 f702) (* f15 f703))) (define-fun f710 () Arctic (+ f16 f708)) (define-fun f711 () Arctic (+ f17 f709)) (define-fun f712 () Arctic (+ (* f30 f704) (* f31 f706))) (define-fun f713 () Arctic (+ (* f30 f705) (* f31 f707))) (define-fun f714 () Arctic (+ (* f32 f704) (* f33 f706))) (define-fun f715 () Arctic (+ (* f32 f705) (* f33 f707))) (define-fun f716 () Arctic (+ (* f30 f710) (* f31 f711))) (define-fun f717 () Arctic (+ (* f32 f710) (* f33 f711))) (define-fun f718 () Arctic (+ f34 f716)) (define-fun f719 () Arctic (+ f35 f717)) (define-fun f720 () Arctic (+ (* f42 f18) (* f43 f20))) (define-fun f721 () Arctic (+ (* f42 f19) (* f43 f21))) (define-fun f722 () Arctic (+ (* f44 f18) (* f45 f20))) (define-fun f723 () Arctic (+ (* f44 f19) (* f45 f21))) (define-fun f724 () Arctic (+ (* f42 f22) (* f43 f23))) (define-fun f725 () Arctic (+ (* f44 f22) (* f45 f23))) (define-fun f726 () Arctic (+ f46 f724)) (define-fun f727 () Arctic (+ f47 f725)) (define-fun f728 () Arctic (+ (* f30 f720) (* f31 f722))) (define-fun f729 () Arctic (+ (* f30 f721) (* f31 f723))) (define-fun f730 () Arctic (+ (* f32 f720) (* f33 f722))) (define-fun f731 () Arctic (+ (* f32 f721) (* f33 f723))) (define-fun f732 () Arctic (+ (* f30 f726) (* f31 f727))) (define-fun f733 () Arctic (+ (* f32 f726) (* f33 f727))) (define-fun f734 () Arctic (+ f34 f732)) (define-fun f735 () Arctic (+ f35 f733)) (define-fun f736 () Arctic (+ (* f42 f18) (* f43 f20))) (define-fun f737 () Arctic (+ (* f42 f19) (* f43 f21))) (define-fun f738 () Arctic (+ (* f44 f18) (* f45 f20))) (define-fun f739 () Arctic (+ (* f44 f19) (* f45 f21))) (define-fun f740 () Arctic (+ (* f42 f22) (* f43 f23))) (define-fun f741 () Arctic (+ (* f44 f22) (* f45 f23))) (define-fun f742 () Arctic (+ f46 f740)) (define-fun f743 () Arctic (+ f47 f741)) (define-fun f744 () Arctic (+ (* f0 f736) (* f1 f738))) (define-fun f745 () Arctic (+ (* f0 f737) (* f1 f739))) (define-fun f746 () Arctic (+ (* f2 f736) (* f3 f738))) (define-fun f747 () Arctic (+ (* f2 f737) (* f3 f739))) (define-fun f748 () Arctic (+ (* f0 f742) (* f1 f743))) (define-fun f749 () Arctic (+ (* f2 f742) (* f3 f743))) (define-fun f750 () Arctic (+ f4 f748)) (define-fun f751 () Arctic (+ f5 f749)) (define-fun f752 () Arctic (+ (* f42 f24) (* f43 f26))) (define-fun f753 () Arctic (+ (* f42 f25) (* f43 f27))) (define-fun f754 () Arctic (+ (* f44 f24) (* f45 f26))) (define-fun f755 () Arctic (+ (* f44 f25) (* f45 f27))) (define-fun f756 () Arctic (+ (* f42 f28) (* f43 f29))) (define-fun f757 () Arctic (+ (* f44 f28) (* f45 f29))) (define-fun f758 () Arctic (+ f46 f756)) (define-fun f759 () Arctic (+ f47 f757)) (define-fun f760 () Arctic (+ (* f30 f752) (* f31 f754))) (define-fun f761 () Arctic (+ (* f30 f753) (* f31 f755))) (define-fun f762 () Arctic (+ (* f32 f752) (* f33 f754))) (define-fun f763 () Arctic (+ (* f32 f753) (* f33 f755))) (define-fun f764 () Arctic (+ (* f30 f758) (* f31 f759))) (define-fun f765 () Arctic (+ (* f32 f758) (* f33 f759))) (define-fun f766 () Arctic (+ f34 f764)) (define-fun f767 () Arctic (+ f35 f765)) (define-fun f768 () Arctic (+ (* f24 f42) (* f25 f44))) (define-fun f769 () Arctic (+ (* f24 f43) (* f25 f45))) (define-fun f770 () Arctic (+ (* f26 f42) (* f27 f44))) (define-fun f771 () Arctic (+ (* f26 f43) (* f27 f45))) (define-fun f772 () Arctic (+ (* f24 f46) (* f25 f47))) (define-fun f773 () Arctic (+ (* f26 f46) (* f27 f47))) (define-fun f774 () Arctic (+ f28 f772)) (define-fun f775 () Arctic (+ f29 f773)) (define-fun f776 () Arctic (+ (* f30 f768) (* f31 f770))) (define-fun f777 () Arctic (+ (* f30 f769) (* f31 f771))) (define-fun f778 () Arctic (+ (* f32 f768) (* f33 f770))) (define-fun f779 () Arctic (+ (* f32 f769) (* f33 f771))) (define-fun f780 () Arctic (+ (* f30 f774) (* f31 f775))) (define-fun f781 () Arctic (+ (* f32 f774) (* f33 f775))) (define-fun f782 () Arctic (+ f34 f780)) (define-fun f783 () Arctic (+ f35 f781)) (define-fun f784 () Arctic (+ (* f42 f24) (* f43 f26))) (define-fun f785 () Arctic (+ (* f42 f25) (* f43 f27))) (define-fun f786 () Arctic (+ (* f44 f24) (* f45 f26))) (define-fun f787 () Arctic (+ (* f44 f25) (* f45 f27))) (define-fun f788 () Arctic (+ (* f42 f28) (* f43 f29))) (define-fun f789 () Arctic (+ (* f44 f28) (* f45 f29))) (define-fun f790 () Arctic (+ f46 f788)) (define-fun f791 () Arctic (+ f47 f789)) (define-fun f792 () Arctic (+ (* f30 f784) (* f31 f786))) (define-fun f793 () Arctic (+ (* f30 f785) (* f31 f787))) (define-fun f794 () Arctic (+ (* f32 f784) (* f33 f786))) (define-fun f795 () Arctic (+ (* f32 f785) (* f33 f787))) (define-fun f796 () Arctic (+ (* f30 f790) (* f31 f791))) (define-fun f797 () Arctic (+ (* f32 f790) (* f33 f791))) (define-fun f798 () Arctic (+ f34 f796)) (define-fun f799 () Arctic (+ f35 f797)) (define-fun f800 () Arctic (+ (* f30 f42) (* f31 f44))) (define-fun f801 () Arctic (+ (* f30 f43) (* f31 f45))) (define-fun f802 () Arctic (+ (* f32 f42) (* f33 f44))) (define-fun f803 () Arctic (+ (* f32 f43) (* f33 f45))) (define-fun f804 () Arctic (+ (* f30 f46) (* f31 f47))) (define-fun f805 () Arctic (+ (* f32 f46) (* f33 f47))) (define-fun f806 () Arctic (+ f34 f804)) (define-fun f807 () Arctic (+ f35 f805)) (define-fun f808 () Arctic (+ (* f48 f12) (* f49 f14))) (define-fun f809 () Arctic (+ (* f48 f13) (* f49 f15))) (define-fun f810 () Arctic (+ (* f50 f12) (* f51 f14))) (define-fun f811 () Arctic (+ (* f50 f13) (* f51 f15))) (define-fun f812 () Arctic (+ (* f48 f16) (* f49 f17))) (define-fun f813 () Arctic (+ (* f50 f16) (* f51 f17))) (define-fun f814 () Arctic (+ f52 f812)) (define-fun f815 () Arctic (+ f53 f813)) (define-fun f816 () Arctic (+ (* f0 f808) (* f1 f810))) (define-fun f817 () Arctic (+ (* f0 f809) (* f1 f811))) (define-fun f818 () Arctic (+ (* f2 f808) (* f3 f810))) (define-fun f819 () Arctic (+ (* f2 f809) (* f3 f811))) (define-fun f820 () Arctic (+ (* f0 f814) (* f1 f815))) (define-fun f821 () Arctic (+ (* f2 f814) (* f3 f815))) (define-fun f822 () Arctic (+ f4 f820)) (define-fun f823 () Arctic (+ f5 f821)) (define-fun f824 () Arctic (+ (* f12 f54) (* f13 f56))) (define-fun f825 () Arctic (+ (* f12 f55) (* f13 f57))) (define-fun f826 () Arctic (+ (* f14 f54) (* f15 f56))) (define-fun f827 () Arctic (+ (* f14 f55) (* f15 f57))) (define-fun f828 () Arctic (+ (* f12 f58) (* f13 f59))) (define-fun f829 () Arctic (+ (* f14 f58) (* f15 f59))) (define-fun f830 () Arctic (+ f16 f828)) (define-fun f831 () Arctic (+ f17 f829)) (define-fun f832 () Arctic (+ (* f30 f824) (* f31 f826))) (define-fun f833 () Arctic (+ (* f30 f825) (* f31 f827))) (define-fun f834 () Arctic (+ (* f32 f824) (* f33 f826))) (define-fun f835 () Arctic (+ (* f32 f825) (* f33 f827))) (define-fun f836 () Arctic (+ (* f30 f830) (* f31 f831))) (define-fun f837 () Arctic (+ (* f32 f830) (* f33 f831))) (define-fun f838 () Arctic (+ f34 f836)) (define-fun f839 () Arctic (+ f35 f837)) (define-fun f840 () Arctic (+ (* f48 f12) (* f49 f14))) (define-fun f841 () Arctic (+ (* f48 f13) (* f49 f15))) (define-fun f842 () Arctic (+ (* f50 f12) (* f51 f14))) (define-fun f843 () Arctic (+ (* f50 f13) (* f51 f15))) (define-fun f844 () Arctic (+ (* f48 f16) (* f49 f17))) (define-fun f845 () Arctic (+ (* f50 f16) (* f51 f17))) (define-fun f846 () Arctic (+ f52 f844)) (define-fun f847 () Arctic (+ f53 f845)) (define-fun f848 () Arctic (+ (* f0 f840) (* f1 f842))) (define-fun f849 () Arctic (+ (* f0 f841) (* f1 f843))) (define-fun f850 () Arctic (+ (* f2 f840) (* f3 f842))) (define-fun f851 () Arctic (+ (* f2 f841) (* f3 f843))) (define-fun f852 () Arctic (+ (* f0 f846) (* f1 f847))) (define-fun f853 () Arctic (+ (* f2 f846) (* f3 f847))) (define-fun f854 () Arctic (+ f4 f852)) (define-fun f855 () Arctic (+ f5 f853)) (define-fun f856 () Arctic (+ (* f0 f54) (* f1 f56))) (define-fun f857 () Arctic (+ (* f0 f55) (* f1 f57))) (define-fun f858 () Arctic (+ (* f2 f54) (* f3 f56))) (define-fun f859 () Arctic (+ (* f2 f55) (* f3 f57))) (define-fun f860 () Arctic (+ (* f0 f58) (* f1 f59))) (define-fun f861 () Arctic (+ (* f2 f58) (* f3 f59))) (define-fun f862 () Arctic (+ f4 f860)) (define-fun f863 () Arctic (+ f5 f861)) (define-fun f864 () Arctic (+ (* f48 f18) (* f49 f20))) (define-fun f865 () Arctic (+ (* f48 f19) (* f49 f21))) (define-fun f866 () Arctic (+ (* f50 f18) (* f51 f20))) (define-fun f867 () Arctic (+ (* f50 f19) (* f51 f21))) (define-fun f868 () Arctic (+ (* f48 f22) (* f49 f23))) (define-fun f869 () Arctic (+ (* f50 f22) (* f51 f23))) (define-fun f870 () Arctic (+ f52 f868)) (define-fun f871 () Arctic (+ f53 f869)) (define-fun f872 () Arctic (+ (* f0 f864) (* f1 f866))) (define-fun f873 () Arctic (+ (* f0 f865) (* f1 f867))) (define-fun f874 () Arctic (+ (* f2 f864) (* f3 f866))) (define-fun f875 () Arctic (+ (* f2 f865) (* f3 f867))) (define-fun f876 () Arctic (+ (* f0 f870) (* f1 f871))) (define-fun f877 () Arctic (+ (* f2 f870) (* f3 f871))) (define-fun f878 () Arctic (+ f4 f876)) (define-fun f879 () Arctic (+ f5 f877)) (define-fun f880 () Arctic (+ (* f54 f18) (* f55 f20))) (define-fun f881 () Arctic (+ (* f54 f19) (* f55 f21))) (define-fun f882 () Arctic (+ (* f56 f18) (* f57 f20))) (define-fun f883 () Arctic (+ (* f56 f19) (* f57 f21))) (define-fun f884 () Arctic (+ (* f54 f22) (* f55 f23))) (define-fun f885 () Arctic (+ (* f56 f22) (* f57 f23))) (define-fun f886 () Arctic (+ f58 f884)) (define-fun f887 () Arctic (+ f59 f885)) (define-fun f888 () Arctic (+ (* f0 f880) (* f1 f882))) (define-fun f889 () Arctic (+ (* f0 f881) (* f1 f883))) (define-fun f890 () Arctic (+ (* f2 f880) (* f3 f882))) (define-fun f891 () Arctic (+ (* f2 f881) (* f3 f883))) (define-fun f892 () Arctic (+ (* f0 f886) (* f1 f887))) (define-fun f893 () Arctic (+ (* f2 f886) (* f3 f887))) (define-fun f894 () Arctic (+ f4 f892)) (define-fun f895 () Arctic (+ f5 f893)) (define-fun f896 () Arctic (+ (* f48 f24) (* f49 f26))) (define-fun f897 () Arctic (+ (* f48 f25) (* f49 f27))) (define-fun f898 () Arctic (+ (* f50 f24) (* f51 f26))) (define-fun f899 () Arctic (+ (* f50 f25) (* f51 f27))) (define-fun f900 () Arctic (+ (* f48 f28) (* f49 f29))) (define-fun f901 () Arctic (+ (* f50 f28) (* f51 f29))) (define-fun f902 () Arctic (+ f52 f900)) (define-fun f903 () Arctic (+ f53 f901)) (define-fun f904 () Arctic (+ (* f0 f896) (* f1 f898))) (define-fun f905 () Arctic (+ (* f0 f897) (* f1 f899))) (define-fun f906 () Arctic (+ (* f2 f896) (* f3 f898))) (define-fun f907 () Arctic (+ (* f2 f897) (* f3 f899))) (define-fun f908 () Arctic (+ (* f0 f902) (* f1 f903))) (define-fun f909 () Arctic (+ (* f2 f902) (* f3 f903))) (define-fun f910 () Arctic (+ f4 f908)) (define-fun f911 () Arctic (+ f5 f909)) (define-fun f912 () Arctic (+ (* f24 f54) (* f25 f56))) (define-fun f913 () Arctic (+ (* f24 f55) (* f25 f57))) (define-fun f914 () Arctic (+ (* f26 f54) (* f27 f56))) (define-fun f915 () Arctic (+ (* f26 f55) (* f27 f57))) (define-fun f916 () Arctic (+ (* f24 f58) (* f25 f59))) (define-fun f917 () Arctic (+ (* f26 f58) (* f27 f59))) (define-fun f918 () Arctic (+ f28 f916)) (define-fun f919 () Arctic (+ f29 f917)) (define-fun f920 () Arctic (+ (* f30 f912) (* f31 f914))) (define-fun f921 () Arctic (+ (* f30 f913) (* f31 f915))) (define-fun f922 () Arctic (+ (* f32 f912) (* f33 f914))) (define-fun f923 () Arctic (+ (* f32 f913) (* f33 f915))) (define-fun f924 () Arctic (+ (* f30 f918) (* f31 f919))) (define-fun f925 () Arctic (+ (* f32 f918) (* f33 f919))) (define-fun f926 () Arctic (+ f34 f924)) (define-fun f927 () Arctic (+ f35 f925)) (define-fun f928 () Arctic (+ (* f48 f24) (* f49 f26))) (define-fun f929 () Arctic (+ (* f48 f25) (* f49 f27))) (define-fun f930 () Arctic (+ (* f50 f24) (* f51 f26))) (define-fun f931 () Arctic (+ (* f50 f25) (* f51 f27))) (define-fun f932 () Arctic (+ (* f48 f28) (* f49 f29))) (define-fun f933 () Arctic (+ (* f50 f28) (* f51 f29))) (define-fun f934 () Arctic (+ f52 f932)) (define-fun f935 () Arctic (+ f53 f933)) (define-fun f936 () Arctic (+ (* f0 f928) (* f1 f930))) (define-fun f937 () Arctic (+ (* f0 f929) (* f1 f931))) (define-fun f938 () Arctic (+ (* f2 f928) (* f3 f930))) (define-fun f939 () Arctic (+ (* f2 f929) (* f3 f931))) (define-fun f940 () Arctic (+ (* f0 f934) (* f1 f935))) (define-fun f941 () Arctic (+ (* f2 f934) (* f3 f935))) (define-fun f942 () Arctic (+ f4 f940)) (define-fun f943 () Arctic (+ f5 f941)) (define-fun f944 () Arctic (+ (* f30 f54) (* f31 f56))) (define-fun f945 () Arctic (+ (* f30 f55) (* f31 f57))) (define-fun f946 () Arctic (+ (* f32 f54) (* f33 f56))) (define-fun f947 () Arctic (+ (* f32 f55) (* f33 f57))) (define-fun f948 () Arctic (+ (* f30 f58) (* f31 f59))) (define-fun f949 () Arctic (+ (* f32 f58) (* f33 f59))) (define-fun f950 () Arctic (+ f34 f948)) (define-fun f951 () Arctic (+ f35 f949)) (define-fun f952 () Arctic (+ (* f54 f12) (* f55 f14))) (define-fun f953 () Arctic (+ (* f54 f13) (* f55 f15))) (define-fun f954 () Arctic (+ (* f56 f12) (* f57 f14))) (define-fun f955 () Arctic (+ (* f56 f13) (* f57 f15))) (define-fun f956 () Arctic (+ (* f54 f16) (* f55 f17))) (define-fun f957 () Arctic (+ (* f56 f16) (* f57 f17))) (define-fun f958 () Arctic (+ f58 f956)) (define-fun f959 () Arctic (+ f59 f957)) (define-fun f960 () Arctic (+ (* f30 f952) (* f31 f954))) (define-fun f961 () Arctic (+ (* f30 f953) (* f31 f955))) (define-fun f962 () Arctic (+ (* f32 f952) (* f33 f954))) (define-fun f963 () Arctic (+ (* f32 f953) (* f33 f955))) (define-fun f964 () Arctic (+ (* f30 f958) (* f31 f959))) (define-fun f965 () Arctic (+ (* f32 f958) (* f33 f959))) (define-fun f966 () Arctic (+ f34 f964)) (define-fun f967 () Arctic (+ f35 f965)) (define-fun f968 () Arctic (+ (* f12 f36) (* f13 f38))) (define-fun f969 () Arctic (+ (* f12 f37) (* f13 f39))) (define-fun f970 () Arctic (+ (* f14 f36) (* f15 f38))) (define-fun f971 () Arctic (+ (* f14 f37) (* f15 f39))) (define-fun f972 () Arctic (+ (* f12 f40) (* f13 f41))) (define-fun f973 () Arctic (+ (* f14 f40) (* f15 f41))) (define-fun f974 () Arctic (+ f16 f972)) (define-fun f975 () Arctic (+ f17 f973)) (define-fun f976 () Arctic (+ (* f0 f968) (* f1 f970))) (define-fun f977 () Arctic (+ (* f0 f969) (* f1 f971))) (define-fun f978 () Arctic (+ (* f2 f968) (* f3 f970))) (define-fun f979 () Arctic (+ (* f2 f969) (* f3 f971))) (define-fun f980 () Arctic (+ (* f0 f974) (* f1 f975))) (define-fun f981 () Arctic (+ (* f2 f974) (* f3 f975))) (define-fun f982 () Arctic (+ f4 f980)) (define-fun f983 () Arctic (+ f5 f981)) (define-fun f984 () Arctic (+ (* f54 f12) (* f55 f14))) (define-fun f985 () Arctic (+ (* f54 f13) (* f55 f15))) (define-fun f986 () Arctic (+ (* f56 f12) (* f57 f14))) (define-fun f987 () Arctic (+ (* f56 f13) (* f57 f15))) (define-fun f988 () Arctic (+ (* f54 f16) (* f55 f17))) (define-fun f989 () Arctic (+ (* f56 f16) (* f57 f17))) (define-fun f990 () Arctic (+ f58 f988)) (define-fun f991 () Arctic (+ f59 f989)) (define-fun f992 () Arctic (+ (* f30 f984) (* f31 f986))) (define-fun f993 () Arctic (+ (* f30 f985) (* f31 f987))) (define-fun f994 () Arctic (+ (* f32 f984) (* f33 f986))) (define-fun f995 () Arctic (+ (* f32 f985) (* f33 f987))) (define-fun f996 () Arctic (+ (* f30 f990) (* f31 f991))) (define-fun f997 () Arctic (+ (* f32 f990) (* f33 f991))) (define-fun f998 () Arctic (+ f34 f996)) (define-fun f999 () Arctic (+ f35 f997)) (define-fun f1000 () Arctic (+ (* f0 f36) (* f1 f38))) (define-fun f1001 () Arctic (+ (* f0 f37) (* f1 f39))) (define-fun f1002 () Arctic (+ (* f2 f36) (* f3 f38))) (define-fun f1003 () Arctic (+ (* f2 f37) (* f3 f39))) (define-fun f1004 () Arctic (+ (* f0 f40) (* f1 f41))) (define-fun f1005 () Arctic (+ (* f2 f40) (* f3 f41))) (define-fun f1006 () Arctic (+ f4 f1004)) (define-fun f1007 () Arctic (+ f5 f1005)) (define-fun f1008 () Arctic (+ (* f54 f18) (* f55 f20))) (define-fun f1009 () Arctic (+ (* f54 f19) (* f55 f21))) (define-fun f1010 () Arctic (+ (* f56 f18) (* f57 f20))) (define-fun f1011 () Arctic (+ (* f56 f19) (* f57 f21))) (define-fun f1012 () Arctic (+ (* f54 f22) (* f55 f23))) (define-fun f1013 () Arctic (+ (* f56 f22) (* f57 f23))) (define-fun f1014 () Arctic (+ f58 f1012)) (define-fun f1015 () Arctic (+ f59 f1013)) (define-fun f1016 () Arctic (+ (* f30 f1008) (* f31 f1010))) (define-fun f1017 () Arctic (+ (* f30 f1009) (* f31 f1011))) (define-fun f1018 () Arctic (+ (* f32 f1008) (* f33 f1010))) (define-fun f1019 () Arctic (+ (* f32 f1009) (* f33 f1011))) (define-fun f1020 () Arctic (+ (* f30 f1014) (* f31 f1015))) (define-fun f1021 () Arctic (+ (* f32 f1014) (* f33 f1015))) (define-fun f1022 () Arctic (+ f34 f1020)) (define-fun f1023 () Arctic (+ f35 f1021)) (define-fun f1024 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f1025 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f1026 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f1027 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f1028 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f1029 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f1030 () Arctic (+ f40 f1028)) (define-fun f1031 () Arctic (+ f41 f1029)) (define-fun f1032 () Arctic (+ (* f12 f1024) (* f13 f1026))) (define-fun f1033 () Arctic (+ (* f12 f1025) (* f13 f1027))) (define-fun f1034 () Arctic (+ (* f14 f1024) (* f15 f1026))) (define-fun f1035 () Arctic (+ (* f14 f1025) (* f15 f1027))) (define-fun f1036 () Arctic (+ (* f12 f1030) (* f13 f1031))) (define-fun f1037 () Arctic (+ (* f14 f1030) (* f15 f1031))) (define-fun f1038 () Arctic (+ f16 f1036)) (define-fun f1039 () Arctic (+ f17 f1037)) (define-fun f1040 () Arctic (+ (* f0 f1032) (* f1 f1034))) (define-fun f1041 () Arctic (+ (* f0 f1033) (* f1 f1035))) (define-fun f1042 () Arctic (+ (* f2 f1032) (* f3 f1034))) (define-fun f1043 () Arctic (+ (* f2 f1033) (* f3 f1035))) (define-fun f1044 () Arctic (+ (* f0 f1038) (* f1 f1039))) (define-fun f1045 () Arctic (+ (* f2 f1038) (* f3 f1039))) (define-fun f1046 () Arctic (+ f4 f1044)) (define-fun f1047 () Arctic (+ f5 f1045)) (define-fun f1048 () Arctic (+ (* f54 f18) (* f55 f20))) (define-fun f1049 () Arctic (+ (* f54 f19) (* f55 f21))) (define-fun f1050 () Arctic (+ (* f56 f18) (* f57 f20))) (define-fun f1051 () Arctic (+ (* f56 f19) (* f57 f21))) (define-fun f1052 () Arctic (+ (* f54 f22) (* f55 f23))) (define-fun f1053 () Arctic (+ (* f56 f22) (* f57 f23))) (define-fun f1054 () Arctic (+ f58 f1052)) (define-fun f1055 () Arctic (+ f59 f1053)) (define-fun f1056 () Arctic (+ (* f30 f1048) (* f31 f1050))) (define-fun f1057 () Arctic (+ (* f30 f1049) (* f31 f1051))) (define-fun f1058 () Arctic (+ (* f32 f1048) (* f33 f1050))) (define-fun f1059 () Arctic (+ (* f32 f1049) (* f33 f1051))) (define-fun f1060 () Arctic (+ (* f30 f1054) (* f31 f1055))) (define-fun f1061 () Arctic (+ (* f32 f1054) (* f33 f1055))) (define-fun f1062 () Arctic (+ f34 f1060)) (define-fun f1063 () Arctic (+ f35 f1061)) (define-fun f1064 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f1065 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f1066 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f1067 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f1068 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f1069 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f1070 () Arctic (+ f40 f1068)) (define-fun f1071 () Arctic (+ f41 f1069)) (define-fun f1072 () Arctic (+ (* f0 f1064) (* f1 f1066))) (define-fun f1073 () Arctic (+ (* f0 f1065) (* f1 f1067))) (define-fun f1074 () Arctic (+ (* f2 f1064) (* f3 f1066))) (define-fun f1075 () Arctic (+ (* f2 f1065) (* f3 f1067))) (define-fun f1076 () Arctic (+ (* f0 f1070) (* f1 f1071))) (define-fun f1077 () Arctic (+ (* f2 f1070) (* f3 f1071))) (define-fun f1078 () Arctic (+ f4 f1076)) (define-fun f1079 () Arctic (+ f5 f1077)) (define-fun f1080 () Arctic (+ (* f54 f24) (* f55 f26))) (define-fun f1081 () Arctic (+ (* f54 f25) (* f55 f27))) (define-fun f1082 () Arctic (+ (* f56 f24) (* f57 f26))) (define-fun f1083 () Arctic (+ (* f56 f25) (* f57 f27))) (define-fun f1084 () Arctic (+ (* f54 f28) (* f55 f29))) (define-fun f1085 () Arctic (+ (* f56 f28) (* f57 f29))) (define-fun f1086 () Arctic (+ f58 f1084)) (define-fun f1087 () Arctic (+ f59 f1085)) (define-fun f1088 () Arctic (+ (* f30 f1080) (* f31 f1082))) (define-fun f1089 () Arctic (+ (* f30 f1081) (* f31 f1083))) (define-fun f1090 () Arctic (+ (* f32 f1080) (* f33 f1082))) (define-fun f1091 () Arctic (+ (* f32 f1081) (* f33 f1083))) (define-fun f1092 () Arctic (+ (* f30 f1086) (* f31 f1087))) (define-fun f1093 () Arctic (+ (* f32 f1086) (* f33 f1087))) (define-fun f1094 () Arctic (+ f34 f1092)) (define-fun f1095 () Arctic (+ f35 f1093)) (define-fun f1096 () Arctic (+ (* f24 f36) (* f25 f38))) (define-fun f1097 () Arctic (+ (* f24 f37) (* f25 f39))) (define-fun f1098 () Arctic (+ (* f26 f36) (* f27 f38))) (define-fun f1099 () Arctic (+ (* f26 f37) (* f27 f39))) (define-fun f1100 () Arctic (+ (* f24 f40) (* f25 f41))) (define-fun f1101 () Arctic (+ (* f26 f40) (* f27 f41))) (define-fun f1102 () Arctic (+ f28 f1100)) (define-fun f1103 () Arctic (+ f29 f1101)) (define-fun f1104 () Arctic (+ (* f0 f1096) (* f1 f1098))) (define-fun f1105 () Arctic (+ (* f0 f1097) (* f1 f1099))) (define-fun f1106 () Arctic (+ (* f2 f1096) (* f3 f1098))) (define-fun f1107 () Arctic (+ (* f2 f1097) (* f3 f1099))) (define-fun f1108 () Arctic (+ (* f0 f1102) (* f1 f1103))) (define-fun f1109 () Arctic (+ (* f2 f1102) (* f3 f1103))) (define-fun f1110 () Arctic (+ f4 f1108)) (define-fun f1111 () Arctic (+ f5 f1109)) (define-fun f1112 () Arctic (+ (* f54 f24) (* f55 f26))) (define-fun f1113 () Arctic (+ (* f54 f25) (* f55 f27))) (define-fun f1114 () Arctic (+ (* f56 f24) (* f57 f26))) (define-fun f1115 () Arctic (+ (* f56 f25) (* f57 f27))) (define-fun f1116 () Arctic (+ (* f54 f28) (* f55 f29))) (define-fun f1117 () Arctic (+ (* f56 f28) (* f57 f29))) (define-fun f1118 () Arctic (+ f58 f1116)) (define-fun f1119 () Arctic (+ f59 f1117)) (define-fun f1120 () Arctic (+ (* f30 f1112) (* f31 f1114))) (define-fun f1121 () Arctic (+ (* f30 f1113) (* f31 f1115))) (define-fun f1122 () Arctic (+ (* f32 f1112) (* f33 f1114))) (define-fun f1123 () Arctic (+ (* f32 f1113) (* f33 f1115))) (define-fun f1124 () Arctic (+ (* f30 f1118) (* f31 f1119))) (define-fun f1125 () Arctic (+ (* f32 f1118) (* f33 f1119))) (define-fun f1126 () Arctic (+ f34 f1124)) (define-fun f1127 () Arctic (+ f35 f1125)) (define-fun f1128 () Arctic (+ (* f30 f36) (* f31 f38))) (define-fun f1129 () Arctic (+ (* f30 f37) (* f31 f39))) (define-fun f1130 () Arctic (+ (* f32 f36) (* f33 f38))) (define-fun f1131 () Arctic (+ (* f32 f37) (* f33 f39))) (define-fun f1132 () Arctic (+ (* f30 f40) (* f31 f41))) (define-fun f1133 () Arctic (+ (* f32 f40) (* f33 f41))) (define-fun f1134 () Arctic (+ f34 f1132)) (define-fun f1135 () Arctic (+ f35 f1133)) (define-fun f1136 () Arctic (+ (* f60 f66) (* f61 f68))) (define-fun f1137 () Arctic (+ (* f60 f67) (* f61 f69))) (define-fun f1138 () Arctic (+ (* f62 f66) (* f63 f68))) (define-fun f1139 () Arctic (+ (* f62 f67) (* f63 f69))) (define-fun f1140 () Arctic (+ (* f60 f70) (* f61 f71))) (define-fun f1141 () Arctic (+ (* f62 f70) (* f63 f71))) (define-fun f1142 () Arctic (+ f64 f1140)) (define-fun f1143 () Arctic (+ f65 f1141)) (define-fun f1144 () Arctic (+ (* f12 f66) (* f13 f68))) (define-fun f1145 () Arctic (+ (* f12 f67) (* f13 f69))) (define-fun f1146 () Arctic (+ (* f14 f66) (* f15 f68))) (define-fun f1147 () Arctic (+ (* f14 f67) (* f15 f69))) (define-fun f1148 () Arctic (+ (* f12 f70) (* f13 f71))) (define-fun f1149 () Arctic (+ (* f14 f70) (* f15 f71))) (define-fun f1150 () Arctic (+ f16 f1148)) (define-fun f1151 () Arctic (+ f17 f1149)) (define-fun f1152 () Arctic (+ (* f60 f1144) (* f61 f1146))) (define-fun f1153 () Arctic (+ (* f60 f1145) (* f61 f1147))) (define-fun f1154 () Arctic (+ (* f62 f1144) (* f63 f1146))) (define-fun f1155 () Arctic (+ (* f62 f1145) (* f63 f1147))) (define-fun f1156 () Arctic (+ (* f60 f1150) (* f61 f1151))) (define-fun f1157 () Arctic (+ (* f62 f1150) (* f63 f1151))) (define-fun f1158 () Arctic (+ f64 f1156)) (define-fun f1159 () Arctic (+ f65 f1157)) (define-fun f1160 () Arctic (+ (* f60 f48) (* f61 f50))) (define-fun f1161 () Arctic (+ (* f60 f49) (* f61 f51))) (define-fun f1162 () Arctic (+ (* f62 f48) (* f63 f50))) (define-fun f1163 () Arctic (+ (* f62 f49) (* f63 f51))) (define-fun f1164 () Arctic (+ (* f60 f52) (* f61 f53))) (define-fun f1165 () Arctic (+ (* f62 f52) (* f63 f53))) (define-fun f1166 () Arctic (+ f64 f1164)) (define-fun f1167 () Arctic (+ f65 f1165)) (define-fun f1168 () Arctic (+ (* f12 f48) (* f13 f50))) (define-fun f1169 () Arctic (+ (* f12 f49) (* f13 f51))) (define-fun f1170 () Arctic (+ (* f14 f48) (* f15 f50))) (define-fun f1171 () Arctic (+ (* f14 f49) (* f15 f51))) (define-fun f1172 () Arctic (+ (* f12 f52) (* f13 f53))) (define-fun f1173 () Arctic (+ (* f14 f52) (* f15 f53))) (define-fun f1174 () Arctic (+ f16 f1172)) (define-fun f1175 () Arctic (+ f17 f1173)) (define-fun f1176 () Arctic (+ (* f60 f1168) (* f61 f1170))) (define-fun f1177 () Arctic (+ (* f60 f1169) (* f61 f1171))) (define-fun f1178 () Arctic (+ (* f62 f1168) (* f63 f1170))) (define-fun f1179 () Arctic (+ (* f62 f1169) (* f63 f1171))) (define-fun f1180 () Arctic (+ (* f60 f1174) (* f61 f1175))) (define-fun f1181 () Arctic (+ (* f62 f1174) (* f63 f1175))) (define-fun f1182 () Arctic (+ f64 f1180)) (define-fun f1183 () Arctic (+ f65 f1181)) (define-fun f1184 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f1185 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f1186 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f1187 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f1188 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f1189 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f1190 () Arctic (+ f10 f1188)) (define-fun f1191 () Arctic (+ f11 f1189)) (define-fun f1192 () Arctic (+ (* f12 f1184) (* f13 f1186))) (define-fun f1193 () Arctic (+ (* f12 f1185) (* f13 f1187))) (define-fun f1194 () Arctic (+ (* f14 f1184) (* f15 f1186))) (define-fun f1195 () Arctic (+ (* f14 f1185) (* f15 f1187))) (define-fun f1196 () Arctic (+ (* f12 f1190) (* f13 f1191))) (define-fun f1197 () Arctic (+ (* f14 f1190) (* f15 f1191))) (define-fun f1198 () Arctic (+ f16 f1196)) (define-fun f1199 () Arctic (+ f17 f1197)) (define-fun f1200 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1201 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1202 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1203 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1204 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1205 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1206 () Arctic (+ f16 f1204)) (define-fun f1207 () Arctic (+ f17 f1205)) (define-fun f1208 () Arctic (+ (* f12 f1200) (* f13 f1202))) (define-fun f1209 () Arctic (+ (* f12 f1201) (* f13 f1203))) (define-fun f1210 () Arctic (+ (* f14 f1200) (* f15 f1202))) (define-fun f1211 () Arctic (+ (* f14 f1201) (* f15 f1203))) (define-fun f1212 () Arctic (+ (* f12 f1206) (* f13 f1207))) (define-fun f1213 () Arctic (+ (* f14 f1206) (* f15 f1207))) (define-fun f1214 () Arctic (+ f16 f1212)) (define-fun f1215 () Arctic (+ f17 f1213)) (define-fun f1216 () Arctic (+ (* f6 f18) (* f7 f20))) (define-fun f1217 () Arctic (+ (* f6 f19) (* f7 f21))) (define-fun f1218 () Arctic (+ (* f8 f18) (* f9 f20))) (define-fun f1219 () Arctic (+ (* f8 f19) (* f9 f21))) (define-fun f1220 () Arctic (+ (* f6 f22) (* f7 f23))) (define-fun f1221 () Arctic (+ (* f8 f22) (* f9 f23))) (define-fun f1222 () Arctic (+ f10 f1220)) (define-fun f1223 () Arctic (+ f11 f1221)) (define-fun f1224 () Arctic (+ (* f12 f1216) (* f13 f1218))) (define-fun f1225 () Arctic (+ (* f12 f1217) (* f13 f1219))) (define-fun f1226 () Arctic (+ (* f14 f1216) (* f15 f1218))) (define-fun f1227 () Arctic (+ (* f14 f1217) (* f15 f1219))) (define-fun f1228 () Arctic (+ (* f12 f1222) (* f13 f1223))) (define-fun f1229 () Arctic (+ (* f14 f1222) (* f15 f1223))) (define-fun f1230 () Arctic (+ f16 f1228)) (define-fun f1231 () Arctic (+ f17 f1229)) (define-fun f1232 () Arctic (+ (* f6 f18) (* f7 f20))) (define-fun f1233 () Arctic (+ (* f6 f19) (* f7 f21))) (define-fun f1234 () Arctic (+ (* f8 f18) (* f9 f20))) (define-fun f1235 () Arctic (+ (* f8 f19) (* f9 f21))) (define-fun f1236 () Arctic (+ (* f6 f22) (* f7 f23))) (define-fun f1237 () Arctic (+ (* f8 f22) (* f9 f23))) (define-fun f1238 () Arctic (+ f10 f1236)) (define-fun f1239 () Arctic (+ f11 f1237)) (define-fun f1240 () Arctic (+ (* f12 f1232) (* f13 f1234))) (define-fun f1241 () Arctic (+ (* f12 f1233) (* f13 f1235))) (define-fun f1242 () Arctic (+ (* f14 f1232) (* f15 f1234))) (define-fun f1243 () Arctic (+ (* f14 f1233) (* f15 f1235))) (define-fun f1244 () Arctic (+ (* f12 f1238) (* f13 f1239))) (define-fun f1245 () Arctic (+ (* f14 f1238) (* f15 f1239))) (define-fun f1246 () Arctic (+ f16 f1244)) (define-fun f1247 () Arctic (+ f17 f1245)) (define-fun f1248 () Arctic (+ (* f12 f1240) (* f13 f1242))) (define-fun f1249 () Arctic (+ (* f12 f1241) (* f13 f1243))) (define-fun f1250 () Arctic (+ (* f14 f1240) (* f15 f1242))) (define-fun f1251 () Arctic (+ (* f14 f1241) (* f15 f1243))) (define-fun f1252 () Arctic (+ (* f12 f1246) (* f13 f1247))) (define-fun f1253 () Arctic (+ (* f14 f1246) (* f15 f1247))) (define-fun f1254 () Arctic (+ f16 f1252)) (define-fun f1255 () Arctic (+ f17 f1253)) (define-fun f1256 () Arctic (+ (* f6 f24) (* f7 f26))) (define-fun f1257 () Arctic (+ (* f6 f25) (* f7 f27))) (define-fun f1258 () Arctic (+ (* f8 f24) (* f9 f26))) (define-fun f1259 () Arctic (+ (* f8 f25) (* f9 f27))) (define-fun f1260 () Arctic (+ (* f6 f28) (* f7 f29))) (define-fun f1261 () Arctic (+ (* f8 f28) (* f9 f29))) (define-fun f1262 () Arctic (+ f10 f1260)) (define-fun f1263 () Arctic (+ f11 f1261)) (define-fun f1264 () Arctic (+ (* f12 f1256) (* f13 f1258))) (define-fun f1265 () Arctic (+ (* f12 f1257) (* f13 f1259))) (define-fun f1266 () Arctic (+ (* f14 f1256) (* f15 f1258))) (define-fun f1267 () Arctic (+ (* f14 f1257) (* f15 f1259))) (define-fun f1268 () Arctic (+ (* f12 f1262) (* f13 f1263))) (define-fun f1269 () Arctic (+ (* f14 f1262) (* f15 f1263))) (define-fun f1270 () Arctic (+ f16 f1268)) (define-fun f1271 () Arctic (+ f17 f1269)) (define-fun f1272 () Arctic (+ (* f24 f6) (* f25 f8))) (define-fun f1273 () Arctic (+ (* f24 f7) (* f25 f9))) (define-fun f1274 () Arctic (+ (* f26 f6) (* f27 f8))) (define-fun f1275 () Arctic (+ (* f26 f7) (* f27 f9))) (define-fun f1276 () Arctic (+ (* f24 f10) (* f25 f11))) (define-fun f1277 () Arctic (+ (* f26 f10) (* f27 f11))) (define-fun f1278 () Arctic (+ f28 f1276)) (define-fun f1279 () Arctic (+ f29 f1277)) (define-fun f1280 () Arctic (+ (* f12 f1272) (* f13 f1274))) (define-fun f1281 () Arctic (+ (* f12 f1273) (* f13 f1275))) (define-fun f1282 () Arctic (+ (* f14 f1272) (* f15 f1274))) (define-fun f1283 () Arctic (+ (* f14 f1273) (* f15 f1275))) (define-fun f1284 () Arctic (+ (* f12 f1278) (* f13 f1279))) (define-fun f1285 () Arctic (+ (* f14 f1278) (* f15 f1279))) (define-fun f1286 () Arctic (+ f16 f1284)) (define-fun f1287 () Arctic (+ f17 f1285)) (define-fun f1288 () Arctic (+ (* f36 f12) (* f37 f14))) (define-fun f1289 () Arctic (+ (* f36 f13) (* f37 f15))) (define-fun f1290 () Arctic (+ (* f38 f12) (* f39 f14))) (define-fun f1291 () Arctic (+ (* f38 f13) (* f39 f15))) (define-fun f1292 () Arctic (+ (* f36 f16) (* f37 f17))) (define-fun f1293 () Arctic (+ (* f38 f16) (* f39 f17))) (define-fun f1294 () Arctic (+ f40 f1292)) (define-fun f1295 () Arctic (+ f41 f1293)) (define-fun f1296 () Arctic (+ (* f24 f1288) (* f25 f1290))) (define-fun f1297 () Arctic (+ (* f24 f1289) (* f25 f1291))) (define-fun f1298 () Arctic (+ (* f26 f1288) (* f27 f1290))) (define-fun f1299 () Arctic (+ (* f26 f1289) (* f27 f1291))) (define-fun f1300 () Arctic (+ (* f24 f1294) (* f25 f1295))) (define-fun f1301 () Arctic (+ (* f26 f1294) (* f27 f1295))) (define-fun f1302 () Arctic (+ f28 f1300)) (define-fun f1303 () Arctic (+ f29 f1301)) (define-fun f1304 () Arctic (+ (* f12 f36) (* f13 f38))) (define-fun f1305 () Arctic (+ (* f12 f37) (* f13 f39))) (define-fun f1306 () Arctic (+ (* f14 f36) (* f15 f38))) (define-fun f1307 () Arctic (+ (* f14 f37) (* f15 f39))) (define-fun f1308 () Arctic (+ (* f12 f40) (* f13 f41))) (define-fun f1309 () Arctic (+ (* f14 f40) (* f15 f41))) (define-fun f1310 () Arctic (+ f16 f1308)) (define-fun f1311 () Arctic (+ f17 f1309)) (define-fun f1312 () Arctic (+ (* f24 f1304) (* f25 f1306))) (define-fun f1313 () Arctic (+ (* f24 f1305) (* f25 f1307))) (define-fun f1314 () Arctic (+ (* f26 f1304) (* f27 f1306))) (define-fun f1315 () Arctic (+ (* f26 f1305) (* f27 f1307))) (define-fun f1316 () Arctic (+ (* f24 f1310) (* f25 f1311))) (define-fun f1317 () Arctic (+ (* f26 f1310) (* f27 f1311))) (define-fun f1318 () Arctic (+ f28 f1316)) (define-fun f1319 () Arctic (+ f29 f1317)) (define-fun f1320 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f1321 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f1322 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f1323 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f1324 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f1325 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f1326 () Arctic (+ f40 f1324)) (define-fun f1327 () Arctic (+ f41 f1325)) (define-fun f1328 () Arctic (+ (* f24 f1320) (* f25 f1322))) (define-fun f1329 () Arctic (+ (* f24 f1321) (* f25 f1323))) (define-fun f1330 () Arctic (+ (* f26 f1320) (* f27 f1322))) (define-fun f1331 () Arctic (+ (* f26 f1321) (* f27 f1323))) (define-fun f1332 () Arctic (+ (* f24 f1326) (* f25 f1327))) (define-fun f1333 () Arctic (+ (* f26 f1326) (* f27 f1327))) (define-fun f1334 () Arctic (+ f28 f1332)) (define-fun f1335 () Arctic (+ f29 f1333)) (define-fun f1336 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f1337 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f1338 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f1339 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f1340 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f1341 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f1342 () Arctic (+ f40 f1340)) (define-fun f1343 () Arctic (+ f41 f1341)) (define-fun f1344 () Arctic (+ (* f12 f1336) (* f13 f1338))) (define-fun f1345 () Arctic (+ (* f12 f1337) (* f13 f1339))) (define-fun f1346 () Arctic (+ (* f14 f1336) (* f15 f1338))) (define-fun f1347 () Arctic (+ (* f14 f1337) (* f15 f1339))) (define-fun f1348 () Arctic (+ (* f12 f1342) (* f13 f1343))) (define-fun f1349 () Arctic (+ (* f14 f1342) (* f15 f1343))) (define-fun f1350 () Arctic (+ f16 f1348)) (define-fun f1351 () Arctic (+ f17 f1349)) (define-fun f1352 () Arctic (+ (* f24 f1344) (* f25 f1346))) (define-fun f1353 () Arctic (+ (* f24 f1345) (* f25 f1347))) (define-fun f1354 () Arctic (+ (* f26 f1344) (* f27 f1346))) (define-fun f1355 () Arctic (+ (* f26 f1345) (* f27 f1347))) (define-fun f1356 () Arctic (+ (* f24 f1350) (* f25 f1351))) (define-fun f1357 () Arctic (+ (* f26 f1350) (* f27 f1351))) (define-fun f1358 () Arctic (+ f28 f1356)) (define-fun f1359 () Arctic (+ f29 f1357)) (define-fun f1360 () Arctic (+ (* f36 f24) (* f37 f26))) (define-fun f1361 () Arctic (+ (* f36 f25) (* f37 f27))) (define-fun f1362 () Arctic (+ (* f38 f24) (* f39 f26))) (define-fun f1363 () Arctic (+ (* f38 f25) (* f39 f27))) (define-fun f1364 () Arctic (+ (* f36 f28) (* f37 f29))) (define-fun f1365 () Arctic (+ (* f38 f28) (* f39 f29))) (define-fun f1366 () Arctic (+ f40 f1364)) (define-fun f1367 () Arctic (+ f41 f1365)) (define-fun f1368 () Arctic (+ (* f24 f1360) (* f25 f1362))) (define-fun f1369 () Arctic (+ (* f24 f1361) (* f25 f1363))) (define-fun f1370 () Arctic (+ (* f26 f1360) (* f27 f1362))) (define-fun f1371 () Arctic (+ (* f26 f1361) (* f27 f1363))) (define-fun f1372 () Arctic (+ (* f24 f1366) (* f25 f1367))) (define-fun f1373 () Arctic (+ (* f26 f1366) (* f27 f1367))) (define-fun f1374 () Arctic (+ f28 f1372)) (define-fun f1375 () Arctic (+ f29 f1373)) (define-fun f1376 () Arctic (+ (* f24 f36) (* f25 f38))) (define-fun f1377 () Arctic (+ (* f24 f37) (* f25 f39))) (define-fun f1378 () Arctic (+ (* f26 f36) (* f27 f38))) (define-fun f1379 () Arctic (+ (* f26 f37) (* f27 f39))) (define-fun f1380 () Arctic (+ (* f24 f40) (* f25 f41))) (define-fun f1381 () Arctic (+ (* f26 f40) (* f27 f41))) (define-fun f1382 () Arctic (+ f28 f1380)) (define-fun f1383 () Arctic (+ f29 f1381)) (define-fun f1384 () Arctic (+ (* f24 f1376) (* f25 f1378))) (define-fun f1385 () Arctic (+ (* f24 f1377) (* f25 f1379))) (define-fun f1386 () Arctic (+ (* f26 f1376) (* f27 f1378))) (define-fun f1387 () Arctic (+ (* f26 f1377) (* f27 f1379))) (define-fun f1388 () Arctic (+ (* f24 f1382) (* f25 f1383))) (define-fun f1389 () Arctic (+ (* f26 f1382) (* f27 f1383))) (define-fun f1390 () Arctic (+ f28 f1388)) (define-fun f1391 () Arctic (+ f29 f1389)) (define-fun f1392 () Arctic (+ (* f36 f12) (* f37 f14))) (define-fun f1393 () Arctic (+ (* f36 f13) (* f37 f15))) (define-fun f1394 () Arctic (+ (* f38 f12) (* f39 f14))) (define-fun f1395 () Arctic (+ (* f38 f13) (* f39 f15))) (define-fun f1396 () Arctic (+ (* f36 f16) (* f37 f17))) (define-fun f1397 () Arctic (+ (* f38 f16) (* f39 f17))) (define-fun f1398 () Arctic (+ f40 f1396)) (define-fun f1399 () Arctic (+ f41 f1397)) (define-fun f1400 () Arctic (+ (* f12 f1392) (* f13 f1394))) (define-fun f1401 () Arctic (+ (* f12 f1393) (* f13 f1395))) (define-fun f1402 () Arctic (+ (* f14 f1392) (* f15 f1394))) (define-fun f1403 () Arctic (+ (* f14 f1393) (* f15 f1395))) (define-fun f1404 () Arctic (+ (* f12 f1398) (* f13 f1399))) (define-fun f1405 () Arctic (+ (* f14 f1398) (* f15 f1399))) (define-fun f1406 () Arctic (+ f16 f1404)) (define-fun f1407 () Arctic (+ f17 f1405)) (define-fun f1408 () Arctic (+ (* f12 f42) (* f13 f44))) (define-fun f1409 () Arctic (+ (* f12 f43) (* f13 f45))) (define-fun f1410 () Arctic (+ (* f14 f42) (* f15 f44))) (define-fun f1411 () Arctic (+ (* f14 f43) (* f15 f45))) (define-fun f1412 () Arctic (+ (* f12 f46) (* f13 f47))) (define-fun f1413 () Arctic (+ (* f14 f46) (* f15 f47))) (define-fun f1414 () Arctic (+ f16 f1412)) (define-fun f1415 () Arctic (+ f17 f1413)) (define-fun f1416 () Arctic (+ (* f12 f1408) (* f13 f1410))) (define-fun f1417 () Arctic (+ (* f12 f1409) (* f13 f1411))) (define-fun f1418 () Arctic (+ (* f14 f1408) (* f15 f1410))) (define-fun f1419 () Arctic (+ (* f14 f1409) (* f15 f1411))) (define-fun f1420 () Arctic (+ (* f12 f1414) (* f13 f1415))) (define-fun f1421 () Arctic (+ (* f14 f1414) (* f15 f1415))) (define-fun f1422 () Arctic (+ f16 f1420)) (define-fun f1423 () Arctic (+ f17 f1421)) (define-fun f1424 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f1425 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f1426 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f1427 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f1428 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f1429 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f1430 () Arctic (+ f40 f1428)) (define-fun f1431 () Arctic (+ f41 f1429)) (define-fun f1432 () Arctic (+ (* f12 f1424) (* f13 f1426))) (define-fun f1433 () Arctic (+ (* f12 f1425) (* f13 f1427))) (define-fun f1434 () Arctic (+ (* f14 f1424) (* f15 f1426))) (define-fun f1435 () Arctic (+ (* f14 f1425) (* f15 f1427))) (define-fun f1436 () Arctic (+ (* f12 f1430) (* f13 f1431))) (define-fun f1437 () Arctic (+ (* f14 f1430) (* f15 f1431))) (define-fun f1438 () Arctic (+ f16 f1436)) (define-fun f1439 () Arctic (+ f17 f1437)) (define-fun f1440 () Arctic (+ (* f42 f18) (* f43 f20))) (define-fun f1441 () Arctic (+ (* f42 f19) (* f43 f21))) (define-fun f1442 () Arctic (+ (* f44 f18) (* f45 f20))) (define-fun f1443 () Arctic (+ (* f44 f19) (* f45 f21))) (define-fun f1444 () Arctic (+ (* f42 f22) (* f43 f23))) (define-fun f1445 () Arctic (+ (* f44 f22) (* f45 f23))) (define-fun f1446 () Arctic (+ f46 f1444)) (define-fun f1447 () Arctic (+ f47 f1445)) (define-fun f1448 () Arctic (+ (* f12 f1440) (* f13 f1442))) (define-fun f1449 () Arctic (+ (* f12 f1441) (* f13 f1443))) (define-fun f1450 () Arctic (+ (* f14 f1440) (* f15 f1442))) (define-fun f1451 () Arctic (+ (* f14 f1441) (* f15 f1443))) (define-fun f1452 () Arctic (+ (* f12 f1446) (* f13 f1447))) (define-fun f1453 () Arctic (+ (* f14 f1446) (* f15 f1447))) (define-fun f1454 () Arctic (+ f16 f1452)) (define-fun f1455 () Arctic (+ f17 f1453)) (define-fun f1456 () Arctic (+ (* f12 f1448) (* f13 f1450))) (define-fun f1457 () Arctic (+ (* f12 f1449) (* f13 f1451))) (define-fun f1458 () Arctic (+ (* f14 f1448) (* f15 f1450))) (define-fun f1459 () Arctic (+ (* f14 f1449) (* f15 f1451))) (define-fun f1460 () Arctic (+ (* f12 f1454) (* f13 f1455))) (define-fun f1461 () Arctic (+ (* f14 f1454) (* f15 f1455))) (define-fun f1462 () Arctic (+ f16 f1460)) (define-fun f1463 () Arctic (+ f17 f1461)) (define-fun f1464 () Arctic (+ (* f36 f24) (* f37 f26))) (define-fun f1465 () Arctic (+ (* f36 f25) (* f37 f27))) (define-fun f1466 () Arctic (+ (* f38 f24) (* f39 f26))) (define-fun f1467 () Arctic (+ (* f38 f25) (* f39 f27))) (define-fun f1468 () Arctic (+ (* f36 f28) (* f37 f29))) (define-fun f1469 () Arctic (+ (* f38 f28) (* f39 f29))) (define-fun f1470 () Arctic (+ f40 f1468)) (define-fun f1471 () Arctic (+ f41 f1469)) (define-fun f1472 () Arctic (+ (* f12 f1464) (* f13 f1466))) (define-fun f1473 () Arctic (+ (* f12 f1465) (* f13 f1467))) (define-fun f1474 () Arctic (+ (* f14 f1464) (* f15 f1466))) (define-fun f1475 () Arctic (+ (* f14 f1465) (* f15 f1467))) (define-fun f1476 () Arctic (+ (* f12 f1470) (* f13 f1471))) (define-fun f1477 () Arctic (+ (* f14 f1470) (* f15 f1471))) (define-fun f1478 () Arctic (+ f16 f1476)) (define-fun f1479 () Arctic (+ f17 f1477)) (define-fun f1480 () Arctic (+ (* f24 f42) (* f25 f44))) (define-fun f1481 () Arctic (+ (* f24 f43) (* f25 f45))) (define-fun f1482 () Arctic (+ (* f26 f42) (* f27 f44))) (define-fun f1483 () Arctic (+ (* f26 f43) (* f27 f45))) (define-fun f1484 () Arctic (+ (* f24 f46) (* f25 f47))) (define-fun f1485 () Arctic (+ (* f26 f46) (* f27 f47))) (define-fun f1486 () Arctic (+ f28 f1484)) (define-fun f1487 () Arctic (+ f29 f1485)) (define-fun f1488 () Arctic (+ (* f12 f1480) (* f13 f1482))) (define-fun f1489 () Arctic (+ (* f12 f1481) (* f13 f1483))) (define-fun f1490 () Arctic (+ (* f14 f1480) (* f15 f1482))) (define-fun f1491 () Arctic (+ (* f14 f1481) (* f15 f1483))) (define-fun f1492 () Arctic (+ (* f12 f1486) (* f13 f1487))) (define-fun f1493 () Arctic (+ (* f14 f1486) (* f15 f1487))) (define-fun f1494 () Arctic (+ f16 f1492)) (define-fun f1495 () Arctic (+ f17 f1493)) (define-fun f1496 () Arctic (+ (* f42 f12) (* f43 f14))) (define-fun f1497 () Arctic (+ (* f42 f13) (* f43 f15))) (define-fun f1498 () Arctic (+ (* f44 f12) (* f45 f14))) (define-fun f1499 () Arctic (+ (* f44 f13) (* f45 f15))) (define-fun f1500 () Arctic (+ (* f42 f16) (* f43 f17))) (define-fun f1501 () Arctic (+ (* f44 f16) (* f45 f17))) (define-fun f1502 () Arctic (+ f46 f1500)) (define-fun f1503 () Arctic (+ f47 f1501)) (define-fun f1504 () Arctic (+ (* f24 f1496) (* f25 f1498))) (define-fun f1505 () Arctic (+ (* f24 f1497) (* f25 f1499))) (define-fun f1506 () Arctic (+ (* f26 f1496) (* f27 f1498))) (define-fun f1507 () Arctic (+ (* f26 f1497) (* f27 f1499))) (define-fun f1508 () Arctic (+ (* f24 f1502) (* f25 f1503))) (define-fun f1509 () Arctic (+ (* f26 f1502) (* f27 f1503))) (define-fun f1510 () Arctic (+ f28 f1508)) (define-fun f1511 () Arctic (+ f29 f1509)) (define-fun f1512 () Arctic (+ (* f12 f42) (* f13 f44))) (define-fun f1513 () Arctic (+ (* f12 f43) (* f13 f45))) (define-fun f1514 () Arctic (+ (* f14 f42) (* f15 f44))) (define-fun f1515 () Arctic (+ (* f14 f43) (* f15 f45))) (define-fun f1516 () Arctic (+ (* f12 f46) (* f13 f47))) (define-fun f1517 () Arctic (+ (* f14 f46) (* f15 f47))) (define-fun f1518 () Arctic (+ f16 f1516)) (define-fun f1519 () Arctic (+ f17 f1517)) (define-fun f1520 () Arctic (+ (* f24 f1512) (* f25 f1514))) (define-fun f1521 () Arctic (+ (* f24 f1513) (* f25 f1515))) (define-fun f1522 () Arctic (+ (* f26 f1512) (* f27 f1514))) (define-fun f1523 () Arctic (+ (* f26 f1513) (* f27 f1515))) (define-fun f1524 () Arctic (+ (* f24 f1518) (* f25 f1519))) (define-fun f1525 () Arctic (+ (* f26 f1518) (* f27 f1519))) (define-fun f1526 () Arctic (+ f28 f1524)) (define-fun f1527 () Arctic (+ f29 f1525)) (define-fun f1528 () Arctic (+ (* f42 f18) (* f43 f20))) (define-fun f1529 () Arctic (+ (* f42 f19) (* f43 f21))) (define-fun f1530 () Arctic (+ (* f44 f18) (* f45 f20))) (define-fun f1531 () Arctic (+ (* f44 f19) (* f45 f21))) (define-fun f1532 () Arctic (+ (* f42 f22) (* f43 f23))) (define-fun f1533 () Arctic (+ (* f44 f22) (* f45 f23))) (define-fun f1534 () Arctic (+ f46 f1532)) (define-fun f1535 () Arctic (+ f47 f1533)) (define-fun f1536 () Arctic (+ (* f24 f1528) (* f25 f1530))) (define-fun f1537 () Arctic (+ (* f24 f1529) (* f25 f1531))) (define-fun f1538 () Arctic (+ (* f26 f1528) (* f27 f1530))) (define-fun f1539 () Arctic (+ (* f26 f1529) (* f27 f1531))) (define-fun f1540 () Arctic (+ (* f24 f1534) (* f25 f1535))) (define-fun f1541 () Arctic (+ (* f26 f1534) (* f27 f1535))) (define-fun f1542 () Arctic (+ f28 f1540)) (define-fun f1543 () Arctic (+ f29 f1541)) (define-fun f1544 () Arctic (+ (* f42 f18) (* f43 f20))) (define-fun f1545 () Arctic (+ (* f42 f19) (* f43 f21))) (define-fun f1546 () Arctic (+ (* f44 f18) (* f45 f20))) (define-fun f1547 () Arctic (+ (* f44 f19) (* f45 f21))) (define-fun f1548 () Arctic (+ (* f42 f22) (* f43 f23))) (define-fun f1549 () Arctic (+ (* f44 f22) (* f45 f23))) (define-fun f1550 () Arctic (+ f46 f1548)) (define-fun f1551 () Arctic (+ f47 f1549)) (define-fun f1552 () Arctic (+ (* f12 f1544) (* f13 f1546))) (define-fun f1553 () Arctic (+ (* f12 f1545) (* f13 f1547))) (define-fun f1554 () Arctic (+ (* f14 f1544) (* f15 f1546))) (define-fun f1555 () Arctic (+ (* f14 f1545) (* f15 f1547))) (define-fun f1556 () Arctic (+ (* f12 f1550) (* f13 f1551))) (define-fun f1557 () Arctic (+ (* f14 f1550) (* f15 f1551))) (define-fun f1558 () Arctic (+ f16 f1556)) (define-fun f1559 () Arctic (+ f17 f1557)) (define-fun f1560 () Arctic (+ (* f24 f1552) (* f25 f1554))) (define-fun f1561 () Arctic (+ (* f24 f1553) (* f25 f1555))) (define-fun f1562 () Arctic (+ (* f26 f1552) (* f27 f1554))) (define-fun f1563 () Arctic (+ (* f26 f1553) (* f27 f1555))) (define-fun f1564 () Arctic (+ (* f24 f1558) (* f25 f1559))) (define-fun f1565 () Arctic (+ (* f26 f1558) (* f27 f1559))) (define-fun f1566 () Arctic (+ f28 f1564)) (define-fun f1567 () Arctic (+ f29 f1565)) (define-fun f1568 () Arctic (+ (* f42 f24) (* f43 f26))) (define-fun f1569 () Arctic (+ (* f42 f25) (* f43 f27))) (define-fun f1570 () Arctic (+ (* f44 f24) (* f45 f26))) (define-fun f1571 () Arctic (+ (* f44 f25) (* f45 f27))) (define-fun f1572 () Arctic (+ (* f42 f28) (* f43 f29))) (define-fun f1573 () Arctic (+ (* f44 f28) (* f45 f29))) (define-fun f1574 () Arctic (+ f46 f1572)) (define-fun f1575 () Arctic (+ f47 f1573)) (define-fun f1576 () Arctic (+ (* f24 f1568) (* f25 f1570))) (define-fun f1577 () Arctic (+ (* f24 f1569) (* f25 f1571))) (define-fun f1578 () Arctic (+ (* f26 f1568) (* f27 f1570))) (define-fun f1579 () Arctic (+ (* f26 f1569) (* f27 f1571))) (define-fun f1580 () Arctic (+ (* f24 f1574) (* f25 f1575))) (define-fun f1581 () Arctic (+ (* f26 f1574) (* f27 f1575))) (define-fun f1582 () Arctic (+ f28 f1580)) (define-fun f1583 () Arctic (+ f29 f1581)) (define-fun f1584 () Arctic (+ (* f24 f42) (* f25 f44))) (define-fun f1585 () Arctic (+ (* f24 f43) (* f25 f45))) (define-fun f1586 () Arctic (+ (* f26 f42) (* f27 f44))) (define-fun f1587 () Arctic (+ (* f26 f43) (* f27 f45))) (define-fun f1588 () Arctic (+ (* f24 f46) (* f25 f47))) (define-fun f1589 () Arctic (+ (* f26 f46) (* f27 f47))) (define-fun f1590 () Arctic (+ f28 f1588)) (define-fun f1591 () Arctic (+ f29 f1589)) (define-fun f1592 () Arctic (+ (* f24 f1584) (* f25 f1586))) (define-fun f1593 () Arctic (+ (* f24 f1585) (* f25 f1587))) (define-fun f1594 () Arctic (+ (* f26 f1584) (* f27 f1586))) (define-fun f1595 () Arctic (+ (* f26 f1585) (* f27 f1587))) (define-fun f1596 () Arctic (+ (* f24 f1590) (* f25 f1591))) (define-fun f1597 () Arctic (+ (* f26 f1590) (* f27 f1591))) (define-fun f1598 () Arctic (+ f28 f1596)) (define-fun f1599 () Arctic (+ f29 f1597)) (define-fun f1600 () Arctic (+ (* f12 f42) (* f13 f44))) (define-fun f1601 () Arctic (+ (* f12 f43) (* f13 f45))) (define-fun f1602 () Arctic (+ (* f14 f42) (* f15 f44))) (define-fun f1603 () Arctic (+ (* f14 f43) (* f15 f45))) (define-fun f1604 () Arctic (+ (* f12 f46) (* f13 f47))) (define-fun f1605 () Arctic (+ (* f14 f46) (* f15 f47))) (define-fun f1606 () Arctic (+ f16 f1604)) (define-fun f1607 () Arctic (+ f17 f1605)) (define-fun f1608 () Arctic (+ (* f66 f24) (* f67 f26))) (define-fun f1609 () Arctic (+ (* f66 f25) (* f67 f27))) (define-fun f1610 () Arctic (+ (* f68 f24) (* f69 f26))) (define-fun f1611 () Arctic (+ (* f68 f25) (* f69 f27))) (define-fun f1612 () Arctic (+ (* f66 f28) (* f67 f29))) (define-fun f1613 () Arctic (+ (* f68 f28) (* f69 f29))) (define-fun f1614 () Arctic (+ f70 f1612)) (define-fun f1615 () Arctic (+ f71 f1613)) (define-fun f1616 () Arctic (+ (* f24 f66) (* f25 f68))) (define-fun f1617 () Arctic (+ (* f24 f67) (* f25 f69))) (define-fun f1618 () Arctic (+ (* f26 f66) (* f27 f68))) (define-fun f1619 () Arctic (+ (* f26 f67) (* f27 f69))) (define-fun f1620 () Arctic (+ (* f24 f70) (* f25 f71))) (define-fun f1621 () Arctic (+ (* f26 f70) (* f27 f71))) (define-fun f1622 () Arctic (+ f28 f1620)) (define-fun f1623 () Arctic (+ f29 f1621)) (define-fun f1624 () Arctic (+ (* f66 f24) (* f67 f26))) (define-fun f1625 () Arctic (+ (* f66 f25) (* f67 f27))) (define-fun f1626 () Arctic (+ (* f68 f24) (* f69 f26))) (define-fun f1627 () Arctic (+ (* f68 f25) (* f69 f27))) (define-fun f1628 () Arctic (+ (* f66 f28) (* f67 f29))) (define-fun f1629 () Arctic (+ (* f68 f28) (* f69 f29))) (define-fun f1630 () Arctic (+ f70 f1628)) (define-fun f1631 () Arctic (+ f71 f1629)) (define-fun f1632 () Arctic (+ (* f12 f66) (* f13 f68))) (define-fun f1633 () Arctic (+ (* f12 f67) (* f13 f69))) (define-fun f1634 () Arctic (+ (* f14 f66) (* f15 f68))) (define-fun f1635 () Arctic (+ (* f14 f67) (* f15 f69))) (define-fun f1636 () Arctic (+ (* f12 f70) (* f13 f71))) (define-fun f1637 () Arctic (+ (* f14 f70) (* f15 f71))) (define-fun f1638 () Arctic (+ f16 f1636)) (define-fun f1639 () Arctic (+ f17 f1637)) (define-fun f1640 () Arctic (+ (* f48 f12) (* f49 f14))) (define-fun f1641 () Arctic (+ (* f48 f13) (* f49 f15))) (define-fun f1642 () Arctic (+ (* f50 f12) (* f51 f14))) (define-fun f1643 () Arctic (+ (* f50 f13) (* f51 f15))) (define-fun f1644 () Arctic (+ (* f48 f16) (* f49 f17))) (define-fun f1645 () Arctic (+ (* f50 f16) (* f51 f17))) (define-fun f1646 () Arctic (+ f52 f1644)) (define-fun f1647 () Arctic (+ f53 f1645)) (define-fun f1648 () Arctic (+ (* f24 f48) (* f25 f50))) (define-fun f1649 () Arctic (+ (* f24 f49) (* f25 f51))) (define-fun f1650 () Arctic (+ (* f26 f48) (* f27 f50))) (define-fun f1651 () Arctic (+ (* f26 f49) (* f27 f51))) (define-fun f1652 () Arctic (+ (* f24 f52) (* f25 f53))) (define-fun f1653 () Arctic (+ (* f26 f52) (* f27 f53))) (define-fun f1654 () Arctic (+ f28 f1652)) (define-fun f1655 () Arctic (+ f29 f1653)) (define-fun f1656 () Arctic (+ (* f48 f24) (* f49 f26))) (define-fun f1657 () Arctic (+ (* f48 f25) (* f49 f27))) (define-fun f1658 () Arctic (+ (* f50 f24) (* f51 f26))) (define-fun f1659 () Arctic (+ (* f50 f25) (* f51 f27))) (define-fun f1660 () Arctic (+ (* f48 f28) (* f49 f29))) (define-fun f1661 () Arctic (+ (* f50 f28) (* f51 f29))) (define-fun f1662 () Arctic (+ f52 f1660)) (define-fun f1663 () Arctic (+ f53 f1661)) (define-fun f1664 () Arctic (+ (* f48 f12) (* f49 f14))) (define-fun f1665 () Arctic (+ (* f48 f13) (* f49 f15))) (define-fun f1666 () Arctic (+ (* f50 f12) (* f51 f14))) (define-fun f1667 () Arctic (+ (* f50 f13) (* f51 f15))) (define-fun f1668 () Arctic (+ (* f48 f16) (* f49 f17))) (define-fun f1669 () Arctic (+ (* f50 f16) (* f51 f17))) (define-fun f1670 () Arctic (+ f52 f1668)) (define-fun f1671 () Arctic (+ f53 f1669)) (define-fun f1672 () Arctic (+ (* f12 f1664) (* f13 f1666))) (define-fun f1673 () Arctic (+ (* f12 f1665) (* f13 f1667))) (define-fun f1674 () Arctic (+ (* f14 f1664) (* f15 f1666))) (define-fun f1675 () Arctic (+ (* f14 f1665) (* f15 f1667))) (define-fun f1676 () Arctic (+ (* f12 f1670) (* f13 f1671))) (define-fun f1677 () Arctic (+ (* f14 f1670) (* f15 f1671))) (define-fun f1678 () Arctic (+ f16 f1676)) (define-fun f1679 () Arctic (+ f17 f1677)) (define-fun f1680 () Arctic (+ (* f12 f54) (* f13 f56))) (define-fun f1681 () Arctic (+ (* f12 f55) (* f13 f57))) (define-fun f1682 () Arctic (+ (* f14 f54) (* f15 f56))) (define-fun f1683 () Arctic (+ (* f14 f55) (* f15 f57))) (define-fun f1684 () Arctic (+ (* f12 f58) (* f13 f59))) (define-fun f1685 () Arctic (+ (* f14 f58) (* f15 f59))) (define-fun f1686 () Arctic (+ f16 f1684)) (define-fun f1687 () Arctic (+ f17 f1685)) (define-fun f1688 () Arctic (+ (* f24 f1680) (* f25 f1682))) (define-fun f1689 () Arctic (+ (* f24 f1681) (* f25 f1683))) (define-fun f1690 () Arctic (+ (* f26 f1680) (* f27 f1682))) (define-fun f1691 () Arctic (+ (* f26 f1681) (* f27 f1683))) (define-fun f1692 () Arctic (+ (* f24 f1686) (* f25 f1687))) (define-fun f1693 () Arctic (+ (* f26 f1686) (* f27 f1687))) (define-fun f1694 () Arctic (+ f28 f1692)) (define-fun f1695 () Arctic (+ f29 f1693)) (define-fun f1696 () Arctic (+ (* f48 f18) (* f49 f20))) (define-fun f1697 () Arctic (+ (* f48 f19) (* f49 f21))) (define-fun f1698 () Arctic (+ (* f50 f18) (* f51 f20))) (define-fun f1699 () Arctic (+ (* f50 f19) (* f51 f21))) (define-fun f1700 () Arctic (+ (* f48 f22) (* f49 f23))) (define-fun f1701 () Arctic (+ (* f50 f22) (* f51 f23))) (define-fun f1702 () Arctic (+ f52 f1700)) (define-fun f1703 () Arctic (+ f53 f1701)) (define-fun f1704 () Arctic (+ (* f12 f1696) (* f13 f1698))) (define-fun f1705 () Arctic (+ (* f12 f1697) (* f13 f1699))) (define-fun f1706 () Arctic (+ (* f14 f1696) (* f15 f1698))) (define-fun f1707 () Arctic (+ (* f14 f1697) (* f15 f1699))) (define-fun f1708 () Arctic (+ (* f12 f1702) (* f13 f1703))) (define-fun f1709 () Arctic (+ (* f14 f1702) (* f15 f1703))) (define-fun f1710 () Arctic (+ f16 f1708)) (define-fun f1711 () Arctic (+ f17 f1709)) (define-fun f1712 () Arctic (+ (* f54 f18) (* f55 f20))) (define-fun f1713 () Arctic (+ (* f54 f19) (* f55 f21))) (define-fun f1714 () Arctic (+ (* f56 f18) (* f57 f20))) (define-fun f1715 () Arctic (+ (* f56 f19) (* f57 f21))) (define-fun f1716 () Arctic (+ (* f54 f22) (* f55 f23))) (define-fun f1717 () Arctic (+ (* f56 f22) (* f57 f23))) (define-fun f1718 () Arctic (+ f58 f1716)) (define-fun f1719 () Arctic (+ f59 f1717)) (define-fun f1720 () Arctic (+ (* f12 f1712) (* f13 f1714))) (define-fun f1721 () Arctic (+ (* f12 f1713) (* f13 f1715))) (define-fun f1722 () Arctic (+ (* f14 f1712) (* f15 f1714))) (define-fun f1723 () Arctic (+ (* f14 f1713) (* f15 f1715))) (define-fun f1724 () Arctic (+ (* f12 f1718) (* f13 f1719))) (define-fun f1725 () Arctic (+ (* f14 f1718) (* f15 f1719))) (define-fun f1726 () Arctic (+ f16 f1724)) (define-fun f1727 () Arctic (+ f17 f1725)) (define-fun f1728 () Arctic (+ (* f24 f1720) (* f25 f1722))) (define-fun f1729 () Arctic (+ (* f24 f1721) (* f25 f1723))) (define-fun f1730 () Arctic (+ (* f26 f1720) (* f27 f1722))) (define-fun f1731 () Arctic (+ (* f26 f1721) (* f27 f1723))) (define-fun f1732 () Arctic (+ (* f24 f1726) (* f25 f1727))) (define-fun f1733 () Arctic (+ (* f26 f1726) (* f27 f1727))) (define-fun f1734 () Arctic (+ f28 f1732)) (define-fun f1735 () Arctic (+ f29 f1733)) (define-fun f1736 () Arctic (+ (* f48 f24) (* f49 f26))) (define-fun f1737 () Arctic (+ (* f48 f25) (* f49 f27))) (define-fun f1738 () Arctic (+ (* f50 f24) (* f51 f26))) (define-fun f1739 () Arctic (+ (* f50 f25) (* f51 f27))) (define-fun f1740 () Arctic (+ (* f48 f28) (* f49 f29))) (define-fun f1741 () Arctic (+ (* f50 f28) (* f51 f29))) (define-fun f1742 () Arctic (+ f52 f1740)) (define-fun f1743 () Arctic (+ f53 f1741)) (define-fun f1744 () Arctic (+ (* f12 f1736) (* f13 f1738))) (define-fun f1745 () Arctic (+ (* f12 f1737) (* f13 f1739))) (define-fun f1746 () Arctic (+ (* f14 f1736) (* f15 f1738))) (define-fun f1747 () Arctic (+ (* f14 f1737) (* f15 f1739))) (define-fun f1748 () Arctic (+ (* f12 f1742) (* f13 f1743))) (define-fun f1749 () Arctic (+ (* f14 f1742) (* f15 f1743))) (define-fun f1750 () Arctic (+ f16 f1748)) (define-fun f1751 () Arctic (+ f17 f1749)) (define-fun f1752 () Arctic (+ (* f24 f54) (* f25 f56))) (define-fun f1753 () Arctic (+ (* f24 f55) (* f25 f57))) (define-fun f1754 () Arctic (+ (* f26 f54) (* f27 f56))) (define-fun f1755 () Arctic (+ (* f26 f55) (* f27 f57))) (define-fun f1756 () Arctic (+ (* f24 f58) (* f25 f59))) (define-fun f1757 () Arctic (+ (* f26 f58) (* f27 f59))) (define-fun f1758 () Arctic (+ f28 f1756)) (define-fun f1759 () Arctic (+ f29 f1757)) (define-fun f1760 () Arctic (+ (* f24 f1752) (* f25 f1754))) (define-fun f1761 () Arctic (+ (* f24 f1753) (* f25 f1755))) (define-fun f1762 () Arctic (+ (* f26 f1752) (* f27 f1754))) (define-fun f1763 () Arctic (+ (* f26 f1753) (* f27 f1755))) (define-fun f1764 () Arctic (+ (* f24 f1758) (* f25 f1759))) (define-fun f1765 () Arctic (+ (* f26 f1758) (* f27 f1759))) (define-fun f1766 () Arctic (+ f28 f1764)) (define-fun f1767 () Arctic (+ f29 f1765)) (define-fun f1768 () Arctic (+ (* f54 f12) (* f55 f14))) (define-fun f1769 () Arctic (+ (* f54 f13) (* f55 f15))) (define-fun f1770 () Arctic (+ (* f56 f12) (* f57 f14))) (define-fun f1771 () Arctic (+ (* f56 f13) (* f57 f15))) (define-fun f1772 () Arctic (+ (* f54 f16) (* f55 f17))) (define-fun f1773 () Arctic (+ (* f56 f16) (* f57 f17))) (define-fun f1774 () Arctic (+ f58 f1772)) (define-fun f1775 () Arctic (+ f59 f1773)) (define-fun f1776 () Arctic (+ (* f24 f1768) (* f25 f1770))) (define-fun f1777 () Arctic (+ (* f24 f1769) (* f25 f1771))) (define-fun f1778 () Arctic (+ (* f26 f1768) (* f27 f1770))) (define-fun f1779 () Arctic (+ (* f26 f1769) (* f27 f1771))) (define-fun f1780 () Arctic (+ (* f24 f1774) (* f25 f1775))) (define-fun f1781 () Arctic (+ (* f26 f1774) (* f27 f1775))) (define-fun f1782 () Arctic (+ f28 f1780)) (define-fun f1783 () Arctic (+ f29 f1781)) (define-fun f1784 () Arctic (+ (* f12 f36) (* f13 f38))) (define-fun f1785 () Arctic (+ (* f12 f37) (* f13 f39))) (define-fun f1786 () Arctic (+ (* f14 f36) (* f15 f38))) (define-fun f1787 () Arctic (+ (* f14 f37) (* f15 f39))) (define-fun f1788 () Arctic (+ (* f12 f40) (* f13 f41))) (define-fun f1789 () Arctic (+ (* f14 f40) (* f15 f41))) (define-fun f1790 () Arctic (+ f16 f1788)) (define-fun f1791 () Arctic (+ f17 f1789)) (define-fun f1792 () Arctic (+ (* f12 f1784) (* f13 f1786))) (define-fun f1793 () Arctic (+ (* f12 f1785) (* f13 f1787))) (define-fun f1794 () Arctic (+ (* f14 f1784) (* f15 f1786))) (define-fun f1795 () Arctic (+ (* f14 f1785) (* f15 f1787))) (define-fun f1796 () Arctic (+ (* f12 f1790) (* f13 f1791))) (define-fun f1797 () Arctic (+ (* f14 f1790) (* f15 f1791))) (define-fun f1798 () Arctic (+ f16 f1796)) (define-fun f1799 () Arctic (+ f17 f1797)) (define-fun f1800 () Arctic (+ (* f54 f18) (* f55 f20))) (define-fun f1801 () Arctic (+ (* f54 f19) (* f55 f21))) (define-fun f1802 () Arctic (+ (* f56 f18) (* f57 f20))) (define-fun f1803 () Arctic (+ (* f56 f19) (* f57 f21))) (define-fun f1804 () Arctic (+ (* f54 f22) (* f55 f23))) (define-fun f1805 () Arctic (+ (* f56 f22) (* f57 f23))) (define-fun f1806 () Arctic (+ f58 f1804)) (define-fun f1807 () Arctic (+ f59 f1805)) (define-fun f1808 () Arctic (+ (* f24 f1800) (* f25 f1802))) (define-fun f1809 () Arctic (+ (* f24 f1801) (* f25 f1803))) (define-fun f1810 () Arctic (+ (* f26 f1800) (* f27 f1802))) (define-fun f1811 () Arctic (+ (* f26 f1801) (* f27 f1803))) (define-fun f1812 () Arctic (+ (* f24 f1806) (* f25 f1807))) (define-fun f1813 () Arctic (+ (* f26 f1806) (* f27 f1807))) (define-fun f1814 () Arctic (+ f28 f1812)) (define-fun f1815 () Arctic (+ f29 f1813)) (define-fun f1816 () Arctic (+ (* f36 f18) (* f37 f20))) (define-fun f1817 () Arctic (+ (* f36 f19) (* f37 f21))) (define-fun f1818 () Arctic (+ (* f38 f18) (* f39 f20))) (define-fun f1819 () Arctic (+ (* f38 f19) (* f39 f21))) (define-fun f1820 () Arctic (+ (* f36 f22) (* f37 f23))) (define-fun f1821 () Arctic (+ (* f38 f22) (* f39 f23))) (define-fun f1822 () Arctic (+ f40 f1820)) (define-fun f1823 () Arctic (+ f41 f1821)) (define-fun f1824 () Arctic (+ (* f12 f1816) (* f13 f1818))) (define-fun f1825 () Arctic (+ (* f12 f1817) (* f13 f1819))) (define-fun f1826 () Arctic (+ (* f14 f1816) (* f15 f1818))) (define-fun f1827 () Arctic (+ (* f14 f1817) (* f15 f1819))) (define-fun f1828 () Arctic (+ (* f12 f1822) (* f13 f1823))) (define-fun f1829 () Arctic (+ (* f14 f1822) (* f15 f1823))) (define-fun f1830 () Arctic (+ f16 f1828)) (define-fun f1831 () Arctic (+ f17 f1829)) (define-fun f1832 () Arctic (+ (* f12 f1824) (* f13 f1826))) (define-fun f1833 () Arctic (+ (* f12 f1825) (* f13 f1827))) (define-fun f1834 () Arctic (+ (* f14 f1824) (* f15 f1826))) (define-fun f1835 () Arctic (+ (* f14 f1825) (* f15 f1827))) (define-fun f1836 () Arctic (+ (* f12 f1830) (* f13 f1831))) (define-fun f1837 () Arctic (+ (* f14 f1830) (* f15 f1831))) (define-fun f1838 () Arctic (+ f16 f1836)) (define-fun f1839 () Arctic (+ f17 f1837)) (define-fun f1840 () Arctic (+ (* f54 f24) (* f55 f26))) (define-fun f1841 () Arctic (+ (* f54 f25) (* f55 f27))) (define-fun f1842 () Arctic (+ (* f56 f24) (* f57 f26))) (define-fun f1843 () Arctic (+ (* f56 f25) (* f57 f27))) (define-fun f1844 () Arctic (+ (* f54 f28) (* f55 f29))) (define-fun f1845 () Arctic (+ (* f56 f28) (* f57 f29))) (define-fun f1846 () Arctic (+ f58 f1844)) (define-fun f1847 () Arctic (+ f59 f1845)) (define-fun f1848 () Arctic (+ (* f24 f1840) (* f25 f1842))) (define-fun f1849 () Arctic (+ (* f24 f1841) (* f25 f1843))) (define-fun f1850 () Arctic (+ (* f26 f1840) (* f27 f1842))) (define-fun f1851 () Arctic (+ (* f26 f1841) (* f27 f1843))) (define-fun f1852 () Arctic (+ (* f24 f1846) (* f25 f1847))) (define-fun f1853 () Arctic (+ (* f26 f1846) (* f27 f1847))) (define-fun f1854 () Arctic (+ f28 f1852)) (define-fun f1855 () Arctic (+ f29 f1853)) (define-fun f1856 () Arctic (+ (* f24 f36) (* f25 f38))) (define-fun f1857 () Arctic (+ (* f24 f37) (* f25 f39))) (define-fun f1858 () Arctic (+ (* f26 f36) (* f27 f38))) (define-fun f1859 () Arctic (+ (* f26 f37) (* f27 f39))) (define-fun f1860 () Arctic (+ (* f24 f40) (* f25 f41))) (define-fun f1861 () Arctic (+ (* f26 f40) (* f27 f41))) (define-fun f1862 () Arctic (+ f28 f1860)) (define-fun f1863 () Arctic (+ f29 f1861)) (define-fun f1864 () Arctic (+ (* f12 f1856) (* f13 f1858))) (define-fun f1865 () Arctic (+ (* f12 f1857) (* f13 f1859))) (define-fun f1866 () Arctic (+ (* f14 f1856) (* f15 f1858))) (define-fun f1867 () Arctic (+ (* f14 f1857) (* f15 f1859))) (define-fun f1868 () Arctic (+ (* f12 f1862) (* f13 f1863))) (define-fun f1869 () Arctic (+ (* f14 f1862) (* f15 f1863))) (define-fun f1870 () Arctic (+ f16 f1868)) (define-fun f1871 () Arctic (+ f17 f1869)) (define-fun f1872 () Arctic (+ (* f18 f6) (* f19 f8))) (define-fun f1873 () Arctic (+ (* f18 f7) (* f19 f9))) (define-fun f1874 () Arctic (+ (* f20 f6) (* f21 f8))) (define-fun f1875 () Arctic (+ (* f20 f7) (* f21 f9))) (define-fun f1876 () Arctic (+ (* f18 f10) (* f19 f11))) (define-fun f1877 () Arctic (+ (* f20 f10) (* f21 f11))) (define-fun f1878 () Arctic (+ f22 f1876)) (define-fun f1879 () Arctic (+ f23 f1877)) (define-fun f1880 () Arctic (+ (* f12 f6) (* f13 f8))) (define-fun f1881 () Arctic (+ (* f12 f7) (* f13 f9))) (define-fun f1882 () Arctic (+ (* f14 f6) (* f15 f8))) (define-fun f1883 () Arctic (+ (* f14 f7) (* f15 f9))) (define-fun f1884 () Arctic (+ (* f12 f10) (* f13 f11))) (define-fun f1885 () Arctic (+ (* f14 f10) (* f15 f11))) (define-fun f1886 () Arctic (+ f16 f1884)) (define-fun f1887 () Arctic (+ f17 f1885)) (define-fun f1888 () Arctic (+ (* f18 f1880) (* f19 f1882))) (define-fun f1889 () Arctic (+ (* f18 f1881) (* f19 f1883))) (define-fun f1890 () Arctic (+ (* f20 f1880) (* f21 f1882))) (define-fun f1891 () Arctic (+ (* f20 f1881) (* f21 f1883))) (define-fun f1892 () Arctic (+ (* f18 f1886) (* f19 f1887))) (define-fun f1893 () Arctic (+ (* f20 f1886) (* f21 f1887))) (define-fun f1894 () Arctic (+ f22 f1892)) (define-fun f1895 () Arctic (+ f23 f1893)) (define-fun f1896 () Arctic (+ (* f18 f36) (* f19 f38))) (define-fun f1897 () Arctic (+ (* f18 f37) (* f19 f39))) (define-fun f1898 () Arctic (+ (* f20 f36) (* f21 f38))) (define-fun f1899 () Arctic (+ (* f20 f37) (* f21 f39))) (define-fun f1900 () Arctic (+ (* f18 f40) (* f19 f41))) (define-fun f1901 () Arctic (+ (* f20 f40) (* f21 f41))) (define-fun f1902 () Arctic (+ f22 f1900)) (define-fun f1903 () Arctic (+ f23 f1901)) (define-fun f1904 () Arctic (+ (* f12 f36) (* f13 f38))) (define-fun f1905 () Arctic (+ (* f12 f37) (* f13 f39))) (define-fun f1906 () Arctic (+ (* f14 f36) (* f15 f38))) (define-fun f1907 () Arctic (+ (* f14 f37) (* f15 f39))) (define-fun f1908 () Arctic (+ (* f12 f40) (* f13 f41))) (define-fun f1909 () Arctic (+ (* f14 f40) (* f15 f41))) (define-fun f1910 () Arctic (+ f16 f1908)) (define-fun f1911 () Arctic (+ f17 f1909)) (define-fun f1912 () Arctic (+ (* f18 f1904) (* f19 f1906))) (define-fun f1913 () Arctic (+ (* f18 f1905) (* f19 f1907))) (define-fun f1914 () Arctic (+ (* f20 f1904) (* f21 f1906))) (define-fun f1915 () Arctic (+ (* f20 f1905) (* f21 f1907))) (define-fun f1916 () Arctic (+ (* f18 f1910) (* f19 f1911))) (define-fun f1917 () Arctic (+ (* f20 f1910) (* f21 f1911))) (define-fun f1918 () Arctic (+ f22 f1916)) (define-fun f1919 () Arctic (+ f23 f1917)) (define-fun f1920 () Arctic (+ (* f18 f42) (* f19 f44))) (define-fun f1921 () Arctic (+ (* f18 f43) (* f19 f45))) (define-fun f1922 () Arctic (+ (* f20 f42) (* f21 f44))) (define-fun f1923 () Arctic (+ (* f20 f43) (* f21 f45))) (define-fun f1924 () Arctic (+ (* f18 f46) (* f19 f47))) (define-fun f1925 () Arctic (+ (* f20 f46) (* f21 f47))) (define-fun f1926 () Arctic (+ f22 f1924)) (define-fun f1927 () Arctic (+ f23 f1925)) (define-fun f1928 () Arctic (+ (* f12 f42) (* f13 f44))) (define-fun f1929 () Arctic (+ (* f12 f43) (* f13 f45))) (define-fun f1930 () Arctic (+ (* f14 f42) (* f15 f44))) (define-fun f1931 () Arctic (+ (* f14 f43) (* f15 f45))) (define-fun f1932 () Arctic (+ (* f12 f46) (* f13 f47))) (define-fun f1933 () Arctic (+ (* f14 f46) (* f15 f47))) (define-fun f1934 () Arctic (+ f16 f1932)) (define-fun f1935 () Arctic (+ f17 f1933)) (define-fun f1936 () Arctic (+ (* f18 f1928) (* f19 f1930))) (define-fun f1937 () Arctic (+ (* f18 f1929) (* f19 f1931))) (define-fun f1938 () Arctic (+ (* f20 f1928) (* f21 f1930))) (define-fun f1939 () Arctic (+ (* f20 f1929) (* f21 f1931))) (define-fun f1940 () Arctic (+ (* f18 f1934) (* f19 f1935))) (define-fun f1941 () Arctic (+ (* f20 f1934) (* f21 f1935))) (define-fun f1942 () Arctic (+ f22 f1940)) (define-fun f1943 () Arctic (+ f23 f1941)) (define-fun f1944 () Arctic (+ (* f18 f66) (* f19 f68))) (define-fun f1945 () Arctic (+ (* f18 f67) (* f19 f69))) (define-fun f1946 () Arctic (+ (* f20 f66) (* f21 f68))) (define-fun f1947 () Arctic (+ (* f20 f67) (* f21 f69))) (define-fun f1948 () Arctic (+ (* f18 f70) (* f19 f71))) (define-fun f1949 () Arctic (+ (* f20 f70) (* f21 f71))) (define-fun f1950 () Arctic (+ f22 f1948)) (define-fun f1951 () Arctic (+ f23 f1949)) (define-fun f1952 () Arctic (+ (* f12 f66) (* f13 f68))) (define-fun f1953 () Arctic (+ (* f12 f67) (* f13 f69))) (define-fun f1954 () Arctic (+ (* f14 f66) (* f15 f68))) (define-fun f1955 () Arctic (+ (* f14 f67) (* f15 f69))) (define-fun f1956 () Arctic (+ (* f12 f70) (* f13 f71))) (define-fun f1957 () Arctic (+ (* f14 f70) (* f15 f71))) (define-fun f1958 () Arctic (+ f16 f1956)) (define-fun f1959 () Arctic (+ f17 f1957)) (define-fun f1960 () Arctic (+ (* f18 f1952) (* f19 f1954))) (define-fun f1961 () Arctic (+ (* f18 f1953) (* f19 f1955))) (define-fun f1962 () Arctic (+ (* f20 f1952) (* f21 f1954))) (define-fun f1963 () Arctic (+ (* f20 f1953) (* f21 f1955))) (define-fun f1964 () Arctic (+ (* f18 f1958) (* f19 f1959))) (define-fun f1965 () Arctic (+ (* f20 f1958) (* f21 f1959))) (define-fun f1966 () Arctic (+ f22 f1964)) (define-fun f1967 () Arctic (+ f23 f1965)) (define-fun f1968 () Arctic (+ (* f18 f48) (* f19 f50))) (define-fun f1969 () Arctic (+ (* f18 f49) (* f19 f51))) (define-fun f1970 () Arctic (+ (* f20 f48) (* f21 f50))) (define-fun f1971 () Arctic (+ (* f20 f49) (* f21 f51))) (define-fun f1972 () Arctic (+ (* f18 f52) (* f19 f53))) (define-fun f1973 () Arctic (+ (* f20 f52) (* f21 f53))) (define-fun f1974 () Arctic (+ f22 f1972)) (define-fun f1975 () Arctic (+ f23 f1973)) (define-fun f1976 () Arctic (+ (* f12 f48) (* f13 f50))) (define-fun f1977 () Arctic (+ (* f12 f49) (* f13 f51))) (define-fun f1978 () Arctic (+ (* f14 f48) (* f15 f50))) (define-fun f1979 () Arctic (+ (* f14 f49) (* f15 f51))) (define-fun f1980 () Arctic (+ (* f12 f52) (* f13 f53))) (define-fun f1981 () Arctic (+ (* f14 f52) (* f15 f53))) (define-fun f1982 () Arctic (+ f16 f1980)) (define-fun f1983 () Arctic (+ f17 f1981)) (define-fun f1984 () Arctic (+ (* f18 f1976) (* f19 f1978))) (define-fun f1985 () Arctic (+ (* f18 f1977) (* f19 f1979))) (define-fun f1986 () Arctic (+ (* f20 f1976) (* f21 f1978))) (define-fun f1987 () Arctic (+ (* f20 f1977) (* f21 f1979))) (define-fun f1988 () Arctic (+ (* f18 f1982) (* f19 f1983))) (define-fun f1989 () Arctic (+ (* f20 f1982) (* f21 f1983))) (define-fun f1990 () Arctic (+ f22 f1988)) (define-fun f1991 () Arctic (+ f23 f1989)) (define-fun f1992 () Arctic (+ (* f18 f54) (* f19 f56))) (define-fun f1993 () Arctic (+ (* f18 f55) (* f19 f57))) (define-fun f1994 () Arctic (+ (* f20 f54) (* f21 f56))) (define-fun f1995 () Arctic (+ (* f20 f55) (* f21 f57))) (define-fun f1996 () Arctic (+ (* f18 f58) (* f19 f59))) (define-fun f1997 () Arctic (+ (* f20 f58) (* f21 f59))) (define-fun f1998 () Arctic (+ f22 f1996)) (define-fun f1999 () Arctic (+ f23 f1997)) (define-fun f2000 () Arctic (+ (* f12 f54) (* f13 f56))) (define-fun f2001 () Arctic (+ (* f12 f55) (* f13 f57))) (define-fun f2002 () Arctic (+ (* f14 f54) (* f15 f56))) (define-fun f2003 () Arctic (+ (* f14 f55) (* f15 f57))) (define-fun f2004 () Arctic (+ (* f12 f58) (* f13 f59))) (define-fun f2005 () Arctic (+ (* f14 f58) (* f15 f59))) (define-fun f2006 () Arctic (+ f16 f2004)) (define-fun f2007 () Arctic (+ f17 f2005)) (define-fun f2008 () Arctic (+ (* f18 f2000) (* f19 f2002))) (define-fun f2009 () Arctic (+ (* f18 f2001) (* f19 f2003))) (define-fun f2010 () Arctic (+ (* f20 f2000) (* f21 f2002))) (define-fun f2011 () Arctic (+ (* f20 f2001) (* f21 f2003))) (define-fun f2012 () Arctic (+ (* f18 f2006) (* f19 f2007))) (define-fun f2013 () Arctic (+ (* f20 f2006) (* f21 f2007))) (define-fun f2014 () Arctic (+ f22 f2012)) (define-fun f2015 () Arctic (+ f23 f2013)) (assert (and (and (and (and (>= f80 f96) (>= f81 f97)) (and (>= f82 f98) (>= f83 f99))) (and (and (>= f86 f102)) (and (>= f87 f103)))) (and (and (and (>= f112 f120) (>= f113 f121)) (and (>= f114 f122) (>= f115 f123))) (and (and (>= f118 f126)) (and (>= f119 f127)))) (and (and (and (>= f136 f160) (>= f137 f161)) (and (>= f138 f162) (>= f139 f163))) (and (and (>= f142 f166)) (and (>= f143 f167)))) (and (and (and (>= f176 f192) (>= f177 f193)) (and (>= f178 f194) (>= f179 f195))) (and (and (>= f182 f198)) (and (>= f183 f199)))) (and (and (and (>= f208 f224) (>= f209 f225)) (and (>= f210 f226) (>= f211 f227))) (and (and (>= f214 f230)) (and (>= f215 f231)))) (and (and (and (>= f240 f248) (>= f241 f249)) (and (>= f242 f250) (>= f243 f251))) (and (and (>= f246 f254)) (and (>= f247 f255)))) (and (and (and (>= f264 f280) (>= f265 f281)) (and (>= f266 f282) (>= f267 f283))) (and (and (>= f270 f286)) (and (>= f271 f287)))) (and (and (and (>= f296 f304) (>= f297 f305)) (and (>= f298 f306) (>= f299 f307))) (and (and (>= f302 f310)) (and (>= f303 f311)))) (and (and (and (>= f320 f344) (>= f321 f345)) (and (>= f322 f346) (>= f323 f347))) (and (and (>= f326 f350)) (and (>= f327 f351)))) (and (and (and (>= f360 f376) (>= f361 f377)) (and (>= f362 f378) (>= f363 f379))) (and (and (>= f366 f382)) (and (>= f367 f383)))) (and (and (and (>= f392 f408) (>= f393 f409)) (and (>= f394 f410) (>= f395 f411))) (and (and (>= f398 f414)) (and (>= f399 f415)))) (and (and (and (>= f424 f432) (>= f425 f433)) (and (>= f426 f434) (>= f427 f435))) (and (and (>= f430 f438)) (and (>= f431 f439)))) (and (and (and (>= f448 f464) (>= f449 f465)) (and (>= f450 f466) (>= f451 f467))) (and (and (>= f454 f470)) (and (>= f455 f471)))) (and (and (and (>= f480 f488) (>= f481 f489)) (and (>= f482 f490) (>= f483 f491))) (and (and (>= f486 f494)) (and (>= f487 f495)))) (and (and (and (>= f504 f528) (>= f505 f529)) (and (>= f506 f530) (>= f507 f531))) (and (and (>= f510 f534)) (and (>= f511 f535)))) (and (and (and (>= f544 f560) (>= f545 f561)) (and (>= f546 f562) (>= f547 f563))) (and (and (>= f550 f566)) (and (>= f551 f567)))) (and (and (and (>= f576 f592) (>= f577 f593)) (and (>= f578 f594) (>= f579 f595))) (and (and (>= f582 f598)) (and (>= f583 f599)))) (and (and (and (>= f608 f616) (>= f609 f617)) (and (>= f610 f618) (>= f611 f619))) (and (and (>= f614 f622)) (and (>= f615 f623)))) (and (and (and (>= f632 f648) (>= f633 f649)) (and (>= f634 f650) (>= f635 f651))) (and (and (>= f638 f654)) (and (>= f639 f655)))) (and (and (and (>= f664 f672) (>= f665 f673)) (and (>= f666 f674) (>= f667 f675))) (and (and (>= f670 f678)) (and (>= f671 f679)))) (and (and (and (>= f688 f712) (>= f689 f713)) (and (>= f690 f714) (>= f691 f715))) (and (and (>= f694 f718)) (and (>= f695 f719)))) (and (and (and (>= f728 f744) (>= f729 f745)) (and (>= f730 f746) (>= f731 f747))) (and (and (>= f734 f750)) (and (>= f735 f751)))) (and (and (and (>= f760 f776) (>= f761 f777)) (and (>= f762 f778) (>= f763 f779))) (and (and (>= f766 f782)) (and (>= f767 f783)))) (and (and (and (>= f792 f800) (>= f793 f801)) (and (>= f794 f802) (>= f795 f803))) (and (and (>= f798 f806)) (and (>= f799 f807)))) (and (and (and (>= f816 f832) (>= f817 f833)) (and (>= f818 f834) (>= f819 f835))) (and (and (>= f822 f838)) (and (>= f823 f839)))) (and (and (and (>= f848 f856) (>= f849 f857)) (and (>= f850 f858) (>= f851 f859))) (and (and (>= f854 f862)) (and (>= f855 f863)))) (and (and (and (>= f872 f888) (>= f873 f889)) (and (>= f874 f890) (>= f875 f891))) (and (and (>= f878 f894)) (and (>= f879 f895)))) (and (and (and (>= f904 f920) (>= f905 f921)) (and (>= f906 f922) (>= f907 f923))) (and (and (>= f910 f926)) (and (>= f911 f927)))) (and (and (and (>= f936 f944) (>= f937 f945)) (and (>= f938 f946) (>= f939 f947))) (and (and (>= f942 f950)) (and (>= f943 f951)))) (and (and (and (>= f960 f976) (>= f961 f977)) (and (>= f962 f978) (>= f963 f979))) (and (and (>= f966 f982)) (and (>= f967 f983)))) (and (and (and (>= f992 f1000) (>= f993 f1001)) (and (>= f994 f1002) (>= f995 f1003))) (and (and (>= f998 f1006)) (and (>= f999 f1007)))) (and (and (and (>= f1016 f1040) (>= f1017 f1041)) (and (>= f1018 f1042) (>= f1019 f1043))) (and (and (>= f1022 f1046)) (and (>= f1023 f1047)))) (and (and (and (>= f1056 f1072) (>= f1057 f1073)) (and (>= f1058 f1074) (>= f1059 f1075))) (and (and (>= f1062 f1078)) (and (>= f1063 f1079)))) (and (and (and (>= f1088 f1104) (>= f1089 f1105)) (and (>= f1090 f1106) (>= f1091 f1107))) (and (and (>= f1094 f1110)) (and (>= f1095 f1111)))) (and (and (and (>= f1120 f1128) (>= f1121 f1129)) (and (>= f1122 f1130) (>= f1123 f1131))) (and (and (>= f1126 f1134)) (and (>= f1127 f1135)))) (and (and (and (>= f1136 f1152) (>= f1137 f1153)) (and (>= f1138 f1154) (>= f1139 f1155))) (and (and (>= f1142 f1158)) (and (>= f1143 f1159)))) (and (and (and (>= f1160 f1176) (>= f1161 f1177)) (and (>= f1162 f1178) (>= f1163 f1179))) (and (and (>= f1166 f1182)) (and (>= f1167 f1183)))) (and (and (and (>= f1192 f1208) (>= f1193 f1209)) (and (>= f1194 f1210) (>= f1195 f1211))) (and (and (>= f1198 f1214)) (and (>= f1199 f1215)))) (and (and (and (>= f1224 f1248) (>= f1225 f1249)) (and (>= f1226 f1250) (>= f1227 f1251))) (and (and (>= f1230 f1254)) (and (>= f1231 f1255)))) (and (and (and (>= f1264 f1280) (>= f1265 f1281)) (and (>= f1266 f1282) (>= f1267 f1283))) (and (and (>= f1270 f1286)) (and (>= f1271 f1287)))) (and (and (and (>= f1296 f1312) (>= f1297 f1313)) (and (>= f1298 f1314) (>= f1299 f1315))) (and (and (>= f1302 f1318)) (and (>= f1303 f1319)))) (and (and (and (>= f1328 f1352) (>= f1329 f1353)) (and (>= f1330 f1354) (>= f1331 f1355))) (and (and (>= f1334 f1358)) (and (>= f1335 f1359)))) (and (and (and (>= f1368 f1384) (>= f1369 f1385)) (and (>= f1370 f1386) (>= f1371 f1387))) (and (and (>= f1374 f1390)) (and (>= f1375 f1391)))) (and (and (and (>= f1400 f1416) (>= f1401 f1417)) (and (>= f1402 f1418) (>= f1403 f1419))) (and (and (>= f1406 f1422)) (and (>= f1407 f1423)))) (and (and (and (>= f1432 f1456) (>= f1433 f1457)) (and (>= f1434 f1458) (>= f1435 f1459))) (and (and (>= f1438 f1462)) (and (>= f1439 f1463)))) (and (and (and (>= f1472 f1488) (>= f1473 f1489)) (and (>= f1474 f1490) (>= f1475 f1491))) (and (and (>= f1478 f1494)) (and (>= f1479 f1495)))) (and (and (and (>= f1504 f1520) (>= f1505 f1521)) (and (>= f1506 f1522) (>= f1507 f1523))) (and (and (>= f1510 f1526)) (and (>= f1511 f1527)))) (and (and (and (>= f1536 f1560) (>= f1537 f1561)) (and (>= f1538 f1562) (>= f1539 f1563))) (and (and (>= f1542 f1566)) (and (>= f1543 f1567)))) (and (and (and (>= f1576 f1592) (>= f1577 f1593)) (and (>= f1578 f1594) (>= f1579 f1595))) (and (and (>= f1582 f1598)) (and (>= f1583 f1599)))) (and (and (and (>= f1600 f1608) (>= f1601 f1609)) (and (>= f1602 f1610) (>= f1603 f1611))) (and (and (>= f1606 f1614)) (and (>= f1607 f1615)))) (and (and (and (>= f1616 f1624) (>= f1617 f1625)) (and (>= f1618 f1626) (>= f1619 f1627))) (and (and (>= f1622 f1630)) (and (>= f1623 f1631)))) (and (and (and (>= f1632 f1640) (>= f1633 f1641)) (and (>= f1634 f1642) (>= f1635 f1643))) (and (and (>= f1638 f1646)) (and (>= f1639 f1647)))) (and (and (and (>= f1648 f1656) (>= f1649 f1657)) (and (>= f1650 f1658) (>= f1651 f1659))) (and (and (>= f1654 f1662)) (and (>= f1655 f1663)))) (and (and (and (>= f1672 f1688) (>= f1673 f1689)) (and (>= f1674 f1690) (>= f1675 f1691))) (and (and (>= f1678 f1694)) (and (>= f1679 f1695)))) (and (and (and (>= f1704 f1728) (>= f1705 f1729)) (and (>= f1706 f1730) (>= f1707 f1731))) (and (and (>= f1710 f1734)) (and (>= f1711 f1735)))) (and (and (and (>= f1744 f1760) (>= f1745 f1761)) (and (>= f1746 f1762) (>= f1747 f1763))) (and (and (>= f1750 f1766)) (and (>= f1751 f1767)))) (and (and (and (>= f1776 f1792) (>= f1777 f1793)) (and (>= f1778 f1794) (>= f1779 f1795))) (and (and (>= f1782 f1798)) (and (>= f1783 f1799)))) (and (and (and (>= f1808 f1832) (>= f1809 f1833)) (and (>= f1810 f1834) (>= f1811 f1835))) (and (and (>= f1814 f1838)) (and (>= f1815 f1839)))) (and (and (and (>= f1848 f1864) (>= f1849 f1865)) (and (>= f1850 f1866) (>= f1851 f1867))) (and (and (>= f1854 f1870)) (and (>= f1855 f1871)))) (and (and (and (>= f1872 f1888) (>= f1873 f1889)) (and (>= f1874 f1890) (>= f1875 f1891))) (and (and (>= f1878 f1894)) (and (>= f1879 f1895)))) (and (and (and (>= f1896 f1912) (>= f1897 f1913)) (and (>= f1898 f1914) (>= f1899 f1915))) (and (and (>= f1902 f1918)) (and (>= f1903 f1919)))) (and (and (and (>= f1920 f1936) (>= f1921 f1937)) (and (>= f1922 f1938) (>= f1923 f1939))) (and (and (>= f1926 f1942)) (and (>= f1927 f1943)))) (and (and (and (>= f1944 f1960) (>= f1945 f1961)) (and (>= f1946 f1962) (>= f1947 f1963))) (and (and (>= f1950 f1966)) (and (>= f1951 f1967)))) (and (and (and (>= f1968 f1984) (>= f1969 f1985)) (and (>= f1970 f1986) (>= f1971 f1987))) (and (and (>= f1974 f1990)) (and (>= f1975 f1991)))) (and (and (and (>= f1992 f2008) (>= f1993 f2009)) (and (>= f1994 f2010) (>= f1995 f2011))) (and (and (>= f1998 f2014)) (and (>= f1999 f2015)))))) (assert (or (and (and (and (>> f80 f96) (>> f81 f97)) (and (>> f82 f98) (>> f83 f99))) (and (and (>> f86 f102)) (and (>> f87 f103)))) (and (and (and (>> f112 f120) (>> f113 f121)) (and (>> f114 f122) (>> f115 f123))) (and (and (>> f118 f126)) (and (>> f119 f127)))) (and (and (and (>> f136 f160) (>> f137 f161)) (and (>> f138 f162) (>> f139 f163))) (and (and (>> f142 f166)) (and (>> f143 f167)))) (and (and (and (>> f176 f192) (>> f177 f193)) (and (>> f178 f194) (>> f179 f195))) (and (and (>> f182 f198)) (and (>> f183 f199)))) (and (and (and (>> f208 f224) (>> f209 f225)) (and (>> f210 f226) (>> f211 f227))) (and (and (>> f214 f230)) (and (>> f215 f231)))) (and (and (and (>> f240 f248) (>> f241 f249)) (and (>> f242 f250) (>> f243 f251))) (and (and (>> f246 f254)) (and (>> f247 f255)))) (and (and (and (>> f264 f280) (>> f265 f281)) (and (>> f266 f282) (>> f267 f283))) (and (and (>> f270 f286)) (and (>> f271 f287)))) (and (and (and (>> f296 f304) (>> f297 f305)) (and (>> f298 f306) (>> f299 f307))) (and (and (>> f302 f310)) (and (>> f303 f311)))) (and (and (and (>> f320 f344) (>> f321 f345)) (and (>> f322 f346) (>> f323 f347))) (and (and (>> f326 f350)) (and (>> f327 f351)))) (and (and (and (>> f360 f376) (>> f361 f377)) (and (>> f362 f378) (>> f363 f379))) (and (and (>> f366 f382)) (and (>> f367 f383)))) (and (and (and (>> f392 f408) (>> f393 f409)) (and (>> f394 f410) (>> f395 f411))) (and (and (>> f398 f414)) (and (>> f399 f415)))) (and (and (and (>> f424 f432) (>> f425 f433)) (and (>> f426 f434) (>> f427 f435))) (and (and (>> f430 f438)) (and (>> f431 f439)))) (and (and (and (>> f448 f464) (>> f449 f465)) (and (>> f450 f466) (>> f451 f467))) (and (and (>> f454 f470)) (and (>> f455 f471)))) (and (and (and (>> f480 f488) (>> f481 f489)) (and (>> f482 f490) (>> f483 f491))) (and (and (>> f486 f494)) (and (>> f487 f495)))) (and (and (and (>> f504 f528) (>> f505 f529)) (and (>> f506 f530) (>> f507 f531))) (and (and (>> f510 f534)) (and (>> f511 f535)))) (and (and (and (>> f544 f560) (>> f545 f561)) (and (>> f546 f562) (>> f547 f563))) (and (and (>> f550 f566)) (and (>> f551 f567)))) (and (and (and (>> f576 f592) (>> f577 f593)) (and (>> f578 f594) (>> f579 f595))) (and (and (>> f582 f598)) (and (>> f583 f599)))) (and (and (and (>> f608 f616) (>> f609 f617)) (and (>> f610 f618) (>> f611 f619))) (and (and (>> f614 f622)) (and (>> f615 f623)))) (and (and (and (>> f632 f648) (>> f633 f649)) (and (>> f634 f650) (>> f635 f651))) (and (and (>> f638 f654)) (and (>> f639 f655)))) (and (and (and (>> f664 f672) (>> f665 f673)) (and (>> f666 f674) (>> f667 f675))) (and (and (>> f670 f678)) (and (>> f671 f679)))) (and (and (and (>> f688 f712) (>> f689 f713)) (and (>> f690 f714) (>> f691 f715))) (and (and (>> f694 f718)) (and (>> f695 f719)))) (and (and (and (>> f728 f744) (>> f729 f745)) (and (>> f730 f746) (>> f731 f747))) (and (and (>> f734 f750)) (and (>> f735 f751)))) (and (and (and (>> f760 f776) (>> f761 f777)) (and (>> f762 f778) (>> f763 f779))) (and (and (>> f766 f782)) (and (>> f767 f783)))) (and (and (and (>> f792 f800) (>> f793 f801)) (and (>> f794 f802) (>> f795 f803))) (and (and (>> f798 f806)) (and (>> f799 f807)))) (and (and (and (>> f816 f832) (>> f817 f833)) (and (>> f818 f834) (>> f819 f835))) (and (and (>> f822 f838)) (and (>> f823 f839)))) (and (and (and (>> f848 f856) (>> f849 f857)) (and (>> f850 f858) (>> f851 f859))) (and (and (>> f854 f862)) (and (>> f855 f863)))) (and (and (and (>> f872 f888) (>> f873 f889)) (and (>> f874 f890) (>> f875 f891))) (and (and (>> f878 f894)) (and (>> f879 f895)))) (and (and (and (>> f904 f920) (>> f905 f921)) (and (>> f906 f922) (>> f907 f923))) (and (and (>> f910 f926)) (and (>> f911 f927)))) (and (and (and (>> f936 f944) (>> f937 f945)) (and (>> f938 f946) (>> f939 f947))) (and (and (>> f942 f950)) (and (>> f943 f951)))) (and (and (and (>> f960 f976) (>> f961 f977)) (and (>> f962 f978) (>> f963 f979))) (and (and (>> f966 f982)) (and (>> f967 f983)))) (and (and (and (>> f992 f1000) (>> f993 f1001)) (and (>> f994 f1002) (>> f995 f1003))) (and (and (>> f998 f1006)) (and (>> f999 f1007)))) (and (and (and (>> f1016 f1040) (>> f1017 f1041)) (and (>> f1018 f1042) (>> f1019 f1043))) (and (and (>> f1022 f1046)) (and (>> f1023 f1047)))) (and (and (and (>> f1056 f1072) (>> f1057 f1073)) (and (>> f1058 f1074) (>> f1059 f1075))) (and (and (>> f1062 f1078)) (and (>> f1063 f1079)))) (and (and (and (>> f1088 f1104) (>> f1089 f1105)) (and (>> f1090 f1106) (>> f1091 f1107))) (and (and (>> f1094 f1110)) (and (>> f1095 f1111)))) (and (and (and (>> f1120 f1128) (>> f1121 f1129)) (and (>> f1122 f1130) (>> f1123 f1131))) (and (and (>> f1126 f1134)) (and (>> f1127 f1135)))) (and (and (and (>> f1136 f1152) (>> f1137 f1153)) (and (>> f1138 f1154) (>> f1139 f1155))) (and (and (>> f1142 f1158)) (and (>> f1143 f1159)))) (and (and (and (>> f1160 f1176) (>> f1161 f1177)) (and (>> f1162 f1178) (>> f1163 f1179))) (and (and (>> f1166 f1182)) (and (>> f1167 f1183)))))) (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))