files / problems / ramsey-r55 / compute / q3 / logs / p7_c5_k2_drat.txt

445 B · on GitHub

c turning on binary mode checking

c parsing input formula with 13461 variables and 326264 clauses

c finished parsing, read 110852953 bytes from proof file

c detected empty clause; start verification via backward checking

c 20297 of 326264 clauses in core

c 1894964 of 2189280 lemmas in core using 95008811 resolution steps

c 0 RAT lemmas in core; 691852 redundant literals in core lemmas

s VERIFIED

c verification time: 355.075 seconds