Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation