cheq_checker_qube_cert_results.txt
summarizes results on QBFEVAL-10, MAIN/SUBMITTED/*
This is 136 benchmarks, 88 solved by qube-cert.
All of the "SAT" certificates produced by CHEQ/qube-cert_0.1
were rejected by CHEQ/checker_0.1.

Other disagreements, on small files, are also given here.

% CHEQ/qube-cert_0.1 qdpllexp_1.qdimacs > qdpllexp_1.proof
% CHEQ/checker_0.1 qdpllexp_1.proof
Resolving 0
Segmentation fault

% CHEQ/qube-cert_0.1 qdpllexp_2.qdimacs > qdpllexp_2.proof
% CHEQ/checker_0.1 qdpllexp_2.proof
Resolving 0
Segmentation fault

Another disagreement, on a slightly larger file, is given below.

% CHEQ/qube-cert_0.1 qdpllexp_20.qdimacs > qdpllexp_20.proof
% CHEQ/checker_0.1 qdpllexp_20.proof
Resolving 0
Segmentation fault

In all cases where the qdimacs and certificates are included
in this directory, qube-cert_0.1 produced NOGOODs that
contained tautologous resolvents.
This is in the style of "long-distance resolution", due to
Zhang and Malik, but it is inconsistent with Q-resolution,
introduced by Kleine Buning et al., 1995.

The only public documentation on qube-cert_0.1 indicates that
it uses Q-resolution and does not admit tautologous resolvents.
Therefore these proof files appear to be counter-examples
to the published information for qube-cert_0.1.
Source codes are not offered, for the CHEQ package, so further
investigation is not possible.