diff options
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 %-------------------------------------------------------------------------- |