TPTP 8.0.0 contains 206 condensed detachment problems, all in the LCL domain. Corpus TPTPCD2 is the subset of those 196 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, and problems with multiple goal theorems.
These experiments show the performance of the SGCD prover included in CD Tools on the TPTPCD2 corpus, in various configurations, and in comparison to selected other provers.
The experiments are described in
The work was supported by the North-German Supercomputing Alliance (HLRN).