diff options
Diffstat (limited to 'test/regress/regress0/fmf/PUZ001+1.smt2')
| -rw-r--r-- | test/regress/regress0/fmf/PUZ001+1.smt2 | 118 |
1 files changed, 0 insertions, 118 deletions
diff --git a/test/regress/regress0/fmf/PUZ001+1.smt2 b/test/regress/regress0/fmf/PUZ001+1.smt2 deleted file mode 100644 index f3db78491..000000000 --- a/test/regress/regress0/fmf/PUZ001+1.smt2 +++ /dev/null @@ -1,118 +0,0 @@ -; COMMAND-LINE: --finite-model-find --no-check-proofs --no-check-unsat-core -; EXPECT: unsat -;%------------------------------------------------------------------------------ -;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. -;% Domain : Puzzles -;% Problem : Dreadbury Mansion -;% Version : Especial. -;% Theorem formulation : Reduced > Complete. -;% English : Someone who lives in Dreadbury Mansion killed Aunt Agatha. -;% Agatha, the butler, and Charles live in Dreadbury Mansion, -;% and are the only people who live therein. A killer always -;% hates his victim, and is never richer than his victim. -;% Charles hates no one that Aunt Agatha hates. Agatha hates -;% everyone except the butler. The butler hates everyone not -;% richer than Aunt Agatha. The butler hates everyone Aunt -;% Agatha hates. No one hates everyone. Agatha is not the -;% butler. Therefore : Agatha killed herself. - -;% Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au -;% : [Hah94] Haehnle (1994), Email to G. Sutcliffe -;% Source : [Hah94] -;% Names : Pelletier 55 [Pel86] - -;% Status : Theorem -;% Rating : 0.07 v5.3.0, 0.19 v5.2.0, 0.00 v5.0.0, 0.08 v4.1.0, 0.13 v4.0.0, 0.12 v3.7.0, 0.14 v3.5.0, 0.00 v3.4.0, 0.08 v3.3.0, 0.11 v3.2.0, 0.22 v3.1.0, 0.17 v2.7.0, 0.00 v2.5.0, 0.33 v2.4.0, 0.33 v2.2.1, 0.00 v2.1.0 -;% Syntax : Number of formulae : 14 ( 6 unit) -;% Number of atoms : 24 ( 5 equality) -;% Maximal formula depth : 5 ( 3 average) -;% Number of connectives : 16 ( 6 ~; 2 |; 1 &) -;% ( 0 <=>; 7 =>; 0 <=; 0 <~>) -;% ( 0 ~|; 0 ~&) -;% Number of predicates : 5 ( 0 propositional; 1-2 arity) -;% Number of functors : 3 ( 3 constant; 0-0 arity) -;% Number of variables : 12 ( 0 sgn; 10 !; 2 ?) -;% Maximal term depth : 1 ( 1 average) -;% SPC : FOF_THM_RFO_SEQ - -;% Comments : Modified by Geoff Sutcliffe. -;% : Also known as "Who killed Aunt Agatha" -;%------------------------------------------------------------------------------ -;%----Problem axioms -(set-logic UF) -(set-info :status unsat) -(declare-sort sort__smt2 0) -; functions -(declare-fun agatha__smt2_0 ( ) sort__smt2) -(declare-fun butler__smt2_0 ( ) sort__smt2) -(declare-fun charles__smt2_0 ( ) sort__smt2) -; predicates -(declare-fun lives__smt2_1 ( sort__smt2 ) Bool) -(declare-fun killed__smt2_2 ( sort__smt2 sort__smt2 ) Bool) -(declare-fun hates__smt2_2 ( sort__smt2 sort__smt2 ) Bool) -(declare-fun richer__smt2_2 ( sort__smt2 sort__smt2 ) Bool) - -; pel55_1 axiom -(assert (exists ((?X sort__smt2)) - (and (lives__smt2_1 ?X) - (killed__smt2_2 ?X agatha__smt2_0)))) - -; pel55_2_1 axiom -(assert (lives__smt2_1 agatha__smt2_0)) - -; pel55_2_2 axiom -(assert (lives__smt2_1 butler__smt2_0)) - -; pel55_2_3 axiom -(assert (lives__smt2_1 charles__smt2_0)) - -; pel55_3 axiom -(assert (forall ((?X sort__smt2)) - (=> (lives__smt2_1 ?X) - (or (= ?X agatha__smt2_0) - (= ?X butler__smt2_0) - (= ?X charles__smt2_0))))) - -; pel55_4 axiom -(assert (forall ((?X sort__smt2) (?Y sort__smt2)) - (=> (killed__smt2_2 ?X ?Y) - (hates__smt2_2 ?X ?Y)))) - -; pel55_5 axiom -(assert (forall ((?X sort__smt2) (?Y sort__smt2)) - (=> (killed__smt2_2 ?X ?Y) - (not (richer__smt2_2 ?X ?Y))))) - -; pel55_6 axiom -(assert (forall ((?X sort__smt2)) - (=> (hates__smt2_2 agatha__smt2_0 ?X) - (not (hates__smt2_2 charles__smt2_0 ?X))))) - -; pel55_7 axiom -(assert (forall ((?X sort__smt2)) - (=> (not (= ?X butler__smt2_0)) - (hates__smt2_2 agatha__smt2_0 ?X)))) - -; pel55_8 axiom -(assert (forall ((?X sort__smt2)) - (=> (not (richer__smt2_2 ?X agatha__smt2_0)) - (hates__smt2_2 butler__smt2_0 ?X)))) - -; pel55_9 axiom -(assert (forall ((?X sort__smt2)) - (=> (hates__smt2_2 agatha__smt2_0 ?X) - (hates__smt2_2 butler__smt2_0 ?X)))) - -; pel55_10 axiom -(assert (forall ((?X sort__smt2)) -(exists ((?Y sort__smt2)) (not (hates__smt2_2 ?X ?Y))))) - -; pel55_11 axiom -(assert (not (= agatha__smt2_0 butler__smt2_0))) - -;----This is the conjecture with negated conjecture -; pel55 conjecture -(assert (not (killed__smt2_2 agatha__smt2_0 agatha__smt2_0))) - - -(check-sat) |