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