Sutcliffe, G.; Benzmueller, C. Automated Reasoning in Higher-Order Logic Using the TPTP THF Infrastructure. JFR 2010, 3, 1-27.