The importance of subsumption as a redundancy elimination method in automated theorem proving is generally acknowledged. For a given Herbrand universe H, it can be further strengthened to the so-called H-subsumption, i.e.: A clause D is H-subsumed by a clause set \({\cal C}\), iff for every H-ground instance Dθ of D there is a clause \(C \in {\cal C}\), s.t. C subsumes Dθ. In recent time, H-subsumption has gained increasing importance especially in the field of automated model building (cf. e.g. [5], [4], [6]). Furthermore, it can be easily shown that H-subsumption may be incorporated as a redundancy deletion rule into many familiar (resolution- and paramodulation-based) inference systems without destroying the refutational completeness.