diff options
Diffstat (limited to 'test/regress/regress0/fmf')
4 files changed, 378 insertions, 347 deletions
diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt deleted file mode 100644 index ab1e41360..000000000 --- a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt +++ /dev/null @@ -1,263 +0,0 @@ -; COMMAND-LINE: --finite-model-find -; EXPECT: unsat -(benchmark Isabelle -:logic AUFLIA -:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11 S12 S13 S14 S15 S16 S17 S18 S19 S20 S21 S22 S23 S24 S25 S26 S27 S28 S29 S30 S31 S32 S33 S34 S35 S36 S37) -:extrafuns ( - (f1 S1) - (f2 S1) - (f3 S3 S2 S1) - (f4 S4 S2 S3) - (f5 S4) - (f6 S6 S5 S1) - (f7 S7 S5 S6) - (f8 S7) - (f9 S9 S8 S1) - (f10 S10 S8 S9) - (f11 S10) - (f12 S1) - (f13 S12 S1) - (f14 S12) - (f15 S12 S1) - (f16 S2) - (f17 S13 S2 S2) - (f18 S14 S11 S13) - (f19 S14) - (f20 S5) - (f21 S16 S5 S5) - (f22 S17 S15 S16) - (f23 S17) - (f24 S8) - (f25 S18 S8 S8) - (f26 S19 S5 S18) - (f27 S19) - (f28 S20 S2 S13) - (f29 S20) - (f30 S21 S5 S16) - (f31 S21) - (f32 S22 S8 S18) - (f33 S22) - (f34 S14) - (f35 S17) - (f36 S19) - (f37 S24 S23 S2) - (f38 S25 S2 S24) - (f39 S25) - (f40 S26 S23 S1) - (f41 S27 Int S26) - (f42 S27) - (f43 S28 S23 S5) - (f44 S29 S5 S28) - (f45 S29) - (f46 S30 S23 S8) - (f47 S31 S8 S30) - (f48 S31) - (f49 S2 S1) - (f50 S5 S1) - (f51 S8 S1) - (f52 S4) - (f53 S7) - (f54 S10) - (f55 S32 S2 S11) - (f56 S32) - (f57 S33 S5 S15) - (f58 S33) - (f59 S34 S8 S5) - (f60 S34) - (f61 S35 S11 S1) - (f62 S2 S35) - (f63 S36 S15 S1) - (f64 S5 S36) - (f65 S8 S6) - (f66 S35 S3) - (f67 S36 S6) - (f68 S6 S9) - (f69 S11 S3) - (f70 S5 S9) - (f71 S15 S6) - (f72 S13) - (f73 S16) - (f74 S18) - (f75 S20) - (f76 S21) - (f77 S22) - (f78 S37 S26 Int) - (f79 S37) -) -:assumption (not (= f1 f2)) -:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f5 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (forall (?v0 S5) (?v1 S5) (iff (= (f6 (f7 f8 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (forall (?v0 S8) (?v1 S8) (iff (= (f9 (f10 f11 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (not (= f12 f1)) -:assumption (forall (?v0 S11) (?v1 S11) (implies (not (= ?v0 ?v1)) (= f12 f1))) -:assumption (exists (?v0 S11) (?v1 S11) (?v2 S11) (distinct ?v0 ?v1 ?v2)) -:assumption (exists (?v0 S11) (?v1 S11) (?v2 S11) (distinct ?v0 ?v1 ?v2) ) -:assumption (= (f13 f14) f1) -:assumption (= (f15 f14) f1) -:assumption (forall (?v0 S11) (?v1 S11) (implies (not (= ?v0 ?v1)) (exists (?v2 S11) (distinct ?v0 ?v1 ?v2))) ) -:assumption (forall (?v0 S11) (?v1 S2) (not (= f16 (f17 (f18 f19 ?v0) ?v1))) ) -:assumption (forall (?v0 S15) (?v1 S5) (not (= f20 (f21 (f22 f23 ?v0) ?v1))) ) -:assumption (forall (?v0 S5) (?v1 S8) (not (= f24 (f25 (f26 f27 ?v0) ?v1))) ) -:assumption (forall (?v0 S11) (?v1 S2) (not (= (f17 (f18 f19 ?v0) ?v1) f16)) ) -:assumption (forall (?v0 S15) (?v1 S5) (not (= (f21 (f22 f23 ?v0) ?v1) f20)) ) -:assumption (forall (?v0 S5) (?v1 S8) (not (= (f25 (f26 f27 ?v0) ?v1) f24)) ) -:assumption (forall (?v0 S2) (iff (not (= ?v0 f16)) (exists (?v1 S11) (?v2 S2) (= ?v0 (f17 (f18 f19 ?v1) ?v2)))) ) -:assumption (forall (?v0 S5) (iff (not (= ?v0 f20)) (exists (?v1 S15) (?v2 S5) (= ?v0 (f21 (f22 f23 ?v1) ?v2)))) ) -:assumption (forall (?v0 S8) (iff (not (= ?v0 f24)) (exists (?v1 S5) (?v2 S8) (= ?v0 (f25 (f26 f27 ?v1) ?v2)))) ) -:assumption (forall (?v0 S2) (implies (implies (= ?v0 f16) false) (implies (forall (?v1 S11) (?v2 S2) (implies (= ?v0 (f17 (f18 f19 ?v1) ?v2)) false)) false)) ) -:assumption (forall (?v0 S5) (implies (implies (= ?v0 f20) false) (implies (forall (?v1 S15) (?v2 S5) (implies (= ?v0 (f21 (f22 f23 ?v1) ?v2)) false)) false)) ) -:assumption (forall (?v0 S8) (implies (implies (= ?v0 f24) false) (implies (forall (?v1 S5) (?v2 S8) (implies (= ?v0 (f25 (f26 f27 ?v1) ?v2)) false)) false)) ) -:assumption (forall (?v0 S2) (?v1 S11) (not (= ?v0 (f17 (f18 f19 ?v1) ?v0))) ) -:assumption (forall (?v0 S8) (?v1 S5) (not (= ?v0 (f25 (f26 f27 ?v1) ?v0))) ) -:assumption (forall (?v0 S5) (?v1 S15) (not (= ?v0 (f21 (f22 f23 ?v1) ?v0))) ) -:assumption (forall (?v0 S11) (?v1 S2) (not (= (f17 (f18 f19 ?v0) ?v1) ?v1)) ) -:assumption (forall (?v0 S5) (?v1 S8) (not (= (f25 (f26 f27 ?v0) ?v1) ?v1)) ) -:assumption (forall (?v0 S15) (?v1 S5) (not (= (f21 (f22 f23 ?v0) ?v1) ?v1)) ) -:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (?v3 S2) (iff (= (f17 (f18 f19 ?v0) ?v1) (f17 (f18 f19 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ) -:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8) (iff (= (f25 (f26 f27 ?v0) ?v1) (f25 (f26 f27 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ) -:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (?v3 S5) (iff (= (f21 (f22 f23 ?v0) ?v1) (f21 (f22 f23 ?v2) ?v3)) (and (= ?v0 ?v2) (= ?v1 ?v3))) ) -:assumption (forall (?v0 S11) (?v1 S2) (= (f17 (f28 f29 (f17 (f18 f19 ?v0) ?v1)) f16) (f17 (f18 f19 ?v0) ?v1)) ) -:assumption (forall (?v0 S15) (?v1 S5) (= (f21 (f30 f31 (f21 (f22 f23 ?v0) ?v1)) f20) (f21 (f22 f23 ?v0) ?v1)) ) -:assumption (forall (?v0 S5) (?v1 S8) (= (f25 (f32 f33 (f25 (f26 f27 ?v0) ?v1)) f24) (f25 (f26 f27 ?v0) ?v1)) ) -:assumption (forall (?v0 S11) (= (f17 (f18 f34 ?v0) f16) (f17 (f18 f19 ?v0) f16)) ) -:assumption (forall (?v0 S15) (= (f21 (f22 f35 ?v0) f20) (f21 (f22 f23 ?v0) f20)) ) -:assumption (forall (?v0 S5) (= (f25 (f26 f36 ?v0) f24) (f25 (f26 f27 ?v0) f24)) ) -:assumption (forall (?v0 S2) (?v1 S3) (implies (not (= ?v0 f16)) (implies (forall (?v2 S11) (= (f3 ?v1 (f17 (f18 f19 ?v2) f16)) f1)) (implies (forall (?v2 S11) (?v3 S2) (implies (not (= ?v3 f16)) (implies (= (f3 ?v1 ?v3) f1) (= (f3 ?v1 (f17 (f18 f19 ?v2) ?v3)) f1)))) (= (f3 ?v1 ?v0) f1)))) ) -:assumption (forall (?v0 S5) (?v1 S6) (implies (not (= ?v0 f20)) (implies (forall (?v2 S15) (= (f6 ?v1 (f21 (f22 f23 ?v2) f20)) f1)) (implies (forall (?v2 S15) (?v3 S5) (implies (not (= ?v3 f20)) (implies (= (f6 ?v1 ?v3) f1) (= (f6 ?v1 (f21 (f22 f23 ?v2) ?v3)) f1)))) (= (f6 ?v1 ?v0) f1)))) ) -:assumption (forall (?v0 S8) (?v1 S9) (implies (not (= ?v0 f24)) (implies (forall (?v2 S5) (= (f9 ?v1 (f25 (f26 f27 ?v2) f24)) f1)) (implies (forall (?v2 S5) (?v3 S8) (implies (not (= ?v3 f24)) (implies (= (f9 ?v1 ?v3) f1) (= (f9 ?v1 (f25 (f26 f27 ?v2) ?v3)) f1)))) (= (f9 ?v1 ?v0) f1)))) ) -:assumption (forall (?v0 S11) (?v1 S23) (= (f37 (f38 f39 (f17 (f18 f19 ?v0) f16)) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) (f17 (f18 f19 ?v0) f16) f16)) ) -:assumption (forall (?v0 S15) (?v1 S23) (= (f43 (f44 f45 (f21 (f22 f23 ?v0) f20)) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) (f21 (f22 f23 ?v0) f20) f20)) ) -:assumption (forall (?v0 S5) (?v1 S23) (= (f46 (f47 f48 (f25 (f26 f27 ?v0) f24)) ?v1) (ite (= (f40 (f41 f42 0) ?v1) f1) (f25 (f26 f27 ?v0) f24) f24)) ) -:assumption (forall (?v0 S23) (= (f37 (f38 f39 f16) ?v0) f16) ) -:assumption (forall (?v0 S23) (= (f43 (f44 f45 f20) ?v0) f20) ) -:assumption (forall (?v0 S23) (= (f46 (f47 f48 f24) ?v0) f24) ) -:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (?v3 S2) (= (f17 (f28 f29 (f17 (f18 f19 ?v0) ?v1)) (f17 (f18 f19 ?v2) ?v3)) (f17 (f18 f19 ?v0) (f17 (f18 f19 ?v2) (f17 (f28 f29 ?v1) ?v3)))) ) -:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (?v3 S8) (= (f25 (f32 f33 (f25 (f26 f27 ?v0) ?v1)) (f25 (f26 f27 ?v2) ?v3)) (f25 (f26 f27 ?v0) (f25 (f26 f27 ?v2) (f25 (f32 f33 ?v1) ?v3)))) ) -:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (?v3 S5) (= (f21 (f30 f31 (f21 (f22 f23 ?v0) ?v1)) (f21 (f22 f23 ?v2) ?v3)) (f21 (f22 f23 ?v0) (f21 (f22 f23 ?v2) (f21 (f30 f31 ?v1) ?v3)))) ) -:assumption (forall (?v0 S2) (= (f17 (f28 f29 ?v0) f16) ?v0) ) -:assumption (forall (?v0 S5) (= (f21 (f30 f31 ?v0) f20) ?v0) ) -:assumption (forall (?v0 S8) (= (f25 (f32 f33 ?v0) f24) ?v0) ) -:assumption (forall (?v0 S2) (= (f17 (f28 f29 f16) ?v0) ?v0) ) -:assumption (forall (?v0 S5) (= (f21 (f30 f31 f20) ?v0) ?v0) ) -:assumption (forall (?v0 S8) (= (f25 (f32 f33 f24) ?v0) ?v0) ) -:assumption (forall (?v0 S2) (iff (= ?v0 f16) (= (f49 ?v0) f1)) ) -:assumption (forall (?v0 S5) (iff (= ?v0 f20) (= (f50 ?v0) f1)) ) -:assumption (forall (?v0 S8) (iff (= ?v0 f24) (= (f51 ?v0) f1)) ) -:assumption (forall (?v0 S2) (iff (= (f49 ?v0) f1) (= ?v0 f16)) ) -:assumption (forall (?v0 S5) (iff (= (f50 ?v0) f1) (= ?v0 f20)) ) -:assumption (forall (?v0 S8) (iff (= (f51 ?v0) f1) (= ?v0 f24)) ) -:assumption (iff (= (f49 f16) f1) true) -:assumption (iff (= (f50 f20) f1) true) -:assumption (iff (= (f51 f24) f1) true) -:assumption (forall (?v0 S11) (?v1 S2) (iff (= (f49 (f17 (f18 f19 ?v0) ?v1)) f1) false) ) -:assumption (forall (?v0 S5) (?v1 S8) (iff (= (f51 (f25 (f26 f27 ?v0) ?v1)) f1) false) ) -:assumption (forall (?v0 S15) (?v1 S5) (iff (= (f50 (f21 (f22 f23 ?v0) ?v1)) f1) false) ) -:assumption (forall (?v0 S2) (iff (= (f3 (f4 f52 ?v0) f16) f1) (= (f49 ?v0) f1)) ) -:assumption (forall (?v0 S5) (iff (= (f6 (f7 f53 ?v0) f20) f1) (= (f50 ?v0) f1)) ) -:assumption (forall (?v0 S8) (iff (= (f9 (f10 f54 ?v0) f24) f1) (= (f51 ?v0) f1)) ) -:assumption (forall (?v0 S11) (?v1 S2) (= (f55 f56 (f17 (f18 f19 ?v0) ?v1)) (ite (= ?v1 f16) ?v0 (f55 f56 ?v1))) ) -:assumption (forall (?v0 S15) (?v1 S5) (= (f57 f58 (f21 (f22 f23 ?v0) ?v1)) (ite (= ?v1 f20) ?v0 (f57 f58 ?v1))) ) -:assumption (forall (?v0 S5) (?v1 S8) (= (f59 f60 (f25 (f26 f27 ?v0) ?v1)) (ite (= ?v1 f24) ?v0 (f59 f60 ?v1))) ) -:assumption (forall (?v0 S2) (?v1 S11) (implies (not (= ?v0 f16)) (= (f55 f56 (f17 (f18 f19 ?v1) ?v0)) (f55 f56 ?v0))) ) -:assumption (forall (?v0 S5) (?v1 S15) (implies (not (= ?v0 f20)) (= (f57 f58 (f21 (f22 f23 ?v1) ?v0)) (f57 f58 ?v0))) ) -:assumption (forall (?v0 S8) (?v1 S5) (implies (not (= ?v0 f24)) (= (f59 f60 (f25 (f26 f27 ?v1) ?v0)) (f59 f60 ?v0))) ) -:assumption (forall (?v0 S2) (?v1 S11) (implies (= ?v0 f16) (= (f55 f56 (f17 (f18 f19 ?v1) ?v0)) ?v1)) ) -:assumption (forall (?v0 S5) (?v1 S15) (implies (= ?v0 f20) (= (f57 f58 (f21 (f22 f23 ?v1) ?v0)) ?v1)) ) -:assumption (forall (?v0 S8) (?v1 S5) (implies (= ?v0 f24) (= (f59 f60 (f25 (f26 f27 ?v1) ?v0)) ?v1)) ) -:assumption (forall (?v0 S11) (iff (= (f61 (f62 f16) ?v0) f1) false) ) -:assumption (forall (?v0 S15) (iff (= (f63 (f64 f20) ?v0) f1) false) ) -:assumption (forall (?v0 S5) (iff (= (f6 (f65 f24) ?v0) f1) false) ) -:assumption (forall (?v0 S35) (iff (= (f3 (f66 ?v0) f16) f1) false) ) -:assumption (forall (?v0 S36) (iff (= (f6 (f67 ?v0) f20) f1) false) ) -:assumption (forall (?v0 S6) (iff (= (f9 (f68 ?v0) f24) f1) false) ) -:assumption (forall (?v0 S11) (?v1 S2) (= (f3 (f69 ?v0) (f17 (f18 f19 ?v0) ?v1)) f1) ) -:assumption (forall (?v0 S5) (?v1 S8) (= (f9 (f70 ?v0) (f25 (f26 f27 ?v0) ?v1)) f1) ) -:assumption (forall (?v0 S15) (?v1 S5) (= (f6 (f71 ?v0) (f21 (f22 f23 ?v0) ?v1)) f1) ) -:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (iff (= (f61 (f62 (f17 (f18 f19 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f61 (f62 ?v1) ?v2) f1))) ) -:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (iff (= (f6 (f65 (f25 (f26 f27 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f6 (f65 ?v1) ?v2) f1))) ) -:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (iff (= (f63 (f64 (f21 (f22 f23 ?v0) ?v1)) ?v2) f1) (or (= ?v0 ?v2) (= (f63 (f64 ?v1) ?v2) f1))) ) -:assumption (forall (?v0 S8) (?v1 S8) (iff (= (f9 (f10 f54 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (forall (?v0 S5) (?v1 S5) (iff (= (f6 (f7 f53 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f52 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (= (f17 f72 f16) f16) -:assumption (= (f21 f73 f20) f20) -:assumption (= (f25 f74 f24) f24) -:assumption (forall (?v0 S11) (?v1 S2) (= (f17 f72 (f17 (f18 f19 ?v0) ?v1)) (ite (= ?v1 f16) f16 (f17 (f18 f19 ?v0) (f17 f72 ?v1)))) ) -:assumption (forall (?v0 S15) (?v1 S5) (= (f21 f73 (f21 (f22 f23 ?v0) ?v1)) (ite (= ?v1 f20) f20 (f21 (f22 f23 ?v0) (f21 f73 ?v1)))) ) -:assumption (forall (?v0 S5) (?v1 S8) (= (f25 f74 (f25 (f26 f27 ?v0) ?v1)) (ite (= ?v1 f24) f24 (f25 (f26 f27 ?v0) (f25 f74 ?v1)))) ) -:assumption (forall (?v0 S11) (?v1 S2) (?v2 S11) (implies (= (f3 (f69 ?v0) ?v1) f1) (= (f3 (f69 ?v0) (f17 (f18 f19 ?v2) ?v1)) f1)) ) -:assumption (forall (?v0 S5) (?v1 S8) (?v2 S5) (implies (= (f9 (f70 ?v0) ?v1) f1) (= (f9 (f70 ?v0) (f25 (f26 f27 ?v2) ?v1)) f1)) ) -:assumption (forall (?v0 S15) (?v1 S5) (?v2 S15) (implies (= (f6 (f71 ?v0) ?v1) f1) (= (f6 (f71 ?v0) (f21 (f22 f23 ?v2) ?v1)) f1)) ) -:assumption (forall (?v0 S2) (implies (not (= ?v0 f16)) (= (f17 (f28 f75 (f17 f72 ?v0)) (f17 (f18 f19 (f55 f56 ?v0)) f16)) ?v0)) ) -:assumption (forall (?v0 S5) (implies (not (= ?v0 f20)) (= (f21 (f30 f76 (f21 f73 ?v0)) (f21 (f22 f23 (f57 f58 ?v0)) f20)) ?v0)) ) -:assumption (forall (?v0 S8) (implies (not (= ?v0 f24)) (= (f25 (f32 f77 (f25 f74 ?v0)) (f25 (f26 f27 (f59 f60 ?v0)) f24)) ?v0)) ) -:assumption (forall (?v0 S2) (?v1 S11) (?v2 S2) (iff (= (f17 (f28 f75 ?v0) (f17 (f18 f19 ?v1) f16)) ?v2) (and (not (= ?v2 f16)) (and (= (f17 f72 ?v2) ?v0) (= (f55 f56 ?v2) ?v1)))) ) -:assumption (forall (?v0 S5) (?v1 S15) (?v2 S5) (iff (= (f21 (f30 f76 ?v0) (f21 (f22 f23 ?v1) f20)) ?v2) (and (not (= ?v2 f20)) (and (= (f21 f73 ?v2) ?v0) (= (f57 f58 ?v2) ?v1)))) ) -:assumption (forall (?v0 S8) (?v1 S5) (?v2 S8) (iff (= (f25 (f32 f77 ?v0) (f25 (f26 f27 ?v1) f24)) ?v2) (and (not (= ?v2 f24)) (and (= (f25 f74 ?v2) ?v0) (= (f59 f60 ?v2) ?v1)))) ) -:assumption (= f11 f54) -:assumption (= f8 f53) -:assumption (= f5 f52) -:assumption (forall (?v0 S8) (?v1 S8) (iff (= (f9 (f10 f54 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (forall (?v0 S5) (?v1 S5) (iff (= (f6 (f7 f53 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (forall (?v0 S2) (?v1 S2) (iff (= (f3 (f4 f52 ?v0) ?v1) f1) (= ?v0 ?v1)) ) -:assumption (forall (?v0 S8) (iff (= (f9 (f10 f54 ?v0) ?v0) f1) true) ) -:assumption (forall (?v0 S5) (iff (= (f6 (f7 f53 ?v0) ?v0) f1) true) ) -:assumption (forall (?v0 S2) (iff (= (f3 (f4 f52 ?v0) ?v0) f1) true) ) -:assumption (= f54 f11) -:assumption (= f53 f8) -:assumption (= f52 f5) -:assumption (forall (?v0 S11) (?v1 S2) (iff (= (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)))))) ) -:assumption (forall (?v0 S5) (?v1 S8) (iff (= (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)))))) ) -:assumption (forall (?v0 S15) (?v1 S5) (iff (= (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)))))) ) -:assumption (forall (?v0 S2) (?v1 S11) (= (f55 f56 (f17 (f28 f75 ?v0) (f17 (f18 f19 ?v1) f16))) ?v1) ) -:assumption (forall (?v0 S5) (?v1 S15) (= (f57 f58 (f21 (f30 f76 ?v0) (f21 (f22 f23 ?v1) f20))) ?v1) ) -:assumption (forall (?v0 S8) (?v1 S5) (= (f59 f60 (f25 (f32 f77 ?v0) (f25 (f26 f27 ?v1) f24))) ?v1) ) -:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8) (implies (= (f25 (f32 f77 ?v0) ?v1) ?v2) (implies (= ?v3 (f25 (f32 f77 ?v1) ?v4)) (= (f25 (f32 f77 ?v0) ?v3) (f25 (f32 f77 ?v2) ?v4)))) ) -:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5) (implies (= (f21 (f30 f76 ?v0) ?v1) ?v2) (implies (= ?v3 (f21 (f30 f76 ?v1) ?v4)) (= (f21 (f30 f76 ?v0) ?v3) (f21 (f30 f76 ?v2) ?v4)))) ) -:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2) (implies (= (f17 (f28 f75 ?v0) ?v1) ?v2) (implies (= ?v3 (f17 (f28 f75 ?v1) ?v4)) (= (f17 (f28 f75 ?v0) ?v3) (f17 (f28 f75 ?v2) ?v4)))) ) -:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (iff (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v2) ?v1)) (= ?v0 ?v2)) ) -:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (iff (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v2) ?v1)) (= ?v0 ?v2)) ) -:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (iff (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v2) ?v1)) (= ?v0 ?v2)) ) -:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (iff (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v0) ?v2)) (= ?v1 ?v2)) ) -:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (iff (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v0) ?v2)) (= ?v1 ?v2)) ) -:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (iff (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v0) ?v2)) (= ?v1 ?v2)) ) -:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (?v3 S8) (iff (= (f25 (f32 f77 ?v0) ?v1) (f25 (f32 f77 ?v2) ?v3)) (exists (?v4 S8) (or (and (= ?v0 (f25 (f32 f77 ?v2) ?v4)) (= (f25 (f32 f77 ?v4) ?v1) ?v3)) (and (= (f25 (f32 f77 ?v0) ?v4) ?v2) (= ?v1 (f25 (f32 f77 ?v4) ?v3)))))) ) -:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (?v3 S5) (iff (= (f21 (f30 f76 ?v0) ?v1) (f21 (f30 f76 ?v2) ?v3)) (exists (?v4 S5) (or (and (= ?v0 (f21 (f30 f76 ?v2) ?v4)) (= (f21 (f30 f76 ?v4) ?v1) ?v3)) (and (= (f21 (f30 f76 ?v0) ?v4) ?v2) (= ?v1 (f21 (f30 f76 ?v4) ?v3)))))) ) -:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (?v3 S2) (iff (= (f17 (f28 f75 ?v0) ?v1) (f17 (f28 f75 ?v2) ?v3)) (exists (?v4 S2) (or (and (= ?v0 (f17 (f28 f75 ?v2) ?v4)) (= (f17 (f28 f75 ?v4) ?v1) ?v3)) (and (= (f17 (f28 f75 ?v0) ?v4) ?v2) (= ?v1 (f17 (f28 f75 ?v4) ?v3)))))) ) -:assumption (forall (?v0 S8) (?v1 S8) (?v2 S8) (= (f25 (f32 f77 (f25 (f32 f77 ?v0) ?v1)) ?v2) (f25 (f32 f77 ?v0) (f25 (f32 f77 ?v1) ?v2))) ) -:assumption (forall (?v0 S5) (?v1 S5) (?v2 S5) (= (f21 (f30 f76 (f21 (f30 f76 ?v0) ?v1)) ?v2) (f21 (f30 f76 ?v0) (f21 (f30 f76 ?v1) ?v2))) ) -:assumption (forall (?v0 S2) (?v1 S2) (?v2 S2) (= (f17 (f28 f75 (f17 (f28 f75 ?v0) ?v1)) ?v2) (f17 (f28 f75 ?v0) (f17 (f28 f75 ?v1) ?v2))) ) -:assumption (forall (?v0 S11) (?v1 S2) (?v2 S2) (= (f17 (f28 f75 (f17 (f18 f19 ?v0) ?v1)) ?v2) (f17 (f18 f19 ?v0) (f17 (f28 f75 ?v1) ?v2))) ) -:assumption (forall (?v0 S5) (?v1 S8) (?v2 S8) (= (f25 (f32 f77 (f25 (f26 f27 ?v0) ?v1)) ?v2) (f25 (f26 f27 ?v0) (f25 (f32 f77 ?v1) ?v2))) ) -:assumption (forall (?v0 S15) (?v1 S5) (?v2 S5) (= (f21 (f30 f76 (f21 (f22 f23 ?v0) ?v1)) ?v2) (f21 (f22 f23 ?v0) (f21 (f30 f76 ?v1) ?v2))) ) -:assumption (forall (?v0 S11) (?v1 S2) (?v2 S2) (?v3 S2) (?v4 S2) (implies (= (f17 (f18 f19 ?v0) ?v1) ?v2) (implies (= ?v3 (f17 (f28 f75 ?v1) ?v4)) (= (f17 (f18 f19 ?v0) ?v3) (f17 (f28 f75 ?v2) ?v4)))) ) -:assumption (forall (?v0 S5) (?v1 S8) (?v2 S8) (?v3 S8) (?v4 S8) (implies (= (f25 (f26 f27 ?v0) ?v1) ?v2) (implies (= ?v3 (f25 (f32 f77 ?v1) ?v4)) (= (f25 (f26 f27 ?v0) ?v3) (f25 (f32 f77 ?v2) ?v4)))) ) -:assumption (forall (?v0 S15) (?v1 S5) (?v2 S5) (?v3 S5) (?v4 S5) (implies (= (f21 (f22 f23 ?v0) ?v1) ?v2) (implies (= ?v3 (f21 (f30 f76 ?v1) ?v4)) (= (f21 (f22 f23 ?v0) ?v3) (f21 (f30 f76 ?v2) ?v4)))) ) -:assumption (forall (?v0 S2) (= (f17 (f28 f75 f16) ?v0) ?v0) ) -:assumption (forall (?v0 S5) (= (f21 (f30 f76 f20) ?v0) ?v0) ) -:assumption (forall (?v0 S8) (= (f25 (f32 f77 f24) ?v0) ?v0) ) -:assumption (forall (?v0 S2) (?v1 S2) (iff (= f16 (f17 (f28 f75 ?v0) ?v1)) (and (= ?v0 f16) (= ?v1 f16))) ) -:assumption (forall (?v0 S5) (?v1 S5) (iff (= f20 (f21 (f30 f76 ?v0) ?v1)) (and (= ?v0 f20) (= ?v1 f20))) ) -:assumption (forall (?v0 S8) (?v1 S8) (iff (= f24 (f25 (f32 f77 ?v0) ?v1)) (and (= ?v0 f24) (= ?v1 f24))) ) -:assumption (forall (?v0 S2) (= (f17 (f28 f75 ?v0) f16) ?v0) ) -:assumption (forall (?v0 S5) (= (f21 (f30 f76 ?v0) f20) ?v0) ) -:assumption (forall (?v0 S8) (= (f25 (f32 f77 ?v0) f24) ?v0) ) -:assumption (forall (?v0 S2) (?v1 S2) (iff (= ?v0 (f17 (f28 f75 ?v0) ?v1)) (= ?v1 f16)) ) -:assumption (forall (?v0 S5) (?v1 S5) (iff (= ?v0 (f21 (f30 f76 ?v0) ?v1)) (= ?v1 f20)) ) -:assumption (forall (?v0 S8) (?v1 S8) (iff (= ?v0 (f25 (f32 f77 ?v0) ?v1)) (= ?v1 f24)) ) -:assumption (forall (?v0 S2) (?v1 S2) (iff (= ?v0 (f17 (f28 f75 ?v1) ?v0)) (= ?v1 f16)) ) -:assumption (forall (?v0 S5) (?v1 S5) (iff (= ?v0 (f21 (f30 f76 ?v1) ?v0)) (= ?v1 f20)) ) -:assumption (forall (?v0 S8) (?v1 S8) (iff (= ?v0 (f25 (f32 f77 ?v1) ?v0)) (= ?v1 f24)) ) -:assumption (forall (?v0 S26) (= (f41 f42 (f78 f79 ?v0)) ?v0)) -:assumption (forall (?v0 Int) (implies (<= 0 ?v0) (= (f78 f79 (f41 f42 ?v0)) ?v0))) -:assumption (forall (?v0 Int) (implies (< ?v0 0) (= (f78 f79 (f41 f42 ?v0)) 0))) -:formula true) -; solver: z3 -; timeout: 5.0 -; random seed: 1 -; arguments: -; DISPLAY_PROOF=true -; PROOF_MODE=2 -; -rs:1 -; MODEL=true -; -smt diff --git a/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smtv1.smt2 b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smtv1.smt2 new file mode 100644 index 000000000..4429107d5 --- /dev/null +++ b/test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smtv1.smt2 @@ -0,0 +1,288 @@ +; 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 )) diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smt b/test/regress/regress0/fmf/QEpres-uf.855035.smt deleted file mode 100644 index 97a585090..000000000 --- a/test/regress/regress0/fmf/QEpres-uf.855035.smt +++ /dev/null @@ -1,84 +0,0 @@ -; COMMAND-LINE: --finite-model-find -; EXPECT: sat -(benchmark Isabelle -:status sat -:logic AUFLIA -:extrasorts ( S1 S2 S3 S4 S5 S6 S7 S8 S9 S10 S11 S12 S13 S14 S15 S16 S17 S18) -:extrafuns ( - (f1 S1) - (f2 S1) - (f3 S2 S3 S4) - (f4 S2) - (f5 S3) - (f6 S4) - (f7 S3 S5 S1) - (f8 S6 S5) - (f9 S6) - (f10 S7 S6 S6) - (f11 S7) - (f12 S8 S4 S4) - (f13 S8) - (f14 S10 S3 S3) - (f15 S11 S9 S10) - (f16 S12 S4 S11) - (f17 S12) - (f18 S4 S13 S1) - (f19 S13) - (f20 S4 S1) - (f21 S2) - (f22 S10) - (f23 S3 S9 S1) - (f24 S14 S9 S9) - (f25 S15 S4 S14) - (f26 S15) - (f27 S13) - (f28 S8) - (f29 S16 S9 S3) - (f30 S17 S4 S16) - (f31 S18 S4 S17) - (f32 S18) - (f33 S18) - (f34 S4 S4 S1) -) -:assumption (not (= f1 f2)) -:assumption (not (not (= (f3 f4 f5) f6))) -:assumption (forall (?v0 S3) (implies (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f4 ?v0) f6))) ) -:assumption (= (f7 f5 (f8 (f10 f11 f9))) f1) -:assumption (forall (?v0 S4) (iff (= f6 ?v0) (= ?v0 f6)) ) -:assumption (= (f12 f13 f6) f6) -:assumption (forall (?v0 S4) (iff (= f6 (f12 f13 ?v0)) (= ?v0 f6)) ) -:assumption (forall (?v0 S4) (iff (= (f12 f13 ?v0) f6) (= ?v0 f6)) ) -:assumption (forall (?v0 S4) (?v1 S9) (?v2 S3) (= (f3 f4 (f14 (f15 (f16 f17 ?v0) ?v1) ?v2)) (f3 f4 ?v2)) ) -:assumption (= (f18 f6 f19) f1) -:assumption (= (f20 f6) f1) -:assumption (forall (?v0 S4) (iff (= (f20 ?v0) f1) (= ?v0 f6)) ) -:assumption (forall (?v0 S3) (implies (= (f7 ?v0 (f8 f9)) f1) (not (= (f3 f21 ?v0) f6))) ) -:assumption (forall (?v0 S3) (implies (not (not (= (f3 f21 ?v0) f6))) (implies (not (= (f3 f4 ?v0) f6)) (not (= (f3 f4 (f14 f22 ?v0)) f6)))) ) -:assumption (forall (?v0 S4) (?v1 S4) (iff (= (f12 f13 ?v0) (f12 f13 ?v1)) (= ?v0 ?v1)) ) -:assumption (forall (?v0 S6) (?v1 S9) (implies (forall (?v2 S3) (implies (= (f7 ?v2 (f8 ?v0)) f1) (not (= (f3 f21 ?v2) f6)))) (iff (exists (?v2 S4) (forall (?v3 S3) (implies (= (f7 ?v3 (f8 (f10 f11 ?v0))) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)))) (exists (?v2 S4) (forall (?v3 S3) (implies (= (f7 ?v3 (f8 ?v0)) f1) (= (f23 ?v3 (f24 (f25 f26 ?v2) ?v1)) f1)))))) ) -:assumption (forall (?v0 S4) (= (f18 (f12 f13 ?v0) f27) f1) ) -:assumption (= (f12 f28 f6) f6) -:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (= (f3 f4 (f29 (f30 (f31 f32 ?v0) ?v1) ?v2)) ?v0) ) -:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (= (f3 f4 (f29 (f30 (f31 f33 ?v0) ?v1) ?v2)) ?v0) ) -:assumption (= (f18 f6 f27) f1) -:assumption (forall (?v0 S3) (?v1 S4) (?v2 S9) (implies (not (not (= (f3 f21 ?v0) f6))) (iff (= (f23 ?v0 (f24 (f25 f26 ?v1) ?v2)) f1) (= (f23 (f14 f22 ?v0) ?v2) f1))) ) -:assumption (forall (?v0 S4) (iff (= (f34 (f12 f13 ?v0) f6) f1) (= (f34 ?v0 f6) f1)) ) -:assumption (forall (?v0 S4) (iff (= (f34 f6 (f12 f13 ?v0)) f1) (= (f34 f6 ?v0) f1)) ) -:assumption (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))) ) -:assumption (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))) ) -:assumption (forall (?v0 S4) (= (f34 ?v0 ?v0) f1) ) -:assumption (forall (?v0 S4) (?v1 S4) (or (= (f34 ?v0 ?v1) f1) (= (f34 ?v1 ?v0) f1)) ) -:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (iff (= (f29 (f30 (f31 f33 ?v0) ?v1) ?v2) (f29 (f30 (f31 f33 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ) -:assumption (forall (?v0 S4) (?v1 S4) (?v2 S9) (?v3 S4) (?v4 S4) (?v5 S9) (iff (= (f29 (f30 (f31 f32 ?v0) ?v1) ?v2) (f29 (f30 (f31 f32 ?v3) ?v4) ?v5)) (and (= ?v0 ?v3) (and (= ?v1 ?v4) (= ?v2 ?v5)))) ) -:assumption (forall (?v0 S4) (?v1 S4) (?v2 S4) (implies (= (f34 ?v0 ?v1) f1) (implies (= (f34 ?v1 ?v2) f1) (= (f34 ?v0 ?v2) f1))) ) -:assumption (forall (?v0 S4) (?v1 S4) (implies (= (f34 ?v0 ?v1) f1) (implies (= (f34 ?v1 ?v0) f1) (= ?v0 ?v1))) ) -:formula true) -; solver: z3 -; timeout: 1.897 -; random seed: 1 -; arguments: -; DISPLAY_PROOF=true -; PROOF_MODE=2 -; -rs:1 -; MODEL=true -; -smt diff --git a/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 new file mode 100644 index 000000000..619779c78 --- /dev/null +++ b/test/regress/regress0/fmf/QEpres-uf.855035.smtv1.smt2 @@ -0,0 +1,90 @@ +; 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 )) |