(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES b# b -> b# a b, b# b -> b#, b# a b b -> b# b a a b a b, b# a b b -> b# a a b a b, b# a b b -> b# a b, b# a b b -> b#, b# a b -> b# a a b, b# a b -> b#, b# a b a a b -> b# b, b# a b a a b -> b#, b b ->= b a b, b a b b ->= b b a a b a b, b a b ->= b a a b, b a b a a b ->= b b) 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) (assert (and (or (finite f24) (finite f33)) (or (finite f12) (finite f21)) (or (finite f0) (finite f9)))) (define-fun f36 () Arctic (+ (* f0 f12) (* f1 f15) (* f2 f18))) (define-fun f37 () Arctic (+ (* f0 f13) (* f1 f16) (* f2 f19))) (define-fun f38 () Arctic (+ (* f0 f14) (* f1 f17) (* f2 f20))) (define-fun f39 () Arctic (+ (* f3 f12) (* f4 f15) (* f5 f18))) (define-fun f40 () Arctic (+ (* f3 f13) (* f4 f16) (* f5 f19))) (define-fun f41 () Arctic (+ (* f3 f14) (* f4 f17) (* f5 f20))) (define-fun f42 () Arctic (+ (* f6 f12) (* f7 f15) (* f8 f18))) (define-fun f43 () Arctic (+ (* f6 f13) (* f7 f16) (* f8 f19))) (define-fun f44 () Arctic (+ (* f6 f14) (* f7 f17) (* f8 f20))) (define-fun f45 () Arctic (+ (* f0 f21) (* f1 f22) (* f2 f23))) (define-fun f46 () Arctic (+ (* f3 f21) (* f4 f22) (* f5 f23))) (define-fun f47 () Arctic (+ (* f6 f21) (* f7 f22) (* f8 f23))) (define-fun f48 () Arctic (+ f9 f45)) (define-fun f49 () Arctic (+ f10 f46)) (define-fun f50 () Arctic (+ f11 f47)) (define-fun f51 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f52 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f53 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f54 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f55 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f56 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f57 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f58 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f59 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f60 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f61 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f62 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f63 () Arctic (+ f33 f60)) (define-fun f64 () Arctic (+ f34 f61)) (define-fun f65 () Arctic (+ f35 f62)) (define-fun f66 () Arctic (+ (* f0 f51) (* f1 f54) (* f2 f57))) (define-fun f67 () Arctic (+ (* f0 f52) (* f1 f55) (* f2 f58))) (define-fun f68 () Arctic (+ (* f0 f53) (* f1 f56) (* f2 f59))) (define-fun f69 () Arctic (+ (* f3 f51) (* f4 f54) (* f5 f57))) (define-fun f70 () Arctic (+ (* f3 f52) (* f4 f55) (* f5 f58))) (define-fun f71 () Arctic (+ (* f3 f53) (* f4 f56) (* f5 f59))) (define-fun f72 () Arctic (+ (* f6 f51) (* f7 f54) (* f8 f57))) (define-fun f73 () Arctic (+ (* f6 f52) (* f7 f55) (* f8 f58))) (define-fun f74 () Arctic (+ (* f6 f53) (* f7 f56) (* f8 f59))) (define-fun f75 () Arctic (+ (* f0 f63) (* f1 f64) (* f2 f65))) (define-fun f76 () Arctic (+ (* f3 f63) (* f4 f64) (* f5 f65))) (define-fun f77 () Arctic (+ (* f6 f63) (* f7 f64) (* f8 f65))) (define-fun f78 () Arctic (+ f9 f75)) (define-fun f79 () Arctic (+ f10 f76)) (define-fun f80 () Arctic (+ f11 f77)) (define-fun f81 () Arctic (+ (* f0 f12) (* f1 f15) (* f2 f18))) (define-fun f82 () Arctic (+ (* f0 f13) (* f1 f16) (* f2 f19))) (define-fun f83 () Arctic (+ (* f0 f14) (* f1 f17) (* f2 f20))) (define-fun f84 () Arctic (+ (* f3 f12) (* f4 f15) (* f5 f18))) (define-fun f85 () Arctic (+ (* f3 f13) (* f4 f16) (* f5 f19))) (define-fun f86 () Arctic (+ (* f3 f14) (* f4 f17) (* f5 f20))) (define-fun f87 () Arctic (+ (* f6 f12) (* f7 f15) (* f8 f18))) (define-fun f88 () Arctic (+ (* f6 f13) (* f7 f16) (* f8 f19))) (define-fun f89 () Arctic (+ (* f6 f14) (* f7 f17) (* f8 f20))) (define-fun f90 () Arctic (+ (* f0 f21) (* f1 f22) (* f2 f23))) (define-fun f91 () Arctic (+ (* f3 f21) (* f4 f22) (* f5 f23))) (define-fun f92 () Arctic (+ (* f6 f21) (* f7 f22) (* f8 f23))) (define-fun f93 () Arctic (+ f9 f90)) (define-fun f94 () Arctic (+ f10 f91)) (define-fun f95 () Arctic (+ f11 f92)) (define-fun f96 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f97 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f98 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f99 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f100 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f101 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f102 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f103 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f104 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f105 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f106 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f107 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f108 () Arctic (+ f21 f105)) (define-fun f109 () Arctic (+ f22 f106)) (define-fun f110 () Arctic (+ f23 f107)) (define-fun f111 () Arctic (+ (* f24 f96) (* f25 f99) (* f26 f102))) (define-fun f112 () Arctic (+ (* f24 f97) (* f25 f100) (* f26 f103))) (define-fun f113 () Arctic (+ (* f24 f98) (* f25 f101) (* f26 f104))) (define-fun f114 () Arctic (+ (* f27 f96) (* f28 f99) (* f29 f102))) (define-fun f115 () Arctic (+ (* f27 f97) (* f28 f100) (* f29 f103))) (define-fun f116 () Arctic (+ (* f27 f98) (* f28 f101) (* f29 f104))) (define-fun f117 () Arctic (+ (* f30 f96) (* f31 f99) (* f32 f102))) (define-fun f118 () Arctic (+ (* f30 f97) (* f31 f100) (* f32 f103))) (define-fun f119 () Arctic (+ (* f30 f98) (* f31 f101) (* f32 f104))) (define-fun f120 () Arctic (+ (* f24 f108) (* f25 f109) (* f26 f110))) (define-fun f121 () Arctic (+ (* f27 f108) (* f28 f109) (* f29 f110))) (define-fun f122 () Arctic (+ (* f30 f108) (* f31 f109) (* f32 f110))) (define-fun f123 () Arctic (+ f33 f120)) (define-fun f124 () Arctic (+ f34 f121)) (define-fun f125 () Arctic (+ f35 f122)) (define-fun f126 () Arctic (+ (* f0 f111) (* f1 f114) (* f2 f117))) (define-fun f127 () Arctic (+ (* f0 f112) (* f1 f115) (* f2 f118))) (define-fun f128 () Arctic (+ (* f0 f113) (* f1 f116) (* f2 f119))) (define-fun f129 () Arctic (+ (* f3 f111) (* f4 f114) (* f5 f117))) (define-fun f130 () Arctic (+ (* f3 f112) (* f4 f115) (* f5 f118))) (define-fun f131 () Arctic (+ (* f3 f113) (* f4 f116) (* f5 f119))) (define-fun f132 () Arctic (+ (* f6 f111) (* f7 f114) (* f8 f117))) (define-fun f133 () Arctic (+ (* f6 f112) (* f7 f115) (* f8 f118))) (define-fun f134 () Arctic (+ (* f6 f113) (* f7 f116) (* f8 f119))) (define-fun f135 () Arctic (+ (* f0 f123) (* f1 f124) (* f2 f125))) (define-fun f136 () Arctic (+ (* f3 f123) (* f4 f124) (* f5 f125))) (define-fun f137 () Arctic (+ (* f6 f123) (* f7 f124) (* f8 f125))) (define-fun f138 () Arctic (+ f9 f135)) (define-fun f139 () Arctic (+ f10 f136)) (define-fun f140 () Arctic (+ f11 f137)) (define-fun f141 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f142 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f143 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f144 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f145 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f146 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f147 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f148 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f149 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f150 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f151 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f152 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f153 () Arctic (+ f33 f150)) (define-fun f154 () Arctic (+ f34 f151)) (define-fun f155 () Arctic (+ f35 f152)) (define-fun f156 () Arctic (+ (* f12 f141) (* f13 f144) (* f14 f147))) (define-fun f157 () Arctic (+ (* f12 f142) (* f13 f145) (* f14 f148))) (define-fun f158 () Arctic (+ (* f12 f143) (* f13 f146) (* f14 f149))) (define-fun f159 () Arctic (+ (* f15 f141) (* f16 f144) (* f17 f147))) (define-fun f160 () Arctic (+ (* f15 f142) (* f16 f145) (* f17 f148))) (define-fun f161 () Arctic (+ (* f15 f143) (* f16 f146) (* f17 f149))) (define-fun f162 () Arctic (+ (* f18 f141) (* f19 f144) (* f20 f147))) (define-fun f163 () Arctic (+ (* f18 f142) (* f19 f145) (* f20 f148))) (define-fun f164 () Arctic (+ (* f18 f143) (* f19 f146) (* f20 f149))) (define-fun f165 () Arctic (+ (* f12 f153) (* f13 f154) (* f14 f155))) (define-fun f166 () Arctic (+ (* f15 f153) (* f16 f154) (* f17 f155))) (define-fun f167 () Arctic (+ (* f18 f153) (* f19 f154) (* f20 f155))) (define-fun f168 () Arctic (+ f21 f165)) (define-fun f169 () Arctic (+ f22 f166)) (define-fun f170 () Arctic (+ f23 f167)) (define-fun f171 () Arctic (+ (* f24 f156) (* f25 f159) (* f26 f162))) (define-fun f172 () Arctic (+ (* f24 f157) (* f25 f160) (* f26 f163))) (define-fun f173 () Arctic (+ (* f24 f158) (* f25 f161) (* f26 f164))) (define-fun f174 () Arctic (+ (* f27 f156) (* f28 f159) (* f29 f162))) (define-fun f175 () Arctic (+ (* f27 f157) (* f28 f160) (* f29 f163))) (define-fun f176 () Arctic (+ (* f27 f158) (* f28 f161) (* f29 f164))) (define-fun f177 () Arctic (+ (* f30 f156) (* f31 f159) (* f32 f162))) (define-fun f178 () Arctic (+ (* f30 f157) (* f31 f160) (* f32 f163))) (define-fun f179 () Arctic (+ (* f30 f158) (* f31 f161) (* f32 f164))) (define-fun f180 () Arctic (+ (* f24 f168) (* f25 f169) (* f26 f170))) (define-fun f181 () Arctic (+ (* f27 f168) (* f28 f169) (* f29 f170))) (define-fun f182 () Arctic (+ (* f30 f168) (* f31 f169) (* f32 f170))) (define-fun f183 () Arctic (+ f33 f180)) (define-fun f184 () Arctic (+ f34 f181)) (define-fun f185 () Arctic (+ f35 f182)) (define-fun f186 () Arctic (+ (* f24 f171) (* f25 f174) (* f26 f177))) (define-fun f187 () Arctic (+ (* f24 f172) (* f25 f175) (* f26 f178))) (define-fun f188 () Arctic (+ (* f24 f173) (* f25 f176) (* f26 f179))) (define-fun f189 () Arctic (+ (* f27 f171) (* f28 f174) (* f29 f177))) (define-fun f190 () Arctic (+ (* f27 f172) (* f28 f175) (* f29 f178))) (define-fun f191 () Arctic (+ (* f27 f173) (* f28 f176) (* f29 f179))) (define-fun f192 () Arctic (+ (* f30 f171) (* f31 f174) (* f32 f177))) (define-fun f193 () Arctic (+ (* f30 f172) (* f31 f175) (* f32 f178))) (define-fun f194 () Arctic (+ (* f30 f173) (* f31 f176) (* f32 f179))) (define-fun f195 () Arctic (+ (* f24 f183) (* f25 f184) (* f26 f185))) (define-fun f196 () Arctic (+ (* f27 f183) (* f28 f184) (* f29 f185))) (define-fun f197 () Arctic (+ (* f30 f183) (* f31 f184) (* f32 f185))) (define-fun f198 () Arctic (+ f33 f195)) (define-fun f199 () Arctic (+ f34 f196)) (define-fun f200 () Arctic (+ f35 f197)) (define-fun f201 () Arctic (+ (* f12 f186) (* f13 f189) (* f14 f192))) (define-fun f202 () Arctic (+ (* f12 f187) (* f13 f190) (* f14 f193))) (define-fun f203 () Arctic (+ (* f12 f188) (* f13 f191) (* f14 f194))) (define-fun f204 () Arctic (+ (* f15 f186) (* f16 f189) (* f17 f192))) (define-fun f205 () Arctic (+ (* f15 f187) (* f16 f190) (* f17 f193))) (define-fun f206 () Arctic (+ (* f15 f188) (* f16 f191) (* f17 f194))) (define-fun f207 () Arctic (+ (* f18 f186) (* f19 f189) (* f20 f192))) (define-fun f208 () Arctic (+ (* f18 f187) (* f19 f190) (* f20 f193))) (define-fun f209 () Arctic (+ (* f18 f188) (* f19 f191) (* f20 f194))) (define-fun f210 () Arctic (+ (* f12 f198) (* f13 f199) (* f14 f200))) (define-fun f211 () Arctic (+ (* f15 f198) (* f16 f199) (* f17 f200))) (define-fun f212 () Arctic (+ (* f18 f198) (* f19 f199) (* f20 f200))) (define-fun f213 () Arctic (+ f21 f210)) (define-fun f214 () Arctic (+ f22 f211)) (define-fun f215 () Arctic (+ f23 f212)) (define-fun f216 () Arctic (+ (* f0 f201) (* f1 f204) (* f2 f207))) (define-fun f217 () Arctic (+ (* f0 f202) (* f1 f205) (* f2 f208))) (define-fun f218 () Arctic (+ (* f0 f203) (* f1 f206) (* f2 f209))) (define-fun f219 () Arctic (+ (* f3 f201) (* f4 f204) (* f5 f207))) (define-fun f220 () Arctic (+ (* f3 f202) (* f4 f205) (* f5 f208))) (define-fun f221 () Arctic (+ (* f3 f203) (* f4 f206) (* f5 f209))) (define-fun f222 () Arctic (+ (* f6 f201) (* f7 f204) (* f8 f207))) (define-fun f223 () Arctic (+ (* f6 f202) (* f7 f205) (* f8 f208))) (define-fun f224 () Arctic (+ (* f6 f203) (* f7 f206) (* f8 f209))) (define-fun f225 () Arctic (+ (* f0 f213) (* f1 f214) (* f2 f215))) (define-fun f226 () Arctic (+ (* f3 f213) (* f4 f214) (* f5 f215))) (define-fun f227 () Arctic (+ (* f6 f213) (* f7 f214) (* f8 f215))) (define-fun f228 () Arctic (+ f9 f225)) (define-fun f229 () Arctic (+ f10 f226)) (define-fun f230 () Arctic (+ f11 f227)) (define-fun f231 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f232 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f233 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f234 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f235 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f236 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f237 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f238 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f239 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f240 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f241 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f242 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f243 () Arctic (+ f21 f240)) (define-fun f244 () Arctic (+ f22 f241)) (define-fun f245 () Arctic (+ f23 f242)) (define-fun f246 () Arctic (+ (* f24 f231) (* f25 f234) (* f26 f237))) (define-fun f247 () Arctic (+ (* f24 f232) (* f25 f235) (* f26 f238))) (define-fun f248 () Arctic (+ (* f24 f233) (* f25 f236) (* f26 f239))) (define-fun f249 () Arctic (+ (* f27 f231) (* f28 f234) (* f29 f237))) (define-fun f250 () Arctic (+ (* f27 f232) (* f28 f235) (* f29 f238))) (define-fun f251 () Arctic (+ (* f27 f233) (* f28 f236) (* f29 f239))) (define-fun f252 () Arctic (+ (* f30 f231) (* f31 f234) (* f32 f237))) (define-fun f253 () Arctic (+ (* f30 f232) (* f31 f235) (* f32 f238))) (define-fun f254 () Arctic (+ (* f30 f233) (* f31 f236) (* f32 f239))) (define-fun f255 () Arctic (+ (* f24 f243) (* f25 f244) (* f26 f245))) (define-fun f256 () Arctic (+ (* f27 f243) (* f28 f244) (* f29 f245))) (define-fun f257 () Arctic (+ (* f30 f243) (* f31 f244) (* f32 f245))) (define-fun f258 () Arctic (+ f33 f255)) (define-fun f259 () Arctic (+ f34 f256)) (define-fun f260 () Arctic (+ f35 f257)) (define-fun f261 () Arctic (+ (* f0 f246) (* f1 f249) (* f2 f252))) (define-fun f262 () Arctic (+ (* f0 f247) (* f1 f250) (* f2 f253))) (define-fun f263 () Arctic (+ (* f0 f248) (* f1 f251) (* f2 f254))) (define-fun f264 () Arctic (+ (* f3 f246) (* f4 f249) (* f5 f252))) (define-fun f265 () Arctic (+ (* f3 f247) (* f4 f250) (* f5 f253))) (define-fun f266 () Arctic (+ (* f3 f248) (* f4 f251) (* f5 f254))) (define-fun f267 () Arctic (+ (* f6 f246) (* f7 f249) (* f8 f252))) (define-fun f268 () Arctic (+ (* f6 f247) (* f7 f250) (* f8 f253))) (define-fun f269 () Arctic (+ (* f6 f248) (* f7 f251) (* f8 f254))) (define-fun f270 () Arctic (+ (* f0 f258) (* f1 f259) (* f2 f260))) (define-fun f271 () Arctic (+ (* f3 f258) (* f4 f259) (* f5 f260))) (define-fun f272 () Arctic (+ (* f6 f258) (* f7 f259) (* f8 f260))) (define-fun f273 () Arctic (+ f9 f270)) (define-fun f274 () Arctic (+ f10 f271)) (define-fun f275 () Arctic (+ f11 f272)) (define-fun f276 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f277 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f278 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f279 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f280 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f281 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f282 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f283 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f284 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f285 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f286 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f287 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f288 () Arctic (+ f33 f285)) (define-fun f289 () Arctic (+ f34 f286)) (define-fun f290 () Arctic (+ f35 f287)) (define-fun f291 () Arctic (+ (* f12 f276) (* f13 f279) (* f14 f282))) (define-fun f292 () Arctic (+ (* f12 f277) (* f13 f280) (* f14 f283))) (define-fun f293 () Arctic (+ (* f12 f278) (* f13 f281) (* f14 f284))) (define-fun f294 () Arctic (+ (* f15 f276) (* f16 f279) (* f17 f282))) (define-fun f295 () Arctic (+ (* f15 f277) (* f16 f280) (* f17 f283))) (define-fun f296 () Arctic (+ (* f15 f278) (* f16 f281) (* f17 f284))) (define-fun f297 () Arctic (+ (* f18 f276) (* f19 f279) (* f20 f282))) (define-fun f298 () Arctic (+ (* f18 f277) (* f19 f280) (* f20 f283))) (define-fun f299 () Arctic (+ (* f18 f278) (* f19 f281) (* f20 f284))) (define-fun f300 () Arctic (+ (* f12 f288) (* f13 f289) (* f14 f290))) (define-fun f301 () Arctic (+ (* f15 f288) (* f16 f289) (* f17 f290))) (define-fun f302 () Arctic (+ (* f18 f288) (* f19 f289) (* f20 f290))) (define-fun f303 () Arctic (+ f21 f300)) (define-fun f304 () Arctic (+ f22 f301)) (define-fun f305 () Arctic (+ f23 f302)) (define-fun f306 () Arctic (+ (* f24 f291) (* f25 f294) (* f26 f297))) (define-fun f307 () Arctic (+ (* f24 f292) (* f25 f295) (* f26 f298))) (define-fun f308 () Arctic (+ (* f24 f293) (* f25 f296) (* f26 f299))) (define-fun f309 () Arctic (+ (* f27 f291) (* f28 f294) (* f29 f297))) (define-fun f310 () Arctic (+ (* f27 f292) (* f28 f295) (* f29 f298))) (define-fun f311 () Arctic (+ (* f27 f293) (* f28 f296) (* f29 f299))) (define-fun f312 () Arctic (+ (* f30 f291) (* f31 f294) (* f32 f297))) (define-fun f313 () Arctic (+ (* f30 f292) (* f31 f295) (* f32 f298))) (define-fun f314 () Arctic (+ (* f30 f293) (* f31 f296) (* f32 f299))) (define-fun f315 () Arctic (+ (* f24 f303) (* f25 f304) (* f26 f305))) (define-fun f316 () Arctic (+ (* f27 f303) (* f28 f304) (* f29 f305))) (define-fun f317 () Arctic (+ (* f30 f303) (* f31 f304) (* f32 f305))) (define-fun f318 () Arctic (+ f33 f315)) (define-fun f319 () Arctic (+ f34 f316)) (define-fun f320 () Arctic (+ f35 f317)) (define-fun f321 () Arctic (+ (* f24 f306) (* f25 f309) (* f26 f312))) (define-fun f322 () Arctic (+ (* f24 f307) (* f25 f310) (* f26 f313))) (define-fun f323 () Arctic (+ (* f24 f308) (* f25 f311) (* f26 f314))) (define-fun f324 () Arctic (+ (* f27 f306) (* f28 f309) (* f29 f312))) (define-fun f325 () Arctic (+ (* f27 f307) (* f28 f310) (* f29 f313))) (define-fun f326 () Arctic (+ (* f27 f308) (* f28 f311) (* f29 f314))) (define-fun f327 () Arctic (+ (* f30 f306) (* f31 f309) (* f32 f312))) (define-fun f328 () Arctic (+ (* f30 f307) (* f31 f310) (* f32 f313))) (define-fun f329 () Arctic (+ (* f30 f308) (* f31 f311) (* f32 f314))) (define-fun f330 () Arctic (+ (* f24 f318) (* f25 f319) (* f26 f320))) (define-fun f331 () Arctic (+ (* f27 f318) (* f28 f319) (* f29 f320))) (define-fun f332 () Arctic (+ (* f30 f318) (* f31 f319) (* f32 f320))) (define-fun f333 () Arctic (+ f33 f330)) (define-fun f334 () Arctic (+ f34 f331)) (define-fun f335 () Arctic (+ f35 f332)) (define-fun f336 () Arctic (+ (* f0 f321) (* f1 f324) (* f2 f327))) (define-fun f337 () Arctic (+ (* f0 f322) (* f1 f325) (* f2 f328))) (define-fun f338 () Arctic (+ (* f0 f323) (* f1 f326) (* f2 f329))) (define-fun f339 () Arctic (+ (* f3 f321) (* f4 f324) (* f5 f327))) (define-fun f340 () Arctic (+ (* f3 f322) (* f4 f325) (* f5 f328))) (define-fun f341 () Arctic (+ (* f3 f323) (* f4 f326) (* f5 f329))) (define-fun f342 () Arctic (+ (* f6 f321) (* f7 f324) (* f8 f327))) (define-fun f343 () Arctic (+ (* f6 f322) (* f7 f325) (* f8 f328))) (define-fun f344 () Arctic (+ (* f6 f323) (* f7 f326) (* f8 f329))) (define-fun f345 () Arctic (+ (* f0 f333) (* f1 f334) (* f2 f335))) (define-fun f346 () Arctic (+ (* f3 f333) (* f4 f334) (* f5 f335))) (define-fun f347 () Arctic (+ (* f6 f333) (* f7 f334) (* f8 f335))) (define-fun f348 () Arctic (+ f9 f345)) (define-fun f349 () Arctic (+ f10 f346)) (define-fun f350 () Arctic (+ f11 f347)) (define-fun f351 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f352 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f353 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f354 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f355 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f356 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f357 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f358 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f359 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f360 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f361 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f362 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f363 () Arctic (+ f21 f360)) (define-fun f364 () Arctic (+ f22 f361)) (define-fun f365 () Arctic (+ f23 f362)) (define-fun f366 () Arctic (+ (* f24 f351) (* f25 f354) (* f26 f357))) (define-fun f367 () Arctic (+ (* f24 f352) (* f25 f355) (* f26 f358))) (define-fun f368 () Arctic (+ (* f24 f353) (* f25 f356) (* f26 f359))) (define-fun f369 () Arctic (+ (* f27 f351) (* f28 f354) (* f29 f357))) (define-fun f370 () Arctic (+ (* f27 f352) (* f28 f355) (* f29 f358))) (define-fun f371 () Arctic (+ (* f27 f353) (* f28 f356) (* f29 f359))) (define-fun f372 () Arctic (+ (* f30 f351) (* f31 f354) (* f32 f357))) (define-fun f373 () Arctic (+ (* f30 f352) (* f31 f355) (* f32 f358))) (define-fun f374 () Arctic (+ (* f30 f353) (* f31 f356) (* f32 f359))) (define-fun f375 () Arctic (+ (* f24 f363) (* f25 f364) (* f26 f365))) (define-fun f376 () Arctic (+ (* f27 f363) (* f28 f364) (* f29 f365))) (define-fun f377 () Arctic (+ (* f30 f363) (* f31 f364) (* f32 f365))) (define-fun f378 () Arctic (+ f33 f375)) (define-fun f379 () Arctic (+ f34 f376)) (define-fun f380 () Arctic (+ f35 f377)) (define-fun f381 () Arctic (+ (* f0 f366) (* f1 f369) (* f2 f372))) (define-fun f382 () Arctic (+ (* f0 f367) (* f1 f370) (* f2 f373))) (define-fun f383 () Arctic (+ (* f0 f368) (* f1 f371) (* f2 f374))) (define-fun f384 () Arctic (+ (* f3 f366) (* f4 f369) (* f5 f372))) (define-fun f385 () Arctic (+ (* f3 f367) (* f4 f370) (* f5 f373))) (define-fun f386 () Arctic (+ (* f3 f368) (* f4 f371) (* f5 f374))) (define-fun f387 () Arctic (+ (* f6 f366) (* f7 f369) (* f8 f372))) (define-fun f388 () Arctic (+ (* f6 f367) (* f7 f370) (* f8 f373))) (define-fun f389 () Arctic (+ (* f6 f368) (* f7 f371) (* f8 f374))) (define-fun f390 () Arctic (+ (* f0 f378) (* f1 f379) (* f2 f380))) (define-fun f391 () Arctic (+ (* f3 f378) (* f4 f379) (* f5 f380))) (define-fun f392 () Arctic (+ (* f6 f378) (* f7 f379) (* f8 f380))) (define-fun f393 () Arctic (+ f9 f390)) (define-fun f394 () Arctic (+ f10 f391)) (define-fun f395 () Arctic (+ f11 f392)) (define-fun f396 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f397 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f398 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f399 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f400 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f401 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f402 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f403 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f404 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f405 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f406 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f407 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f408 () Arctic (+ f33 f405)) (define-fun f409 () Arctic (+ f34 f406)) (define-fun f410 () Arctic (+ f35 f407)) (define-fun f411 () Arctic (+ (* f0 f396) (* f1 f399) (* f2 f402))) (define-fun f412 () Arctic (+ (* f0 f397) (* f1 f400) (* f2 f403))) (define-fun f413 () Arctic (+ (* f0 f398) (* f1 f401) (* f2 f404))) (define-fun f414 () Arctic (+ (* f3 f396) (* f4 f399) (* f5 f402))) (define-fun f415 () Arctic (+ (* f3 f397) (* f4 f400) (* f5 f403))) (define-fun f416 () Arctic (+ (* f3 f398) (* f4 f401) (* f5 f404))) (define-fun f417 () Arctic (+ (* f6 f396) (* f7 f399) (* f8 f402))) (define-fun f418 () Arctic (+ (* f6 f397) (* f7 f400) (* f8 f403))) (define-fun f419 () Arctic (+ (* f6 f398) (* f7 f401) (* f8 f404))) (define-fun f420 () Arctic (+ (* f0 f408) (* f1 f409) (* f2 f410))) (define-fun f421 () Arctic (+ (* f3 f408) (* f4 f409) (* f5 f410))) (define-fun f422 () Arctic (+ (* f6 f408) (* f7 f409) (* f8 f410))) (define-fun f423 () Arctic (+ f9 f420)) (define-fun f424 () Arctic (+ f10 f421)) (define-fun f425 () Arctic (+ f11 f422)) (define-fun f426 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f427 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f428 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f429 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f430 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f431 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f432 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f433 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f434 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f435 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f436 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f437 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f438 () Arctic (+ f21 f435)) (define-fun f439 () Arctic (+ f22 f436)) (define-fun f440 () Arctic (+ f23 f437)) (define-fun f441 () Arctic (+ (* f24 f426) (* f25 f429) (* f26 f432))) (define-fun f442 () Arctic (+ (* f24 f427) (* f25 f430) (* f26 f433))) (define-fun f443 () Arctic (+ (* f24 f428) (* f25 f431) (* f26 f434))) (define-fun f444 () Arctic (+ (* f27 f426) (* f28 f429) (* f29 f432))) (define-fun f445 () Arctic (+ (* f27 f427) (* f28 f430) (* f29 f433))) (define-fun f446 () Arctic (+ (* f27 f428) (* f28 f431) (* f29 f434))) (define-fun f447 () Arctic (+ (* f30 f426) (* f31 f429) (* f32 f432))) (define-fun f448 () Arctic (+ (* f30 f427) (* f31 f430) (* f32 f433))) (define-fun f449 () Arctic (+ (* f30 f428) (* f31 f431) (* f32 f434))) (define-fun f450 () Arctic (+ (* f24 f438) (* f25 f439) (* f26 f440))) (define-fun f451 () Arctic (+ (* f27 f438) (* f28 f439) (* f29 f440))) (define-fun f452 () Arctic (+ (* f30 f438) (* f31 f439) (* f32 f440))) (define-fun f453 () Arctic (+ f33 f450)) (define-fun f454 () Arctic (+ f34 f451)) (define-fun f455 () Arctic (+ f35 f452)) (define-fun f456 () Arctic (+ (* f0 f441) (* f1 f444) (* f2 f447))) (define-fun f457 () Arctic (+ (* f0 f442) (* f1 f445) (* f2 f448))) (define-fun f458 () Arctic (+ (* f0 f443) (* f1 f446) (* f2 f449))) (define-fun f459 () Arctic (+ (* f3 f441) (* f4 f444) (* f5 f447))) (define-fun f460 () Arctic (+ (* f3 f442) (* f4 f445) (* f5 f448))) (define-fun f461 () Arctic (+ (* f3 f443) (* f4 f446) (* f5 f449))) (define-fun f462 () Arctic (+ (* f6 f441) (* f7 f444) (* f8 f447))) (define-fun f463 () Arctic (+ (* f6 f442) (* f7 f445) (* f8 f448))) (define-fun f464 () Arctic (+ (* f6 f443) (* f7 f446) (* f8 f449))) (define-fun f465 () Arctic (+ (* f0 f453) (* f1 f454) (* f2 f455))) (define-fun f466 () Arctic (+ (* f3 f453) (* f4 f454) (* f5 f455))) (define-fun f467 () Arctic (+ (* f6 f453) (* f7 f454) (* f8 f455))) (define-fun f468 () Arctic (+ f9 f465)) (define-fun f469 () Arctic (+ f10 f466)) (define-fun f470 () Arctic (+ f11 f467)) (define-fun f471 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f472 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f473 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f474 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f475 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f476 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f477 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f478 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f479 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f480 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f481 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f482 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f483 () Arctic (+ f33 f480)) (define-fun f484 () Arctic (+ f34 f481)) (define-fun f485 () Arctic (+ f35 f482)) (define-fun f486 () Arctic (+ (* f0 f471) (* f1 f474) (* f2 f477))) (define-fun f487 () Arctic (+ (* f0 f472) (* f1 f475) (* f2 f478))) (define-fun f488 () Arctic (+ (* f0 f473) (* f1 f476) (* f2 f479))) (define-fun f489 () Arctic (+ (* f3 f471) (* f4 f474) (* f5 f477))) (define-fun f490 () Arctic (+ (* f3 f472) (* f4 f475) (* f5 f478))) (define-fun f491 () Arctic (+ (* f3 f473) (* f4 f476) (* f5 f479))) (define-fun f492 () Arctic (+ (* f6 f471) (* f7 f474) (* f8 f477))) (define-fun f493 () Arctic (+ (* f6 f472) (* f7 f475) (* f8 f478))) (define-fun f494 () Arctic (+ (* f6 f473) (* f7 f476) (* f8 f479))) (define-fun f495 () Arctic (+ (* f0 f483) (* f1 f484) (* f2 f485))) (define-fun f496 () Arctic (+ (* f3 f483) (* f4 f484) (* f5 f485))) (define-fun f497 () Arctic (+ (* f6 f483) (* f7 f484) (* f8 f485))) (define-fun f498 () Arctic (+ f9 f495)) (define-fun f499 () Arctic (+ f10 f496)) (define-fun f500 () Arctic (+ f11 f497)) (define-fun f501 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f502 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f503 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f504 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f505 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f506 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f507 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f508 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f509 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f510 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f511 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f512 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f513 () Arctic (+ f33 f510)) (define-fun f514 () Arctic (+ f34 f511)) (define-fun f515 () Arctic (+ f35 f512)) (define-fun f516 () Arctic (+ (* f24 f501) (* f25 f504) (* f26 f507))) (define-fun f517 () Arctic (+ (* f24 f502) (* f25 f505) (* f26 f508))) (define-fun f518 () Arctic (+ (* f24 f503) (* f25 f506) (* f26 f509))) (define-fun f519 () Arctic (+ (* f27 f501) (* f28 f504) (* f29 f507))) (define-fun f520 () Arctic (+ (* f27 f502) (* f28 f505) (* f29 f508))) (define-fun f521 () Arctic (+ (* f27 f503) (* f28 f506) (* f29 f509))) (define-fun f522 () Arctic (+ (* f30 f501) (* f31 f504) (* f32 f507))) (define-fun f523 () Arctic (+ (* f30 f502) (* f31 f505) (* f32 f508))) (define-fun f524 () Arctic (+ (* f30 f503) (* f31 f506) (* f32 f509))) (define-fun f525 () Arctic (+ (* f24 f513) (* f25 f514) (* f26 f515))) (define-fun f526 () Arctic (+ (* f27 f513) (* f28 f514) (* f29 f515))) (define-fun f527 () Arctic (+ (* f30 f513) (* f31 f514) (* f32 f515))) (define-fun f528 () Arctic (+ f33 f525)) (define-fun f529 () Arctic (+ f34 f526)) (define-fun f530 () Arctic (+ f35 f527)) (define-fun f531 () Arctic (+ (* f0 f516) (* f1 f519) (* f2 f522))) (define-fun f532 () Arctic (+ (* f0 f517) (* f1 f520) (* f2 f523))) (define-fun f533 () Arctic (+ (* f0 f518) (* f1 f521) (* f2 f524))) (define-fun f534 () Arctic (+ (* f3 f516) (* f4 f519) (* f5 f522))) (define-fun f535 () Arctic (+ (* f3 f517) (* f4 f520) (* f5 f523))) (define-fun f536 () Arctic (+ (* f3 f518) (* f4 f521) (* f5 f524))) (define-fun f537 () Arctic (+ (* f6 f516) (* f7 f519) (* f8 f522))) (define-fun f538 () Arctic (+ (* f6 f517) (* f7 f520) (* f8 f523))) (define-fun f539 () Arctic (+ (* f6 f518) (* f7 f521) (* f8 f524))) (define-fun f540 () Arctic (+ (* f0 f528) (* f1 f529) (* f2 f530))) (define-fun f541 () Arctic (+ (* f3 f528) (* f4 f529) (* f5 f530))) (define-fun f542 () Arctic (+ (* f6 f528) (* f7 f529) (* f8 f530))) (define-fun f543 () Arctic (+ f9 f540)) (define-fun f544 () Arctic (+ f10 f541)) (define-fun f545 () Arctic (+ f11 f542)) (define-fun f546 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f547 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f548 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f549 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f550 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f551 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f552 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f553 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f554 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f555 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f556 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f557 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f558 () Arctic (+ f33 f555)) (define-fun f559 () Arctic (+ f34 f556)) (define-fun f560 () Arctic (+ f35 f557)) (define-fun f561 () Arctic (+ (* f0 f546) (* f1 f549) (* f2 f552))) (define-fun f562 () Arctic (+ (* f0 f547) (* f1 f550) (* f2 f553))) (define-fun f563 () Arctic (+ (* f0 f548) (* f1 f551) (* f2 f554))) (define-fun f564 () Arctic (+ (* f3 f546) (* f4 f549) (* f5 f552))) (define-fun f565 () Arctic (+ (* f3 f547) (* f4 f550) (* f5 f553))) (define-fun f566 () Arctic (+ (* f3 f548) (* f4 f551) (* f5 f554))) (define-fun f567 () Arctic (+ (* f6 f546) (* f7 f549) (* f8 f552))) (define-fun f568 () Arctic (+ (* f6 f547) (* f7 f550) (* f8 f553))) (define-fun f569 () Arctic (+ (* f6 f548) (* f7 f551) (* f8 f554))) (define-fun f570 () Arctic (+ (* f0 f558) (* f1 f559) (* f2 f560))) (define-fun f571 () Arctic (+ (* f3 f558) (* f4 f559) (* f5 f560))) (define-fun f572 () Arctic (+ (* f6 f558) (* f7 f559) (* f8 f560))) (define-fun f573 () Arctic (+ f9 f570)) (define-fun f574 () Arctic (+ f10 f571)) (define-fun f575 () Arctic (+ f11 f572)) (define-fun f576 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f577 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f578 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f579 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f580 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f581 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f582 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f583 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f584 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f585 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f586 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f587 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f588 () Arctic (+ f33 f585)) (define-fun f589 () Arctic (+ f34 f586)) (define-fun f590 () Arctic (+ f35 f587)) (define-fun f591 () Arctic (+ (* f24 f576) (* f25 f579) (* f26 f582))) (define-fun f592 () Arctic (+ (* f24 f577) (* f25 f580) (* f26 f583))) (define-fun f593 () Arctic (+ (* f24 f578) (* f25 f581) (* f26 f584))) (define-fun f594 () Arctic (+ (* f27 f576) (* f28 f579) (* f29 f582))) (define-fun f595 () Arctic (+ (* f27 f577) (* f28 f580) (* f29 f583))) (define-fun f596 () Arctic (+ (* f27 f578) (* f28 f581) (* f29 f584))) (define-fun f597 () Arctic (+ (* f30 f576) (* f31 f579) (* f32 f582))) (define-fun f598 () Arctic (+ (* f30 f577) (* f31 f580) (* f32 f583))) (define-fun f599 () Arctic (+ (* f30 f578) (* f31 f581) (* f32 f584))) (define-fun f600 () Arctic (+ (* f24 f588) (* f25 f589) (* f26 f590))) (define-fun f601 () Arctic (+ (* f27 f588) (* f28 f589) (* f29 f590))) (define-fun f602 () Arctic (+ (* f30 f588) (* f31 f589) (* f32 f590))) (define-fun f603 () Arctic (+ f33 f600)) (define-fun f604 () Arctic (+ f34 f601)) (define-fun f605 () Arctic (+ f35 f602)) (define-fun f606 () Arctic (+ (* f12 f591) (* f13 f594) (* f14 f597))) (define-fun f607 () Arctic (+ (* f12 f592) (* f13 f595) (* f14 f598))) (define-fun f608 () Arctic (+ (* f12 f593) (* f13 f596) (* f14 f599))) (define-fun f609 () Arctic (+ (* f15 f591) (* f16 f594) (* f17 f597))) (define-fun f610 () Arctic (+ (* f15 f592) (* f16 f595) (* f17 f598))) (define-fun f611 () Arctic (+ (* f15 f593) (* f16 f596) (* f17 f599))) (define-fun f612 () Arctic (+ (* f18 f591) (* f19 f594) (* f20 f597))) (define-fun f613 () Arctic (+ (* f18 f592) (* f19 f595) (* f20 f598))) (define-fun f614 () Arctic (+ (* f18 f593) (* f19 f596) (* f20 f599))) (define-fun f615 () Arctic (+ (* f12 f603) (* f13 f604) (* f14 f605))) (define-fun f616 () Arctic (+ (* f15 f603) (* f16 f604) (* f17 f605))) (define-fun f617 () Arctic (+ (* f18 f603) (* f19 f604) (* f20 f605))) (define-fun f618 () Arctic (+ f21 f615)) (define-fun f619 () Arctic (+ f22 f616)) (define-fun f620 () Arctic (+ f23 f617)) (define-fun f621 () Arctic (+ (* f24 f606) (* f25 f609) (* f26 f612))) (define-fun f622 () Arctic (+ (* f24 f607) (* f25 f610) (* f26 f613))) (define-fun f623 () Arctic (+ (* f24 f608) (* f25 f611) (* f26 f614))) (define-fun f624 () Arctic (+ (* f27 f606) (* f28 f609) (* f29 f612))) (define-fun f625 () Arctic (+ (* f27 f607) (* f28 f610) (* f29 f613))) (define-fun f626 () Arctic (+ (* f27 f608) (* f28 f611) (* f29 f614))) (define-fun f627 () Arctic (+ (* f30 f606) (* f31 f609) (* f32 f612))) (define-fun f628 () Arctic (+ (* f30 f607) (* f31 f610) (* f32 f613))) (define-fun f629 () Arctic (+ (* f30 f608) (* f31 f611) (* f32 f614))) (define-fun f630 () Arctic (+ (* f24 f618) (* f25 f619) (* f26 f620))) (define-fun f631 () Arctic (+ (* f27 f618) (* f28 f619) (* f29 f620))) (define-fun f632 () Arctic (+ (* f30 f618) (* f31 f619) (* f32 f620))) (define-fun f633 () Arctic (+ f33 f630)) (define-fun f634 () Arctic (+ f34 f631)) (define-fun f635 () Arctic (+ f35 f632)) (define-fun f636 () Arctic (+ (* f0 f621) (* f1 f624) (* f2 f627))) (define-fun f637 () Arctic (+ (* f0 f622) (* f1 f625) (* f2 f628))) (define-fun f638 () Arctic (+ (* f0 f623) (* f1 f626) (* f2 f629))) (define-fun f639 () Arctic (+ (* f3 f621) (* f4 f624) (* f5 f627))) (define-fun f640 () Arctic (+ (* f3 f622) (* f4 f625) (* f5 f628))) (define-fun f641 () Arctic (+ (* f3 f623) (* f4 f626) (* f5 f629))) (define-fun f642 () Arctic (+ (* f6 f621) (* f7 f624) (* f8 f627))) (define-fun f643 () Arctic (+ (* f6 f622) (* f7 f625) (* f8 f628))) (define-fun f644 () Arctic (+ (* f6 f623) (* f7 f626) (* f8 f629))) (define-fun f645 () Arctic (+ (* f0 f633) (* f1 f634) (* f2 f635))) (define-fun f646 () Arctic (+ (* f3 f633) (* f4 f634) (* f5 f635))) (define-fun f647 () Arctic (+ (* f6 f633) (* f7 f634) (* f8 f635))) (define-fun f648 () Arctic (+ f9 f645)) (define-fun f649 () Arctic (+ f10 f646)) (define-fun f650 () Arctic (+ f11 f647)) (define-fun f651 () Arctic (+ (* f0 f12) (* f1 f15) (* f2 f18))) (define-fun f652 () Arctic (+ (* f0 f13) (* f1 f16) (* f2 f19))) (define-fun f653 () Arctic (+ (* f0 f14) (* f1 f17) (* f2 f20))) (define-fun f654 () Arctic (+ (* f3 f12) (* f4 f15) (* f5 f18))) (define-fun f655 () Arctic (+ (* f3 f13) (* f4 f16) (* f5 f19))) (define-fun f656 () Arctic (+ (* f3 f14) (* f4 f17) (* f5 f20))) (define-fun f657 () Arctic (+ (* f6 f12) (* f7 f15) (* f8 f18))) (define-fun f658 () Arctic (+ (* f6 f13) (* f7 f16) (* f8 f19))) (define-fun f659 () Arctic (+ (* f6 f14) (* f7 f17) (* f8 f20))) (define-fun f660 () Arctic (+ (* f0 f21) (* f1 f22) (* f2 f23))) (define-fun f661 () Arctic (+ (* f3 f21) (* f4 f22) (* f5 f23))) (define-fun f662 () Arctic (+ (* f6 f21) (* f7 f22) (* f8 f23))) (define-fun f663 () Arctic (+ f9 f660)) (define-fun f664 () Arctic (+ f10 f661)) (define-fun f665 () Arctic (+ f11 f662)) (define-fun f666 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f667 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f668 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f669 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f670 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f671 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f672 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f673 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f674 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f675 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f676 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f677 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f678 () Arctic (+ f33 f675)) (define-fun f679 () Arctic (+ f34 f676)) (define-fun f680 () Arctic (+ f35 f677)) (define-fun f681 () Arctic (+ (* f24 f666) (* f25 f669) (* f26 f672))) (define-fun f682 () Arctic (+ (* f24 f667) (* f25 f670) (* f26 f673))) (define-fun f683 () Arctic (+ (* f24 f668) (* f25 f671) (* f26 f674))) (define-fun f684 () Arctic (+ (* f27 f666) (* f28 f669) (* f29 f672))) (define-fun f685 () Arctic (+ (* f27 f667) (* f28 f670) (* f29 f673))) (define-fun f686 () Arctic (+ (* f27 f668) (* f28 f671) (* f29 f674))) (define-fun f687 () Arctic (+ (* f30 f666) (* f31 f669) (* f32 f672))) (define-fun f688 () Arctic (+ (* f30 f667) (* f31 f670) (* f32 f673))) (define-fun f689 () Arctic (+ (* f30 f668) (* f31 f671) (* f32 f674))) (define-fun f690 () Arctic (+ (* f24 f678) (* f25 f679) (* f26 f680))) (define-fun f691 () Arctic (+ (* f27 f678) (* f28 f679) (* f29 f680))) (define-fun f692 () Arctic (+ (* f30 f678) (* f31 f679) (* f32 f680))) (define-fun f693 () Arctic (+ f33 f690)) (define-fun f694 () Arctic (+ f34 f691)) (define-fun f695 () Arctic (+ f35 f692)) (define-fun f696 () Arctic (+ (* f12 f681) (* f13 f684) (* f14 f687))) (define-fun f697 () Arctic (+ (* f12 f682) (* f13 f685) (* f14 f688))) (define-fun f698 () Arctic (+ (* f12 f683) (* f13 f686) (* f14 f689))) (define-fun f699 () Arctic (+ (* f15 f681) (* f16 f684) (* f17 f687))) (define-fun f700 () Arctic (+ (* f15 f682) (* f16 f685) (* f17 f688))) (define-fun f701 () Arctic (+ (* f15 f683) (* f16 f686) (* f17 f689))) (define-fun f702 () Arctic (+ (* f18 f681) (* f19 f684) (* f20 f687))) (define-fun f703 () Arctic (+ (* f18 f682) (* f19 f685) (* f20 f688))) (define-fun f704 () Arctic (+ (* f18 f683) (* f19 f686) (* f20 f689))) (define-fun f705 () Arctic (+ (* f12 f693) (* f13 f694) (* f14 f695))) (define-fun f706 () Arctic (+ (* f15 f693) (* f16 f694) (* f17 f695))) (define-fun f707 () Arctic (+ (* f18 f693) (* f19 f694) (* f20 f695))) (define-fun f708 () Arctic (+ f21 f705)) (define-fun f709 () Arctic (+ f22 f706)) (define-fun f710 () Arctic (+ f23 f707)) (define-fun f711 () Arctic (+ (* f24 f696) (* f25 f699) (* f26 f702))) (define-fun f712 () Arctic (+ (* f24 f697) (* f25 f700) (* f26 f703))) (define-fun f713 () Arctic (+ (* f24 f698) (* f25 f701) (* f26 f704))) (define-fun f714 () Arctic (+ (* f27 f696) (* f28 f699) (* f29 f702))) (define-fun f715 () Arctic (+ (* f27 f697) (* f28 f700) (* f29 f703))) (define-fun f716 () Arctic (+ (* f27 f698) (* f28 f701) (* f29 f704))) (define-fun f717 () Arctic (+ (* f30 f696) (* f31 f699) (* f32 f702))) (define-fun f718 () Arctic (+ (* f30 f697) (* f31 f700) (* f32 f703))) (define-fun f719 () Arctic (+ (* f30 f698) (* f31 f701) (* f32 f704))) (define-fun f720 () Arctic (+ (* f24 f708) (* f25 f709) (* f26 f710))) (define-fun f721 () Arctic (+ (* f27 f708) (* f28 f709) (* f29 f710))) (define-fun f722 () Arctic (+ (* f30 f708) (* f31 f709) (* f32 f710))) (define-fun f723 () Arctic (+ f33 f720)) (define-fun f724 () Arctic (+ f34 f721)) (define-fun f725 () Arctic (+ f35 f722)) (define-fun f726 () Arctic (+ (* f0 f711) (* f1 f714) (* f2 f717))) (define-fun f727 () Arctic (+ (* f0 f712) (* f1 f715) (* f2 f718))) (define-fun f728 () Arctic (+ (* f0 f713) (* f1 f716) (* f2 f719))) (define-fun f729 () Arctic (+ (* f3 f711) (* f4 f714) (* f5 f717))) (define-fun f730 () Arctic (+ (* f3 f712) (* f4 f715) (* f5 f718))) (define-fun f731 () Arctic (+ (* f3 f713) (* f4 f716) (* f5 f719))) (define-fun f732 () Arctic (+ (* f6 f711) (* f7 f714) (* f8 f717))) (define-fun f733 () Arctic (+ (* f6 f712) (* f7 f715) (* f8 f718))) (define-fun f734 () Arctic (+ (* f6 f713) (* f7 f716) (* f8 f719))) (define-fun f735 () Arctic (+ (* f0 f723) (* f1 f724) (* f2 f725))) (define-fun f736 () Arctic (+ (* f3 f723) (* f4 f724) (* f5 f725))) (define-fun f737 () Arctic (+ (* f6 f723) (* f7 f724) (* f8 f725))) (define-fun f738 () Arctic (+ f9 f735)) (define-fun f739 () Arctic (+ f10 f736)) (define-fun f740 () Arctic (+ f11 f737)) (define-fun f741 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f742 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f743 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f744 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f745 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f746 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f747 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f748 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f749 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f750 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f751 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f752 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f753 () Arctic (+ f21 f750)) (define-fun f754 () Arctic (+ f22 f751)) (define-fun f755 () Arctic (+ f23 f752)) (define-fun f756 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f757 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f758 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f759 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f760 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f761 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f762 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f763 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f764 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f765 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f766 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f767 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f768 () Arctic (+ f33 f765)) (define-fun f769 () Arctic (+ f34 f766)) (define-fun f770 () Arctic (+ f35 f767)) (define-fun f771 () Arctic (+ (* f12 f756) (* f13 f759) (* f14 f762))) (define-fun f772 () Arctic (+ (* f12 f757) (* f13 f760) (* f14 f763))) (define-fun f773 () Arctic (+ (* f12 f758) (* f13 f761) (* f14 f764))) (define-fun f774 () Arctic (+ (* f15 f756) (* f16 f759) (* f17 f762))) (define-fun f775 () Arctic (+ (* f15 f757) (* f16 f760) (* f17 f763))) (define-fun f776 () Arctic (+ (* f15 f758) (* f16 f761) (* f17 f764))) (define-fun f777 () Arctic (+ (* f18 f756) (* f19 f759) (* f20 f762))) (define-fun f778 () Arctic (+ (* f18 f757) (* f19 f760) (* f20 f763))) (define-fun f779 () Arctic (+ (* f18 f758) (* f19 f761) (* f20 f764))) (define-fun f780 () Arctic (+ (* f12 f768) (* f13 f769) (* f14 f770))) (define-fun f781 () Arctic (+ (* f15 f768) (* f16 f769) (* f17 f770))) (define-fun f782 () Arctic (+ (* f18 f768) (* f19 f769) (* f20 f770))) (define-fun f783 () Arctic (+ f21 f780)) (define-fun f784 () Arctic (+ f22 f781)) (define-fun f785 () Arctic (+ f23 f782)) (define-fun f786 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f787 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f788 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f789 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f790 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f791 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f792 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f793 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f794 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f795 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f796 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f797 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f798 () Arctic (+ f21 f795)) (define-fun f799 () Arctic (+ f22 f796)) (define-fun f800 () Arctic (+ f23 f797)) (define-fun f801 () Arctic (+ (* f24 f786) (* f25 f789) (* f26 f792))) (define-fun f802 () Arctic (+ (* f24 f787) (* f25 f790) (* f26 f793))) (define-fun f803 () Arctic (+ (* f24 f788) (* f25 f791) (* f26 f794))) (define-fun f804 () Arctic (+ (* f27 f786) (* f28 f789) (* f29 f792))) (define-fun f805 () Arctic (+ (* f27 f787) (* f28 f790) (* f29 f793))) (define-fun f806 () Arctic (+ (* f27 f788) (* f28 f791) (* f29 f794))) (define-fun f807 () Arctic (+ (* f30 f786) (* f31 f789) (* f32 f792))) (define-fun f808 () Arctic (+ (* f30 f787) (* f31 f790) (* f32 f793))) (define-fun f809 () Arctic (+ (* f30 f788) (* f31 f791) (* f32 f794))) (define-fun f810 () Arctic (+ (* f24 f798) (* f25 f799) (* f26 f800))) (define-fun f811 () Arctic (+ (* f27 f798) (* f28 f799) (* f29 f800))) (define-fun f812 () Arctic (+ (* f30 f798) (* f31 f799) (* f32 f800))) (define-fun f813 () Arctic (+ f33 f810)) (define-fun f814 () Arctic (+ f34 f811)) (define-fun f815 () Arctic (+ f35 f812)) (define-fun f816 () Arctic (+ (* f12 f801) (* f13 f804) (* f14 f807))) (define-fun f817 () Arctic (+ (* f12 f802) (* f13 f805) (* f14 f808))) (define-fun f818 () Arctic (+ (* f12 f803) (* f13 f806) (* f14 f809))) (define-fun f819 () Arctic (+ (* f15 f801) (* f16 f804) (* f17 f807))) (define-fun f820 () Arctic (+ (* f15 f802) (* f16 f805) (* f17 f808))) (define-fun f821 () Arctic (+ (* f15 f803) (* f16 f806) (* f17 f809))) (define-fun f822 () Arctic (+ (* f18 f801) (* f19 f804) (* f20 f807))) (define-fun f823 () Arctic (+ (* f18 f802) (* f19 f805) (* f20 f808))) (define-fun f824 () Arctic (+ (* f18 f803) (* f19 f806) (* f20 f809))) (define-fun f825 () Arctic (+ (* f12 f813) (* f13 f814) (* f14 f815))) (define-fun f826 () Arctic (+ (* f15 f813) (* f16 f814) (* f17 f815))) (define-fun f827 () Arctic (+ (* f18 f813) (* f19 f814) (* f20 f815))) (define-fun f828 () Arctic (+ f21 f825)) (define-fun f829 () Arctic (+ f22 f826)) (define-fun f830 () Arctic (+ f23 f827)) (define-fun f831 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f832 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f833 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f834 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f835 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f836 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f837 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f838 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f839 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f840 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f841 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f842 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f843 () Arctic (+ f33 f840)) (define-fun f844 () Arctic (+ f34 f841)) (define-fun f845 () Arctic (+ f35 f842)) (define-fun f846 () Arctic (+ (* f12 f831) (* f13 f834) (* f14 f837))) (define-fun f847 () Arctic (+ (* f12 f832) (* f13 f835) (* f14 f838))) (define-fun f848 () Arctic (+ (* f12 f833) (* f13 f836) (* f14 f839))) (define-fun f849 () Arctic (+ (* f15 f831) (* f16 f834) (* f17 f837))) (define-fun f850 () Arctic (+ (* f15 f832) (* f16 f835) (* f17 f838))) (define-fun f851 () Arctic (+ (* f15 f833) (* f16 f836) (* f17 f839))) (define-fun f852 () Arctic (+ (* f18 f831) (* f19 f834) (* f20 f837))) (define-fun f853 () Arctic (+ (* f18 f832) (* f19 f835) (* f20 f838))) (define-fun f854 () Arctic (+ (* f18 f833) (* f19 f836) (* f20 f839))) (define-fun f855 () Arctic (+ (* f12 f843) (* f13 f844) (* f14 f845))) (define-fun f856 () Arctic (+ (* f15 f843) (* f16 f844) (* f17 f845))) (define-fun f857 () Arctic (+ (* f18 f843) (* f19 f844) (* f20 f845))) (define-fun f858 () Arctic (+ f21 f855)) (define-fun f859 () Arctic (+ f22 f856)) (define-fun f860 () Arctic (+ f23 f857)) (define-fun f861 () Arctic (+ (* f24 f846) (* f25 f849) (* f26 f852))) (define-fun f862 () Arctic (+ (* f24 f847) (* f25 f850) (* f26 f853))) (define-fun f863 () Arctic (+ (* f24 f848) (* f25 f851) (* f26 f854))) (define-fun f864 () Arctic (+ (* f27 f846) (* f28 f849) (* f29 f852))) (define-fun f865 () Arctic (+ (* f27 f847) (* f28 f850) (* f29 f853))) (define-fun f866 () Arctic (+ (* f27 f848) (* f28 f851) (* f29 f854))) (define-fun f867 () Arctic (+ (* f30 f846) (* f31 f849) (* f32 f852))) (define-fun f868 () Arctic (+ (* f30 f847) (* f31 f850) (* f32 f853))) (define-fun f869 () Arctic (+ (* f30 f848) (* f31 f851) (* f32 f854))) (define-fun f870 () Arctic (+ (* f24 f858) (* f25 f859) (* f26 f860))) (define-fun f871 () Arctic (+ (* f27 f858) (* f28 f859) (* f29 f860))) (define-fun f872 () Arctic (+ (* f30 f858) (* f31 f859) (* f32 f860))) (define-fun f873 () Arctic (+ f33 f870)) (define-fun f874 () Arctic (+ f34 f871)) (define-fun f875 () Arctic (+ f35 f872)) (define-fun f876 () Arctic (+ (* f24 f861) (* f25 f864) (* f26 f867))) (define-fun f877 () Arctic (+ (* f24 f862) (* f25 f865) (* f26 f868))) (define-fun f878 () Arctic (+ (* f24 f863) (* f25 f866) (* f26 f869))) (define-fun f879 () Arctic (+ (* f27 f861) (* f28 f864) (* f29 f867))) (define-fun f880 () Arctic (+ (* f27 f862) (* f28 f865) (* f29 f868))) (define-fun f881 () Arctic (+ (* f27 f863) (* f28 f866) (* f29 f869))) (define-fun f882 () Arctic (+ (* f30 f861) (* f31 f864) (* f32 f867))) (define-fun f883 () Arctic (+ (* f30 f862) (* f31 f865) (* f32 f868))) (define-fun f884 () Arctic (+ (* f30 f863) (* f31 f866) (* f32 f869))) (define-fun f885 () Arctic (+ (* f24 f873) (* f25 f874) (* f26 f875))) (define-fun f886 () Arctic (+ (* f27 f873) (* f28 f874) (* f29 f875))) (define-fun f887 () Arctic (+ (* f30 f873) (* f31 f874) (* f32 f875))) (define-fun f888 () Arctic (+ f33 f885)) (define-fun f889 () Arctic (+ f34 f886)) (define-fun f890 () Arctic (+ f35 f887)) (define-fun f891 () Arctic (+ (* f12 f876) (* f13 f879) (* f14 f882))) (define-fun f892 () Arctic (+ (* f12 f877) (* f13 f880) (* f14 f883))) (define-fun f893 () Arctic (+ (* f12 f878) (* f13 f881) (* f14 f884))) (define-fun f894 () Arctic (+ (* f15 f876) (* f16 f879) (* f17 f882))) (define-fun f895 () Arctic (+ (* f15 f877) (* f16 f880) (* f17 f883))) (define-fun f896 () Arctic (+ (* f15 f878) (* f16 f881) (* f17 f884))) (define-fun f897 () Arctic (+ (* f18 f876) (* f19 f879) (* f20 f882))) (define-fun f898 () Arctic (+ (* f18 f877) (* f19 f880) (* f20 f883))) (define-fun f899 () Arctic (+ (* f18 f878) (* f19 f881) (* f20 f884))) (define-fun f900 () Arctic (+ (* f12 f888) (* f13 f889) (* f14 f890))) (define-fun f901 () Arctic (+ (* f15 f888) (* f16 f889) (* f17 f890))) (define-fun f902 () Arctic (+ (* f18 f888) (* f19 f889) (* f20 f890))) (define-fun f903 () Arctic (+ f21 f900)) (define-fun f904 () Arctic (+ f22 f901)) (define-fun f905 () Arctic (+ f23 f902)) (define-fun f906 () Arctic (+ (* f12 f891) (* f13 f894) (* f14 f897))) (define-fun f907 () Arctic (+ (* f12 f892) (* f13 f895) (* f14 f898))) (define-fun f908 () Arctic (+ (* f12 f893) (* f13 f896) (* f14 f899))) (define-fun f909 () Arctic (+ (* f15 f891) (* f16 f894) (* f17 f897))) (define-fun f910 () Arctic (+ (* f15 f892) (* f16 f895) (* f17 f898))) (define-fun f911 () Arctic (+ (* f15 f893) (* f16 f896) (* f17 f899))) (define-fun f912 () Arctic (+ (* f18 f891) (* f19 f894) (* f20 f897))) (define-fun f913 () Arctic (+ (* f18 f892) (* f19 f895) (* f20 f898))) (define-fun f914 () Arctic (+ (* f18 f893) (* f19 f896) (* f20 f899))) (define-fun f915 () Arctic (+ (* f12 f903) (* f13 f904) (* f14 f905))) (define-fun f916 () Arctic (+ (* f15 f903) (* f16 f904) (* f17 f905))) (define-fun f917 () Arctic (+ (* f18 f903) (* f19 f904) (* f20 f905))) (define-fun f918 () Arctic (+ f21 f915)) (define-fun f919 () Arctic (+ f22 f916)) (define-fun f920 () Arctic (+ f23 f917)) (define-fun f921 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f922 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f923 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f924 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f925 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f926 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f927 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f928 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f929 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f930 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f931 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f932 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f933 () Arctic (+ f33 f930)) (define-fun f934 () Arctic (+ f34 f931)) (define-fun f935 () Arctic (+ f35 f932)) (define-fun f936 () Arctic (+ (* f12 f921) (* f13 f924) (* f14 f927))) (define-fun f937 () Arctic (+ (* f12 f922) (* f13 f925) (* f14 f928))) (define-fun f938 () Arctic (+ (* f12 f923) (* f13 f926) (* f14 f929))) (define-fun f939 () Arctic (+ (* f15 f921) (* f16 f924) (* f17 f927))) (define-fun f940 () Arctic (+ (* f15 f922) (* f16 f925) (* f17 f928))) (define-fun f941 () Arctic (+ (* f15 f923) (* f16 f926) (* f17 f929))) (define-fun f942 () Arctic (+ (* f18 f921) (* f19 f924) (* f20 f927))) (define-fun f943 () Arctic (+ (* f18 f922) (* f19 f925) (* f20 f928))) (define-fun f944 () Arctic (+ (* f18 f923) (* f19 f926) (* f20 f929))) (define-fun f945 () Arctic (+ (* f12 f933) (* f13 f934) (* f14 f935))) (define-fun f946 () Arctic (+ (* f15 f933) (* f16 f934) (* f17 f935))) (define-fun f947 () Arctic (+ (* f18 f933) (* f19 f934) (* f20 f935))) (define-fun f948 () Arctic (+ f21 f945)) (define-fun f949 () Arctic (+ f22 f946)) (define-fun f950 () Arctic (+ f23 f947)) (define-fun f951 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f952 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f953 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f954 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f955 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f956 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f957 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f958 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f959 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f960 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f961 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f962 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f963 () Arctic (+ f33 f960)) (define-fun f964 () Arctic (+ f34 f961)) (define-fun f965 () Arctic (+ f35 f962)) (define-fun f966 () Arctic (+ (* f24 f951) (* f25 f954) (* f26 f957))) (define-fun f967 () Arctic (+ (* f24 f952) (* f25 f955) (* f26 f958))) (define-fun f968 () Arctic (+ (* f24 f953) (* f25 f956) (* f26 f959))) (define-fun f969 () Arctic (+ (* f27 f951) (* f28 f954) (* f29 f957))) (define-fun f970 () Arctic (+ (* f27 f952) (* f28 f955) (* f29 f958))) (define-fun f971 () Arctic (+ (* f27 f953) (* f28 f956) (* f29 f959))) (define-fun f972 () Arctic (+ (* f30 f951) (* f31 f954) (* f32 f957))) (define-fun f973 () Arctic (+ (* f30 f952) (* f31 f955) (* f32 f958))) (define-fun f974 () Arctic (+ (* f30 f953) (* f31 f956) (* f32 f959))) (define-fun f975 () Arctic (+ (* f24 f963) (* f25 f964) (* f26 f965))) (define-fun f976 () Arctic (+ (* f27 f963) (* f28 f964) (* f29 f965))) (define-fun f977 () Arctic (+ (* f30 f963) (* f31 f964) (* f32 f965))) (define-fun f978 () Arctic (+ f33 f975)) (define-fun f979 () Arctic (+ f34 f976)) (define-fun f980 () Arctic (+ f35 f977)) (define-fun f981 () Arctic (+ (* f12 f966) (* f13 f969) (* f14 f972))) (define-fun f982 () Arctic (+ (* f12 f967) (* f13 f970) (* f14 f973))) (define-fun f983 () Arctic (+ (* f12 f968) (* f13 f971) (* f14 f974))) (define-fun f984 () Arctic (+ (* f15 f966) (* f16 f969) (* f17 f972))) (define-fun f985 () Arctic (+ (* f15 f967) (* f16 f970) (* f17 f973))) (define-fun f986 () Arctic (+ (* f15 f968) (* f16 f971) (* f17 f974))) (define-fun f987 () Arctic (+ (* f18 f966) (* f19 f969) (* f20 f972))) (define-fun f988 () Arctic (+ (* f18 f967) (* f19 f970) (* f20 f973))) (define-fun f989 () Arctic (+ (* f18 f968) (* f19 f971) (* f20 f974))) (define-fun f990 () Arctic (+ (* f12 f978) (* f13 f979) (* f14 f980))) (define-fun f991 () Arctic (+ (* f15 f978) (* f16 f979) (* f17 f980))) (define-fun f992 () Arctic (+ (* f18 f978) (* f19 f979) (* f20 f980))) (define-fun f993 () Arctic (+ f21 f990)) (define-fun f994 () Arctic (+ f22 f991)) (define-fun f995 () Arctic (+ f23 f992)) (define-fun f996 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f997 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f998 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f999 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f1000 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f1001 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f1002 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f1003 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f1004 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f1005 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f1006 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f1007 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f1008 () Arctic (+ f33 f1005)) (define-fun f1009 () Arctic (+ f34 f1006)) (define-fun f1010 () Arctic (+ f35 f1007)) (define-fun f1011 () Arctic (+ (* f24 f996) (* f25 f999) (* f26 f1002))) (define-fun f1012 () Arctic (+ (* f24 f997) (* f25 f1000) (* f26 f1003))) (define-fun f1013 () Arctic (+ (* f24 f998) (* f25 f1001) (* f26 f1004))) (define-fun f1014 () Arctic (+ (* f27 f996) (* f28 f999) (* f29 f1002))) (define-fun f1015 () Arctic (+ (* f27 f997) (* f28 f1000) (* f29 f1003))) (define-fun f1016 () Arctic (+ (* f27 f998) (* f28 f1001) (* f29 f1004))) (define-fun f1017 () Arctic (+ (* f30 f996) (* f31 f999) (* f32 f1002))) (define-fun f1018 () Arctic (+ (* f30 f997) (* f31 f1000) (* f32 f1003))) (define-fun f1019 () Arctic (+ (* f30 f998) (* f31 f1001) (* f32 f1004))) (define-fun f1020 () Arctic (+ (* f24 f1008) (* f25 f1009) (* f26 f1010))) (define-fun f1021 () Arctic (+ (* f27 f1008) (* f28 f1009) (* f29 f1010))) (define-fun f1022 () Arctic (+ (* f30 f1008) (* f31 f1009) (* f32 f1010))) (define-fun f1023 () Arctic (+ f33 f1020)) (define-fun f1024 () Arctic (+ f34 f1021)) (define-fun f1025 () Arctic (+ f35 f1022)) (define-fun f1026 () Arctic (+ (* f12 f1011) (* f13 f1014) (* f14 f1017))) (define-fun f1027 () Arctic (+ (* f12 f1012) (* f13 f1015) (* f14 f1018))) (define-fun f1028 () Arctic (+ (* f12 f1013) (* f13 f1016) (* f14 f1019))) (define-fun f1029 () Arctic (+ (* f15 f1011) (* f16 f1014) (* f17 f1017))) (define-fun f1030 () Arctic (+ (* f15 f1012) (* f16 f1015) (* f17 f1018))) (define-fun f1031 () Arctic (+ (* f15 f1013) (* f16 f1016) (* f17 f1019))) (define-fun f1032 () Arctic (+ (* f18 f1011) (* f19 f1014) (* f20 f1017))) (define-fun f1033 () Arctic (+ (* f18 f1012) (* f19 f1015) (* f20 f1018))) (define-fun f1034 () Arctic (+ (* f18 f1013) (* f19 f1016) (* f20 f1019))) (define-fun f1035 () Arctic (+ (* f12 f1023) (* f13 f1024) (* f14 f1025))) (define-fun f1036 () Arctic (+ (* f15 f1023) (* f16 f1024) (* f17 f1025))) (define-fun f1037 () Arctic (+ (* f18 f1023) (* f19 f1024) (* f20 f1025))) (define-fun f1038 () Arctic (+ f21 f1035)) (define-fun f1039 () Arctic (+ f22 f1036)) (define-fun f1040 () Arctic (+ f23 f1037)) (define-fun f1041 () Arctic (+ (* f24 f1026) (* f25 f1029) (* f26 f1032))) (define-fun f1042 () Arctic (+ (* f24 f1027) (* f25 f1030) (* f26 f1033))) (define-fun f1043 () Arctic (+ (* f24 f1028) (* f25 f1031) (* f26 f1034))) (define-fun f1044 () Arctic (+ (* f27 f1026) (* f28 f1029) (* f29 f1032))) (define-fun f1045 () Arctic (+ (* f27 f1027) (* f28 f1030) (* f29 f1033))) (define-fun f1046 () Arctic (+ (* f27 f1028) (* f28 f1031) (* f29 f1034))) (define-fun f1047 () Arctic (+ (* f30 f1026) (* f31 f1029) (* f32 f1032))) (define-fun f1048 () Arctic (+ (* f30 f1027) (* f31 f1030) (* f32 f1033))) (define-fun f1049 () Arctic (+ (* f30 f1028) (* f31 f1031) (* f32 f1034))) (define-fun f1050 () Arctic (+ (* f24 f1038) (* f25 f1039) (* f26 f1040))) (define-fun f1051 () Arctic (+ (* f27 f1038) (* f28 f1039) (* f29 f1040))) (define-fun f1052 () Arctic (+ (* f30 f1038) (* f31 f1039) (* f32 f1040))) (define-fun f1053 () Arctic (+ f33 f1050)) (define-fun f1054 () Arctic (+ f34 f1051)) (define-fun f1055 () Arctic (+ f35 f1052)) (define-fun f1056 () Arctic (+ (* f12 f1041) (* f13 f1044) (* f14 f1047))) (define-fun f1057 () Arctic (+ (* f12 f1042) (* f13 f1045) (* f14 f1048))) (define-fun f1058 () Arctic (+ (* f12 f1043) (* f13 f1046) (* f14 f1049))) (define-fun f1059 () Arctic (+ (* f15 f1041) (* f16 f1044) (* f17 f1047))) (define-fun f1060 () Arctic (+ (* f15 f1042) (* f16 f1045) (* f17 f1048))) (define-fun f1061 () Arctic (+ (* f15 f1043) (* f16 f1046) (* f17 f1049))) (define-fun f1062 () Arctic (+ (* f18 f1041) (* f19 f1044) (* f20 f1047))) (define-fun f1063 () Arctic (+ (* f18 f1042) (* f19 f1045) (* f20 f1048))) (define-fun f1064 () Arctic (+ (* f18 f1043) (* f19 f1046) (* f20 f1049))) (define-fun f1065 () Arctic (+ (* f12 f1053) (* f13 f1054) (* f14 f1055))) (define-fun f1066 () Arctic (+ (* f15 f1053) (* f16 f1054) (* f17 f1055))) (define-fun f1067 () Arctic (+ (* f18 f1053) (* f19 f1054) (* f20 f1055))) (define-fun f1068 () Arctic (+ f21 f1065)) (define-fun f1069 () Arctic (+ f22 f1066)) (define-fun f1070 () Arctic (+ f23 f1067)) (define-fun f1071 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f1072 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f1073 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f1074 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f1075 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f1076 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f1077 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f1078 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f1079 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f1080 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f1081 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f1082 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f1083 () Arctic (+ f21 f1080)) (define-fun f1084 () Arctic (+ f22 f1081)) (define-fun f1085 () Arctic (+ f23 f1082)) (assert (and (and (and (and (>= f36 f66) (>= f37 f67) (>= f38 f68)) (and (>= f39 f69) (>= f40 f70) (>= f41 f71)) (and (>= f42 f72) (>= f43 f73) (>= f44 f74))) (and (and (>= f48 f78)) (and (>= f49 f79)) (and (>= f50 f80)))) (and (and (and (>= f81 f0) (>= f82 f1) (>= f83 f2)) (and (>= f84 f3) (>= f85 f4) (>= f86 f5)) (and (>= f87 f6) (>= f88 f7) (>= f89 f8))) (and (and (>= f93 f9)) (and (>= f94 f10)) (and (>= f95 f11)))) (and (and (and (>= f126 f216) (>= f127 f217) (>= f128 f218)) (and (>= f129 f219) (>= f130 f220) (>= f131 f221)) (and (>= f132 f222) (>= f133 f223) (>= f134 f224))) (and (and (>= f138 f228)) (and (>= f139 f229)) (and (>= f140 f230)))) (and (and (and (>= f261 f336) (>= f262 f337) (>= f263 f338)) (and (>= f264 f339) (>= f265 f340) (>= f266 f341)) (and (>= f267 f342) (>= f268 f343) (>= f269 f344))) (and (and (>= f273 f348)) (and (>= f274 f349)) (and (>= f275 f350)))) (and (and (and (>= f381 f411) (>= f382 f412) (>= f383 f413)) (and (>= f384 f414) (>= f385 f415) (>= f386 f416)) (and (>= f387 f417) (>= f388 f418) (>= f389 f419))) (and (and (>= f393 f423)) (and (>= f394 f424)) (and (>= f395 f425)))) (and (and (and (>= f456 f0) (>= f457 f1) (>= f458 f2)) (and (>= f459 f3) (>= f460 f4) (>= f461 f5)) (and (>= f462 f6) (>= f463 f7) (>= f464 f8))) (and (and (>= f468 f9)) (and (>= f469 f10)) (and (>= f470 f11)))) (and (and (and (>= f486 f531) (>= f487 f532) (>= f488 f533)) (and (>= f489 f534) (>= f490 f535) (>= f491 f536)) (and (>= f492 f537) (>= f493 f538) (>= f494 f539))) (and (and (>= f498 f543)) (and (>= f499 f544)) (and (>= f500 f545)))) (and (and (and (>= f561 f0) (>= f562 f1) (>= f563 f2)) (and (>= f564 f3) (>= f565 f4) (>= f566 f5)) (and (>= f567 f6) (>= f568 f7) (>= f569 f8))) (and (and (>= f573 f9)) (and (>= f574 f10)) (and (>= f575 f11)))) (and (and (and (>= f636 f651) (>= f637 f652) (>= f638 f653)) (and (>= f639 f654) (>= f640 f655) (>= f641 f656)) (and (>= f642 f657) (>= f643 f658) (>= f644 f659))) (and (and (>= f648 f663)) (and (>= f649 f664)) (and (>= f650 f665)))) (and (and (and (>= f726 f0) (>= f727 f1) (>= f728 f2)) (and (>= f729 f3) (>= f730 f4) (>= f731 f5)) (and (>= f732 f6) (>= f733 f7) (>= f734 f8))) (and (and (>= f738 f9)) (and (>= f739 f10)) (and (>= f740 f11)))) (and (and (and (>= f741 f771) (>= f742 f772) (>= f743 f773)) (and (>= f744 f774) (>= f745 f775) (>= f746 f776)) (and (>= f747 f777) (>= f748 f778) (>= f749 f779))) (and (and (>= f753 f783)) (and (>= f754 f784)) (and (>= f755 f785)))) (and (and (and (>= f816 f906) (>= f817 f907) (>= f818 f908)) (and (>= f819 f909) (>= f820 f910) (>= f821 f911)) (and (>= f822 f912) (>= f823 f913) (>= f824 f914))) (and (and (>= f828 f918)) (and (>= f829 f919)) (and (>= f830 f920)))) (and (and (and (>= f936 f981) (>= f937 f982) (>= f938 f983)) (and (>= f939 f984) (>= f940 f985) (>= f941 f986)) (and (>= f942 f987) (>= f943 f988) (>= f944 f989))) (and (and (>= f948 f993)) (and (>= f949 f994)) (and (>= f950 f995)))) (and (and (and (>= f1056 f1071) (>= f1057 f1072) (>= f1058 f1073)) (and (>= f1059 f1074) (>= f1060 f1075) (>= f1061 f1076)) (and (>= f1062 f1077) (>= f1063 f1078) (>= f1064 f1079))) (and (and (>= f1068 f1083)) (and (>= f1069 f1084)) (and (>= f1070 f1085)))))) (assert (or (and (and (and (>> f36 f66) (>> f37 f67) (>> f38 f68)) (and (>> f39 f69) (>> f40 f70) (>> f41 f71)) (and (>> f42 f72) (>> f43 f73) (>> f44 f74))) (and (and (>> f48 f78)) (and (>> f49 f79)) (and (>> f50 f80)))) (and (and (and (>> f81 f0) (>> f82 f1) (>> f83 f2)) (and (>> f84 f3) (>> f85 f4) (>> f86 f5)) (and (>> f87 f6) (>> f88 f7) (>> f89 f8))) (and (and (>> f93 f9)) (and (>> f94 f10)) (and (>> f95 f11)))) (and (and (and (>> f126 f216) (>> f127 f217) (>> f128 f218)) (and (>> f129 f219) (>> f130 f220) (>> f131 f221)) (and (>> f132 f222) (>> f133 f223) (>> f134 f224))) (and (and (>> f138 f228)) (and (>> f139 f229)) (and (>> f140 f230)))) (and (and (and (>> f261 f336) (>> f262 f337) (>> f263 f338)) (and (>> f264 f339) (>> f265 f340) (>> f266 f341)) (and (>> f267 f342) (>> f268 f343) (>> f269 f344))) (and (and (>> f273 f348)) (and (>> f274 f349)) (and (>> f275 f350)))) (and (and (and (>> f381 f411) (>> f382 f412) (>> f383 f413)) (and (>> f384 f414) (>> f385 f415) (>> f386 f416)) (and (>> f387 f417) (>> f388 f418) (>> f389 f419))) (and (and (>> f393 f423)) (and (>> f394 f424)) (and (>> f395 f425)))) (and (and (and (>> f456 f0) (>> f457 f1) (>> f458 f2)) (and (>> f459 f3) (>> f460 f4) (>> f461 f5)) (and (>> f462 f6) (>> f463 f7) (>> f464 f8))) (and (and (>> f468 f9)) (and (>> f469 f10)) (and (>> f470 f11)))) (and (and (and (>> f486 f531) (>> f487 f532) (>> f488 f533)) (and (>> f489 f534) (>> f490 f535) (>> f491 f536)) (and (>> f492 f537) (>> f493 f538) (>> f494 f539))) (and (and (>> f498 f543)) (and (>> f499 f544)) (and (>> f500 f545)))) (and (and (and (>> f561 f0) (>> f562 f1) (>> f563 f2)) (and (>> f564 f3) (>> f565 f4) (>> f566 f5)) (and (>> f567 f6) (>> f568 f7) (>> f569 f8))) (and (and (>> f573 f9)) (and (>> f574 f10)) (and (>> f575 f11)))) (and (and (and (>> f636 f651) (>> f637 f652) (>> f638 f653)) (and (>> f639 f654) (>> f640 f655) (>> f641 f656)) (and (>> f642 f657) (>> f643 f658) (>> f644 f659))) (and (and (>> f648 f663)) (and (>> f649 f664)) (and (>> f650 f665)))) (and (and (and (>> f726 f0) (>> f727 f1) (>> f728 f2)) (and (>> f729 f3) (>> f730 f4) (>> f731 f5)) (and (>> f732 f6) (>> f733 f7) (>> f734 f8))) (and (and (>> f738 f9)) (and (>> f739 f10)) (and (>> f740 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 f768 f769 f770 f771 f772 f773 f774 f775 f776 f777 f778 f779 f780 f781 f782 f783 f784 f785 f786 f787 f788 f789 f790 f791 f792 f793 f794 f795 f796 f797 f798 f799 f800 f801 f802 f803 f804 f805 f806 f807 f808 f809 f810 f811 f812 f813 f814 f815 f816 f817 f818 f819 f820 f821 f822 f823 f824 f825 f826 f827 f828 f829 f830 f831 f832 f833 f834 f835 f836 f837 f838 f839 f840 f841 f842 f843 f844 f845 f846 f847 f848 f849 f850 f851 f852 f853 f854 f855 f856 f857 f858 f859 f860 f861 f862 f863 f864 f865 f866 f867 f868 f869 f870 f871 f872 f873 f874 f875 f876 f877 f878 f879 f880 f881 f882 f883 f884 f885 f886 f887 f888 f889 f890 f891 f892 f893 f894 f895 f896 f897 f898 f899 f900 f901 f902 f903 f904 f905 f906 f907 f908 f909 f910 f911 f912 f913 f914 f915 f916 f917 f918 f919 f920 f921 f922 f923 f924 f925 f926 f927 f928 f929 f930 f931 f932 f933 f934 f935 f936 f937 f938 f939 f940 f941 f942 f943 f944 f945 f946 f947 f948 f949 f950 f951 f952 f953 f954 f955 f956 f957 f958 f959 f960 f961 f962 f963 f964 f965 f966 f967 f968 f969 f970 f971 f972 f973 f974 f975 f976 f977 f978 f979 f980 f981 f982 f983 f984 f985 f986 f987 f988 f989 f990 f991 f992 f993 f994 f995 f996 f997 f998 f999 f1000 f1001 f1002 f1003 f1004 f1005 f1006 f1007 f1008 f1009 f1010 f1011 f1012 f1013 f1014 f1015 f1016 f1017 f1018 f1019 f1020 f1021 f1022 f1023 f1024 f1025 f1026 f1027 f1028 f1029 f1030 f1031 f1032 f1033 f1034 f1035 f1036 f1037 f1038 f1039 f1040 f1041 f1042 f1043 f1044 f1045 f1046 f1047 f1048 f1049 f1050 f1051 f1052 f1053 f1054 f1055 f1056 f1057 f1058 f1059 f1060 f1061 f1062 f1063 f1064 f1065 f1066 f1067 f1068 f1069 f1070 f1071 f1072 f1073 f1074 f1075 f1076 f1077 f1078 f1079 f1080 f1081 f1082 f1083 f1084 f1085))