Ganzinger, H., & Stuber, J. (2005). Superposition with equivalence reasoning and delayed clause normal form transformation. Information and Computation, 199, 3-23.