path: root/test/regress/regress1/quantifiers/infer-arith-trigger-eq.smt2

; COMMAND-LINE: --infer-arith-trigger-eq
; EXPECT: unsat
(set-info :smt-lib-version 2.6)
(set-logic UFLIA)
(set-info :status unsat)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 () S2)
(declare-fun f4 () S3)
(declare-fun f5 (S4 S2) S3)
(declare-fun f6 () S4)
(declare-fun f7 () S2)
(declare-fun f8 () S5)
(declare-fun f9 (S6 S3) Int)
(declare-fun f10 () S6)
(declare-fun f11 (S7 S5) S5)
(declare-fun f12 (S8 S2) S7)
(declare-fun f13 () S8)
(declare-fun f14 () S2)
(declare-fun f15 (S9 Int) S3)
(declare-fun f16 () S9)
(declare-fun f17 () S5)
(declare-fun f18 (S10 S5) S7)
(declare-fun f19 () S10)
(declare-fun f20 () S5)
(declare-fun f21 () S10)
(declare-fun f22 (S11 S3) S5)
(declare-fun f23 (S12 S5) S11)
(declare-fun f24 () S12)
(declare-fun f25 () S5)
(declare-fun f26 () S2)
(declare-fun f27 (S13 S2) S2)
(declare-fun f28 (S14 S5) S13)
(declare-fun f29 () S14)
(declare-fun f30 (S15 S3) S3)
(declare-fun f31 (S16 S17) S15)
(declare-fun f32 () S16)
(declare-fun f33 () S17)
(declare-fun f34 () S3)
(declare-fun f35 (S19 S18) S18)
(declare-fun f36 (S20 S21) S19)
(declare-fun f37 () S20)
(declare-fun f38 () S21)
(declare-fun f39 () S18)
(declare-fun f40 (S23 S22) S22)
(declare-fun f41 (S24 S25) S23)
(declare-fun f42 () S24)
(declare-fun f43 () S25)
(declare-fun f44 () S22)
(declare-fun f45 (S26 S22) S13)
(declare-fun f46 () S26)
(declare-fun f47 (S27 Int) Int)
(declare-fun f48 (S28 S18) S27)
(declare-fun f49 () S28)
(declare-fun f50 (S29 S18) S19)
(declare-fun f51 () S29)
(declare-fun f52 (S30 S3) S18)
(declare-fun f53 (S31 S18) S30)
(declare-fun f54 () S31)
(declare-fun f55 (S32 Int) S6)
(declare-fun f56 () S32)
(declare-fun f57 () S29)
(declare-fun f58 (S33 Int) S27)
(declare-fun f59 () S33)
(declare-fun f60 (S34 S3) S15)
(declare-fun f61 () S34)
(declare-fun f62 () S34)
(declare-fun f63 (S35 S22) S23)
(declare-fun f64 () S35)
(declare-fun f65 () S35)
(declare-fun f66 (S36 S2) S13)
(declare-fun f67 () S36)
(declare-fun f68 () S36)
(declare-fun f69 (S37 S18) S3)
(declare-fun f70 () S37)
(declare-fun f71 (S38 S22) S3)
(declare-fun f72 () S38)
(declare-fun f73 (S39 S3) S22)
(declare-fun f74 (S40 S22) S39)
(declare-fun f75 () S40)
(declare-fun f76 (S41 S3) S2)
(declare-fun f77 (S42 S2) S41)
(declare-fun f78 () S42)
(declare-fun f79 (S44 S17) S17)
(declare-fun f80 (S45 S43) S44)
(declare-fun f81 () S45)
(declare-fun f82 (S46 S3) S43)
(declare-fun f83 (S47 S43) S46)
(declare-fun f84 () S47)
(declare-fun f85 (S48 S3) S17)
(declare-fun f86 (S49 S17) S48)
(declare-fun f87 () S49)
(declare-fun f88 () S34)
(declare-fun f89 () S37)
(declare-fun f90 () S38)
(declare-fun f91 () S4)
(declare-fun f92 (S50 S17) S44)
(declare-fun f93 () S50)
(declare-fun f94 (S51 S21) S21)
(declare-fun f95 (S52 S21) S51)
(declare-fun f96 () S52)
(declare-fun f97 () S50)
(declare-fun f98 () S52)
(declare-fun f99 (S53 S17) S3)
(declare-fun f100 () S53)
(declare-fun f101 (S54 Int) S19)
(declare-fun f102 () S54)
(declare-fun f103 (S55 S2) S23)
(declare-fun f104 () S55)
(declare-fun f105 (S56 S18) S51)
(declare-fun f106 () S56)
(declare-fun f107 (S57 S3) S44)
(declare-fun f108 () S57)
(declare-fun f109 (S58 S25) S25)
(declare-fun f110 (S59 S22) S58)
(declare-fun f111 () S59)
(declare-fun f112 () S27)
(declare-fun f113 (S7) S1)
(declare-fun f114 () S36)
(declare-fun f115 (S60 S2) S1)
(declare-fun f116 (S61 S5) S4)
(declare-fun f117 () S61)
(declare-fun f118 (S62 Int) S37)
(declare-fun f119 () S62)
(declare-fun f120 (S63 S2) S38)
(declare-fun f121 () S63)
(assert (not (= f1 f2)))
(assert (not (exists ((?v0 S2)) (let ((?v_0 (= ?v0 f3)) (?v_1 (f5 f6 f7))) (and (=> ?v_0 (and (= f4 ?v_1) (forall ((?v1 S5)) (let ((?v_2 (= ?v1 f8))) (or ?v_2 (or (and ?v_2 (< 0 (f9 f10 f4))) (or ?v_2 (= (f11 (f12 f13 f14) ?v1) f8)))))))) (=> (not ?v_0) (and (= (f15 f16 (+ (+ (f9 f10 (f5 f6 ?v0)) (f9 f10 f4)) 1)) ?v_1) (forall ((?v1 S5)) (let ((?v_3 (= ?v1 f8))) (or ?v_3 (or (and ?v_3 (< 0 (f9 f10 f4))) (or ?v_3 (= (f11 (f12 f13 f14) ?v1) (f11 (f12 f13 ?v0) ?v1))))))))))))))
(assert (not (= f17 f8)))
(assert (not (= (f11 (f18 f19 f20) (f11 (f18 f21 f17) (f11 (f12 f13 f14) f17))) f8)))
(assert (not (= f20 f8)))
(assert (= (f15 f16 (+ (ite (= f14 f3) 0 (+ (f9 f10 (f5 f6 f14)) 1)) (f9 f10 f4))) (f5 f6 f7)))
(assert (forall ((?v0 S5)) (= (f11 (f12 f13 f7) ?v0) (f11 (f18 f21 (f22 (f23 f24 ?v0) f4)) (f11 (f18 f19 f20) (f11 (f18 f21 ?v0) (f11 (f12 f13 f14) ?v0)))))))
(assert (not (= f7 f3)))
(assert (= f25 f8))
(assert (not (forall ((?v0 S5)) (=> (not (= ?v0 f8)) (= (f11 (f12 f13 f26) ?v0) f8)))))
(assert (=> (not (forall ((?v0 S5)) (=> (not (= ?v0 f8)) (= (f11 (f12 f13 f7) ?v0) f8)))) (exists ((?v0 S3) (?v1 S5) (?v2 S2)) (and (not (= ?v1 f8)) (and (= (f15 f16 (+ (+ (ite (= ?v2 f3) 0 (+ (f9 f10 (f5 f6 ?v2)) 1)) (f9 f10 ?v0)) 1)) (ite (= f7 f3) (f15 f16 0) (f15 f16 (+ (f9 f10 (f5 f6 f7)) 1)))) (forall ((?v3 S5)) (= (f11 (f12 f13 f7) ?v3) (f11 (f18 f21 (f22 (f23 f24 ?v3) ?v0)) (f11 (f12 f13 (f27 (f28 f29 ?v1) ?v2)) ?v3)))))))))
(assert (forall ((?v0 S3)) (= (f30 (f31 f32 f33) ?v0) f34)))
(assert (forall ((?v0 S18)) (= (f35 (f36 f37 f38) ?v0) f39)))
(assert (forall ((?v0 S22)) (= (f40 (f41 f42 f43) ?v0) f44)))
(assert (forall ((?v0 S2)) (= (f27 (f45 f46 f44) ?v0) f3)))
(assert (forall ((?v0 Int)) (= (f47 (f48 f49 f39) ?v0) 0)))
(assert (forall ((?v0 S5)) (= (f11 (f12 f13 f3) ?v0) f8)))
(assert (forall ((?v0 S18) (?v1 S18)) (let ((?v_0 (f15 f16 2))) (= (= (f35 (f50 f51 (f52 (f53 f54 ?v0) ?v_0)) (f52 (f53 f54 ?v1) ?v_0)) f39) (and (= ?v0 f39) (= ?v1 f39))))))
(assert (forall ((?v0 Int) (?v1 Int)) (let ((?v_0 (f15 f16 2))) (= (= (+ (f9 (f55 f56 ?v0) ?v_0) (f9 (f55 f56 ?v1) ?v_0)) 0) (and (= ?v0 0) (= ?v1 0))))))
(assert (forall ((?v0 S18) (?v1 S18)) (= (= (f35 (f50 f51 (f35 (f50 f57 ?v0) ?v0)) (f35 (f50 f57 ?v1) ?v1)) f39) (and (= ?v0 f39) (= ?v1 f39)))))
(assert (forall ((?v0 Int) (?v1 Int)) (= (= (+ (f47 (f58 f59 ?v0) ?v0) (f47 (f58 f59 ?v1) ?v1)) 0) (and (= ?v0 0) (= ?v1 0)))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18) (?v3 S18) (?v4 S18)) (let ((?v_0 (f50 f57 ?v0))) (=> (not (= ?v0 f39)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f35 (f50 f51 ?v1) (f35 ?v_0 ?v3)) (f35 (f50 f51 ?v2) (f35 ?v_0 ?v4)))))))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3) (?v3 S3) (?v4 S3)) (let ((?v_0 (f60 f62 ?v0))) (=> (not (= ?v0 f34)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f30 (f60 f61 ?v1) (f30 ?v_0 ?v3)) (f30 (f60 f61 ?v2) (f30 ?v_0 ?v4)))))))))
(assert (forall ((?v0 S22) (?v1 S22) (?v2 S22) (?v3 S22) (?v4 S22)) (let ((?v_0 (f63 f65 ?v0))) (=> (not (= ?v0 f44)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f40 (f63 f64 ?v1) (f40 ?v_0 ?v3)) (f40 (f63 f64 ?v2) (f40 ?v_0 ?v4)))))))))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2)) (let ((?v_0 (f66 f68 ?v0))) (=> (not (= ?v0 f3)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f27 (f66 f67 ?v1) (f27 ?v_0 ?v3)) (f27 (f66 f67 ?v2) (f27 ?v_0 ?v4)))))))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int) (?v3 Int) (?v4 Int)) (let ((?v_0 (f58 f59 ?v0))) (=> (not (= ?v0 0)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (+ ?v1 (f47 ?v_0 ?v3)) (+ ?v2 (f47 ?v_0 ?v4)))))))))
(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5)) (let ((?v_0 (f18 f21 ?v0))) (=> (not (= ?v0 f8)) (=> (and (= ?v1 ?v2) (not (= ?v3 ?v4))) (not (= (f11 (f18 f19 ?v1) (f11 ?v_0 ?v3)) (f11 (f18 f19 ?v2) (f11 ?v_0 ?v4)))))))))
(assert (not (forall ((?v0 S5)) (=> (not (= ?v0 f8)) (= (f11 (f12 f13 (f27 (f28 f29 f25) f7)) ?v0) f8)))))
(assert (forall ((?v0 S18)) (= (= (f48 f49 ?v0) (f48 f49 f39)) (= ?v0 f39))))
(assert (= (f69 f70 f39) (f15 f16 0)))
(assert (= (f71 f72 f44) (f15 f16 0)))
(assert (= (f5 f6 f3) (f15 f16 0)))
(assert (forall ((?v0 S18) (?v1 S3) (?v2 Int)) (= (f47 (f48 f49 (f52 (f53 f54 ?v0) ?v1)) ?v2) (f9 (f55 f56 (f47 (f48 f49 ?v0) ?v2)) ?v1))))
(assert (forall ((?v0 S22) (?v1 S3) (?v2 S2)) (= (f27 (f45 f46 (f73 (f74 f75 ?v0) ?v1)) ?v2) (f76 (f77 f78 (f27 (f45 f46 ?v0) ?v2)) ?v1))))
(assert (forall ((?v0 S43) (?v1 S3) (?v2 S17)) (= (f79 (f80 f81 (f82 (f83 f84 ?v0) ?v1)) ?v2) (f85 (f86 f87 (f79 (f80 f81 ?v0) ?v2)) ?v1))))
(assert (forall ((?v0 S17) (?v1 S3) (?v2 S3)) (= (f30 (f31 f32 (f85 (f86 f87 ?v0) ?v1)) ?v2) (f30 (f60 f88 (f30 (f31 f32 ?v0) ?v2)) ?v1))))
(assert (forall ((?v0 S2) (?v1 S3) (?v2 S5)) (= (f11 (f12 f13 (f76 (f77 f78 ?v0) ?v1)) ?v2) (f22 (f23 f24 (f11 (f12 f13 ?v0) ?v2)) ?v1))))
(assert (forall ((?v0 S18)) (= (f69 f89 ?v0) (ite (= ?v0 f39) (f15 f16 0) (f15 f16 (+ (f9 f10 (f69 f70 ?v0)) 1))))))
(assert (forall ((?v0 S22)) (= (f71 f90 ?v0) (ite (= ?v0 f44) (f15 f16 0) (f15 f16 (+ (f9 f10 (f71 f72 ?v0)) 1))))))
(assert (forall ((?v0 S2)) (= (f5 f91 ?v0) (ite (= ?v0 f3) (f15 f16 0) (f15 f16 (+ (f9 f10 (f5 f6 ?v0)) 1))))))
(assert (forall ((?v0 S22) (?v1 S22) (?v2 S2)) (= (f27 (f45 f46 (f40 (f63 f64 ?v0) ?v1)) ?v2) (f27 (f66 f67 (f27 (f45 f46 ?v0) ?v2)) (f27 (f45 f46 ?v1) ?v2)))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S3)) (= (f30 (f31 f32 (f79 (f92 f93 ?v0) ?v1)) ?v2) (f30 (f60 f61 (f30 (f31 f32 ?v0) ?v2)) (f30 (f31 f32 ?v1) ?v2)))))
(assert (forall ((?v0 S21) (?v1 S21) (?v2 S18)) (= (f35 (f36 f37 (f94 (f95 f96 ?v0) ?v1)) ?v2) (f35 (f50 f51 (f35 (f36 f37 ?v0) ?v2)) (f35 (f36 f37 ?v1) ?v2)))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 Int)) (= (f47 (f48 f49 (f35 (f50 f51 ?v0) ?v1)) ?v2) (+ (f47 (f48 f49 ?v0) ?v2) (f47 (f48 f49 ?v1) ?v2)))))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S5)) (= (f11 (f12 f13 (f27 (f66 f67 ?v0) ?v1)) ?v2) (f11 (f18 f19 (f11 (f12 f13 ?v0) ?v2)) (f11 (f12 f13 ?v1) ?v2)))))
(assert (forall ((?v0 S22) (?v1 S22) (?v2 S2)) (= (f27 (f45 f46 (f40 (f63 f65 ?v0) ?v1)) ?v2) (f27 (f66 f68 (f27 (f45 f46 ?v0) ?v2)) (f27 (f45 f46 ?v1) ?v2)))))
(assert (forall ((?v0 S17) (?v1 S17) (?v2 S3)) (= (f30 (f31 f32 (f79 (f92 f97 ?v0) ?v1)) ?v2) (f30 (f60 f62 (f30 (f31 f32 ?v0) ?v2)) (f30 (f31 f32 ?v1) ?v2)))))
(assert (forall ((?v0 S21) (?v1 S21) (?v2 S18)) (= (f35 (f36 f37 (f94 (f95 f98 ?v0) ?v1)) ?v2) (f35 (f50 f57 (f35 (f36 f37 ?v0) ?v2)) (f35 (f36 f37 ?v1) ?v2)))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 Int)) (= (f47 (f48 f49 (f35 (f50 f57 ?v0) ?v1)) ?v2) (f47 (f58 f59 (f47 (f48 f49 ?v0) ?v2)) (f47 (f48 f49 ?v1) ?v2)))))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S5)) (= (f11 (f12 f13 (f27 (f66 f68 ?v0) ?v1)) ?v2) (f11 (f18 f21 (f11 (f12 f13 ?v0) ?v2)) (f11 (f12 f13 ?v1) ?v2)))))
(assert (forall ((?v0 S17) (?v1 S3)) (<= (f9 f10 (f99 f100 (f85 (f86 f87 ?v0) ?v1))) (f47 (f58 f59 (f9 f10 (f99 f100 ?v0))) (f9 f10 ?v1)))))
(assert (forall ((?v0 S2) (?v1 S3)) (<= (f9 f10 (f5 f6 (f76 (f77 f78 ?v0) ?v1))) (f47 (f58 f59 (f9 f10 (f5 f6 ?v0))) (f9 f10 ?v1)))))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (= (f27 (f66 f68 (f27 (f66 f67 ?v0) ?v1)) ?v2) (f27 (f66 f67 (f27 (f66 f68 ?v0) ?v2)) (f27 (f66 f68 ?v1) ?v2)))))
(assert (forall ((?v0 S18) (?v1 S18) (?v2 S18)) (= (f35 (f50 f57 (f35 (f50 f51 ?v0) ?v1)) ?v2) (f35 (f50 f51 (f35 (f50 f57 ?v0) ?v2)) (f35 (f50 f57 ?v1) ?v2)))))
(assert (forall ((?v0 Int) (?v1 S18) (?v2 Int) (?v3 S18)) (= (= (f35 (f101 f102 ?v0) ?v1) (f35 (f101 f102 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
(assert (forall ((?v0 S2) (?v1 S22) (?v2 S2) (?v3 S22)) (= (= (f40 (f103 f104 ?v0) ?v1) (f40 (f103 f104 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
(assert (forall ((?v0 S5) (?v1 S2) (?v2 S5) (?v3 S2)) (= (= (f27 (f28 f29 ?v0) ?v1) (f27 (f28 f29 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3)))))
(assert (forall ((?v0 S2) (?v1 S22) (?v2 S2) (?v3 S22)) (= (f40 (f63 f64 (f40 (f103 f104 ?v0) ?v1)) (f40 (f103 f104 ?v2) ?v3)) (f40 (f103 f104 (f27 (f66 f67 ?v0) ?v2)) (f40 (f63 f64 ?v1) ?v3)))))
(assert (forall ((?v0 S18) (?v1 S21) (?v2 S18) (?v3 S21)) (= (f94 (f95 f96 (f94 (f105 f106 ?v0) ?v1)) (f94 (f105 f106 ?v2) ?v3)) (f94 (f105 f106 (f35 (f50 f51 ?v0) ?v2)) (f94 (f95 f96 ?v1) ?v3)))))
(assert (forall ((?v0 Int) (?v1 S18) (?v2 Int) (?v3 S18)) (= (f35 (f50 f51 (f35 (f101 f102 ?v0) ?v1)) (f35 (f101 f102 ?v2) ?v3)) (f35 (f101 f102 (+ ?v0 ?v2)) (f35 (f50 f51 ?v1) ?v3)))))
(assert (forall ((?v0 S5) (?v1 S2) (?v2 S5) (?v3 S2)) (= (f27 (f66 f67 (f27 (f28 f29 ?v0) ?v1)) (f27 (f28 f29 ?v2) ?v3)) (f27 (f28 f29 (f11 (f18 f19 ?v0) ?v2)) (f27 (f66 f67 ?v1) ?v3)))))
(assert (forall ((?v0 Int) (?v1 S3) (?v2 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 (f55 f56 (f9 ?v_0 ?v1)) ?v2) (f9 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2))))))))
(assert (forall ((?v0 S2) (?v1 S3) (?v2 S3)) (let ((?v_0 (f77 f78 ?v0))) (= (f76 (f77 f78 (f76 ?v_0 ?v1)) ?v2) (f76 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2))))))))
(assert (forall ((?v0 S17) (?v1 S3) (?v2 S3)) (let ((?v_0 (f86 f87 ?v0))) (= (f85 (f86 f87 (f85 ?v_0 ?v1)) ?v2) (f85 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2))))))))
(assert (forall ((?v0 S5) (?v1 S3) (?v2 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 (f23 f24 (f22 ?v_0 ?v1)) ?v2) (f22 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2))))))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 (f60 f88 (f30 ?v_0 ?v1)) ?v2) (f30 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2))))))))
(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f9 (f55 f56 (f9 ?v_0 ?v1)) (f15 f16 2))))))
(assert (forall ((?v0 S2) (?v1 S3)) (let ((?v_0 (f77 f78 ?v0))) (= (f76 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f76 (f77 f78 (f76 ?v_0 ?v1)) (f15 f16 2))))))
(assert (forall ((?v0 S17) (?v1 S3)) (let ((?v_0 (f86 f87 ?v0))) (= (f85 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f85 (f86 f87 (f85 ?v_0 ?v1)) (f15 f16 2))))))
(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f22 (f23 f24 (f22 ?v_0 ?v1)) (f15 f16 2))))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (* 2 (f9 f10 ?v1)))) (f30 (f60 f88 (f30 ?v_0 ?v1)) (f15 f16 2))))))
(assert (forall ((?v0 Int) (?v1 S18)) (<= (f9 f10 (f69 f70 (f35 (f101 f102 ?v0) ?v1))) (+ (f9 f10 (f69 f70 ?v1)) 1))))
(assert (forall ((?v0 S2) (?v1 S22)) (<= (f9 f10 (f71 f72 (f40 (f103 f104 ?v0) ?v1))) (+ (f9 f10 (f71 f72 ?v1)) 1))))
(assert (forall ((?v0 S5) (?v1 S2)) (<= (f9 f10 (f5 f6 (f27 (f28 f29 ?v0) ?v1))) (+ (f9 f10 (f5 f6 ?v1)) 1))))
(assert (forall ((?v0 S18)) (= (f35 (f50 f51 ?v0) f39) ?v0)))
(assert (forall ((?v0 S22)) (= (f40 (f63 f64 ?v0) f44) ?v0)))
(assert (forall ((?v0 S2)) (= (f27 (f66 f67 ?v0) f3) ?v0)))
(assert (forall ((?v0 S18)) (= (f35 (f50 f51 f39) ?v0) ?v0)))
(assert (forall ((?v0 S22)) (= (f40 (f63 f64 f44) ?v0) ?v0)))
(assert (forall ((?v0 S2)) (= (f27 (f66 f67 f3) ?v0) ?v0)))
(assert (forall ((?v0 S18)) (= (f35 (f50 f57 ?v0) f39) f39)))
(assert (forall ((?v0 S22)) (= (f40 (f63 f65 ?v0) f44) f44)))
(assert (forall ((?v0 S2)) (= (f27 (f66 f68 ?v0) f3) f3)))
(assert (forall ((?v0 S18)) (= (f35 (f50 f57 f39) ?v0) f39)))
(assert (forall ((?v0 S22)) (= (f40 (f63 f65 f44) ?v0) f44)))
(assert (forall ((?v0 S2)) (= (f27 (f66 f68 f3) ?v0) f3)))
(assert (forall ((?v0 S18) (?v1 S18)) (let ((?v_0 (f69 f70 ?v1))) (=> (< (f9 f10 (f69 f70 ?v0)) (f9 f10 ?v_0)) (= (f69 f70 (f35 (f50 f51 ?v1) ?v0)) ?v_0)))))
(assert (forall ((?v0 S2) (?v1 S2)) (let ((?v_0 (f5 f6 ?v1))) (=> (< (f9 f10 (f5 f6 ?v0)) (f9 f10 ?v_0)) (= (f5 f6 (f27 (f66 f67 ?v1) ?v0)) ?v_0)))))
(assert (forall ((?v0 S18) (?v1 S18)) (let ((?v_0 (f69 f70 ?v1))) (=> (< (f9 f10 (f69 f70 ?v0)) (f9 f10 ?v_0)) (= (f69 f70 (f35 (f50 f51 ?v0) ?v1)) ?v_0)))))
(assert (forall ((?v0 S2) (?v1 S2)) (let ((?v_0 (f5 f6 ?v1))) (=> (< (f9 f10 (f5 f6 ?v0)) (f9 f10 ?v_0)) (= (f5 f6 (f27 (f66 f67 ?v0) ?v1)) ?v_0)))))
(assert (forall ((?v0 S18) (?v1 S3) (?v2 S18)) (let ((?v_0 (f9 f10 ?v1))) (=> (<= (f9 f10 (f69 f70 ?v0)) ?v_0) (=> (<= (f9 f10 (f69 f70 ?v2)) ?v_0) (<= (f9 f10 (f69 f70 (f35 (f50 f51 ?v0) ?v2))) ?v_0))))))
(assert (forall ((?v0 S2) (?v1 S3) (?v2 S2)) (let ((?v_0 (f9 f10 ?v1))) (=> (<= (f9 f10 (f5 f6 ?v0)) ?v_0) (=> (<= (f9 f10 (f5 f6 ?v2)) ?v_0) (<= (f9 f10 (f5 f6 (f27 (f66 f67 ?v0) ?v2))) ?v_0))))))
(assert (forall ((?v0 S18) (?v1 S3) (?v2 S18)) (let ((?v_0 (f9 f10 ?v1))) (=> (< (f9 f10 (f69 f70 ?v0)) ?v_0) (=> (< (f9 f10 (f69 f70 ?v2)) ?v_0) (< (f9 f10 (f69 f70 (f35 (f50 f51 ?v0) ?v2))) ?v_0))))))
(assert (forall ((?v0 S2) (?v1 S3) (?v2 S2)) (let ((?v_0 (f9 f10 ?v1))) (=> (< (f9 f10 (f5 f6 ?v0)) ?v_0) (=> (< (f9 f10 (f5 f6 ?v2)) ?v_0) (< (f9 f10 (f5 f6 (f27 (f66 f67 ?v0) ?v2))) ?v_0))))))
(assert (forall ((?v0 S18) (?v1 S18)) (let ((?v_0 (f69 f70 ?v1)) (?v_1 (f69 f70 ?v0))) (<= (f9 f10 (f69 f70 (f35 (f50 f51 ?v0) ?v1))) (f9 f10 (ite (<= (f9 f10 ?v_1) (f9 f10 ?v_0)) ?v_0 ?v_1))))))
(assert (forall ((?v0 S2) (?v1 S2)) (let ((?v_0 (f5 f6 ?v1)) (?v_1 (f5 f6 ?v0))) (<= (f9 f10 (f5 f6 (f27 (f66 f67 ?v0) ?v1))) (f9 f10 (ite (<= (f9 f10 ?v_1) (f9 f10 ?v_0)) ?v_0 ?v_1))))))


