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

439 B · on GitHub

c turning on binary mode checking

c parsing input formula with 25627 variables and 417582 clauses

c finished parsing, read 27067458 bytes from proof file

c detected empty clause; start verification via backward checking

c 11337 of 417582 clauses in core

c 388840 of 462779 lemmas in core using 6788296 resolution steps

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

s VERIFIED

c verification time: 35.562 seconds