Something probably wrong...

[DennisYurichev]

Downloaded your 'rate' today...

Can't process these two files.
PROOFs are generated by Kissat.

https://yurichev.com/tmp/rate-issues/

drat-trim and ACL2 can process them all.

% ./rate ~/Downloads/SAT_lib.MOLS2_order6.cnf ~/Downloads/SAT_lib.MOLS2_order6.proof
...
c /home/i/Downloads/SAT_lib.MOLS2_order6.proof:62257 redundancy check failed for [56363] 3892 3894 57 117 3896 3897 3898 3899 3900 3901 3902 0
s NOT VERIFIED


% ./rate ~/Downloads/t2.cnf ~/Downloads/t2.proof
...
c /home/i/Downloads/t2.proof:2307388 redundancy check failed for [1203948] -18367 -3206 2026 2858 0
s NOT VERIFIED

[krobelus]

Your proof looks suspicious. How exactly did you generate it?
The reason I'm asking is that rate shows that your proof has "bad" unit deletions¹:

c reason deletions shrinking trail:               242

but if I create a proof myself with kissat version
02cd69626a53e93e09286b1978ccb5d6bec58b8e and check it with rate, I get 0 "reason deletions shrinking trail".
This is more what I expected, because kissat is a reimplementation of CaDiCaL, which always has 0 here.
Repeated invocations of kissat give me exactly the same proof.

It's possible but not very likely that there is a bug in rate. rate's
rejections are actually double checked: after we find a lemma that fails the
redundancy check, we compute an incorrectness certificate that gives hints as
to why the lemma does not have the given redundancy property (usually RAT).
Much like LRAT, this certificate is easy to validate. We validate it by
reading the formula + proof again, applying the proof until the failing step
and then fully checking that it does not have the redundancy property
(without doing any expensive/complex unit progagation).
The incorrectness certificate is checked automatically internally, but it can
be written out with the -S option and checked separately with sick-check
from the rate-sick-check crate.

Footnotes

1. These deletion instructions are ignored by drat-trim but not by rate,
   hence the different results. They normally indicate a bug in the solver
   since there is hardly ever a reason to delete such a unit clause. ↩

[DennisYurichev]

Ah yes. The files I've shared I generated with older Kissat:

c Copyright (c) 2019-2020 Armin Biere JKU Linz
c
c Version sc2020 039805f203ac24f204fd6ae0b3d6bae54332ee1e

With newer Kissat all problems with 'rate' are gone:

c Copyright (c) 2019-2021 Armin Biere JKU Linz
c
c Version 2.0.1 02cd69626a53e93e09286b1978ccb5d6bec58b8e

Thanks for your help!