(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# b a b -> b# a b a a b b, b# b a b -> b# a a b b, b# b a b -> b# b, b# b a b -> b#, b# a b -> b# a a b, b# a b -> b#, b# a a b a b -> b# b, b# a a b a b -> b#, b b ->= b a b, b b a b ->= b a b a a b b, b a b ->= b a a b, b a a b 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 (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f97 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f98 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f99 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f100 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f101 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f102 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f103 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f104 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f105 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f106 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f107 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f108 () Arctic (+ f33 f105)) (define-fun f109 () Arctic (+ f34 f106)) (define-fun f110 () Arctic (+ f35 f107)) (define-fun f111 () Arctic (+ (* f12 f96) (* f13 f99) (* f14 f102))) (define-fun f112 () Arctic (+ (* f12 f97) (* f13 f100) (* f14 f103))) (define-fun f113 () Arctic (+ (* f12 f98) (* f13 f101) (* f14 f104))) (define-fun f114 () Arctic (+ (* f15 f96) (* f16 f99) (* f17 f102))) (define-fun f115 () Arctic (+ (* f15 f97) (* f16 f100) (* f17 f103))) (define-fun f116 () Arctic (+ (* f15 f98) (* f16 f101) (* f17 f104))) (define-fun f117 () Arctic (+ (* f18 f96) (* f19 f99) (* f20 f102))) (define-fun f118 () Arctic (+ (* f18 f97) (* f19 f100) (* f20 f103))) (define-fun f119 () Arctic (+ (* f18 f98) (* f19 f101) (* f20 f104))) (define-fun f120 () Arctic (+ (* f12 f108) (* f13 f109) (* f14 f110))) (define-fun f121 () Arctic (+ (* f15 f108) (* f16 f109) (* f17 f110))) (define-fun f122 () Arctic (+ (* f18 f108) (* f19 f109) (* f20 f110))) (define-fun f123 () Arctic (+ f21 f120)) (define-fun f124 () Arctic (+ f22 f121)) (define-fun f125 () Arctic (+ f23 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 (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f142 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f143 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f144 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f145 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f146 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f147 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f148 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f149 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f150 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f151 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f152 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f153 () Arctic (+ f21 f150)) (define-fun f154 () Arctic (+ f22 f151)) (define-fun f155 () Arctic (+ f23 f152)) (define-fun f156 () Arctic (+ (* f24 f141) (* f25 f144) (* f26 f147))) (define-fun f157 () Arctic (+ (* f24 f142) (* f25 f145) (* f26 f148))) (define-fun f158 () Arctic (+ (* f24 f143) (* f25 f146) (* f26 f149))) (define-fun f159 () Arctic (+ (* f27 f141) (* f28 f144) (* f29 f147))) (define-fun f160 () Arctic (+ (* f27 f142) (* f28 f145) (* f29 f148))) (define-fun f161 () Arctic (+ (* f27 f143) (* f28 f146) (* f29 f149))) (define-fun f162 () Arctic (+ (* f30 f141) (* f31 f144) (* f32 f147))) (define-fun f163 () Arctic (+ (* f30 f142) (* f31 f145) (* f32 f148))) (define-fun f164 () Arctic (+ (* f30 f143) (* f31 f146) (* f32 f149))) (define-fun f165 () Arctic (+ (* f24 f153) (* f25 f154) (* f26 f155))) (define-fun f166 () Arctic (+ (* f27 f153) (* f28 f154) (* f29 f155))) (define-fun f167 () Arctic (+ (* f30 f153) (* f31 f154) (* f32 f155))) (define-fun f168 () Arctic (+ f33 f165)) (define-fun f169 () Arctic (+ f34 f166)) (define-fun f170 () Arctic (+ f35 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 (+ (* f12 f171) (* f13 f174) (* f14 f177))) (define-fun f187 () Arctic (+ (* f12 f172) (* f13 f175) (* f14 f178))) (define-fun f188 () Arctic (+ (* f12 f173) (* f13 f176) (* f14 f179))) (define-fun f189 () Arctic (+ (* f15 f171) (* f16 f174) (* f17 f177))) (define-fun f190 () Arctic (+ (* f15 f172) (* f16 f175) (* f17 f178))) (define-fun f191 () Arctic (+ (* f15 f173) (* f16 f176) (* f17 f179))) (define-fun f192 () Arctic (+ (* f18 f171) (* f19 f174) (* f20 f177))) (define-fun f193 () Arctic (+ (* f18 f172) (* f19 f175) (* f20 f178))) (define-fun f194 () Arctic (+ (* f18 f173) (* f19 f176) (* f20 f179))) (define-fun f195 () Arctic (+ (* f12 f183) (* f13 f184) (* f14 f185))) (define-fun f196 () Arctic (+ (* f15 f183) (* f16 f184) (* f17 f185))) (define-fun f197 () Arctic (+ (* f18 f183) (* f19 f184) (* f20 f185))) (define-fun f198 () Arctic (+ f21 f195)) (define-fun f199 () Arctic (+ f22 f196)) (define-fun f200 () Arctic (+ f23 f197)) (define-fun f201 () Arctic (+ (* f24 f186) (* f25 f189) (* f26 f192))) (define-fun f202 () Arctic (+ (* f24 f187) (* f25 f190) (* f26 f193))) (define-fun f203 () Arctic (+ (* f24 f188) (* f25 f191) (* f26 f194))) (define-fun f204 () Arctic (+ (* f27 f186) (* f28 f189) (* f29 f192))) (define-fun f205 () Arctic (+ (* f27 f187) (* f28 f190) (* f29 f193))) (define-fun f206 () Arctic (+ (* f27 f188) (* f28 f191) (* f29 f194))) (define-fun f207 () Arctic (+ (* f30 f186) (* f31 f189) (* f32 f192))) (define-fun f208 () Arctic (+ (* f30 f187) (* f31 f190) (* f32 f193))) (define-fun f209 () Arctic (+ (* f30 f188) (* f31 f191) (* f32 f194))) (define-fun f210 () Arctic (+ (* f24 f198) (* f25 f199) (* f26 f200))) (define-fun f211 () Arctic (+ (* f27 f198) (* f28 f199) (* f29 f200))) (define-fun f212 () Arctic (+ (* f30 f198) (* f31 f199) (* f32 f200))) (define-fun f213 () Arctic (+ f33 f210)) (define-fun f214 () Arctic (+ f34 f211)) (define-fun f215 () Arctic (+ f35 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 (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f232 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f233 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f234 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f235 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f236 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f237 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f238 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f239 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f240 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f241 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f242 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f243 () Arctic (+ f33 f240)) (define-fun f244 () Arctic (+ f34 f241)) (define-fun f245 () Arctic (+ f35 f242)) (define-fun f246 () Arctic (+ (* f12 f231) (* f13 f234) (* f14 f237))) (define-fun f247 () Arctic (+ (* f12 f232) (* f13 f235) (* f14 f238))) (define-fun f248 () Arctic (+ (* f12 f233) (* f13 f236) (* f14 f239))) (define-fun f249 () Arctic (+ (* f15 f231) (* f16 f234) (* f17 f237))) (define-fun f250 () Arctic (+ (* f15 f232) (* f16 f235) (* f17 f238))) (define-fun f251 () Arctic (+ (* f15 f233) (* f16 f236) (* f17 f239))) (define-fun f252 () Arctic (+ (* f18 f231) (* f19 f234) (* f20 f237))) (define-fun f253 () Arctic (+ (* f18 f232) (* f19 f235) (* f20 f238))) (define-fun f254 () Arctic (+ (* f18 f233) (* f19 f236) (* f20 f239))) (define-fun f255 () Arctic (+ (* f12 f243) (* f13 f244) (* f14 f245))) (define-fun f256 () Arctic (+ (* f15 f243) (* f16 f244) (* f17 f245))) (define-fun f257 () Arctic (+ (* f18 f243) (* f19 f244) (* f20 f245))) (define-fun f258 () Arctic (+ f21 f255)) (define-fun f259 () Arctic (+ f22 f256)) (define-fun f260 () Arctic (+ f23 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 (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f277 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f278 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f279 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f280 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f281 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f282 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f283 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f284 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f285 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f286 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f287 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f288 () Arctic (+ f21 f285)) (define-fun f289 () Arctic (+ f22 f286)) (define-fun f290 () Arctic (+ f23 f287)) (define-fun f291 () Arctic (+ (* f24 f276) (* f25 f279) (* f26 f282))) (define-fun f292 () Arctic (+ (* f24 f277) (* f25 f280) (* f26 f283))) (define-fun f293 () Arctic (+ (* f24 f278) (* f25 f281) (* f26 f284))) (define-fun f294 () Arctic (+ (* f27 f276) (* f28 f279) (* f29 f282))) (define-fun f295 () Arctic (+ (* f27 f277) (* f28 f280) (* f29 f283))) (define-fun f296 () Arctic (+ (* f27 f278) (* f28 f281) (* f29 f284))) (define-fun f297 () Arctic (+ (* f30 f276) (* f31 f279) (* f32 f282))) (define-fun f298 () Arctic (+ (* f30 f277) (* f31 f280) (* f32 f283))) (define-fun f299 () Arctic (+ (* f30 f278) (* f31 f281) (* f32 f284))) (define-fun f300 () Arctic (+ (* f24 f288) (* f25 f289) (* f26 f290))) (define-fun f301 () Arctic (+ (* f27 f288) (* f28 f289) (* f29 f290))) (define-fun f302 () Arctic (+ (* f30 f288) (* f31 f289) (* f32 f290))) (define-fun f303 () Arctic (+ f33 f300)) (define-fun f304 () Arctic (+ f34 f301)) (define-fun f305 () Arctic (+ f35 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 (+ (* f0 f306) (* f1 f309) (* f2 f312))) (define-fun f322 () Arctic (+ (* f0 f307) (* f1 f310) (* f2 f313))) (define-fun f323 () Arctic (+ (* f0 f308) (* f1 f311) (* f2 f314))) (define-fun f324 () Arctic (+ (* f3 f306) (* f4 f309) (* f5 f312))) (define-fun f325 () Arctic (+ (* f3 f307) (* f4 f310) (* f5 f313))) (define-fun f326 () Arctic (+ (* f3 f308) (* f4 f311) (* f5 f314))) (define-fun f327 () Arctic (+ (* f6 f306) (* f7 f309) (* f8 f312))) (define-fun f328 () Arctic (+ (* f6 f307) (* f7 f310) (* f8 f313))) (define-fun f329 () Arctic (+ (* f6 f308) (* f7 f311) (* f8 f314))) (define-fun f330 () Arctic (+ (* f0 f318) (* f1 f319) (* f2 f320))) (define-fun f331 () Arctic (+ (* f3 f318) (* f4 f319) (* f5 f320))) (define-fun f332 () Arctic (+ (* f6 f318) (* f7 f319) (* f8 f320))) (define-fun f333 () Arctic (+ f9 f330)) (define-fun f334 () Arctic (+ f10 f331)) (define-fun f335 () Arctic (+ f11 f332)) (define-fun f336 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f337 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f338 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f339 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f340 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f341 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f342 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f343 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f344 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f345 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f346 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f347 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f348 () Arctic (+ f33 f345)) (define-fun f349 () Arctic (+ f34 f346)) (define-fun f350 () Arctic (+ f35 f347)) (define-fun f351 () Arctic (+ (* f12 f336) (* f13 f339) (* f14 f342))) (define-fun f352 () Arctic (+ (* f12 f337) (* f13 f340) (* f14 f343))) (define-fun f353 () Arctic (+ (* f12 f338) (* f13 f341) (* f14 f344))) (define-fun f354 () Arctic (+ (* f15 f336) (* f16 f339) (* f17 f342))) (define-fun f355 () Arctic (+ (* f15 f337) (* f16 f340) (* f17 f343))) (define-fun f356 () Arctic (+ (* f15 f338) (* f16 f341) (* f17 f344))) (define-fun f357 () Arctic (+ (* f18 f336) (* f19 f339) (* f20 f342))) (define-fun f358 () Arctic (+ (* f18 f337) (* f19 f340) (* f20 f343))) (define-fun f359 () Arctic (+ (* f18 f338) (* f19 f341) (* f20 f344))) (define-fun f360 () Arctic (+ (* f12 f348) (* f13 f349) (* f14 f350))) (define-fun f361 () Arctic (+ (* f15 f348) (* f16 f349) (* f17 f350))) (define-fun f362 () Arctic (+ (* f18 f348) (* f19 f349) (* f20 f350))) (define-fun f363 () Arctic (+ f21 f360)) (define-fun f364 () Arctic (+ f22 f361)) (define-fun f365 () Arctic (+ f23 f362)) (define-fun f366 () Arctic (+ (* f0 f351) (* f1 f354) (* f2 f357))) (define-fun f367 () Arctic (+ (* f0 f352) (* f1 f355) (* f2 f358))) (define-fun f368 () Arctic (+ (* f0 f353) (* f1 f356) (* f2 f359))) (define-fun f369 () Arctic (+ (* f3 f351) (* f4 f354) (* f5 f357))) (define-fun f370 () Arctic (+ (* f3 f352) (* f4 f355) (* f5 f358))) (define-fun f371 () Arctic (+ (* f3 f353) (* f4 f356) (* f5 f359))) (define-fun f372 () Arctic (+ (* f6 f351) (* f7 f354) (* f8 f357))) (define-fun f373 () Arctic (+ (* f6 f352) (* f7 f355) (* f8 f358))) (define-fun f374 () Arctic (+ (* f6 f353) (* f7 f356) (* f8 f359))) (define-fun f375 () Arctic (+ (* f0 f363) (* f1 f364) (* f2 f365))) (define-fun f376 () Arctic (+ (* f3 f363) (* f4 f364) (* f5 f365))) (define-fun f377 () Arctic (+ (* f6 f363) (* f7 f364) (* f8 f365))) (define-fun f378 () Arctic (+ f9 f375)) (define-fun f379 () Arctic (+ f10 f376)) (define-fun f380 () Arctic (+ f11 f377)) (define-fun f381 () Arctic (+ (* f0 f12) (* f1 f15) (* f2 f18))) (define-fun f382 () Arctic (+ (* f0 f13) (* f1 f16) (* f2 f19))) (define-fun f383 () Arctic (+ (* f0 f14) (* f1 f17) (* f2 f20))) (define-fun f384 () Arctic (+ (* f3 f12) (* f4 f15) (* f5 f18))) (define-fun f385 () Arctic (+ (* f3 f13) (* f4 f16) (* f5 f19))) (define-fun f386 () Arctic (+ (* f3 f14) (* f4 f17) (* f5 f20))) (define-fun f387 () Arctic (+ (* f6 f12) (* f7 f15) (* f8 f18))) (define-fun f388 () Arctic (+ (* f6 f13) (* f7 f16) (* f8 f19))) (define-fun f389 () Arctic (+ (* f6 f14) (* f7 f17) (* f8 f20))) (define-fun f390 () Arctic (+ (* f0 f21) (* f1 f22) (* f2 f23))) (define-fun f391 () Arctic (+ (* f3 f21) (* f4 f22) (* f5 f23))) (define-fun f392 () Arctic (+ (* f6 f21) (* f7 f22) (* f8 f23))) (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 (+ (* f12 f396) (* f13 f399) (* f14 f402))) (define-fun f412 () Arctic (+ (* f12 f397) (* f13 f400) (* f14 f403))) (define-fun f413 () Arctic (+ (* f12 f398) (* f13 f401) (* f14 f404))) (define-fun f414 () Arctic (+ (* f15 f396) (* f16 f399) (* f17 f402))) (define-fun f415 () Arctic (+ (* f15 f397) (* f16 f400) (* f17 f403))) (define-fun f416 () Arctic (+ (* f15 f398) (* f16 f401) (* f17 f404))) (define-fun f417 () Arctic (+ (* f18 f396) (* f19 f399) (* f20 f402))) (define-fun f418 () Arctic (+ (* f18 f397) (* f19 f400) (* f20 f403))) (define-fun f419 () Arctic (+ (* f18 f398) (* f19 f401) (* f20 f404))) (define-fun f420 () Arctic (+ (* f12 f408) (* f13 f409) (* f14 f410))) (define-fun f421 () Arctic (+ (* f15 f408) (* f16 f409) (* f17 f410))) (define-fun f422 () Arctic (+ (* f18 f408) (* f19 f409) (* f20 f410))) (define-fun f423 () Arctic (+ f21 f420)) (define-fun f424 () Arctic (+ f22 f421)) (define-fun f425 () Arctic (+ f23 f422)) (define-fun f426 () Arctic (+ (* f0 f411) (* f1 f414) (* f2 f417))) (define-fun f427 () Arctic (+ (* f0 f412) (* f1 f415) (* f2 f418))) (define-fun f428 () Arctic (+ (* f0 f413) (* f1 f416) (* f2 f419))) (define-fun f429 () Arctic (+ (* f3 f411) (* f4 f414) (* f5 f417))) (define-fun f430 () Arctic (+ (* f3 f412) (* f4 f415) (* f5 f418))) (define-fun f431 () Arctic (+ (* f3 f413) (* f4 f416) (* f5 f419))) (define-fun f432 () Arctic (+ (* f6 f411) (* f7 f414) (* f8 f417))) (define-fun f433 () Arctic (+ (* f6 f412) (* f7 f415) (* f8 f418))) (define-fun f434 () Arctic (+ (* f6 f413) (* f7 f416) (* f8 f419))) (define-fun f435 () Arctic (+ (* f0 f423) (* f1 f424) (* f2 f425))) (define-fun f436 () Arctic (+ (* f3 f423) (* f4 f424) (* f5 f425))) (define-fun f437 () Arctic (+ (* f6 f423) (* f7 f424) (* f8 f425))) (define-fun f438 () Arctic (+ f9 f435)) (define-fun f439 () Arctic (+ f10 f436)) (define-fun f440 () Arctic (+ f11 f437)) (define-fun f441 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f442 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f443 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f444 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f445 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f446 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f447 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f448 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f449 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f450 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f451 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f452 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (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 (+ (* f24 f471) (* f25 f474) (* f26 f477))) (define-fun f487 () Arctic (+ (* f24 f472) (* f25 f475) (* f26 f478))) (define-fun f488 () Arctic (+ (* f24 f473) (* f25 f476) (* f26 f479))) (define-fun f489 () Arctic (+ (* f27 f471) (* f28 f474) (* f29 f477))) (define-fun f490 () Arctic (+ (* f27 f472) (* f28 f475) (* f29 f478))) (define-fun f491 () Arctic (+ (* f27 f473) (* f28 f476) (* f29 f479))) (define-fun f492 () Arctic (+ (* f30 f471) (* f31 f474) (* f32 f477))) (define-fun f493 () Arctic (+ (* f30 f472) (* f31 f475) (* f32 f478))) (define-fun f494 () Arctic (+ (* f30 f473) (* f31 f476) (* f32 f479))) (define-fun f495 () Arctic (+ (* f24 f483) (* f25 f484) (* f26 f485))) (define-fun f496 () Arctic (+ (* f27 f483) (* f28 f484) (* f29 f485))) (define-fun f497 () Arctic (+ (* f30 f483) (* f31 f484) (* f32 f485))) (define-fun f498 () Arctic (+ f33 f495)) (define-fun f499 () Arctic (+ f34 f496)) (define-fun f500 () Arctic (+ f35 f497)) (define-fun f501 () Arctic (+ (* f0 f486) (* f1 f489) (* f2 f492))) (define-fun f502 () Arctic (+ (* f0 f487) (* f1 f490) (* f2 f493))) (define-fun f503 () Arctic (+ (* f0 f488) (* f1 f491) (* f2 f494))) (define-fun f504 () Arctic (+ (* f3 f486) (* f4 f489) (* f5 f492))) (define-fun f505 () Arctic (+ (* f3 f487) (* f4 f490) (* f5 f493))) (define-fun f506 () Arctic (+ (* f3 f488) (* f4 f491) (* f5 f494))) (define-fun f507 () Arctic (+ (* f6 f486) (* f7 f489) (* f8 f492))) (define-fun f508 () Arctic (+ (* f6 f487) (* f7 f490) (* f8 f493))) (define-fun f509 () Arctic (+ (* f6 f488) (* f7 f491) (* f8 f494))) (define-fun f510 () Arctic (+ (* f0 f498) (* f1 f499) (* f2 f500))) (define-fun f511 () Arctic (+ (* f3 f498) (* f4 f499) (* f5 f500))) (define-fun f512 () Arctic (+ (* f6 f498) (* f7 f499) (* f8 f500))) (define-fun f513 () Arctic (+ f9 f510)) (define-fun f514 () Arctic (+ f10 f511)) (define-fun f515 () Arctic (+ f11 f512)) (define-fun f516 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f517 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f518 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f519 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f520 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f521 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f522 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f523 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f524 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f525 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f526 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f527 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (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 (+ (* f12 f546) (* f13 f549) (* f14 f552))) (define-fun f562 () Arctic (+ (* f12 f547) (* f13 f550) (* f14 f553))) (define-fun f563 () Arctic (+ (* f12 f548) (* f13 f551) (* f14 f554))) (define-fun f564 () Arctic (+ (* f15 f546) (* f16 f549) (* f17 f552))) (define-fun f565 () Arctic (+ (* f15 f547) (* f16 f550) (* f17 f553))) (define-fun f566 () Arctic (+ (* f15 f548) (* f16 f551) (* f17 f554))) (define-fun f567 () Arctic (+ (* f18 f546) (* f19 f549) (* f20 f552))) (define-fun f568 () Arctic (+ (* f18 f547) (* f19 f550) (* f20 f553))) (define-fun f569 () Arctic (+ (* f18 f548) (* f19 f551) (* f20 f554))) (define-fun f570 () Arctic (+ (* f12 f558) (* f13 f559) (* f14 f560))) (define-fun f571 () Arctic (+ (* f15 f558) (* f16 f559) (* f17 f560))) (define-fun f572 () Arctic (+ (* f18 f558) (* f19 f559) (* f20 f560))) (define-fun f573 () Arctic (+ f21 f570)) (define-fun f574 () Arctic (+ f22 f571)) (define-fun f575 () Arctic (+ f23 f572)) (define-fun f576 () Arctic (+ (* f24 f561) (* f25 f564) (* f26 f567))) (define-fun f577 () Arctic (+ (* f24 f562) (* f25 f565) (* f26 f568))) (define-fun f578 () Arctic (+ (* f24 f563) (* f25 f566) (* f26 f569))) (define-fun f579 () Arctic (+ (* f27 f561) (* f28 f564) (* f29 f567))) (define-fun f580 () Arctic (+ (* f27 f562) (* f28 f565) (* f29 f568))) (define-fun f581 () Arctic (+ (* f27 f563) (* f28 f566) (* f29 f569))) (define-fun f582 () Arctic (+ (* f30 f561) (* f31 f564) (* f32 f567))) (define-fun f583 () Arctic (+ (* f30 f562) (* f31 f565) (* f32 f568))) (define-fun f584 () Arctic (+ (* f30 f563) (* f31 f566) (* f32 f569))) (define-fun f585 () Arctic (+ (* f24 f573) (* f25 f574) (* f26 f575))) (define-fun f586 () Arctic (+ (* f27 f573) (* f28 f574) (* f29 f575))) (define-fun f587 () Arctic (+ (* f30 f573) (* f31 f574) (* f32 f575))) (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 (+ (* f0 f591) (* f1 f594) (* f2 f597))) (define-fun f607 () Arctic (+ (* f0 f592) (* f1 f595) (* f2 f598))) (define-fun f608 () Arctic (+ (* f0 f593) (* f1 f596) (* f2 f599))) (define-fun f609 () Arctic (+ (* f3 f591) (* f4 f594) (* f5 f597))) (define-fun f610 () Arctic (+ (* f3 f592) (* f4 f595) (* f5 f598))) (define-fun f611 () Arctic (+ (* f3 f593) (* f4 f596) (* f5 f599))) (define-fun f612 () Arctic (+ (* f6 f591) (* f7 f594) (* f8 f597))) (define-fun f613 () Arctic (+ (* f6 f592) (* f7 f595) (* f8 f598))) (define-fun f614 () Arctic (+ (* f6 f593) (* f7 f596) (* f8 f599))) (define-fun f615 () Arctic (+ (* f0 f603) (* f1 f604) (* f2 f605))) (define-fun f616 () Arctic (+ (* f3 f603) (* f4 f604) (* f5 f605))) (define-fun f617 () Arctic (+ (* f6 f603) (* f7 f604) (* f8 f605))) (define-fun f618 () Arctic (+ f9 f615)) (define-fun f619 () Arctic (+ f10 f616)) (define-fun f620 () Arctic (+ f11 f617)) (define-fun f621 () Arctic (+ (* f0 f12) (* f1 f15) (* f2 f18))) (define-fun f622 () Arctic (+ (* f0 f13) (* f1 f16) (* f2 f19))) (define-fun f623 () Arctic (+ (* f0 f14) (* f1 f17) (* f2 f20))) (define-fun f624 () Arctic (+ (* f3 f12) (* f4 f15) (* f5 f18))) (define-fun f625 () Arctic (+ (* f3 f13) (* f4 f16) (* f5 f19))) (define-fun f626 () Arctic (+ (* f3 f14) (* f4 f17) (* f5 f20))) (define-fun f627 () Arctic (+ (* f6 f12) (* f7 f15) (* f8 f18))) (define-fun f628 () Arctic (+ (* f6 f13) (* f7 f16) (* f8 f19))) (define-fun f629 () Arctic (+ (* f6 f14) (* f7 f17) (* f8 f20))) (define-fun f630 () Arctic (+ (* f0 f21) (* f1 f22) (* f2 f23))) (define-fun f631 () Arctic (+ (* f3 f21) (* f4 f22) (* f5 f23))) (define-fun f632 () Arctic (+ (* f6 f21) (* f7 f22) (* f8 f23))) (define-fun f633 () Arctic (+ f9 f630)) (define-fun f634 () Arctic (+ f10 f631)) (define-fun f635 () Arctic (+ f11 f632)) (define-fun f636 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f637 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f638 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f639 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f640 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f641 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f642 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f643 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f644 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f645 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f646 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f647 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f648 () Arctic (+ f33 f645)) (define-fun f649 () Arctic (+ f34 f646)) (define-fun f650 () Arctic (+ f35 f647)) (define-fun f651 () Arctic (+ (* f12 f636) (* f13 f639) (* f14 f642))) (define-fun f652 () Arctic (+ (* f12 f637) (* f13 f640) (* f14 f643))) (define-fun f653 () Arctic (+ (* f12 f638) (* f13 f641) (* f14 f644))) (define-fun f654 () Arctic (+ (* f15 f636) (* f16 f639) (* f17 f642))) (define-fun f655 () Arctic (+ (* f15 f637) (* f16 f640) (* f17 f643))) (define-fun f656 () Arctic (+ (* f15 f638) (* f16 f641) (* f17 f644))) (define-fun f657 () Arctic (+ (* f18 f636) (* f19 f639) (* f20 f642))) (define-fun f658 () Arctic (+ (* f18 f637) (* f19 f640) (* f20 f643))) (define-fun f659 () Arctic (+ (* f18 f638) (* f19 f641) (* f20 f644))) (define-fun f660 () Arctic (+ (* f12 f648) (* f13 f649) (* f14 f650))) (define-fun f661 () Arctic (+ (* f15 f648) (* f16 f649) (* f17 f650))) (define-fun f662 () Arctic (+ (* f18 f648) (* f19 f649) (* f20 f650))) (define-fun f663 () Arctic (+ f21 f660)) (define-fun f664 () Arctic (+ f22 f661)) (define-fun f665 () Arctic (+ f23 f662)) (define-fun f666 () Arctic (+ (* f24 f651) (* f25 f654) (* f26 f657))) (define-fun f667 () Arctic (+ (* f24 f652) (* f25 f655) (* f26 f658))) (define-fun f668 () Arctic (+ (* f24 f653) (* f25 f656) (* f26 f659))) (define-fun f669 () Arctic (+ (* f27 f651) (* f28 f654) (* f29 f657))) (define-fun f670 () Arctic (+ (* f27 f652) (* f28 f655) (* f29 f658))) (define-fun f671 () Arctic (+ (* f27 f653) (* f28 f656) (* f29 f659))) (define-fun f672 () Arctic (+ (* f30 f651) (* f31 f654) (* f32 f657))) (define-fun f673 () Arctic (+ (* f30 f652) (* f31 f655) (* f32 f658))) (define-fun f674 () Arctic (+ (* f30 f653) (* f31 f656) (* f32 f659))) (define-fun f675 () Arctic (+ (* f24 f663) (* f25 f664) (* f26 f665))) (define-fun f676 () Arctic (+ (* f27 f663) (* f28 f664) (* f29 f665))) (define-fun f677 () Arctic (+ (* f30 f663) (* f31 f664) (* f32 f665))) (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 (+ (* f0 f681) (* f1 f684) (* f2 f687))) (define-fun f697 () Arctic (+ (* f0 f682) (* f1 f685) (* f2 f688))) (define-fun f698 () Arctic (+ (* f0 f683) (* f1 f686) (* f2 f689))) (define-fun f699 () Arctic (+ (* f3 f681) (* f4 f684) (* f5 f687))) (define-fun f700 () Arctic (+ (* f3 f682) (* f4 f685) (* f5 f688))) (define-fun f701 () Arctic (+ (* f3 f683) (* f4 f686) (* f5 f689))) (define-fun f702 () Arctic (+ (* f6 f681) (* f7 f684) (* f8 f687))) (define-fun f703 () Arctic (+ (* f6 f682) (* f7 f685) (* f8 f688))) (define-fun f704 () Arctic (+ (* f6 f683) (* f7 f686) (* f8 f689))) (define-fun f705 () Arctic (+ (* f0 f693) (* f1 f694) (* f2 f695))) (define-fun f706 () Arctic (+ (* f3 f693) (* f4 f694) (* f5 f695))) (define-fun f707 () Arctic (+ (* f6 f693) (* f7 f694) (* f8 f695))) (define-fun f708 () Arctic (+ f9 f705)) (define-fun f709 () Arctic (+ f10 f706)) (define-fun f710 () Arctic (+ f11 f707)) (define-fun f711 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f712 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f713 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f714 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f715 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f716 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f717 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f718 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f719 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f720 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f721 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f722 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f723 () Arctic (+ f21 f720)) (define-fun f724 () Arctic (+ f22 f721)) (define-fun f725 () Arctic (+ f23 f722)) (define-fun f726 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f727 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f728 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f729 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f730 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f731 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f732 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f733 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f734 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f735 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f736 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f737 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f738 () Arctic (+ f33 f735)) (define-fun f739 () Arctic (+ f34 f736)) (define-fun f740 () Arctic (+ f35 f737)) (define-fun f741 () Arctic (+ (* f12 f726) (* f13 f729) (* f14 f732))) (define-fun f742 () Arctic (+ (* f12 f727) (* f13 f730) (* f14 f733))) (define-fun f743 () Arctic (+ (* f12 f728) (* f13 f731) (* f14 f734))) (define-fun f744 () Arctic (+ (* f15 f726) (* f16 f729) (* f17 f732))) (define-fun f745 () Arctic (+ (* f15 f727) (* f16 f730) (* f17 f733))) (define-fun f746 () Arctic (+ (* f15 f728) (* f16 f731) (* f17 f734))) (define-fun f747 () Arctic (+ (* f18 f726) (* f19 f729) (* f20 f732))) (define-fun f748 () Arctic (+ (* f18 f727) (* f19 f730) (* f20 f733))) (define-fun f749 () Arctic (+ (* f18 f728) (* f19 f731) (* f20 f734))) (define-fun f750 () Arctic (+ (* f12 f738) (* f13 f739) (* f14 f740))) (define-fun f751 () Arctic (+ (* f15 f738) (* f16 f739) (* f17 f740))) (define-fun f752 () Arctic (+ (* f18 f738) (* f19 f739) (* f20 f740))) (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 f771) (* f13 f774) (* f14 f777))) (define-fun f787 () Arctic (+ (* f12 f772) (* f13 f775) (* f14 f778))) (define-fun f788 () Arctic (+ (* f12 f773) (* f13 f776) (* f14 f779))) (define-fun f789 () Arctic (+ (* f15 f771) (* f16 f774) (* f17 f777))) (define-fun f790 () Arctic (+ (* f15 f772) (* f16 f775) (* f17 f778))) (define-fun f791 () Arctic (+ (* f15 f773) (* f16 f776) (* f17 f779))) (define-fun f792 () Arctic (+ (* f18 f771) (* f19 f774) (* f20 f777))) (define-fun f793 () Arctic (+ (* f18 f772) (* f19 f775) (* f20 f778))) (define-fun f794 () Arctic (+ (* f18 f773) (* f19 f776) (* f20 f779))) (define-fun f795 () Arctic (+ (* f12 f783) (* f13 f784) (* f14 f785))) (define-fun f796 () Arctic (+ (* f15 f783) (* f16 f784) (* f17 f785))) (define-fun f797 () Arctic (+ (* f18 f783) (* f19 f784) (* f20 f785))) (define-fun f798 () Arctic (+ f21 f795)) (define-fun f799 () Arctic (+ f22 f796)) (define-fun f800 () Arctic (+ f23 f797)) (define-fun f801 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f802 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f803 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f804 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f805 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f806 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f807 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f808 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f809 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f810 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f811 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f812 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f813 () Arctic (+ f21 f810)) (define-fun f814 () Arctic (+ f22 f811)) (define-fun f815 () Arctic (+ f23 f812)) (define-fun f816 () Arctic (+ (* f24 f801) (* f25 f804) (* f26 f807))) (define-fun f817 () Arctic (+ (* f24 f802) (* f25 f805) (* f26 f808))) (define-fun f818 () Arctic (+ (* f24 f803) (* f25 f806) (* f26 f809))) (define-fun f819 () Arctic (+ (* f27 f801) (* f28 f804) (* f29 f807))) (define-fun f820 () Arctic (+ (* f27 f802) (* f28 f805) (* f29 f808))) (define-fun f821 () Arctic (+ (* f27 f803) (* f28 f806) (* f29 f809))) (define-fun f822 () Arctic (+ (* f30 f801) (* f31 f804) (* f32 f807))) (define-fun f823 () Arctic (+ (* f30 f802) (* f31 f805) (* f32 f808))) (define-fun f824 () Arctic (+ (* f30 f803) (* f31 f806) (* f32 f809))) (define-fun f825 () Arctic (+ (* f24 f813) (* f25 f814) (* f26 f815))) (define-fun f826 () Arctic (+ (* f27 f813) (* f28 f814) (* f29 f815))) (define-fun f827 () Arctic (+ (* f30 f813) (* f31 f814) (* f32 f815))) (define-fun f828 () Arctic (+ f33 f825)) (define-fun f829 () Arctic (+ f34 f826)) (define-fun f830 () Arctic (+ f35 f827)) (define-fun f831 () Arctic (+ (* f24 f816) (* f25 f819) (* f26 f822))) (define-fun f832 () Arctic (+ (* f24 f817) (* f25 f820) (* f26 f823))) (define-fun f833 () Arctic (+ (* f24 f818) (* f25 f821) (* f26 f824))) (define-fun f834 () Arctic (+ (* f27 f816) (* f28 f819) (* f29 f822))) (define-fun f835 () Arctic (+ (* f27 f817) (* f28 f820) (* f29 f823))) (define-fun f836 () Arctic (+ (* f27 f818) (* f28 f821) (* f29 f824))) (define-fun f837 () Arctic (+ (* f30 f816) (* f31 f819) (* f32 f822))) (define-fun f838 () Arctic (+ (* f30 f817) (* f31 f820) (* f32 f823))) (define-fun f839 () Arctic (+ (* f30 f818) (* f31 f821) (* f32 f824))) (define-fun f840 () Arctic (+ (* f24 f828) (* f25 f829) (* f26 f830))) (define-fun f841 () Arctic (+ (* f27 f828) (* f28 f829) (* f29 f830))) (define-fun f842 () Arctic (+ (* f30 f828) (* f31 f829) (* f32 f830))) (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 (+ (* f12 f861) (* f13 f864) (* f14 f867))) (define-fun f877 () Arctic (+ (* f12 f862) (* f13 f865) (* f14 f868))) (define-fun f878 () Arctic (+ (* f12 f863) (* f13 f866) (* f14 f869))) (define-fun f879 () Arctic (+ (* f15 f861) (* f16 f864) (* f17 f867))) (define-fun f880 () Arctic (+ (* f15 f862) (* f16 f865) (* f17 f868))) (define-fun f881 () Arctic (+ (* f15 f863) (* f16 f866) (* f17 f869))) (define-fun f882 () Arctic (+ (* f18 f861) (* f19 f864) (* f20 f867))) (define-fun f883 () Arctic (+ (* f18 f862) (* f19 f865) (* f20 f868))) (define-fun f884 () Arctic (+ (* f18 f863) (* f19 f866) (* f20 f869))) (define-fun f885 () Arctic (+ (* f12 f873) (* f13 f874) (* f14 f875))) (define-fun f886 () Arctic (+ (* f15 f873) (* f16 f874) (* f17 f875))) (define-fun f887 () Arctic (+ (* f18 f873) (* f19 f874) (* f20 f875))) (define-fun f888 () Arctic (+ f21 f885)) (define-fun f889 () Arctic (+ f22 f886)) (define-fun f890 () Arctic (+ f23 f887)) (define-fun f891 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f892 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f893 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f894 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f895 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f896 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f897 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f898 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f899 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f900 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f901 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f902 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f903 () Arctic (+ f33 f900)) (define-fun f904 () Arctic (+ f34 f901)) (define-fun f905 () Arctic (+ f35 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 (+ (* f24 f921) (* f25 f924) (* f26 f927))) (define-fun f937 () Arctic (+ (* f24 f922) (* f25 f925) (* f26 f928))) (define-fun f938 () Arctic (+ (* f24 f923) (* f25 f926) (* f26 f929))) (define-fun f939 () Arctic (+ (* f27 f921) (* f28 f924) (* f29 f927))) (define-fun f940 () Arctic (+ (* f27 f922) (* f28 f925) (* f29 f928))) (define-fun f941 () Arctic (+ (* f27 f923) (* f28 f926) (* f29 f929))) (define-fun f942 () Arctic (+ (* f30 f921) (* f31 f924) (* f32 f927))) (define-fun f943 () Arctic (+ (* f30 f922) (* f31 f925) (* f32 f928))) (define-fun f944 () Arctic (+ (* f30 f923) (* f31 f926) (* f32 f929))) (define-fun f945 () Arctic (+ (* f24 f933) (* f25 f934) (* f26 f935))) (define-fun f946 () Arctic (+ (* f27 f933) (* f28 f934) (* f29 f935))) (define-fun f947 () Arctic (+ (* f30 f933) (* f31 f934) (* f32 f935))) (define-fun f948 () Arctic (+ f33 f945)) (define-fun f949 () Arctic (+ f34 f946)) (define-fun f950 () Arctic (+ f35 f947)) (define-fun f951 () Arctic (+ (* f12 f936) (* f13 f939) (* f14 f942))) (define-fun f952 () Arctic (+ (* f12 f937) (* f13 f940) (* f14 f943))) (define-fun f953 () Arctic (+ (* f12 f938) (* f13 f941) (* f14 f944))) (define-fun f954 () Arctic (+ (* f15 f936) (* f16 f939) (* f17 f942))) (define-fun f955 () Arctic (+ (* f15 f937) (* f16 f940) (* f17 f943))) (define-fun f956 () Arctic (+ (* f15 f938) (* f16 f941) (* f17 f944))) (define-fun f957 () Arctic (+ (* f18 f936) (* f19 f939) (* f20 f942))) (define-fun f958 () Arctic (+ (* f18 f937) (* f19 f940) (* f20 f943))) (define-fun f959 () Arctic (+ (* f18 f938) (* f19 f941) (* f20 f944))) (define-fun f960 () Arctic (+ (* f12 f948) (* f13 f949) (* f14 f950))) (define-fun f961 () Arctic (+ (* f15 f948) (* f16 f949) (* f17 f950))) (define-fun f962 () Arctic (+ (* f18 f948) (* f19 f949) (* f20 f950))) (define-fun f963 () Arctic (+ f21 f960)) (define-fun f964 () Arctic (+ f22 f961)) (define-fun f965 () Arctic (+ f23 f962)) (define-fun f966 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f967 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f968 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f969 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f970 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f971 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f972 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f973 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f974 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f975 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f976 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f977 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (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 f981) (* f25 f984) (* f26 f987))) (define-fun f997 () Arctic (+ (* f24 f982) (* f25 f985) (* f26 f988))) (define-fun f998 () Arctic (+ (* f24 f983) (* f25 f986) (* f26 f989))) (define-fun f999 () Arctic (+ (* f27 f981) (* f28 f984) (* f29 f987))) (define-fun f1000 () Arctic (+ (* f27 f982) (* f28 f985) (* f29 f988))) (define-fun f1001 () Arctic (+ (* f27 f983) (* f28 f986) (* f29 f989))) (define-fun f1002 () Arctic (+ (* f30 f981) (* f31 f984) (* f32 f987))) (define-fun f1003 () Arctic (+ (* f30 f982) (* f31 f985) (* f32 f988))) (define-fun f1004 () Arctic (+ (* f30 f983) (* f31 f986) (* f32 f989))) (define-fun f1005 () Arctic (+ (* f24 f993) (* f25 f994) (* f26 f995))) (define-fun f1006 () Arctic (+ (* f27 f993) (* f28 f994) (* f29 f995))) (define-fun f1007 () Arctic (+ (* f30 f993) (* f31 f994) (* f32 f995))) (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 (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f1042 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f1043 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f1044 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f1045 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f1046 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f1047 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f1048 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f1049 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f1050 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f1051 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f1052 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f1053 () Arctic (+ f21 f1050)) (define-fun f1054 () Arctic (+ f22 f1051)) (define-fun f1055 () Arctic (+ f23 f1052)) (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 f321) (>= f262 f322) (>= f263 f323)) (and (>= f264 f324) (>= f265 f325) (>= f266 f326)) (and (>= f267 f327) (>= f268 f328) (>= f269 f329))) (and (and (>= f273 f333)) (and (>= f274 f334)) (and (>= f275 f335)))) (and (and (and (>= f366 f381) (>= f367 f382) (>= f368 f383)) (and (>= f369 f384) (>= f370 f385) (>= f371 f386)) (and (>= f372 f387) (>= f373 f388) (>= f374 f389))) (and (and (>= f378 f393)) (and (>= f379 f394)) (and (>= f380 f395)))) (and (and (and (>= f426 f0) (>= f427 f1) (>= f428 f2)) (and (>= f429 f3) (>= f430 f4) (>= f431 f5)) (and (>= f432 f6) (>= f433 f7) (>= f434 f8))) (and (and (>= f438 f9)) (and (>= f439 f10)) (and (>= f440 f11)))) (and (and (and (>= f456 f501) (>= f457 f502) (>= f458 f503)) (and (>= f459 f504) (>= f460 f505) (>= f461 f506)) (and (>= f462 f507) (>= f463 f508) (>= f464 f509))) (and (and (>= f468 f513)) (and (>= f469 f514)) (and (>= f470 f515)))) (and (and (and (>= f531 f0) (>= f532 f1) (>= f533 f2)) (and (>= f534 f3) (>= f535 f4) (>= f536 f5)) (and (>= f537 f6) (>= f538 f7) (>= f539 f8))) (and (and (>= f543 f9)) (and (>= f544 f10)) (and (>= f545 f11)))) (and (and (and (>= f606 f621) (>= f607 f622) (>= f608 f623)) (and (>= f609 f624) (>= f610 f625) (>= f611 f626)) (and (>= f612 f627) (>= f613 f628) (>= f614 f629))) (and (and (>= f618 f633)) (and (>= f619 f634)) (and (>= f620 f635)))) (and (and (and (>= f696 f0) (>= f697 f1) (>= f698 f2)) (and (>= f699 f3) (>= f700 f4) (>= f701 f5)) (and (>= f702 f6) (>= f703 f7) (>= f704 f8))) (and (and (>= f708 f9)) (and (>= f709 f10)) (and (>= f710 f11)))) (and (and (and (>= f711 f741) (>= f712 f742) (>= f713 f743)) (and (>= f714 f744) (>= f715 f745) (>= f716 f746)) (and (>= f717 f747) (>= f718 f748) (>= f719 f749))) (and (and (>= f723 f753)) (and (>= f724 f754)) (and (>= f725 f755)))) (and (and (and (>= f786 f876) (>= f787 f877) (>= f788 f878)) (and (>= f789 f879) (>= f790 f880) (>= f791 f881)) (and (>= f792 f882) (>= f793 f883) (>= f794 f884))) (and (and (>= f798 f888)) (and (>= f799 f889)) (and (>= f800 f890)))) (and (and (and (>= f906 f951) (>= f907 f952) (>= f908 f953)) (and (>= f909 f954) (>= f910 f955) (>= f911 f956)) (and (>= f912 f957) (>= f913 f958) (>= f914 f959))) (and (and (>= f918 f963)) (and (>= f919 f964)) (and (>= f920 f965)))) (and (and (and (>= f1026 f1041) (>= f1027 f1042) (>= f1028 f1043)) (and (>= f1029 f1044) (>= f1030 f1045) (>= f1031 f1046)) (and (>= f1032 f1047) (>= f1033 f1048) (>= f1034 f1049))) (and (and (>= f1038 f1053)) (and (>= f1039 f1054)) (and (>= f1040 f1055)))))) (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 f321) (>> f262 f322) (>> f263 f323)) (and (>> f264 f324) (>> f265 f325) (>> f266 f326)) (and (>> f267 f327) (>> f268 f328) (>> f269 f329))) (and (and (>> f273 f333)) (and (>> f274 f334)) (and (>> f275 f335)))) (and (and (and (>> f366 f381) (>> f367 f382) (>> f368 f383)) (and (>> f369 f384) (>> f370 f385) (>> f371 f386)) (and (>> f372 f387) (>> f373 f388) (>> f374 f389))) (and (and (>> f378 f393)) (and (>> f379 f394)) (and (>> f380 f395)))) (and (and (and (>> f426 f0) (>> f427 f1) (>> f428 f2)) (and (>> f429 f3) (>> f430 f4) (>> f431 f5)) (and (>> f432 f6) (>> f433 f7) (>> f434 f8))) (and (and (>> f438 f9)) (and (>> f439 f10)) (and (>> f440 f11)))) (and (and (and (>> f456 f501) (>> f457 f502) (>> f458 f503)) (and (>> f459 f504) (>> f460 f505) (>> f461 f506)) (and (>> f462 f507) (>> f463 f508) (>> f464 f509))) (and (and (>> f468 f513)) (and (>> f469 f514)) (and (>> f470 f515)))) (and (and (and (>> f531 f0) (>> f532 f1) (>> f533 f2)) (and (>> f534 f3) (>> f535 f4) (>> f536 f5)) (and (>> f537 f6) (>> f538 f7) (>> f539 f8))) (and (and (>> f543 f9)) (and (>> f544 f10)) (and (>> f545 f11)))) (and (and (and (>> f606 f621) (>> f607 f622) (>> f608 f623)) (and (>> f609 f624) (>> f610 f625) (>> f611 f626)) (and (>> f612 f627) (>> f613 f628) (>> f614 f629))) (and (and (>> f618 f633)) (and (>> f619 f634)) (and (>> f620 f635)))) (and (and (and (>> f696 f0) (>> f697 f1) (>> f698 f2)) (and (>> f699 f3) (>> f700 f4) (>> f701 f5)) (and (>> f702 f6) (>> f703 f7) (>> f704 f8))) (and (and (>> f708 f9)) (and (>> f709 f10)) (and (>> f710 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))