Testing

(Conservative) System Configuration

• No Initial Proof Attempts
• Greedy Termination and Aggressive Selection disabled
• No Batch Selection or Limited Selection
• Automated reasoning components
  • E 0.99 to test for (counter)theoremhood and unsatisfiability
  • EP 0.99 to find proofs
  • FMDarwin 1.3g to build models
  • Paradox 2.0b to test for (counter)satisfiability
  • SPASS 2.2 to further test for (counter)satisfiability.
• 2.8GHz Intel Xeon CPU, 1GB memory, Linux 2.6.
• Overall CPU limit 600s
• Component CPU limits: 10s (counter)theoremhood, 120s unsatisfiability, 600s proofs, 10s models, 2s (counter)satifiability

Test Problems

• Problems not solved by E 0.99 in 20s
• 75 modal logic problems (from 132 problems LCL448+1 to LCL578+1)
• 103 Mizar set theory problems (from 253 problems SET866+1 to SEU118+1)
• 61 NASA software verification problems (from 109 problems SWV022+1 to SWV130+1)

• Superfluous axioms in principle and due to encodings