Avoiding the Dangers

Evaluation

• The TPTP is the facto standard for evaluating 1st order ATP systems
• Risk of TPTP dependency
• Problems getting (relatively) easy
• Release new TPTP versions
  • Problems collected from researchers
  • The more, the better

Machine Generation of New Problems

• Problems with recognizable semantics, e.g., an algebra
• Hard enough for contemporary ATP systems