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