S. J. Lee and D. A. Plaisted, “Controlling the Consumption of Storage with Sliding Priority Search in a Hyper-Linking Based Theorem Prover”, Comput. Inform., vol. 14, no. 6, pp. 563–578, Jan. 2012.