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