debruijn_p.002.ljt

%------------------------------------------------------------------------------
% File     : debruijn_p2 : Dyckhoff's benchmark formulae (1997)
% Domain   : Syntactic
% Problem  : de Bruijn's example
% Version  : Especial.
%            Problem formulation : Intuit. Valid  Size 2
% 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    :    6 (   0 unit)
%            Number of atoms       :   40 (   0 equality)
%            Maximal formula depth :    6 (   5 average)
%            Number of connectives :   34 (   0 ~  ;   0  |;  24  &)
%                                         (   5 <=>;   5 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    5 (   5 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.002.p 
%------------------------------------------------------------------------------

f((

% axiom1, axiom.
(( ( p1 <-> p2 ) -> ( p1 & ( p2 & ( p3 & ( p4 & p5 ) ) ) ) ))

 & 

% axiom2, axiom.
(( ( p2 <-> p3 ) -> ( p1 & ( p2 & ( p3 & ( p4 & p5 ) ) ) ) ))

 & 

% axiom3, axiom.
(( ( p3 <-> p4 ) -> ( p1 & ( p2 & ( p3 & ( p4 & p5 ) ) ) ) ))

 & 

% axiom4, axiom.
(( ( p4 <-> p5 ) -> ( p1 & ( p2 & ( p3 & ( p4 & p5 ) ) ) ) ))

 & 

% axiom5, axiom.
(( ( p5 <-> p1 ) -> ( p1 & ( p2 & ( p3 & ( p4 & p5 ) ) ) ) ))

  ->

% conjecture_name, conjecture.
(( p1 & ( p2 & ( p3 & ( p4 & p5 ) ) ) ))

)).

%------------------------------------------------------------------------------