
c turning on binary mode checking

c parsing input formula with 610 variables and 13029 clauses

c finished parsing, read 112914 bytes from proof file

c detected empty clause; start verification via backward checking

c 792 of 13029 clauses in core                            

c 702 of 3552 lemmas in core using 7010 resolution steps

c 356 RAT lemmas in core; 150 redundant literals in core lemmas

s VERIFIED

c verification time: 0.070 seconds
