Schlichtkrull, A., Blanchette, J., Traytel, D., & Waldmann, U. (2020). Formalizing Bachmair and Ganzinger's Ordered Resolution Prover. Journal of Automated Reasoning, 64, 1169-1195. doi:10.1007/s10817-020-09561-0.