%------------------------------------------------------------------------------ % File : debruijn_p6 : Dyckhoff's benchmark formulae (1997) % Domain : Syntactic % Problem : de Bruijn's example % Version : Especial. % Problem formulation : Intuit. Valid Size 6 % English : LHS(2*N+1) => RHS(2*N+1) with % Refs : [Dyc97] Roy Dyckhoff. Some benchmark formulae for % intuitionistic propositional logic. At % http://www.dcs.st-and.ac.uk/~rd/logic/marks.html % : "de Bruijn, N.: personal communication in about 1990." % Source : [Dyc97] % Names : % Status : Theorem % Rating : 0.60 v 1.0 % Syntax : Number of formulae : 14 ( 0 unit) % Number of atoms : 208 ( 0 equality) % Maximal formula depth : 14 ( 13 average) % Number of connectives : 194 ( 0 ~ ; 0 |; 168 &) % ( 13 <=>; 13 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 13 ( 13 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) % Comments : "quite a tough exercise for students to prove by natural % deduction" [Dyc97] % : tptp2X -f ljt debruijn_p.006.p %------------------------------------------------------------------------------ f(( % axiom1, axiom. (( ( p1 <-> p2 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom2, axiom. (( ( p2 <-> p3 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom3, axiom. (( ( p3 <-> p4 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom4, axiom. (( ( p4 <-> p5 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom5, axiom. (( ( p5 <-> p6 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom6, axiom. (( ( p6 <-> p7 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom7, axiom. (( ( p7 <-> p8 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom8, axiom. (( ( p8 <-> p9 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom9, axiom. (( ( p9 <-> p10 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom10, axiom. (( ( p10 <-> p11 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom11, axiom. (( ( p11 <-> p12 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom12, axiom. (( ( p12 <-> p13 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) & % axiom13, axiom. (( ( p13 <-> p1 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) ) )) -> % conjecture_name, conjecture. (( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & p13 ) ) ) ) ) ) ) ) ) ) ) )) )). %------------------------------------------------------------------------------