Ganzinger, Harald Programming Logics, MPI for Informatics, Max Planck Society;
https://rdcu.be/dv6ML (Publisher version)
Bachmair, L., & Ganzinger, H. (1990). On Restrictions of Ordered Paramodulation with Simplification. In M. E. Stickel (Ed.), 10th International Conference on Automated Deduction (pp. 427-441). Berlin: Springer.