tptp2X and X2tptp
tptp2X
- Conversion of problems to system specific formulation and format
- Convert between FOF and CNF
- Remove and add equality axioms
- Apply Mark Stickel's magic set transformation
- Rename and reorder
- Conversion of problems to system specific syntax
- Control generic problem generation
- Reads and writes both old and new TPTP syntax
- New TPTP syntax is the default output syntax
X2tptp
- Conversion of derivations from system specific syntax