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