; COMMAND-LINE: --finite-model-find
; EXPECT: unsat
(set-option :incremental false)
(set-logic AUFLIA)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S3 S2) S1)
(declare-fun f4 (S4 S2) S3)
(declare-fun f5 () S4)
(declare-fun f6 (S6 S5) S1)
(declare-fun f7 (S7 S5) S6)
(declare-fun f8 () S7)
(declare-fun f9 (S9 S8) S1)
(declare-fun f10 (S10 S8) S9)
(declare-fun f11 () S10)
(declare-fun f12 () S1)
(declare-fun f13 (S12) S1)
(declare-fun f14 () S12)
(declare-fun f15 (S12) S1)
(declare-fun f16 () S2)
(declare-fun f17 (S13 S2) S2)
(declare-fun f18 (S14 S11) S13)
(declare-fun f19 () S14)
(declare-fun f20 () S5)
(declare-fun f21 (S16 S5) S5)
(declare-fun f22 (S17 S15) S16)
(declare-fun f23 () S17)
(declare-fun f24 () S8)
(declare-fun f25 (S18 S8) S8)
(declare-fun f26 (S19 S5) S18)
(declare-fun f27 () S19)
(declare-fun f28 (S20 S2) S13)
(declare-fun f29 () S20)
(declare-fun f30 (S21 S5) S16)
(declare-fun f31 () S21)
(declare-fun f32 (S22 S8) S18)
(declare-fun f33 () S22)
(declare-fun f34 () S14)
(declare-fun f35 () S17)
(declare-fun f36 () S19)
(declare-fun f37 (S24 S23) S2)
(declare-fun f38 (S25 S2) S24)
(declare-fun f39 () S25)
(declare-fun f40 (S26 S23) S1)
(declare-fun f41 (S27 Int) S26)
(declare-fun f42 () S27)
(declare-fun f43 (S28 S23) S5)
(declare-fun f44 (S29 S5) S28)
(declare-fun f45 () S29)
(declare-fun f46 (S30 S23) S8)
(declare-fun f47 (S31 S8) S30)
(declare-fun f48 () S31)
(declare-fun f49 (S2) S1)
(declare-fun f50 (S5) S1)
(declare-fun f51 (S8) S1)
(declare-fun f52 () S4)
(declare-fun f53 () S7)
(declare-fun f54 () S10)
(declare-fun f55 (S32 S2) S11)
(declare-fun f56 () S32)
(declare-fun f57 (S33 S5) S15)
(declare-fun f58 () S33)
(declare-fun f59 (S34 S8) S5)
(declare-fun f60 () S34)
(declare-fun f61 (S35 S11) S1)
(declare-fun f62 (S2) S35)
(declare-fun f63 (S36 S15) S1)
(declare-fun f64 (S5) S36)
(declare-fun f65 (S8) S6)
(declare-fun f66 (S35) S3)
(declare-fun f67 (S36) S6)
(declare-fun f68 (S6) S9)
(declare-fun f69 (S11) S3)
(declare-fun f70 (S5) S9)
(declare-fun f71 (S15) S6)
(declare-fun f72 () S13)
(declare-fun f73 () S16)
(declare-fun f74 () S18)
(declare-fun f75 () S20)
(declare-fun f76 () S21)
(declare-fun f77 () S22)
(declare-fun f78 (S37 S26) Int)
(declare-fun f79 () S37)
(assert (not (= f1 f2)))
(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f6 (f7 f8 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f9 (f10 f11 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
(assert (not (= f12 f1)))
(assert (forall ((?v0 S11) (?v1 S11)) (=> (not (= ?v0 ?v1)) (= f12 f1)) ))
(assert (exists ((?v0 S11) (?v1 S11) (?v2 S11)) (distinct ?v0 ?v1 ?v2) ))
(assert (exists ((?v0 S11) (?v1 S11) (?v2 S11)) (distinct ?v0 ?v1 ?v2) ))
(assert (= (f13 f14) f1))
(assert (= (f15 f14) f1))
(assert (forall ((?v0 S11) (?v1 S11)) (=> (not (= ?v0 ?v1)) (exists ((?v2 S11)) (distinct ?v0 ?v1 ?v2) )) ))
(assert (forall ((?v0 S11) (?v1 S2)) (not (= f16 (f17 (f18 f19 ?v0) ?v1))) ))
(assert (forall ((?v0 S15) (?v1 S5)) (not (= f20 (f21 (f22 f23 ?v0) ?v1))) ))
(assert (forall ((?v0 S5) (?v1 S8)) (not (= f24 (f25 (f26 f27 ?v0) ?v1))) ))
(assert (forall ((?v0 S11) (?v1 S2)) (not (= (f17 (f18 f19 ?v0) ?v1) f16)) ))
(assert (forall ((?v0 S15) (?v1 S5)) (not (= (f21 (f22 f23 ?v0) ?v1) f20)) ))
(assert (forall ((?v0 S5) (?v1 S8)) (not (= (f25 (f26 f27 ?v0) ?v1) f24)) ))
(assert (forall ((?v0 S2)) (= (not (= ?v0 f16)) (exists ((?v1 S11) (?v2 S2)) (= ?v0 (f17 (f18 f19 ?v1) ?v2)) )) ))
(assert (forall ((?v0 S5)) (= (not (= ?v0 f20)) (exists ((?v1 S15) (?v2 S5)) (= ?v0 (f21 (f22 f23 ?v1) ?v2)) )) ))
(assert (forall ((?v0 S8)) (= (not (= ?v0 f24)) (exists ((?v1 S5) (?v2 S8)) (= ?v0 (f25 (f26 f27 ?v1) ?v2)) )) ))
(assert (forall ((?v0 S2)) (=> (=> (= ?v0 f16) false) (=> (forall ((?v1 S11) (?v2 S2)) (=> (= ?v0 (f17 (f18 f19 ?v1) ?v2)) false) ) false)) ))
(assert (forall ((?v0 S5)) (=> (=> (= ?v0 f20) false) (=> (forall ((?v1 S15) (?v2 S5)) (=> (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false) ) false)) ))
(assert (forall ((?v0 S8)) (=> (=> (= ?v0 f24) false) (=> (forall ((?v1 S5) (?v2 S8)) (=> (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false) ) false)) ))
(assert (forall ((?v0 S2) (?v1 S11)) (not (= ?v0 (f17 (f18 f19 ?v1) ?v0))) ))
(assert (forall ((?v0 S8) (?v1 S5)) (not (= ?v0 (f25 (f26 f27 ?v1) ?v0))) ))
(assert (forall ((?v0 S5) (?v1 S15)) (not (= ?v0 (f21 (f22 f23 ?v1) ?v0))) ))
(assert (forall ((?v0 S11) (?v1 S2)) (not (= (f17 (f18 f19 ?v0) ?v1) ?v1)) ))
(assert (forall ((?v0 S5) (?v1 S8)) (not (= (f25 (f26 f27 ?v0) ?v1) ?v1)) ))
(assert (forall ((?v0 S15) (?v1 S5)) (not (= (f21 (f22 f23 ?v0) ?v1) ?v1)) ))
(assert (forall ((?v0 S11) (?v1 S2) (?v2 S11) (?v3 S2)) (= (= (f17 (f18 f19 ?v0) ?v1) (f17 (f18 f19 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8)) (= (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 S15) (?v1 S5) (?v2 S15) (?v3 S5)) (= (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ))
(assert (forall ((?v0 S11) (?v1 S2)) (let ((_let_0 (f17 (f18 f19 ?v0) ?v1))) (= (f17 (f28 f29 _let_0) f16) _let_0)) ))
(assert (forall ((?v0 S15) (?v1 S5)) (let ((_let_0 (f21 (f22 f23 ?v0) ?v1))) (= (f21 (f30 f31 _let_0) f20) _let_0)) ))
(assert (forall ((?v0 S5) (?v1 S8)) (let ((_let_0 (f25 (f26 f27 ?v0) ?v1))) (= (f25 (f32 f33 _let_0) f24) _let_0)) ))
(assert (forall ((?v0 S11)) (= (f17 (f18 f34 ?v0) f16) (f17 (f18 f19 ?v0) f16)) ))
(assert (forall ((?v0 S15)) (= (f21 (f22 f35 ?v0) f20) (f21 (f22 f23 ?v0) f20)) ))
(assert (forall ((?v0 S5)) (= (f25 (f26 f36 ?v0) f24) (f25 (f26 f27 ?v0) f24)) ))
(assert (forall ((?v0 S2) (?v1 S3)) (=> (not (= ?v0 f16)) (=> (forall ((?v2 S11)) (= (f3 ?v1 (f17 (f18 f19 ?v2) f16)) f1) ) (=> (forall ((?v2 S11) (?v3 S2)) (=> (not (= ?v3 f16)) (=> (= (f3 ?v1 ?v3) f1) (= (f3 ?v1 (f17 (f18 f19 ?v2) ?v3)) f1))) ) (= (f3 ?v1 ?v0) f1)))) ))
(assert (forall ((?v0 S5) (?v1 S6)) (=> (not (= ?v0 f20)) (=> (forall ((?v2 S15)) (= (f6 ?v1 (f21 (f22 f23 ?v2) f20)) f1) ) (=> (forall ((?v2 S15) (?v3 S5)) (=> (not (= ?v3 f20)) (=> (= (f6 ?v1 ?v3) f1) (= (f6 ?v1 (f21 (f22 f23 ?v2) ?v3)) f1))) ) (= (f6 ?v1 ?v0) f1)))) ))
(assert (forall ((?v0 S8) (?v1 S9)) (=> (not (= ?v0 f24)) (=> (forall ((?v2 S5)) (= (f9 ?v1 (f25 (f26 f27 ?v2) f24)) f1) ) (=> (forall ((?v2 S5) (?v3 S8)) (=> (not (= ?v3 f24)) (=> (= (f9 ?v1 ?v3) f1) (= (f9 ?v1 (f25 (f26 f27 ?v2) ?v3)) f1))) ) (= (f9 ?v1 ?v0) f1)))) ))
(assert (forall ((?v0 S11) (?v1 S23)) (let ((_let_0 (f17 (f18 f19 ?v0) f16))) (= (f37 (f38 f39 _let_0) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) _let_0 f16))) ))
(assert (forall ((?v0 S15) (?v1 S23)) (let ((_let_0 (f21 (f22 f23 ?v0) f20))) (= (f43 (f44 f45 _let_0) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) _let_0 f20))) ))
(assert (forall ((?v0 S5) (?v1 S23)) (let ((_let_0 (f25 (f26 f27 ?v0) f24))) (= (f46 (f47 f48 _let_0) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) _let_0 f24))) ))
(assert (forall ((?v0 S23)) (= (f37 (f38 f39 f16) ?v0) f16) ))
(assert (forall ((?v0 S23)) (= (f43 (f44 f45 f20) ?v0) f20) ))
(assert (forall ((?v0 S23)) (= (f46 (f47 f48 f24) ?v0) f24) ))
(assert (forall ((?v0 S11) (?v1 S2) (?v2 S11) (?v3 S2)) (let ((_let_0 (f18 f19 ?v0))) (let ((_let_1 (f18 f19 ?v2))) (= (f17 (f28 f29 (f17 _let_0 ?v1)) (f17 _let_1 ?v3)) (f17 _let_0 (f17 _let_1 (f17 (f28 f29 ?v1) ?v3)))))) ))
(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8)) (let ((_let_0 (f26 f27 ?v0))) (let ((_let_1 (f26 f27 ?v2))) (= (f25 (f32 f33 (f25 _let_0 ?v1)) (f25 _let_1 ?v3)) (f25 _let_0 (f25 _let_1 (f25 (f32 f33 ?v1) ?v3)))))) ))
(assert (forall ((?v0 S15) (?v1 S5) (?v2 S15) (?v3 S5)) (let ((_let_0 (f22 f23 ?v0))) (let ((_let_1 (f22 f23 ?v2))) (= (f21 (f30 f31 (f21 _let_0 ?v1)) (f21 _let_1 ?v3)) (f21 _let_0 (f21 _let_1 (f21 (f30 f31 ?v1) ?v3)))))) ))
(assert (forall ((?v0 S2)) (= (f17 (f28 f29 ?v0) f16) ?v0) ))
(assert (forall ((?v0 S5)) (= (f21 (f30 f31 ?v0) f20) ?v0) ))
(assert (forall ((?v0 S8)) (= (f25 (f32 f33 ?v0) f24) ?v0) ))
(assert (forall ((?v0 S2)) (= (f17 (f28 f29 f16) ?v0) ?v0) ))
(assert (forall ((?v0 S5)) (= (f21 (f30 f31 f20) ?v0) ?v0) ))
(assert (forall ((?v0 S8)) (= (f25 (f32 f33 f24) ?v0) ?v0) ))
(assert (forall ((?v0 S2)) (= (= ?v0 f16) (= (f49 ?v0) f1)) ))
(assert (forall ((?v0 S5)) (= (= ?v0 f20) (= (f50 ?v0) f1)) ))
(assert (forall ((?v0 S8)) (= (= ?v0 f24) (= (f51 ?v0) f1)) ))
(assert (forall ((?v0 S2)) (= (= (f49 ?v0) f1) (= ?v0 f16)) ))
(assert (forall ((?v0 S5)) (= (= (f50 ?v0) f1) (= ?v0 f20)) ))
(assert (forall ((?v0 S8)) (= (= (f51 ?v0) f1) (= ?v0 f24)) ))
(assert (= (= (f49 f16) f1) true))
(assert (= (= (f50 f20) f1) true))
(assert (= (= (f51 f24) f1) true))
(assert (forall ((?v0 S11) (?v1 S2)) (= (= (f49 (f17 (f18 f19 ?v0) ?v1)) f1) false) ))
(assert (forall ((?v0 S5) (?v1 S8)) (= (= (f51 (f25 (f26 f27 ?v0) ?v1)) f1) false) ))
(assert (forall ((?v0 S15) (?v1 S5)) (= (= (f50 (f21 (f22 f23 ?v0) ?v1)) f1) false) ))
(assert (forall ((?v0 S2)) (= (= (f3 (f4 f52 ?v0) f16) f1) (= (f49 ?v0) f1)) ))
(assert (forall ((?v0 S5)) (= (= (f6 (f7 f53 ?v0) f20) f1) (= (f50 ?v0) f1)) ))
(assert (forall ((?v0 S8)) (= (= (f9 (f10 f54 ?v0) f24) f1) (= (f51 ?v0) f1)) ))
(assert (forall ((?v0 S11) (?v1 S2)) (= (f55 f56 (f17 (f18 f19 ?v0) ?v1)) (ite (= ?v1 f16) ?v0 (f55 f56 ?v1))) ))
(assert (forall ((?v0 S15) (?v1 S5)) (= (f57 f58 (f21 (f22 f23 ?v0) ?v1)) (ite (= ?v1 f20) ?v0 (f57 f58 ?v1))) ))
(assert (forall ((?v0 S5) (?v1 S8)) (= (f59 f60 (f25 (f26 f27 ?v0) ?v1)) (ite (= ?v1 f24) ?v0 (f59 f60 ?v1))) ))
(assert (forall ((?v0 S2) (?v1 S11)) (=> (not (= ?v0 f16)) (= (f55 f56 (f17 (f18 f19 ?v1) ?v0)) (f55 f56 ?v0))) ))
(assert (forall ((?v0 S5) (?v1 S15)) (=> (not (= ?v0 f20)) (= (f57 f58 (f21 (f22 f23 ?v1) ?v0)) (f57 f58 ?v0))) ))
(assert (forall ((?v0 S8) (?v1 S5)) (=> (not (= ?v0 f24)) (= (f59 f60 (f25 (f26 f27 ?v1) ?v0)) (f59 f60 ?v0))) ))
(assert (forall ((?v0 S2) (?v1 S11)) (=> (= ?v0 f16) (= (f55 f56 (f17 (f18 f19 ?v1) ?v0)) ?v1)) ))
(assert (forall ((?v0 S5) (?v1 S15)) (=> (= ?v0 f20) (= (f57 f58 (f21 (f22 f23 ?v1) ?v0)) ?v1)) ))
(assert (forall ((?v0 S8) (?v1 S5)) (=> (= ?v0 f24) (= (f59 f60 (f25 (f26 f27 ?v1) ?v0)) ?v1)) ))
(assert (forall ((?v0 S11)) (= (= (f61 (f62 f16) ?v0) f1) false) ))
(assert (forall ((?v0 S15)) (= (= (f63 (f64 f20) ?v0) f1) false) ))
(assert (forall ((?v0 S5)) (= (= (f6 (f65 f24) ?v0) f1) false) ))
(assert (forall ((?v0 S35)) (= (= (f3 (f66 ?v0) f16) f1) false) ))
(assert (forall ((?v0 S36)) (= (= (f6 (f67 ?v0) f20) f1) false) ))
(assert (forall ((?v0 S6)) (= (= (f9 (f68 ?v0) f24) f1) false) ))
(assert (forall ((?v0 S11) (?v1 S2)) (= (f3 (f69 ?v0) (f17 (f18 f19 ?v0) ?v1)) f1) ))
(assert (forall ((?v0 S5) (?v1 S8)) (= (f9 (f70 ?v0) (f25 (f26 f27 ?v0) ?v1)) f1) ))
(assert (forall ((?v0 S15) (?v1 S5)) (= (f6 (f71 ?v0) (f21 (f22 f23 ?v0) ?v1)) f1) ))
(assert (forall ((?v0 S11) (?v1 S2) (?v2 S11)) (= (= (f61 (f62 (f17 (f18 f19 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f61 (f62 ?v1) ?v2) f1))) ))
(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5)) (= (= (f6 (f65 (f25 (f26 f27 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f6 (f65 ?v1) ?v2) f1))) ))
(assert (forall ((?v0 S15) (?v1 S5) (?v2 S15)) (= (= (f63 (f64 (f21 (f22 f23 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f63 (f64 ?v1) ?v2) f1))) ))
(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f9 (f10 f54 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f6 (f7 f53 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f52 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
(assert (= (f17 f72 f16) f16))
(assert (= (f21 f73 f20) f20))
(assert (= (f25 f74 f24) f24))
(assert (forall ((?v0 S11) (?v1 S2)) (let ((_let_0 (f18 f19 ?v0))) (= (f17 f72 (f17 _let_0 ?v1)) (ite (= ?v1 f16) f16 (f17 _let_0 (f17 f72 ?v1))))) ))
(assert (forall ((?v0 S15) (?v1 S5)) (let ((_let_0 (f22 f23 ?v0))) (= (f21 f73 (f21 _let_0 ?v1)) (ite (= ?v1 f20) f20 (f21 _let_0 (f21 f73 ?v1))))) ))
(assert (forall ((?v0 S5) (?v1 S8)) (let ((_let_0 (f26 f27 ?v0))) (= (f25 f74 (f25 _let_0 ?v1)) (ite (= ?v1 f24) f24 (f25 _let_0 (f25 f74 ?v1))))) ))
(assert (forall ((?v0 S11) (?v1 S2) (?v2 S11)) (let ((_let_0 (f69 ?v0))) (=> (= (f3 _let_0 ?v1) f1) (= (f3 _let_0 (f17 (f18 f19 ?v2) ?v1)) f1))) ))
(assert (forall ((?v0 S5) (?v1 S8) (?v2 S5)) (let ((_let_0 (f70 ?v0))) (=> (= (f9 _let_0 ?v1) f1) (= (f9 _let_0 (f25 (f26 f27 ?v2) ?v1)) f1))) ))
(assert (forall ((?v0 S15) (?v1 S5) (?v2 S15)) (let ((_let_0 (f71 ?v0))) (=> (= (f6 _let_0 ?v1) f1) (= (f6 _let_0 (f21 (f22 f23 ?v2) ?v1)) f1))) ))
(assert (forall ((?v0 S2)) (=> (not (= ?v0 f16)) (= (f17 (f28 f75 (f17 f72 ?v0)) (f17 (f18 f19 (f55 f56 ?v0)) f16)) ?v0)) ))
(assert (forall ((?v0 S5)) (=> (not (= ?v0 f20)) (= (f21 (f30 f76 (f21 f73 ?v0)) (f21 (f22 f23 (f57 f58 ?v0)) f20)) ?v0)) ))
(assert (forall ((?v0 S8)) (=> (not (= ?v0 f24)) (= (f25 (f32 f77 (f25 f74 ?v0)) (f25 (f26 f27 (f59 f60 ?v0)) f24)) ?v0)) ))
(assert (forall ((?v0 S2) (?v1 S11) (?v2 S2)) (= (= (f17 (f28 f75 ?v0) (f17 (f18 f19 ?v1) f16)) ?v2) (and (not (= ?v2 f16)) (and (= (f17 f72 ?v2) ?v0) (= (f55 f56 ?v2) ?v1)))) ))
(assert (forall ((?v0 S5) (?v1 S15) (?v2 S5)) (= (= (f21 (f30 f76 ?v0) (f21 (f22 f23 ?v1) f20)) ?v2) (and (not (= ?v2 f20)) (and (= (f21 f73 ?v2) ?v0) (= (f57 f58 ?v2) ?v1)))) ))
(assert (forall ((?v0 S8) (?v1 S5) (?v2 S8)) (= (= (f25 (f32 f77 ?v0) (f25 (f26 f27 ?v1) f24)) ?v2) (and (not (= ?v2 f24)) (and (= (f25 f74 ?v2) ?v0) (= (f59 f60 ?v2) ?v1)))) ))
(assert (= f11 f54))
(assert (= f8 f53))
(assert (= f5 f52))
(assert (forall ((?v0 S8) (?v1 S8)) (= (= (f9 (f10 f54 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
(assert (forall ((?v0 S5) (?v1 S5)) (= (= (f6 (f7 f53 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
(assert (forall ((?v0 S2) (?v1 S2)) (= (= (f3 (f4 f52 ?v0) ?v1) f1) (= ?v0 ?v1)) ))
(assert (forall ((?v0 S8)) (= (= (f9 (f10 f54 ?v0) ?v0) f1) true) ))
(assert (forall ((?v0 S5)) (= (= (f6 (f7 f53 ?v0) ?v0) f1) true) ))
(assert (forall ((?v0 S2)) (= (= (f3 (f4 f52 ?v0) ?v0) f1) true) ))
(assert (= f54 f11))
(assert (= f53 f8))
(assert (= f52 f5))
(assert (forall ((?v0 S11) (?v1 S2)) (= (= (f3 (f69 ?v0) ?v1) f1) (or (exists ((?v2 S11) (?v3 S2)) (and (= ?v0 ?v2) (= ?v1 (f17 (f18 f19 ?v2) ?v3))) ) (exists ((?v2 S11) (?v3 S2) (?v4 S11)) (and (= ?v0 ?v2) (and (= ?v1 (f17 (f18 f19 ?v4) ?v3)) (= (f3 (f69 ?v2) ?v3) f1))) ))) ))
(assert (forall ((?v0 S5) (?v1 S8)) (= (= (f9 (f70 ?v0) ?v1) f1) (or (exists ((?v2 S5) (?v3 S8)) (and (= ?v0 ?v2) (= ?v1 (f25 (f26 f27 ?v2) ?v3))) ) (exists ((?v2 S5) (?v3 S8) (?v4 S5)) (and (= ?v0 ?v2) (and (= ?v1 (f25 (f26 f27 ?v4) ?v3)) (= (f9 (f70 ?v2) ?v3) f1))) ))) ))
(assert (forall ((?v0 S15) (?v1 S5)) (= (= (f6 (f71 ?v0) ?v1) f1) (or (exists ((?v2 S15) (?v3 S5)) (and (= ?v0 ?v2) (= ?v1 (f21 (f22 f23 ?v2) ?v3))) ) (exists ((?v2 S15) (?v3 S5) (?v4 S15)) (and (= ?v0 ?v2) (and (= ?v1 (f21 (f22 f23 ?v4) ?v3)) (= (f6 (f71 ?v2) ?v3) f1))) ))) ))
(assert (forall ((?v0 S2) (?v1 S11)) (= (f55 f56 (f17 (f28 f75 ?v0) (f17 (f18 f19 ?v1) f16))) ?v1) ))
(assert (forall ((?v0 S5) (?v1 S15)) (= (f57 f58 (f21 (f30 f76 ?v0) (f21 (f22 f23 ?v1) f20))) ?v1) ))
(assert (forall ((?v0 S8) (?v1 S5)) (= (f59 f60 (f25 (f32 f77 ?v0) (f25 (f26 f27 ?v1) f24))) ?v1) ))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8)) (let ((_let_0 (f32 f77 ?v0))) (=> (= (f25 _let_0 ?v1) ?v2) (=> (= ?v3 (f25 (f32 f77 ?v1) ?v4)) (= (f25 _let_0 ?v3) (f25 (f32 f77 ?v2) ?v4))))) ))
(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5)) (let ((_let_0 (f30 f76 ?v0))) (=> (= (f21 _let_0 ?v1) ?v2) (=> (= ?v3 (f21 (f30 f76 ?v1) ?v4)) (= (f21 _let_0 ?v3) (f21 (f30 f76 ?v2) ?v4))))) ))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2)) (let ((_let_0 (f28 f75 ?v0))) (=> (= (f17 _let_0 ?v1) ?v2) (=> (= ?v3 (f17 (f28 f75 ?v1) ?v4)) (= (f17 _let_0 ?v3) (f17 (f28 f75 ?v2) ?v4))))) ))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8)) (= (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v2) ?v1)) (= ?v0 ?v2)) ))
(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (= (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v2) ?v1)) (= ?v0 ?v2)) ))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (= (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v2) ?v1)) (= ?v0 ?v2)) ))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8)) (let ((_let_0 (f32 f77 ?v0))) (= (= (f25 _let_0 ?v1) (f25 _let_0 ?v2)) (= ?v1 ?v2))) ))
(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (let ((_let_0 (f30 f76 ?v0))) (= (= (f21 _let_0 ?v1) (f21 _let_0 ?v2)) (= ?v1 ?v2))) ))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (let ((_let_0 (f28 f75 ?v0))) (= (= (f17 _let_0 ?v1) (f17 _let_0 ?v2)) (= ?v1 ?v2))) ))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8)) (= (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v2) ?v3)) (exists ((?v4 S8)) (let ((_let_0 (f32 f77 ?v4))) (or (and (= ?v0 (f25 (f32 f77 ?v2) ?v4)) (= (f25 _let_0 ?v1) ?v3)) (and (= (f25 (f32 f77 ?v0) ?v4) ?v2) (= ?v1 (f25 _let_0 ?v3))))) )) ))
(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5)) (= (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v2) ?v3)) (exists ((?v4 S5)) (let ((_let_0 (f30 f76 ?v4))) (or (and (= ?v0 (f21 (f30 f76 ?v2) ?v4)) (= (f21 _let_0 ?v1) ?v3)) (and (= (f21 (f30 f76 ?v0) ?v4) ?v2) (= ?v1 (f21 _let_0 ?v3))))) )) ))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2)) (= (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v2) ?v3)) (exists ((?v4 S2)) (let ((_let_0 (f28 f75 ?v4))) (or (and (= ?v0 (f17 (f28 f75 ?v2) ?v4)) (= (f17 _let_0 ?v1) ?v3)) (and (= (f17 (f28 f75 ?v0) ?v4) ?v2) (= ?v1 (f17 _let_0 ?v3))))) )) ))
(assert (forall ((?v0 S8) (?v1 S8) (?v2 S8)) (let ((_let_0 (f32 f77 ?v0))) (= (f25 (f32 f77 (f25 _let_0 ?v1)) ?v2) (f25 _let_0 (f25 (f32 f77 ?v1) ?v2)))) ))
(assert (forall ((?v0 S5) (?v1 S5) (?v2 S5)) (let ((_let_0 (f30 f76 ?v0))) (= (f21 (f30 f76 (f21 _let_0 ?v1)) ?v2) (f21 _let_0 (f21 (f30 f76 ?v1) ?v2)))) ))
(assert (forall ((?v0 S2) (?v1 S2) (?v2 S2)) (let ((_let_0 (f28 f75 ?v0))) (= (f17 (f28 f75 (f17 _let_0 ?v1)) ?v2) (f17 _let_0 (f17 (f28 f75 ?v1) ?v2)))) ))
(assert (forall ((?v0 S11) (?v1 S2) (?v2 S2)) (let ((_let_0 (f18 f19 ?v0))) (= (f17 (f28 f75 (f17 _let_0 ?v1)) ?v2) (f17 _let_0 (f17 (f28 f75 ?v1) ?v2)))) ))
(assert (forall ((?v0 S5) (?v1 S8) (?v2 S8)) (let ((_let_0 (f26 f27 ?v0))) (= (f25 (f32 f77 (f25 _let_0 ?v1)) ?v2) (f25 _let_0 (f25 (f32 f77 ?v1) ?v2)))) ))
(assert (forall ((?v0 S15) (?v1 S5) (?v2 S5)) (let ((_let_0 (f22 f23 ?v0))) (= (f21 (f30 f76 (f21 _let_0 ?v1)) ?v2) (f21 _let_0 (f21 (f30 f76 ?v1) ?v2)))) ))
(assert (forall ((?v0 S11) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2)) (let ((_let_0 (f18 f19 ?v0))) (=> (= (f17 _let_0 ?v1) ?v2) (=> (= ?v3 (f17 (f28 f75 ?v1) ?v4)) (= (f17 _let_0 ?v3) (f17 (f28 f75 ?v2) ?v4))))) ))
(assert (forall ((?v0 S5) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8)) (let ((_let_0 (f26 f27 ?v0))) (=> (= (f25 _let_0 ?v1) ?v2) (=> (= ?v3 (f25 (f32 f77 ?v1) ?v4)) (= (f25 _let_0 ?v3) (f25 (f32 f77 ?v2) ?v4))))) ))
(assert (forall ((?v0 S15) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5)) (let ((_let_0 (f22 f23 ?v0))) (=> (= (f21 _let_0 ?v1) ?v2) (=> (= ?v3 (f21 (f30 f76 ?v1) ?v4)) (= (f21 _let_0 ?v3) (f21 (f30 f76 ?v2) ?v4))))) ))
(assert (forall ((?v0 S2)) (= (f17 (f28 f75 f16) ?v0) ?v0) ))
(assert (forall ((?v0 S5)) (= (f21 (f30 f76 f20) ?v0) ?v0) ))
(assert (forall ((?v0 S8)) (= (f25 (f32 f77 f24) ?v0) ?v0) ))
(assert (forall ((?v0 S2) (?v1 S2)) (= (= f16 (f17 (f28 f75 ?v0) ?v1)) (and (= ?v0 f16) (= ?v1 f16))) ))
(assert (forall ((?v0 S5) (?v1 S5)) (= (= f20 (f21 (f30 f76 ?v0) ?v1)) (and (= ?v0 f20) (= ?v1 f20))) ))
(assert (forall ((?v0 S8) (?v1 S8)) (= (= f24 (f25 (f32 f77 ?v0) ?v1)) (and (= ?v0 f24) (= ?v1 f24))) ))
(assert (forall ((?v0 S2)) (= (f17 (f28 f75 ?v0) f16) ?v0) ))
(assert (forall ((?v0 S5)) (= (f21 (f30 f76 ?v0) f20) ?v0) ))
(assert (forall ((?v0 S8)) (= (f25 (f32 f77 ?v0) f24) ?v0) ))
(assert (forall ((?v0 S2) (?v1 S2)) (= (= ?v0 (f17 (f28 f75 ?v0) ?v1)) (= ?v1 f16)) ))
(assert (forall ((?v0 S5) (?v1 S5)) (= (= ?v0 (f21 (f30 f76 ?v0) ?v1)) (= ?v1 f20)) ))
(assert (forall ((?v0 S8) (?v1 S8)) (= (= ?v0 (f25 (f32 f77 ?v0) ?v1)) (= ?v1 f24)) ))
(assert (forall ((?v0 S2) (?v1 S2)) (= (= ?v0 (f17 (f28 f75 ?v1) ?v0)) (= ?v1 f16)) ))
(assert (forall ((?v0 S5) (?v1 S5)) (= (= ?v0 (f21 (f30 f76 ?v1) ?v0)) (= ?v1 f20)) ))
(assert (forall ((?v0 S8) (?v1 S8)) (= (= ?v0 (f25 (f32 f77 ?v1) ?v0)) (= ?v1 f24)) ))
(assert (forall ((?v0 S26)) (= (f41 f42 (f78 f79 ?v0)) ?v0) ))
(assert (forall ((?v0 Int)) (=> (<= 0 ?v0) (= (f78 f79 (f41 f42 ?v0)) ?v0)) ))
(assert (forall ((?v0 Int)) (=> (< ?v0 0) (= (f78 f79 (f41 f42 ?v0)) 0)) ))
(check-sat-assuming ( true ))