For every condensed detachment proof, there exists a substitution and detachment proof.

If both the antecedent of the major premise, e. g. one having form Cα
β or (p → q) or (p) → (q) or pqC or C(p, q), or (p, q)i, etc., and the minor premise γ qualify as equiform, then a condensed detachment proof corresponds to a single step substitution and detachment proof. We just make a detachment.

If the antecedent of the major premise α
and the minor premise γ both require substitutions to transform them into equiform forms, then we need to make two substitutions, and one detachment to expand the condensed detachment proof into a substitution and detachment proof. Examples of such a case would consist of taking CCzCNxNyCzCyx as the major premise and CCNyyCNyx as the minor, which after condensed detachment yields CCNyyCxy or any formula having the same relative positions of the variables in the formula after condensed detachment, such as CCNxxCyx or CCNaaCba, or if the major and minor premise looked differently and appropriately so ((¬f→ f) → (u →f)) etc. Or taking two copies of CCCCqrCprsCCpqs and then reproducing the condensed detachment of those two copies.
Often enough though, we only need to make one substitution in exclusively the major or the minor premise to expand the condensed detachment proof into a substitution and detachment proof. Thus, we require only two steps for an expansion of the condensed detachment proof into the corresponding substitution and detachment proof; a simultaneous substitution and a detachment.

Meta-Theorem 1: If exclusively the antecedent of the major premise or the minor premise have exactly one instance of any propositional variable throughout the antecedent or the major premise respectively, then for any condensed detachment proof, there exists a two line substitution and detachment proof.
Meta-Proof: A most general unifier can get found simply by substituting each variable in the antecedent of the major premise or in the minor premise whichever satisfies the hypothesis. Consequently, the substitution and detachment proof will only need one simultaneous substitution to make a detachment. Since the detachment qualifies as a step also, that makes for a two line proof as was to get metalogically demonstrated.

Meta-Corollary 1: Systems with formulas of any of the following: CpCqp, CCCpqrCqr, CCCpqqCCqpp, CCCpqrCCprr, CCCpqrCCrpp, CCpqCCqrCpr, CCpqCCrpCrq, CCpCqrCqCpr, CpCCpqq, CCpqCCCprqq, CpCCNqNpq and possibly many more do not have a last theorem under condensed detachment.
Discussion: This size of the question space is a bit small to contain much of a meta-proof. But, to see how this works fix the formula selected under condensed detachment and call it a. For formulas which have a in the antecedent, the meta-corollary follows directly from Meta-Theorem 1. For some others, the antecedent of a has bracket type Cαβ, while any detached formula from a also has bracket type Cαβ. For another set, the bracket type of the formula gets preserved under condensed detachment.

Given a condensed detachment proof, let us call the number of steps (lines in a proof) in any of the shortest corresponding substitution and detachment proofs, the condensed detachment expansion number, CoDEN, of a condensed detachment proof of a formula P, CoDEN(⊢P), or just CoDEN for short.

Now, suppose we had a large number of condensed detachment proofs in classical propositional calculi... I don't know maybe a million or a billion or maybe just a hundred, or even just a few proof. What is the value of CoDEN over all of those proofs? If we took the limit of all formal proofs as n gets larger and larger, would CoDEN converge to a rational number or transcendental number? What would make for a suitable upper estimate and a lower estimate for CoDEN if using it to predicate the length of a minimal substitution and detachment proof from a condensed detachment proof? I'll guess between 2.0 and 2.5. Does it matter which set of formal proofs we select? Does selecting theories which have their formal theorems contained in classical propositional logic substantially alter the value of CoDEN? Using a program that I wrote, and perhaps I'll analyze some other proofs, the value of CoDEN for the proof here is 2.25.

Related paper