equiv_n.002.ljt

%------------------------------------------------------------------------------
% File     : equiv_n2 : Dyckhoff's benchmark formulae (1997)
% Domain   : Syntactic
% Problem  : Equivalences
% Version  : Especial.
%            Problem formulation : Inuit. Invalid.   Size 2
% 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   : Non-Theorem
% Rating   : 0.60 v 1.0
% Syntax   : Number of formulae    :    1 (   0 unit)
%            Number of atoms       :    4 (   0 equality)
%            Maximal formula depth :    5 (   5 average)
%            Number of connectives :    5 (   2 ~  ;   0  |;   0  &)
%                                         (   3 <=>;   0 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :    2 (   2 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_n.002.p 
%------------------------------------------------------------------------------

f((

% conjecture_name, conjecture.
(( ( ( ~ ( ~ a1 ) ) <-> a2 ) <-> ( a2 <-> a1 ) ))

)).

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