files / problems / kissing-5d / compute / q5 / t5_36_drat_trim.txt
c turning on binary mode checking c parsing input formula with 23323 variables and 56352 clauses c finished parsing, read 671198215 bytes from proof file c detected empty clause; start verification via backward checking c 18420 of 56352 clauses in core c 4787602 of 10804713 lemmas in core using 303220601 resolution steps c 0 RAT lemmas in core; 2457201 redundant literals in core lemmas s VERIFIED c verification time: 756.366 seconds