G. Sutcliffe and C. Benzmueller, “Automated Reasoning in Higher-Order Logic using the TPTP THF Infrastructure”, JFR, vol. 3, no. 1, pp. 1–27, Jan. 2010.