(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES a# d b d b a a -> a# a c a a, a# d b d b a a -> a# c a a, a# d b d b a a -> c# a a, a# d b d b a a -> a# a, a# d b d b a a -> a#, c# a a -> a# a c c, c# a a -> a# c c, c# a a -> c# c, c# a a -> c#, c# c c -> c# d b, a d b d b a a ->= d b a a c a a, c a a ->= a a c c, c c c ->= d b c d b) 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) (assert (and (or (finite f18) (finite f22)) (or (finite f12) (finite f16)) (or (finite f24) (finite f28)) (or (finite f6) (finite f10)) (or (finite f0) (finite f4)) (or (finite f30) (finite f34)))) (define-fun f36 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f37 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f38 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f39 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f40 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f41 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f42 () Arctic (+ f22 f40)) (define-fun f43 () Arctic (+ f23 f41)) (define-fun f44 () Arctic (+ (* f12 f36) (* f13 f38))) (define-fun f45 () Arctic (+ (* f12 f37) (* f13 f39))) (define-fun f46 () Arctic (+ (* f14 f36) (* f15 f38))) (define-fun f47 () Arctic (+ (* f14 f37) (* f15 f39))) (define-fun f48 () Arctic (+ (* f12 f42) (* f13 f43))) (define-fun f49 () Arctic (+ (* f14 f42) (* f15 f43))) (define-fun f50 () Arctic (+ f16 f48)) (define-fun f51 () Arctic (+ f17 f49)) (define-fun f52 () Arctic (+ (* f6 f44) (* f7 f46))) (define-fun f53 () Arctic (+ (* f6 f45) (* f7 f47))) (define-fun f54 () Arctic (+ (* f8 f44) (* f9 f46))) (define-fun f55 () Arctic (+ (* f8 f45) (* f9 f47))) (define-fun f56 () Arctic (+ (* f6 f50) (* f7 f51))) (define-fun f57 () Arctic (+ (* f8 f50) (* f9 f51))) (define-fun f58 () Arctic (+ f10 f56)) (define-fun f59 () Arctic (+ f11 f57)) (define-fun f60 () Arctic (+ (* f12 f52) (* f13 f54))) (define-fun f61 () Arctic (+ (* f12 f53) (* f13 f55))) (define-fun f62 () Arctic (+ (* f14 f52) (* f15 f54))) (define-fun f63 () Arctic (+ (* f14 f53) (* f15 f55))) (define-fun f64 () Arctic (+ (* f12 f58) (* f13 f59))) (define-fun f65 () Arctic (+ (* f14 f58) (* f15 f59))) (define-fun f66 () Arctic (+ f16 f64)) (define-fun f67 () Arctic (+ f17 f65)) (define-fun f68 () Arctic (+ (* f6 f60) (* f7 f62))) (define-fun f69 () Arctic (+ (* f6 f61) (* f7 f63))) (define-fun f70 () Arctic (+ (* f8 f60) (* f9 f62))) (define-fun f71 () Arctic (+ (* f8 f61) (* f9 f63))) (define-fun f72 () Arctic (+ (* f6 f66) (* f7 f67))) (define-fun f73 () Arctic (+ (* f8 f66) (* f9 f67))) (define-fun f74 () Arctic (+ f10 f72)) (define-fun f75 () Arctic (+ f11 f73)) (define-fun f76 () Arctic (+ (* f0 f68) (* f1 f70))) (define-fun f77 () Arctic (+ (* f0 f69) (* f1 f71))) (define-fun f78 () Arctic (+ (* f2 f68) (* f3 f70))) (define-fun f79 () Arctic (+ (* f2 f69) (* f3 f71))) (define-fun f80 () Arctic (+ (* f0 f74) (* f1 f75))) (define-fun f81 () Arctic (+ (* f2 f74) (* f3 f75))) (define-fun f82 () Arctic (+ f4 f80)) (define-fun f83 () Arctic (+ f5 f81)) (define-fun f84 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f85 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f86 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f87 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f88 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f89 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f90 () Arctic (+ f22 f88)) (define-fun f91 () Arctic (+ f23 f89)) (define-fun f92 () Arctic (+ (* f24 f84) (* f25 f86))) (define-fun f93 () Arctic (+ (* f24 f85) (* f25 f87))) (define-fun f94 () Arctic (+ (* f26 f84) (* f27 f86))) (define-fun f95 () Arctic (+ (* f26 f85) (* f27 f87))) (define-fun f96 () Arctic (+ (* f24 f90) (* f25 f91))) (define-fun f97 () Arctic (+ (* f26 f90) (* f27 f91))) (define-fun f98 () Arctic (+ f28 f96)) (define-fun f99 () Arctic (+ f29 f97)) (define-fun f100 () Arctic (+ (* f18 f92) (* f19 f94))) (define-fun f101 () Arctic (+ (* f18 f93) (* f19 f95))) (define-fun f102 () Arctic (+ (* f20 f92) (* f21 f94))) (define-fun f103 () Arctic (+ (* f20 f93) (* f21 f95))) (define-fun f104 () Arctic (+ (* f18 f98) (* f19 f99))) (define-fun f105 () Arctic (+ (* f20 f98) (* f21 f99))) (define-fun f106 () Arctic (+ f22 f104)) (define-fun f107 () Arctic (+ f23 f105)) (define-fun f108 () Arctic (+ (* f0 f100) (* f1 f102))) (define-fun f109 () Arctic (+ (* f0 f101) (* f1 f103))) (define-fun f110 () Arctic (+ (* f2 f100) (* f3 f102))) (define-fun f111 () Arctic (+ (* f2 f101) (* f3 f103))) (define-fun f112 () Arctic (+ (* f0 f106) (* f1 f107))) (define-fun f113 () Arctic (+ (* f2 f106) (* f3 f107))) (define-fun f114 () Arctic (+ f4 f112)) (define-fun f115 () Arctic (+ f5 f113)) (define-fun f116 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f117 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f118 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f119 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f120 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f121 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f122 () Arctic (+ f22 f120)) (define-fun f123 () Arctic (+ f23 f121)) (define-fun f124 () Arctic (+ (* f12 f116) (* f13 f118))) (define-fun f125 () Arctic (+ (* f12 f117) (* f13 f119))) (define-fun f126 () Arctic (+ (* f14 f116) (* f15 f118))) (define-fun f127 () Arctic (+ (* f14 f117) (* f15 f119))) (define-fun f128 () Arctic (+ (* f12 f122) (* f13 f123))) (define-fun f129 () Arctic (+ (* f14 f122) (* f15 f123))) (define-fun f130 () Arctic (+ f16 f128)) (define-fun f131 () Arctic (+ f17 f129)) (define-fun f132 () Arctic (+ (* f6 f124) (* f7 f126))) (define-fun f133 () Arctic (+ (* f6 f125) (* f7 f127))) (define-fun f134 () Arctic (+ (* f8 f124) (* f9 f126))) (define-fun f135 () Arctic (+ (* f8 f125) (* f9 f127))) (define-fun f136 () Arctic (+ (* f6 f130) (* f7 f131))) (define-fun f137 () Arctic (+ (* f8 f130) (* f9 f131))) (define-fun f138 () Arctic (+ f10 f136)) (define-fun f139 () Arctic (+ f11 f137)) (define-fun f140 () Arctic (+ (* f12 f132) (* f13 f134))) (define-fun f141 () Arctic (+ (* f12 f133) (* f13 f135))) (define-fun f142 () Arctic (+ (* f14 f132) (* f15 f134))) (define-fun f143 () Arctic (+ (* f14 f133) (* f15 f135))) (define-fun f144 () Arctic (+ (* f12 f138) (* f13 f139))) (define-fun f145 () Arctic (+ (* f14 f138) (* f15 f139))) (define-fun f146 () Arctic (+ f16 f144)) (define-fun f147 () Arctic (+ f17 f145)) (define-fun f148 () Arctic (+ (* f6 f140) (* f7 f142))) (define-fun f149 () Arctic (+ (* f6 f141) (* f7 f143))) (define-fun f150 () Arctic (+ (* f8 f140) (* f9 f142))) (define-fun f151 () Arctic (+ (* f8 f141) (* f9 f143))) (define-fun f152 () Arctic (+ (* f6 f146) (* f7 f147))) (define-fun f153 () Arctic (+ (* f8 f146) (* f9 f147))) (define-fun f154 () Arctic (+ f10 f152)) (define-fun f155 () Arctic (+ f11 f153)) (define-fun f156 () Arctic (+ (* f0 f148) (* f1 f150))) (define-fun f157 () Arctic (+ (* f0 f149) (* f1 f151))) (define-fun f158 () Arctic (+ (* f2 f148) (* f3 f150))) (define-fun f159 () Arctic (+ (* f2 f149) (* f3 f151))) (define-fun f160 () Arctic (+ (* f0 f154) (* f1 f155))) (define-fun f161 () Arctic (+ (* f2 f154) (* f3 f155))) (define-fun f162 () Arctic (+ f4 f160)) (define-fun f163 () Arctic (+ f5 f161)) (define-fun f164 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f165 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f166 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f167 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f168 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f169 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f170 () Arctic (+ f22 f168)) (define-fun f171 () Arctic (+ f23 f169)) (define-fun f172 () Arctic (+ (* f24 f164) (* f25 f166))) (define-fun f173 () Arctic (+ (* f24 f165) (* f25 f167))) (define-fun f174 () Arctic (+ (* f26 f164) (* f27 f166))) (define-fun f175 () Arctic (+ (* f26 f165) (* f27 f167))) (define-fun f176 () Arctic (+ (* f24 f170) (* f25 f171))) (define-fun f177 () Arctic (+ (* f26 f170) (* f27 f171))) (define-fun f178 () Arctic (+ f28 f176)) (define-fun f179 () Arctic (+ f29 f177)) (define-fun f180 () Arctic (+ (* f0 f172) (* f1 f174))) (define-fun f181 () Arctic (+ (* f0 f173) (* f1 f175))) (define-fun f182 () Arctic (+ (* f2 f172) (* f3 f174))) (define-fun f183 () Arctic (+ (* f2 f173) (* f3 f175))) (define-fun f184 () Arctic (+ (* f0 f178) (* f1 f179))) (define-fun f185 () Arctic (+ (* f2 f178) (* f3 f179))) (define-fun f186 () Arctic (+ f4 f184)) (define-fun f187 () Arctic (+ f5 f185)) (define-fun f188 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f189 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f190 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f191 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f192 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f193 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f194 () Arctic (+ f22 f192)) (define-fun f195 () Arctic (+ f23 f193)) (define-fun f196 () Arctic (+ (* f12 f188) (* f13 f190))) (define-fun f197 () Arctic (+ (* f12 f189) (* f13 f191))) (define-fun f198 () Arctic (+ (* f14 f188) (* f15 f190))) (define-fun f199 () Arctic (+ (* f14 f189) (* f15 f191))) (define-fun f200 () Arctic (+ (* f12 f194) (* f13 f195))) (define-fun f201 () Arctic (+ (* f14 f194) (* f15 f195))) (define-fun f202 () Arctic (+ f16 f200)) (define-fun f203 () Arctic (+ f17 f201)) (define-fun f204 () Arctic (+ (* f6 f196) (* f7 f198))) (define-fun f205 () Arctic (+ (* f6 f197) (* f7 f199))) (define-fun f206 () Arctic (+ (* f8 f196) (* f9 f198))) (define-fun f207 () Arctic (+ (* f8 f197) (* f9 f199))) (define-fun f208 () Arctic (+ (* f6 f202) (* f7 f203))) (define-fun f209 () Arctic (+ (* f8 f202) (* f9 f203))) (define-fun f210 () Arctic (+ f10 f208)) (define-fun f211 () Arctic (+ f11 f209)) (define-fun f212 () Arctic (+ (* f12 f204) (* f13 f206))) (define-fun f213 () Arctic (+ (* f12 f205) (* f13 f207))) (define-fun f214 () Arctic (+ (* f14 f204) (* f15 f206))) (define-fun f215 () Arctic (+ (* f14 f205) (* f15 f207))) (define-fun f216 () Arctic (+ (* f12 f210) (* f13 f211))) (define-fun f217 () Arctic (+ (* f14 f210) (* f15 f211))) (define-fun f218 () Arctic (+ f16 f216)) (define-fun f219 () Arctic (+ f17 f217)) (define-fun f220 () Arctic (+ (* f6 f212) (* f7 f214))) (define-fun f221 () Arctic (+ (* f6 f213) (* f7 f215))) (define-fun f222 () Arctic (+ (* f8 f212) (* f9 f214))) (define-fun f223 () Arctic (+ (* f8 f213) (* f9 f215))) (define-fun f224 () Arctic (+ (* f6 f218) (* f7 f219))) (define-fun f225 () Arctic (+ (* f8 f218) (* f9 f219))) (define-fun f226 () Arctic (+ f10 f224)) (define-fun f227 () Arctic (+ f11 f225)) (define-fun f228 () Arctic (+ (* f0 f220) (* f1 f222))) (define-fun f229 () Arctic (+ (* f0 f221) (* f1 f223))) (define-fun f230 () Arctic (+ (* f2 f220) (* f3 f222))) (define-fun f231 () Arctic (+ (* f2 f221) (* f3 f223))) (define-fun f232 () Arctic (+ (* f0 f226) (* f1 f227))) (define-fun f233 () Arctic (+ (* f2 f226) (* f3 f227))) (define-fun f234 () Arctic (+ f4 f232)) (define-fun f235 () Arctic (+ f5 f233)) (define-fun f236 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f237 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f238 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f239 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f240 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f241 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f242 () Arctic (+ f22 f240)) (define-fun f243 () Arctic (+ f23 f241)) (define-fun f244 () Arctic (+ (* f30 f236) (* f31 f238))) (define-fun f245 () Arctic (+ (* f30 f237) (* f31 f239))) (define-fun f246 () Arctic (+ (* f32 f236) (* f33 f238))) (define-fun f247 () Arctic (+ (* f32 f237) (* f33 f239))) (define-fun f248 () Arctic (+ (* f30 f242) (* f31 f243))) (define-fun f249 () Arctic (+ (* f32 f242) (* f33 f243))) (define-fun f250 () Arctic (+ f34 f248)) (define-fun f251 () Arctic (+ f35 f249)) (define-fun f252 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f253 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f254 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f255 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f256 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f257 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f258 () Arctic (+ f22 f256)) (define-fun f259 () Arctic (+ f23 f257)) (define-fun f260 () Arctic (+ (* f12 f252) (* f13 f254))) (define-fun f261 () Arctic (+ (* f12 f253) (* f13 f255))) (define-fun f262 () Arctic (+ (* f14 f252) (* f15 f254))) (define-fun f263 () Arctic (+ (* f14 f253) (* f15 f255))) (define-fun f264 () Arctic (+ (* f12 f258) (* f13 f259))) (define-fun f265 () Arctic (+ (* f14 f258) (* f15 f259))) (define-fun f266 () Arctic (+ f16 f264)) (define-fun f267 () Arctic (+ f17 f265)) (define-fun f268 () Arctic (+ (* f6 f260) (* f7 f262))) (define-fun f269 () Arctic (+ (* f6 f261) (* f7 f263))) (define-fun f270 () Arctic (+ (* f8 f260) (* f9 f262))) (define-fun f271 () Arctic (+ (* f8 f261) (* f9 f263))) (define-fun f272 () Arctic (+ (* f6 f266) (* f7 f267))) (define-fun f273 () Arctic (+ (* f8 f266) (* f9 f267))) (define-fun f274 () Arctic (+ f10 f272)) (define-fun f275 () Arctic (+ f11 f273)) (define-fun f276 () Arctic (+ (* f12 f268) (* f13 f270))) (define-fun f277 () Arctic (+ (* f12 f269) (* f13 f271))) (define-fun f278 () Arctic (+ (* f14 f268) (* f15 f270))) (define-fun f279 () Arctic (+ (* f14 f269) (* f15 f271))) (define-fun f280 () Arctic (+ (* f12 f274) (* f13 f275))) (define-fun f281 () Arctic (+ (* f14 f274) (* f15 f275))) (define-fun f282 () Arctic (+ f16 f280)) (define-fun f283 () Arctic (+ f17 f281)) (define-fun f284 () Arctic (+ (* f6 f276) (* f7 f278))) (define-fun f285 () Arctic (+ (* f6 f277) (* f7 f279))) (define-fun f286 () Arctic (+ (* f8 f276) (* f9 f278))) (define-fun f287 () Arctic (+ (* f8 f277) (* f9 f279))) (define-fun f288 () Arctic (+ (* f6 f282) (* f7 f283))) (define-fun f289 () Arctic (+ (* f8 f282) (* f9 f283))) (define-fun f290 () Arctic (+ f10 f288)) (define-fun f291 () Arctic (+ f11 f289)) (define-fun f292 () Arctic (+ (* f0 f284) (* f1 f286))) (define-fun f293 () Arctic (+ (* f0 f285) (* f1 f287))) (define-fun f294 () Arctic (+ (* f2 f284) (* f3 f286))) (define-fun f295 () Arctic (+ (* f2 f285) (* f3 f287))) (define-fun f296 () Arctic (+ (* f0 f290) (* f1 f291))) (define-fun f297 () Arctic (+ (* f2 f290) (* f3 f291))) (define-fun f298 () Arctic (+ f4 f296)) (define-fun f299 () Arctic (+ f5 f297)) (define-fun f300 () Arctic (+ (* f0 f18) (* f1 f20))) (define-fun f301 () Arctic (+ (* f0 f19) (* f1 f21))) (define-fun f302 () Arctic (+ (* f2 f18) (* f3 f20))) (define-fun f303 () Arctic (+ (* f2 f19) (* f3 f21))) (define-fun f304 () Arctic (+ (* f0 f22) (* f1 f23))) (define-fun f305 () Arctic (+ (* f2 f22) (* f3 f23))) (define-fun f306 () Arctic (+ f4 f304)) (define-fun f307 () Arctic (+ f5 f305)) (define-fun f308 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f309 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f310 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f311 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f312 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f313 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f314 () Arctic (+ f22 f312)) (define-fun f315 () Arctic (+ f23 f313)) (define-fun f316 () Arctic (+ (* f12 f308) (* f13 f310))) (define-fun f317 () Arctic (+ (* f12 f309) (* f13 f311))) (define-fun f318 () Arctic (+ (* f14 f308) (* f15 f310))) (define-fun f319 () Arctic (+ (* f14 f309) (* f15 f311))) (define-fun f320 () Arctic (+ (* f12 f314) (* f13 f315))) (define-fun f321 () Arctic (+ (* f14 f314) (* f15 f315))) (define-fun f322 () Arctic (+ f16 f320)) (define-fun f323 () Arctic (+ f17 f321)) (define-fun f324 () Arctic (+ (* f6 f316) (* f7 f318))) (define-fun f325 () Arctic (+ (* f6 f317) (* f7 f319))) (define-fun f326 () Arctic (+ (* f8 f316) (* f9 f318))) (define-fun f327 () Arctic (+ (* f8 f317) (* f9 f319))) (define-fun f328 () Arctic (+ (* f6 f322) (* f7 f323))) (define-fun f329 () Arctic (+ (* f8 f322) (* f9 f323))) (define-fun f330 () Arctic (+ f10 f328)) (define-fun f331 () Arctic (+ f11 f329)) (define-fun f332 () Arctic (+ (* f12 f324) (* f13 f326))) (define-fun f333 () Arctic (+ (* f12 f325) (* f13 f327))) (define-fun f334 () Arctic (+ (* f14 f324) (* f15 f326))) (define-fun f335 () Arctic (+ (* f14 f325) (* f15 f327))) (define-fun f336 () Arctic (+ (* f12 f330) (* f13 f331))) (define-fun f337 () Arctic (+ (* f14 f330) (* f15 f331))) (define-fun f338 () Arctic (+ f16 f336)) (define-fun f339 () Arctic (+ f17 f337)) (define-fun f340 () Arctic (+ (* f6 f332) (* f7 f334))) (define-fun f341 () Arctic (+ (* f6 f333) (* f7 f335))) (define-fun f342 () Arctic (+ (* f8 f332) (* f9 f334))) (define-fun f343 () Arctic (+ (* f8 f333) (* f9 f335))) (define-fun f344 () Arctic (+ (* f6 f338) (* f7 f339))) (define-fun f345 () Arctic (+ (* f8 f338) (* f9 f339))) (define-fun f346 () Arctic (+ f10 f344)) (define-fun f347 () Arctic (+ f11 f345)) (define-fun f348 () Arctic (+ (* f0 f340) (* f1 f342))) (define-fun f349 () Arctic (+ (* f0 f341) (* f1 f343))) (define-fun f350 () Arctic (+ (* f2 f340) (* f3 f342))) (define-fun f351 () Arctic (+ (* f2 f341) (* f3 f343))) (define-fun f352 () Arctic (+ (* f0 f346) (* f1 f347))) (define-fun f353 () Arctic (+ (* f2 f346) (* f3 f347))) (define-fun f354 () Arctic (+ f4 f352)) (define-fun f355 () Arctic (+ f5 f353)) (define-fun f356 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f357 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f358 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f359 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f360 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f361 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f362 () Arctic (+ f22 f360)) (define-fun f363 () Arctic (+ f23 f361)) (define-fun f364 () Arctic (+ (* f30 f356) (* f31 f358))) (define-fun f365 () Arctic (+ (* f30 f357) (* f31 f359))) (define-fun f366 () Arctic (+ (* f32 f356) (* f33 f358))) (define-fun f367 () Arctic (+ (* f32 f357) (* f33 f359))) (define-fun f368 () Arctic (+ (* f30 f362) (* f31 f363))) (define-fun f369 () Arctic (+ (* f32 f362) (* f33 f363))) (define-fun f370 () Arctic (+ f34 f368)) (define-fun f371 () Arctic (+ f35 f369)) (define-fun f372 () Arctic (+ (* f24 f24) (* f25 f26))) (define-fun f373 () Arctic (+ (* f24 f25) (* f25 f27))) (define-fun f374 () Arctic (+ (* f26 f24) (* f27 f26))) (define-fun f375 () Arctic (+ (* f26 f25) (* f27 f27))) (define-fun f376 () Arctic (+ (* f24 f28) (* f25 f29))) (define-fun f377 () Arctic (+ (* f26 f28) (* f27 f29))) (define-fun f378 () Arctic (+ f28 f376)) (define-fun f379 () Arctic (+ f29 f377)) (define-fun f380 () Arctic (+ (* f18 f372) (* f19 f374))) (define-fun f381 () Arctic (+ (* f18 f373) (* f19 f375))) (define-fun f382 () Arctic (+ (* f20 f372) (* f21 f374))) (define-fun f383 () Arctic (+ (* f20 f373) (* f21 f375))) (define-fun f384 () Arctic (+ (* f18 f378) (* f19 f379))) (define-fun f385 () Arctic (+ (* f20 f378) (* f21 f379))) (define-fun f386 () Arctic (+ f22 f384)) (define-fun f387 () Arctic (+ f23 f385)) (define-fun f388 () Arctic (+ (* f0 f380) (* f1 f382))) (define-fun f389 () Arctic (+ (* f0 f381) (* f1 f383))) (define-fun f390 () Arctic (+ (* f2 f380) (* f3 f382))) (define-fun f391 () Arctic (+ (* f2 f381) (* f3 f383))) (define-fun f392 () Arctic (+ (* f0 f386) (* f1 f387))) (define-fun f393 () Arctic (+ (* f2 f386) (* f3 f387))) (define-fun f394 () Arctic (+ f4 f392)) (define-fun f395 () Arctic (+ f5 f393)) (define-fun f396 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f397 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f398 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f399 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f400 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f401 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f402 () Arctic (+ f22 f400)) (define-fun f403 () Arctic (+ f23 f401)) (define-fun f404 () Arctic (+ (* f30 f396) (* f31 f398))) (define-fun f405 () Arctic (+ (* f30 f397) (* f31 f399))) (define-fun f406 () Arctic (+ (* f32 f396) (* f33 f398))) (define-fun f407 () Arctic (+ (* f32 f397) (* f33 f399))) (define-fun f408 () Arctic (+ (* f30 f402) (* f31 f403))) (define-fun f409 () Arctic (+ (* f32 f402) (* f33 f403))) (define-fun f410 () Arctic (+ f34 f408)) (define-fun f411 () Arctic (+ f35 f409)) (define-fun f412 () Arctic (+ (* f24 f24) (* f25 f26))) (define-fun f413 () Arctic (+ (* f24 f25) (* f25 f27))) (define-fun f414 () Arctic (+ (* f26 f24) (* f27 f26))) (define-fun f415 () Arctic (+ (* f26 f25) (* f27 f27))) (define-fun f416 () Arctic (+ (* f24 f28) (* f25 f29))) (define-fun f417 () Arctic (+ (* f26 f28) (* f27 f29))) (define-fun f418 () Arctic (+ f28 f416)) (define-fun f419 () Arctic (+ f29 f417)) (define-fun f420 () Arctic (+ (* f0 f412) (* f1 f414))) (define-fun f421 () Arctic (+ (* f0 f413) (* f1 f415))) (define-fun f422 () Arctic (+ (* f2 f412) (* f3 f414))) (define-fun f423 () Arctic (+ (* f2 f413) (* f3 f415))) (define-fun f424 () Arctic (+ (* f0 f418) (* f1 f419))) (define-fun f425 () Arctic (+ (* f2 f418) (* f3 f419))) (define-fun f426 () Arctic (+ f4 f424)) (define-fun f427 () Arctic (+ f5 f425)) (define-fun f428 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f429 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f430 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f431 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f432 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f433 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f434 () Arctic (+ f22 f432)) (define-fun f435 () Arctic (+ f23 f433)) (define-fun f436 () Arctic (+ (* f30 f428) (* f31 f430))) (define-fun f437 () Arctic (+ (* f30 f429) (* f31 f431))) (define-fun f438 () Arctic (+ (* f32 f428) (* f33 f430))) (define-fun f439 () Arctic (+ (* f32 f429) (* f33 f431))) (define-fun f440 () Arctic (+ (* f30 f434) (* f31 f435))) (define-fun f441 () Arctic (+ (* f32 f434) (* f33 f435))) (define-fun f442 () Arctic (+ f34 f440)) (define-fun f443 () Arctic (+ f35 f441)) (define-fun f444 () Arctic (+ (* f30 f24) (* f31 f26))) (define-fun f445 () Arctic (+ (* f30 f25) (* f31 f27))) (define-fun f446 () Arctic (+ (* f32 f24) (* f33 f26))) (define-fun f447 () Arctic (+ (* f32 f25) (* f33 f27))) (define-fun f448 () Arctic (+ (* f30 f28) (* f31 f29))) (define-fun f449 () Arctic (+ (* f32 f28) (* f33 f29))) (define-fun f450 () Arctic (+ f34 f448)) (define-fun f451 () Arctic (+ f35 f449)) (define-fun f452 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f453 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f454 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f455 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f456 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f457 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f458 () Arctic (+ f22 f456)) (define-fun f459 () Arctic (+ f23 f457)) (define-fun f460 () Arctic (+ (* f30 f452) (* f31 f454))) (define-fun f461 () Arctic (+ (* f30 f453) (* f31 f455))) (define-fun f462 () Arctic (+ (* f32 f452) (* f33 f454))) (define-fun f463 () Arctic (+ (* f32 f453) (* f33 f455))) (define-fun f464 () Arctic (+ (* f30 f458) (* f31 f459))) (define-fun f465 () Arctic (+ (* f32 f458) (* f33 f459))) (define-fun f466 () Arctic (+ f34 f464)) (define-fun f467 () Arctic (+ f35 f465)) (define-fun f468 () Arctic (+ (* f24 f24) (* f25 f26))) (define-fun f469 () Arctic (+ (* f24 f25) (* f25 f27))) (define-fun f470 () Arctic (+ (* f26 f24) (* f27 f26))) (define-fun f471 () Arctic (+ (* f26 f25) (* f27 f27))) (define-fun f472 () Arctic (+ (* f24 f28) (* f25 f29))) (define-fun f473 () Arctic (+ (* f26 f28) (* f27 f29))) (define-fun f474 () Arctic (+ f28 f472)) (define-fun f475 () Arctic (+ f29 f473)) (define-fun f476 () Arctic (+ (* f30 f468) (* f31 f470))) (define-fun f477 () Arctic (+ (* f30 f469) (* f31 f471))) (define-fun f478 () Arctic (+ (* f32 f468) (* f33 f470))) (define-fun f479 () Arctic (+ (* f32 f469) (* f33 f471))) (define-fun f480 () Arctic (+ (* f30 f474) (* f31 f475))) (define-fun f481 () Arctic (+ (* f32 f474) (* f33 f475))) (define-fun f482 () Arctic (+ f34 f480)) (define-fun f483 () Arctic (+ f35 f481)) (define-fun f484 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f485 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f486 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f487 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f488 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f489 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f490 () Arctic (+ f10 f488)) (define-fun f491 () Arctic (+ f11 f489)) (define-fun f492 () Arctic (+ (* f30 f484) (* f31 f486))) (define-fun f493 () Arctic (+ (* f30 f485) (* f31 f487))) (define-fun f494 () Arctic (+ (* f32 f484) (* f33 f486))) (define-fun f495 () Arctic (+ (* f32 f485) (* f33 f487))) (define-fun f496 () Arctic (+ (* f30 f490) (* f31 f491))) (define-fun f497 () Arctic (+ (* f32 f490) (* f33 f491))) (define-fun f498 () Arctic (+ f34 f496)) (define-fun f499 () Arctic (+ f35 f497)) (define-fun f500 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f501 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f502 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f503 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f504 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f505 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f506 () Arctic (+ f22 f504)) (define-fun f507 () Arctic (+ f23 f505)) (define-fun f508 () Arctic (+ (* f12 f500) (* f13 f502))) (define-fun f509 () Arctic (+ (* f12 f501) (* f13 f503))) (define-fun f510 () Arctic (+ (* f14 f500) (* f15 f502))) (define-fun f511 () Arctic (+ (* f14 f501) (* f15 f503))) (define-fun f512 () Arctic (+ (* f12 f506) (* f13 f507))) (define-fun f513 () Arctic (+ (* f14 f506) (* f15 f507))) (define-fun f514 () Arctic (+ f16 f512)) (define-fun f515 () Arctic (+ f17 f513)) (define-fun f516 () Arctic (+ (* f6 f508) (* f7 f510))) (define-fun f517 () Arctic (+ (* f6 f509) (* f7 f511))) (define-fun f518 () Arctic (+ (* f8 f508) (* f9 f510))) (define-fun f519 () Arctic (+ (* f8 f509) (* f9 f511))) (define-fun f520 () Arctic (+ (* f6 f514) (* f7 f515))) (define-fun f521 () Arctic (+ (* f8 f514) (* f9 f515))) (define-fun f522 () Arctic (+ f10 f520)) (define-fun f523 () Arctic (+ f11 f521)) (define-fun f524 () Arctic (+ (* f12 f516) (* f13 f518))) (define-fun f525 () Arctic (+ (* f12 f517) (* f13 f519))) (define-fun f526 () Arctic (+ (* f14 f516) (* f15 f518))) (define-fun f527 () Arctic (+ (* f14 f517) (* f15 f519))) (define-fun f528 () Arctic (+ (* f12 f522) (* f13 f523))) (define-fun f529 () Arctic (+ (* f14 f522) (* f15 f523))) (define-fun f530 () Arctic (+ f16 f528)) (define-fun f531 () Arctic (+ f17 f529)) (define-fun f532 () Arctic (+ (* f6 f524) (* f7 f526))) (define-fun f533 () Arctic (+ (* f6 f525) (* f7 f527))) (define-fun f534 () Arctic (+ (* f8 f524) (* f9 f526))) (define-fun f535 () Arctic (+ (* f8 f525) (* f9 f527))) (define-fun f536 () Arctic (+ (* f6 f530) (* f7 f531))) (define-fun f537 () Arctic (+ (* f8 f530) (* f9 f531))) (define-fun f538 () Arctic (+ f10 f536)) (define-fun f539 () Arctic (+ f11 f537)) (define-fun f540 () Arctic (+ (* f18 f532) (* f19 f534))) (define-fun f541 () Arctic (+ (* f18 f533) (* f19 f535))) (define-fun f542 () Arctic (+ (* f20 f532) (* f21 f534))) (define-fun f543 () Arctic (+ (* f20 f533) (* f21 f535))) (define-fun f544 () Arctic (+ (* f18 f538) (* f19 f539))) (define-fun f545 () Arctic (+ (* f20 f538) (* f21 f539))) (define-fun f546 () Arctic (+ f22 f544)) (define-fun f547 () Arctic (+ f23 f545)) (define-fun f548 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f549 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f550 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f551 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f552 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f553 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f554 () Arctic (+ f22 f552)) (define-fun f555 () Arctic (+ f23 f553)) (define-fun f556 () Arctic (+ (* f24 f548) (* f25 f550))) (define-fun f557 () Arctic (+ (* f24 f549) (* f25 f551))) (define-fun f558 () Arctic (+ (* f26 f548) (* f27 f550))) (define-fun f559 () Arctic (+ (* f26 f549) (* f27 f551))) (define-fun f560 () Arctic (+ (* f24 f554) (* f25 f555))) (define-fun f561 () Arctic (+ (* f26 f554) (* f27 f555))) (define-fun f562 () Arctic (+ f28 f560)) (define-fun f563 () Arctic (+ f29 f561)) (define-fun f564 () Arctic (+ (* f18 f556) (* f19 f558))) (define-fun f565 () Arctic (+ (* f18 f557) (* f19 f559))) (define-fun f566 () Arctic (+ (* f20 f556) (* f21 f558))) (define-fun f567 () Arctic (+ (* f20 f557) (* f21 f559))) (define-fun f568 () Arctic (+ (* f18 f562) (* f19 f563))) (define-fun f569 () Arctic (+ (* f20 f562) (* f21 f563))) (define-fun f570 () Arctic (+ f22 f568)) (define-fun f571 () Arctic (+ f23 f569)) (define-fun f572 () Arctic (+ (* f18 f564) (* f19 f566))) (define-fun f573 () Arctic (+ (* f18 f565) (* f19 f567))) (define-fun f574 () Arctic (+ (* f20 f564) (* f21 f566))) (define-fun f575 () Arctic (+ (* f20 f565) (* f21 f567))) (define-fun f576 () Arctic (+ (* f18 f570) (* f19 f571))) (define-fun f577 () Arctic (+ (* f20 f570) (* f21 f571))) (define-fun f578 () Arctic (+ f22 f576)) (define-fun f579 () Arctic (+ f23 f577)) (define-fun f580 () Arctic (+ (* f12 f572) (* f13 f574))) (define-fun f581 () Arctic (+ (* f12 f573) (* f13 f575))) (define-fun f582 () Arctic (+ (* f14 f572) (* f15 f574))) (define-fun f583 () Arctic (+ (* f14 f573) (* f15 f575))) (define-fun f584 () Arctic (+ (* f12 f578) (* f13 f579))) (define-fun f585 () Arctic (+ (* f14 f578) (* f15 f579))) (define-fun f586 () Arctic (+ f16 f584)) (define-fun f587 () Arctic (+ f17 f585)) (define-fun f588 () Arctic (+ (* f6 f580) (* f7 f582))) (define-fun f589 () Arctic (+ (* f6 f581) (* f7 f583))) (define-fun f590 () Arctic (+ (* f8 f580) (* f9 f582))) (define-fun f591 () Arctic (+ (* f8 f581) (* f9 f583))) (define-fun f592 () Arctic (+ (* f6 f586) (* f7 f587))) (define-fun f593 () Arctic (+ (* f8 f586) (* f9 f587))) (define-fun f594 () Arctic (+ f10 f592)) (define-fun f595 () Arctic (+ f11 f593)) (define-fun f596 () Arctic (+ (* f18 f18) (* f19 f20))) (define-fun f597 () Arctic (+ (* f18 f19) (* f19 f21))) (define-fun f598 () Arctic (+ (* f20 f18) (* f21 f20))) (define-fun f599 () Arctic (+ (* f20 f19) (* f21 f21))) (define-fun f600 () Arctic (+ (* f18 f22) (* f19 f23))) (define-fun f601 () Arctic (+ (* f20 f22) (* f21 f23))) (define-fun f602 () Arctic (+ f22 f600)) (define-fun f603 () Arctic (+ f23 f601)) (define-fun f604 () Arctic (+ (* f24 f596) (* f25 f598))) (define-fun f605 () Arctic (+ (* f24 f597) (* f25 f599))) (define-fun f606 () Arctic (+ (* f26 f596) (* f27 f598))) (define-fun f607 () Arctic (+ (* f26 f597) (* f27 f599))) (define-fun f608 () Arctic (+ (* f24 f602) (* f25 f603))) (define-fun f609 () Arctic (+ (* f26 f602) (* f27 f603))) (define-fun f610 () Arctic (+ f28 f608)) (define-fun f611 () Arctic (+ f29 f609)) (define-fun f612 () Arctic (+ (* f24 f24) (* f25 f26))) (define-fun f613 () Arctic (+ (* f24 f25) (* f25 f27))) (define-fun f614 () Arctic (+ (* f26 f24) (* f27 f26))) (define-fun f615 () Arctic (+ (* f26 f25) (* f27 f27))) (define-fun f616 () Arctic (+ (* f24 f28) (* f25 f29))) (define-fun f617 () Arctic (+ (* f26 f28) (* f27 f29))) (define-fun f618 () Arctic (+ f28 f616)) (define-fun f619 () Arctic (+ f29 f617)) (define-fun f620 () Arctic (+ (* f18 f612) (* f19 f614))) (define-fun f621 () Arctic (+ (* f18 f613) (* f19 f615))) (define-fun f622 () Arctic (+ (* f20 f612) (* f21 f614))) (define-fun f623 () Arctic (+ (* f20 f613) (* f21 f615))) (define-fun f624 () Arctic (+ (* f18 f618) (* f19 f619))) (define-fun f625 () Arctic (+ (* f20 f618) (* f21 f619))) (define-fun f626 () Arctic (+ f22 f624)) (define-fun f627 () Arctic (+ f23 f625)) (define-fun f628 () Arctic (+ (* f18 f620) (* f19 f622))) (define-fun f629 () Arctic (+ (* f18 f621) (* f19 f623))) (define-fun f630 () Arctic (+ (* f20 f620) (* f21 f622))) (define-fun f631 () Arctic (+ (* f20 f621) (* f21 f623))) (define-fun f632 () Arctic (+ (* f18 f626) (* f19 f627))) (define-fun f633 () Arctic (+ (* f20 f626) (* f21 f627))) (define-fun f634 () Arctic (+ f22 f632)) (define-fun f635 () Arctic (+ f23 f633)) (define-fun f636 () Arctic (+ (* f24 f24) (* f25 f26))) (define-fun f637 () Arctic (+ (* f24 f25) (* f25 f27))) (define-fun f638 () Arctic (+ (* f26 f24) (* f27 f26))) (define-fun f639 () Arctic (+ (* f26 f25) (* f27 f27))) (define-fun f640 () Arctic (+ (* f24 f28) (* f25 f29))) (define-fun f641 () Arctic (+ (* f26 f28) (* f27 f29))) (define-fun f642 () Arctic (+ f28 f640)) (define-fun f643 () Arctic (+ f29 f641)) (define-fun f644 () Arctic (+ (* f24 f636) (* f25 f638))) (define-fun f645 () Arctic (+ (* f24 f637) (* f25 f639))) (define-fun f646 () Arctic (+ (* f26 f636) (* f27 f638))) (define-fun f647 () Arctic (+ (* f26 f637) (* f27 f639))) (define-fun f648 () Arctic (+ (* f24 f642) (* f25 f643))) (define-fun f649 () Arctic (+ (* f26 f642) (* f27 f643))) (define-fun f650 () Arctic (+ f28 f648)) (define-fun f651 () Arctic (+ f29 f649)) (define-fun f652 () Arctic (+ (* f6 f12) (* f7 f14))) (define-fun f653 () Arctic (+ (* f6 f13) (* f7 f15))) (define-fun f654 () Arctic (+ (* f8 f12) (* f9 f14))) (define-fun f655 () Arctic (+ (* f8 f13) (* f9 f15))) (define-fun f656 () Arctic (+ (* f6 f16) (* f7 f17))) (define-fun f657 () Arctic (+ (* f8 f16) (* f9 f17))) (define-fun f658 () Arctic (+ f10 f656)) (define-fun f659 () Arctic (+ f11 f657)) (define-fun f660 () Arctic (+ (* f24 f652) (* f25 f654))) (define-fun f661 () Arctic (+ (* f24 f653) (* f25 f655))) (define-fun f662 () Arctic (+ (* f26 f652) (* f27 f654))) (define-fun f663 () Arctic (+ (* f26 f653) (* f27 f655))) (define-fun f664 () Arctic (+ (* f24 f658) (* f25 f659))) (define-fun f665 () Arctic (+ (* f26 f658) (* f27 f659))) (define-fun f666 () Arctic (+ f28 f664)) (define-fun f667 () Arctic (+ f29 f665)) (define-fun f668 () Arctic (+ (* f12 f660) (* f13 f662))) (define-fun f669 () Arctic (+ (* f12 f661) (* f13 f663))) (define-fun f670 () Arctic (+ (* f14 f660) (* f15 f662))) (define-fun f671 () Arctic (+ (* f14 f661) (* f15 f663))) (define-fun f672 () Arctic (+ (* f12 f666) (* f13 f667))) (define-fun f673 () Arctic (+ (* f14 f666) (* f15 f667))) (define-fun f674 () Arctic (+ f16 f672)) (define-fun f675 () Arctic (+ f17 f673)) (define-fun f676 () Arctic (+ (* f6 f668) (* f7 f670))) (define-fun f677 () Arctic (+ (* f6 f669) (* f7 f671))) (define-fun f678 () Arctic (+ (* f8 f668) (* f9 f670))) (define-fun f679 () Arctic (+ (* f8 f669) (* f9 f671))) (define-fun f680 () Arctic (+ (* f6 f674) (* f7 f675))) (define-fun f681 () Arctic (+ (* f8 f674) (* f9 f675))) (define-fun f682 () Arctic (+ f10 f680)) (define-fun f683 () Arctic (+ f11 f681)) (assert (and (and (and (and (>= f76 f108) (>= f77 f109)) (and (>= f78 f110) (>= f79 f111))) (and (and (>= f82 f114)) (and (>= f83 f115)))) (and (and (and (>= f156 f180) (>= f157 f181)) (and (>= f158 f182) (>= f159 f183))) (and (and (>= f162 f186)) (and (>= f163 f187)))) (and (and (and (>= f228 f244) (>= f229 f245)) (and (>= f230 f246) (>= f231 f247))) (and (and (>= f234 f250)) (and (>= f235 f251)))) (and (and (and (>= f292 f300) (>= f293 f301)) (and (>= f294 f302) (>= f295 f303))) (and (and (>= f298 f306)) (and (>= f299 f307)))) (and (and (and (>= f348 f0) (>= f349 f1)) (and (>= f350 f2) (>= f351 f3))) (and (and (>= f354 f4)) (and (>= f355 f5)))) (and (and (and (>= f364 f388) (>= f365 f389)) (and (>= f366 f390) (>= f367 f391))) (and (and (>= f370 f394)) (and (>= f371 f395)))) (and (and (and (>= f404 f420) (>= f405 f421)) (and (>= f406 f422) (>= f407 f423))) (and (and (>= f410 f426)) (and (>= f411 f427)))) (and (and (and (>= f436 f444) (>= f437 f445)) (and (>= f438 f446) (>= f439 f447))) (and (and (>= f442 f450)) (and (>= f443 f451)))) (and (and (and (>= f460 f30) (>= f461 f31)) (and (>= f462 f32) (>= f463 f33))) (and (and (>= f466 f34)) (and (>= f467 f35)))) (and (and (and (>= f476 f492) (>= f477 f493)) (and (>= f478 f494) (>= f479 f495))) (and (and (>= f482 f498)) (and (>= f483 f499)))) (and (and (and (>= f540 f588) (>= f541 f589)) (and (>= f542 f590) (>= f543 f591))) (and (and (>= f546 f594)) (and (>= f547 f595)))) (and (and (and (>= f604 f628) (>= f605 f629)) (and (>= f606 f630) (>= f607 f631))) (and (and (>= f610 f634)) (and (>= f611 f635)))) (and (and (and (>= f644 f676) (>= f645 f677)) (and (>= f646 f678) (>= f647 f679))) (and (and (>= f650 f682)) (and (>= f651 f683)))))) (assert (or (and (and (and (>> f76 f108) (>> f77 f109)) (and (>> f78 f110) (>> f79 f111))) (and (and (>> f82 f114)) (and (>> f83 f115)))) (and (and (and (>> f156 f180) (>> f157 f181)) (and (>> f158 f182) (>> f159 f183))) (and (and (>> f162 f186)) (and (>> f163 f187)))) (and (and (and (>> f228 f244) (>> f229 f245)) (and (>> f230 f246) (>> f231 f247))) (and (and (>> f234 f250)) (and (>> f235 f251)))) (and (and (and (>> f292 f300) (>> f293 f301)) (and (>> f294 f302) (>> f295 f303))) (and (and (>> f298 f306)) (and (>> f299 f307)))) (and (and (and (>> f348 f0) (>> f349 f1)) (and (>> f350 f2) (>> f351 f3))) (and (and (>> f354 f4)) (and (>> f355 f5)))) (and (and (and (>> f364 f388) (>> f365 f389)) (and (>> f366 f390) (>> f367 f391))) (and (and (>> f370 f394)) (and (>> f371 f395)))) (and (and (and (>> f404 f420) (>> f405 f421)) (and (>> f406 f422) (>> f407 f423))) (and (and (>> f410 f426)) (and (>> f411 f427)))) (and (and (and (>> f436 f444) (>> f437 f445)) (and (>> f438 f446) (>> f439 f447))) (and (and (>> f442 f450)) (and (>> f443 f451)))) (and (and (and (>> f460 f30) (>> f461 f31)) (and (>> f462 f32) (>> f463 f33))) (and (and (>> f466 f34)) (and (>> f467 f35)))) (and (and (and (>> f476 f492) (>> f477 f493)) (and (>> f478 f494) (>> f479 f495))) (and (and (>> f482 f498)) (and (>> f483 f499)))))) (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))