Demodulation is an important simplification rule in saturation-based theorem proving that performs rewriting using unit equalities.
However, in certain problem encodings, particularly ones coming from software verification, many useful equalities appear with side conditions.
We present (forward) subsumption demodulation, a generalization of demodulation to non-unit clauses,
and discuss its implementation in the theorem prover Vampire along with experimental results.