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