The TPTP2T Problem and Solution Selector

Problem Characteristics

• Logical, e.g., THF vs. FOF vs. CNF, SZS status
• Language, e.g., effective order, use of equality
• Syntax, e.g., Horness, size
• TPTP, e.g., rating, domains

Solution Characteristics

• System name and version
• Result and output from SZS ontology
• Derivation shape, e.g., selectivity, girth

Available online at tptp.org/cgi-bin/TPTP2T