tptp2X

• Converts TPTP problems to formats used by existing ATP systems

  Bliksem	CoDe	CLIN-S	Dedam
  DFG	DIMACS	FINDER	ILF
  KIF	leanTAP	3TAP	METEOR
  MGTP	OSCAR	OTTER	PROTEIN
  PTTP	Satchmo	SCOTT	SEM
  SETHEO	SPRFN	THINKER	Waldmeister

• Applies transformations
  • Simplify and transform FOF problems to CNF problems
  • Formula, literal, and argument reordering
  • Remove and add equality axioms
  • Apply Mark Stickel's magic set transformation
  • Replace all the symbols by short, meaningless symbols

• Controls generation