Presentation of Problems

(TPTP) presentation should not affect evaluation

• Predicate and function symbol names are irrelevant

• Formula, clause, literal, and argument ordering is irrelevant

• Redundant built in theories can be removed
• Dependant established theories can be added

• Formula type information can be used

Implement appropriate preprocessing