A Herbrand strategy T is that algorithm which for an arbitrary prenex formula F gives a sequence of its Herbrand disjunctions. Let FT be the first tautology in this sequence. T is complete if for every deducible F, FT exists. The strategy T gives k superfluous terms for F if k disjuncts can be removed from FT while preserving its tautological character; T is optimal for F if there exists no Herbrand disjunction for F shorter than FT. There are complete strategies that give arbitrarily small proportion of terms for all F. There are also strategies that work with incomplete information about F (e.g., with the signature of F or a list of its elementary subformulas). For any such complete strategy we can construct a class of formulas for which the proportion of superfluous terms tends to 1 as the length of the formula tends to ∞. However, there is no possible algorithm for finding the superfluous terms which may be dropped. Even for strategies that require complete and uniform review of all possible permutations of terms (for a given signature), the class of formulas for which T is optimal is undecidable. The proof uses properties of the relation “F is more deducible than G,” studied in terms of the general theory of calculi.