diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-06-24 19:58:37 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-11 17:15:59 -0400 |
| commit | e80b93ca958bdbeb28959029868f6193b39a3f19 (patch) | |
| tree | 92218adf47348cb8011a41599e158b371f5659de /test/regress/regress0 | |
| parent | b76afedab3a23525da478ba4a8687c882793ea81 (diff) | |
Support for TPTP's TFF0 (with arithmetic)
This commit reverses an "SZS ontology compliance hack" that was
done for CASC-24 this year, and adds a TPTP pretty-printer which
is capable of outputting results in the TPTP way (rather than the
SMT way).
This commit includes minor changes to the Expr package to add
obvious missing functionality, and to fix the way expressions
with builtin operators are made. These changes are truly a
_fix_, the implementation had not been properly aligned with
the design vision for some corner cases.
Diffstat (limited to 'test/regress/regress0')
39 files changed, 2438 insertions, 33 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index e380f2fc2..b1c15c73a 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,5 +1,5 @@ -SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf -DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess unconstrained decision fmf +SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf +DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf BINARY = cvc4 LOG_COMPILER = @srcdir@/../run_regression @@ -101,17 +101,7 @@ CVC_TESTS = \ print_lambda.cvc # Regression tests for TPTP inputs -TPTP_TESTS = \ - tptp_parser.p \ - tptp_parser2.p \ - tptp_parser3.p \ - tptp_parser4.p \ - tptp_parser5.p \ - tptp_parser6.p \ - tptp_parser7.p \ - tptp_parser8.p \ - tptp_parser9.p \ - tptp_parser10.p +TPTP_TESTS = # Regression tests derived from bug reports BUG_TESTS = \ diff --git a/test/regress/regress0/tptp/ARI086=1.p b/test/regress/regress0/tptp/ARI086=1.p new file mode 100644 index 000000000..f6d2fcb28 --- /dev/null +++ b/test/regress/regress0/tptp/ARI086=1.p @@ -0,0 +1,32 @@ +%------------------------------------------------------------------------------ +% File : ARI086=1 : TPTP v5.5.0. Released v5.0.0. +% Domain : Arithmetic +% Problem : Integer: Sum 2 and 2 is 5 +% Version : Especial. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : CounterSatisfiable +% Rating : 0.00 v5.2.0, 1.00 v5.0.0 +% Syntax : Number of formulae : 1 ( 1 unit; 0 type) +% Number of atoms : 1 ( 1 equality) +% Maximal formula depth : 1 ( 1 average) +% Number of connectives : 0 ( 0 ~; 0 |; 0 &) +% ( 0 <=>; 0 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 3 ( 2 constant; 0-2 arity) +% Number of variables : 0 ( 0 sgn; 0 !; 0 ?) +% Maximal term depth : 2 ( 2 average) +% Arithmetic symbols : 3 ( 0 pred; 1 func; 2 numbers) +% SPC : TFF_CSA_EQU_ARI + +% Comments : +%------------------------------------------------------------------------------ +tff(anti_sum_2_2_5,conjecture, + ( $sum(2,2) = 5 )). +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/Axioms/BOO004-0.ax b/test/regress/regress0/tptp/Axioms/BOO004-0.ax new file mode 100644 index 000000000..e02b4c2f8 --- /dev/null +++ b/test/regress/regress0/tptp/Axioms/BOO004-0.ax @@ -0,0 +1,48 @@ +%-------------------------------------------------------------------------- +% File : BOO004-0 : TPTP v5.5.0. Released v1.0.0. +% Domain : Boolean Algebra +% Axioms : Boolean algebra (equality) axioms +% Version : [Ver94] (equality) axioms. +% English : + +% Refs : [Ver94] Veroff (1994), Problem Set +% Source : [Ver94] +% Names : + +% Status : Satisfiable +% Syntax : Number of clauses : 8 ( 0 non-Horn; 8 unit; 0 RR) +% Number of atoms : 8 ( 8 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 5 ( 2 constant; 0-2 arity) +% Number of variables : 14 ( 0 singleton) +% Maximal term depth : 3 ( 2 average) +% SPC : + +% Comments : +%-------------------------------------------------------------------------- +cnf(commutativity_of_add,axiom, + ( add(X,Y) = add(Y,X) )). + +cnf(commutativity_of_multiply,axiom, + ( multiply(X,Y) = multiply(Y,X) )). + +cnf(distributivity1,axiom, + ( add(X,multiply(Y,Z)) = multiply(add(X,Y),add(X,Z)) )). + +cnf(distributivity2,axiom, + ( multiply(X,add(Y,Z)) = add(multiply(X,Y),multiply(X,Z)) )). + +cnf(additive_id1,axiom, + ( add(X,additive_identity) = X )). + +cnf(multiplicative_id1,axiom, + ( multiply(X,multiplicative_identity) = X )). + +cnf(additive_inverse1,axiom, + ( add(X,inverse(X)) = multiplicative_identity )). + +cnf(multiplicative_inverse1,axiom, + ( multiply(X,inverse(X)) = additive_identity )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/Axioms/SYN000+0.ax b/test/regress/regress0/tptp/Axioms/SYN000+0.ax new file mode 100644 index 000000000..24ef682b7 --- /dev/null +++ b/test/regress/regress0/tptp/Axioms/SYN000+0.ax @@ -0,0 +1,37 @@ +%------------------------------------------------------------------------------ +% File : SYN000+0 : TPTP v5.5.0. Released v3.6.0. +% Domain : Syntactic +% Axioms : A simple include file for FOF +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Syntax : Number of formulae : 3 ( 3 unit) +% Number of atoms : 3 ( 0 equality) +% Maximal formula depth : 1 ( 1 average) +% Number of connectives : 0 ( 0 ~ ; 0 |; 0 &) +% ( 0 <=>; 0 =>; 0 <=) +% ( 0 <~>; 0 ~|; 0 ~&) +% Number of predicates : 3 ( 3 propositional; 0-0 arity) +% Number of functors : 0 ( 0 constant; --- arity) +% Number of variables : 0 ( 0 singleton; 0 !; 0 ?) +% Maximal term depth : 0 ( 0 average) +% SPC : + +% Comments : +%------------------------------------------------------------------------------ +%----Some axioms to include +fof(ia1,axiom, + ia1). + +fof(ia2,axiom, + ia2). + +fof(ia3,axiom, + ia3). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/Axioms/SYN000-0.ax b/test/regress/regress0/tptp/Axioms/SYN000-0.ax new file mode 100644 index 000000000..d67e61aee --- /dev/null +++ b/test/regress/regress0/tptp/Axioms/SYN000-0.ax @@ -0,0 +1,34 @@ +%------------------------------------------------------------------------------ +% File : SYN000-0 : TPTP v5.5.0. Released v3.6.0. +% Domain : Syntactic +% Axioms : A simple include file for CNF +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Syntax : Number of clauses : 3 ( 0 non-Horn; 3 unit; 3 RR) +% Number of atoms : 3 ( 0 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 3 ( 3 propositional; 0-0 arity) +% Number of functors : 0 ( 0 constant; --- arity) +% Number of variables : 0 ( 0 singleton) +% Maximal term depth : 0 ( 0 average) +% SPC : + +% Comments : +%------------------------------------------------------------------------------ +%----Some axioms to include +cnf(ia1,axiom, + ia1). + +cnf(ia2,axiom, + ia2). + +cnf(ia3,axiom, + ia3). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/Axioms/SYN000_0.ax b/test/regress/regress0/tptp/Axioms/SYN000_0.ax new file mode 100644 index 000000000..acb557ef4 --- /dev/null +++ b/test/regress/regress0/tptp/Axioms/SYN000_0.ax @@ -0,0 +1,47 @@ +%------------------------------------------------------------------------------ +% File : SYN000_0 : TPTP v5.5.0. Released v5.0.0. +% Domain : Syntactic +% Axioms : A simple include file for TFF +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Syntax : Number of formulae : 6 ( 6 unit; 3 type) +% Number of atoms : 6 ( 0 equality) +% Maximal formula depth : 2 ( 2 average) +% Number of connectives : 0 ( 0 ~; 0 |; 0 &) +% ( 0 <=>; 0 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<) +% Number of predicates : 4 ( 4 propositional; 0-0 arity) +% Number of functors : 0 ( 0 constant; --- arity) +% Number of variables : 0 ( 0 sgn; 0 !; 0 ?) +% Maximal term depth : 0 ( 0 average) +% SPC : + +% Comments : +%------------------------------------------------------------------------------ +%----Some axioms to include +tff(ia1_type,type,( + ia1: $o )). + +tff(ia2_type,type,( + ia2: $o )). + +tff(ia3_type,type,( + ia3: $o )). + +tff(ia1,axiom,( + ia1 )). + +tff(ia2,axiom,( + ia2 )). + +tff(ia3,axiom,( + ia3 )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/BOO003-4.p b/test/regress/regress0/tptp/BOO003-4.p new file mode 100644 index 000000000..0ea15fefc --- /dev/null +++ b/test/regress/regress0/tptp/BOO003-4.p @@ -0,0 +1,31 @@ +%-------------------------------------------------------------------------- +% File : BOO003-4 : TPTP v5.5.0. Released v1.1.0. +% Domain : Boolean Algebra +% Problem : Multiplication is idempotent (X * X = X) +% Version : [Ver94] (equality) axioms. +% English : + +% Refs : [Ver94] Veroff (1994), Problem Set +% Source : [Ver94] +% Names : TA [Ver94] + +% Status : Unsatisfiable +% Rating : 0.10 v5.5.0, 0.05 v5.4.0, 0.00 v2.1.0, 0.13 v2.0.0 +% Syntax : Number of clauses : 9 ( 0 non-Horn; 9 unit; 1 RR) +% Number of atoms : 9 ( 9 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 6 ( 3 constant; 0-2 arity) +% Number of variables : 14 ( 0 singleton) +% Maximal term depth : 3 ( 2 average) +% SPC : CNF_UNS_RFO_PEQ_UEQ + +% Comments : +%-------------------------------------------------------------------------- +%----Include boolean algebra axioms for equality formulation +include('Axioms/BOO004-0.ax'). +%-------------------------------------------------------------------------- +cnf(prove_a_times_a_is_a,negated_conjecture, + ( multiply(a,a) != a )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/BOO027-1.p b/test/regress/regress0/tptp/BOO027-1.p new file mode 100644 index 000000000..a3cd4224c --- /dev/null +++ b/test/regress/regress0/tptp/BOO027-1.p @@ -0,0 +1,48 @@ +%-------------------------------------------------------------------------- +% File : BOO027-1 : TPTP v5.5.0. Released v2.2.0. +% Domain : Boolean Algebra +% Problem : Independence of self-dual 2-basis. +% Version : [MP96] (eqiality) axioms : Especial. +% English : Show that half of the self-dual 2-basis in DUAL-BA-3 is not +% a basis for Boolean Algebra. + +% Refs : [McC98] McCune (1998), Email to G. Sutcliffe +% : [MP96] McCune & Padmanabhan (1996), Automated Deduction in Eq +% Source : [McC98] +% Names : DUAL-BA-4 [MP96] + +% Status : Satisfiable +% Rating : 0.00 v5.5.0, 0.20 v5.4.0, 0.25 v5.3.0, 0.33 v5.2.0, 0.00 v3.2.0, 0.33 v3.1.0, 0.00 v2.2.1 +% Syntax : Number of clauses : 6 ( 0 non-Horn; 6 unit; 1 RR) +% Number of atoms : 6 ( 6 equality) +% Maximal clause size : 1 ( 1 average) +% Number of predicates : 1 ( 0 propositional; 2-2 arity) +% Number of functors : 5 ( 2 constant; 0-2 arity) +% Number of variables : 10 ( 0 singleton) +% Maximal term depth : 5 ( 3 average) +% SPC : CNF_SAT_RFO_PEQ_UEQ + +% Comments : There is a 2-element model. +%-------------------------------------------------------------------------- +%----Two properties of Boolean algebra: +cnf(multiply_add_property,axiom, + ( multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) )). + +cnf(additive_inverse,axiom, + ( add(X,inverse(X)) = one )). + +%----Pixley properties: +cnf(pixley1,axiom, + ( add(multiply(X,inverse(X)),add(multiply(X,Y),multiply(inverse(X),Y))) = Y )). + +cnf(pixley2,axiom, + ( add(multiply(X,inverse(Y)),add(multiply(X,Y),multiply(inverse(Y),Y))) = X )). + +cnf(pixley3,axiom, + ( add(multiply(X,inverse(Y)),add(multiply(X,X),multiply(inverse(Y),X))) = X )). + +%----Denial of a property of Boolean Algebra: +cnf(prove_idempotence,negated_conjecture, + ( add(a,a) != a )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/DAT001=1.p b/test/regress/regress0/tptp/DAT001=1.p new file mode 100644 index 000000000..922a6cfc3 --- /dev/null +++ b/test/regress/regress0/tptp/DAT001=1.p @@ -0,0 +1,57 @@ +%------------------------------------------------------------------------------ +% File : DAT001=1 : TPTP v5.5.0. Released v5.0.0. +% Domain : Data Structures +% Problem : Recursive list sort +% Version : Especial. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : 0.12 v5.5.0, 0.25 v5.4.0, 0.38 v5.3.0, 0.29 v5.2.0, 0.20 v5.1.0, 0.25 v5.0.0 +% Syntax : Number of formulae : 8 ( 5 unit; 4 type) +% Number of atoms : 13 ( 0 equality) +% Maximal formula depth : 6 ( 3 average) +% Number of connectives : 2 ( 0 ~; 0 |; 1 &) +% ( 0 <=>; 1 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 3 ( 2 >; 1 *; 0 +; 0 <<) +% Number of predicates : 9 ( 7 propositional; 0-2 arity) +% Number of functors : 7 ( 6 constant; 0-2 arity) +% Number of variables : 4 ( 0 sgn; 4 !; 0 ?) +% Maximal term depth : 6 ( 2 average) +% Arithmetic symbols : 7 ( 2 pred; 0 func; 5 numbers) +% SPC : TFF_THM_NEQ_ARI + +% Comments : +%------------------------------------------------------------------------------ +tff(list_type,type,( + list: $tType )). + +tff(nil_type,type,( + nil: list )). + +tff(mycons_type,type,( + mycons: ( $int * list ) > list )). + +tff(sorted_type,type,( + sorted: list > $o )). + +tff(empty_is_sorted,axiom,( + sorted(nil) )). + +tff(single_is_sorted,axiom,( + ! [X: $int] : sorted(mycons(X,nil)) )). + +tff(recursive_sort,axiom,( + ! [X: $int,Y: $int,R: list] : + ( ( $less(X,Y) + & sorted(mycons(Y,R)) ) + => sorted(mycons(X,mycons(Y,R))) ) )). + +tff(check_list,conjecture,( + sorted(mycons(1,mycons(2,mycons(4,mycons(7,mycons(100,nil)))))) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/KRS018+1.p b/test/regress/regress0/tptp/KRS018+1.p new file mode 100644 index 000000000..91039877b --- /dev/null +++ b/test/regress/regress0/tptp/KRS018+1.p @@ -0,0 +1,55 @@ +%------------------------------------------------------------------------------ +% File : KRS018+1 : TPTP v5.5.0. Released v3.1.0. +% Domain : Knowledge Representation (Semantic Web) +% Problem : Nothing can be defined using OWL Lite restrictions +% Version : Especial. +% English : + +% Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe +% : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW +% Source : [Bec03] +% Names : consistent_I5.2-Manifest001 [Bec03] + +% Status : Satisfiable +% Rating : 0.00 v4.1.0, 0.25 v4.0.1, 0.00 v3.1.0 +% Syntax : Number of formulae : 4 ( 0 unit) +% Number of atoms : 8 ( 0 equality) +% Maximal formula depth : 5 ( 4 average) +% Number of connectives : 7 ( 3 ~ ; 0 |; 1 &) +% ( 1 <=>; 2 =>; 0 <=) +% ( 0 <~>; 0 ~|; 0 ~&) +% Number of predicates : 6 ( 0 propositional; 1-2 arity) +% Number of functors : 0 ( 0 constant; --- arity) +% Number of variables : 6 ( 0 singleton; 4 !; 2 ?) +% Maximal term depth : 1 ( 1 average) +% SPC : FOF_SAT_RFO_NEQ + +% Comments : Sean Bechhofer says there are some errors in the encoding of +% datatypes, so this problem may not be perfect. At least it's +% still representative of the type of reasoning required for OWL. +%------------------------------------------------------------------------------ +%----Thing and Nothing +fof(axiom_0,axiom, + ( ! [X] : + ( cowlThing(X) + & ~ cowlNothing(X) ) )). + +%----String and Integer disjoint +fof(axiom_1,axiom, + ( ! [X] : + ( xsd_string(X) + <=> ~ xsd_integer(X) ) )). + +%----Super cNothing +fof(axiom_2,axiom, + ( ! [X] : + ( cNothing(X) + => ~ ( ? [Y] : rp(X,Y) ) ) )). + +%----Super cNothing +fof(axiom_3,axiom, + ( ! [X] : + ( cNothing(X) + => ? [Y0] : rp(X,Y0) ) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/KRS063+1.p b/test/regress/regress0/tptp/KRS063+1.p new file mode 100644 index 000000000..737741dee --- /dev/null +++ b/test/regress/regress0/tptp/KRS063+1.p @@ -0,0 +1,181 @@ +%------------------------------------------------------------------------------ +% File : KRS063+1 : TPTP v5.5.0. Released v3.1.0. +% Domain : Knowledge Representation (Semantic Web) +% Problem : An example combining owl:oneOf and owl:inverseOf +% Version : Especial. +% English : + +% Refs : [Bec03] Bechhofer (2003), Email to G. Sutcliffe +% : [TR+04] Tsarkov et al. (2004), Using Vampire to Reason with OW +% Source : [Bec03] +% Names : inconsistent_I4.5-Manifest002 [Bec03] + +% Status : Unsatisfiable +% Rating : 0.00 v3.1.0 +% Syntax : Number of formulae : 27 ( 9 unit) +% Number of atoms : 63 ( 18 equality) +% Maximal formula depth : 8 ( 4 average) +% Number of connectives : 39 ( 3 ~ ; 5 |; 14 &) +% ( 4 <=>; 13 =>; 0 <=) +% ( 0 <~>; 0 ~|; 0 ~&) +% Number of predicates : 11 ( 0 propositional; 1-2 arity) +% Number of functors : 7 ( 7 constant; 0-0 arity) +% Number of variables : 37 ( 0 singleton; 36 !; 1 ?) +% Maximal term depth : 1 ( 1 average) +% SPC : FOF_UNS_RFO_SEQ + +% Comments : Sean Bechhofer says there are some errors in the encoding of +% datatypes, so this problem may not be perfect. At least it's +% still representative of the type of reasoning required for OWL. +%------------------------------------------------------------------------------ +fof(cEUCountry_substitution_1,axiom, + ( ! [A,B] : + ( ( A = B + & cEUCountry(A) ) + => cEUCountry(B) ) )). + +fof(cEuroMP_substitution_1,axiom, + ( ! [A,B] : + ( ( A = B + & cEuroMP(A) ) + => cEuroMP(B) ) )). + +fof(cEuropeanCountry_substitution_1,axiom, + ( ! [A,B] : + ( ( A = B + & cEuropeanCountry(A) ) + => cEuropeanCountry(B) ) )). + +fof(cPerson_substitution_1,axiom, + ( ! [A,B] : + ( ( A = B + & cPerson(A) ) + => cPerson(B) ) )). + +fof(cowlNothing_substitution_1,axiom, + ( ! [A,B] : + ( ( A = B + & cowlNothing(A) ) + => cowlNothing(B) ) )). + +fof(cowlThing_substitution_1,axiom, + ( ! [A,B] : + ( ( A = B + & cowlThing(A) ) + => cowlThing(B) ) )). + +fof(rhasEuroMP_substitution_1,axiom, + ( ! [A,B,C] : + ( ( A = B + & rhasEuroMP(A,C) ) + => rhasEuroMP(B,C) ) )). + +fof(rhasEuroMP_substitution_2,axiom, + ( ! [A,B,C] : + ( ( A = B + & rhasEuroMP(C,A) ) + => rhasEuroMP(C,B) ) )). + +fof(risEuroMPFrom_substitution_1,axiom, + ( ! [A,B,C] : + ( ( A = B + & risEuroMPFrom(A,C) ) + => risEuroMPFrom(B,C) ) )). + +fof(risEuroMPFrom_substitution_2,axiom, + ( ! [A,B,C] : + ( ( A = B + & risEuroMPFrom(C,A) ) + => risEuroMPFrom(C,B) ) )). + +fof(xsd_integer_substitution_1,axiom, + ( ! [A,B] : + ( ( A = B + & xsd_integer(A) ) + => xsd_integer(B) ) )). + +fof(xsd_string_substitution_1,axiom, + ( ! [A,B] : + ( ( A = B + & xsd_string(A) ) + => xsd_string(B) ) )). + +%----Thing and Nothing +fof(axiom_0,axiom, + ( ! [X] : + ( cowlThing(X) + & ~ cowlNothing(X) ) )). + +%----String and Integer disjoint +fof(axiom_1,axiom, + ( ! [X] : + ( xsd_string(X) + <=> ~ xsd_integer(X) ) )). + +%----Enumeration cEUCountry +fof(axiom_2,axiom, + ( ! [X] : + ( cEUCountry(X) + <=> ( X = iPT + | X = iBE + | X = iNL + | X = iES + | X = iFR + | X = iUK ) ) )). + +%----Equality cEuroMP +fof(axiom_3,axiom, + ( ! [X] : + ( cEuroMP(X) + <=> ? [Y] : + ( risEuroMPFrom(X,Y) + & cowlThing(Y) ) ) )). + +%----Domain: rhasEuroMP +fof(axiom_4,axiom, + ( ! [X,Y] : + ( rhasEuroMP(X,Y) + => cEUCountry(X) ) )). + +%----Inverse: risEuroMPFrom +fof(axiom_5,axiom, + ( ! [X,Y] : + ( risEuroMPFrom(X,Y) + <=> rhasEuroMP(Y,X) ) )). + +%----iBE +fof(axiom_6,axiom, + ( cEuropeanCountry(iBE) )). + +%----iES +fof(axiom_7,axiom, + ( cEuropeanCountry(iES) )). + +%----iFR +fof(axiom_8,axiom, + ( cEuropeanCountry(iFR) )). + +%----iKinnock +fof(axiom_9,axiom, + ( cPerson(iKinnock) )). + +%----iKinnock +fof(axiom_10,axiom, + ( ~ cEuroMP(iKinnock) )). + +%----iNL +fof(axiom_11,axiom, + ( cEuropeanCountry(iNL) )). + +%----iPT +fof(axiom_12,axiom, + ( cEuropeanCountry(iPT) )). + +%----iUK +fof(axiom_13,axiom, + ( cEuropeanCountry(iUK) )). + +fof(axiom_14,axiom, + ( rhasEuroMP(iUK,iKinnock) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/MGT019+2.p b/test/regress/regress0/tptp/MGT019+2.p new file mode 100644 index 000000000..fb2cd7f62 --- /dev/null +++ b/test/regress/regress0/tptp/MGT019+2.p @@ -0,0 +1,84 @@ +%-------------------------------------------------------------------------- +% File : MGT019+2 : TPTP v5.5.0. Released v2.0.0. +% Domain : Management (Organisation Theory) +% Problem : Growth rate of EPs exceeds that of FMs in stable environments +% Version : [PM93] axioms. +% English : The growth rate of efficent producers exceeds the growth rate +% of first movers past a certain time in stable environments. + +% Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg +% : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg +% : [PB+94] Peli et al. (1994), A Logical Approach to Formalizing +% Source : [PM93] +% Names : LEMMA 1 [PM93] +% : L1 [PB+94] + +% Status : CounterSatisfiable +% Rating : 0.00 v4.1.0, 0.20 v4.0.1, 0.00 v3.5.0, 0.33 v3.4.0, 0.00 v2.1.0 +% Syntax : Number of formulae : 5 ( 0 unit) +% Number of atoms : 21 ( 1 equality) +% Maximal formula depth : 8 ( 6 average) +% Number of connectives : 17 ( 1 ~ ; 1 |; 8 &) +% ( 0 <=>; 7 =>; 0 <=) +% ( 0 <~>; 0 ~|; 0 ~&) +% Number of predicates : 7 ( 0 propositional; 1-4 arity) +% Number of functors : 5 ( 2 constant; 0-2 arity) +% Number of variables : 11 ( 0 singleton; 9 !; 2 ?) +% Maximal term depth : 2 ( 1 average) +% SPC : FOF_CSA_RFO_SEQ + +% Comments : There is no MGT019+1 as Kamps did not send it to me. +%-------------------------------------------------------------------------- +%----Subsitution axioms +%----Problem axioms +%----L2. The disbanding rate of first movers exceeds the disbanding +%----rate of efficient producers. +fof(l2,axiom, + ( ~ ( ! [E,T] : + ( ( environment(E) + & subpopulations(first_movers,efficient_producers,E,T) ) + => greater(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T)) ) ) )). + +%----If EP have lower disbanding rate and not lower founding rate than +%----FM, then EP have higher growth rate. +fof(mp_EP_lower_disbanding_rate,axiom, + ( ! [T] : + ( ( greater(disbanding_rate(first_movers,T),disbanding_rate(efficient_producers,T)) + & greater_or_equal(founding_rate(efficient_producers,T),founding_rate(first_movers,T)) ) + => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) )). + +%----MP. on "greater or equal to" +fof(mp_greater_or_equal,axiom, + ( ! [X,Y] : + ( greater_or_equal(X,Y) + => ( greater(X,Y) + | X = Y ) ) )). + +%----A8. The founding rate of first movers does not exceed the founding +%----rate of efficient producers past a certain point in a stable +%----environment. +fof(a8,hypothesis, + ( ! [E] : + ( ( environment(E) + & stable(E) ) + => ? [To] : + ( in_environment(E,To) + & ! [T] : + ( ( subpopulations(first_movers,efficient_producers,E,T) + & greater_or_equal(T,To) ) + => greater_or_equal(founding_rate(efficient_producers,T),founding_rate(first_movers,T)) ) ) ) )). + +%----GOAL: L1. The growth rate of efficient producers exceeds the growth +%----rate of first movers past a certain time in stable environments. +fof(prove_l1,conjecture, + ( ! [E] : + ( ( environment(E) + & stable(E) ) + => ? [To] : + ( in_environment(E,To) + & ! [T] : + ( ( subpopulations(first_movers,efficient_producers,E,T) + & greater_or_equal(T,To) ) + => greater(growth_rate(efficient_producers,T),growth_rate(first_movers,T)) ) ) ) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/MGT031-1.p b/test/regress/regress0/tptp/MGT031-1.p new file mode 100644 index 000000000..f5cd1937e --- /dev/null +++ b/test/regress/regress0/tptp/MGT031-1.p @@ -0,0 +1,95 @@ +%-------------------------------------------------------------------------- +% File : MGT031-1 : TPTP v5.5.0. Released v2.4.0. +% Domain : Management (Organisation Theory) +% Problem : First movers appear first in an environment +% Version : [PB+94] axioms : Reduced & Augmented > Complete. +% English : + +% Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg +% : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg +% : [Kam95] Kamps (1995), Email to G. Sutcliffe +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 0.00 v2.5.0, 0.17 v2.4.0 +% Syntax : Number of clauses : 15 ( 2 non-Horn; 3 unit; 15 RR) +% Number of atoms : 38 ( 5 equality) +% Maximal clause size : 5 ( 3 average) +% Number of predicates : 6 ( 0 propositional; 1-3 arity) +% Number of functors : 10 ( 6 constant; 0-2 arity) +% Number of variables : 23 ( 0 singleton) +% Maximal term depth : 3 ( 1 average) +% SPC : CNF_SAT_RFO_EQU_NUE + +% Comments : Created with tptp2X -f tptp -t clausify:otter MGT031+1.p +%-------------------------------------------------------------------------- +cnf(mp_positive_number_when_appear_20,axiom, + ( ~ environment(A) + | greater(number_of_organizations(e,appear(an_organisation,A)),zero) )). + +cnf(mp_number_mean_non_empty_21,axiom, + ( ~ environment(A) + | ~ greater(number_of_organizations(A,B),zero) + | subpopulation(sk1(B,A),A,B) )). + +cnf(mp_number_mean_non_empty_22,axiom, + ( ~ environment(A) + | ~ greater(number_of_organizations(A,B),zero) + | greater(cardinality_at_time(sk1(B,A),B),zero) )). + +cnf(mp_no_EP_before_appearance_23,axiom, + ( ~ environment(A) + | ~ in_environment(A,B) + | ~ greater(appear(efficient_producers,A),B) + | ~ greater(cardinality_at_time(efficient_producers,B),zero) )). + +cnf(mp_no_FM_before_appearance_24,axiom, + ( ~ environment(A) + | ~ in_environment(A,B) + | ~ greater(appear(first_movers,A),B) + | ~ greater(cardinality_at_time(first_movers,B),zero) )). + +cnf(mp_FM_not_precede_first_25,axiom, + ( ~ environment(A) + | greater_or_equal(appear(first_movers,A),appear(an_organisation,A)) )). + +cnf(mp_greater_transitivity_26,axiom, + ( ~ greater(A,B) + | ~ greater(B,C) + | greater(A,C) )). + +cnf(mp_greater_or_equal_27,axiom, + ( ~ greater_or_equal(A,B) + | greater(A,B) + | A = B )). + +cnf(mp_greater_or_equal_28,axiom, + ( ~ greater(A,B) + | greater_or_equal(A,B) )). + +cnf(mp_greater_or_equal_29,axiom, + ( A != B + | greater_or_equal(A,B) )). + +cnf(a9_30,hypothesis, + ( ~ environment(A) + | ~ subpopulation(B,A,C) + | ~ greater(cardinality_at_time(B,C),zero) + | B = efficient_producers + | B = first_movers )). + +cnf(a13_31,hypothesis, + ( ~ environment(A) + | greater(appear(efficient_producers,e),appear(first_movers,A)) )). + +cnf(prove_l13_32,negated_conjecture, + ( environment(sk2) )). + +cnf(prove_l13_33,negated_conjecture, + ( in_environment(sk2,appear(an_organisation,sk2)) )). + +cnf(prove_l13_34,negated_conjecture, + ( appear(an_organisation,sk2) != appear(first_movers,sk2) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/MGT041-2.p b/test/regress/regress0/tptp/MGT041-2.p new file mode 100644 index 000000000..a10a2f42d --- /dev/null +++ b/test/regress/regress0/tptp/MGT041-2.p @@ -0,0 +1,61 @@ +%-------------------------------------------------------------------------- +% File : MGT041-2 : TPTP v5.5.0. Released v2.4.0. +% Domain : Management (Organisation Theory) +% Problem : There are non-FM and non-EP organisations +% Version : [PM93] axioms. +% English : There are non-first mover and non-efficient producers +% organisations. + +% Refs : [PM93] Peli & Masuch (1993), The Logic of Propogation Strateg +% : [PM94] Peli & Masuch (1994), The Logic of Propogation Strateg +% : [Kam95] Kamps (1995), Email to G. Sutcliffe +% Source : [TPTP] +% Names : + +% Status : Unsatisfiable +% Rating : 0.00 v2.4.0 +% Syntax : Number of clauses : 8 ( 1 non-Horn; 4 unit; 8 RR) +% Number of atoms : 17 ( 0 equality) +% Maximal clause size : 4 ( 2 average) +% Number of predicates : 6 ( 0 propositional; 1-3 arity) +% Number of functors : 4 ( 4 constant; 0-0 arity) +% Number of variables : 8 ( 1 singleton) +% Maximal term depth : 1 ( 1 average) +% SPC : CNF_UNS_EPR + +% Comments : Created with tptp2X -f tptp -t clausify:otter MGT041+2.p +%-------------------------------------------------------------------------- +cnf(mp_not_high_and_low_1,axiom, + ( ~ number_of_routines(A,B,low) + | ~ number_of_routines(A,B,high) )). + +cnf(a14_2,hypothesis, + ( ~ organisation_at_time(A,B) + | ~ efficient_producer(A) + | ~ founding_time(A,B) + | has_elaborated_routines(A,B) )). + +cnf(a15_3,hypothesis, + ( ~ organisation_at_time(A,B) + | ~ first_mover(A) + | ~ founding_time(A,B) + | number_of_routines(A,B,low) )). + +cnf(a16_4,hypothesis, + ( organisation_at_time(sk1,sk2) )). + +cnf(a16_5,hypothesis, + ( founding_time(sk1,sk2) )). + +cnf(a16_6,hypothesis, + ( number_of_routines(sk1,sk2,high) )). + +cnf(a16_7,hypothesis, + ( ~ has_elaborated_routines(sk1,sk2) )). + +cnf(prove_t10_8,negated_conjecture, + ( ~ organisation_at_time(A,B) + | first_mover(A) + | efficient_producer(A) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/Makefile b/test/regress/regress0/tptp/Makefile new file mode 100644 index 000000000..8c3909592 --- /dev/null +++ b/test/regress/regress0/tptp/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/tptp + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am new file mode 100644 index 000000000..130a9dc7c --- /dev/null +++ b/test/regress/regress0/tptp/Makefile.am @@ -0,0 +1,79 @@ +BINARY = cvc4 +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +# escape the `=' in file names +equals = = + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + tptp_parser.p \ + tptp_parser2.p \ + tptp_parser3.p \ + tptp_parser4.p \ + tptp_parser5.p \ + tptp_parser6.p \ + tptp_parser7.p \ + tptp_parser8.p \ + tptp_parser9.p \ + tptp_parser10.p \ + tff0.p \ + tff0-arith.p \ + ARI086$(equals)1.p \ + BOO003-4.p \ + DAT001$(equals)1.p \ + KRS018+1.p \ + KRS063+1.p \ + MGT019+2.p \ + MGT041-2.p \ + PUZ131_1.p \ + SYN000+1.p \ + SYN000+2.p \ + SYN000-1.p \ + SYN000-2.p \ + SYN000$(equals)2.p \ + SYN000_1.p \ + SYN000_2.p \ + SYN075-1.p + +# axiom files required for the above tests +TEST_DEPS_DIST = \ + Axioms/BOO004-0.ax \ + Axioms/SYN000_0.ax \ + Axioms/SYN000-0.ax \ + Axioms/SYN000+0.ax + +# these take too long at present +EXTRA_DIST = $(TESTS) \ + $(TEST_DEPS_DIST) \ + BOO027-1.p \ + MGT031-1.p \ + NLP114-1.p \ + SYN075+1.p + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/tptp/NLP114-1.p b/test/regress/regress0/tptp/NLP114-1.p new file mode 100644 index 000000000..cf5bd272a --- /dev/null +++ b/test/regress/regress0/tptp/NLP114-1.p @@ -0,0 +1,202 @@ +%-------------------------------------------------------------------------- +% File : NLP114-1 : TPTP v5.5.0. Released v2.4.0. +% Domain : Natural Language Processing +% Problem : An old dirty white Chevy, problem 1 +% Version : [Bos00b] axioms. +% English : Eliminating logically equivalent interpretations in the statement +% "An old dirty white chevy barrels down a lonely street in +% hollywood." + +% Refs : [Bos00a] Bos (2000), DORIS: Discourse Oriented Representation a +% [Bos00b] Bos (2000), Applied Theorem Proving - Natural Language +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 0.00 v2.4.0 +% Syntax : Number of clauses : 36 ( 16 non-Horn; 2 unit; 36 RR) +% Number of atoms : 102 ( 0 equality) +% Maximal clause size : 18 ( 3 average) +% Number of predicates : 18 ( 1 propositional; 0-3 arity) +% Number of functors : 11 ( 11 constant; 0-0 arity) +% Number of variables : 11 ( 0 singleton) +% Maximal term depth : 1 ( 1 average) +% SPC : CNF_SAT_EPR + +% Comments : Created from NLP114+1.p using FLOTTER +%-------------------------------------------------------------------------- +cnf(clause1,negated_conjecture, + ( actual_world(skc17) )). + +cnf(clause2,negated_conjecture, + ( actual_world(skc11) )). + +cnf(clause3,negated_conjecture, + ( ssSkC0 + | city(skc17,skc20) )). + +cnf(clause4,negated_conjecture, + ( ssSkC0 + | street(skc17,skc20) )). + +cnf(clause5,negated_conjecture, + ( ssSkC0 + | lonely(skc17,skc20) )). + +cnf(clause6,negated_conjecture, + ( ssSkC0 + | placename(skc17,skc21) )). + +cnf(clause7,negated_conjecture, + ( ssSkC0 + | hollywood_placename(skc17,skc21) )). + +cnf(clause8,negated_conjecture, + ( ssSkC0 + | event(skc17,skc18) )). + +cnf(clause9,negated_conjecture, + ( ssSkC0 + | present(skc17,skc18) )). + +cnf(clause10,negated_conjecture, + ( ssSkC0 + | barrel(skc17,skc18) )). + +cnf(clause11,negated_conjecture, + ( ssSkC0 + | old(skc17,skc19) )). + +cnf(clause12,negated_conjecture, + ( ssSkC0 + | dirty(skc17,skc19) )). + +cnf(clause13,negated_conjecture, + ( ssSkC0 + | white(skc17,skc19) )). + +cnf(clause14,negated_conjecture, + ( ssSkC0 + | chevy(skc17,skc19) )). + +cnf(clause15,negated_conjecture, + ( ~ ssSkC0 + | lonely(skc11,skc16) )). + +cnf(clause16,negated_conjecture, + ( ~ ssSkC0 + | street(skc11,skc16) )). + +cnf(clause17,negated_conjecture, + ( ~ ssSkC0 + | barrel(skc11,skc12) )). + +cnf(clause18,negated_conjecture, + ( ~ ssSkC0 + | present(skc11,skc12) )). + +cnf(clause19,negated_conjecture, + ( ~ ssSkC0 + | event(skc11,skc12) )). + +cnf(clause20,negated_conjecture, + ( ~ ssSkC0 + | hollywood_placename(skc11,skc14) )). + +cnf(clause21,negated_conjecture, + ( ~ ssSkC0 + | placename(skc11,skc14) )). + +cnf(clause22,negated_conjecture, + ( ~ ssSkC0 + | city(skc11,skc15) )). + +cnf(clause23,negated_conjecture, + ( ~ ssSkC0 + | chevy(skc11,skc13) )). + +cnf(clause24,negated_conjecture, + ( ~ ssSkC0 + | white(skc11,skc13) )). + +cnf(clause25,negated_conjecture, + ( ~ ssSkC0 + | dirty(skc11,skc13) )). + +cnf(clause26,negated_conjecture, + ( ~ ssSkC0 + | old(skc11,skc13) )). + +cnf(clause27,negated_conjecture, + ( ssSkC0 + | down(skc17,skc18,skc20) )). + +cnf(clause28,negated_conjecture, + ( ssSkC0 + | in(skc17,skc18,skc20) )). + +cnf(clause29,negated_conjecture, + ( ssSkC0 + | of(skc17,skc21,skc20) )). + +cnf(clause30,negated_conjecture, + ( ssSkC0 + | agent(skc17,skc18,skc19) )). + +cnf(clause31,negated_conjecture, + ( ~ ssSkC0 + | down(skc11,skc12,skc16) )). + +cnf(clause32,negated_conjecture, + ( ~ ssSkC0 + | in(skc11,skc12,skc15) )). + +cnf(clause33,negated_conjecture, + ( ~ ssSkC0 + | of(skc11,skc14,skc15) )). + +cnf(clause34,negated_conjecture, + ( ~ ssSkC0 + | agent(skc11,skc12,skc13) )). + +cnf(clause35,negated_conjecture, + ( ~ down(U,V,W) + | ~ lonely(U,W) + | ~ street(U,W) + | ~ barrel(U,V) + | ~ present(U,V) + | ~ event(U,V) + | ~ hollywood_placename(U,X) + | ~ placename(U,X) + | ~ in(U,V,Y) + | ~ city(U,Y) + | ~ of(U,X,Y) + | ~ chevy(U,Z) + | ~ white(U,Z) + | ~ dirty(U,Z) + | ~ old(U,Z) + | ~ agent(U,V,Z) + | ~ actual_world(U) + | ssSkC0 )). + +cnf(clause36,negated_conjecture, + ( ~ city(U,V) + | ~ street(U,V) + | ~ lonely(U,V) + | ~ down(U,W,V) + | ~ in(U,W,V) + | ~ placename(U,X) + | ~ hollywood_placename(U,X) + | ~ of(U,X,V) + | ~ event(U,W) + | ~ present(U,W) + | ~ barrel(U,W) + | ~ agent(U,W,Y) + | ~ old(U,Y) + | ~ dirty(U,Y) + | ~ white(U,Y) + | ~ chevy(U,Y) + | ~ actual_world(U) + | ~ ssSkC0 )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/PUZ131_1.p b/test/regress/regress0/tptp/PUZ131_1.p new file mode 100644 index 000000000..b9e1c648b --- /dev/null +++ b/test/regress/regress0/tptp/PUZ131_1.p @@ -0,0 +1,100 @@ +%------------------------------------------------------------------------------ +% File : PUZ131_1 : TPTP v5.5.0. Released v5.0.0. +% Domain : Puzzles +% Problem : Victor teaches Michael +% Version : Especial. +% English : Every student is enrolled in at least one course. Every professor +% teaches at least one course. Every course has at least one student +% enrolled. Every course has at least one professor teaching. The +% coordinator of a course teaches the course. If a student is +% enroled in a course then the student is taught by every professor +% who teaches the course. Michael is enrolled in CSC410. Victor is +% the coordinator of CSC410. Therefore, Michael is taught by Victor. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : 0.00 v5.0.0 +% Syntax : Number of formulae : 19 ( 14 unit; 10 type) +% Number of atoms : 28 ( 1 equality) +% Maximal formula depth : 6 ( 3 average) +% Number of connectives : 2 ( 0 ~; 0 |; 0 &) +% ( 0 <=>; 2 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 7 ( 4 >; 3 *; 0 +; 0 <<) +% Number of predicates : 16 ( 12 propositional; 0-2 arity) +% Number of functors : 4 ( 3 constant; 0-1 arity) +% Number of variables : 12 ( 0 sgn; 8 !; 4 ?) +% Maximal term depth : 2 ( 1 average) +% SPC : TFF_THM_EQU_NAR + +% Comments : +%------------------------------------------------------------------------------ +tff(student_type,type,( + student: $tType )). + +tff(professor_type,type,( + professor: $tType )). + +tff(course_type,type,( + course: $tType )). + +tff(michael_type,type,( + michael: student )). + +tff(victor_type,type,( + victor: professor )). + +tff(csc410_type,type,( + csc410: course )). + +tff(enrolled_type,type,( + enrolled: ( student * course ) > $o )). + +tff(teaches_type,type,( + teaches: ( professor * course ) > $o )). + +tff(taught_by_type,type,( + taughtby: ( student * professor ) > $o )). + +tff(coordinator_of_type,type,( + coordinatorof: course > professor )). + +tff(student_enrolled_axiom,axiom,( + ! [X: student] : + ? [Y: course] : enrolled(X,Y) )). + +tff(professor_teaches,axiom,( + ! [X: professor] : + ? [Y: course] : teaches(X,Y) )). + +tff(course_enrolled,axiom,( + ! [X: course] : + ? [Y: student] : enrolled(Y,X) )). + +tff(course_teaches,axiom,( + ! [X: course] : + ? [Y: professor] : teaches(Y,X) )). + +tff(coordinator_teaches,axiom,( + ! [X: course] : teaches(coordinatorof(X),X) )). + +tff(student_enrolled_taught,axiom,( + ! [X: student,Y: course] : + ( enrolled(X,Y) + => ! [Z: professor] : + ( teaches(Z,Y) + => taughtby(X,Z) ) ) )). + +tff(michael_enrolled_csc410_axiom,axiom,( + enrolled(michael,csc410) )). + +tff(victor_coordinator_csc410_axiom,axiom,( + coordinatorof(csc410) = victor )). + +tff(teaching_conjecture,conjecture,( + taughtby(michael,victor) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000+1.p b/test/regress/regress0/tptp/SYN000+1.p new file mode 100644 index 000000000..682c11b69 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000+1.p @@ -0,0 +1,99 @@ +%------------------------------------------------------------------------------ +% File : SYN000+1 : TPTP v5.5.0. Released v4.0.0. +% Domain : Syntactic +% Problem : Basic TPTP FOF syntax +% Version : Biased. +% English : Basic TPTP FOF syntax that you can't survive without parsing. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : 0.43 v5.5.0, 0.48 v5.4.0, 0.46 v5.3.0, 0.52 v5.2.0, 0.40 v5.1.0, 0.43 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.1, 0.78 v4.0.0 +% Syntax : Number of formulae : 12 ( 5 unit) +% Number of atoms : 31 ( 3 equality) +% Maximal formula depth : 7 ( 4 average) +% Number of connectives : 28 ( 9 ~; 10 |; 3 &) +% ( 1 <=>; 3 =>; 1 <=) +% ( 1 <~>; 0 ~|; 0 ~&) +% Number of predicates : 16 ( 10 propositional; 0-3 arity) +% Number of functors : 8 ( 5 constant; 0-3 arity) +% Number of variables : 13 ( 0 sgn; 5 !; 8 ?) +% Maximal term depth : 4 ( 2 average) +% SPC : FOF_THM_RFO_SEQ + +% Comments : +%------------------------------------------------------------------------------ +%----Propositional +fof(propositional,axiom, + ( ( p0 + & ~ q0 ) + => ( r0 + | ~ s0 ) )). + +%----First-order +fof(first_order,axiom,( + ! [X] : + ( ( p(X) + | ~ q(X,a) ) + => ? [Y,Z] : + ( r(X,f(Y),g(X,f(Y),Z)) + & ~ s(f(f(f(b)))) ) ) )). + +%----Equality +fof(equality,axiom,( + ? [Y] : + ! [X,Z] : + ( f(Y) = g(X,f(Y),Z) + | f(f(f(b))) != a + | X = f(Y) ) )). + +%----True and false +fof(true_false,axiom, + ( $true + | $false )). + +%----Quoted symbols +fof(single_quoted,axiom, + ( 'A proposition' + | 'A predicate'(a) + | p('A constant') + | p('A function'(a)) + | p('A \'quoted \\ escape\'') )). + +%----Connectives - seen |, &, =>, ~ already +fof(useful_connectives,axiom,( + ! [X] : + ( ( p(X) + <= ~ q(X,a) ) + <=> ? [Y,Z] : + ( r(X,f(Y),g(X,f(Y),Z)) + <~> ~ s(f(f(f(b)))) ) ) )). + +%----Annotated formula names +fof(123,axiom,( + ! [X] : + ( ( p(X) + | ~ q(X,a) ) + => ? [Y,Z] : + ( r(X,f(Y),g(X,f(Y),Z)) + & ~ s(f(f(f(b)))) ) ) )). + +%----Roles +fof(role_hypothesis,hypothesis,( + p(h) )). + +fof(role_conjecture,conjecture,( + ? [X] : p(X) )). + +%----Include directive +include('Axioms/SYN000+0.ax'). + +%----Comments +/* This + is a block + comment. +*/ + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000+2.p b/test/regress/regress0/tptp/SYN000+2.p new file mode 100644 index 000000000..8c6f2f9f9 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000+2.p @@ -0,0 +1,127 @@ +%------------------------------------------------------------------------------ +% File : SYN000+2 : TPTP v5.5.0. Bugfixed v4.1.1. +% Domain : Syntactic +% Problem : Advanced TPTP FOF syntax +% Version : Biased. +% English : Advanced TPTP FOF syntax that you will encounter some time. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 0.50 v5.5.0, 0.67 v5.2.0, 1.00 v5.0.0 +% Syntax : Number of formulae : 20 ( 16 unit) +% Number of atoms : 31 ( 2 equality) +% Maximal formula depth : 7 ( 2 average) +% Number of connectives : 13 ( 2 ~; 9 |; 0 &) +% ( 0 <=>; 0 =>; 0 <=; 0 <~>) +% ( 1 ~|; 1 ~&) +% Number of predicates : 8 ( 3 propositional; 0-3 arity) +% Number of functors : 22 ( 20 constant; 0-3 arity) +% Number of variables : 8 ( 0 sgn; 8 !; 0 ?) +% Maximal term depth : 2 ( 1 average) +% Arithmetic symbols : 12 ( 0 pred; 0 func; 12 numbers) +% SPC : FOF_SAT_RFO_SEQ + +% Comments : +% Bugfixes : v4.0.1 - Added more numbers, particularly rationals. +% : v4.1.1 - Removed rationals with negative denominators. +%------------------------------------------------------------------------------ +%----Quoted symbols +fof(distinct_object,axiom,( + "An Apple" != "A \"Microsoft \\ escape\"" )). + +%----Numbers +fof(integers,axiom, + ( p(12) + | p(-12) )). + +fof(rationals,axiom, + ( p(123/456) + | p(-123/456) + | p(+123/456) )). + +fof(reals,axiom, + ( p(123.456 ) + | p(-123.456 ) + | p(123.456E789 ) + | p(123.456e789 ) + | p(-123.456E789 ) + | p(123.456E-789 ) + | p(-123.456E-789 ) )). + +%----Connectives - seen |, &, =>, ~ already +fof(never_used_connectives,axiom,( + ! [X] : + ( ( p(X) + ~| ~ q(X,a) ) + ~& p(X) ) )). + +%----Roles +fof(role_definition,definition,( + ! [X] : f(d) = f(X) )). + +fof(role_assumption,assumption,( + p(a) )). + +fof(role_lemma,lemma,( + p(l) )). + +fof(role_theorem,theorem,( + p(t) )). + +fof(role_unknown,unknown,( + p(u) )). + +%----Selective include directive +include('Axioms/SYN000+0.ax',[ia1,ia3]). + +%----Source +fof(source_unknown,axiom,( + ! [X] : p(X) ), + unknown). + +fof(source,axiom,( + ! [X] : p(X) ), + file('SYN000-1.p')). + +fof(source_name,axiom,( + ! [X] : p(X) ), + file('SYN000-1.p',source_unknown)). + +fof(source_copy,axiom,( + ! [X] : p(X) ), + source_unknown). + +fof(source_introduced_assumption,axiom,( + ! [X] : p(X) ), + introduced(assumption,[from,the,world])). + +fof(source_inference,plain,( + p(a) ), + inference(magic, + [status(thm),assumptions([source_introduced_assumption])], + [theory(equality),source_unknown])). + +fof(source_inference_with_bind,plain,( + p(a) ), + inference(magic, + [status(thm)], + [theory(equality),source_unknown:[bind(X,$fot(a))]])). + +%----Useful info +fof(useful_info,axiom,( + ! [X] : p(X) ), + unknown, + [simple, + prolog(like,Data,[nested,12.2]), + AVariable, + 12.2, + "A distinct object", + $fof(p(X) | ~ q(X,a) | r(X,f(Y),g(X,f(Y),Z)) | ~ s(f(f(f(b))))), + data(name):[colon,list,2], + [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2] + ]). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000-1.p b/test/regress/regress0/tptp/SYN000-1.p new file mode 100644 index 000000000..b6a68ec95 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000-1.p @@ -0,0 +1,83 @@ +%------------------------------------------------------------------------------ +% File : SYN000-1 : TPTP v5.5.0. Released v4.0.0. +% Domain : Syntactic +% Problem : Basic TPTP CNF syntax +% Version : Biased. +% English : Basic TPTP CNF syntax that you can't survive without parsing. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Unsatisfiable +% Rating : 0.50 v5.4.0, 0.55 v5.3.0, 0.56 v5.2.0, 0.62 v5.1.0, 0.65 v5.0.0, 0.64 v4.1.0, 0.62 v4.0.1, 0.64 v4.0.0 +% Syntax : Number of clauses : 11 ( 6 non-Horn; 5 unit; 7 RR) +% Number of atoms : 27 ( 3 equality) +% Maximal clause size : 5 ( 2 average) +% Number of predicates : 16 ( 10 propositional; 0-3 arity) +% Number of functors : 8 ( 5 constant; 0-3 arity) +% Number of variables : 11 ( 5 singleton) +% Maximal term depth : 4 ( 2 average) +% SPC : CNF_UNS_RFO_SEQ_NHN + +% Comments : +%------------------------------------------------------------------------------ +%----Propositional +cnf(propositional,axiom, + ( p0 + | ~ q0 + | r0 + | ~ s0 )). + +%----First-order +cnf(first_order,axiom, + ( p(X) + | ~ q(X,a) + | r(X,f(Y),g(X,f(Y),Z)) + | ~ s(f(f(f(b)))) )). + +%----Equality +cnf(equality,axiom, + ( f(Y) = g(X,f(Y),Z) + | f(f(f(b))) != a + | X = f(Y) )). + +%----True and false +cnf(true_false,axiom, + ( $true + | $false )). + +%----Quoted symbols +cnf(single_quoted,axiom, + ( 'A proposition' + | 'A predicate'(Y) + | p('A constant') + | p('A function'(a)) + | p('A \'quoted \\ escape\'') )). + +%----Connectives - seen them all already + +%----Annotated formula names +cnf(123,axiom, + ( p(X) + | ~ q(X,a) + | r(X,f(Y),g(X,f(Y),Z)) + | ~ s(f(f(f(b)))) )). + +%----Roles - seen axiom already +cnf(role_hypothesis,hypothesis, + p(h)). + +cnf(role_negated_conjecture,negated_conjecture, + ~ p(X)). + +%----Include directive +include('Axioms/SYN000-0.ax'). + +%----Comments +/* This + is a block + comment. +*/ + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000-2.p b/test/regress/regress0/tptp/SYN000-2.p new file mode 100644 index 000000000..0c6c0b59f --- /dev/null +++ b/test/regress/regress0/tptp/SYN000-2.p @@ -0,0 +1,117 @@ +%------------------------------------------------------------------------------ +% File : SYN000-2 : TPTP v5.5.0. Bugfixed v4.1.1. +% Domain : Syntactic +% Problem : Advanced TPTP CNF syntax +% Version : Biased. +% English : Advanced TPTP CNF syntax that you will encounter some time. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : 1.00 v5.4.0, 0.90 v5.3.0, 0.89 v5.2.0, 0.90 v5.0.0 +% Syntax : Number of clauses : 19 ( 3 non-Horn; 16 unit; 12 RR) +% Number of atoms : 28 ( 2 equality) +% Maximal clause size : 7 ( 1 average) +% Number of predicates : 8 ( 3 propositional; 0-3 arity) +% Number of functors : 22 ( 20 constant; 0-3 arity) +% Number of variables : 7 ( 7 singleton) +% Maximal term depth : 2 ( 1 average) +% Arithmetic symbols : 12 ( 0 pred; 0 func; 12 numbers) +% SPC : CNF_SAT_RFO_EQU_NUE + +% Comments : +% Bugfixes : v4.0.1 - Added more numbers, particularly rationals. +% : v4.1.1 - Removed rationals with negative denominators. +%------------------------------------------------------------------------------ +%----Quoted symbols +cnf(distinct_object,axiom, + ( "An Apple" != "A \"Microsoft \\ escape\"" )). + +%----Numbers +cnf(integers,axiom, + ( p(12) + | p(-12) )). + +cnf(rationals,axiom, + ( p(123/456) + | p(-123/456) + | p(+123/456) )). + +cnf(reals,axiom, + ( p(123.456 ) + | p(-123.456 ) + | p(123.456E789 ) + | p(123.456e789 ) + | p(-123.456E789 ) + | p(123.456E-789 ) + | p(-123.456E-789 ) )). + +%----Roles - seen axiom already +cnf(role_definition,definition, + f(d) = f(X) ). + +cnf(role_assumption,assumption, + p(a) ). + +cnf(role_lemma,lemma, + p(l) ). + +cnf(role_theorem,theorem, + p(t) ). + +cnf(role_unknown,unknown, + p(u) ). + +%----Selective include directive +include('Axioms/SYN000-0.ax',[ia1,ia3]). + +%----Source +cnf(source_unknown,axiom, + p(X), + unknown). + +cnf(source,axiom, + p(X), + file('SYN000-1.p')). + +cnf(source_name,axiom, + p(X), + file('SYN000-1.p',source_unknown)). + +cnf(source_copy,axiom, + p(X), + source_unknown). + +cnf(source_introduced_assumption,axiom, + p(X), + introduced(assumption,[from,the,world])). + +cnf(source_inference,plain, + p(a), + inference(magic, + [status(thm),assumptions([source_introduced_assumption])], + [theory(equality),source_unknown]) ). + +cnf(source_inference_with_bind,plain, + p(a), + inference(magic, + [status(thm)], + [theory(equality),source_unknown:[bind(X,$fot(a))]]) ). + +%----Useful info +cnf(useful_info,axiom, + p(X), + unknown, + [simple, + prolog(like,Data,[nested,12.2]), + AVariable, + 12.2, + "A distinct object", + $cnf(p(X) | ~q(X,a) | r(X,f(Y),g(X,f(Y),Z)) | ~ s(f(f(f(b))))), + data(name):[colon,list,2], + [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2] + ]). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000=2.p b/test/regress/regress0/tptp/SYN000=2.p new file mode 100644 index 000000000..802613f4b --- /dev/null +++ b/test/regress/regress0/tptp/SYN000=2.p @@ -0,0 +1,309 @@ +%------------------------------------------------------------------------------ +% File : SYN000=2 : TPTP v5.5.0. Bugfixed v5.5.1. +% Domain : Syntactic +% Problem : TF0 syntax with arithmetic +% Version : Biased. +% English : + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : ? v5.5.1 +% Syntax : Number of formulae : 83 ( 73 unit; 6 type) +% Number of atoms : 100 ( 4 equality) +% Maximal formula depth : 7 ( 1 average) +% Number of connectives : 14 ( 0 ~; 10 |; 1 &) +% ( 0 <=>; 3 =>; 0 <=; 0 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 3 ( 3 >; 0 *; 0 +; 0 <<) +% Number of predicates : 20 ( 10 propositional; 0-2 arity) +% Number of functors : 41 ( 24 constant; 0-2 arity) +% Number of variables : 14 ( 1 sgn; 3 !; 11 ?) +% Maximal term depth : 3 ( 1 average) +% Arithmetic symbols : 37 ( 9 pred; 7 func; 21 numbers) +% SPC : TF0_THM_EQU_ARI + +% Comments : +% Bugfixes : v5.5.1 - Removed $evaleq. +%------------------------------------------------------------------------------ +%----Types for what follows +tff(p_int_type,type,( + p_int: $int > $o )). + +tff(p_rat_type,type,( + p_rat: $rat > $o )). + +tff(p_real_type,type,( + p_real: $real > $o )). + +tff(a_int,type,( + a_int: $int )). + +tff(a_rat,type,( + a_rat: $rat )). + +tff(a_real,type,( + a_real: $real )). + +%----Numbers +tff(integers,axiom, + ( p_int(123) + | p_int(-123) )). + +tff(rationals,axiom, + ( p_rat(123/456) + | p_rat(-123/456) + | p_rat(123/456) )). + +tff(reals,axiom, + ( p_real(123.456) + | p_real(-123.456) + | p_real(123.456E78) + | p_real(123.456e78) + | p_real(-123.456E78) + | p_real(123.456E-78) + | p_real(-123.456E-78) )). + +%----Variables +tff(variables_int,axiom,( + ! [X: $int] : + ? [Y: $int] : + ( p_int(X) + => p_int(Y) ) )). + +tff(variables_rat,axiom,( + ! [X: $rat] : + ? [Y: $rat] : + ( p_rat(X) + => p_rat(Y) ) )). + +tff(variables_real,axiom,( + ! [X: $real] : + ? [Y: $real] : + ( p_real(X) + => p_real(Y) ) )). + +%----Arithmetic relations +tff(less_int,axiom,( + $less(a_int,3) )). + +tff(less_rat,axiom,( + $less(a_rat,3/9) )). + +tff(less_real,axiom,( + $less(a_real,3.3) )). + +tff(lesseq_int,axiom,( + $lesseq(a_int,3) )). + +tff(lesseq_rat,axiom,( + $lesseq(a_rat,3/9) )). + +tff(lesseq_real,axiom,( + $lesseq(a_real,3.3) )). + +tff(greater_int,axiom,( + $greater(a_int,-3) )). + +tff(greater_rat,axiom,( + $greater(a_rat,-3/9) )). + +tff(greater_real,axiom,( + $greater(a_real,-3.3) )). + +tff(greatereq_int,axiom,( + $greatereq(a_int,-3) )). + +tff(greatereq_rat,axiom,( + $greatereq(a_rat,-3/9) )). + +tff(greatereq_real,axiom,( + $greatereq(a_real,-3.3) )). + +tff(equal_int,axiom,( + a_int = 0 )). + +tff(equal_rat,axiom,( + a_rat = 0/1 )). + +tff(equal_real,axiom,( + a_real = 0.0 )). + +%----Arithmetic functions +tff(uminus_int,axiom,( + p_int($uminus(3)) )). + +tff(uminus_rat,axiom,( + p_rat($uminus(3/9)) )). + +tff(uminus_real,axiom,( + p_real($uminus(3.3)) )). + +tff(sum_int,axiom,( + p_int($sum(3,3)) )). + +tff(sum_rat,axiom,( + p_rat($sum(3/9,3/9)) )). + +tff(sum_real,axiom,( + p_real($sum(3.3,3.3)) )). + +tff(difference_int,axiom,( + p_int($difference(3,3)) )). + +tff(difference_rat,axiom,( + p_rat($difference(3/9,3/9)) )). + +tff(difference_real,axiom,( + p_real($difference(3.3,3.3)) )). + +tff(product_int,axiom,( + p_int($product(3,3)) )). + +tff(product_rat,axiom,( + p_rat($product(3/9,3/9)) )). + +tff(product_real,axiom,( + p_real($product(3.3,3.3)) )). + +tff(quotient_rat,axiom,( + p_rat($quotient(3/9,3/9)) )). + +tff(quotient_real,axiom,( + p_real($quotient(3.3,3.3)) )). + +tff(quotient_e_int,axiom,( + p_int($quotient_e(3,3)) )). + +tff(quotient_e_rat,axiom,( + p_rat($quotient_e(3/9,3/9)) )). + +tff(quotient_e_real,axiom,( + p_real($quotient_e(3.3,3.3)) )). + +tff(quotient_t_int,axiom,( + p_int($quotient_t(3,3)) )). + +tff(quotient_t_rat,axiom,( + p_rat($quotient_t(3/9,3/9)) )). + +tff(quotient_t_real,axiom,( + p_real($quotient_t(3.3,3.3)) )). + +tff(quotient_f_int,axiom,( + p_int($quotient_f(3,3)) )). + +tff(quotient_f_rat,axiom,( + p_rat($quotient_f(3/9,3/9)) )). + +tff(quotient_f_real,axiom,( + p_real($quotient_f(3.3,3.3)) )). + +tff(remainder_e_int,axiom,( + p_int($remainder_e(3,3)) )). + +tff(remainder_e_rat,axiom,( + p_rat($remainder_e(3/9,3/9)) )). + +tff(remainder_e_real,axiom,( + p_real($remainder_e(3.3,3.3)) )). + +tff(remainder_t_int,axiom,( + p_int($remainder_t(3,3)) )). + +tff(remainder_t_rat,axiom,( + p_rat($remainder_t(3/9,3/9)) )). + +tff(remainder_t_real,axiom,( + p_real($remainder_t(3.3,3.3)) )). + +tff(remainder_f_int,axiom,( + p_int($remainder_f(3,3)) )). + +tff(remainder_f_rat,axiom,( + p_rat($remainder_f(3/9,3/9)) )). + +tff(remainder_f_real,axiom,( + p_real($remainder_f(3.3,3.3)) )). + +tff(floor_int,axiom,( + p_int($floor(3)) )). + +tff(floor_rat,axiom,( + p_rat($floor(3/9)) )). + +tff(floor_int,axiom,( + p_real($floor(3.3)) )). + +tff(ceiling_int,axiom,( + p_int($ceiling(3)) )). + +tff(ceiling_rat,axiom,( + p_rat($ceiling(3/9)) )). + +tff(ceiling_int,axiom,( + p_real($ceiling(3.3)) )). + +tff(truncate_int,axiom,( + p_int($truncate(3)) )). + +tff(truncate_rat,axiom,( + p_rat($truncate(3/9)) )). + +tff(truncate_int,axiom,( + p_real($truncate(3.3)) )). + +%----Recognizing numbers +tff(is_int_int,axiom,( + ? [X: $int] : $is_int(X) )). + +tff(is_int_rat,axiom,( + ? [X: $rat] : $is_int(X) )). + +tff(is_int_real,axiom,( + ? [X: $real] : $is_int(X) )). + +tff(is_rat_rat,axiom,( + ? [X: $rat] : $is_rat(X) )). + +tff(is_rat_real,axiom,( + ? [X: $real] : $is_rat(X) )). + +%----Coercion +tff(to_int_int,axiom,( + p_int($to_int(3)) )). + +tff(to_int_rat,axiom,( + p_int($to_int(3/9)) )). + +tff(to_int_real,axiom,( + p_int($to_int(3.3)) )). + +tff(to_rat_int,axiom,( + p_rat($to_rat(3)) )). + +tff(to_rat_rat,axiom,( + p_rat($to_rat(3/9)) )). + +tff(to_rat_real,axiom,( + p_rat($to_rat(3.3)) )). + +tff(to_real_int,axiom,( + p_real($to_real(3)) )). + +tff(to_real_rat,axiom,( + p_real($to_real(3/9)) )). + +tff(to_real_real,axiom,( + p_real($to_real(3.3)) )). + +%----A conjecture to prove +tff(mixed,conjecture,( + ? [X: $int,Y: $rat,Z: $real] : + ( Y = $to_rat($sum(X,2)) + & ( $less($to_int(Y),3) + | $greater($to_real(Y),3.3) ) ) )). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000_1.p b/test/regress/regress0/tptp/SYN000_1.p new file mode 100644 index 000000000..ed683c070 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000_1.p @@ -0,0 +1,170 @@ +%------------------------------------------------------------------------------ +% File : SYN000_1 : TPTP v5.5.0. Released v5.0.0. +% Domain : Syntactic +% Problem : Basic TPTP TFF syntax without arithmetic +% Version : Biased. +% English : Basic TPTP TFF syntax that you can't survive without parsing. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Theorem +% Rating : 0.40 v5.5.0, 0.25 v5.4.0, 0.33 v5.2.0, 0.67 v5.0.0 +% Syntax : Number of formulae : 38 ( 21 unit; 25 type) +% Number of atoms : 74 ( 3 equality) +% Maximal formula depth : 7 ( 3 average) +% Number of connectives : 28 ( 9 ~; 10 |; 3 &) +% ( 1 <=>; 3 =>; 1 <=; 1 <~>) +% ( 0 ~|; 0 ~&) +% Number of type conns : 17 ( 10 >; 7 *; 0 +; 0 <<) +% Number of predicates : 37 ( 30 propositional; 0-3 arity) +% Number of functors : 10 ( 6 constant; 0-3 arity) +% Number of variables : 14 ( 1 sgn; 6 !; 8 ?) +% Maximal term depth : 4 ( 2 average) +% SPC : TFF_THM_EQU_NAR + +% Comments : +%------------------------------------------------------------------------------ +%----Propositional +tff(p0_type,type,( + p0: $o )). + +tff(q0_type,type,( + q0: $o )). + +tff(r0_type,type,( + r0: $o )). + +tff(s0_type,type,( + s0: $o )). + +tff(propositional,axiom, + ( ( p0 + & ~ q0 ) + => ( r0 + | ~ s0 ) )). + +%----First-order +tff(a_type,type,( + a: $i )). + +tff(b_type,type,( + b: $i )). + +tff(h_type,type,( + h: $i )). + +tff(f_type,type,( + f: $i > $i )). + +tff(g_type,type,( + g: ( $i * $i * $i ) > $i )). + +tff(p_type,type,( + p: $i > $o )). + +tff(q_type,type,( + q: ( $i * $i ) > $o )). + +tff(r_type,type,( + r: ( $i * $i * $i ) > $o )). + +tff(s_type,type,( + s: $i > $o )). + +tff(first_order,axiom,( + ! [X: $i] : + ( ( p(X) + | ~ q(X,a) ) + => ? [Y: $i,Z: $i] : + ( r(X,f(Y),g(X,f(Y),Z)) + & ~ s(f(f(f(b)))) ) ) )). + +%----Equality +tff(equality,axiom,( + ? [Y: $i] : + ! [X: $i,Z: $i] : + ( f(Y) = g(X,f(Y),Z) + | f(f(f(b))) != a + | X = f(Y) ) )). + +%----True and false +tff(true_false,axiom, + ( $true + | $false )). + +tff(quoted_proposition_type,type,( + 'A proposition': $o )). + +tff(quoted_predicate_type,type,( + 'A predicate': $i > $o )). + +tff(quoted_constant_type,type,( + 'A constant': $i )). + +tff(quoted_function_type,type,( + 'A function': $i > $i )). + +tff(quoted_escape_type,type,( + 'A \'quoted \\ escape\'': $i )). + +%----Quoted symbols +tff(single_quoted,axiom, + ( 'A proposition' + | 'A predicate'(a) + | p('A constant') + | p('A function'(a)) + | p('A \'quoted \\ escape\'') )). + +%----Connectives - seen |, &, =>, ~ already +tff(useful_connectives,axiom,( + ! [X: $i] : + ( ( p(X) + <= ~ q(X,a) ) + <=> ? [Y: $i,Z: $i] : + ( r(X,f(Y),g(X,f(Y),Z)) + <~> ~ s(f(f(f(b)))) ) ) )). + +%----New types +tff(new_type,type,( + new: $tType )). + +tff(newc_type,type,( + newc: new )). + +tff(newf_type,type,( + newf: ( new * $i ) > new )). + +tff(newp_type,type,( + newp: ( new * $i ) > $o )). + +tff(new_axiom,axiom,( + ! [X: new] : newp(newf(newc,a),a) )). + +%----Annotated formula names +tff(123,axiom,( + ! [X: $i] : + ( ( p(X) + | ~ q(X,a) ) + => ? [Y: $i,Z: $i] : + ( r(X,f(Y),g(X,f(Y),Z)) + & ~ s(f(f(f(b)))) ) ) )). + +%----Roles +tff(role_hypothesis,hypothesis,( + p(h) )). + +tff(role_conjecture,conjecture,( + ? [X: $i] : p(X) )). + +%----Include directive +include('Axioms/SYN000_0.ax'). + +%----Comments +/* This + is a block + comment. +*/ + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN000_2.p b/test/regress/regress0/tptp/SYN000_2.p new file mode 100644 index 000000000..ece5fa6b1 --- /dev/null +++ b/test/regress/regress0/tptp/SYN000_2.p @@ -0,0 +1,135 @@ +%------------------------------------------------------------------------------ +% File : SYN000_2 : TPTP v5.5.0. Bugfixed v5.5.1. +% Domain : Syntactic +% Problem : Advanced TPTP TF0 syntax without arithmetic +% Version : Biased. +% English : Advanced TPTP TF0 syntax that you will encounter some time. + +% Refs : +% Source : [TPTP] +% Names : + +% Status : Satisfiable +% Rating : ? v5.5.1 +% Syntax : Number of formulae : 26 ( 18 unit; 7 type) +% Number of atoms : 42 ( 2 equality) +% Maximal formula depth : 5 ( 2 average) +% Number of connectives : 6 ( 2 ~; 0 |; 1 &) +% ( 1 <=>; 0 =>; 0 <=; 0 <~>) +% ( 1 ~|; 1 ~&) +% Number of type conns : 9 ( 5 >; 4 *; 0 +; 0 <<) +% Number of predicates : 14 ( 11 propositional; 0-2 arity) +% Number of functors : 6 ( 4 constant; 0-2 arity) +% Number of variables : 18 ( 0 sgn; 13 !; 1 ?) +% Maximal term depth : 2 ( 1 average) +% SPC : TF0_SAT_EQU_NAR + +% Comments : +% Bugfixes : v5.5.1 - Fixed let_binders. +%------------------------------------------------------------------------------ +%----Quoted symbols +tff(distinct_object,axiom,( + "An Apple" != "A \"Microsoft \\ escape\"" )). + +%----Types for stuff below +tff(a_type,type,( + a: $i )). + +tff(b_type,type,( + b: $i )). + +tff(f_type,type,( + f: $i > $i )). + +tff(g_type,type,( + g: ( $i * $i ) > $i )). + +tff(h_type,type,( + h: ( $i * $i * $i ) > $i )). + +tff(p_type,type,( + p: $i > $o )). + +tff(q_type,type,( + q: ( $i * $i ) > $o )). + +%----Conditional constructs +tff(conditionals,axiom,( + ! [Z: $i] : + $ite_f( + ? [X: $i] : p(X) + , ! [X: $i] : q(X,X) + , q(Z,$ite_t(! [X: $i] : p(X), f(a), f(Z))) ) )). + +%----Let binders +tff(let_binders,axiom,( + ! [X: $i] : + $let_ff( + ! [Y1: $i,Y2: $i] : + ( q(Y1,Y2) + <=> p(Y1) ) + , ( q($let_tt(! [Z1: $i] : f(Z1) = g(Z1,b), f(a)),X) + & p($let_ft(! [Y3: $i] : ! [Y4: $i] : ( q(Y3,Y4) <=> $ite_f(Y3 = Y4, q(a,a), q(Y3,Y4) ) ), $ite_t(q(b,b), f(a), f(X)))) ) ) )). + +%----Rare connectives +tff(never_used_connectives,axiom,( + ! [X: $i] : + ( ( p(X) + ~| ~ q(X,a) ) + ~& p(X) ) )). + +%----Roles +tff(role_definition,definition,( + ! [X: $i] : f(a) = f(X) )). + +tff(role_assumption,assumption,( + p(a) )). + +tff(role_lemma,lemma,( + p(a) )). + +tff(role_theorem,theorem,( + p(a) )). + +tff(role_unknown,unknown,( + p(a) )). + +%----Selective include directive +include('Axioms/SYN000_0.ax',[ia1,ia3]). + +%----Source +tff(source_unknown,axiom,( + ! [X: $i] : p(X) ), + unknown). + +tff(source,axiom,( + ! [X: $i] : p(X) ), + file('SYN000-1.p')). + +tff(source_name,axiom,( + ! [X: $i] : p(X) ), + file('SYN000-1.p',source_unknown)). + +tff(source_copy,axiom,( + ! [X: $i] : p(X) ), + source_unknown). + +tff(source_introduced_assumption,axiom,( + ! [X: $i] : p(X) ), + introduced(assumption,[from,the,world])). + +tff(source_inference,plain,( + p(a) ), + inference(magic,[status(thm),assumptions([source_introduced_assumption])],[theory(equality),source_unknown])). + +tff(source_inference_with_bind,plain,( + p(a) ), + inference(magic,[status(thm)],[theory(equality),source_unknown:[bind(X,$fot(a))]])). + +%----Useful info +tff(useful_info,axiom,( + ! [X: $i] : p(X) ), + unknown, + [simple,prolog(like,Data,[nested,12.2]),AVariable,12.2,"A distinct object",$tff(p(X) | ~ q(X,a)),data(name):[colon,list,2],[simple,prolog(like,Data,[nested,12.2]),AVariable,12.2]]). + +%------------------------------------------------------------------------------ diff --git a/test/regress/regress0/tptp/SYN075+1.p b/test/regress/regress0/tptp/SYN075+1.p new file mode 100644 index 000000000..7ef40217c --- /dev/null +++ b/test/regress/regress0/tptp/SYN075+1.p @@ -0,0 +1,46 @@ +%-------------------------------------------------------------------------- +% File : SYN075+1 : TPTP v5.5.0. Released v2.0.0. +% Domain : Syntactic +% Problem : Pelletier Problem 52 +% Version : Especial. +% English : + +% Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au +% : [Hah94] Haehnle (1994), Email to G. Sutcliffe +% Source : [Hah94] +% Names : Pelletier 52 [Pel86] + +% Status : Theorem +% Rating : 0.22 v5.5.0, 0.15 v5.4.0, 0.18 v5.3.0, 0.26 v5.2.0, 0.05 v5.0.0, 0.21 v4.1.0, 0.17 v4.0.1, 0.22 v4.0.0, 0.21 v3.7.0, 0.00 v3.3.0, 0.11 v3.2.0, 0.33 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 : 2 ( 0 unit) +% Number of atoms : 6 ( 4 equality) +% Maximal formula depth : 7 ( 7 average) +% Number of connectives : 4 ( 0 ~ ; 0 |; 1 &) +% ( 3 <=>; 0 =>; 0 <=) +% ( 0 <~>; 0 ~|; 0 ~&) +% Number of predicates : 2 ( 0 propositional; 2-2 arity) +% Number of functors : 0 ( 0 constant; --- arity) +% Number of variables : 8 ( 0 singleton; 4 !; 4 ?) +% Maximal term depth : 1 ( 1 average) +% SPC : FOF_THM_RFO_SEQ + +% Comments : +%-------------------------------------------------------------------------- +%----Problem axioms +fof(pel52_1,axiom, + ( ? [Z,W] : + ! [X,Y] : + ( big_f(X,Y) + <=> ( X = Z + & Y = W ) ) )). + +fof(pel52,conjecture, + ( ? [W] : + ! [Y] : + ( ? [Z] : + ! [X] : + ( big_f(X,Y) + <=> X = Z ) + <=> Y = W ) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/SYN075-1.p b/test/regress/regress0/tptp/SYN075-1.p new file mode 100644 index 000000000..40b49fa36 --- /dev/null +++ b/test/regress/regress0/tptp/SYN075-1.p @@ -0,0 +1,76 @@ +%-------------------------------------------------------------------------- +% File : SYN075-1 : TPTP v5.5.0. Released v1.0.0. +% Domain : Syntactic +% Problem : Pelletier Problem 52 +% Version : Especial. +% English : + +% Refs : [Pel86] Pelletier (1986), Seventy-five Problems for Testing Au +% Source : [Pel86] +% Names : Pelletier 52 [Pel86] + +% Status : Unsatisfiable +% Rating : 0.00 v5.5.0, 0.20 v5.3.0, 0.22 v5.2.0, 0.12 v5.1.0, 0.06 v5.0.0, 0.07 v4.1.0, 0.08 v4.0.1, 0.18 v4.0.0, 0.09 v3.7.0, 0.00 v3.3.0, 0.14 v3.2.0, 0.08 v3.1.0, 0.09 v2.7.0, 0.08 v2.6.0, 0.00 v2.5.0, 0.08 v2.4.0, 0.11 v2.2.1, 0.11 v2.2.0, 0.22 v2.1.0, 0.33 v2.0.0 +% Syntax : Number of clauses : 10 ( 4 non-Horn; 0 unit; 8 RR) +% Number of atoms : 31 ( 17 equality) +% Maximal clause size : 4 ( 3 average) +% Number of predicates : 2 ( 0 propositional; 2-2 arity) +% Number of functors : 5 ( 2 constant; 0-2 arity) +% Number of variables : 23 ( 2 singleton) +% Maximal term depth : 2 ( 1 average) +% SPC : CNF_UNS_RFO_SEQ_NHN + +% Comments : +%-------------------------------------------------------------------------- +cnf(clause_1,axiom, + ( ~ big_f(X,Y) + | X = a )). + +cnf(clause_2,axiom, + ( ~ big_f(X,Y) + | Y = b )). + +cnf(clause_3,axiom, + ( X != a + | Y != b + | big_f(X,Y) )). + +cnf(clause_4,negated_conjecture, + ( ~ big_f(Y,f(X)) + | Y != g(X) + | f(X) = X )). + +cnf(clause_5,negated_conjecture, + ( ~ big_f(Y,f(X)) + | Y = g(X) + | big_f(h(X,Z),f(X)) + | ~ big_f(h(X,Z),f(X)) )). + +cnf(clause_6,negated_conjecture, + ( Y != g(X) + | big_f(Y,f(X)) + | f(X) = X )). + +cnf(clause_7,negated_conjecture, + ( Y != g(X) + | big_f(Y,f(X)) + | big_f(h(X,Z),f(X)) + | h(X,Z) = Z )). + +cnf(clause_8,negated_conjecture, + ( Y != g(X) + | big_f(Y,f(X)) + | h(X,Z) != Z + | ~ big_f(h(X,Z),f(X)) )). + +cnf(clause_9,negated_conjecture, + ( f(X) != X + | big_f(h(X,Z),f(X)) + | h(X,Z) = Z )). + +cnf(clause_10,negated_conjecture, + ( f(X) != X + | h(X,Z) != Z + | ~ big_f(h(X,Z),f(X)) )). + +%-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp/tff0-arith.p b/test/regress/regress0/tptp/tff0-arith.p new file mode 100644 index 000000000..c0e9af25a --- /dev/null +++ b/test/regress/regress0/tptp/tff0-arith.p @@ -0,0 +1,27 @@ +% example from the TFF0 paper +% see https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa +% +% Status : Theorem +% +tff(list_type,type, ( list: $tType )). +tff(nil_type,type, ( nil: list )). +tff(mycons_type,type,( mycons: ( $int * list ) > list )). +tff(sorted_type,type,( fib_sorted: list > $o )). + +tff(empty_fib_sorted,axiom,( + fib_sorted(nil) )). +tff(single_is_fib_sorted,axiom,( + ! [X: $int] : fib_sorted(mycons(X,nil)) )). +tff(double_is_fib_sorted_if_ordered,axiom,( + ! [X: $int,Y: $int] : + ( $less(X,Y) + => fib_sorted(mycons(X,mycons(Y,nil))) ) )). +tff(recursive_fib_sort,axiom,( + ! [X: $int,Y: $int,Z: $int,R: list] : + ( ( $less(X,Y) + & $greatereq(Z,$sum(X,Y)) + & fib_sorted(mycons(Y,mycons(Z,R))) ) + => fib_sorted(mycons(X,mycons(Y,mycons(Z,R)))) ) )). + +tff(check_list,conjecture,( + fib_sorted(mycons(1,mycons(2,mycons(4,nil)))) )). diff --git a/test/regress/regress0/tptp/tff0.p b/test/regress/regress0/tptp/tff0.p new file mode 100644 index 000000000..0402687bc --- /dev/null +++ b/test/regress/regress0/tptp/tff0.p @@ -0,0 +1,37 @@ +% example from the TFF0 paper +% see https://sites.google.com/site/polymorphictptptff/relevant-links/tff-tfa +% +% Status : Theorem +% +tff(student_type,type, ( student: $tType )). +tff(professor_type,type,( professor: $tType )). +tff(course_type,type, ( course: $tType )). +tff(michael_type,type, ( michael: student )). +tff(victor_type,type, ( victor: professor )). +tff(csc410_type,type, ( csc410: course )). +tff(enrolled_type,type, ( enrolled: ( student * course ) > $o )). +tff(teaches_type,type, ( teaches: ( professor * course ) > $o )). +tff(taught_by_type,type,( taughtby: ( student * professor ) > $o )). +tff(coordinator_of_type,type,( coordinatorof: course > professor )). + +tff(student_enrolled_axiom,axiom,( + ! [X: student] : ? [Y: course] : enrolled(X,Y) )). +tff(professor_teaches,axiom,( + ! [X: professor] : ? [Y: course] : teaches(X,Y) )). +tff(course_enrolled,axiom,( + ! [X: course] : ? [Y: student] : enrolled(Y,X) )). +tff(course_teaches,axiom,( + ! [X: course] : ? [Y: professor] : teaches(Y,X) )). +tff(coordinator_teaches,axiom,( + ! [X: course] : teaches(coordinatorof(X),X) )). +tff(student_enrolled_taught,axiom,( + ! [X: student,Y: course] : + ( enrolled(X,Y) + => ! [Z: professor] : ( teaches(Z,Y) => taughtby(X,Z) ) ) )). +tff(michael_enrolled_csc410_axiom,axiom,( + enrolled(michael,csc410) )). +tff(victor_coordinator_csc410_axiom,axiom,( + coordinatorof(csc410) = victor )). + +tff(teaching_conjecture,conjecture,( + taughtby(michael,victor) )). diff --git a/test/regress/regress0/tptp_parser.p b/test/regress/regress0/tptp/tptp_parser.p index 0be0adbbf..9c10d5bd3 100644 --- a/test/regress/regress0/tptp_parser.p +++ b/test/regress/regress0/tptp/tptp_parser.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Unsatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser10.p b/test/regress/regress0/tptp/tptp_parser10.p index 90db619e7..d6a257121 100644 --- a/test/regress/regress0/tptp_parser10.p +++ b/test/regress/regress0/tptp/tptp_parser10.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Theorem %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser2.p b/test/regress/regress0/tptp/tptp_parser2.p index 83a5f7b83..e165b6b2f 100644 --- a/test/regress/regress0/tptp_parser2.p +++ b/test/regress/regress0/tptp/tptp_parser2.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Unsatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser3.p b/test/regress/regress0/tptp/tptp_parser3.p index 3677e6ffe..2840892bc 100644 --- a/test/regress/regress0/tptp_parser3.p +++ b/test/regress/regress0/tptp/tptp_parser3.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Unsatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser4.p b/test/regress/regress0/tptp/tptp_parser4.p index 6c5bd29da..448db77d2 100644 --- a/test/regress/regress0/tptp_parser4.p +++ b/test/regress/regress0/tptp/tptp_parser4.p @@ -1,5 +1,4 @@ -% EXPECT: unsat -% EXIT: 20 +% Status: Unsatisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser5.p b/test/regress/regress0/tptp/tptp_parser5.p index 23ddf3e60..c90d1cdad 100644 --- a/test/regress/regress0/tptp_parser5.p +++ b/test/regress/regress0/tptp/tptp_parser5.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: Satisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser6.p b/test/regress/regress0/tptp/tptp_parser6.p index 799bc4c6d..6283eb29a 100644 --- a/test/regress/regress0/tptp_parser6.p +++ b/test/regress/regress0/tptp/tptp_parser6.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: Satisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser7.p b/test/regress/regress0/tptp/tptp_parser7.p index f87c3484c..73c2b3834 100644 --- a/test/regress/regress0/tptp_parser7.p +++ b/test/regress/regress0/tptp/tptp_parser7.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: Satisfiable %-------------------------------------------------------------------------- diff --git a/test/regress/regress0/tptp_parser8.p b/test/regress/regress0/tptp/tptp_parser8.p index 4bb2694ea..da281151b 100644 --- a/test/regress/regress0/tptp_parser8.p +++ b/test/regress/regress0/tptp/tptp_parser8.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: Satisfiable %-------------------------------------------------------------------------- include('tptp_parser7.p'). diff --git a/test/regress/regress0/tptp_parser9.p b/test/regress/regress0/tptp/tptp_parser9.p index bcbb88598..9bed19702 100644 --- a/test/regress/regress0/tptp_parser9.p +++ b/test/regress/regress0/tptp/tptp_parser9.p @@ -1,5 +1,4 @@ -% EXPECT: unknown -% EXIT: 0 +% Status: CounterSatisfiable %-------------------------------------------------------------------------- |