(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# a a b, b# a b -> b#, b# a b a a b -> 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 (+ (* 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 (+ (* f0 f231) (* f1 f234) (* f2 f237))) (define-fun f247 () Arctic (+ (* f0 f232) (* f1 f235) (* f2 f238))) (define-fun f248 () Arctic (+ (* f0 f233) (* f1 f236) (* f2 f239))) (define-fun f249 () Arctic (+ (* f3 f231) (* f4 f234) (* f5 f237))) (define-fun f250 () Arctic (+ (* f3 f232) (* f4 f235) (* f5 f238))) (define-fun f251 () Arctic (+ (* f3 f233) (* f4 f236) (* f5 f239))) (define-fun f252 () Arctic (+ (* f6 f231) (* f7 f234) (* f8 f237))) (define-fun f253 () Arctic (+ (* f6 f232) (* f7 f235) (* f8 f238))) (define-fun f254 () Arctic (+ (* f6 f233) (* f7 f236) (* f8 f239))) (define-fun f255 () Arctic (+ (* f0 f243) (* f1 f244) (* f2 f245))) (define-fun f256 () Arctic (+ (* f3 f243) (* f4 f244) (* f5 f245))) (define-fun f257 () Arctic (+ (* f6 f243) (* f7 f244) (* f8 f245))) (define-fun f258 () Arctic (+ f9 f255)) (define-fun f259 () Arctic (+ f10 f256)) (define-fun f260 () Arctic (+ f11 f257)) (define-fun f261 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f262 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f263 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f264 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f265 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f266 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f267 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f268 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f269 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f270 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f271 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f272 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f273 () Arctic (+ f33 f270)) (define-fun f274 () Arctic (+ f34 f271)) (define-fun f275 () Arctic (+ f35 f272)) (define-fun f276 () Arctic (+ (* f24 f261) (* f25 f264) (* f26 f267))) (define-fun f277 () Arctic (+ (* f24 f262) (* f25 f265) (* f26 f268))) (define-fun f278 () Arctic (+ (* f24 f263) (* f25 f266) (* f26 f269))) (define-fun f279 () Arctic (+ (* f27 f261) (* f28 f264) (* f29 f267))) (define-fun f280 () Arctic (+ (* f27 f262) (* f28 f265) (* f29 f268))) (define-fun f281 () Arctic (+ (* f27 f263) (* f28 f266) (* f29 f269))) (define-fun f282 () Arctic (+ (* f30 f261) (* f31 f264) (* f32 f267))) (define-fun f283 () Arctic (+ (* f30 f262) (* f31 f265) (* f32 f268))) (define-fun f284 () Arctic (+ (* f30 f263) (* f31 f266) (* f32 f269))) (define-fun f285 () Arctic (+ (* f24 f273) (* f25 f274) (* f26 f275))) (define-fun f286 () Arctic (+ (* f27 f273) (* f28 f274) (* f29 f275))) (define-fun f287 () Arctic (+ (* f30 f273) (* f31 f274) (* f32 f275))) (define-fun f288 () Arctic (+ f33 f285)) (define-fun f289 () Arctic (+ f34 f286)) (define-fun f290 () Arctic (+ f35 f287)) (define-fun f291 () Arctic (+ (* f0 f276) (* f1 f279) (* f2 f282))) (define-fun f292 () Arctic (+ (* f0 f277) (* f1 f280) (* f2 f283))) (define-fun f293 () Arctic (+ (* f0 f278) (* f1 f281) (* f2 f284))) (define-fun f294 () Arctic (+ (* f3 f276) (* f4 f279) (* f5 f282))) (define-fun f295 () Arctic (+ (* f3 f277) (* f4 f280) (* f5 f283))) (define-fun f296 () Arctic (+ (* f3 f278) (* f4 f281) (* f5 f284))) (define-fun f297 () Arctic (+ (* f6 f276) (* f7 f279) (* f8 f282))) (define-fun f298 () Arctic (+ (* f6 f277) (* f7 f280) (* f8 f283))) (define-fun f299 () Arctic (+ (* f6 f278) (* f7 f281) (* f8 f284))) (define-fun f300 () Arctic (+ (* f0 f288) (* f1 f289) (* f2 f290))) (define-fun f301 () Arctic (+ (* f3 f288) (* f4 f289) (* f5 f290))) (define-fun f302 () Arctic (+ (* f6 f288) (* f7 f289) (* f8 f290))) (define-fun f303 () Arctic (+ f9 f300)) (define-fun f304 () Arctic (+ f10 f301)) (define-fun f305 () Arctic (+ f11 f302)) (define-fun f306 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f307 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f308 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f309 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f310 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f311 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f312 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f313 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f314 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f315 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f316 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f317 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (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 (+ (* f24 f336) (* f25 f339) (* f26 f342))) (define-fun f352 () Arctic (+ (* f24 f337) (* f25 f340) (* f26 f343))) (define-fun f353 () Arctic (+ (* f24 f338) (* f25 f341) (* f26 f344))) (define-fun f354 () Arctic (+ (* f27 f336) (* f28 f339) (* f29 f342))) (define-fun f355 () Arctic (+ (* f27 f337) (* f28 f340) (* f29 f343))) (define-fun f356 () Arctic (+ (* f27 f338) (* f28 f341) (* f29 f344))) (define-fun f357 () Arctic (+ (* f30 f336) (* f31 f339) (* f32 f342))) (define-fun f358 () Arctic (+ (* f30 f337) (* f31 f340) (* f32 f343))) (define-fun f359 () Arctic (+ (* f30 f338) (* f31 f341) (* f32 f344))) (define-fun f360 () Arctic (+ (* f24 f348) (* f25 f349) (* f26 f350))) (define-fun f361 () Arctic (+ (* f27 f348) (* f28 f349) (* f29 f350))) (define-fun f362 () Arctic (+ (* f30 f348) (* f31 f349) (* f32 f350))) (define-fun f363 () Arctic (+ f33 f360)) (define-fun f364 () Arctic (+ f34 f361)) (define-fun f365 () Arctic (+ f35 f362)) (define-fun f366 () Arctic (+ (* f12 f351) (* f13 f354) (* f14 f357))) (define-fun f367 () Arctic (+ (* f12 f352) (* f13 f355) (* f14 f358))) (define-fun f368 () Arctic (+ (* f12 f353) (* f13 f356) (* f14 f359))) (define-fun f369 () Arctic (+ (* f15 f351) (* f16 f354) (* f17 f357))) (define-fun f370 () Arctic (+ (* f15 f352) (* f16 f355) (* f17 f358))) (define-fun f371 () Arctic (+ (* f15 f353) (* f16 f356) (* f17 f359))) (define-fun f372 () Arctic (+ (* f18 f351) (* f19 f354) (* f20 f357))) (define-fun f373 () Arctic (+ (* f18 f352) (* f19 f355) (* f20 f358))) (define-fun f374 () Arctic (+ (* f18 f353) (* f19 f356) (* f20 f359))) (define-fun f375 () Arctic (+ (* f12 f363) (* f13 f364) (* f14 f365))) (define-fun f376 () Arctic (+ (* f15 f363) (* f16 f364) (* f17 f365))) (define-fun f377 () Arctic (+ (* f18 f363) (* f19 f364) (* f20 f365))) (define-fun f378 () Arctic (+ f21 f375)) (define-fun f379 () Arctic (+ f22 f376)) (define-fun f380 () Arctic (+ f23 f377)) (define-fun f381 () Arctic (+ (* f24 f366) (* f25 f369) (* f26 f372))) (define-fun f382 () Arctic (+ (* f24 f367) (* f25 f370) (* f26 f373))) (define-fun f383 () Arctic (+ (* f24 f368) (* f25 f371) (* f26 f374))) (define-fun f384 () Arctic (+ (* f27 f366) (* f28 f369) (* f29 f372))) (define-fun f385 () Arctic (+ (* f27 f367) (* f28 f370) (* f29 f373))) (define-fun f386 () Arctic (+ (* f27 f368) (* f28 f371) (* f29 f374))) (define-fun f387 () Arctic (+ (* f30 f366) (* f31 f369) (* f32 f372))) (define-fun f388 () Arctic (+ (* f30 f367) (* f31 f370) (* f32 f373))) (define-fun f389 () Arctic (+ (* f30 f368) (* f31 f371) (* f32 f374))) (define-fun f390 () Arctic (+ (* f24 f378) (* f25 f379) (* f26 f380))) (define-fun f391 () Arctic (+ (* f27 f378) (* f28 f379) (* f29 f380))) (define-fun f392 () Arctic (+ (* f30 f378) (* f31 f379) (* f32 f380))) (define-fun f393 () Arctic (+ f33 f390)) (define-fun f394 () Arctic (+ f34 f391)) (define-fun f395 () Arctic (+ f35 f392)) (define-fun f396 () Arctic (+ (* f0 f381) (* f1 f384) (* f2 f387))) (define-fun f397 () Arctic (+ (* f0 f382) (* f1 f385) (* f2 f388))) (define-fun f398 () Arctic (+ (* f0 f383) (* f1 f386) (* f2 f389))) (define-fun f399 () Arctic (+ (* f3 f381) (* f4 f384) (* f5 f387))) (define-fun f400 () Arctic (+ (* f3 f382) (* f4 f385) (* f5 f388))) (define-fun f401 () Arctic (+ (* f3 f383) (* f4 f386) (* f5 f389))) (define-fun f402 () Arctic (+ (* f6 f381) (* f7 f384) (* f8 f387))) (define-fun f403 () Arctic (+ (* f6 f382) (* f7 f385) (* f8 f388))) (define-fun f404 () Arctic (+ (* f6 f383) (* f7 f386) (* f8 f389))) (define-fun f405 () Arctic (+ (* f0 f393) (* f1 f394) (* f2 f395))) (define-fun f406 () Arctic (+ (* f3 f393) (* f4 f394) (* f5 f395))) (define-fun f407 () Arctic (+ (* f6 f393) (* f7 f394) (* f8 f395))) (define-fun f408 () Arctic (+ f9 f405)) (define-fun f409 () Arctic (+ f10 f406)) (define-fun f410 () Arctic (+ f11 f407)) (define-fun f411 () Arctic (+ (* f0 f12) (* f1 f15) (* f2 f18))) (define-fun f412 () Arctic (+ (* f0 f13) (* f1 f16) (* f2 f19))) (define-fun f413 () Arctic (+ (* f0 f14) (* f1 f17) (* f2 f20))) (define-fun f414 () Arctic (+ (* f3 f12) (* f4 f15) (* f5 f18))) (define-fun f415 () Arctic (+ (* f3 f13) (* f4 f16) (* f5 f19))) (define-fun f416 () Arctic (+ (* f3 f14) (* f4 f17) (* f5 f20))) (define-fun f417 () Arctic (+ (* f6 f12) (* f7 f15) (* f8 f18))) (define-fun f418 () Arctic (+ (* f6 f13) (* f7 f16) (* f8 f19))) (define-fun f419 () Arctic (+ (* f6 f14) (* f7 f17) (* f8 f20))) (define-fun f420 () Arctic (+ (* f0 f21) (* f1 f22) (* f2 f23))) (define-fun f421 () Arctic (+ (* f3 f21) (* f4 f22) (* f5 f23))) (define-fun f422 () Arctic (+ (* f6 f21) (* f7 f22) (* f8 f23))) (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 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 (+ (* f12 f441) (* f13 f444) (* f14 f447))) (define-fun f457 () Arctic (+ (* f12 f442) (* f13 f445) (* f14 f448))) (define-fun f458 () Arctic (+ (* f12 f443) (* f13 f446) (* f14 f449))) (define-fun f459 () Arctic (+ (* f15 f441) (* f16 f444) (* f17 f447))) (define-fun f460 () Arctic (+ (* f15 f442) (* f16 f445) (* f17 f448))) (define-fun f461 () Arctic (+ (* f15 f443) (* f16 f446) (* f17 f449))) (define-fun f462 () Arctic (+ (* f18 f441) (* f19 f444) (* f20 f447))) (define-fun f463 () Arctic (+ (* f18 f442) (* f19 f445) (* f20 f448))) (define-fun f464 () Arctic (+ (* f18 f443) (* f19 f446) (* f20 f449))) (define-fun f465 () Arctic (+ (* f12 f453) (* f13 f454) (* f14 f455))) (define-fun f466 () Arctic (+ (* f15 f453) (* f16 f454) (* f17 f455))) (define-fun f467 () Arctic (+ (* f18 f453) (* f19 f454) (* f20 f455))) (define-fun f468 () Arctic (+ f21 f465)) (define-fun f469 () Arctic (+ f22 f466)) (define-fun f470 () Arctic (+ f23 f467)) (define-fun f471 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f472 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f473 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f474 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f475 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f476 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f477 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f478 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f479 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f480 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f481 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f482 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f483 () Arctic (+ f21 f480)) (define-fun f484 () Arctic (+ f22 f481)) (define-fun f485 () Arctic (+ f23 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 (+ (* f12 f486) (* f13 f489) (* f14 f492))) (define-fun f502 () Arctic (+ (* f12 f487) (* f13 f490) (* f14 f493))) (define-fun f503 () Arctic (+ (* f12 f488) (* f13 f491) (* f14 f494))) (define-fun f504 () Arctic (+ (* f15 f486) (* f16 f489) (* f17 f492))) (define-fun f505 () Arctic (+ (* f15 f487) (* f16 f490) (* f17 f493))) (define-fun f506 () Arctic (+ (* f15 f488) (* f16 f491) (* f17 f494))) (define-fun f507 () Arctic (+ (* f18 f486) (* f19 f489) (* f20 f492))) (define-fun f508 () Arctic (+ (* f18 f487) (* f19 f490) (* f20 f493))) (define-fun f509 () Arctic (+ (* f18 f488) (* f19 f491) (* f20 f494))) (define-fun f510 () Arctic (+ (* f12 f498) (* f13 f499) (* f14 f500))) (define-fun f511 () Arctic (+ (* f15 f498) (* f16 f499) (* f17 f500))) (define-fun f512 () Arctic (+ (* f18 f498) (* f19 f499) (* f20 f500))) (define-fun f513 () Arctic (+ f21 f510)) (define-fun f514 () Arctic (+ f22 f511)) (define-fun f515 () Arctic (+ f23 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 (+ (* f12 f516) (* f13 f519) (* f14 f522))) (define-fun f532 () Arctic (+ (* f12 f517) (* f13 f520) (* f14 f523))) (define-fun f533 () Arctic (+ (* f12 f518) (* f13 f521) (* f14 f524))) (define-fun f534 () Arctic (+ (* f15 f516) (* f16 f519) (* f17 f522))) (define-fun f535 () Arctic (+ (* f15 f517) (* f16 f520) (* f17 f523))) (define-fun f536 () Arctic (+ (* f15 f518) (* f16 f521) (* f17 f524))) (define-fun f537 () Arctic (+ (* f18 f516) (* f19 f519) (* f20 f522))) (define-fun f538 () Arctic (+ (* f18 f517) (* f19 f520) (* f20 f523))) (define-fun f539 () Arctic (+ (* f18 f518) (* f19 f521) (* f20 f524))) (define-fun f540 () Arctic (+ (* f12 f528) (* f13 f529) (* f14 f530))) (define-fun f541 () Arctic (+ (* f15 f528) (* f16 f529) (* f17 f530))) (define-fun f542 () Arctic (+ (* f18 f528) (* f19 f529) (* f20 f530))) (define-fun f543 () Arctic (+ f21 f540)) (define-fun f544 () Arctic (+ f22 f541)) (define-fun f545 () Arctic (+ f23 f542)) (define-fun f546 () Arctic (+ (* f24 f531) (* f25 f534) (* f26 f537))) (define-fun f547 () Arctic (+ (* f24 f532) (* f25 f535) (* f26 f538))) (define-fun f548 () Arctic (+ (* f24 f533) (* f25 f536) (* f26 f539))) (define-fun f549 () Arctic (+ (* f27 f531) (* f28 f534) (* f29 f537))) (define-fun f550 () Arctic (+ (* f27 f532) (* f28 f535) (* f29 f538))) (define-fun f551 () Arctic (+ (* f27 f533) (* f28 f536) (* f29 f539))) (define-fun f552 () Arctic (+ (* f30 f531) (* f31 f534) (* f32 f537))) (define-fun f553 () Arctic (+ (* f30 f532) (* f31 f535) (* f32 f538))) (define-fun f554 () Arctic (+ (* f30 f533) (* f31 f536) (* f32 f539))) (define-fun f555 () Arctic (+ (* f24 f543) (* f25 f544) (* f26 f545))) (define-fun f556 () Arctic (+ (* f27 f543) (* f28 f544) (* f29 f545))) (define-fun f557 () Arctic (+ (* f30 f543) (* f31 f544) (* f32 f545))) (define-fun f558 () Arctic (+ f33 f555)) (define-fun f559 () Arctic (+ f34 f556)) (define-fun f560 () Arctic (+ f35 f557)) (define-fun f561 () Arctic (+ (* f24 f546) (* f25 f549) (* f26 f552))) (define-fun f562 () Arctic (+ (* f24 f547) (* f25 f550) (* f26 f553))) (define-fun f563 () Arctic (+ (* f24 f548) (* f25 f551) (* f26 f554))) (define-fun f564 () Arctic (+ (* f27 f546) (* f28 f549) (* f29 f552))) (define-fun f565 () Arctic (+ (* f27 f547) (* f28 f550) (* f29 f553))) (define-fun f566 () Arctic (+ (* f27 f548) (* f28 f551) (* f29 f554))) (define-fun f567 () Arctic (+ (* f30 f546) (* f31 f549) (* f32 f552))) (define-fun f568 () Arctic (+ (* f30 f547) (* f31 f550) (* f32 f553))) (define-fun f569 () Arctic (+ (* f30 f548) (* f31 f551) (* f32 f554))) (define-fun f570 () Arctic (+ (* f24 f558) (* f25 f559) (* f26 f560))) (define-fun f571 () Arctic (+ (* f27 f558) (* f28 f559) (* f29 f560))) (define-fun f572 () Arctic (+ (* f30 f558) (* f31 f559) (* f32 f560))) (define-fun f573 () Arctic (+ f33 f570)) (define-fun f574 () Arctic (+ f34 f571)) (define-fun f575 () Arctic (+ f35 f572)) (define-fun f576 () Arctic (+ (* f12 f561) (* f13 f564) (* f14 f567))) (define-fun f577 () Arctic (+ (* f12 f562) (* f13 f565) (* f14 f568))) (define-fun f578 () Arctic (+ (* f12 f563) (* f13 f566) (* f14 f569))) (define-fun f579 () Arctic (+ (* f15 f561) (* f16 f564) (* f17 f567))) (define-fun f580 () Arctic (+ (* f15 f562) (* f16 f565) (* f17 f568))) (define-fun f581 () Arctic (+ (* f15 f563) (* f16 f566) (* f17 f569))) (define-fun f582 () Arctic (+ (* f18 f561) (* f19 f564) (* f20 f567))) (define-fun f583 () Arctic (+ (* f18 f562) (* f19 f565) (* f20 f568))) (define-fun f584 () Arctic (+ (* f18 f563) (* f19 f566) (* f20 f569))) (define-fun f585 () Arctic (+ (* f12 f573) (* f13 f574) (* f14 f575))) (define-fun f586 () Arctic (+ (* f15 f573) (* f16 f574) (* f17 f575))) (define-fun f587 () Arctic (+ (* f18 f573) (* f19 f574) (* f20 f575))) (define-fun f588 () Arctic (+ f21 f585)) (define-fun f589 () Arctic (+ f22 f586)) (define-fun f590 () Arctic (+ f23 f587)) (define-fun f591 () Arctic (+ (* f12 f576) (* f13 f579) (* f14 f582))) (define-fun f592 () Arctic (+ (* f12 f577) (* f13 f580) (* f14 f583))) (define-fun f593 () Arctic (+ (* f12 f578) (* f13 f581) (* f14 f584))) (define-fun f594 () Arctic (+ (* f15 f576) (* f16 f579) (* f17 f582))) (define-fun f595 () Arctic (+ (* f15 f577) (* f16 f580) (* f17 f583))) (define-fun f596 () Arctic (+ (* f15 f578) (* f16 f581) (* f17 f584))) (define-fun f597 () Arctic (+ (* f18 f576) (* f19 f579) (* f20 f582))) (define-fun f598 () Arctic (+ (* f18 f577) (* f19 f580) (* f20 f583))) (define-fun f599 () Arctic (+ (* f18 f578) (* f19 f581) (* f20 f584))) (define-fun f600 () Arctic (+ (* f12 f588) (* f13 f589) (* f14 f590))) (define-fun f601 () Arctic (+ (* f15 f588) (* f16 f589) (* f17 f590))) (define-fun f602 () Arctic (+ (* f18 f588) (* f19 f589) (* f20 f590))) (define-fun f603 () Arctic (+ f21 f600)) (define-fun f604 () Arctic (+ f22 f601)) (define-fun f605 () Arctic (+ f23 f602)) (define-fun f606 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f607 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f608 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f609 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f610 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f611 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f612 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f613 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f614 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f615 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f616 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f617 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f618 () Arctic (+ f33 f615)) (define-fun f619 () Arctic (+ f34 f616)) (define-fun f620 () Arctic (+ f35 f617)) (define-fun f621 () Arctic (+ (* f12 f606) (* f13 f609) (* f14 f612))) (define-fun f622 () Arctic (+ (* f12 f607) (* f13 f610) (* f14 f613))) (define-fun f623 () Arctic (+ (* f12 f608) (* f13 f611) (* f14 f614))) (define-fun f624 () Arctic (+ (* f15 f606) (* f16 f609) (* f17 f612))) (define-fun f625 () Arctic (+ (* f15 f607) (* f16 f610) (* f17 f613))) (define-fun f626 () Arctic (+ (* f15 f608) (* f16 f611) (* f17 f614))) (define-fun f627 () Arctic (+ (* f18 f606) (* f19 f609) (* f20 f612))) (define-fun f628 () Arctic (+ (* f18 f607) (* f19 f610) (* f20 f613))) (define-fun f629 () Arctic (+ (* f18 f608) (* f19 f611) (* f20 f614))) (define-fun f630 () Arctic (+ (* f12 f618) (* f13 f619) (* f14 f620))) (define-fun f631 () Arctic (+ (* f15 f618) (* f16 f619) (* f17 f620))) (define-fun f632 () Arctic (+ (* f18 f618) (* f19 f619) (* f20 f620))) (define-fun f633 () Arctic (+ f21 f630)) (define-fun f634 () Arctic (+ f22 f631)) (define-fun f635 () Arctic (+ f23 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 (+ (* f24 f636) (* f25 f639) (* f26 f642))) (define-fun f652 () Arctic (+ (* f24 f637) (* f25 f640) (* f26 f643))) (define-fun f653 () Arctic (+ (* f24 f638) (* f25 f641) (* f26 f644))) (define-fun f654 () Arctic (+ (* f27 f636) (* f28 f639) (* f29 f642))) (define-fun f655 () Arctic (+ (* f27 f637) (* f28 f640) (* f29 f643))) (define-fun f656 () Arctic (+ (* f27 f638) (* f28 f641) (* f29 f644))) (define-fun f657 () Arctic (+ (* f30 f636) (* f31 f639) (* f32 f642))) (define-fun f658 () Arctic (+ (* f30 f637) (* f31 f640) (* f32 f643))) (define-fun f659 () Arctic (+ (* f30 f638) (* f31 f641) (* f32 f644))) (define-fun f660 () Arctic (+ (* f24 f648) (* f25 f649) (* f26 f650))) (define-fun f661 () Arctic (+ (* f27 f648) (* f28 f649) (* f29 f650))) (define-fun f662 () Arctic (+ (* f30 f648) (* f31 f649) (* f32 f650))) (define-fun f663 () Arctic (+ f33 f660)) (define-fun f664 () Arctic (+ f34 f661)) (define-fun f665 () Arctic (+ f35 f662)) (define-fun f666 () Arctic (+ (* f12 f651) (* f13 f654) (* f14 f657))) (define-fun f667 () Arctic (+ (* f12 f652) (* f13 f655) (* f14 f658))) (define-fun f668 () Arctic (+ (* f12 f653) (* f13 f656) (* f14 f659))) (define-fun f669 () Arctic (+ (* f15 f651) (* f16 f654) (* f17 f657))) (define-fun f670 () Arctic (+ (* f15 f652) (* f16 f655) (* f17 f658))) (define-fun f671 () Arctic (+ (* f15 f653) (* f16 f656) (* f17 f659))) (define-fun f672 () Arctic (+ (* f18 f651) (* f19 f654) (* f20 f657))) (define-fun f673 () Arctic (+ (* f18 f652) (* f19 f655) (* f20 f658))) (define-fun f674 () Arctic (+ (* f18 f653) (* f19 f656) (* f20 f659))) (define-fun f675 () Arctic (+ (* f12 f663) (* f13 f664) (* f14 f665))) (define-fun f676 () Arctic (+ (* f15 f663) (* f16 f664) (* f17 f665))) (define-fun f677 () Arctic (+ (* f18 f663) (* f19 f664) (* f20 f665))) (define-fun f678 () Arctic (+ f21 f675)) (define-fun f679 () Arctic (+ f22 f676)) (define-fun f680 () Arctic (+ f23 f677)) (define-fun f681 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f682 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f683 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f684 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f685 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f686 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f687 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f688 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f689 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f690 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f691 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f692 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f693 () Arctic (+ f33 f690)) (define-fun f694 () Arctic (+ f34 f691)) (define-fun f695 () Arctic (+ f35 f692)) (define-fun f696 () Arctic (+ (* f24 f681) (* f25 f684) (* f26 f687))) (define-fun f697 () Arctic (+ (* f24 f682) (* f25 f685) (* f26 f688))) (define-fun f698 () Arctic (+ (* f24 f683) (* f25 f686) (* f26 f689))) (define-fun f699 () Arctic (+ (* f27 f681) (* f28 f684) (* f29 f687))) (define-fun f700 () Arctic (+ (* f27 f682) (* f28 f685) (* f29 f688))) (define-fun f701 () Arctic (+ (* f27 f683) (* f28 f686) (* f29 f689))) (define-fun f702 () Arctic (+ (* f30 f681) (* f31 f684) (* f32 f687))) (define-fun f703 () Arctic (+ (* f30 f682) (* f31 f685) (* f32 f688))) (define-fun f704 () Arctic (+ (* f30 f683) (* f31 f686) (* f32 f689))) (define-fun f705 () Arctic (+ (* f24 f693) (* f25 f694) (* f26 f695))) (define-fun f706 () Arctic (+ (* f27 f693) (* f28 f694) (* f29 f695))) (define-fun f707 () Arctic (+ (* f30 f693) (* f31 f694) (* f32 f695))) (define-fun f708 () Arctic (+ f33 f705)) (define-fun f709 () Arctic (+ f34 f706)) (define-fun f710 () Arctic (+ f35 f707)) (define-fun f711 () Arctic (+ (* f12 f696) (* f13 f699) (* f14 f702))) (define-fun f712 () Arctic (+ (* f12 f697) (* f13 f700) (* f14 f703))) (define-fun f713 () Arctic (+ (* f12 f698) (* f13 f701) (* f14 f704))) (define-fun f714 () Arctic (+ (* f15 f696) (* f16 f699) (* f17 f702))) (define-fun f715 () Arctic (+ (* f15 f697) (* f16 f700) (* f17 f703))) (define-fun f716 () Arctic (+ (* f15 f698) (* f16 f701) (* f17 f704))) (define-fun f717 () Arctic (+ (* f18 f696) (* f19 f699) (* f20 f702))) (define-fun f718 () Arctic (+ (* f18 f697) (* f19 f700) (* f20 f703))) (define-fun f719 () Arctic (+ (* f18 f698) (* f19 f701) (* f20 f704))) (define-fun f720 () Arctic (+ (* f12 f708) (* f13 f709) (* f14 f710))) (define-fun f721 () Arctic (+ (* f15 f708) (* f16 f709) (* f17 f710))) (define-fun f722 () Arctic (+ (* f18 f708) (* f19 f709) (* f20 f710))) (define-fun f723 () Arctic (+ f21 f720)) (define-fun f724 () Arctic (+ f22 f721)) (define-fun f725 () Arctic (+ f23 f722)) (define-fun f726 () Arctic (+ (* f24 f711) (* f25 f714) (* f26 f717))) (define-fun f727 () Arctic (+ (* f24 f712) (* f25 f715) (* f26 f718))) (define-fun f728 () Arctic (+ (* f24 f713) (* f25 f716) (* f26 f719))) (define-fun f729 () Arctic (+ (* f27 f711) (* f28 f714) (* f29 f717))) (define-fun f730 () Arctic (+ (* f27 f712) (* f28 f715) (* f29 f718))) (define-fun f731 () Arctic (+ (* f27 f713) (* f28 f716) (* f29 f719))) (define-fun f732 () Arctic (+ (* f30 f711) (* f31 f714) (* f32 f717))) (define-fun f733 () Arctic (+ (* f30 f712) (* f31 f715) (* f32 f718))) (define-fun f734 () Arctic (+ (* f30 f713) (* f31 f716) (* f32 f719))) (define-fun f735 () Arctic (+ (* f24 f723) (* f25 f724) (* f26 f725))) (define-fun f736 () Arctic (+ (* f27 f723) (* f28 f724) (* f29 f725))) (define-fun f737 () Arctic (+ (* f30 f723) (* f31 f724) (* f32 f725))) (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 (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f757 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f758 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f759 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f760 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f761 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f762 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f763 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f764 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f765 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f766 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f767 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f768 () Arctic (+ f21 f765)) (define-fun f769 () Arctic (+ f22 f766)) (define-fun f770 () Arctic (+ f23 f767)) (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 (>= f246 f291) (>= f247 f292) (>= f248 f293)) (and (>= f249 f294) (>= f250 f295) (>= f251 f296)) (and (>= f252 f297) (>= f253 f298) (>= f254 f299))) (and (and (>= f258 f303)) (and (>= f259 f304)) (and (>= f260 f305)))) (and (and (and (>= f321 f0) (>= f322 f1) (>= f323 f2)) (and (>= f324 f3) (>= f325 f4) (>= f326 f5)) (and (>= f327 f6) (>= f328 f7) (>= f329 f8))) (and (and (>= f333 f9)) (and (>= f334 f10)) (and (>= f335 f11)))) (and (and (and (>= f396 f411) (>= f397 f412) (>= f398 f413)) (and (>= f399 f414) (>= f400 f415) (>= f401 f416)) (and (>= f402 f417) (>= f403 f418) (>= f404 f419))) (and (and (>= f408 f423)) (and (>= f409 f424)) (and (>= f410 f425)))) (and (and (and (>= f426 f456) (>= f427 f457) (>= f428 f458)) (and (>= f429 f459) (>= f430 f460) (>= f431 f461)) (and (>= f432 f462) (>= f433 f463) (>= f434 f464))) (and (and (>= f438 f468)) (and (>= f439 f469)) (and (>= f440 f470)))) (and (and (and (>= f501 f591) (>= f502 f592) (>= f503 f593)) (and (>= f504 f594) (>= f505 f595) (>= f506 f596)) (and (>= f507 f597) (>= f508 f598) (>= f509 f599))) (and (and (>= f513 f603)) (and (>= f514 f604)) (and (>= f515 f605)))) (and (and (and (>= f621 f666) (>= f622 f667) (>= f623 f668)) (and (>= f624 f669) (>= f625 f670) (>= f626 f671)) (and (>= f627 f672) (>= f628 f673) (>= f629 f674))) (and (and (>= f633 f678)) (and (>= f634 f679)) (and (>= f635 f680)))) (and (and (and (>= f741 f756) (>= f742 f757) (>= f743 f758)) (and (>= f744 f759) (>= f745 f760) (>= f746 f761)) (and (>= f747 f762) (>= f748 f763) (>= f749 f764))) (and (and (>= f753 f768)) (and (>= f754 f769)) (and (>= f755 f770)))))) (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 (>> f246 f291) (>> f247 f292) (>> f248 f293)) (and (>> f249 f294) (>> f250 f295) (>> f251 f296)) (and (>> f252 f297) (>> f253 f298) (>> f254 f299))) (and (and (>> f258 f303)) (and (>> f259 f304)) (and (>> f260 f305)))) (and (and (and (>> f321 f0) (>> f322 f1) (>> f323 f2)) (and (>> f324 f3) (>> f325 f4) (>> f326 f5)) (and (>> f327 f6) (>> f328 f7) (>> f329 f8))) (and (and (>> f333 f9)) (and (>> f334 f10)) (and (>> f335 f11)))) (and (and (and (>> f396 f411) (>> f397 f412) (>> f398 f413)) (and (>> f399 f414) (>> f400 f415) (>> f401 f416)) (and (>> f402 f417) (>> f403 f418) (>> f404 f419))) (and (and (>> f408 f423)) (and (>> f409 f424)) (and (>> f410 f425)))))) (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))