²The paramodulation inference rule used in paramodulation-based theorem proving [87] is similar to narrowing and does not require non-variable positions.