Given a deductive system $\Lambda$, and some well-formed-formula S, one can ask the question Is there a proof S in $\Lambda$ of length n?  If n is presented in base-1 and if all the axioms of $\Lambda$ are polynomial-time verifiable, and if $\Lambda$ is sufficiently powerful to express the verification for some NP-Complete problem like 3-SAT, this problem is known to be NP-Complete.  It requires super-polynomial time if n is not.I know how to prove this, but I am also sure that somebody else has already proven this.  Can somebody direct me to an existing published reference?
Looking for reference on NP-Completeness of proofs of length n
reference request;np complete;automated theorem proving