  Rewriting techniques based on reduction orderings generate "just enough"
consequences to retain first-order completeness. This is ideal for
superposition-based first-order theorem proving, but for at least one approach
to inductive reasoning we show that we are missing crucial consequences. We
therefore extend the superposition calculus with rewriting-based techniques to
generate sufficient consequences for automating induction in saturation. When
applying our work within the unit-equational fragment, our experiments with the
theorem prover Vampire show significant improvements for inductive reasoning.
