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