(assert (forall ((?v0 S3)) (= (f30 (f60 f88 ?v0) (f15 f16 3)) (f30 (f60 f62 (f30 (f60 f62 ?v0) ?v0)) ?v0))))
(assert (forall ((?v0 S5)) (= (f22 (f23 f24 ?v0) (f15 f16 3)) (f11 (f18 f21 (f11 (f18 f21 ?v0) ?v0)) ?v0))))
(assert (forall ((?v0 Int)) (= (f9 (f55 f56 ?v0) (f15 f16 3)) (f47 (f58 f59 (f47 (f58 f59 ?v0) ?v0)) ?v0))))
(assert (forall ((?v0 S3)) (= (f30 (f60 f88 ?v0) (f15 f16 2)) (f30 (f60 f62 ?v0) ?v0))))
(assert (forall ((?v0 S5)) (= (f22 (f23 f24 ?v0) (f15 f16 2)) (f11 (f18 f21 ?v0) ?v0))))
(assert (forall ((?v0 Int)) (= (f9 (f55 f56 ?v0) (f15 f16 2)) (f47 (f58 f59 ?v0) ?v0))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f30 (f60 f62 ?v0) (f30 ?v_0 ?v1))))))
(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f11 (f18 f21 ?v0) (f22 ?v_0 ?v1))))))
(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f47 (f58 f59 ?v0) (f9 ?v_0 ?v1))))))
(assert (forall ((?v0 S3)) (= (f30 (f60 f62 ?v0) ?v0) (f30 (f60 f88 ?v0) (f15 f16 2)))))
(assert (forall ((?v0 S5)) (= (f11 (f18 f21 ?v0) ?v0) (f22 (f23 f24 ?v0) (f15 f16 2)))))
(assert (forall ((?v0 Int)) (= (f47 (f58 f59 ?v0) ?v0) (f9 (f55 f56 ?v0) (f15 f16 2)))))
(assert (forall ((?v0 S2)) (=> (not (= (f113 (f12 f13 ?v0)) f1)) (<= 2 (f9 f10 (f5 f91 ?v0))))))
(assert (forall ((?v0 S5) (?v1 S2) (?v2 S2)) (let ((?v_0 (f28 f29 ?v0))) (= (f27 (f66 f114 (f27 ?v_0 ?v1)) ?v2) (f27 (f66 f67 (f27 ?v_0 f3)) (f27 (f66 f68 ?v2) (f27 (f66 f114 ?v1) ?v2)))))))
(assert (forall ((?v0 S60) (?v1 S2)) (=> (= (f115 ?v0 f3) f1) (=> (forall ((?v2 S5) (?v3 S2)) (=> (= (f115 ?v0 ?v3) f1) (= (f115 ?v0 (f27 (f28 f29 ?v2) ?v3)) f1))) (= (f115 ?v0 ?v1) f1)))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f9 f10 ?v1)) (?v_1 (f9 f10 ?v0)) (?v_2 (f60 f88 ?v2))) (=> (<= ?v_1 ?v_0) (= (f30 ?v_2 (f15 f16 (- (+ ?v_0 1) ?v_1))) (f30 (f60 f62 (f30 ?v_2 (f15 f16 (- ?v_0 ?v_1)))) ?v2))))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S5)) (let ((?v_0 (f9 f10 ?v1)) (?v_1 (f9 f10 ?v0)) (?v_2 (f23 f24 ?v2))) (=> (<= ?v_1 ?v_0) (= (f22 ?v_2 (f15 f16 (- (+ ?v_0 1) ?v_1))) (f11 (f18 f21 (f22 ?v_2 (f15 f16 (- ?v_0 ?v_1)))) ?v2))))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 Int)) (let ((?v_0 (f9 f10 ?v1)) (?v_1 (f9 f10 ?v0)) (?v_2 (f55 f56 ?v2))) (=> (<= ?v_1 ?v_0) (= (f9 ?v_2 (f15 f16 (- (+ ?v_0 1) ?v_1))) (f47 (f58 f59 (f9 ?v_2 (f15 f16 (- ?v_0 ?v_1)))) ?v2))))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f60 f88 ?v1))) (=> (< 0 ?v_0) (= (f30 (f60 f62 (f30 ?v_1 (f15 f16 (- ?v_0 1)))) ?v1) (f30 ?v_1 ?v0))))))
(assert (forall ((?v0 S3) (?v1 S5)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f23 f24 ?v1))) (=> (< 0 ?v_0) (= (f11 (f18 f21 (f22 ?v_1 (f15 f16 (- ?v_0 1)))) ?v1) (f22 ?v_1 ?v0))))))
(assert (forall ((?v0 S3) (?v1 Int)) (let ((?v_0 (f9 f10 ?v0)) (?v_1 (f55 f56 ?v1))) (=> (< 0 ?v_0) (= (f47 (f58 f59 (f9 ?v_1 (f15 f16 (- ?v_0 1)))) ?v1) (f9 ?v_1 ?v0))))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (= (f30 (f60 f88 (f30 (f60 f62 ?v0) ?v1)) ?v2) (f30 (f60 f62 (f30 (f60 f88 ?v0) ?v2)) (f30 (f60 f88 ?v1) ?v2)))))
(assert (forall ((?v0 S5) (?v1 S5) (?v2 S3)) (= (f22 (f23 f24 (f11 (f18 f21 ?v0) ?v1)) ?v2) (f11 (f18 f21 (f22 (f23 f24 ?v0) ?v2)) (f22 (f23 f24 ?v1) ?v2)))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 S3)) (= (f9 (f55 f56 (f47 (f58 f59 ?v0) ?v1)) ?v2) (f47 (f58 f59 (f9 (f55 f56 ?v0) ?v2)) (f9 (f55 f56 ?v1) ?v2)))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f30 (f60 f88 ?v0) ?v1))) (= (f30 (f60 f62 ?v_0) ?v0) (f30 (f60 f62 ?v0) ?v_0)))))
(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f22 (f23 f24 ?v0) ?v1))) (= (f11 (f18 f21 ?v_0) ?v0) (f11 (f18 f21 ?v0) ?v_0)))))
(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f9 (f55 f56 ?v0) ?v1))) (= (f47 (f58 f59 ?v_0) ?v0) (f47 (f58 f59 ?v0) ?v_0)))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (+ (f9 f10 ?v1) (f9 f10 ?v2)))) (f30 (f60 f62 (f30 ?v_0 ?v1)) (f30 ?v_0 ?v2))))))
(assert (forall ((?v0 S5) (?v1 S3) (?v2 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (+ (f9 f10 ?v1) (f9 f10 ?v2)))) (f11 (f18 f21 (f22 ?v_0 ?v1)) (f22 ?v_0 ?v2))))))
(assert (forall ((?v0 Int) (?v1 S3) (?v2 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (+ (f9 f10 ?v1) (f9 f10 ?v2)))) (f47 (f58 f59 (f9 ?v_0 ?v1)) (f9 ?v_0 ?v2))))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f30 (f60 f62 (f30 ?v_0 ?v1)) ?v0)))))
(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f11 (f18 f21 (f22 ?v_0 ?v1)) ?v0)))))
(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f47 (f58 f59 (f9 ?v_0 ?v1)) ?v0)))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f30 (f60 f62 ?v0) (f30 ?v_0 ?v1))))))
(assert (forall ((?v0 S5) (?v1 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f11 (f18 f21 ?v0) (f22 ?v_0 ?v1))))))
(assert (forall ((?v0 Int) (?v1 S3)) (let ((?v_0 (f55 f56 ?v0))) (= (f9 ?v_0 (f15 f16 (+ (f9 f10 ?v1) 1))) (f47 (f58 f59 ?v0) (f9 ?v_0 ?v1))))))
(assert (forall ((?v0 S2) (?v1 S5)) (= (= (f11 (f12 f13 ?v0) ?v1) f8) (or (= ?v0 f3) (not (= (f5 (f116 f117 ?v1) ?v0) (f15 f16 0)))))))
(assert (forall ((?v0 S18) (?v1 Int)) (= (= (f47 (f48 f49 ?v0) ?v1) 0) (or (= ?v0 f39) (not (= (f69 (f118 f119 ?v1) ?v0) (f15 f16 0)))))))
(assert (forall ((?v0 S22) (?v1 S2)) (= (= (f27 (f45 f46 ?v0) ?v1) f3) (or (= ?v0 f44) (not (= (f71 (f120 f121 ?v1) ?v0) (f15 f16 0)))))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 ?v1) (ite (= ?v1 (f15 f16 0)) (f15 f16 1) (f15 f16 (f47 (f58 f59 (f9 f10 ?v0)) (f9 f10 (f30 ?v_0 (f15 f16 (- (f9 f10 ?v1) 1)))))))))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f15 f16 0)) (?v_2 (f9 f10 ?v0)) (?v_1 (f9 f10 ?v1))) (= (f15 f16 (f47 (f58 f59 ?v_2) ?v_1)) (ite (= ?v0 ?v_0) ?v_0 (f15 f16 (+ ?v_1 (f47 (f58 f59 (f9 f10 (f15 f16 (- ?v_2 1)))) ?v_1))))))))
(assert (forall ((?v0 S3)) (let ((?v_0 (f9 f10 ?v0))) (= (f15 f16 (* ?v_0 2)) (f15 f16 (+ ?v_0 ?v_0))))))
(assert (forall ((?v0 S3)) (let ((?v_0 (f9 f10 ?v0))) (= (f15 f16 (* 2 ?v_0)) (f15 f16 (+ ?v_0 ?v_0))))))
(assert (forall ((?v0 S2)) (= (f27 (f66 f114 f3) ?v0) f3)))
(assert (forall ((?v0 S2) (?v1 S2)) (<= (f9 f10 (f5 f6 (f27 (f66 f114 ?v0) ?v1))) (f47 (f58 f59 (f9 f10 (f5 f6 ?v0))) (f9 f10 (f5 f6 ?v1))))))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S5)) (= (f11 (f12 f13 (f27 (f66 f114 ?v0) ?v1)) ?v2) (f11 (f12 f13 ?v0) (f11 (f12 f13 ?v1) ?v2)))))
(assert (forall ((?v0 S3)) (= (f30 (f60 f88 ?v0) (f15 f16 1)) ?v0)))
(assert (forall ((?v0 S5)) (= (f22 (f23 f24 ?v0) (f15 f16 1)) ?v0)))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f60 f88 ?v0))) (= (f30 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2)))) (f30 (f60 f88 (f30 ?v_0 ?v1)) ?v2)))))
(assert (forall ((?v0 S5) (?v1 S3) (?v2 S3)) (let ((?v_0 (f23 f24 ?v0))) (= (f22 ?v_0 (f15 f16 (f47 (f58 f59 (f9 f10 ?v1)) (f9 f10 ?v2)))) (f22 (f23 f24 (f22 ?v_0 ?v1)) ?v2)))))
(assert (forall ((?v0 S2) (?v1 S5)) (=> (not (= ?v0 f3)) (<= (f9 f10 (f5 (f116 f117 ?v1) ?v0)) (f9 f10 (f5 f6 ?v0))))))
(assert (forall ((?v0 S3)) (= (f9 (f55 f56 0) (f15 f16 (+ (f9 f10 ?v0) 1))) 0)))
(assert (forall ((?v0 S3)) (= (f22 (f23 f24 f8) (f15 f16 (+ (f9 f10 ?v0) 1))) f8)))
(assert (forall ((?v0 S3)) (= (f76 (f77 f78 f3) (f15 f16 (+ (f9 f10 ?v0) 1))) f3)))
(assert (forall ((?v0 S3)) (= (f30 (f60 f88 f34) (f15 f16 (+ (f9 f10 ?v0) 1))) f34)))
(assert (forall ((?v0 Int) (?v1 S3)) (= (= (f9 (f55 f56 ?v0) ?v1) 0) (and (= ?v0 0) (not (= ?v1 (f15 f16 0)))))))
(assert (forall ((?v0 S5) (?v1 S3)) (= (= (f22 (f23 f24 ?v0) ?v1) f8) (and (= ?v0 f8) (not (= ?v1 (f15 f16 0)))))))
(assert (forall ((?v0 S2) (?v1 S3)) (= (= (f76 (f77 f78 ?v0) ?v1) f3) (and (= ?v0 f3) (not (= ?v1 (f15 f16 0)))))))
(assert (forall ((?v0 S3) (?v1 S3)) (= (= (f30 (f60 f88 ?v0) ?v1) f34) (and (= ?v0 f34) (not (= ?v1 (f15 f16 0)))))))
(assert (forall ((?v0 Int) (?v1 S3)) (=> (not (= ?v0 0)) (not (= (f9 (f55 f56 ?v0) ?v1) 0)))))
(assert (forall ((?v0 S5) (?v1 S3)) (=> (not (= ?v0 f8)) (not (= (f22 (f23 f24 ?v0) ?v1) f8)))))
(assert (forall ((?v0 S2) (?v1 S3)) (=> (not (= ?v0 f3)) (not (= (f76 (f77 f78 ?v0) ?v1) f3)))))
(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (= (f11 (f18 f21 (f11 (f18 f19 ?v0) ?v1)) ?v2) (f11 (f18 f19 (f11 (f18 f21 ?v0) ?v2)) (f11 (f18 f21 ?v1) ?v2)))))
(assert (forall ((?v0 Int) (?v1 Int) (?v2 Int)) (= (f47 (f58 f59 (+ ?v0 ?v1)) ?v2) (+ (f47 (f58 f59 ?v0) ?v2) (f47 (f58 f59 ?v1) ?v2)))))
(assert (forall ((?v0 S3) (?v1 S3)) (= (< 0 (f9 f10 (f30 (f60 f88 ?v0) ?v1))) (or (< 0 (f9 f10 ?v0)) (= ?v1 (f15 f16 0))))))
(assert (forall ((?v0 S3)) (let ((?v_0 (f15 f16 (+ 0 1)))) (= (f30 (f60 f88 ?v_0) ?v0) ?v_0))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (f15 f16 (+ 0 1)))) (= (= (f30 (f60 f88 ?v0) ?v1) ?v_0) (or (= ?v1 (f15 f16 0)) (= ?v0 ?v_0))))))
(assert (forall ((?v0 S3) (?v1 S3) (?v2 S3)) (let ((?v_0 (f60 f88 ?v0))) (=> (< 0 (f9 f10 ?v0)) (=> (< (f9 f10 (f30 ?v_0 ?v1)) (f9 f10 (f30 ?v_0 ?v2))) (< (f9 f10 ?v1) (f9 f10 ?v2)))))))
(assert (forall ((?v0 S3) (?v1 S3)) (let ((?v_0 (+ 0 1))) (=> (<= ?v_0 (f9 f10 ?v0)) (<= ?v_0 (f9 f10 (f30 (f60 f88 ?v0) ?v1)))))))
(assert (forall ((?v0 Int)) (let ((?v_0 (f47 f112 ?v0))) (= (f47 (f58 f59 ?v_0) ?v_0) (f47 (f58 f59 ?v0) ?v0)))))
(assert (forall ((?v0 Int) (?v1 Int)) (= (f47 f112 (f47 (f58 f59 ?v0) ?v1)) (f47 (f58 f59 (f47 f112 ?v0)) (f47 f112 ?v1)))))
(assert (forall ((?v0 Int) (?v1 Int)) (=> (= (f47 (f58 f59 ?v0) ?v1) 0) (or (= ?v0 0) (= ?v1 0)))))
(assert (forall ((?v0 S5) (?v1 S5)) (=> (= (f11 (f18 f21 ?v0) ?v1) f8) (or (= ?v0 f8) (= ?v1 f8)))))
(assert (forall ((?v0 S2) (?v1 S2)) (=> (= (f27 (f66 f68 ?v0) ?v1) f3) (or (= ?v0 f3) (= ?v1 f3)))))
(assert (forall ((?v0 Int) (?v1 Int)) (=> (not (= ?v0 0)) (=> (not (= ?v1 0)) (not (= (f47 (f58 f59 ?v0) ?v1) 0))))))
(assert (forall ((?v0 S5) (?v1 S5)) (=> (not (= ?v0 f8)) (=> (not (= ?v1 f8)) (not (= (f11 (f18 f21 ?v0) ?v1) f8))))))
(assert (forall ((?v0 S2) (?v1 S2)) (=> (not (= ?v0 f3)) (=> (not (= ?v1 f3)) (not (= (f27 (f66 f68 ?v0) ?v1) f3))))))
(assert (forall ((?v0 Int) (?v1 Int)) (= (= (f47 (f58 f59 ?v0) ?v1) 0) (or (= ?v0 0) (= ?v1 0)))))
(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f11 (f18 f21 ?v0) ?v1) f8) (or (= ?v0 f8) (= ?v1 f8)))))
(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f27 (f66 f68 ?v0) ?v1) f3) (or (= ?v0 f3) (= ?v1 f3)))))
(assert (forall ((?v0 Int)) (= (* ?v0 0) 0)))
(assert (forall ((?v0 S5)) (= (f11 (f18 f21 ?v0) f8) f8)))
(assert (forall ((?v0 S2)) (= (f27 (f66 f68 ?v0) f3) f3)))
(assert (forall ((?v0 S3)) (= (f15 f16 (f9 f10 ?v0)) ?v0)))
(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f9 f10 (f15 f16 ?v0)) ?v0))))
(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f9 f10 (f15 f16 ?v0)) 0))))
(check-sat)
(exit)