
c turning on binary mode checking

c parsing input formula with 951 variables and 19141 clauses

c finished parsing, read 120012 bytes from proof file

c detected empty clause; start verification via backward checking

c 132 of 19141 clauses in core                            

c 80 of 2650 lemmas in core using 423 resolution steps

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

s VERIFIED

c verification time: 0.078 seconds
