System Design & Delivery

  • Systems must be fully automatic; i.e., all command lines must be the same for all problems.
  • System results must be reproducible by running the system again.
  • Entrants must deliver a package containing everything required, including any external tools.

Output

  • Proof: %SZS Proof Checked
  • No proof: %SZS Proof Error at step X
  • Gave up: %SZS Gave up

System Evaluation

  • 100 proofs (50 good / 50 bad proof)
  • Timeout: 30 seconds

Grading Scheme

  • Identifying a Bad proof as Bad = +2
  • Identifying a Good proof as Good = +1
  • Giving up = 0
  • Identifying a Good proof as Bad = -1
  • Identifying a Bad proof as Good = -10

Organization

For questions, please contact Julie Cailler or Simon Guilloud.