lambdabot-4.0: scripts/Djinn/tests/ljt/debruijn_p.010.ljt
%------------------------------------------------------------------------------
% File : debruijn_p10 : Dyckhoff's benchmark formulae (1997)
% Domain : Syntactic
% Problem : de Bruijn's example
% Version : Especial.
% Problem formulation : Intuit. Valid Size 10
% English : LHS(2*N+1) => RHS(2*N+1) with
% 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 : Theorem
% Rating : 0.60 v 1.0
% Syntax : Number of formulae : 22 ( 0 unit)
% Number of atoms : 504 ( 0 equality)
% Maximal formula depth : 22 ( 21 average)
% Number of connectives : 482 ( 0 ~ ; 0 |; 440 &)
% ( 21 <=>; 21 =>; 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_p.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 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom2, axiom.
(( ( p2 <-> p3 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom3, axiom.
(( ( p3 <-> p4 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom4, axiom.
(( ( p4 <-> p5 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom5, axiom.
(( ( p5 <-> p6 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom6, axiom.
(( ( p6 <-> p7 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom7, axiom.
(( ( p7 <-> p8 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom8, axiom.
(( ( p8 <-> p9 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom9, axiom.
(( ( p9 <-> p10 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom10, axiom.
(( ( p10 <-> p11 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom11, axiom.
(( ( p11 <-> p12 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom12, axiom.
(( ( p12 <-> p13 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom13, axiom.
(( ( p13 <-> p14 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom14, axiom.
(( ( p14 <-> p15 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom15, axiom.
(( ( p15 <-> p16 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom16, axiom.
(( ( p16 <-> p17 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom17, axiom.
(( ( p17 <-> p18 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom18, axiom.
(( ( p18 <-> p19 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom19, axiom.
(( ( p19 <-> p20 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom20, axiom.
(( ( p20 <-> p21 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
&
% axiom21, axiom.
(( ( p21 <-> p1 ) -> ( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
->
% conjecture_name, conjecture.
(( p1 & ( p2 & ( p3 & ( p4 & ( p5 & ( p6 & ( p7 & ( p8 & ( p9 & ( p10 & ( p11 & ( p12 & ( p13 & ( p14 & ( p15 & ( p16 & ( p17 & ( p18 & ( p19 & ( p20 & p21 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ))
)).
%------------------------------------------------------------------------------