
c turning on binary mode checking

c parsing input formula with 983 variables and 19405 clauses

c finished parsing, read 123227 bytes from proof file

c detected empty clause; start verification via backward checking

c 555 of 19405 clauses in core                            

c 8 of 1211 lemmas in core using 1007 resolution steps

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

s VERIFIED

c verification time: 0.073 seconds
