CM Prover – Evaluation on the TPTP

The CM Prover, embedded in the PIE system for preprocessing, has been tested on all suitable TPTP problems. In different tested configurations it could, on current hardware with a timeout of 600s, solve 1627 problems of the 2143 problems without equality and 2955 of the 11321 problems with equality.

Table Explanation

Problem Selection

Prover Configurations

Measured Time


Resource Limitations

Software Versions

Log Files