Experimental Setup

QMLTP Library

• Used QMLTP library v1.1
• Fixed (what we saw as) syntax and semantic errors
• 600 problems; domains in 5 groups
  • APM - Mixed applications. 10 problems.
  • G?? - Gödel encodings of TPTP problems. 245 problems.
  • MML - Multi-modal problems. 20 problems. One specified logic.
  • NLP and SET - Classical logic problems. 80 problems.
  • SYM - Syntactic problems. 245 problems.
• Results for some semantic variations provided

Process

• Convert from QMLTP syntax to NX0.
• Add 20 logic specifications (5 modal systems, 4 domain types) to non-MML
  Add 1 specified logic to MML problems
• Translate the 11620 NX0 problems to THF
• Run THF ATP systems on all problems
  • agsyHOL 1.0, cvc5 1.0, E 2.6, HOLyHammer 0.21, lambdaE 22.03.23,
    Leo-III 1.6.6, Satallax 3.5, Vampire 4.6.1, Zipperposition 2.1
  • StarExec Miami - Octa-core Intel Xeon @ 2.10GHz, 128GB memory
  • 180s CPU limit
• Not all the 11620 THF problems are theorems