 Term rewriting, like any other automated deduction method, needs strategies to direct its application. Rippling (Bundy, Stevens &amp; Harmelen 1993, Basin &amp; Walsh 1996) is a heuristic that has its origins in inductive theorem-proving that uses annotations to selectively restrict the rewriting process. The superposition calculus is a calculus of equational first-order logic that combines notions from first-order resolution and Knuth-Bendix ordering equality. Superposition is refutation complete (Bachmair &amp; Ganzinger 1994) and is at the heart of a number of theorem provers, most notably the E equational theorem prover (Schulz 2004) and Vampire (Voronkov 1995).