We propose several methods for writing efficient subsumption procedures for non-unit clauses, tested in practice as parts incorporated into the Gandalf family of theorem provers. Versions of Gandalf exist for classical logic, first order intuitionistic logic and type theory.