Analysis Data

Data from the TPTP and TSTP

• From TPTP v6.3.0, released on 28th November 2015
• To TPTP v8.2.0, released on 13th June 2023
• From the ProblemAndSolutionStatistics file

Data Cleaning

• Cleaning for bias - unfair data
• Cleaning for bugfixes - discontinued data
• Cleaning for the past - assuming the past
• Cleaning for change - strange new data

Coherent SPC Sets

• CNF unit equality (UEQ) 1140 problems
• CNF unsatisfiable (CNF UNS) 4441 problems
• CNF satisfiable (CNF SAT) 1042 problems
• Effectively propositional (EPR) 1425 problems
• FOF theorems (FOF THM) 7202 problems
• FOF non-theorems (FOF CSA/SAT) 1028 problems
• TF0 theorems without arithmetic (TF0 NAR) 397 problems
• TF0 theorems with arithmetic (TF0 ARI) 1087 problems
• TH0 theorems (TH0) 3183 problems