Sutcliffe, G., and C. Benzmueller. “Automated Reasoning in Higher-Order Logic Using the TPTP THF Infrastructure”. Journal of Formalized Reasoning, vol. 3, no. 1, Jan. 2010, pp. 1-27, doi:10.6092/issn.1972-5787/1710.