 A closely related and further simplified principle has also been presented and studied in Steen 2018, where it was applied for showing completeness of the paramodulation calculus (Steen 2018) that is underlying the theorem prover Leo-III (Steen &amp; Benzmüller 2018).