(set-option :produce-models true) (set-logic QF_Arctic) (set-info :source |remove at least one strict rule from (RULES a# b b a -> b# a a b, b# a b -> a# b b b, a b b a ->= b a a b, b a b ->= a b b b) by arctic matrix interpretation with dimension 3|) (declare-fun f0 () Arctic) (declare-fun f1 () Arctic) (declare-fun f2 () Arctic) (declare-fun f3 () Arctic) (declare-fun f4 () Arctic) (declare-fun f5 () Arctic) (declare-fun f6 () Arctic) (declare-fun f7 () Arctic) (declare-fun f8 () Arctic) (declare-fun f9 () Arctic) (declare-fun f10 () Arctic) (declare-fun f11 () Arctic) (declare-fun f12 () Arctic) (declare-fun f13 () Arctic) (declare-fun f14 () Arctic) (declare-fun f15 () Arctic) (declare-fun f16 () Arctic) (declare-fun f17 () Arctic) (declare-fun f18 () Arctic) (declare-fun f19 () Arctic) (declare-fun f20 () Arctic) (declare-fun f21 () Arctic) (declare-fun f22 () Arctic) (declare-fun f23 () Arctic) (declare-fun f24 () Arctic) (declare-fun f25 () Arctic) (declare-fun f26 () Arctic) (declare-fun f27 () Arctic) (declare-fun f28 () Arctic) (declare-fun f29 () Arctic) (declare-fun f30 () Arctic) (declare-fun f31 () Arctic) (declare-fun f32 () Arctic) (declare-fun f33 () Arctic) (declare-fun f34 () Arctic) (declare-fun f35 () Arctic) (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 f24) (finite f33)) (or (finite f12) (finite f21)) (or (finite f0) (finite f9)) (or (finite f36) (finite f45)))) (define-fun f48 () Arctic (+ (* f12 f24) (* f13 f27) (* f14 f30))) (define-fun f49 () Arctic (+ (* f12 f25) (* f13 f28) (* f14 f31))) (define-fun f50 () Arctic (+ (* f12 f26) (* f13 f29) (* f14 f32))) (define-fun f51 () Arctic (+ (* f15 f24) (* f16 f27) (* f17 f30))) (define-fun f52 () Arctic (+ (* f15 f25) (* f16 f28) (* f17 f31))) (define-fun f53 () Arctic (+ (* f15 f26) (* f16 f29) (* f17 f32))) (define-fun f54 () Arctic (+ (* f18 f24) (* f19 f27) (* f20 f30))) (define-fun f55 () Arctic (+ (* f18 f25) (* f19 f28) (* f20 f31))) (define-fun f56 () Arctic (+ (* f18 f26) (* f19 f29) (* f20 f32))) (define-fun f57 () Arctic (+ (* f12 f33) (* f13 f34) (* f14 f35))) (define-fun f58 () Arctic (+ (* f15 f33) (* f16 f34) (* f17 f35))) (define-fun f59 () Arctic (+ (* f18 f33) (* f19 f34) (* f20 f35))) (define-fun f60 () Arctic (+ f21 f57)) (define-fun f61 () Arctic (+ f22 f58)) (define-fun f62 () Arctic (+ f23 f59)) (define-fun f63 () Arctic (+ (* f12 f48) (* f13 f51) (* f14 f54))) (define-fun f64 () Arctic (+ (* f12 f49) (* f13 f52) (* f14 f55))) (define-fun f65 () Arctic (+ (* f12 f50) (* f13 f53) (* f14 f56))) (define-fun f66 () Arctic (+ (* f15 f48) (* f16 f51) (* f17 f54))) (define-fun f67 () Arctic (+ (* f15 f49) (* f16 f52) (* f17 f55))) (define-fun f68 () Arctic (+ (* f15 f50) (* f16 f53) (* f17 f56))) (define-fun f69 () Arctic (+ (* f18 f48) (* f19 f51) (* f20 f54))) (define-fun f70 () Arctic (+ (* f18 f49) (* f19 f52) (* f20 f55))) (define-fun f71 () Arctic (+ (* f18 f50) (* f19 f53) (* f20 f56))) (define-fun f72 () Arctic (+ (* f12 f60) (* f13 f61) (* f14 f62))) (define-fun f73 () Arctic (+ (* f15 f60) (* f16 f61) (* f17 f62))) (define-fun f74 () Arctic (+ (* f18 f60) (* f19 f61) (* f20 f62))) (define-fun f75 () Arctic (+ f21 f72)) (define-fun f76 () Arctic (+ f22 f73)) (define-fun f77 () Arctic (+ f23 f74)) (define-fun f78 () Arctic (+ (* f0 f63) (* f1 f66) (* f2 f69))) (define-fun f79 () Arctic (+ (* f0 f64) (* f1 f67) (* f2 f70))) (define-fun f80 () Arctic (+ (* f0 f65) (* f1 f68) (* f2 f71))) (define-fun f81 () Arctic (+ (* f3 f63) (* f4 f66) (* f5 f69))) (define-fun f82 () Arctic (+ (* f3 f64) (* f4 f67) (* f5 f70))) (define-fun f83 () Arctic (+ (* f3 f65) (* f4 f68) (* f5 f71))) (define-fun f84 () Arctic (+ (* f6 f63) (* f7 f66) (* f8 f69))) (define-fun f85 () Arctic (+ (* f6 f64) (* f7 f67) (* f8 f70))) (define-fun f86 () Arctic (+ (* f6 f65) (* f7 f68) (* f8 f71))) (define-fun f87 () Arctic (+ (* f0 f75) (* f1 f76) (* f2 f77))) (define-fun f88 () Arctic (+ (* f3 f75) (* f4 f76) (* f5 f77))) (define-fun f89 () Arctic (+ (* f6 f75) (* f7 f76) (* f8 f77))) (define-fun f90 () Arctic (+ f9 f87)) (define-fun f91 () Arctic (+ f10 f88)) (define-fun f92 () Arctic (+ f11 f89)) (define-fun f93 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f94 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f95 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f96 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f97 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f98 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f99 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f100 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f101 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f102 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f103 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f104 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f105 () Arctic (+ f33 f102)) (define-fun f106 () Arctic (+ f34 f103)) (define-fun f107 () Arctic (+ f35 f104)) (define-fun f108 () Arctic (+ (* f24 f93) (* f25 f96) (* f26 f99))) (define-fun f109 () Arctic (+ (* f24 f94) (* f25 f97) (* f26 f100))) (define-fun f110 () Arctic (+ (* f24 f95) (* f25 f98) (* f26 f101))) (define-fun f111 () Arctic (+ (* f27 f93) (* f28 f96) (* f29 f99))) (define-fun f112 () Arctic (+ (* f27 f94) (* f28 f97) (* f29 f100))) (define-fun f113 () Arctic (+ (* f27 f95) (* f28 f98) (* f29 f101))) (define-fun f114 () Arctic (+ (* f30 f93) (* f31 f96) (* f32 f99))) (define-fun f115 () Arctic (+ (* f30 f94) (* f31 f97) (* f32 f100))) (define-fun f116 () Arctic (+ (* f30 f95) (* f31 f98) (* f32 f101))) (define-fun f117 () Arctic (+ (* f24 f105) (* f25 f106) (* f26 f107))) (define-fun f118 () Arctic (+ (* f27 f105) (* f28 f106) (* f29 f107))) (define-fun f119 () Arctic (+ (* f30 f105) (* f31 f106) (* f32 f107))) (define-fun f120 () Arctic (+ f33 f117)) (define-fun f121 () Arctic (+ f34 f118)) (define-fun f122 () Arctic (+ f35 f119)) (define-fun f123 () Arctic (+ (* f36 f108) (* f37 f111) (* f38 f114))) (define-fun f124 () Arctic (+ (* f36 f109) (* f37 f112) (* f38 f115))) (define-fun f125 () Arctic (+ (* f36 f110) (* f37 f113) (* f38 f116))) (define-fun f126 () Arctic (+ (* f39 f108) (* f40 f111) (* f41 f114))) (define-fun f127 () Arctic (+ (* f39 f109) (* f40 f112) (* f41 f115))) (define-fun f128 () Arctic (+ (* f39 f110) (* f40 f113) (* f41 f116))) (define-fun f129 () Arctic (+ (* f42 f108) (* f43 f111) (* f44 f114))) (define-fun f130 () Arctic (+ (* f42 f109) (* f43 f112) (* f44 f115))) (define-fun f131 () Arctic (+ (* f42 f110) (* f43 f113) (* f44 f116))) (define-fun f132 () Arctic (+ (* f36 f120) (* f37 f121) (* f38 f122))) (define-fun f133 () Arctic (+ (* f39 f120) (* f40 f121) (* f41 f122))) (define-fun f134 () Arctic (+ (* f42 f120) (* f43 f121) (* f44 f122))) (define-fun f135 () Arctic (+ f45 f132)) (define-fun f136 () Arctic (+ f46 f133)) (define-fun f137 () Arctic (+ f47 f134)) (define-fun f138 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f139 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f140 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f141 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f142 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f143 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f144 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f145 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f146 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f147 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f148 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f149 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f150 () Arctic (+ f33 f147)) (define-fun f151 () Arctic (+ f34 f148)) (define-fun f152 () Arctic (+ f35 f149)) (define-fun f153 () Arctic (+ (* f36 f138) (* f37 f141) (* f38 f144))) (define-fun f154 () Arctic (+ (* f36 f139) (* f37 f142) (* f38 f145))) (define-fun f155 () Arctic (+ (* f36 f140) (* f37 f143) (* f38 f146))) (define-fun f156 () Arctic (+ (* f39 f138) (* f40 f141) (* f41 f144))) (define-fun f157 () Arctic (+ (* f39 f139) (* f40 f142) (* f41 f145))) (define-fun f158 () Arctic (+ (* f39 f140) (* f40 f143) (* f41 f146))) (define-fun f159 () Arctic (+ (* f42 f138) (* f43 f141) (* f44 f144))) (define-fun f160 () Arctic (+ (* f42 f139) (* f43 f142) (* f44 f145))) (define-fun f161 () Arctic (+ (* f42 f140) (* f43 f143) (* f44 f146))) (define-fun f162 () Arctic (+ (* f36 f150) (* f37 f151) (* f38 f152))) (define-fun f163 () Arctic (+ (* f39 f150) (* f40 f151) (* f41 f152))) (define-fun f164 () Arctic (+ (* f42 f150) (* f43 f151) (* f44 f152))) (define-fun f165 () Arctic (+ f45 f162)) (define-fun f166 () Arctic (+ f46 f163)) (define-fun f167 () Arctic (+ f47 f164)) (define-fun f168 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f169 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f170 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f171 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f172 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f173 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f174 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f175 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f176 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f177 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f178 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f179 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f180 () Arctic (+ f21 f177)) (define-fun f181 () Arctic (+ f22 f178)) (define-fun f182 () Arctic (+ f23 f179)) (define-fun f183 () Arctic (+ (* f12 f168) (* f13 f171) (* f14 f174))) (define-fun f184 () Arctic (+ (* f12 f169) (* f13 f172) (* f14 f175))) (define-fun f185 () Arctic (+ (* f12 f170) (* f13 f173) (* f14 f176))) (define-fun f186 () Arctic (+ (* f15 f168) (* f16 f171) (* f17 f174))) (define-fun f187 () Arctic (+ (* f15 f169) (* f16 f172) (* f17 f175))) (define-fun f188 () Arctic (+ (* f15 f170) (* f16 f173) (* f17 f176))) (define-fun f189 () Arctic (+ (* f18 f168) (* f19 f171) (* f20 f174))) (define-fun f190 () Arctic (+ (* f18 f169) (* f19 f172) (* f20 f175))) (define-fun f191 () Arctic (+ (* f18 f170) (* f19 f173) (* f20 f176))) (define-fun f192 () Arctic (+ (* f12 f180) (* f13 f181) (* f14 f182))) (define-fun f193 () Arctic (+ (* f15 f180) (* f16 f181) (* f17 f182))) (define-fun f194 () Arctic (+ (* f18 f180) (* f19 f181) (* f20 f182))) (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 (+ (* f12 f24) (* f13 f27) (* f14 f30))) (define-fun f214 () Arctic (+ (* f12 f25) (* f13 f28) (* f14 f31))) (define-fun f215 () Arctic (+ (* f12 f26) (* f13 f29) (* f14 f32))) (define-fun f216 () Arctic (+ (* f15 f24) (* f16 f27) (* f17 f30))) (define-fun f217 () Arctic (+ (* f15 f25) (* f16 f28) (* f17 f31))) (define-fun f218 () Arctic (+ (* f15 f26) (* f16 f29) (* f17 f32))) (define-fun f219 () Arctic (+ (* f18 f24) (* f19 f27) (* f20 f30))) (define-fun f220 () Arctic (+ (* f18 f25) (* f19 f28) (* f20 f31))) (define-fun f221 () Arctic (+ (* f18 f26) (* f19 f29) (* f20 f32))) (define-fun f222 () Arctic (+ (* f12 f33) (* f13 f34) (* f14 f35))) (define-fun f223 () Arctic (+ (* f15 f33) (* f16 f34) (* f17 f35))) (define-fun f224 () Arctic (+ (* f18 f33) (* f19 f34) (* f20 f35))) (define-fun f225 () Arctic (+ f21 f222)) (define-fun f226 () Arctic (+ f22 f223)) (define-fun f227 () Arctic (+ f23 f224)) (define-fun f228 () Arctic (+ (* f12 f213) (* f13 f216) (* f14 f219))) (define-fun f229 () Arctic (+ (* f12 f214) (* f13 f217) (* f14 f220))) (define-fun f230 () Arctic (+ (* f12 f215) (* f13 f218) (* f14 f221))) (define-fun f231 () Arctic (+ (* f15 f213) (* f16 f216) (* f17 f219))) (define-fun f232 () Arctic (+ (* f15 f214) (* f16 f217) (* f17 f220))) (define-fun f233 () Arctic (+ (* f15 f215) (* f16 f218) (* f17 f221))) (define-fun f234 () Arctic (+ (* f18 f213) (* f19 f216) (* f20 f219))) (define-fun f235 () Arctic (+ (* f18 f214) (* f19 f217) (* f20 f220))) (define-fun f236 () Arctic (+ (* f18 f215) (* f19 f218) (* f20 f221))) (define-fun f237 () Arctic (+ (* f12 f225) (* f13 f226) (* f14 f227))) (define-fun f238 () Arctic (+ (* f15 f225) (* f16 f226) (* f17 f227))) (define-fun f239 () Arctic (+ (* f18 f225) (* f19 f226) (* f20 f227))) (define-fun f240 () Arctic (+ f21 f237)) (define-fun f241 () Arctic (+ f22 f238)) (define-fun f242 () Arctic (+ f23 f239)) (define-fun f243 () Arctic (+ (* f24 f228) (* f25 f231) (* f26 f234))) (define-fun f244 () Arctic (+ (* f24 f229) (* f25 f232) (* f26 f235))) (define-fun f245 () Arctic (+ (* f24 f230) (* f25 f233) (* f26 f236))) (define-fun f246 () Arctic (+ (* f27 f228) (* f28 f231) (* f29 f234))) (define-fun f247 () Arctic (+ (* f27 f229) (* f28 f232) (* f29 f235))) (define-fun f248 () Arctic (+ (* f27 f230) (* f28 f233) (* f29 f236))) (define-fun f249 () Arctic (+ (* f30 f228) (* f31 f231) (* f32 f234))) (define-fun f250 () Arctic (+ (* f30 f229) (* f31 f232) (* f32 f235))) (define-fun f251 () Arctic (+ (* f30 f230) (* f31 f233) (* f32 f236))) (define-fun f252 () Arctic (+ (* f24 f240) (* f25 f241) (* f26 f242))) (define-fun f253 () Arctic (+ (* f27 f240) (* f28 f241) (* f29 f242))) (define-fun f254 () Arctic (+ (* f30 f240) (* f31 f241) (* f32 f242))) (define-fun f255 () Arctic (+ f33 f252)) (define-fun f256 () Arctic (+ f34 f253)) (define-fun f257 () Arctic (+ f35 f254)) (define-fun f258 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f259 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f260 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f261 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f262 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f263 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f264 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f265 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f266 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f267 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f268 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f269 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (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 (+ (* f12 f273) (* f13 f276) (* f14 f279))) (define-fun f289 () Arctic (+ (* f12 f274) (* f13 f277) (* f14 f280))) (define-fun f290 () Arctic (+ (* f12 f275) (* f13 f278) (* f14 f281))) (define-fun f291 () Arctic (+ (* f15 f273) (* f16 f276) (* f17 f279))) (define-fun f292 () Arctic (+ (* f15 f274) (* f16 f277) (* f17 f280))) (define-fun f293 () Arctic (+ (* f15 f275) (* f16 f278) (* f17 f281))) (define-fun f294 () Arctic (+ (* f18 f273) (* f19 f276) (* f20 f279))) (define-fun f295 () Arctic (+ (* f18 f274) (* f19 f277) (* f20 f280))) (define-fun f296 () Arctic (+ (* f18 f275) (* f19 f278) (* f20 f281))) (define-fun f297 () Arctic (+ (* f12 f285) (* f13 f286) (* f14 f287))) (define-fun f298 () Arctic (+ (* f15 f285) (* f16 f286) (* f17 f287))) (define-fun f299 () Arctic (+ (* f18 f285) (* f19 f286) (* f20 f287))) (define-fun f300 () Arctic (+ f21 f297)) (define-fun f301 () Arctic (+ f22 f298)) (define-fun f302 () Arctic (+ f23 f299)) (define-fun f303 () Arctic (+ (* f24 f12) (* f25 f15) (* f26 f18))) (define-fun f304 () Arctic (+ (* f24 f13) (* f25 f16) (* f26 f19))) (define-fun f305 () Arctic (+ (* f24 f14) (* f25 f17) (* f26 f20))) (define-fun f306 () Arctic (+ (* f27 f12) (* f28 f15) (* f29 f18))) (define-fun f307 () Arctic (+ (* f27 f13) (* f28 f16) (* f29 f19))) (define-fun f308 () Arctic (+ (* f27 f14) (* f28 f17) (* f29 f20))) (define-fun f309 () Arctic (+ (* f30 f12) (* f31 f15) (* f32 f18))) (define-fun f310 () Arctic (+ (* f30 f13) (* f31 f16) (* f32 f19))) (define-fun f311 () Arctic (+ (* f30 f14) (* f31 f17) (* f32 f20))) (define-fun f312 () Arctic (+ (* f24 f21) (* f25 f22) (* f26 f23))) (define-fun f313 () Arctic (+ (* f27 f21) (* f28 f22) (* f29 f23))) (define-fun f314 () Arctic (+ (* f30 f21) (* f31 f22) (* f32 f23))) (define-fun f315 () Arctic (+ f33 f312)) (define-fun f316 () Arctic (+ f34 f313)) (define-fun f317 () Arctic (+ f35 f314)) (define-fun f318 () Arctic (+ (* f12 f303) (* f13 f306) (* f14 f309))) (define-fun f319 () Arctic (+ (* f12 f304) (* f13 f307) (* f14 f310))) (define-fun f320 () Arctic (+ (* f12 f305) (* f13 f308) (* f14 f311))) (define-fun f321 () Arctic (+ (* f15 f303) (* f16 f306) (* f17 f309))) (define-fun f322 () Arctic (+ (* f15 f304) (* f16 f307) (* f17 f310))) (define-fun f323 () Arctic (+ (* f15 f305) (* f16 f308) (* f17 f311))) (define-fun f324 () Arctic (+ (* f18 f303) (* f19 f306) (* f20 f309))) (define-fun f325 () Arctic (+ (* f18 f304) (* f19 f307) (* f20 f310))) (define-fun f326 () Arctic (+ (* f18 f305) (* f19 f308) (* f20 f311))) (define-fun f327 () Arctic (+ (* f12 f315) (* f13 f316) (* f14 f317))) (define-fun f328 () Arctic (+ (* f15 f315) (* f16 f316) (* f17 f317))) (define-fun f329 () Arctic (+ (* f18 f315) (* f19 f316) (* f20 f317))) (define-fun f330 () Arctic (+ f21 f327)) (define-fun f331 () Arctic (+ f22 f328)) (define-fun f332 () Arctic (+ f23 f329)) (define-fun f333 () Arctic (+ (* f12 f12) (* f13 f15) (* f14 f18))) (define-fun f334 () Arctic (+ (* f12 f13) (* f13 f16) (* f14 f19))) (define-fun f335 () Arctic (+ (* f12 f14) (* f13 f17) (* f14 f20))) (define-fun f336 () Arctic (+ (* f15 f12) (* f16 f15) (* f17 f18))) (define-fun f337 () Arctic (+ (* f15 f13) (* f16 f16) (* f17 f19))) (define-fun f338 () Arctic (+ (* f15 f14) (* f16 f17) (* f17 f20))) (define-fun f339 () Arctic (+ (* f18 f12) (* f19 f15) (* f20 f18))) (define-fun f340 () Arctic (+ (* f18 f13) (* f19 f16) (* f20 f19))) (define-fun f341 () Arctic (+ (* f18 f14) (* f19 f17) (* f20 f20))) (define-fun f342 () Arctic (+ (* f12 f21) (* f13 f22) (* f14 f23))) (define-fun f343 () Arctic (+ (* f15 f21) (* f16 f22) (* f17 f23))) (define-fun f344 () Arctic (+ (* f18 f21) (* f19 f22) (* f20 f23))) (define-fun f345 () Arctic (+ f21 f342)) (define-fun f346 () Arctic (+ f22 f343)) (define-fun f347 () Arctic (+ f23 f344)) (define-fun f348 () Arctic (+ (* f12 f333) (* f13 f336) (* f14 f339))) (define-fun f349 () Arctic (+ (* f12 f334) (* f13 f337) (* f14 f340))) (define-fun f350 () Arctic (+ (* f12 f335) (* f13 f338) (* f14 f341))) (define-fun f351 () Arctic (+ (* f15 f333) (* f16 f336) (* f17 f339))) (define-fun f352 () Arctic (+ (* f15 f334) (* f16 f337) (* f17 f340))) (define-fun f353 () Arctic (+ (* f15 f335) (* f16 f338) (* f17 f341))) (define-fun f354 () Arctic (+ (* f18 f333) (* f19 f336) (* f20 f339))) (define-fun f355 () Arctic (+ (* f18 f334) (* f19 f337) (* f20 f340))) (define-fun f356 () Arctic (+ (* f18 f335) (* f19 f338) (* f20 f341))) (define-fun f357 () Arctic (+ (* f12 f345) (* f13 f346) (* f14 f347))) (define-fun f358 () Arctic (+ (* f15 f345) (* f16 f346) (* f17 f347))) (define-fun f359 () Arctic (+ (* f18 f345) (* f19 f346) (* f20 f347))) (define-fun f360 () Arctic (+ f21 f357)) (define-fun f361 () Arctic (+ f22 f358)) (define-fun f362 () Arctic (+ f23 f359)) (define-fun f363 () Arctic (+ (* f24 f348) (* f25 f351) (* f26 f354))) (define-fun f364 () Arctic (+ (* f24 f349) (* f25 f352) (* f26 f355))) (define-fun f365 () Arctic (+ (* f24 f350) (* f25 f353) (* f26 f356))) (define-fun f366 () Arctic (+ (* f27 f348) (* f28 f351) (* f29 f354))) (define-fun f367 () Arctic (+ (* f27 f349) (* f28 f352) (* f29 f355))) (define-fun f368 () Arctic (+ (* f27 f350) (* f28 f353) (* f29 f356))) (define-fun f369 () Arctic (+ (* f30 f348) (* f31 f351) (* f32 f354))) (define-fun f370 () Arctic (+ (* f30 f349) (* f31 f352) (* f32 f355))) (define-fun f371 () Arctic (+ (* f30 f350) (* f31 f353) (* f32 f356))) (define-fun f372 () Arctic (+ (* f24 f360) (* f25 f361) (* f26 f362))) (define-fun f373 () Arctic (+ (* f27 f360) (* f28 f361) (* f29 f362))) (define-fun f374 () Arctic (+ (* f30 f360) (* f31 f361) (* f32 f362))) (define-fun f375 () Arctic (+ f33 f372)) (define-fun f376 () Arctic (+ f34 f373)) (define-fun f377 () Arctic (+ f35 f374)) (assert (and (and (and (and (>= f78 f123) (>= f79 f124) (>= f80 f125)) (and (>= f81 f126) (>= f82 f127) (>= f83 f128)) (and (>= f84 f129) (>= f85 f130) (>= f86 f131))) (and (and (>= f90 f135)) (and (>= f91 f136)) (and (>= f92 f137)))) (and (and (and (>= f153 f198) (>= f154 f199) (>= f155 f200)) (and (>= f156 f201) (>= f157 f202) (>= f158 f203)) (and (>= f159 f204) (>= f160 f205) (>= f161 f206))) (and (and (>= f165 f210)) (and (>= f166 f211)) (and (>= f167 f212)))) (and (and (and (>= f243 f288) (>= f244 f289) (>= f245 f290)) (and (>= f246 f291) (>= f247 f292) (>= f248 f293)) (and (>= f249 f294) (>= f250 f295) (>= f251 f296))) (and (and (>= f255 f300)) (and (>= f256 f301)) (and (>= f257 f302)))) (and (and (and (>= f318 f363) (>= f319 f364) (>= f320 f365)) (and (>= f321 f366) (>= f322 f367) (>= f323 f368)) (and (>= f324 f369) (>= f325 f370) (>= f326 f371))) (and (and (>= f330 f375)) (and (>= f331 f376)) (and (>= f332 f377)))))) (assert (or (and (and (and (>> f78 f123) (>> f79 f124) (>> f80 f125)) (and (>> f81 f126) (>> f82 f127) (>> f83 f128)) (and (>> f84 f129) (>> f85 f130) (>> f86 f131))) (and (and (>> f90 f135)) (and (>> f91 f136)) (and (>> f92 f137)))) (and (and (and (>> f153 f198) (>> f154 f199) (>> f155 f200)) (and (>> f156 f201) (>> f157 f202) (>> f158 f203)) (and (>> f159 f204) (>> f160 f205) (>> f161 f206))) (and (and (>> f165 f210)) (and (>> f166 f211)) (and (>> f167 f212)))))) (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))