Lee, S. J.; Plaisted, D. A. Controlling the Consumption of Storage With Sliding Priority Search in a Hyper-Linking Based Theorem Prover. Comput. Inform. 2012, 14, 563-578.