TPTP2X and TPTP4X

• Transform problems and solutions
  • Translate between TFF and FOF and CNF
  • Reorder formulae, literals, and arguments
  • Remove and add equality axioms
  • Convert to pure equality representation
  • Standardize predicates and functions apart
  • Replace all the symbols by short, meaningless symbols
  • Expand include directives and remove comments
  • Compute statistics
  • Pretty print
  (TPTP2X and TPTP4X support some each.)

• Convert TPTP problems to formats used by existing ATP systems
  Bliksem CARINE CLIF Dedam DFG DIMACS EQP FINDER Geo Isabelle/HOL KIF leanCoP OSCAR Otter PROTEIN Prover9 SEM SETHEO SMT THINKER TPS Twelf Waldmeister
  (TPTP4X supports only a few.)

• Generate parameterized problems (TPTP2X only)