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

399 B · on GitHub

c parsing input formula with 6321 variables and 1653870 clauses

c finished parsing

c detected empty clause; start verification via backward checking

c 27808 of 1653870 clauses in core                            

c 84529 of 954480 lemmas in core using 21026951 resolution steps

c 916 RAT lemmas in core; 250087 redundant literals in core lemmas

s VERIFIED

c verification time: 68.711 seconds