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