The technique described in this paper can be used in studying various strategies for establishing the correctness of theorem proving techniques. The idea is to well-order the set of all terms (not necessarily grounded) in such a way that simpler terms precede more complex terms, and substitutions preserve the ordering. Such orderings are usually transfinite. This ordering, of course, determines well-orderings of atomic formulas with similar properties.

Such orderings can then be used to find models in completeness proofs in Herbrand interpretations of the language. For general set-theoretical reasons, the partial interpretations of the language that are defined on the initial segment of that well-ordering are endowed with a tree structure. The authors study this tree and show how it reflects theorem proving strategies. Paramodulation is studied in this context, including lifting lemmas for paramodulation. The authors compare various strategies.