diff options
Diffstat (limited to 'test/regress/regress0/tptp/SYN000+2.p')
| -rw-r--r-- | test/regress/regress0/tptp/SYN000+2.p | 127 |
1 files changed, 127 insertions, 0 deletions
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] + ]). + +%------------------------------------------------------------------------------ |