
c turning on binary mode checking

c parsing input formula with 614 variables and 13062 clauses

c finished parsing, read 112675 bytes from proof file

c detected empty clause; start verification via backward checking

c 812 of 13062 clauses in core                            

c 768 of 3395 lemmas in core using 8659 resolution steps

c 352 RAT lemmas in core; 172 redundant literals in core lemmas

s VERIFIED

c verification time: 0.060 seconds
