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