Superposition is an automated theorem proving method for first-order logic with equality. One approach to handling equality in resolution-based theorem provers is to explicitly add equality axioms (reflexivity, symmetry, transitivity and congruences with respect to all function and variable) as clauses. But that turns out to be quite inefficient, since these axioms can kind of always apply to anything (e.g., one can apply reflexivity on any existing term, then symmetry on the resulting equality, etc). Also, reasoning about deep terms takes a sequence of axiom applications (e.g., after deriving $f(a) = f(b)$, it still takes many inferences using congruence axioms to unpack $f(f(f(a)))$ and $f(f(f(b)))$ derive their equality).
Superposition is an alternative proof system that essentially drops all predicate symbols except for equality, and handles equality specially. To drop a predicate $p$, one can create a new function symbol $f_p$ with the same arity, and then replace $p(x)$ by $f(x) = true$, or $\neg p(x)$ by $f(x) \neq true$, where $true$ is a new constant symbol. The inference rules then allow for substituting equalities into other formulas and dropping contradictions of the form $t \neq t$. This paper has a review and a simple example of a proof by superposition. Superposition is used in a number of state-of-the-art automated theorem provers for first-order logic with equality, like in E.