THF Solutions

The TSTP

• The TSTP is the "flip side" of the TPTP
• Four higher-orer ATP systems tested
  • LEO II - Chris Benzmüller's magic
  • TPS-GOOD1 - Chad Brown's sorcery
  • IsabelleP - wizardry by Makarius Wenzel and Stefan Berghofer
  • IsabelleM - added mojo by Jasmin Blanchette
  • IsabelleM - new trickery by Jasmin Blanchette

The Results

• This table shows ...
• GRA problems are hard
• Problems pose interesting challenges
• There are differences between the systems
• Each system contributes to the state of the art