The TPTP Typed First-order Form with Arithmetic

                        Geoff Sutcliffe
                        Stephan Schulz
                        Koen Claessen
                        Peter Baumgartner

The TPTP World is a well established infrastructure sup- porting
research, development, and deployment of Automated Theorem Proving
systems. Recently, the TPTP World has been extended to in- clude a
typed first-order logic, which in turn has enabled the integration of
arithmetic. This paper describes these developments.