(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES c# a a c -> a# a a, c# a a c -> a# a, c# a a c -> a#, b# -> a# c a, b# -> c# a, b# -> a#, a# b a -> b# b, c a a c ->= a a a, b ->= a c a, a b a ->= 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) (declare-fun f36 () Arctic) (declare-fun f37 () Arctic) (declare-fun f38 () Arctic) (declare-fun f39 () Arctic) (declare-fun f40 () Arctic) (declare-fun f41 () Arctic) (declare-fun f42 () Arctic) (declare-fun f43 () Arctic) (declare-fun f44 () Arctic) (declare-fun f45 () Arctic) (declare-fun f46 () Arctic) (declare-fun f47 () Arctic) (declare-fun f48 () Arctic) (declare-fun f49 () Arctic) (declare-fun f50 () Arctic) (declare-fun f51 () Arctic) (declare-fun f52 () Arctic) (declare-fun f53 () Arctic) (declare-fun f54 () Arctic) (declare-fun f55 () Arctic) (declare-fun f56 () Arctic) (declare-fun f57 () Arctic) (declare-fun f58 () Arctic) (declare-fun f59 () Arctic) (declare-fun f60 () Arctic) (declare-fun f61 () Arctic) (declare-fun f62 () Arctic) (declare-fun f63 () Arctic) (declare-fun f64 () Arctic) (declare-fun f65 () Arctic) (declare-fun f66 () Arctic) (declare-fun f67 () Arctic) (declare-fun f68 () Arctic) (declare-fun f69 () Arctic) (declare-fun f70 () Arctic) (declare-fun f71 () Arctic) (assert (and (or (finite f12) (finite f21)) (or (finite f60) (finite f69)) (or (finite f24) (finite f33)) (or (finite f36) (finite f45)) (or (finite f48) (finite f57)) (or (finite f0) (finite f9)))) (define-fun f72 () Arctic (+ (* f12 f24) (* f13 f27) (* f14 f30))) (define-fun f73 () Arctic (+ (* f12 f25) (* f13 f28) (* f14 f31))) (define-fun f74 () Arctic (+ (* f12 f26) (* f13 f29) (* f14 f32))) (define-fun f75 () Arctic (+ (* f15 f24) (* f16 f27) (* f17 f30))) (define-fun f76 () Arctic (+ (* f15 f25) (* f16 f28) (* f17 f31))) (define-fun f77 () Arctic (+ (* f15 f26) (* f16 f29) (* f17 f32))) (define-fun f78 () Arctic (+ (* f18 f24) (* f19 f27) (* f20 f30))) (define-fun f79 () Arctic (+ (* f18 f25) (* f19 f28) (* f20 f31))) (define-fun f80 () Arctic (+ (* f18 f26) (* f19 f29) (* f20 f32))) (define-fun f81 () Arctic (+ (* f12 f33) (* f13 f34) (* f14 f35))) (define-fun f82 () Arctic (+ (* f15 f33) (* f16 f34) (* f17 f35))) (define-fun f83 () Arctic (+ (* f18 f33) (* f19 f34) (* f20 f35))) (define-fun f84 () Arctic (+ f21 f81)) (define-fun f85 () Arctic (+ f22 f82)) (define-fun f86 () Arctic (+ f23 f83)) (define-fun f87 () Arctic (+ (* f12 f72) (* f13 f75) (* f14 f78))) (define-fun f88 () Arctic (+ (* f12 f73) (* f13 f76) (* f14 f79))) (define-fun f89 () Arctic (+ (* f12 f74) (* f13 f77) (* f14 f80))) (define-fun f90 () Arctic (+ (* f15 f72) (* f16 f75) (* f17 f78))) (define-fun f91 () Arctic (+ (* f15 f73) (* f16 f76) (* f17 f79))) (define-fun f92 () Arctic (+ (* f15 f74) (* f16 f77) (* f17 f80))) (define-fun f93 () Arctic (+ (* f18 f72) (* f19 f75) (* f20 f78))) (define-fun f94 () Arctic (+ (* f18 f73) (* f19 f76) (* f20 f79))) (define-fun f95 () Arctic (+ (* f18 f74) (* f19 f77) (* f20 f80))) (define-fun f96 () Arctic (+ (* f12 f84) (* f13 f85) (* f14 f86))) (define-fun f97 () Arctic (+ (* f15 f84) (* f16 f85) (* f17 f86))) (define-fun f98 () Arctic (+ (* f18 f84) (* f19 f85) (* f20 f86))) (define-fun f99 () Arctic (+ f21 f96)) (define-fun f100 () Arctic (+ f22 f97)) (define-fun f101 () Arctic (+ f23 f98)) (define-fun f102 () Arctic (+ (* f0 f87) (* f1 f90) (* f2 f93))) (define-fun f103 () Arctic (+ (* f0 f88) (* f1 f91) (* f2 f94))) (define-fun f104 () Arctic (+ (* f0 f89) (* f1 f92) (* f2 f95))) (define-fun f105 () Arctic (+ (* f3 f87) (* f4 f90) (* f5 f93))) (define-fun f106 () Arctic (+ (* f3 f88) (* f4 f91) (* f5 f94))) (define-fun f107 () Arctic (+ (* f3 f89) (* f4 f92) (* f5 f95))) (define-fun f108 () Arctic (+ (* f6 f87) (* f7 f90) (* f8 f93))) (define-fun f109 () Arctic (+ (* f6 f88) (* f7 f91) (* f8 f94))) (define-fun f110 () Arctic (+ (* f6 f89) (* f7 f92) (* f8 f95))) (define-fun f111 () Arctic (+ (* f0 f99) (* f1 f100) (* f2 f101))) (define-fun f112 () Arctic (+ (* f3 f99) (* f4 f100) (* f5 f101))) (define-fun f113 () Arctic (+ (* f6 f99) (* f7 f100) (* f8 f101))) (define-fun f114 () Arctic (+ f9 f111)) (define-fun f115 () Arctic (+ f10 f112)) (define-fun f116 () Arctic (+ f11 f113)) (define-fun f117 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f118 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f119 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f120 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f121 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f122 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f123 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f124 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f125 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f126 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f127 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f128 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f129 () Arctic (+ f21 f126)) (define-fun f130 () Arctic (+ f22 f127)) (define-fun f131 () Arctic (+ f23 f128)) (define-fun f132 () Arctic (+ (* f36 f117) (* f37 f120) (* f38 f123))) (define-fun f133 () Arctic (+ (* f36 f118) (* f37 f121) (* f38 f124))) (define-fun f134 () Arctic (+ (* f36 f119) (* f37 f122) (* f38 f125))) (define-fun f135 () Arctic (+ (* f39 f117) (* f40 f120) (* f41 f123))) (define-fun f136 () Arctic (+ (* f39 f118) (* f40 f121) (* f41 f124))) (define-fun f137 () Arctic (+ (* f39 f119) (* f40 f122) (* f41 f125))) (define-fun f138 () Arctic (+ (* f42 f117) (* f43 f120) (* f44 f123))) (define-fun f139 () Arctic (+ (* f42 f118) (* f43 f121) (* f44 f124))) (define-fun f140 () Arctic (+ (* f42 f119) (* f43 f122) (* f44 f125))) (define-fun f141 () Arctic (+ (* f36 f129) (* f37 f130) (* f38 f131))) (define-fun f142 () Arctic (+ (* f39 f129) (* f40 f130) (* f41 f131))) (define-fun f143 () Arctic (+ (* f42 f129) (* f43 f130) (* f44 f131))) (define-fun f144 () Arctic (+ f45 f141)) (define-fun f145 () Arctic (+ f46 f142)) (define-fun f146 () Arctic (+ f47 f143)) (define-fun f147 () Arctic (+ (* f12 f24) (* f13 f27) (* f14 f30))) (define-fun f148 () Arctic (+ (* f12 f25) (* f13 f28) (* f14 f31))) (define-fun f149 () Arctic (+ (* f12 f26) (* f13 f29) (* f14 f32))) (define-fun f150 () Arctic (+ (* f15 f24) (* f16 f27) (* f17 f30))) (define-fun f151 () Arctic (+ (* f15 f25) (* f16 f28) (* f17 f31))) (define-fun f152 () Arctic (+ (* f15 f26) (* f16 f29) (* f17 f32))) (define-fun f153 () Arctic (+ (* f18 f24) (* f19 f27) (* f20 f30))) (define-fun f154 () Arctic (+ (* f18 f25) (* f19 f28) (* f20 f31))) (define-fun f155 () Arctic (+ (* f18 f26) (* f19 f29) (* f20 f32))) (define-fun f156 () Arctic (+ (* f12 f33) (* f13 f34) (* f14 f35))) (define-fun f157 () Arctic (+ (* f15 f33) (* f16 f34) (* f17 f35))) (define-fun f158 () Arctic (+ (* f18 f33) (* f19 f34) (* f20 f35))) (define-fun f159 () Arctic (+ f21 f156)) (define-fun f160 () Arctic (+ f22 f157)) (define-fun f161 () Arctic (+ f23 f158)) (define-fun f162 () Arctic (+ (* f12 f147) (* f13 f150) (* f14 f153))) (define-fun f163 () Arctic (+ (* f12 f148) (* f13 f151) (* f14 f154))) (define-fun f164 () Arctic (+ (* f12 f149) (* f13 f152) (* f14 f155))) (define-fun f165 () Arctic (+ (* f15 f147) (* f16 f150) (* f17 f153))) (define-fun f166 () Arctic (+ (* f15 f148) (* f16 f151) (* f17 f154))) (define-fun f167 () Arctic (+ (* f15 f149) (* f16 f152) (* f17 f155))) (define-fun f168 () Arctic (+ (* f18 f147) (* f19 f150) (* f20 f153))) (define-fun f169 () Arctic (+ (* f18 f148) (* f19 f151) (* f20 f154))) (define-fun f170 () Arctic (+ (* f18 f149) (* f19 f152) (* f20 f155))) (define-fun f171 () Arctic (+ (* f12 f159) (* f13 f160) (* f14 f161))) (define-fun f172 () Arctic (+ (* f15 f159) (* f16 f160) (* f17 f161))) (define-fun f173 () Arctic (+ (* f18 f159) (* f19 f160) (* f20 f161))) (define-fun f174 () Arctic (+ f21 f171)) (define-fun f175 () Arctic (+ f22 f172)) (define-fun f176 () Arctic (+ f23 f173)) (define-fun f177 () Arctic (+ (* f0 f162) (* f1 f165) (* f2 f168))) (define-fun f178 () Arctic (+ (* f0 f163) (* f1 f166) (* f2 f169))) (define-fun f179 () Arctic (+ (* f0 f164) (* f1 f167) (* f2 f170))) (define-fun f180 () Arctic (+ (* f3 f162) (* f4 f165) (* f5 f168))) (define-fun f181 () Arctic (+ (* f3 f163) (* f4 f166) (* f5 f169))) (define-fun f182 () Arctic (+ (* f3 f164) (* f4 f167) (* f5 f170))) (define-fun f183 () Arctic (+ (* f6 f162) (* f7 f165) (* f8 f168))) (define-fun f184 () Arctic (+ (* f6 f163) (* f7 f166) (* f8 f169))) (define-fun f185 () Arctic (+ (* f6 f164) (* f7 f167) (* f8 f170))) (define-fun f186 () Arctic (+ (* f0 f174) (* f1 f175) (* f2 f176))) (define-fun f187 () Arctic (+ (* f3 f174) (* f4 f175) (* f5 f176))) (define-fun f188 () Arctic (+ (* f6 f174) (* f7 f175) (* f8 f176))) (define-fun f189 () Arctic (+ f9 f186)) (define-fun f190 () Arctic (+ f10 f187)) (define-fun f191 () Arctic (+ f11 f188)) (define-fun f192 () Arctic (+ (* f36 f12) (* f37 f15) (* f38 f18))) (define-fun f193 () Arctic (+ (* f36 f13) (* f37 f16) (* f38 f19))) (define-fun f194 () Arctic (+ (* f36 f14) (* f37 f17) (* f38 f20))) (define-fun f195 () Arctic (+ (* f39 f12) (* f40 f15) (* f41 f18))) (define-fun f196 () Arctic (+ (* f39 f13) (* f40 f16) (* f41 f19))) (define-fun f197 () Arctic (+ (* f39 f14) (* f40 f17) (* f41 f20))) (define-fun f198 () Arctic (+ (* f42 f12) (* f43 f15) (* f44 f18))) (define-fun f199 () Arctic (+ (* f42 f13) (* f43 f16) (* f44 f19))) (define-fun f200 () Arctic (+ (* f42 f14) (* f43 f17) (* f44 f20))) (define-fun f201 () Arctic (+ (* f36 f21) (* f37 f22) (* f38 f23))) (define-fun f202 () Arctic (+ (* f39 f21) (* f40 f22) (* f41 f23))) (define-fun f203 () Arctic (+ (* f42 f21) (* f43 f22) (* f44 f23))) (define-fun f204 () Arctic (+ f45 f201)) (define-fun f205 () Arctic (+ f46 f202)) (define-fun f206 () Arctic (+ f47 f203)) (define-fun f207 () Arctic (+ (* f12 f24) (* f13 f27) (* f14 f30))) (define-fun f208 () Arctic (+ (* f12 f25) (* f13 f28) (* f14 f31))) (define-fun f209 () Arctic (+ (* f12 f26) (* f13 f29) (* f14 f32))) (define-fun f210 () Arctic (+ (* f15 f24) (* f16 f27) (* f17 f30))) (define-fun f211 () Arctic (+ (* f15 f25) (* f16 f28) (* f17 f31))) (define-fun f212 () Arctic (+ (* f15 f26) (* f16 f29) (* f17 f32))) (define-fun f213 () Arctic (+ (* f18 f24) (* f19 f27) (* f20 f30))) (define-fun f214 () Arctic (+ (* f18 f25) (* f19 f28) (* f20 f31))) (define-fun f215 () Arctic (+ (* f18 f26) (* f19 f29) (* f20 f32))) (define-fun f216 () Arctic (+ (* f12 f33) (* f13 f34) (* f14 f35))) (define-fun f217 () Arctic (+ (* f15 f33) (* f16 f34) (* f17 f35))) (define-fun f218 () Arctic (+ (* f18 f33) (* f19 f34) (* f20 f35))) (define-fun f219 () Arctic (+ f21 f216)) (define-fun f220 () Arctic (+ f22 f217)) (define-fun f221 () Arctic (+ f23 f218)) (define-fun f222 () Arctic (+ (* f12 f207) (* f13 f210) (* f14 f213))) (define-fun f223 () Arctic (+ (* f12 f208) (* f13 f211) (* f14 f214))) (define-fun f224 () Arctic (+ (* f12 f209) (* f13 f212) (* f14 f215))) (define-fun f225 () Arctic (+ (* f15 f207) (* f16 f210) (* f17 f213))) (define-fun f226 () Arctic (+ (* f15 f208) (* f16 f211) (* f17 f214))) (define-fun f227 () Arctic (+ (* f15 f209) (* f16 f212) (* f17 f215))) (define-fun f228 () Arctic (+ (* f18 f207) (* f19 f210) (* f20 f213))) (define-fun f229 () Arctic (+ (* f18 f208) (* f19 f211) (* f20 f214))) (define-fun f230 () Arctic (+ (* f18 f209) (* f19 f212) (* f20 f215))) (define-fun f231 () Arctic (+ (* f12 f219) (* f13 f220) (* f14 f221))) (define-fun f232 () Arctic (+ (* f15 f219) (* f16 f220) (* f17 f221))) (define-fun f233 () Arctic (+ (* f18 f219) (* f19 f220) (* f20 f221))) (define-fun f234 () Arctic (+ f21 f231)) (define-fun f235 () Arctic (+ f22 f232)) (define-fun f236 () Arctic (+ f23 f233)) (define-fun f237 () Arctic (+ (* f0 f222) (* f1 f225) (* f2 f228))) (define-fun f238 () Arctic (+ (* f0 f223) (* f1 f226) (* f2 f229))) (define-fun f239 () Arctic (+ (* f0 f224) (* f1 f227) (* f2 f230))) (define-fun f240 () Arctic (+ (* f3 f222) (* f4 f225) (* f5 f228))) (define-fun f241 () Arctic (+ (* f3 f223) (* f4 f226) (* f5 f229))) (define-fun f242 () Arctic (+ (* f3 f224) (* f4 f227) (* f5 f230))) (define-fun f243 () Arctic (+ (* f6 f222) (* f7 f225) (* f8 f228))) (define-fun f244 () Arctic (+ (* f6 f223) (* f7 f226) (* f8 f229))) (define-fun f245 () Arctic (+ (* f6 f224) (* f7 f227) (* f8 f230))) (define-fun f246 () Arctic (+ (* f0 f234) (* f1 f235) (* f2 f236))) (define-fun f247 () Arctic (+ (* f3 f234) (* f4 f235) (* f5 f236))) (define-fun f248 () Arctic (+ (* f6 f234) (* f7 f235) (* f8 f236))) (define-fun f249 () Arctic (+ f9 f246)) (define-fun f250 () Arctic (+ f10 f247)) (define-fun f251 () Arctic (+ f11 f248)) (define-fun f252 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f253 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f254 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f255 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f256 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f257 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f258 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f259 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f260 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f261 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f262 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f263 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f264 () Arctic (+ f33 f261)) (define-fun f265 () Arctic (+ f34 f262)) (define-fun f266 () Arctic (+ f35 f263)) (define-fun f267 () Arctic (+ (* f36 f252) (* f37 f255) (* f38 f258))) (define-fun f268 () Arctic (+ (* f36 f253) (* f37 f256) (* f38 f259))) (define-fun f269 () Arctic (+ (* f36 f254) (* f37 f257) (* f38 f260))) (define-fun f270 () Arctic (+ (* f39 f252) (* f40 f255) (* f41 f258))) (define-fun f271 () Arctic (+ (* f39 f253) (* f40 f256) (* f41 f259))) (define-fun f272 () Arctic (+ (* f39 f254) (* f40 f257) (* f41 f260))) (define-fun f273 () Arctic (+ (* f42 f252) (* f43 f255) (* f44 f258))) (define-fun f274 () Arctic (+ (* f42 f253) (* f43 f256) (* f44 f259))) (define-fun f275 () Arctic (+ (* f42 f254) (* f43 f257) (* f44 f260))) (define-fun f276 () Arctic (+ (* f36 f264) (* f37 f265) (* f38 f266))) (define-fun f277 () Arctic (+ (* f39 f264) (* f40 f265) (* f41 f266))) (define-fun f278 () Arctic (+ (* f42 f264) (* f43 f265) (* f44 f266))) (define-fun f279 () Arctic (+ f45 f276)) (define-fun f280 () Arctic (+ f46 f277)) (define-fun f281 () Arctic (+ f47 f278)) (define-fun f282 () Arctic (+ (* f0 f12) (* f1 f15) (* f2 f18))) (define-fun f283 () Arctic (+ (* f0 f13) (* f1 f16) (* f2 f19))) (define-fun f284 () Arctic (+ (* f0 f14) (* f1 f17) (* f2 f20))) (define-fun f285 () Arctic (+ (* f3 f12) (* f4 f15) (* f5 f18))) (define-fun f286 () Arctic (+ (* f3 f13) (* f4 f16) (* f5 f19))) (define-fun f287 () Arctic (+ (* f3 f14) (* f4 f17) (* f5 f20))) (define-fun f288 () Arctic (+ (* f6 f12) (* f7 f15) (* f8 f18))) (define-fun f289 () Arctic (+ (* f6 f13) (* f7 f16) (* f8 f19))) (define-fun f290 () Arctic (+ (* f6 f14) (* f7 f17) (* f8 f20))) (define-fun f291 () Arctic (+ (* f0 f21) (* f1 f22) (* f2 f23))) (define-fun f292 () Arctic (+ (* f3 f21) (* f4 f22) (* f5 f23))) (define-fun f293 () Arctic (+ (* f6 f21) (* f7 f22) (* f8 f23))) (define-fun f294 () Arctic (+ f9 f291)) (define-fun f295 () Arctic (+ f10 f292)) (define-fun f296 () Arctic (+ f11 f293)) (define-fun f297 () Arctic (+ (* f60 f12) (* f61 f15) (* f62 f18))) (define-fun f298 () Arctic (+ (* f60 f13) (* f61 f16) (* f62 f19))) (define-fun f299 () Arctic (+ (* f60 f14) (* f61 f17) (* f62 f20))) (define-fun f300 () Arctic (+ (* f63 f12) (* f64 f15) (* f65 f18))) (define-fun f301 () Arctic (+ (* f63 f13) (* f64 f16) (* f65 f19))) (define-fun f302 () Arctic (+ (* f63 f14) (* f64 f17) (* f65 f20))) (define-fun f303 () Arctic (+ (* f66 f12) (* f67 f15) (* f68 f18))) (define-fun f304 () Arctic (+ (* f66 f13) (* f67 f16) (* f68 f19))) (define-fun f305 () Arctic (+ (* f66 f14) (* f67 f17) (* f68 f20))) (define-fun f306 () Arctic (+ (* f60 f21) (* f61 f22) (* f62 f23))) (define-fun f307 () Arctic (+ (* f63 f21) (* f64 f22) (* f65 f23))) (define-fun f308 () Arctic (+ (* f66 f21) (* f67 f22) (* f68 f23))) (define-fun f309 () Arctic (+ f69 f306)) (define-fun f310 () Arctic (+ f70 f307)) (define-fun f311 () Arctic (+ f71 f308)) (define-fun f312 () Arctic (+ (* f36 f297) (* f37 f300) (* f38 f303))) (define-fun f313 () Arctic (+ (* f36 f298) (* f37 f301) (* f38 f304))) (define-fun f314 () Arctic (+ (* f36 f299) (* f37 f302) (* f38 f305))) (define-fun f315 () Arctic (+ (* f39 f297) (* f40 f300) (* f41 f303))) (define-fun f316 () Arctic (+ (* f39 f298) (* f40 f301) (* f41 f304))) (define-fun f317 () Arctic (+ (* f39 f299) (* f40 f302) (* f41 f305))) (define-fun f318 () Arctic (+ (* f42 f297) (* f43 f300) (* f44 f303))) (define-fun f319 () Arctic (+ (* f42 f298) (* f43 f301) (* f44 f304))) (define-fun f320 () Arctic (+ (* f42 f299) (* f43 f302) (* f44 f305))) (define-fun f321 () Arctic (+ (* f36 f309) (* f37 f310) (* f38 f311))) (define-fun f322 () Arctic (+ (* f39 f309) (* f40 f310) (* f41 f311))) (define-fun f323 () Arctic (+ (* f42 f309) (* f43 f310) (* f44 f311))) (define-fun f324 () Arctic (+ f45 f321)) (define-fun f325 () Arctic (+ f46 f322)) (define-fun f326 () Arctic (+ f47 f323)) (define-fun f327 () Arctic (+ (* f48 f60) (* f49 f63) (* f50 f66))) (define-fun f328 () Arctic (+ (* f48 f61) (* f49 f64) (* f50 f67))) (define-fun f329 () Arctic (+ (* f48 f62) (* f49 f65) (* f50 f68))) (define-fun f330 () Arctic (+ (* f51 f60) (* f52 f63) (* f53 f66))) (define-fun f331 () Arctic (+ (* f51 f61) (* f52 f64) (* f53 f67))) (define-fun f332 () Arctic (+ (* f51 f62) (* f52 f65) (* f53 f68))) (define-fun f333 () Arctic (+ (* f54 f60) (* f55 f63) (* f56 f66))) (define-fun f334 () Arctic (+ (* f54 f61) (* f55 f64) (* f56 f67))) (define-fun f335 () Arctic (+ (* f54 f62) (* f55 f65) (* f56 f68))) (define-fun f336 () Arctic (+ (* f48 f69) (* f49 f70) (* f50 f71))) (define-fun f337 () Arctic (+ (* f51 f69) (* f52 f70) (* f53 f71))) (define-fun f338 () Arctic (+ (* f54 f69) (* f55 f70) (* f56 f71))) (define-fun f339 () Arctic (+ f57 f336)) (define-fun f340 () Arctic (+ f58 f337)) (define-fun f341 () Arctic (+ f59 f338)) (define-fun f342 () Arctic (+ (* f12 f24) (* f13 f27) (* f14 f30))) (define-fun f343 () Arctic (+ (* f12 f25) (* f13 f28) (* f14 f31))) (define-fun f344 () Arctic (+ (* f12 f26) (* f13 f29) (* f14 f32))) (define-fun f345 () Arctic (+ (* f15 f24) (* f16 f27) (* f17 f30))) (define-fun f346 () Arctic (+ (* f15 f25) (* f16 f28) (* f17 f31))) (define-fun f347 () Arctic (+ (* f15 f26) (* f16 f29) (* f17 f32))) (define-fun f348 () Arctic (+ (* f18 f24) (* f19 f27) (* f20 f30))) (define-fun f349 () Arctic (+ (* f18 f25) (* f19 f28) (* f20 f31))) (define-fun f350 () Arctic (+ (* f18 f26) (* f19 f29) (* f20 f32))) (define-fun f351 () Arctic (+ (* f12 f33) (* f13 f34) (* f14 f35))) (define-fun f352 () Arctic (+ (* f15 f33) (* f16 f34) (* f17 f35))) (define-fun f353 () Arctic (+ (* f18 f33) (* f19 f34) (* f20 f35))) (define-fun f354 () Arctic (+ f21 f351)) (define-fun f355 () Arctic (+ f22 f352)) (define-fun f356 () Arctic (+ f23 f353)) (define-fun f357 () Arctic (+ (* f12 f342) (* f13 f345) (* f14 f348))) (define-fun f358 () Arctic (+ (* f12 f343) (* f13 f346) (* f14 f349))) (define-fun f359 () Arctic (+ (* f12 f344) (* f13 f347) (* f14 f350))) (define-fun f360 () Arctic (+ (* f15 f342) (* f16 f345) (* f17 f348))) (define-fun f361 () Arctic (+ (* f15 f343) (* f16 f346) (* f17 f349))) (define-fun f362 () Arctic (+ (* f15 f344) (* f16 f347) (* f17 f350))) (define-fun f363 () Arctic (+ (* f18 f342) (* f19 f345) (* f20 f348))) (define-fun f364 () Arctic (+ (* f18 f343) (* f19 f346) (* f20 f349))) (define-fun f365 () Arctic (+ (* f18 f344) (* f19 f347) (* f20 f350))) (define-fun f366 () Arctic (+ (* f12 f354) (* f13 f355) (* f14 f356))) (define-fun f367 () Arctic (+ (* f15 f354) (* f16 f355) (* f17 f356))) (define-fun f368 () Arctic (+ (* f18 f354) (* f19 f355) (* f20 f356))) (define-fun f369 () Arctic (+ f21 f366)) (define-fun f370 () Arctic (+ f22 f367)) (define-fun f371 () Arctic (+ f23 f368)) (define-fun f372 () Arctic (+ (* f24 f357) (* f25 f360) (* f26 f363))) (define-fun f373 () Arctic (+ (* f24 f358) (* f25 f361) (* f26 f364))) (define-fun f374 () Arctic (+ (* f24 f359) (* f25 f362) (* f26 f365))) (define-fun f375 () Arctic (+ (* f27 f357) (* f28 f360) (* f29 f363))) (define-fun f376 () Arctic (+ (* f27 f358) (* f28 f361) (* f29 f364))) (define-fun f377 () Arctic (+ (* f27 f359) (* f28 f362) (* f29 f365))) (define-fun f378 () Arctic (+ (* f30 f357) (* f31 f360) (* f32 f363))) (define-fun f379 () Arctic (+ (* f30 f358) (* f31 f361) (* f32 f364))) (define-fun f380 () Arctic (+ (* f30 f359) (* f31 f362) (* f32 f365))) (define-fun f381 () Arctic (+ (* f24 f369) (* f25 f370) (* f26 f371))) (define-fun f382 () Arctic (+ (* f27 f369) (* f28 f370) (* f29 f371))) (define-fun f383 () Arctic (+ (* f30 f369) (* f31 f370) (* f32 f371))) (define-fun f384 () Arctic (+ f33 f381)) (define-fun f385 () Arctic (+ f34 f382)) (define-fun f386 () Arctic (+ f35 f383)) (define-fun f387 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f388 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f389 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f390 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f391 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f392 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f393 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f394 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f395 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f396 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f397 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f398 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f399 () Arctic (+ f21 f396)) (define-fun f400 () Arctic (+ f22 f397)) (define-fun f401 () Arctic (+ f23 f398)) (define-fun f402 () Arctic (+ (* f12 f387) (* f13 f390) (* f14 f393))) (define-fun f403 () Arctic (+ (* f12 f388) (* f13 f391) (* f14 f394))) (define-fun f404 () Arctic (+ (* f12 f389) (* f13 f392) (* f14 f395))) (define-fun f405 () Arctic (+ (* f15 f387) (* f16 f390) (* f17 f393))) (define-fun f406 () Arctic (+ (* f15 f388) (* f16 f391) (* f17 f394))) (define-fun f407 () Arctic (+ (* f15 f389) (* f16 f392) (* f17 f395))) (define-fun f408 () Arctic (+ (* f18 f387) (* f19 f390) (* f20 f393))) (define-fun f409 () Arctic (+ (* f18 f388) (* f19 f391) (* f20 f394))) (define-fun f410 () Arctic (+ (* f18 f389) (* f19 f392) (* f20 f395))) (define-fun f411 () Arctic (+ (* f12 f399) (* f13 f400) (* f14 f401))) (define-fun f412 () Arctic (+ (* f15 f399) (* f16 f400) (* f17 f401))) (define-fun f413 () Arctic (+ (* f18 f399) (* f19 f400) (* f20 f401))) (define-fun f414 () Arctic (+ f21 f411)) (define-fun f415 () Arctic (+ f22 f412)) (define-fun f416 () Arctic (+ f23 f413)) (define-fun f417 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f418 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f419 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f420 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f421 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f422 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f423 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f424 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f425 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f426 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f427 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f428 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f429 () Arctic (+ f33 f426)) (define-fun f430 () Arctic (+ f34 f427)) (define-fun f431 () Arctic (+ f35 f428)) (define-fun f432 () Arctic (+ (* f12 f417) (* f13 f420) (* f14 f423))) (define-fun f433 () Arctic (+ (* f12 f418) (* f13 f421) (* f14 f424))) (define-fun f434 () Arctic (+ (* f12 f419) (* f13 f422) (* f14 f425))) (define-fun f435 () Arctic (+ (* f15 f417) (* f16 f420) (* f17 f423))) (define-fun f436 () Arctic (+ (* f15 f418) (* f16 f421) (* f17 f424))) (define-fun f437 () Arctic (+ (* f15 f419) (* f16 f422) (* f17 f425))) (define-fun f438 () Arctic (+ (* f18 f417) (* f19 f420) (* f20 f423))) (define-fun f439 () Arctic (+ (* f18 f418) (* f19 f421) (* f20 f424))) (define-fun f440 () Arctic (+ (* f18 f419) (* f19 f422) (* f20 f425))) (define-fun f441 () Arctic (+ (* f12 f429) (* f13 f430) (* f14 f431))) (define-fun f442 () Arctic (+ (* f15 f429) (* f16 f430) (* f17 f431))) (define-fun f443 () Arctic (+ (* f18 f429) (* f19 f430) (* f20 f431))) (define-fun f444 () Arctic (+ f21 f441)) (define-fun f445 () Arctic (+ f22 f442)) (define-fun f446 () Arctic (+ f23 f443)) (define-fun f447 () Arctic (+ (* f60 f12) (* f61 f15) (* f62 f18))) (define-fun f448 () Arctic (+ (* f60 f13) (* f61 f16) (* f62 f19))) (define-fun f449 () Arctic (+ (* f60 f14) (* f61 f17) (* f62 f20))) (define-fun f450 () Arctic (+ (* f63 f12) (* f64 f15) (* f65 f18))) (define-fun f451 () Arctic (+ (* f63 f13) (* f64 f16) (* f65 f19))) (define-fun f452 () Arctic (+ (* f63 f14) (* f64 f17) (* f65 f20))) (define-fun f453 () Arctic (+ (* f66 f12) (* f67 f15) (* f68 f18))) (define-fun f454 () Arctic (+ (* f66 f13) (* f67 f16) (* f68 f19))) (define-fun f455 () Arctic (+ (* f66 f14) (* f67 f17) (* f68 f20))) (define-fun f456 () Arctic (+ (* f60 f21) (* f61 f22) (* f62 f23))) (define-fun f457 () Arctic (+ (* f63 f21) (* f64 f22) (* f65 f23))) (define-fun f458 () Arctic (+ (* f66 f21) (* f67 f22) (* f68 f23))) (define-fun f459 () Arctic (+ f69 f456)) (define-fun f460 () Arctic (+ f70 f457)) (define-fun f461 () Arctic (+ f71 f458)) (define-fun f462 () Arctic (+ (* f12 f447) (* f13 f450) (* f14 f453))) (define-fun f463 () Arctic (+ (* f12 f448) (* f13 f451) (* f14 f454))) (define-fun f464 () Arctic (+ (* f12 f449) (* f13 f452) (* f14 f455))) (define-fun f465 () Arctic (+ (* f15 f447) (* f16 f450) (* f17 f453))) (define-fun f466 () Arctic (+ (* f15 f448) (* f16 f451) (* f17 f454))) (define-fun f467 () Arctic (+ (* f15 f449) (* f16 f452) (* f17 f455))) (define-fun f468 () Arctic (+ (* f18 f447) (* f19 f450) (* f20 f453))) (define-fun f469 () Arctic (+ (* f18 f448) (* f19 f451) (* f20 f454))) (define-fun f470 () Arctic (+ (* f18 f449) (* f19 f452) (* f20 f455))) (define-fun f471 () Arctic (+ (* f12 f459) (* f13 f460) (* f14 f461))) (define-fun f472 () Arctic (+ (* f15 f459) (* f16 f460) (* f17 f461))) (define-fun f473 () Arctic (+ (* f18 f459) (* f19 f460) (* f20 f461))) (define-fun f474 () Arctic (+ f21 f471)) (define-fun f475 () Arctic (+ f22 f472)) (define-fun f476 () Arctic (+ f23 f473)) (define-fun f477 () Arctic (+ (* f60 f60) (* f61 f63) (* f62 f66))) (define-fun f478 () Arctic (+ (* f60 f61) (* f61 f64) (* f62 f67))) (define-fun f479 () Arctic (+ (* f60 f62) (* f61 f65) (* f62 f68))) (define-fun f480 () Arctic (+ (* f63 f60) (* f64 f63) (* f65 f66))) (define-fun f481 () Arctic (+ (* f63 f61) (* f64 f64) (* f65 f67))) (define-fun f482 () Arctic (+ (* f63 f62) (* f64 f65) (* f65 f68))) (define-fun f483 () Arctic (+ (* f66 f60) (* f67 f63) (* f68 f66))) (define-fun f484 () Arctic (+ (* f66 f61) (* f67 f64) (* f68 f67))) (define-fun f485 () Arctic (+ (* f66 f62) (* f67 f65) (* f68 f68))) (define-fun f486 () Arctic (+ (* f60 f69) (* f61 f70) (* f62 f71))) (define-fun f487 () Arctic (+ (* f63 f69) (* f64 f70) (* f65 f71))) (define-fun f488 () Arctic (+ (* f66 f69) (* f67 f70) (* f68 f71))) (define-fun f489 () Arctic (+ f69 f486)) (define-fun f490 () Arctic (+ f70 f487)) (define-fun f491 () Arctic (+ f71 f488)) (assert (and (and (and (and (>= f102 f132) (>= f103 f133) (>= f104 f134)) (and (>= f105 f135) (>= f106 f136) (>= f107 f137)) (and (>= f108 f138) (>= f109 f139) (>= f110 f140))) (and (and (>= f114 f144)) (and (>= f115 f145)) (and (>= f116 f146)))) (and (and (and (>= f177 f192) (>= f178 f193) (>= f179 f194)) (and (>= f180 f195) (>= f181 f196) (>= f182 f197)) (and (>= f183 f198) (>= f184 f199) (>= f185 f200))) (and (and (>= f189 f204)) (and (>= f190 f205)) (and (>= f191 f206)))) (and (and (and (>= f237 f36) (>= f238 f37) (>= f239 f38)) (and (>= f240 f39) (>= f241 f40) (>= f242 f41)) (and (>= f243 f42) (>= f244 f43) (>= f245 f44))) (and (and (>= f249 f45)) (and (>= f250 f46)) (and (>= f251 f47)))) (and (and (and (>= f48 f267) (>= f49 f268) (>= f50 f269)) (and (>= f51 f270) (>= f52 f271) (>= f53 f272)) (and (>= f54 f273) (>= f55 f274) (>= f56 f275))) (and (and (>= f57 f279)) (and (>= f58 f280)) (and (>= f59 f281)))) (and (and (and (>= f48 f282) (>= f49 f283) (>= f50 f284)) (and (>= f51 f285) (>= f52 f286) (>= f53 f287)) (and (>= f54 f288) (>= f55 f289) (>= f56 f290))) (and (and (>= f57 f294)) (and (>= f58 f295)) (and (>= f59 f296)))) (and (and (and (>= f48 f36) (>= f49 f37) (>= f50 f38)) (and (>= f51 f39) (>= f52 f40) (>= f53 f41)) (and (>= f54 f42) (>= f55 f43) (>= f56 f44))) (and (and (>= f57 f45)) (and (>= f58 f46)) (and (>= f59 f47)))) (and (and (and (>= f312 f327) (>= f313 f328) (>= f314 f329)) (and (>= f315 f330) (>= f316 f331) (>= f317 f332)) (and (>= f318 f333) (>= f319 f334) (>= f320 f335))) (and (and (>= f324 f339)) (and (>= f325 f340)) (and (>= f326 f341)))) (and (and (and (>= f372 f402) (>= f373 f403) (>= f374 f404)) (and (>= f375 f405) (>= f376 f406) (>= f377 f407)) (and (>= f378 f408) (>= f379 f409) (>= f380 f410))) (and (and (>= f384 f414)) (and (>= f385 f415)) (and (>= f386 f416)))) (and (and (and (>= f60 f432) (>= f61 f433) (>= f62 f434)) (and (>= f63 f435) (>= f64 f436) (>= f65 f437)) (and (>= f66 f438) (>= f67 f439) (>= f68 f440))) (and (and (>= f69 f444)) (and (>= f70 f445)) (and (>= f71 f446)))) (and (and (and (>= f462 f477) (>= f463 f478) (>= f464 f479)) (and (>= f465 f480) (>= f466 f481) (>= f467 f482)) (and (>= f468 f483) (>= f469 f484) (>= f470 f485))) (and (and (>= f474 f489)) (and (>= f475 f490)) (and (>= f476 f491)))))) (assert (or (and (and (and (>> f102 f132) (>> f103 f133) (>> f104 f134)) (and (>> f105 f135) (>> f106 f136) (>> f107 f137)) (and (>> f108 f138) (>> f109 f139) (>> f110 f140))) (and (and (>> f114 f144)) (and (>> f115 f145)) (and (>> f116 f146)))) (and (and (and (>> f177 f192) (>> f178 f193) (>> f179 f194)) (and (>> f180 f195) (>> f181 f196) (>> f182 f197)) (and (>> f183 f198) (>> f184 f199) (>> f185 f200))) (and (and (>> f189 f204)) (and (>> f190 f205)) (and (>> f191 f206)))) (and (and (and (>> f237 f36) (>> f238 f37) (>> f239 f38)) (and (>> f240 f39) (>> f241 f40) (>> f242 f41)) (and (>> f243 f42) (>> f244 f43) (>> f245 f44))) (and (and (>> f249 f45)) (and (>> f250 f46)) (and (>> f251 f47)))) (and (and (and (>> f48 f267) (>> f49 f268) (>> f50 f269)) (and (>> f51 f270) (>> f52 f271) (>> f53 f272)) (and (>> f54 f273) (>> f55 f274) (>> f56 f275))) (and (and (>> f57 f279)) (and (>> f58 f280)) (and (>> f59 f281)))) (and (and (and (>> f48 f282) (>> f49 f283) (>> f50 f284)) (and (>> f51 f285) (>> f52 f286) (>> f53 f287)) (and (>> f54 f288) (>> f55 f289) (>> f56 f290))) (and (and (>> f57 f294)) (and (>> f58 f295)) (and (>> f59 f296)))) (and (and (and (>> f48 f36) (>> f49 f37) (>> f50 f38)) (and (>> f51 f39) (>> f52 f40) (>> f53 f41)) (and (>> f54 f42) (>> f55 f43) (>> f56 f44))) (and (and (>> f57 f45)) (and (>> f58 f46)) (and (>> f59 f47)))) (and (and (and (>> f312 f327) (>> f313 f328) (>> f314 f329)) (and (>> f315 f330) (>> f316 f331) (>> f317 f332)) (and (>> f318 f333) (>> f319 f334) (>> f320 f335))) (and (and (>> f324 f339)) (and (>> f325 f340)) (and (>> f326 f341)))))) (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))