equiv_p.006.ljt

%------------------------------------------------------------------------------
% File     : equiv_p6 : Dyckhoff's benchmark formulae (1997)
% Domain   : Syntactic
% Problem  : Equivalences
% Version  : Especial.
%            Problem formulation : Intuit. Valid  Size 6
% English  : (..(( p(1) <=> p(2)) <=> p(3)) <=> .. <=> p(N))  <=>
%            (p(N) <=> ( p(N-1) <=> (.. (p(2) <=> p(1)) ) ))

% Refs     : [Dyc97] Roy Dyckhoff. Some benchmark formulae for
%                    intuitionistic propositional logic. At
%                    http://www.dcs.st-and.ac.uk/~rd/logic/marks.html
% Source   : [Dyc97]
% Names    : 

% Status   : Theorem
% Rating   : 0.60 v 1.0
% Syntax   : Number of formulae    :    1 (   0 unit)
%            Number of atoms       :   12 (   0 equality)
%            Maximal formula depth :    7 (   7 average)
%            Number of connectives :   11 (   0 ~  ;   0  |;   0  &)
%                                         (  11 <=>;   0 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    6 (   6 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 : this formula is different to the equivalences formulated
%            in Pelletier 71 [Pel86], TPTP SYN007+1
%          : tptp2X -f ljt equiv_p.006.p 
%------------------------------------------------------------------------------

f((

% conjecture_name, conjecture.
(( ( ( ( ( ( a1 <-> a2 ) <-> a3 ) <-> a4 ) <-> a5 ) <-> a6 ) <-> ( a6 <-> ( a5 <-> ( a4 <-> ( a3 <-> ( a2 <-> a1 ) ) ) ) ) ))

)).

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