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