TPTP 7.5.0 contains 206 condensed detachment problems, all in the LCL domain. Corpus TPTPCD is the subset of those 195 problems that remain after excluding problems of the following types: Problems with a form of detachment for disjunction and negation instead of implication, problems known as satisfiable, problems with multiple goal theorems and one problem for which TPTP 7.5.0 contains no historic prover statistics in file ProblemAndSolutionStatistics.
These experiments show the performance of the SGCD prover included in CD Tools on the TPTPCD corpus, in various configurations, and in comparison to selected other provers.
The work was supported by the North-German Supercomputing Alliance (HLRN).