path: root/test/regress/regress1/nl/quant-nl.smt2

; COMMAND-LINE: --nl-ext
; EXPECT: unsat
(set-logic UFNIA)
(set-info :status unsat)
(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011.  Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(declare-sort S1 0)
(declare-sort S2 0)
(declare-sort S3 0)
(declare-sort S4 0)
(declare-sort S5 0)
(declare-sort S6 0)
(declare-sort S7 0)
(declare-sort S8 0)
(declare-sort S9 0)
(declare-sort S10 0)
(declare-sort S11 0)
(declare-sort S12 0)
(declare-sort S13 0)
(declare-sort S14 0)
(declare-sort S15 0)
(declare-sort S16 0)
(declare-sort S17 0)
(declare-sort S18 0)
(declare-sort S19 0)
(declare-sort S20 0)
(declare-sort S21 0)
(declare-sort S22 0)
(declare-sort S23 0)
(declare-sort S24 0)
(declare-sort S25 0)
(declare-sort S26 0)
(declare-sort S27 0)
(declare-sort S28 0)
(declare-sort S29 0)
(declare-sort S30 0)
(declare-sort S31 0)
(declare-sort S32 0)
(declare-sort S33 0)
(declare-sort S34 0)
(declare-sort S35 0)
(declare-sort S36 0)
(declare-sort S37 0)
(declare-sort S38 0)
(declare-sort S39 0)
(declare-sort S40 0)
(declare-sort S41 0)
(declare-sort S42 0)
(declare-sort S43 0)
(declare-sort S44 0)
(declare-sort S45 0)
(declare-sort S46 0)
(declare-sort S47 0)
(declare-sort S48 0)
(declare-sort S49 0)
(declare-sort S50 0)
(declare-sort S51 0)
(declare-sort S52 0)
(declare-sort S53 0)
(declare-sort S54 0)
(declare-sort S55 0)
(declare-sort S56 0)
(declare-sort S57 0)
(declare-sort S58 0)
(declare-sort S59 0)
(declare-sort S60 0)
(declare-sort S61 0)
(declare-sort S62 0)
(declare-sort S63 0)
(declare-sort S64 0)
(declare-sort S65 0)
(declare-sort S66 0)
(declare-sort S67 0)
(declare-sort S68 0)
(declare-sort S69 0)
(declare-sort S70 0)
(declare-sort S71 0)
(declare-sort S72 0)
(declare-sort S73 0)
(declare-sort S74 0)
(declare-sort S75 0)
(declare-sort S76 0)
(declare-sort S77 0)
(declare-sort S78 0)
(declare-sort S79 0)
(declare-sort S80 0)
(declare-sort S81 0)
(declare-sort S82 0)
(declare-sort S83 0)
(declare-sort S84 0)
(declare-sort S85 0)
(declare-sort S86 0)
(declare-sort S87 0)
(declare-sort S88 0)
(declare-sort S89 0)
(declare-sort S90 0)
(declare-sort S91 0)
(declare-sort S92 0)
(declare-sort S93 0)
(declare-sort S94 0)
(declare-sort S95 0)
(declare-sort S96 0)
(declare-sort S97 0)
(declare-sort S98 0)
(declare-sort S99 0)
(declare-sort S100 0)
(declare-sort S101 0)
(declare-sort S102 0)
(declare-sort S103 0)
(declare-sort S104 0)
(declare-sort S105 0)
(declare-sort S106 0)
(declare-sort S107 0)
(declare-sort S108 0)
(declare-sort S109 0)
(declare-sort S110 0)
(declare-sort S111 0)
(declare-sort S112 0)
(declare-sort S113 0)
(declare-sort S114 0)
(declare-sort S115 0)
(declare-sort S116 0)
(declare-sort S117 0)
(declare-sort S118 0)
(declare-sort S119 0)
(declare-sort S120 0)
(declare-sort S121 0)
(declare-sort S122 0)
(declare-sort S123 0)
(declare-sort S124 0)
(declare-sort S125 0)
(declare-sort S126 0)
(declare-sort S127 0)
(declare-sort S128 0)
(declare-sort S129 0)
(declare-sort S130 0)
(declare-sort S131 0)
(declare-sort S132 0)
(declare-sort S133 0)
(declare-sort S134 0)
(declare-sort S135 0)
(declare-sort S136 0)
(declare-sort S137 0)
(declare-sort S138 0)
(declare-sort S139 0)
(declare-sort S140 0)
(declare-sort S141 0)
(declare-sort S142 0)
(declare-sort S143 0)
(declare-sort S144 0)
(declare-sort S145 0)
(declare-sort S146 0)
(declare-sort S147 0)
(declare-sort S148 0)
(declare-sort S149 0)
(declare-sort S150 0)
(declare-sort S151 0)
(declare-sort S152 0)
(declare-sort S153 0)
(declare-sort S154 0)
(declare-sort S155 0)
(declare-sort S156 0)
(declare-sort S157 0)
(declare-sort S158 0)
(declare-sort S159 0)
(declare-sort S160 0)
(declare-sort S161 0)
(declare-sort S162 0)
(declare-sort S163 0)
(declare-sort S164 0)
(declare-sort S165 0)
(declare-sort S166 0)
(declare-sort S167 0)
(declare-sort S168 0)
(declare-sort S169 0)
(declare-sort S170 0)
(declare-sort S171 0)
(declare-sort S172 0)
(declare-sort S173 0)
(declare-sort S174 0)
(declare-sort S175 0)
(declare-sort S176 0)
(declare-sort S177 0)
(declare-sort S178 0)
(declare-sort S179 0)
(declare-sort S180 0)
(declare-sort S181 0)
(declare-sort S182 0)
(declare-sort S183 0)
(declare-sort S184 0)
(declare-sort S185 0)
(declare-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (Int) S1)
(declare-fun f4 () Int)
(declare-fun f5 () Int)
(declare-fun f6 (S2 S3) Int)
(declare-fun f7 () S2)
(declare-fun f8 (S4 Int) S3)
(declare-fun f9 (S5 Int) S4)
(declare-fun f10 () S5)
(declare-fun f11 (S6 S7) S1)
(declare-fun f12 (S9 S8) S7)
(declare-fun f13 (S10 S8) S9)
(declare-fun f14 () S10)
(declare-fun f15 (S11 S12) S1)
(declare-fun f16 (S13 S3) S12)
(declare-fun f17 (S14 S3) S13)
(declare-fun f18 () S14)
(declare-fun f19 (S15 S3) S1)
(declare-fun f20 (S16 S17) S1)
(declare-fun f21 (S19 S18) S17)
(declare-fun f22 (S20 S18) S19)
(declare-fun f23 () S20)
(declare-fun f24 (S21 S8) S1)
(declare-fun f25 (S22 S17) S8)
(declare-fun f26 (S23 S17) S22)
(declare-fun f27 () S23)
(declare-fun f28 (S24 S8) S21)
(declare-fun f29 (S6) S24)
(declare-fun f30 (S7 S6) S1)
(declare-fun f31 (S25 S3) S15)
(declare-fun f32 (S11) S25)
(declare-fun f33 (S12 S11) S1)
(declare-fun f34 (S26 Int) S1)
(declare-fun f35 (S27 Int) S26)
(declare-fun f36 (S15) S27)
(declare-fun f37 (S3 S15) S1)
(declare-fun f38 (S28 S18) S1)
(declare-fun f39 (S29 S18) S28)
(declare-fun f40 (S16) S29)
(declare-fun f41 (S17 S16) S1)
(declare-fun f42 (S30 S17) S16)
(declare-fun f43 (S21) S30)
(declare-fun f44 (S8 S21) S1)
(declare-fun f45 (S31 S8) S6)
(declare-fun f46 (S32 S33) S1)
(declare-fun f47 (S7 S7) S32)
(declare-fun f48 (S34 S31) S33)
(declare-fun f49 (S21) S34)
(declare-fun f50 (S35 S3) S11)
(declare-fun f51 (S36 S37) S1)
(declare-fun f52 (S12 S12) S36)
(declare-fun f53 (S38 S35) S37)
(declare-fun f54 (S15) S38)
(declare-fun f55 (S39 Int) S15)
(declare-fun f56 (S40 S39) S11)
(declare-fun f57 (S26) S40)
(declare-fun f58 (S41 S17) S21)
(declare-fun f59 (S42 S41) S6)
(declare-fun f60 (S16) S42)
(declare-fun f61 (S43 S18) S16)
(declare-fun f62 (S44 S43) S21)
(declare-fun f63 (S28) S44)
(declare-fun f64 (S6) S1)
(declare-fun f65 (S11) S1)
(declare-fun f66 (S15) S1)
(declare-fun f67 (S16) S1)
(declare-fun f68 (S21) S1)
(declare-fun f69 (S6) S1)
(declare-fun f70 (S11) S1)
(declare-fun f71 (S15) S1)
(declare-fun f72 (S16) S1)
(declare-fun f73 (S21) S1)
(declare-fun f74 (S6) S24)
(declare-fun f75 (S11) S25)
(declare-fun f76 (S15) S27)
(declare-fun f77 (S16) S29)
(declare-fun f78 (S21) S30)
(declare-fun f79 (S45 S6) S33)
(declare-fun f80 (S6) S45)
(declare-fun f81 (S46 S11) S37)
(declare-fun f82 (S11) S46)
(declare-fun f83 (S47 S15) S11)
(declare-fun f84 (S15) S47)
(declare-fun f85 (S48 S21) S6)
(declare-fun f86 (S21) S48)
(declare-fun f87 (S49 S50) S1)
(declare-fun f88 (S51 S51) S49)
(declare-fun f89 (Int S8) S51)
(declare-fun f90 (S15 S6) S50)
(declare-fun f91 (S52 S53) S1)
(declare-fun f92 (S54 S54) S52)
(declare-fun f93 (Int S3) S54)
(declare-fun f94 (S15 S11) S53)
(declare-fun f95 (S55 S56) S1)
(declare-fun f96 (S57 S57) S55)
(declare-fun f97 (S8 Int) S57)
(declare-fun f98 (S6 S15) S56)
(declare-fun f99 (S58 S59) S1)
(declare-fun f100 (S60 S60) S58)
(declare-fun f101 (S3 Int) S60)
(declare-fun f102 (S11 S15) S59)
(declare-fun f103 (S61 S16) S21)
(declare-fun f104 (S16) S61)
(declare-fun f105 (S62 S63) S1)
(declare-fun f106 (S64 S64) S62)
(declare-fun f107 (S18 Int) S64)
(declare-fun f108 (S16 S15) S63)
(declare-fun f109 (S65 S66) S1)
(declare-fun f110 (S67 S67) S65)
(declare-fun f111 (S18 S8) S67)
(declare-fun f112 (S16 S6) S66)
(declare-fun f113 (S68 S69) S1)
(declare-fun f114 (S70 S70) S68)
(declare-fun f115 (S18 S3) S70)
(declare-fun f116 (S16 S11) S69)
(declare-fun f117 (S71 S72) S1)
(declare-fun f118 (S73 S73) S71)
(declare-fun f119 (S17 Int) S73)
(declare-fun f120 (S21 S15) S72)
(declare-fun f121 (S74 S75) S1)
(declare-fun f122 (S76 S76) S74)
(declare-fun f123 (S17 S8) S76)
(declare-fun f124 (S21 S6) S75)
(declare-fun f125 (S77 S78) S1)
(declare-fun f126 (S79 S79) S77)
(declare-fun f127 (S17 S3) S79)
(declare-fun f128 (S21 S11) S78)
(declare-fun f129 (S80 S81) S1)
(declare-fun f130 (S82 S82) S80)
(declare-fun f131 (Int S18) S82)
(declare-fun f132 (S15 S16) S81)
(declare-fun f133 (S83 S84) S1)
(declare-fun f134 (S85 S85) S83)
(declare-fun f135 (S8 S18) S85)
(declare-fun f136 (S6 S16) S84)
(declare-fun f137 (S86 S87) S1)
(declare-fun f138 (S88 S88) S86)
(declare-fun f139 (S3 S18) S88)
(declare-fun f140 (S11 S16) S87)
(declare-fun f141 (S89 S90) S1)
(declare-fun f142 (S91 S91) S89)
(declare-fun f143 (Int S17) S91)
(declare-fun f144 (S15 S21) S90)
(declare-fun f145 (S92 S93) S1)
(declare-fun f146 (S94 S94) S92)
(declare-fun f147 (S8 S17) S94)
(declare-fun f148 (S6 S21) S93)
(declare-fun f149 (S95 S96) S1)
(declare-fun f150 (S97 S97) S95)
(declare-fun f151 (S3 S17) S97)
(declare-fun f152 (S11 S21) S96)
(declare-fun f153 (S98) S6)
(declare-fun f154 (S99 S18) Int)
(declare-fun f155 () S99)
(declare-fun f156 (S98 S8) S18)
(declare-fun f157 (S100) S11)
(declare-fun f158 (S100 S3) S18)
(declare-fun f159 (S101) S15)
(declare-fun f160 (S101 Int) S18)
(declare-fun f161 (S102) S16)
(declare-fun f162 (S102 S18) S18)
(declare-fun f163 (S103) S21)
(declare-fun f164 (S103 S17) S18)
(declare-fun f165 (S104 S6) S6)
(declare-fun f166 (S98) S104)
(declare-fun f167 (S105 S11) S11)
(declare-fun f168 (S100) S105)
(declare-fun f169 (S106 S15) S15)
(declare-fun f170 (S101) S106)
(declare-fun f171 (S107 S16) S16)
(declare-fun f172 (S102) S107)
(declare-fun f173 (S108 S21) S21)
(declare-fun f174 (S103) S108)
(declare-fun f175 (S15 S11) S1)
(declare-fun f176 (S6 S33) S1)
(declare-fun f177 (S11 S37) S1)
(declare-fun f178 (S26 S15) S1)
(declare-fun f179 (Int S26) S1)
(declare-fun f180 (S21 S6) S1)
(declare-fun f181 (S28 S16) S1)
(declare-fun f182 (S18 S28) S1)
(declare-fun f183 (S16 S21) S1)
(declare-fun f184 () S109)
(declare-fun f185 () S109)
(declare-fun f186 () S110)
(declare-fun f187 () S110)
(declare-fun f188 () S111)
(declare-fun f189 () S111)
(declare-fun f190 (S113 S112) S15)
(declare-fun f191 (S6) S113)
(declare-fun f192 (S112 Int) S8)
(declare-fun f193 (S114 S4) S15)
(declare-fun f194 (S11) S114)
(declare-fun f195 (S116 S115) S15)
(declare-fun f196 (S15) S116)
(declare-fun f197 (S115 Int) Int)
(declare-fun f198 (S118 S117) S6)
(declare-fun f199 (S15) S118)
(declare-fun f200 (S117 S8) Int)
(declare-fun f201 (S119 S2) S11)
(declare-fun f202 (S15) S119)
(declare-fun f203 (S120 S99) S16)
(declare-fun f204 (S15) S120)
(declare-fun f205 (S122 S121) S16)
(declare-fun f206 (S6) S122)
(declare-fun f207 (S121 S18) S8)
(declare-fun f208 (S124 S123) S16)
(declare-fun f209 (S11) S124)
(declare-fun f210 (S123 S18) S3)
(declare-fun f211 (S126 S125) S21)
(declare-fun f212 (S15) S126)
(declare-fun f213 (S125 S17) Int)
(declare-fun f214 (S127 S22) S21)
(declare-fun f215 (S6) S127)
(declare-fun f216 (S129 S128) S21)
(declare-fun f217 (S11) S129)
(declare-fun f218 (S128 S17) S3)
(declare-fun f219 (S130 S101) S15)
(declare-fun f220 (S16) S130)
(declare-fun f221 (S131 S98) S6)
(declare-fun f222 (S16) S131)
(declare-fun f223 (S132 S100) S11)
(declare-fun f224 (S16) S132)
(declare-fun f225 (S134 S133) S15)
(declare-fun f226 (S21) S134)
(declare-fun f227 (S133 Int) S17)
(declare-fun f228 (S136 S135) S6)
(declare-fun f229 (S21) S136)
(declare-fun f230 (S135 S8) S17)
(declare-fun f231 (S138 S137) S11)
(declare-fun f232 (S21) S138)
(declare-fun f233 (S137 S3) S17)
(declare-fun f234 (S24) S6)
(declare-fun f235 (S25) S11)
(declare-fun f236 (S111 S27) S15)
(declare-fun f237 (S110 S29) S16)
(declare-fun f238 (S109 S30) S21)
(declare-fun f239 (S139 Int) S39)
(declare-fun f240 (S139) S25)
(declare-fun f241 (S141 Int) S6)
(declare-fun f242 (S140 Int) S141)
(declare-fun f243 (S142 S3) S6)
(declare-fun f244 (S140) S142)
(declare-fun f245 (S144 Int) S11)
(declare-fun f246 (S143 Int) S144)
(declare-fun f247 (S143) S35)
(declare-fun f248 (S146 Int) S28)
(declare-fun f249 (S145 Int) S146)
(declare-fun f250 (S147 S3) S28)
(declare-fun f251 (S145) S147)
(declare-fun f252 (S148 Int) S27)
(declare-fun f253 (S149 S3) S26)
(declare-fun f254 (S148) S149)
(declare-fun f255 (S151 S18) S15)
(declare-fun f256 (S150 S18) S151)
(declare-fun f257 (S152 S17) S15)
(declare-fun f258 (S150) S152)
(declare-fun f259 (S154 S18) S6)
(declare-fun f260 (S153 S18) S154)
(declare-fun f261 (S155 S17) S6)
(declare-fun f262 (S153) S155)
(declare-fun f263 (S157 S18) S11)
(declare-fun f264 (S156 S18) S157)
(declare-fun f265 (S158 S17) S11)
(declare-fun f266 (S156) S158)
(declare-fun f267 (S159 S18) S29)
(declare-fun f268 (S160 S17) S28)
(declare-fun f269 (S159) S160)
(declare-fun f270 (S162 S18) S26)
(declare-fun f271 (S161 S18) S162)
(declare-fun f272 (S163 S17) S26)
(declare-fun f273 (S161) S163)
(declare-fun f274 (S164 S17) S152)
(declare-fun f275 (S165 S8) S15)
(declare-fun f276 (S164) S165)
(declare-fun f277 (S166 S17) S155)
(declare-fun f278 (S166) S31)
(declare-fun f279 (S167 S17) S158)
(declare-fun f280 (S168 S8) S11)
(declare-fun f281 (S167) S168)
(declare-fun f282 (S169 S17) S160)
(declare-fun f283 (S170 S8) S28)
(declare-fun f284 (S169) S170)
(declare-fun f285 (S171 S17) S163)
(declare-fun f286 (S172 S8) S26)
(declare-fun f287 (S171) S172)
(declare-fun f288 (S174 S8) S16)
(declare-fun f289 (S173 S8) S174)
(declare-fun f290 (S175 S7) S16)
(declare-fun f291 (S173) S175)
(declare-fun f292 (S177 S3) S16)
(declare-fun f293 (S176 S3) S177)
(declare-fun f294 (S178 S12) S16)
(declare-fun f295 (S176) S178)
(declare-fun f296 (S179 S8) S24)
(declare-fun f297 (S180 S7) S21)
(declare-fun f298 (S179) S180)
(declare-fun f299 (S182 S3) S21)
(declare-fun f300 (S181 S3) S182)
(declare-fun f301 (S183 S12) S21)
(declare-fun f302 (S181) S183)
(declare-fun f303 () S16)
(declare-fun f304 () S21)
(declare-fun f305 (S16) S1)
(declare-fun f306 (S21) S1)
(declare-fun f307 (S16) S1)
(declare-fun f308 (S21) S1)
(declare-fun f309 (S16) S1)
(declare-fun f310 (S15) S1)
(declare-fun f311 (S21) S1)
(declare-fun f312 (S15) S1)
(declare-fun f313 (S15) S1)
(declare-fun f314 (S6) S1)
(declare-fun f315 () S101)
(declare-fun f316 (S30) S1)
(declare-fun f317 (S29) S1)
(declare-fun f318 (S24) S1)
(declare-fun f319 () S16)
(declare-fun f320 () S21)
(declare-fun f321 (S184) S1)
(declare-fun f322 (S21) S184)
(declare-fun f323 (S185) S1)
(declare-fun f324 (S16) S185)
(declare-fun f325 (S16) S16)
(declare-fun f326 (S21) S21)
(declare-fun f327 (S15) S15)
(declare-fun f328 (S21) S184)
(declare-fun f329 (S16) S185)
(declare-fun f330 (S6) S6)
(declare-fun f331 (S11) S11)
(assert (not (= f1 f2)))
(assert (not (= (f3 (* f4 f5)) f1)))
(assert (= (f3 f4) f1))
(assert (= (f3 f5) f1))
(assert (forall ((?v0 Int)) (= (= (f3 ?v0) f1) (exists ((?v1 Int) (?v2 Int)) (= (f6 f7 (f8 (f9 f10 ?v1) ?v2)) ?v0)))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int)) (= (* (f6 f7 (f8 (f9 f10 ?v0) ?v1)) (f6 f7 (f8 (f9 f10 ?v2) ?v3))) (f6 f7 (f8 (f9 f10 (+ (* ?v0 ?v2) (* ?v1 ?v3))) (- (* ?v0 ?v3) (* ?v1 ?v2)))))))
(assert (forall ((?v0 S6)) (= (forall ((?v1 S7)) (= (f11 ?v0 ?v1) f1)) (forall ((?v1 S8) (?v2 S8)) (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S11)) (= (forall ((?v1 S12)) (= (f15 ?v0 ?v1) f1)) (forall ((?v1 S3) (?v2 S3)) (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S15)) (= (forall ((?v1 S3)) (= (f19 ?v0 ?v1) f1)) (forall ((?v1 Int) (?v2 Int)) (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S16)) (= (forall ((?v1 S17)) (= (f20 ?v0 ?v1) f1)) (forall ((?v1 S18) (?v2 S18)) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S21)) (= (forall ((?v1 S8)) (= (f24 ?v0 ?v1) f1)) (forall ((?v1 S17) (?v2 S17)) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8)) (= (= (f12 (f13 f14 ?v0) ?v1) (f12 (f13 f14 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3)) (= (= (f16 (f17 f18 ?v0) ?v1) (f16 (f17 f18 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int)) (= (= (f8 (f9 f10 ?v0) ?v1) (f8 (f9 f10 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (= (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S17) (?v3 S17)) (= (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8)) (=> (= (f12 (f13 f14 ?v0) ?v1) (f12 (f13 f14 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3)) (=> (= (f16 (f17 f18 ?v0) ?v1) (f16 (f17 f18 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int)) (=> (= (f8 (f9 f10 ?v0) ?v1) (f8 (f9 f10 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S17) (?v3 S17)) (=> (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (=> (=> (= ?v0 ?v2) (=> (= ?v1 ?v3) false)) false))))
(assert (forall ((?v0 S6) (?v1 S8) (?v2 S8)) (= (= (f24 (f28 (f29 ?v0) ?v1) ?v2) f1) (= (f30 (f12 (f13 f14 ?v1) ?v2) ?v0) f1))))
(assert (forall ((?v0 S11) (?v1 S3) (?v2 S3)) (= (= (f19 (f31 (f32 ?v0) ?v1) ?v2) f1) (= (f33 (f16 (f17 f18 ?v1) ?v2) ?v0) f1))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (= (= (f34 (f35 (f36 ?v0) ?v1) ?v2) f1) (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (= (= (f38 (f39 (f40 ?v0) ?v1) ?v2) f1) (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (= (= (f20 (f42 (f43 ?v0) ?v1) ?v2) f1) (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1))))
(assert (forall ((?v0 S21) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S31)) (let ((?v_0 (f13 f14 ?v1))) (=> (= (f24 ?v0 ?v1) f1) (=> (= (f30 (f12 (f13 f14 ?v2) ?v3) (f45 ?v4 ?v1)) f1) (= (f46 (f47 (f12 ?v_0 ?v2) (f12 ?v_0 ?v3)) (f48 (f49 ?v0) ?v4)) f1))))))
(assert (forall ((?v0 S15) (?v1 S3) (?v2 S3) (?v3 S3) (?v4 S35)) (let ((?v_0 (f17 f18 ?v1))) (=> (= (f19 ?v0 ?v1) f1) (=> (= (f33 (f16 (f17 f18 ?v2) ?v3) (f50 ?v4 ?v1)) f1) (= (f51 (f52 (f16 ?v_0 ?v2) (f16 ?v_0 ?v3)) (f53 (f54 ?v0) ?v4)) f1))))))
(assert (forall ((?v0 S26) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 S39)) (let ((?v_0 (f9 f10 ?v1))) (=> (= (f34 ?v0 ?v1) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v3) (f55 ?v4 ?v1)) f1) (= (f33 (f16 (f17 f18 (f8 ?v_0 ?v2)) (f8 ?v_0 ?v3)) (f56 (f57 ?v0) ?v4)) f1))))))
(assert (forall ((?v0 S16) (?v1 S17) (?v2 S17) (?v3 S17) (?v4 S41)) (let ((?v_0 (f26 f27 ?v1))) (=> (= (f20 ?v0 ?v1) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v3) (f58 ?v4 ?v1)) f1) (= (f30 (f12 (f13 f14 (f25 ?v_0 ?v2)) (f25 ?v_0 ?v3)) (f59 (f60 ?v0) ?v4)) f1))))))
(assert (forall ((?v0 S28) (?v1 S18) (?v2 S18) (?v3 S18) (?v4 S43)) (let ((?v_0 (f22 f23 ?v1))) (=> (= (f38 ?v0 ?v1) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v3) (f61 ?v4 ?v1)) f1) (= (f44 (f25 (f26 f27 (f21 ?v_0 ?v2)) (f21 ?v_0 ?v3)) (f62 (f63 ?v0) ?v4)) f1))))))
(assert (forall ((?v0 S6)) (= (= (f64 ?v0) f1) (forall ((?v1 S8)) (= (f30 (f12 (f13 f14 ?v1) ?v1) ?v0) f1)))))
(assert (forall ((?v0 S11)) (= (= (f65 ?v0) f1) (forall ((?v1 S3)) (= (f33 (f16 (f17 f18 ?v1) ?v1) ?v0) f1)))))
(assert (forall ((?v0 S15)) (= (= (f66 ?v0) f1) (forall ((?v1 Int)) (= (f37 (f8 (f9 f10 ?v1) ?v1) ?v0) f1)))))
(assert (forall ((?v0 S16)) (= (= (f67 ?v0) f1) (forall ((?v1 S18)) (= (f41 (f21 (f22 f23 ?v1) ?v1) ?v0) f1)))))
(assert (forall ((?v0 S21)) (= (= (f68 ?v0) f1) (forall ((?v1 S17)) (= (f44 (f25 (f26 f27 ?v1) ?v1) ?v0) f1)))))
(assert (forall ((?v0 S6)) (= (= (f69 ?v0) f1) (forall ((?v1 S8)) (not (= (f30 (f12 (f13 f14 ?v1) ?v1) ?v0) f1))))))
(assert (forall ((?v0 S11)) (= (= (f70 ?v0) f1) (forall ((?v1 S3)) (not (= (f33 (f16 (f17 f18 ?v1) ?v1) ?v0) f1))))))
(assert (forall ((?v0 S15)) (= (= (f71 ?v0) f1) (forall ((?v1 Int)) (not (= (f37 (f8 (f9 f10 ?v1) ?v1) ?v0) f1))))))
(assert (forall ((?v0 S16)) (= (= (f72 ?v0) f1) (forall ((?v1 S18)) (not (= (f41 (f21 (f22 f23 ?v1) ?v1) ?v0) f1))))))
(assert (forall ((?v0 S21)) (= (= (f73 ?v0) f1) (forall ((?v1 S17)) (not (= (f44 (f25 (f26 f27 ?v1) ?v1) ?v0) f1))))))
(assert (forall ((?v0 S6)) (= (exists ((?v1 S7)) (= (f11 ?v0 ?v1) f1)) (exists ((?v1 S8) (?v2 S8)) (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S11)) (= (exists ((?v1 S12)) (= (f15 ?v0 ?v1) f1)) (exists ((?v1 S3) (?v2 S3)) (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S15)) (= (exists ((?v1 S3)) (= (f19 ?v0 ?v1) f1)) (exists ((?v1 Int) (?v2 Int)) (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S16)) (= (exists ((?v1 S17)) (= (f20 ?v0 ?v1) f1)) (exists ((?v1 S18) (?v2 S18)) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S21)) (= (exists ((?v1 S8)) (= (f24 ?v0 ?v1) f1)) (exists ((?v1 S17) (?v2 S17)) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1)))))
(assert (forall ((?v0 S7)) (=> (forall ((?v1 S8) (?v2 S17) (?v3 S18) (?v4 S18)) (=> (= ?v0 (f12 (f13 f14 ?v1) (f25 (f26 f27 ?v2) (f21 (f22 f23 ?v3) ?v4)))) false)) false)))
(assert (forall ((?v0 S6) (?v1 S7)) (=> (forall ((?v2 S8) (?v3 S17) (?v4 S18) (?v5 S18)) (= (f11 ?v0 (f12 (f13 f14 ?v2) (f25 (f26 f27 ?v3) (f21 (f22 f23 ?v4) ?v5)))) f1)) (= (f11 ?v0 ?v1) f1))))
(assert (forall ((?v0 S8)) (=> (forall ((?v1 S17) (?v2 S18) (?v3 S18)) (=> (= ?v0 (f25 (f26 f27 ?v1) (f21 (f22 f23 ?v2) ?v3))) false)) false)))
(assert (forall ((?v0 S12)) (=> (forall ((?v1 S3) (?v2 Int) (?v3 Int)) (=> (= ?v0 (f16 (f17 f18 ?v1) (f8 (f9 f10 ?v2) ?v3))) false)) false)))
(assert (forall ((?v0 S7)) (=> (forall ((?v1 S8) (?v2 S17) (?v3 S17)) (=> (= ?v0 (f12 (f13 f14 ?v1) (f25 (f26 f27 ?v2) ?v3))) false)) false)))
(assert (forall ((?v0 S21) (?v1 S8)) (=> (forall ((?v2 S17) (?v3 S18) (?v4 S18)) (= (f24 ?v0 (f25 (f26 f27 ?v2) (f21 (f22 f23 ?v3) ?v4))) f1)) (= (f24 ?v0 ?v1) f1))))
(assert (forall ((?v0 S11) (?v1 S12)) (=> (forall ((?v2 S3) (?v3 Int) (?v4 Int)) (= (f15 ?v0 (f16 (f17 f18 ?v2) (f8 (f9 f10 ?v3) ?v4))) f1)) (= (f15 ?v0 ?v1) f1))))
(assert (forall ((?v0 S6) (?v1 S7)) (=> (forall ((?v2 S8) (?v3 S17) (?v4 S17)) (= (f11 ?v0 (f12 (f13 f14 ?v2) (f25 (f26 f27 ?v3) ?v4))) f1)) (= (f11 ?v0 ?v1) f1))))
(assert (forall ((?v0 S7)) (=> (forall ((?v1 S8) (?v2 S8)) (=> (= ?v0 (f12 (f13 f14 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S12)) (=> (forall ((?v1 S3) (?v2 S3)) (=> (= ?v0 (f16 (f17 f18 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S3)) (=> (forall ((?v1 Int) (?v2 Int)) (=> (= ?v0 (f8 (f9 f10 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S17)) (=> (forall ((?v1 S18) (?v2 S18)) (=> (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S8)) (=> (forall ((?v1 S17) (?v2 S17)) (=> (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S7)) (=> (forall ((?v1 S8) (?v2 S8)) (=> (= ?v0 (f12 (f13 f14 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S12)) (=> (forall ((?v1 S3) (?v2 S3)) (=> (= ?v0 (f16 (f17 f18 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S3)) (=> (forall ((?v1 Int) (?v2 Int)) (=> (= ?v0 (f8 (f9 f10 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S17)) (=> (forall ((?v1 S18) (?v2 S18)) (=> (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S8)) (=> (forall ((?v1 S17) (?v2 S17)) (=> (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false)) false)))
(assert (forall ((?v0 S6) (?v1 S8) (?v2 S8)) (=> (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1) (= (f24 (f28 (f74 ?v0) ?v1) ?v2) f1))))
(assert (forall ((?v0 S11) (?v1 S3) (?v2 S3)) (=> (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1) (= (f19 (f31 (f75 ?v0) ?v1) ?v2) f1))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1) (= (f34 (f35 (f76 ?v0) ?v1) ?v2) f1))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1) (= (f38 (f39 (f77 ?v0) ?v1) ?v2) f1))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1) (= (f20 (f42 (f78 ?v0) ?v1) ?v2) f1))))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S6) (?v5 S6)) (let ((?v_0 (f13 f14 ?v0))) (= (= (f46 (f47 (f12 ?v_0 ?v1) (f12 (f13 f14 ?v2) ?v3)) (f79 (f80 ?v4) ?v5)) f1) (or (= (f30 (f12 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f30 (f12 (f13 f14 ?v1) ?v3) ?v5) f1)))))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3) (?v4 S11) (?v5 S11)) (let ((?v_0 (f17 f18 ?v0))) (= (= (f51 (f52 (f16 ?v_0 ?v1) (f16 (f17 f18 ?v2) ?v3)) (f81 (f82 ?v4) ?v5)) f1) (or (= (f33 (f16 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f33 (f16 (f17 f18 ?v1) ?v3) ?v5) f1)))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 S15) (?v5 S15)) (let ((?v_0 (f9 f10 ?v0))) (= (= (f33 (f16 (f17 f18 (f8 ?v_0 ?v1)) (f8 (f9 f10 ?v2) ?v3)) (f83 (f84 ?v4) ?v5)) f1) (or (= (f37 (f8 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1)))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S17) (?v3 S17) (?v4 S21) (?v5 S21)) (let ((?v_0 (f26 f27 ?v0))) (= (= (f30 (f12 (f13 f14 (f25 ?v_0 ?v1)) (f25 (f26 f27 ?v2) ?v3)) (f85 (f86 ?v4) ?v5)) f1) (or (= (f44 (f25 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v5) f1)))))))
(assert (forall ((?v0 Int) (?v1 S8) (?v2 Int) (?v3 S8) (?v4 S15) (?v5 S6)) (= (= (f87 (f88 (f89 ?v0 ?v1) (f89 ?v2 ?v3)) (f90 ?v4 ?v5)) f1) (or (= (f37 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f30 (f12 (f13 f14 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 Int) (?v1 S3) (?v2 Int) (?v3 S3) (?v4 S15) (?v5 S11)) (= (= (f91 (f92 (f93 ?v0 ?v1) (f93 ?v2 ?v3)) (f94 ?v4 ?v5)) f1) (or (= (f37 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f33 (f16 (f17 f18 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S8) (?v1 Int) (?v2 S8) (?v3 Int) (?v4 S6) (?v5 S15)) (= (= (f95 (f96 (f97 ?v0 ?v1) (f97 ?v2 ?v3)) (f98 ?v4 ?v5)) f1) (or (= (f30 (f12 (f13 f14 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S3) (?v1 Int) (?v2 S3) (?v3 Int) (?v4 S11) (?v5 S15)) (= (= (f99 (f100 (f101 ?v0 ?v1) (f101 ?v2 ?v3)) (f102 ?v4 ?v5)) f1) (or (= (f33 (f16 (f17 f18 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18) (?v4 S16) (?v5 S16)) (let ((?v_0 (f22 f23 ?v0))) (= (= (f44 (f25 (f26 f27 (f21 ?v_0 ?v1)) (f21 (f22 f23 ?v2) ?v3)) (f103 (f104 ?v4) ?v5)) f1) (or (= (f41 (f21 ?v_0 ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v5) f1)))))))
(assert (forall ((?v0 S18) (?v1 Int) (?v2 S18) (?v3 Int) (?v4 S16) (?v5 S15)) (= (= (f105 (f106 (f107 ?v0 ?v1) (f107 ?v2 ?v3)) (f108 ?v4 ?v5)) f1) (or (= (f41 (f21 (f22 f23 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S18) (?v1 S8) (?v2 S18) (?v3 S8) (?v4 S16) (?v5 S6)) (= (= (f109 (f110 (f111 ?v0 ?v1) (f111 ?v2 ?v3)) (f112 ?v4 ?v5)) f1) (or (= (f41 (f21 (f22 f23 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f30 (f12 (f13 f14 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S18) (?v1 S3) (?v2 S18) (?v3 S3) (?v4 S16) (?v5 S11)) (= (= (f113 (f114 (f115 ?v0 ?v1) (f115 ?v2 ?v3)) (f116 ?v4 ?v5)) f1) (or (= (f41 (f21 (f22 f23 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f33 (f16 (f17 f18 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S17) (?v1 Int) (?v2 S17) (?v3 Int) (?v4 S21) (?v5 S15)) (= (= (f117 (f118 (f119 ?v0 ?v1) (f119 ?v2 ?v3)) (f120 ?v4 ?v5)) f1) (or (= (f44 (f25 (f26 f27 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S17) (?v1 S8) (?v2 S17) (?v3 S8) (?v4 S21) (?v5 S6)) (= (= (f121 (f122 (f123 ?v0 ?v1) (f123 ?v2 ?v3)) (f124 ?v4 ?v5)) f1) (or (= (f44 (f25 (f26 f27 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f30 (f12 (f13 f14 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S17) (?v1 S3) (?v2 S17) (?v3 S3) (?v4 S21) (?v5 S11)) (= (= (f125 (f126 (f127 ?v0 ?v1) (f127 ?v2 ?v3)) (f128 ?v4 ?v5)) f1) (or (= (f44 (f25 (f26 f27 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f33 (f16 (f17 f18 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 Int) (?v1 S18) (?v2 Int) (?v3 S18) (?v4 S15) (?v5 S16)) (= (= (f129 (f130 (f131 ?v0 ?v1) (f131 ?v2 ?v3)) (f132 ?v4 ?v5)) f1) (or (= (f37 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S8) (?v1 S18) (?v2 S8) (?v3 S18) (?v4 S6) (?v5 S16)) (= (= (f133 (f134 (f135 ?v0 ?v1) (f135 ?v2 ?v3)) (f136 ?v4 ?v5)) f1) (or (= (f30 (f12 (f13 f14 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S3) (?v1 S18) (?v2 S3) (?v3 S18) (?v4 S11) (?v5 S16)) (= (= (f137 (f138 (f139 ?v0 ?v1) (f139 ?v2 ?v3)) (f140 ?v4 ?v5)) f1) (or (= (f33 (f16 (f17 f18 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 Int) (?v1 S17) (?v2 Int) (?v3 S17) (?v4 S15) (?v5 S21)) (= (= (f141 (f142 (f143 ?v0 ?v1) (f143 ?v2 ?v3)) (f144 ?v4 ?v5)) f1) (or (= (f37 (f8 (f9 f10 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S8) (?v1 S17) (?v2 S8) (?v3 S17) (?v4 S6) (?v5 S21)) (= (= (f145 (f146 (f147 ?v0 ?v1) (f147 ?v2 ?v3)) (f148 ?v4 ?v5)) f1) (or (= (f30 (f12 (f13 f14 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S3) (?v1 S17) (?v2 S3) (?v3 S17) (?v4 S11) (?v5 S21)) (= (= (f149 (f150 (f151 ?v0 ?v1) (f151 ?v2 ?v3)) (f152 ?v4 ?v5)) f1) (or (= (f33 (f16 (f17 f18 ?v0) ?v2) ?v4) f1) (and (= ?v0 ?v2) (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v5) f1))))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (= (= (f34 (f35 (f76 ?v0) ?v1) ?v2) f1) (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (= (= (f38 (f39 (f77 ?v0) ?v1) ?v2) f1) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (= (= (f20 (f42 (f78 ?v0) ?v1) ?v2) f1) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S6) (?v1 S8) (?v2 S8)) (=> (= (f24 (f28 (f74 ?v0) ?v1) ?v2) f1) (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S11) (?v1 S3) (?v2 S3)) (=> (= (f19 (f31 (f75 ?v0) ?v1) ?v2) f1) (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f34 (f35 (f76 ?v0) ?v1) ?v2) f1) (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f38 (f39 (f77 ?v0) ?v1) ?v2) f1) (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f20 (f42 (f78 ?v0) ?v1) ?v2) f1) (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S6) (?v1 S8) (?v2 S8)) (=> (= (f24 (f28 (f74 ?v0) ?v1) ?v2) f1) (=> (=> (= (f11 ?v0 (f12 (f13 f14 ?v1) ?v2)) f1) false) false))))
(assert (forall ((?v0 S11) (?v1 S3) (?v2 S3)) (=> (= (f19 (f31 (f75 ?v0) ?v1) ?v2) f1) (=> (=> (= (f15 ?v0 (f16 (f17 f18 ?v1) ?v2)) f1) false) false))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f34 (f35 (f76 ?v0) ?v1) ?v2) f1) (=> (=> (= (f19 ?v0 (f8 (f9 f10 ?v1) ?v2)) f1) false) false))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f38 (f39 (f77 ?v0) ?v1) ?v2) f1) (=> (=> (= (f20 ?v0 (f21 (f22 f23 ?v1) ?v2)) f1) false) false))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f20 (f42 (f78 ?v0) ?v1) ?v2) f1) (=> (=> (= (f24 ?v0 (f25 (f26 f27 ?v1) ?v2)) f1) false) false))))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S98)) (= (= (f30 (f12 (f13 f14 ?v0) ?v1) (f153 ?v2)) f1) (< (f154 f155 (f156 ?v2 ?v0)) (f154 f155 (f156 ?v2 ?v1))))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S100)) (= (= (f33 (f16 (f17 f18 ?v0) ?v1) (f157 ?v2)) f1) (< (f154 f155 (f158 ?v2 ?v0)) (f154 f155 (f158 ?v2 ?v1))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S101)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f159 ?v2)) f1) (< (f154 f155 (f160 ?v2 ?v0)) (f154 f155 (f160 ?v2 ?v1))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S102)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f161 ?v2)) f1) (< (f154 f155 (f162 ?v2 ?v0)) (f154 f155 (f162 ?v2 ?v1))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S103)) (= (= (f44 (f25 (f26 f27 ?v0) ?v1) (f163 ?v2)) f1) (< (f154 f155 (f164 ?v2 ?v0)) (f154 f155 (f164 ?v2 ?v1))))))
(assert (forall ((?v0 S98) (?v1 S8) (?v2 S8) (?v3 S6)) (=> (< (f154 f155 (f156 ?v0 ?v1)) (f154 f155 (f156 ?v0 ?v2))) (= (f30 (f12 (f13 f14 ?v1) ?v2) (f165 (f166 ?v0) ?v3)) f1))))
(assert (forall ((?v0 S100) (?v1 S3) (?v2 S3) (?v3 S11)) (=> (< (f154 f155 (f158 ?v0 ?v1)) (f154 f155 (f158 ?v0 ?v2))) (= (f33 (f16 (f17 f18 ?v1) ?v2) (f167 (f168 ?v0) ?v3)) f1))))
(assert (forall ((?v0 S101) (?v1 Int) (?v2 Int) (?v3 S15)) (=> (< (f154 f155 (f160 ?v0 ?v1)) (f154 f155 (f160 ?v0 ?v2))) (= (f37 (f8 (f9 f10 ?v1) ?v2) (f169 (f170 ?v0) ?v3)) f1))))
(assert (forall ((?v0 S102) (?v1 S18) (?v2 S18) (?v3 S16)) (=> (< (f154 f155 (f162 ?v0 ?v1)) (f154 f155 (f162 ?v0 ?v2))) (= (f41 (f21 (f22 f23 ?v1) ?v2) (f171 (f172 ?v0) ?v3)) f1))))
(assert (forall ((?v0 S103) (?v1 S17) (?v2 S17) (?v3 S21)) (=> (< (f154 f155 (f164 ?v0 ?v1)) (f154 f155 (f164 ?v0 ?v2))) (= (f44 (f25 (f26 f27 ?v1) ?v2) (f173 (f174 ?v0) ?v3)) f1))))
(assert (forall ((?v0 S98) (?v1 S8) (?v2 S8) (?v3 S6)) (let ((?v_0 (f12 (f13 f14 ?v1) ?v2))) (=> (<= (f154 f155 (f156 ?v0 ?v1)) (f154 f155 (f156 ?v0 ?v2))) (=> (= (f30 ?v_0 ?v3) f1) (= (f30 ?v_0 (f165 (f166 ?v0) ?v3)) f1))))))
(assert (forall ((?v0 S100) (?v1 S3) (?v2 S3) (?v3 S11)) (let ((?v_0 (f16 (f17 f18 ?v1) ?v2))) (=> (<= (f154 f155 (f158 ?v0 ?v1)) (f154 f155 (f158 ?v0 ?v2))) (=> (= (f33 ?v_0 ?v3) f1) (= (f33 ?v_0 (f167 (f168 ?v0) ?v3)) f1))))))
(assert (forall ((?v0 S101) (?v1 Int) (?v2 Int) (?v3 S15)) (let ((?v_0 (f8 (f9 f10 ?v1) ?v2))) (=> (<= (f154 f155 (f160 ?v0 ?v1)) (f154 f155 (f160 ?v0 ?v2))) (=> (= (f37 ?v_0 ?v3) f1) (= (f37 ?v_0 (f169 (f170 ?v0) ?v3)) f1))))))
(assert (forall ((?v0 S102) (?v1 S18) (?v2 S18) (?v3 S16)) (let ((?v_0 (f21 (f22 f23 ?v1) ?v2))) (=> (<= (f154 f155 (f162 ?v0 ?v1)) (f154 f155 (f162 ?v0 ?v2))) (=> (= (f41 ?v_0 ?v3) f1) (= (f41 ?v_0 (f171 (f172 ?v0) ?v3)) f1))))))
(assert (forall ((?v0 S103) (?v1 S17) (?v2 S17) (?v3 S21)) (let ((?v_0 (f25 (f26 f27 ?v1) ?v2))) (=> (<= (f154 f155 (f164 ?v0 ?v1)) (f154 f155 (f164 ?v0 ?v2))) (=> (= (f44 ?v_0 ?v3) f1) (= (f44 ?v_0 (f173 (f174 ?v0) ?v3)) f1))))))
(assert (forall ((?v0 S15) (?v1 S11)) (= (= (f175 ?v0 ?v1) f1) (forall ((?v2 S3)) (=> (= (f37 ?v2 ?v0) f1) (forall ((?v3 S3)) (=> (= (f37 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f33 (f16 (f17 f18 ?v2) ?v3) ?v1) f1) (= (f33 (f16 (f17 f18 ?v3) ?v2) ?v1) f1))))))))))
(assert (forall ((?v0 S6) (?v1 S33)) (= (= (f176 ?v0 ?v1) f1) (forall ((?v2 S7)) (=> (= (f30 ?v2 ?v0) f1) (forall ((?v3 S7)) (=> (= (f30 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f46 (f47 ?v2 ?v3) ?v1) f1) (= (f46 (f47 ?v3 ?v2) ?v1) f1))))))))))
(assert (forall ((?v0 S11) (?v1 S37)) (= (= (f177 ?v0 ?v1) f1) (forall ((?v2 S12)) (=> (= (f33 ?v2 ?v0) f1) (forall ((?v3 S12)) (=> (= (f33 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f51 (f52 ?v2 ?v3) ?v1) f1) (= (f51 (f52 ?v3 ?v2) ?v1) f1))))))))))
(assert (forall ((?v0 S26) (?v1 S15)) (= (= (f178 ?v0 ?v1) f1) (forall ((?v2 Int)) (=> (= (f179 ?v2 ?v0) f1) (forall ((?v3 Int)) (=> (= (f179 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f37 (f8 (f9 f10 ?v2) ?v3) ?v1) f1) (= (f37 (f8 (f9 f10 ?v3) ?v2) ?v1) f1))))))))))
(assert (forall ((?v0 S21) (?v1 S6)) (= (= (f180 ?v0 ?v1) f1) (forall ((?v2 S8)) (=> (= (f44 ?v2 ?v0) f1) (forall ((?v3 S8)) (=> (= (f44 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f30 (f12 (f13 f14 ?v2) ?v3) ?v1) f1) (= (f30 (f12 (f13 f14 ?v3) ?v2) ?v1) f1))))))))))
(assert (forall ((?v0 S28) (?v1 S16)) (= (= (f181 ?v0 ?v1) f1) (forall ((?v2 S18)) (=> (= (f182 ?v2 ?v0) f1) (forall ((?v3 S18)) (=> (= (f182 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f41 (f21 (f22 f23 ?v2) ?v3) ?v1) f1) (= (f41 (f21 (f22 f23 ?v3) ?v2) ?v1) f1))))))))))
(assert (forall ((?v0 S16) (?v1 S21)) (= (= (f183 ?v0 ?v1) f1) (forall ((?v2 S17)) (=> (= (f41 ?v2 ?v0) f1) (forall ((?v3 S17)) (=> (= (f41 ?v3 ?v0) f1) (=> (not (= ?v2 ?v3)) (or (= (f44 (f25 (f26 f27 ?v2) ?v3) ?v1) f1) (= (f44 (f25 (f26 f27 ?v3) ?v2) ?v1) f1))))))))))
(assert (= f184 f185))
(assert (= f186 f187))
(assert (= f188 f189))
(assert (forall ((?v0 S7)) (exists ((?v1 S8) (?v2 S8)) (= ?v0 (f12 (f13 f14 ?v1) ?v2)))))
(assert (forall ((?v0 S12)) (exists ((?v1 S3) (?v2 S3)) (= ?v0 (f16 (f17 f18 ?v1) ?v2)))))
(assert (forall ((?v0 S3)) (exists ((?v1 Int) (?v2 Int)) (= ?v0 (f8 (f9 f10 ?v1) ?v2)))))
(assert (forall ((?v0 S17)) (exists ((?v1 S18) (?v2 S18)) (= ?v0 (f21 (f22 f23 ?v1) ?v2)))))
(assert (forall ((?v0 S8)) (exists ((?v1 S17) (?v2 S17)) (= ?v0 (f25 (f26 f27 ?v1) ?v2)))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S6) (?v3 S112)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f190 (f191 ?v2) ?v3)) f1) (= (f30 (f12 (f13 f14 (f192 ?v3 ?v0)) (f192 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S11) (?v3 S4)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f193 (f194 ?v2) ?v3)) f1) (= (f33 (f16 (f17 f18 (f8 ?v3 ?v0)) (f8 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 S115)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f195 (f196 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f197 ?v3 ?v0)) (f197 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S15) (?v3 S117)) (= (= (f30 (f12 (f13 f14 ?v0) ?v1) (f198 (f199 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f200 ?v3 ?v0)) (f200 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S15) (?v3 S2)) (= (= (f33 (f16 (f17 f18 ?v0) ?v1) (f201 (f202 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f6 ?v3 ?v0)) (f6 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S15) (?v3 S99)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f203 (f204 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f154 ?v3 ?v0)) (f154 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S6) (?v3 S121)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f205 (f206 ?v2) ?v3)) f1) (= (f30 (f12 (f13 f14 (f207 ?v3 ?v0)) (f207 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S11) (?v3 S123)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f208 (f209 ?v2) ?v3)) f1) (= (f33 (f16 (f17 f18 (f210 ?v3 ?v0)) (f210 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S15) (?v3 S125)) (= (= (f44 (f25 (f26 f27 ?v0) ?v1) (f211 (f212 ?v2) ?v3)) f1) (= (f37 (f8 (f9 f10 (f213 ?v3 ?v0)) (f213 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S6) (?v3 S22)) (= (= (f44 (f25 (f26 f27 ?v0) ?v1) (f214 (f215 ?v2) ?v3)) f1) (= (f30 (f12 (f13 f14 (f25 ?v3 ?v0)) (f25 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S11) (?v3 S128)) (= (= (f44 (f25 (f26 f27 ?v0) ?v1) (f216 (f217 ?v2) ?v3)) f1) (= (f33 (f16 (f17 f18 (f218 ?v3 ?v0)) (f218 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S16) (?v3 S101)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f219 (f220 ?v2) ?v3)) f1) (= (f41 (f21 (f22 f23 (f160 ?v3 ?v0)) (f160 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S16) (?v3 S98)) (= (= (f30 (f12 (f13 f14 ?v0) ?v1) (f221 (f222 ?v2) ?v3)) f1) (= (f41 (f21 (f22 f23 (f156 ?v3 ?v0)) (f156 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S16) (?v3 S100)) (= (= (f33 (f16 (f17 f18 ?v0) ?v1) (f223 (f224 ?v2) ?v3)) f1) (= (f41 (f21 (f22 f23 (f158 ?v3 ?v0)) (f158 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S21) (?v3 S133)) (= (= (f37 (f8 (f9 f10 ?v0) ?v1) (f225 (f226 ?v2) ?v3)) f1) (= (f44 (f25 (f26 f27 (f227 ?v3 ?v0)) (f227 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S21) (?v3 S135)) (= (= (f30 (f12 (f13 f14 ?v0) ?v1) (f228 (f229 ?v2) ?v3)) f1) (= (f44 (f25 (f26 f27 (f230 ?v3 ?v0)) (f230 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S21) (?v3 S137)) (= (= (f33 (f16 (f17 f18 ?v0) ?v1) (f231 (f232 ?v2) ?v3)) f1) (= (f44 (f25 (f26 f27 (f233 ?v3 ?v0)) (f233 ?v3 ?v1)) ?v2) f1))))
(assert (forall ((?v0 S24) (?v1 S8) (?v2 S8)) (=> (= (f24 (f28 ?v0 ?v1) ?v2) f1) (= (f11 (f234 ?v0) (f12 (f13 f14 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S25) (?v1 S3) (?v2 S3)) (=> (= (f19 (f31 ?v0 ?v1) ?v2) f1) (= (f15 (f235 ?v0) (f16 (f17 f18 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S27) (?v1 Int) (?v2 Int)) (=> (= (f34 (f35 ?v0 ?v1) ?v2) f1) (= (f19 (f236 f189 ?v0) (f8 (f9 f10 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (=> (= (f38 (f39 ?v0 ?v1) ?v2) f1) (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (=> (= (f20 (f42 ?v0 ?v1) ?v2) f1) (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S24) (?v1 S8) (?v2 S8)) (=> (= (f24 (f28 ?v0 ?v1) ?v2) f1) (= (f11 (f234 ?v0) (f12 (f13 f14 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S25) (?v1 S3) (?v2 S3)) (=> (= (f19 (f31 ?v0 ?v1) ?v2) f1) (= (f15 (f235 ?v0) (f16 (f17 f18 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S27) (?v1 Int) (?v2 Int)) (=> (= (f34 (f35 ?v0 ?v1) ?v2) f1) (= (f19 (f236 f189 ?v0) (f8 (f9 f10 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (=> (= (f38 (f39 ?v0 ?v1) ?v2) f1) (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (=> (= (f20 (f42 ?v0 ?v1) ?v2) f1) (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1))))
(assert (forall ((?v0 S3) (?v1 S139) (?v2 Int) (?v3 Int)) (=> (= (f37 ?v0 (f55 (f239 ?v1 ?v2) ?v3)) f1) (= (f37 ?v0 (f31 (f240 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S7) (?v1 S140) (?v2 Int) (?v3 Int)) (=> (= (f30 ?v0 (f241 (f242 ?v1 ?v2) ?v3)) f1) (= (f30 ?v0 (f243 (f244 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S12) (?v1 S143) (?v2 Int) (?v3 Int)) (=> (= (f33 ?v0 (f245 (f246 ?v1 ?v2) ?v3)) f1) (= (f33 ?v0 (f50 (f247 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S18) (?v1 S145) (?v2 Int) (?v3 Int)) (=> (= (f182 ?v0 (f248 (f249 ?v1 ?v2) ?v3)) f1) (= (f182 ?v0 (f250 (f251 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1))))
(assert (forall ((?v0 Int) (?v1 S148) (?v2 Int) (?v3 Int)) (=> (= (f179 ?v0 (f35 (f252 ?v1 ?v2) ?v3)) f1) (= (f179 ?v0 (f253 (f254 ?v1) (f8 (f9 f10 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S3) (?v1 S150) (?v2 S18) (?v3 S18)) (=> (= (f37 ?v0 (f255 (f256 ?v1 ?v2) ?v3)) f1) (= (f37 ?v0 (f257 (f258 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S7) (?v1 S153) (?v2 S18) (?v3 S18)) (=> (= (f30 ?v0 (f259 (f260 ?v1 ?v2) ?v3)) f1) (= (f30 ?v0 (f261 (f262 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S12) (?v1 S156) (?v2 S18) (?v3 S18)) (=> (= (f33 ?v0 (f263 (f264 ?v1 ?v2) ?v3)) f1) (= (f33 ?v0 (f265 (f266 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S18) (?v1 S159) (?v2 S18) (?v3 S18)) (=> (= (f182 ?v0 (f39 (f267 ?v1 ?v2) ?v3)) f1) (= (f182 ?v0 (f268 (f269 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1))))
(assert (forall ((?v0 Int) (?v1 S161) (?v2 S18) (?v3 S18)) (=> (= (f179 ?v0 (f270 (f271 ?v1 ?v2) ?v3)) f1) (= (f179 ?v0 (f272 (f273 ?v1) (f21 (f22 f23 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S3) (?v1 S164) (?v2 S17) (?v3 S17)) (=> (= (f37 ?v0 (f257 (f274 ?v1 ?v2) ?v3)) f1) (= (f37 ?v0 (f275 (f276 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S7) (?v1 S166) (?v2 S17) (?v3 S17)) (=> (= (f30 ?v0 (f261 (f277 ?v1 ?v2) ?v3)) f1) (= (f30 ?v0 (f45 (f278 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S12) (?v1 S167) (?v2 S17) (?v3 S17)) (=> (= (f33 ?v0 (f265 (f279 ?v1 ?v2) ?v3)) f1) (= (f33 ?v0 (f280 (f281 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S18) (?v1 S169) (?v2 S17) (?v3 S17)) (=> (= (f182 ?v0 (f268 (f282 ?v1 ?v2) ?v3)) f1) (= (f182 ?v0 (f283 (f284 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1))))
(assert (forall ((?v0 Int) (?v1 S171) (?v2 S17) (?v3 S17)) (=> (= (f179 ?v0 (f272 (f285 ?v1 ?v2) ?v3)) f1) (= (f179 ?v0 (f286 (f287 ?v1) (f25 (f26 f27 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S17) (?v1 S173) (?v2 S8) (?v3 S8)) (=> (= (f41 ?v0 (f288 (f289 ?v1 ?v2) ?v3)) f1) (= (f41 ?v0 (f290 (f291 ?v1) (f12 (f13 f14 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S17) (?v1 S176) (?v2 S3) (?v3 S3)) (=> (= (f41 ?v0 (f292 (f293 ?v1 ?v2) ?v3)) f1) (= (f41 ?v0 (f294 (f295 ?v1) (f16 (f17 f18 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S8) (?v1 S179) (?v2 S8) (?v3 S8)) (=> (= (f44 ?v0 (f28 (f296 ?v1 ?v2) ?v3)) f1) (= (f44 ?v0 (f297 (f298 ?v1) (f12 (f13 f14 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S8) (?v1 S181) (?v2 S3) (?v3 S3)) (=> (= (f44 ?v0 (f299 (f300 ?v1 ?v2) ?v3)) f1) (= (f44 ?v0 (f301 (f302 ?v1) (f16 (f17 f18 ?v2) ?v3))) f1))))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S30)) (let ((?v_0 (f238 f185 ?v2))) (=> (= ?v0 ?v1) (= (= (f24 ?v_0 ?v0) f1) (= (f24 ?v_0 ?v1) f1))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S29)) (let ((?v_0 (f237 f187 ?v2))) (=> (= ?v0 ?v1) (= (= (f20 ?v_0 ?v0) f1) (= (f20 ?v_0 ?v1) f1))))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S27)) (let ((?v_0 (f236 f189 ?v2))) (=> (= ?v0 ?v1) (= (= (f19 ?v_0 ?v0) f1) (= (f19 ?v_0 ?v1) f1))))))
(assert (forall ((?v0 S24) (?v1 S8) (?v2 S8)) (=> (= (f11 (f234 ?v0) (f12 (f13 f14 ?v1) ?v2)) f1) (= (f24 (f28 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S25) (?v1 S3) (?v2 S3)) (=> (= (f15 (f235 ?v0) (f16 (f17 f18 ?v1) ?v2)) f1) (= (f19 (f31 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S27) (?v1 Int) (?v2 Int)) (=> (= (f19 (f236 f189 ?v0) (f8 (f9 f10 ?v1) ?v2)) f1) (= (f34 (f35 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (=> (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1) (= (f38 (f39 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (=> (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1) (= (f20 (f42 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S27) (?v1 Int) (?v2 Int)) (= (= (f19 (f236 f189 ?v0) (f8 (f9 f10 ?v1) ?v2)) f1) (= (f34 (f35 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (= (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1) (= (f38 (f39 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (= (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1) (= (f20 (f42 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S29) (?v1 S18) (?v2 S18)) (= (= (f20 (f237 f187 ?v0) (f21 (f22 f23 ?v1) ?v2)) f1) (= (f38 (f39 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S30) (?v1 S17) (?v2 S17)) (= (= (f24 (f238 f185 ?v0) (f25 (f26 f27 ?v1) ?v2)) f1) (= (f20 (f42 ?v0 ?v1) ?v2) f1))))
(assert (forall ((?v0 S30) (?v1 S8)) (=> (= (f24 (f238 f185 ?v0) ?v1) f1) (=> (forall ((?v2 S17) (?v3 S17)) (=> (= ?v1 (f25 (f26 f27 ?v2) ?v3)) (=> (= (f20 (f42 ?v0 ?v2) ?v3) f1) false))) false))))
(assert (forall ((?v0 S29) (?v1 S17)) (=> (= (f20 (f237 f187 ?v0) ?v1) f1) (=> (forall ((?v2 S18) (?v3 S18)) (=> (= ?v1 (f21 (f22 f23 ?v2) ?v3)) (=> (= (f38 (f39 ?v0 ?v2) ?v3) f1) false))) false))))
(assert (forall ((?v0 S27) (?v1 S3)) (=> (= (f19 (f236 f189 ?v0) ?v1) f1) (=> (forall ((?v2 Int) (?v3 Int)) (=> (= ?v1 (f8 (f9 f10 ?v2) ?v3)) (=> (= (f34 (f35 ?v0 ?v2) ?v3) f1) false))) false))))
(assert (forall ((?v0 S8) (?v1 S30)) (=> (forall ((?v2 S17) (?v3 S17)) (=> (= ?v0 (f25 (f26 f27 ?v2) ?v3)) (= (f20 (f42 ?v1 ?v2) ?v3) f1))) (= (f24 (f238 f185 ?v1) ?v0) f1))))
(assert (forall ((?v0 S17) (?v1 S29)) (=> (forall ((?v2 S18) (?v3 S18)) (=> (= ?v0 (f21 (f22 f23 ?v2) ?v3)) (= (f38 (f39 ?v1 ?v2) ?v3) f1))) (= (f20 (f237 f187 ?v1) ?v0) f1))))
(assert (forall ((?v0 S3) (?v1 S27)) (=> (forall ((?v2 Int) (?v3 Int)) (=> (= ?v0 (f8 (f9 f10 ?v2) ?v3)) (= (f34 (f35 ?v1 ?v2) ?v3) f1))) (= (f19 (f236 f189 ?v1) ?v0) f1))))
(assert (forall ((?v0 S18) (?v1 S18)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) f303) f1) (< (f154 f155 ?v0) (f154 f155 ?v1)))))
(assert (= f304 (f103 (f104 f303) f303)))
(assert (= (f305 f303) f1))
(assert (forall ((?v0 S103)) (= (f306 (f163 ?v0)) f1)))
(assert (forall ((?v0 S102)) (= (f307 (f161 ?v0)) f1)))
(assert (forall ((?v0 S21)) (= (= (f308 ?v0) f1) (forall ((?v1 S17) (?v2 S17)) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))))))
(assert (forall ((?v0 S16)) (= (= (f309 ?v0) f1) (forall ((?v1 S18) (?v2 S18)) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))))))
(assert (forall ((?v0 S15)) (= (= (f310 ?v0) f1) (forall ((?v1 Int) (?v2 Int)) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))))))
(assert (= (f307 f303) f1))
(assert (forall ((?v0 S16) (?v1 S16)) (=> (= (f307 ?v0) f1) (=> (= (f307 ?v1) f1) (= (f306 (f103 (f104 ?v0) ?v1)) f1)))))
(assert (forall ((?v0 S16) (?v1 S16)) (=> (= (f305 ?v0) f1) (=> (= (f305 ?v1) f1) (= (f311 (f103 (f104 ?v0) ?v1)) f1)))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (<= (f154 f155 ?v0) (f154 f155 ?v1)) (=> (< (f154 f155 ?v2) (f154 f155 ?v3)) (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v2)) (f21 (f22 f23 ?v1) ?v3)) f304) f1)))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (< (f154 f155 ?v0) (f154 f155 ?v1)) (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v2)) (f21 (f22 f23 ?v1) ?v3)) f304) f1))))
(assert (= (f306 f304) f1))
(assert (forall ((?v0 S21) (?v1 S17)) (=> (= (f306 ?v0) f1) (=> (=> (not (= (f44 (f25 (f26 f27 ?v1) ?v1) ?v0) f1)) false) false))))
(assert (forall ((?v0 S16) (?v1 S18)) (=> (= (f307 ?v0) f1) (=> (=> (not (= (f41 (f21 (f22 f23 ?v1) ?v1) ?v0) f1)) false) false))))
(assert (forall ((?v0 S15) (?v1 Int)) (=> (= (f312 ?v0) f1) (=> (=> (not (= (f37 (f8 (f9 f10 ?v1) ?v1) ?v0) f1)) false) false))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f306 ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (=> (=> (not (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1)) false) false)))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f307 ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (=> (=> (not (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1)) false) false)))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f312 ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (=> (=> (not (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1)) false) false)))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f306 ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (not (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1))))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f307 ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (not (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1))))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f312 ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (not (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1))))))
(assert (forall ((?v0 S21) (?v1 S17)) (=> (= (f306 ?v0) f1) (not (= (f44 (f25 (f26 f27 ?v1) ?v1) ?v0) f1)))))
(assert (forall ((?v0 S16) (?v1 S18)) (=> (= (f307 ?v0) f1) (not (= (f41 (f21 (f22 f23 ?v1) ?v1) ?v0) f1)))))
(assert (forall ((?v0 S15) (?v1 Int)) (=> (= (f312 ?v0) f1) (not (= (f37 (f8 (f9 f10 ?v1) ?v1) ?v0) f1)))))
(assert (forall ((?v0 S8) (?v1 S21)) (= (= (f44 ?v0 ?v1) f1) (= (f24 ?v1 ?v0) f1))))
(assert (forall ((?v0 S17) (?v1 S16)) (= (= (f41 ?v0 ?v1) f1) (= (f20 ?v1 ?v0) f1))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17) (?v3 S17)) (let ((?v_0 (f26 f27 ?v1))) (=> (= (f311 ?v0) f1) (=> (= (f44 (f25 ?v_0 ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v3) ?v0) f1) (= (f44 (f25 ?v_0 ?v3) ?v0) f1)))))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18) (?v3 S18)) (let ((?v_0 (f22 f23 ?v1))) (=> (= (f305 ?v0) f1) (=> (= (f41 (f21 ?v_0 ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v3) ?v0) f1) (= (f41 (f21 ?v_0 ?v3) ?v0) f1)))))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int) (?v3 Int)) (let ((?v_0 (f9 f10 ?v1))) (=> (= (f313 ?v0) f1) (=> (= (f37 (f8 ?v_0 ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v3) ?v0) f1) (= (f37 (f8 ?v_0 ?v3) ?v0) f1)))))))
(assert (forall ((?v0 S21)) (= (= (f311 ?v0) f1) (forall ((?v1 S17) (?v2 S17) (?v3 S17)) (let ((?v_0 (f26 f27 ?v1))) (=> (= (f44 (f25 ?v_0 ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v3) ?v0) f1) (= (f44 (f25 ?v_0 ?v3) ?v0) f1))))))))
(assert (forall ((?v0 S16)) (= (= (f305 ?v0) f1) (forall ((?v1 S18) (?v2 S18) (?v3 S18)) (let ((?v_0 (f22 f23 ?v1))) (=> (= (f41 (f21 ?v_0 ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v3) ?v0) f1) (= (f41 (f21 ?v_0 ?v3) ?v0) f1))))))))
(assert (forall ((?v0 S15)) (= (= (f313 ?v0) f1) (forall ((?v1 Int) (?v2 Int) (?v3 Int)) (let ((?v_0 (f9 f10 ?v1))) (=> (= (f37 (f8 ?v_0 ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v3) ?v0) f1) (= (f37 (f8 ?v_0 ?v3) ?v0) f1))))))))
(assert (forall ((?v0 S21) (?v1 S103)) (=> (= (f306 ?v0) f1) (= (f306 (f173 (f174 ?v1) ?v0)) f1))))
(assert (forall ((?v0 S16) (?v1 S102)) (=> (= (f307 ?v0) f1) (= (f307 (f171 (f172 ?v1) ?v0)) f1))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (= (f308 ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2))))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (= (f309 ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2))))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (= (f310 ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2))))))
(assert (forall ((?v0 S28) (?v1 S43)) (=> (forall ((?v2 S18)) (=> (= (f38 ?v0 ?v2) f1) (= (f307 (f61 ?v1 ?v2)) f1))) (= (f306 (f62 (f63 ?v0) ?v1)) f1))))
(assert (forall ((?v0 S21)) (=> (forall ((?v1 S17) (?v2 S17)) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))) (= (f308 ?v0) f1))))
(assert (forall ((?v0 S16)) (=> (forall ((?v1 S18) (?v2 S18)) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))) (= (f309 ?v0) f1))))
(assert (forall ((?v0 S15)) (=> (forall ((?v1 Int) (?v2 Int)) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v1) ?v0) f1) (= ?v1 ?v2)))) (= (f310 ?v0) f1))))
(assert (forall ((?v0 S21)) (=> (forall ((?v1 S17) (?v2 S17) (?v3 S17)) (let ((?v_0 (f26 f27 ?v1))) (=> (= (f44 (f25 ?v_0 ?v2) ?v0) f1) (=> (= (f44 (f25 (f26 f27 ?v2) ?v3) ?v0) f1) (= (f44 (f25 ?v_0 ?v3) ?v0) f1))))) (= (f311 ?v0) f1))))
(assert (forall ((?v0 S16)) (=> (forall ((?v1 S18) (?v2 S18) (?v3 S18)) (let ((?v_0 (f22 f23 ?v1))) (=> (= (f41 (f21 ?v_0 ?v2) ?v0) f1) (=> (= (f41 (f21 (f22 f23 ?v2) ?v3) ?v0) f1) (= (f41 (f21 ?v_0 ?v3) ?v0) f1))))) (= (f305 ?v0) f1))))
(assert (forall ((?v0 S15)) (=> (forall ((?v1 Int) (?v2 Int) (?v3 Int)) (let ((?v_0 (f9 f10 ?v1))) (=> (= (f37 (f8 ?v_0 ?v2) ?v0) f1) (=> (= (f37 (f8 (f9 f10 ?v2) ?v3) ?v0) f1) (= (f37 (f8 ?v_0 ?v3) ?v0) f1))))) (= (f313 ?v0) f1))))
(assert (forall ((?v0 S21)) (= (= (f306 ?v0) f1) (forall ((?v1 S16) (?v2 S17)) (=> (= (f41 ?v2 ?v1) f1) (exists ((?v3 S17)) (and (= (f41 ?v3 ?v1) f1) (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (not (= (f41 ?v4 ?v1) f1)))))))))))
(assert (forall ((?v0 S16)) (= (= (f307 ?v0) f1) (forall ((?v1 S28) (?v2 S18)) (=> (= (f182 ?v2 ?v1) f1) (exists ((?v3 S18)) (and (= (f182 ?v3 ?v1) f1) (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (not (= (f182 ?v4 ?v1) f1)))))))))))
(assert (forall ((?v0 S6)) (= (= (f314 ?v0) f1) (forall ((?v1 S21) (?v2 S8)) (=> (= (f44 ?v2 ?v1) f1) (exists ((?v3 S8)) (and (= (f44 ?v3 ?v1) f1) (forall ((?v4 S8)) (=> (= (f30 (f12 (f13 f14 ?v4) ?v3) ?v0) f1) (not (= (f44 ?v4 ?v1) f1)))))))))))
(assert (forall ((?v0 S15)) (= (= (f312 ?v0) f1) (forall ((?v1 S26) (?v2 Int)) (=> (= (f179 ?v2 ?v1) f1) (exists ((?v3 Int)) (and (= (f179 ?v3 ?v1) f1) (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (not (= (f179 ?v4 ?v1) f1)))))))))))
(assert (forall ((?v0 S21) (?v1 S103) (?v2 S103)) (=> (forall ((?v3 S17) (?v4 S17)) (let ((?v_0 (f154 f155 (f164 ?v1 ?v3))) (?v_1 (f154 f155 (f164 ?v2 ?v4)))) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (and (<= (f154 f155 (f164 ?v1 ?v4)) ?v_0) (and (<= ?v_1 ?v_0) (< (f154 f155 (f164 ?v2 ?v3)) ?v_1)))))) (= (f306 ?v0) f1))))
(assert (forall ((?v0 S16) (?v1 S102) (?v2 S102)) (=> (forall ((?v3 S18) (?v4 S18)) (let ((?v_0 (f154 f155 (f162 ?v1 ?v3))) (?v_1 (f154 f155 (f162 ?v2 ?v4)))) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (and (<= (f154 f155 (f162 ?v1 ?v4)) ?v_0) (and (<= ?v_1 ?v_0) (< (f154 f155 (f162 ?v2 ?v3)) ?v_1)))))) (= (f307 ?v0) f1))))
(assert (forall ((?v0 S15) (?v1 S101) (?v2 S101)) (=> (forall ((?v3 Int) (?v4 Int)) (let ((?v_0 (f154 f155 (f160 ?v1 ?v3))) (?v_1 (f154 f155 (f160 ?v2 ?v4)))) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (and (<= (f154 f155 (f160 ?v1 ?v4)) ?v_0) (and (<= ?v_1 ?v_0) (< (f154 f155 (f160 ?v2 ?v3)) ?v_1)))))) (= (f312 ?v0) f1))))
(assert (forall ((?v0 S21)) (= (= (f306 ?v0) f1) (not (exists ((?v1 S19)) (forall ((?v2 S18)) (= (f44 (f25 (f26 f27 (f21 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f21 ?v1 ?v2)) ?v0) f1)))))))
(assert (forall ((?v0 S16)) (= (= (f307 ?v0) f1) (not (exists ((?v1 S102)) (forall ((?v2 S18)) (= (f41 (f21 (f22 f23 (f162 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f162 ?v1 ?v2)) ?v0) f1)))))))
(assert (forall ((?v0 S15)) (= (= (f312 ?v0) f1) (not (exists ((?v1 S99)) (forall ((?v2 S18)) (= (f37 (f8 (f9 f10 (f154 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f154 ?v1 ?v2)) ?v0) f1)))))))
(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (= (f316 (f43 ?v0)) f1))))
(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (= (f317 (f40 ?v0)) f1))))
(assert (forall ((?v0 S21) (?v1 S19)) (=> (= (f306 ?v0) f1) (=> (forall ((?v2 S18)) (=> (not (= (f44 (f25 (f26 f27 (f21 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f21 ?v1 ?v2)) ?v0) f1)) false)) false))))
(assert (forall ((?v0 S16) (?v1 S102)) (=> (= (f307 ?v0) f1) (=> (forall ((?v2 S18)) (=> (not (= (f41 (f21 (f22 f23 (f162 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f162 ?v1 ?v2)) ?v0) f1)) false)) false))))
(assert (forall ((?v0 S15) (?v1 S99)) (=> (= (f312 ?v0) f1) (=> (forall ((?v2 S18)) (=> (not (= (f37 (f8 (f9 f10 (f154 ?v1 (f160 f315 (+ (f154 f155 ?v2) 1)))) (f154 ?v1 ?v2)) ?v0) f1)) false)) false))))
(assert (forall ((?v0 S24)) (= (= (f318 ?v0) f1) (forall ((?v1 S21) (?v2 S8)) (=> (= (f44 ?v2 ?v1) f1) (exists ((?v3 S8)) (and (= (f44 ?v3 ?v1) f1) (forall ((?v4 S8)) (=> (= (f24 (f28 ?v0 ?v4) ?v3) f1) (not (= (f44 ?v4 ?v1) f1)))))))))))
(assert (forall ((?v0 S30)) (= (= (f316 ?v0) f1) (forall ((?v1 S16) (?v2 S17)) (=> (= (f41 ?v2 ?v1) f1) (exists ((?v3 S17)) (and (= (f41 ?v3 ?v1) f1) (forall ((?v4 S17)) (=> (= (f20 (f42 ?v0 ?v4) ?v3) f1) (not (= (f41 ?v4 ?v1) f1)))))))))))
(assert (= (f307 f319) f1))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (< (f154 f155 ?v0) (f154 f155 ?v1)) (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v2)) (f21 (f22 f23 ?v1) ?v3)) f320) f1))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18)) (=> (<= (f154 f155 ?v0) (f154 f155 ?v1)) (=> (<= (f154 f155 ?v2) (f154 f155 ?v3)) (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v2)) (f21 (f22 f23 ?v1) ?v3)) f320) f1)))))
(assert (forall ((?v0 S21)) (= (= (f306 ?v0) f1) (forall ((?v1 S16)) (=> (forall ((?v2 S17)) (=> (forall ((?v3 S17)) (=> (= (f44 (f25 (f26 f27 ?v3) ?v2) ?v0) f1) (= (f20 ?v1 ?v3) f1))) (= (f20 ?v1 ?v2) f1))) (forall ((?v2 S17)) (= (f20 ?v1 ?v2) f1)))))))
(assert (forall ((?v0 S16)) (= (= (f307 ?v0) f1) (forall ((?v1 S28)) (=> (forall ((?v2 S18)) (=> (forall ((?v3 S18)) (=> (= (f41 (f21 (f22 f23 ?v3) ?v2) ?v0) f1) (= (f38 ?v1 ?v3) f1))) (= (f38 ?v1 ?v2) f1))) (forall ((?v2 S18)) (= (f38 ?v1 ?v2) f1)))))))
(assert (forall ((?v0 S15)) (= (= (f312 ?v0) f1) (forall ((?v1 S26)) (=> (forall ((?v2 Int)) (=> (forall ((?v3 Int)) (=> (= (f37 (f8 (f9 f10 ?v3) ?v2) ?v0) f1) (= (f34 ?v1 ?v3) f1))) (= (f34 ?v1 ?v2) f1))) (forall ((?v2 Int)) (= (f34 ?v1 ?v2) f1)))))))
(assert (forall ((?v0 S21)) (=> (forall ((?v1 S17) (?v2 S16)) (=> (= (f41 ?v1 ?v2) f1) (exists ((?v3 S17)) (and (= (f41 ?v3 ?v2) f1) (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (not (= (f41 ?v4 ?v2) f1)))))))) (= (f306 ?v0) f1))))
(assert (forall ((?v0 S16)) (=> (forall ((?v1 S18) (?v2 S28)) (=> (= (f182 ?v1 ?v2) f1) (exists ((?v3 S18)) (and (= (f182 ?v3 ?v2) f1) (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (not (= (f182 ?v4 ?v2) f1)))))))) (= (f307 ?v0) f1))))
(assert (forall ((?v0 S6)) (=> (forall ((?v1 S8) (?v2 S21)) (=> (= (f44 ?v1 ?v2) f1) (exists ((?v3 S8)) (and (= (f44 ?v3 ?v2) f1) (forall ((?v4 S8)) (=> (= (f30 (f12 (f13 f14 ?v4) ?v3) ?v0) f1) (not (= (f44 ?v4 ?v2) f1)))))))) (= (f314 ?v0) f1))))
(assert (forall ((?v0 S15)) (=> (forall ((?v1 Int) (?v2 S26)) (=> (= (f179 ?v1 ?v2) f1) (exists ((?v3 Int)) (and (= (f179 ?v3 ?v2) f1) (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (not (= (f179 ?v4 ?v2) f1)))))))) (= (f312 ?v0) f1))))
(assert (forall ((?v0 S21) (?v1 S16) (?v2 S17)) (=> (= (f306 ?v0) f1) (=> (forall ((?v3 S17)) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (= (f20 ?v1 ?v4) f1))) (= (f20 ?v1 ?v3) f1))) (= (f20 ?v1 ?v2) f1)))))
(assert (forall ((?v0 S16) (?v1 S28) (?v2 S18)) (=> (= (f307 ?v0) f1) (=> (forall ((?v3 S18)) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (= (f38 ?v1 ?v4) f1))) (= (f38 ?v1 ?v3) f1))) (= (f38 ?v1 ?v2) f1)))))
(assert (forall ((?v0 S15) (?v1 S26) (?v2 Int)) (=> (= (f312 ?v0) f1) (=> (forall ((?v3 Int)) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (= (f34 ?v1 ?v4) f1))) (= (f34 ?v1 ?v3) f1))) (= (f34 ?v1 ?v2) f1)))))
(assert (forall ((?v0 S21) (?v1 S16) (?v2 S17)) (=> (= (f306 ?v0) f1) (=> (forall ((?v3 S17)) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (= (f20 ?v1 ?v4) f1))) (= (f20 ?v1 ?v3) f1))) (= (f20 ?v1 ?v2) f1)))))
(assert (forall ((?v0 S16) (?v1 S28) (?v2 S18)) (=> (= (f307 ?v0) f1) (=> (forall ((?v3 S18)) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (= (f38 ?v1 ?v4) f1))) (= (f38 ?v1 ?v3) f1))) (= (f38 ?v1 ?v2) f1)))))
(assert (forall ((?v0 S15) (?v1 S26) (?v2 Int)) (=> (= (f312 ?v0) f1) (=> (forall ((?v3 Int)) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (= (f34 ?v1 ?v4) f1))) (= (f34 ?v1 ?v3) f1))) (= (f34 ?v1 ?v2) f1)))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S16)) (=> (= (f306 ?v0) f1) (=> (= (f41 ?v1 ?v2) f1) (=> (forall ((?v3 S17)) (=> (= (f41 ?v3 ?v2) f1) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v3) ?v0) f1) (not (= (f41 ?v4 ?v2) f1)))) false))) false)))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S28)) (=> (= (f307 ?v0) f1) (=> (= (f182 ?v1 ?v2) f1) (=> (forall ((?v3 S18)) (=> (= (f182 ?v3 ?v2) f1) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v3) ?v0) f1) (not (= (f182 ?v4 ?v2) f1)))) false))) false)))))
(assert (forall ((?v0 S6) (?v1 S8) (?v2 S21)) (=> (= (f314 ?v0) f1) (=> (= (f44 ?v1 ?v2) f1) (=> (forall ((?v3 S8)) (=> (= (f44 ?v3 ?v2) f1) (=> (forall ((?v4 S8)) (=> (= (f30 (f12 (f13 f14 ?v4) ?v3) ?v0) f1) (not (= (f44 ?v4 ?v2) f1)))) false))) false)))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 S26)) (=> (= (f312 ?v0) f1) (=> (= (f179 ?v1 ?v2) f1) (=> (forall ((?v3 Int)) (=> (= (f179 ?v3 ?v2) f1) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v3) ?v0) f1) (not (= (f179 ?v4 ?v2) f1)))) false))) false)))))
(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (forall ((?v1 S16)) (=> (forall ((?v2 S17)) (=> (forall ((?v3 S17)) (=> (= (f44 (f25 (f26 f27 ?v3) ?v2) ?v0) f1) (= (f20 ?v1 ?v3) f1))) (= (f20 ?v1 ?v2) f1))) (forall ((?v2 S17)) (= (f20 ?v1 ?v2) f1)))))))
(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (forall ((?v1 S28)) (=> (forall ((?v2 S18)) (=> (forall ((?v3 S18)) (=> (= (f41 (f21 (f22 f23 ?v3) ?v2) ?v0) f1) (= (f38 ?v1 ?v3) f1))) (= (f38 ?v1 ?v2) f1))) (forall ((?v2 S18)) (= (f38 ?v1 ?v2) f1)))))))
(assert (forall ((?v0 S15)) (=> (= (f312 ?v0) f1) (forall ((?v1 S26)) (=> (forall ((?v2 Int)) (=> (forall ((?v3 Int)) (=> (= (f37 (f8 (f9 f10 ?v3) ?v2) ?v0) f1) (= (f34 ?v1 ?v3) f1))) (= (f34 ?v1 ?v2) f1))) (forall ((?v2 Int)) (= (f34 ?v1 ?v2) f1)))))))
(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (= (f321 (f322 ?v0)) f1))))
(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (= (f323 (f324 ?v0)) f1))))
(assert (= f303 (f325 f319)))
(assert (forall ((?v0 S18) (?v1 S18)) (= (= (f41 (f21 (f22 f23 ?v0) ?v1) (f325 f319)) f1) (< (f154 f155 ?v0) (f154 f155 ?v1)))))
(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (= (f306 (f326 ?v0)) f1))))
(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (= (f307 (f325 ?v0)) f1))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21)) (let ((?v_0 (f25 (f26 f27 ?v0) ?v1))) (=> (= (f44 ?v_0 ?v2) f1) (= (f44 ?v_0 (f326 ?v2)) f1)))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16)) (let ((?v_0 (f21 (f22 f23 ?v0) ?v1))) (=> (= (f41 ?v_0 ?v2) f1) (= (f41 ?v_0 (f325 ?v2)) f1)))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15)) (let ((?v_0 (f8 (f9 f10 ?v0) ?v1))) (=> (= (f37 ?v_0 ?v2) f1) (= (f37 ?v_0 (f327 ?v2)) f1)))))
(assert (forall ((?v0 S16)) (=> (= (f305 ?v0) f1) (= (f325 ?v0) ?v0))))
(assert (forall ((?v0 S16)) (= (f305 (f325 ?v0)) f1)))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S17)) (let ((?v_0 (f26 f27 ?v0))) (=> (= (f44 (f25 ?v_0 ?v1) ?v2) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v2) f1) (= (f44 (f25 ?v_0 ?v3) (f326 ?v2)) f1))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S18)) (let ((?v_0 (f22 f23 ?v0))) (=> (= (f41 (f21 ?v_0 ?v1) ?v2) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v2) f1) (= (f41 (f21 ?v_0 ?v3) (f325 ?v2)) f1))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 Int)) (let ((?v_0 (f9 f10 ?v0))) (=> (= (f37 (f8 ?v_0 ?v1) ?v2) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v2) f1) (= (f37 (f8 ?v_0 ?v3) (f327 ?v2)) f1))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S17)) (let ((?v_0 (f26 f27 ?v0)) (?v_1 (f326 ?v2))) (=> (= (f44 (f25 ?v_0 ?v1) ?v2) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v_1) f1) (= (f44 (f25 ?v_0 ?v3) ?v_1) f1))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S18)) (let ((?v_0 (f22 f23 ?v0)) (?v_1 (f325 ?v2))) (=> (= (f41 (f21 ?v_0 ?v1) ?v2) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v_1) f1) (= (f41 (f21 ?v_0 ?v3) ?v_1) f1))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 Int)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f327 ?v2))) (=> (= (f37 (f8 ?v_0 ?v1) ?v2) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v_1) f1) (= (f37 (f8 ?v_0 ?v3) ?v_1) f1))))))
(assert (forall ((?v0 S8) (?v1 S21)) (=> (= (f44 ?v0 ?v1) f1) (= (f44 ?v0 (f326 ?v1)) f1))))
(assert (forall ((?v0 S17) (?v1 S16)) (=> (= (f41 ?v0 ?v1) f1) (= (f41 ?v0 (f325 ?v1)) f1))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S17)) (let ((?v_1 (f26 f27 ?v0)) (?v_0 (f326 ?v2))) (=> (= (f44 (f25 ?v_1 ?v1) ?v_0) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v_0) f1) (= (f44 (f25 ?v_1 ?v3) ?v_0) f1))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S18)) (let ((?v_1 (f22 f23 ?v0)) (?v_0 (f325 ?v2))) (=> (= (f41 (f21 ?v_1 ?v1) ?v_0) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v_0) f1) (= (f41 (f21 ?v_1 ?v3) ?v_0) f1))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 Int)) (let ((?v_1 (f9 f10 ?v0)) (?v_0 (f327 ?v2))) (=> (= (f37 (f8 ?v_1 ?v1) ?v_0) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v_0) f1) (= (f37 (f8 ?v_1 ?v3) ?v_0) f1))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S17)) (let ((?v_0 (f26 f27 ?v0)) (?v_1 (f326 ?v2))) (=> (= (f44 (f25 ?v_0 ?v1) ?v_1) f1) (=> (= (f44 (f25 (f26 f27 ?v1) ?v3) ?v2) f1) (= (f44 (f25 ?v_0 ?v3) ?v_1) f1))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S18)) (let ((?v_0 (f22 f23 ?v0)) (?v_1 (f325 ?v2))) (=> (= (f41 (f21 ?v_0 ?v1) ?v_1) f1) (=> (= (f41 (f21 (f22 f23 ?v1) ?v3) ?v2) f1) (= (f41 (f21 ?v_0 ?v3) ?v_1) f1))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 Int)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f327 ?v2))) (=> (= (f37 (f8 ?v_0 ?v1) ?v_1) f1) (=> (= (f37 (f8 (f9 f10 ?v1) ?v3) ?v2) f1) (= (f37 (f8 ?v_0 ?v3) ?v_1) f1))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21)) (let ((?v_0 (f25 (f26 f27 ?v0) ?v1))) (=> (= (f44 ?v_0 (f326 ?v2)) f1) (=> (=> (= (f44 ?v_0 ?v2) f1) false) (=> (forall ((?v3 S17)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v3) (f326 ?v2)) f1) (=> (= (f44 (f25 (f26 f27 ?v3) ?v1) ?v2) f1) false))) false))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16)) (let ((?v_0 (f21 (f22 f23 ?v0) ?v1))) (=> (= (f41 ?v_0 (f325 ?v2)) f1) (=> (=> (= (f41 ?v_0 ?v2) f1) false) (=> (forall ((?v3 S18)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v3) (f325 ?v2)) f1) (=> (= (f41 (f21 (f22 f23 ?v3) ?v1) ?v2) f1) false))) false))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15)) (let ((?v_0 (f8 (f9 f10 ?v0) ?v1))) (=> (= (f37 ?v_0 (f327 ?v2)) f1) (=> (=> (= (f37 ?v_0 ?v2) f1) false) (=> (forall ((?v3 Int)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v3) (f327 ?v2)) f1) (=> (= (f37 (f8 (f9 f10 ?v3) ?v1) ?v2) f1) false))) false))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21)) (let ((?v_0 (f25 (f26 f27 ?v0) ?v1))) (=> (= (f44 ?v_0 (f326 ?v2)) f1) (=> (=> (= (f44 ?v_0 ?v2) f1) false) (=> (forall ((?v3 S17)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v3) ?v2) f1) (=> (= (f44 (f25 (f26 f27 ?v3) ?v1) (f326 ?v2)) f1) false))) false))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16)) (let ((?v_0 (f21 (f22 f23 ?v0) ?v1))) (=> (= (f41 ?v_0 (f325 ?v2)) f1) (=> (=> (= (f41 ?v_0 ?v2) f1) false) (=> (forall ((?v3 S18)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v3) ?v2) f1) (=> (= (f41 (f21 (f22 f23 ?v3) ?v1) (f325 ?v2)) f1) false))) false))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15)) (let ((?v_0 (f8 (f9 f10 ?v0) ?v1))) (=> (= (f37 ?v_0 (f327 ?v2)) f1) (=> (=> (= (f37 ?v_0 ?v2) f1) false) (=> (forall ((?v3 Int)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v3) ?v2) f1) (=> (= (f37 (f8 (f9 f10 ?v3) ?v1) (f327 ?v2)) f1) false))) false))))))
(assert (forall ((?v0 S21) (?v1 S17) (?v2 S17)) (=> (forall ((?v3 S17)) (not (= (f44 (f25 (f26 f27 ?v3) ?v3) (f326 ?v0)) f1))) (=> (= (f44 (f25 (f26 f27 ?v1) ?v2) ?v0) f1) (not (= ?v1 ?v2))))))
(assert (forall ((?v0 S16) (?v1 S18) (?v2 S18)) (=> (forall ((?v3 S18)) (not (= (f41 (f21 (f22 f23 ?v3) ?v3) (f325 ?v0)) f1))) (=> (= (f41 (f21 (f22 f23 ?v1) ?v2) ?v0) f1) (not (= ?v1 ?v2))))))
(assert (forall ((?v0 S15) (?v1 Int) (?v2 Int)) (=> (forall ((?v3 Int)) (not (= (f37 (f8 (f9 f10 ?v3) ?v3) (f327 ?v0)) f1))) (=> (= (f37 (f8 (f9 f10 ?v1) ?v2) ?v0) f1) (not (= ?v1 ?v2))))))
(assert (forall ((?v0 S21)) (=> (= (f306 ?v0) f1) (= (f321 (f328 ?v0)) f1))))
(assert (forall ((?v0 S16)) (=> (= (f307 ?v0) f1) (= (f323 (f329 ?v0)) f1))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18) (?v4 S21) (?v5 S29)) (=> (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v1)) (f21 (f22 f23 ?v2) ?v3)) (f326 ?v4)) f1) (=> (forall ((?v6 S18) (?v7 S18)) (=> (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v1)) (f21 (f22 f23 ?v6) ?v7)) ?v4) f1) (= (f38 (f39 ?v5 ?v6) ?v7) f1))) (=> (forall ((?v6 S18) (?v7 S18) (?v8 S18) (?v9 S18)) (let ((?v_0 (f21 (f22 f23 ?v6) ?v7))) (=> (= (f44 (f25 (f26 f27 (f21 (f22 f23 ?v0) ?v1)) ?v_0) (f326 ?v4)) f1) (=> (= (f44 (f25 (f26 f27 ?v_0) (f21 (f22 f23 ?v8) ?v9)) ?v4) f1) (=> (= (f38 (f39 ?v5 ?v6) ?v7) f1) (= (f38 (f39 ?v5 ?v8) ?v9) f1)))))) (= (f38 (f39 ?v5 ?v2) ?v3) f1))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S17) (?v3 S17) (?v4 S6) (?v5 S30)) (=> (= (f30 (f12 (f13 f14 (f25 (f26 f27 ?v0) ?v1)) (f25 (f26 f27 ?v2) ?v3)) (f330 ?v4)) f1) (=> (forall ((?v6 S17) (?v7 S17)) (=> (= (f30 (f12 (f13 f14 (f25 (f26 f27 ?v0) ?v1)) (f25 (f26 f27 ?v6) ?v7)) ?v4) f1) (= (f20 (f42 ?v5 ?v6) ?v7) f1))) (=> (forall ((?v6 S17) (?v7 S17) (?v8 S17) (?v9 S17)) (let ((?v_0 (f25 (f26 f27 ?v6) ?v7))) (=> (= (f30 (f12 (f13 f14 (f25 (f26 f27 ?v0) ?v1)) ?v_0) (f330 ?v4)) f1) (=> (= (f30 (f12 (f13 f14 ?v_0) (f25 (f26 f27 ?v8) ?v9)) ?v4) f1) (=> (= (f20 (f42 ?v5 ?v6) ?v7) f1) (= (f20 (f42 ?v5 ?v8) ?v9) f1)))))) (= (f20 (f42 ?v5 ?v2) ?v3) f1))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 S11) (?v5 S27)) (=> (= (f33 (f16 (f17 f18 (f8 (f9 f10 ?v0) ?v1)) (f8 (f9 f10 ?v2) ?v3)) (f331 ?v4)) f1) (=> (forall ((?v6 Int) (?v7 Int)) (=> (= (f33 (f16 (f17 f18 (f8 (f9 f10 ?v0) ?v1)) (f8 (f9 f10 ?v6) ?v7)) ?v4) f1) (= (f34 (f35 ?v5 ?v6) ?v7) f1))) (=> (forall ((?v6 Int) (?v7 Int) (?v8 Int) (?v9 Int)) (let ((?v_0 (f8 (f9 f10 ?v6) ?v7))) (=> (= (f33 (f16 (f17 f18 (f8 (f9 f10 ?v0) ?v1)) ?v_0) (f331 ?v4)) f1) (=> (= (f33 (f16 (f17 f18 ?v_0) (f8 (f9 f10 ?v8) ?v9)) ?v4) f1) (=> (= (f34 (f35 ?v5 ?v6) ?v7) f1) (= (f34 (f35 ?v5 ?v8) ?v9) f1)))))) (= (f34 (f35 ?v5 ?v2) ?v3) f1))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S16)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v1) (f326 ?v2)) f1) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v1) ?v2) f1) (= (f20 ?v3 ?v4) f1))) (=> (forall ((?v4 S17) (?v5 S17)) (=> (= (f44 (f25 (f26 f27 ?v4) ?v5) ?v2) f1) (=> (= (f44 (f25 (f26 f27 ?v5) ?v1) (f326 ?v2)) f1) (=> (= (f20 ?v3 ?v5) f1) (= (f20 ?v3 ?v4) f1))))) (= (f20 ?v3 ?v0) f1))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S28)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v1) (f325 ?v2)) f1) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v1) ?v2) f1) (= (f38 ?v3 ?v4) f1))) (=> (forall ((?v4 S18) (?v5 S18)) (=> (= (f41 (f21 (f22 f23 ?v4) ?v5) ?v2) f1) (=> (= (f41 (f21 (f22 f23 ?v5) ?v1) (f325 ?v2)) f1) (=> (= (f38 ?v3 ?v5) f1) (= (f38 ?v3 ?v4) f1))))) (= (f38 ?v3 ?v0) f1))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 S26)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v1) (f327 ?v2)) f1) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v1) ?v2) f1) (= (f34 ?v3 ?v4) f1))) (=> (forall ((?v4 Int) (?v5 Int)) (=> (= (f37 (f8 (f9 f10 ?v4) ?v5) ?v2) f1) (=> (= (f37 (f8 (f9 f10 ?v5) ?v1) (f327 ?v2)) f1) (=> (= (f34 ?v3 ?v5) f1) (= (f34 ?v3 ?v4) f1))))) (= (f34 ?v3 ?v0) f1))))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S21) (?v3 S16)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v1) (f326 ?v2)) f1) (=> (forall ((?v4 S17)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v4) ?v2) f1) (= (f20 ?v3 ?v4) f1))) (=> (forall ((?v4 S17) (?v5 S17)) (=> (= (f44 (f25 (f26 f27 ?v0) ?v4) (f326 ?v2)) f1) (=> (= (f44 (f25 (f26 f27 ?v4) ?v5) ?v2) f1) (=> (= (f20 ?v3 ?v4) f1) (= (f20 ?v3 ?v5) f1))))) (= (f20 ?v3 ?v1) f1))))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S16) (?v3 S28)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v1) (f325 ?v2)) f1) (=> (forall ((?v4 S18)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v4) ?v2) f1) (= (f38 ?v3 ?v4) f1))) (=> (forall ((?v4 S18) (?v5 S18)) (=> (= (f41 (f21 (f22 f23 ?v0) ?v4) (f325 ?v2)) f1) (=> (= (f41 (f21 (f22 f23 ?v4) ?v5) ?v2) f1) (=> (= (f38 ?v3 ?v4) f1) (= (f38 ?v3 ?v5) f1))))) (= (f38 ?v3 ?v1) f1))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S15) (?v3 S26)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v1) (f327 ?v2)) f1) (=> (forall ((?v4 Int)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v4) ?v2) f1) (= (f34 ?v3 ?v4) f1))) (=> (forall ((?v4 Int) (?v5 Int)) (=> (= (f37 (f8 (f9 f10 ?v0) ?v4) (f327 ?v2)) f1) (=> (= (f37 (f8 (f9 f10 ?v4) ?v5) ?v2) f1) (=> (= (f34 ?v3 ?v4) f1) (= (f34 ?v3 ?v5) f1))))) (= (f34 ?v3 ?v1) f1))))))
(assert (forall ((?v0 S18)) (= (f160 f315 (f154 f155 ?v0)) ?v0)))
(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f154 f155 (f160 f315 ?v0)) ?v0))))
(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f154 f155 (f160 f315 ?v0)) 0))))
(check-sat)
(exit)