Conclusion

• Fulfilled the main aims and motivations
  • Evaluated the relative abilities of cuurrent ATP systems
  • Stimulated development of and interest in ATP systems

• Development efforts have received public recognition
  • Provided exposure for system builders ... both within and beyond the community
  • Provided an overview of the implementation state of running, fully automatic, first order ATP systems

• Next year and Beyond
  • Only TPTP input syntax, with includes
  • New THF (typed higher-order form) division
  • Your Prover (You)