; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-option :incremental false)
(set-info :status sat)
(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-fun f1 () S1)
(declare-fun f2 () S1)
(declare-fun f3 (S2 S3) S4)
(declare-fun f4 () S2)
(declare-fun f5 () S3)
(declare-fun f6 () S4)
(declare-fun f7 (S3 S5) S1)
(declare-fun f8 (S6) S5)
(declare-fun f9 () S6)
(declare-fun f10 (S7 S6) S6)
(declare-fun f11 () S7)
(declare-fun f12 (S8 S4) S4)
(declare-fun f13 () S8)
(declare-fun f14 (S10 S3) S3)
(declare-fun f15 (S11 S9) S10)
(declare-fun f16 (S12 S4) S11)
(declare-fun f17 () S12)
(declare-fun f18 (S4 S13) S1)
(declare-fun f19 () S13)
(declare-fun f20 (S4) S1)
(declare-fun f21 () S2)
(declare-fun f22 () S10)
(declare-fun f23 (S3 S9) S1)
(declare-fun f24 (S14 S9) S9)
(declare-fun f25 (S15 S4) S14)
(declare-fun f26 () S15)
(declare-fun f27 () S13)
(declare-fun f28 () S8)
(declare-fun f29 (S16 S9) S3)
(declare-fun f30 (S17 S4) S16)
(declare-fun f31 (S18 S4) S17)
(declare-fun f32 () S18)
(declare-fun f33 () S18)
(declare-fun f34 (S4 S4) S1)
(assert (not (= f1 f2)))
(assert (not (not (= (f3 f4 f5) f6))))
(assert (forall ((?v0 S3)) (=> (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f4 ?v0) f6))) ))
(assert (= (f7 f5 (f8 (f10 f11 f9))) f1))
(assert (forall ((?v0 S4)) (= (= f6 ?v0) (= ?v0 f6)) ))
(assert (= (f12 f13 f6) f6))
(assert (forall ((?v0 S4)) (= (= f6 (f12 f13 ?v0)) (= ?v0 f6)) ))
(assert (forall ((?v0 S4)) (= (= (f12 f13 ?v0) f6) (= ?v0 f6)) ))
(assert (forall ((?v0 S4) (?v1 S9) (?v2 S3)) (= (f3 f4 (f14 (f15 (f16 f17 ?v0) ?v1) ?v2)) (f3 f4 ?v2)) ))
(assert (= (f18 f6 f19) f1))
(assert (= (f20 f6) f1))
(assert (forall ((?v0 S4)) (= (= (f20 ?v0) f1) (= ?v0 f6)) ))
(assert (forall ((?v0 S3)) (=> (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f21 ?v0) f6))) ))
(assert (forall ((?v0 S3)) (=> (not (not (= (f3 f21 ?v0) f6))) (=> (not (= (f3 f4 ?v0) f6)) (not (= (f3 f4 (f14 f22 ?v0)) f6)))) ))
(assert (forall ((?v0 S4) (?v1 S4)) (= (= (f12 f13 ?v0) (f12 f13 ?v1)) (= ?v0 ?v1)) ))
(assert (forall ((?v0 S6) (?v1 S9)) (=> (forall ((?v2 S3)) (=> (= (f7 ?v2 (f8 ?v0)) f1) (not (= (f3 f21 ?v2) f6))) ) (= (exists ((?v2 S4)) (forall ((?v3 S3)) (=> (= (f7 ?v3 (f8 (f10 f11 ?v0))) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)) ) ) (exists ((?v2 S4)) (forall ((?v3 S3)) (=> (= (f7 ?v3 (f8 ?v0)) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)) ) ))) ))
(assert (forall ((?v0 S4)) (= (f18 (f12 f13 ?v0) f27) f1) ))
(assert (= (f12 f28 f6) f6))
(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9)) (= (f3 f4 (f29 (f30 (f31 f32 ?v0) ?v1) ?v2)) ?v0) ))
(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9)) (= (f3 f4 (f29 (f30 (f31 f33 ?v0) ?v1) ?v2)) ?v0) ))
(assert (= (f18 f6 f27) f1))
(assert (forall ((?v0 S3) (?v1 S4) (?v2 S9)) (=> (not (not (= (f3 f21 ?v0) f6))) (= (= (f23 ?v0 (f24 (f25 f26 ?v1) ?v2)) f1) (= (f23 (f14 f22 ?v0) ?v2) f1))) ))
(assert (forall ((?v0 S4)) (= (= (f34 (f12 f13 ?v0) f6) f1) (= (f34 ?v0 f6) f1)) ))
(assert (forall ((?v0 S4)) (= (= (f34 f6 (f12 f13 ?v0)) f1) (= (f34 f6 ?v0) f1)) ))
(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9)) (not (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5))) ))
(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9)) (not (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5))) ))
(assert (forall ((?v0 S4)) (= (f34 ?v0 ?v0) f1) ))
(assert (forall ((?v0 S4) (?v1 S4)) (or (= (f34 ?v0 ?v1) f1) (= (f34 ?v1 ?v0) f1)) ))
(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9)) (= (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ))
(assert (forall ((?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9)) (= (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ))
(assert (forall ((?v0 S4) (?v1 S4) (?v2 S4)) (=> (= (f34 ?v0 ?v1) f1) (=> (= (f34 ?v1 ?v2) f1) (= (f34 ?v0 ?v2) f1))) ))
(assert (forall ((?v0 S4) (?v1 S4)) (=> (= (f34 ?v0 ?v1) f1) (=> (= (f34 ?v1 ?v0) f1) (= ?v0 ?v1))) ))
(check-sat-assuming ( true ))