  In this article we present a class of formulas Fn, n in Nat, that need at
least 2^n assumptions to be proved in a normal proof in Natural Deduction for
purely implicational minimal propositional logic. In purely implicational
classical propositional logic, with Peirce's rule, each Fn is proved with only
one assumption in Natural Deduction in a normal proof. Hence, the formulas Fn
have exponentially sized proofs in cut-free Sequent Calculus and Tableaux. In
fact 2^n is the lower-bound for normal proofs in ND, cut-free Sequent proofs
and Tableaux. We discuss the consequences of the existence of this class of
formulas for designing automatic proof-procedures based on these deductive
systems.
