files / problems / ramsey-r55 / compute / q2 / logs / drat_trim_repair_r3.txt

390 B · on GitHub

c parsing input formula with 4515 variables and 307418 clauses

c finished parsing

c detected empty clause; start verification via backward checking

c 14691 of 307418 clauses in core                            

c 6940 of 18219 lemmas in core using 5008053 resolution steps

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

s VERIFIED

c verification time: 1.449 seconds