kk_p.006.ljt

%------------------------------------------------------------------------------
% File     : kk_p6 : Dyckhoff's benchmark formulae (1997)
% Domain   : Syntactic
% Problem  : Formulae of Korn & Kreitz
% Version  : Especial.
%            Problem formulation : Intuit. Valid  Size 6
% English  : ((A & B(N) & C1(N)) => f) & ((C2(N) & B(N) & A) => f) with
%            A = (a(0) => f), B(N) = (b(N) => b(0) => a(N)),
%            C1(N) = (&&_{i=1..n} ((b(i-1) => a(i)) => a(i-1))),
%            C2(N) = (&&_{i=n..1} ((b(i-1) => a(i)) => a(i-1)))

% Refs     : [Dyc97] Roy Dyckhoff. Some benchmark formulae for
%                    intuitionistic propositional logic. At
%                    http://www.dcs.st-and.ac.uk/~rd/logic/marks.html
%          : [KK97]  D. Korn & C. Kreitz, A constructively adequate
%                    refutation system for intuitionistic logic,
%                    position paper at Tableaux'97, available at
%                    http://www.cs.uni-potsdam.de/ti/kreitz/PDF/
% Source   : [Dyc97]
% Names    : 

% Status   : Theorem
% Rating   : 0.60 v 1.0
% Syntax   : Number of formulae    :    1 (   0 unit)
%            Number of atoms       :   48 (   0 equality)
%            Maximal formula depth :   12 (  12 average)
%            Number of connectives :   47 (   0 ~  ;   0  |;  15  &)
%                                         (   0 <=>;  32 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :   15 (  15 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 : 
%          : tptp2X -f ljt kk_p.006.p 
%------------------------------------------------------------------------------

f((

% conjecture_name, conjecture.
(( ( ( ( a0 -> f ) & ( ( ( b6 -> b0 ) -> a6 ) & ( ( ( b0 -> a1 ) -> a0 ) & ( ( ( b1 -> a2 ) -> a1 ) & ( ( ( b2 -> a3 ) -> a2 ) & ( ( ( b3 -> a4 ) -> a3 ) & ( ( ( b4 -> a5 ) -> a4 ) & ( ( b5 -> a6 ) -> a5 ) ) ) ) ) ) ) ) -> f ) & ( ( ( ( b5 -> a6 ) -> a5 ) & ( ( ( b4 -> a5 ) -> a4 ) & ( ( ( b3 -> a4 ) -> a3 ) & ( ( ( b2 -> a3 ) -> a2 ) & ( ( ( b1 -> a2 ) -> a1 ) & ( ( ( b0 -> a1 ) -> a0 ) & ( ( ( b6 -> b0 ) -> a6 ) & ( a0 -> f ) ) ) ) ) ) ) ) -> f ) ))

)).

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