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