%------------------------------------------------------------------------------
% File     : schwicht_p10 : Dyckhoff's benchmark formulae (1997)
% Domain   : Syntactic
% Problem  : Formulae with normal natural deduction proofs only of exponential size
% Version  : Especial.
%            Problem formulation : Intuit. Valid  Size 10
% English  : (p(N) & &&_{i=1..N} (p(i) => p(i) => p(i-1))) => p(0)

% Refs     : [Dyc97] Roy Dyckhoff. Some benchmark formulae for
%                    intuitionistic propositional logic. At
%                    http://www.dcs.st-and.ac.uk/~rd/logic/marks.html
%          : [Sch97] H. Schwichtenberg, Termination of permutative
%                    conversions in Gentzen's sequent calculus,
%                    unpublished (1997). 
% Source   : [Dyc97]
% Names    : 

% Status   : Theorem
% Rating   : 0.40 v 1.0
% Syntax   : Number of formulae    :   12 (   2 unit)
%            Number of atoms       :   32 (   0 equality)
%            Maximal formula depth :    3 (   2 average)
%            Number of connectives :   20 (   0 ~  ;   0  |;   0  &)
%                                         (   0 <=>;  20 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :   11 (  11 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 : "...no normal natural deduction proof of size less than an
%             expontial function of N.
%            ..Our experience of these problems is that they can be decided
%            very fast but can generate space problems, e.g. for some
%            implementations of Prolog." [Dyc97]
%          : tptp2X -f ljt schwicht_p.010.p 
%------------------------------------------------------------------------------

f((

% axiom1, axiom.
(p10)

 & 

% axiom2, axiom.
(( p1 -> ( p1 -> p0 ) ))

 & 

% axiom3, axiom.
(( p2 -> ( p2 -> p1 ) ))

 & 

% axiom4, axiom.
(( p3 -> ( p3 -> p2 ) ))

 & 

% axiom5, axiom.
(( p4 -> ( p4 -> p3 ) ))

 & 

% axiom6, axiom.
(( p5 -> ( p5 -> p4 ) ))

 & 

% axiom7, axiom.
(( p6 -> ( p6 -> p5 ) ))

 & 

% axiom8, axiom.
(( p7 -> ( p7 -> p6 ) ))

 & 

% axiom9, axiom.
(( p8 -> ( p8 -> p7 ) ))

 & 

% axiom10, axiom.
(( p9 -> ( p9 -> p8 ) ))

 & 

% axiom11, axiom.
(( p10 -> ( p10 -> p9 ) ))

  ->

% conjecture_name, conjecture.
(p0)

)).

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