%------------------------------------------------------------------------------ % File : schwicht_n6 : Dyckhoff's benchmark formulae (1997) % Domain : Syntactic % Problem : Formulae with normal natural deduction proofs only of exponential size % Version : Especial. % Problem formulation : Inuit. Invalid. Size 6 % English : (~~p(N) & &&_{i=1..N} (p(i) => p(i) => p(i-1))) => p(0) % Refs : [Dyc97] Roy Dyckhoff. Some benchmark formulae for % intuitionistic propositional logic. At % http://www.dcs.st-and.ac.uk/~rd/logic/marks.html % : [Sch97] H. Schwichtenberg, Termination of permutative % conversions in Gentzen's sequent calculus, % unpublished (1997). % Source : [Dyc97] % Names : % Status : Non-Theorem % Rating : 0.40 v 1.0 % Syntax : Number of formulae : 8 ( 2 unit) % Number of atoms : 20 ( 0 equality) % Maximal formula depth : 3 ( 2 average) % Number of connectives : 14 ( 2 ~ ; 0 |; 0 &) % ( 0 <=>; 12 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 7 ( 7 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 : "...no normal natural deduction proof of size less than an % expontial function of N. % ..Our experience of these problems is that they can be decided % very fast but can generate space problems, e.g. for some % implementations of Prolog." [Dyc97] % : tptp2X -f ljt schwicht_n.006.p %------------------------------------------------------------------------------ f(( % axiom1, axiom. (( ~ ( ~ p6 ) )) & % axiom2, axiom. (( p1 -> ( p1 -> p0 ) )) & % axiom3, axiom. (( p2 -> ( p2 -> p1 ) )) & % axiom4, axiom. (( p3 -> ( p3 -> p2 ) )) & % axiom5, axiom. (( p4 -> ( p4 -> p3 ) )) & % axiom6, axiom. (( p5 -> ( p5 -> p4 ) )) & % axiom7, axiom. (( p6 -> ( p6 -> p5 ) )) -> % conjecture_name, conjecture. (p0) )). %------------------------------------------------------------------------------