%------------------------------------------------------------------------------ % File : kk_p6 : Dyckhoff's benchmark formulae (1997) % Domain : Syntactic % Problem : Formulae of Korn & Kreitz % Version : Especial. % Problem formulation : Intuit. Valid Size 6 % English : ((A & B(N) & C1(N)) => f) & ((C2(N) & B(N) & A) => f) with % A = (a(0) => f), B(N) = (b(N) => b(0) => a(N)), % C1(N) = (&&_{i=1..n} ((b(i-1) => a(i)) => a(i-1))), % C2(N) = (&&_{i=n..1} ((b(i-1) => a(i)) => a(i-1))) % Refs : [Dyc97] Roy Dyckhoff. Some benchmark formulae for % intuitionistic propositional logic. At % http://www.dcs.st-and.ac.uk/~rd/logic/marks.html % : [KK97] D. Korn & C. Kreitz, A constructively adequate % refutation system for intuitionistic logic, % position paper at Tableaux'97, available at % http://www.cs.uni-potsdam.de/ti/kreitz/PDF/ % Source : [Dyc97] % Names : % Status : Theorem % Rating : 0.60 v 1.0 % Syntax : Number of formulae : 1 ( 0 unit) % Number of atoms : 48 ( 0 equality) % Maximal formula depth : 12 ( 12 average) % Number of connectives : 47 ( 0 ~ ; 0 |; 15 &) % ( 0 <=>; 32 =>; 0 <=) % ( 0 <~>; 0 ~|; 0 ~&) % Number of predicates : 15 ( 15 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 : % : tptp2X -f ljt kk_p.006.p %------------------------------------------------------------------------------ f(( % conjecture_name, conjecture. (( ( ( ( a0 -> f ) & ( ( ( b6 -> b0 ) -> a6 ) & ( ( ( b0 -> a1 ) -> a0 ) & ( ( ( b1 -> a2 ) -> a1 ) & ( ( ( b2 -> a3 ) -> a2 ) & ( ( ( b3 -> a4 ) -> a3 ) & ( ( ( b4 -> a5 ) -> a4 ) & ( ( b5 -> a6 ) -> a5 ) ) ) ) ) ) ) ) -> f ) & ( ( ( ( b5 -> a6 ) -> a5 ) & ( ( ( b4 -> a5 ) -> a4 ) & ( ( ( b3 -> a4 ) -> a3 ) & ( ( ( b2 -> a3 ) -> a2 ) & ( ( ( b1 -> a2 ) -> a1 ) & ( ( ( b0 -> a1 ) -> a0 ) & ( ( ( b6 -> b0 ) -> a6 ) & ( a0 -> f ) ) ) ) ) ) ) ) -> f ) )) )). %------------------------------------------------------------------------------