Will the Results be Useful?

In the Biggest Sense

• Bob Kelley told me ...
     You only have to discover one good theorem to get a PhD in math
• Can we find one? I hope so!

In a Big Sense

• In the "Y-front" projects

In the TPTP

• The TPTP is a de facto test standard
• Growth required to combat tuning
• Discovered theorems in the TPTP
  • Even if they're not incredibly interesting