This page contains supplementary material for the article “A Curiously Effective Backtracking Strategy for Connection Tableaux” submitted to CADE-28.

The current version of the paper is here.

Implementation

The source code for the meanCoP prover is available at https://github.com/01mf02/cop-rs.

Evaluation

Instructions to run the evaluation of meanCoP can be found in the eval directory of cop-rs.

The raw output of the evaluation is here. (Note that inference statistics over 1kB and proofs were omitted due to their large size.) The sets of problems solved by the various meanCoP variants are here.

Note the following naming conventions that were used to generate the files: the R cut is noted as cutred, the EI cut as cutextdeep, and the EX cut as cutextshallow.