Testing Environment

Problems

• Three test problems, lemmas extracted from human proofs
  • Graph triangles (GT) - 11 lemmas
  • Short 5 lemma part 2 (S5L) - 15 lemmas
  • Kitchen sink (KS) - 12 lemmas
• Lemmas supplied in order, and randomized and reversed for KS
• GT has a linear proof structure, S5L and KS are branching

Testing Tools

• SPASS 2.1
  • Cannot solve GT or S5L in 6200s
  • Solves KS in 400s, but results are illustrative
• Dell P3, 930Mhz, 512MB, Linux 2.4
• 20s CPU limit on each SPASS proof