Harald Ganzinger, Jürgen Stuber. Superposition with Equivalence Reasoning and Delayed Clause Normal Form Transformation.
19th International Conference on Automated Deduction - CADE-19, 2003, Miami Beach, FL, United States. pp.335-349,
⟨10.1007/978-3-540-45085-6_31⟩.
⟨inria-00099710⟩