%------------------------------------------------------------------------------
% File     : debruijn_n10 : Dyckhoff's benchmark formulae (1997)
% Domain   : Syntactic
% Problem  : de Bruijn's example
% Version  : Especial.
%            Problem formulation : Inuit. Invalid.   Size 10
% English  : LHS(2*N) -> (p0 | RHS(2*N) | ~p0)
%            RHS(m) = &&_{i=1..m} p(i),
%            LHS(m) = &&_{i=1..m} ((p(i)<=>p(i+1)) => c(N))
%            where addition is computed modulo m, and with
%            c(N) = &&_{i=1..N} p(i)

% 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   : Non-Theorem
% Rating   : 1.00 v 1.0
% Syntax   : Number of formulae    :   21 (   0 unit)
%            Number of atoms       :  462 (   0 equality)
%            Maximal formula depth :   22 (  21 average)
%            Number of connectives :  442 (   1 ~  ;   2  |; 399  &)
%                                         (  20 <=>;  20 =>;   0 <=)
%                                         (   0 <~>;   0 ~|;   0 ~&)
%            Number of predicates  :   21 (  21 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_n.010.p 
%------------------------------------------------------------------------------

f((

% axiom1, axiom.
(( ( p1 <-> p2 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom2, axiom.
(( ( p2 <-> p3 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom3, axiom.
(( ( p3 <-> p4 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom4, axiom.
(( ( p4 <-> p5 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom5, axiom.
(( ( p5 <-> p6 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom6, axiom.
(( ( p6 <-> p7 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom7, axiom.
(( ( p7 <-> p8 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom8, axiom.
(( ( p8 <-> p9 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom9, axiom.
(( ( p9 <-> p10 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom10, axiom.
(( ( p10 <-> p11 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom11, axiom.
(( ( p11 <-> p12 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom12, axiom.
(( ( p12 <-> p13 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom13, axiom.
(( ( p13 <-> p14 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom14, axiom.
(( ( p14 <-> p15 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom15, axiom.
(( ( p15 <-> p16 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom16, axiom.
(( ( p16 <-> p17 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom17, axiom.
(( ( p17 <-> p18 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom18, axiom.
(( ( p18 <-> p19 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom19, axiom.
(( ( p19 <-> p20 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

 & 

% axiom20, axiom.
(( ( p20 <-> p1 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))

  ->

% conjecture_name, conjecture.
(( p0 v ( ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & p20 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) v ( ~ p0 ) ) ))

)).

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