Cutting down the TPTP language (and others) Nahku Saidy, Hanna Siegfried, Stephan Schulz, Geoff Sutcliffe Computer languages are likely to grow over time as they get more complex when their functionality is extended. An example of that is the TPT P language for automated theorem proving. Over time various forms of classical logics ranging from Clause Normal Form (CNF) to Typed Higher-order Form (THF) have been added, and that extended the TPTP language. This paper describes \emph{Synplifier}, a tool that automatically extracts sub-languages from the TPTP language. Automatic extraction instead of manually maintaining sub-languages has the advantage of avoiding maintenance overhead as well as unnoticed divergences from the full language. Sub-languages of interest are for example CNF and First-order Form (FOF), and are extracted based on the user's selection. Synplifier has been successfully tested by extracting CNF from the TPTP language.