
c turning on binary mode checking

c parsing input formula with 991 variables and 19471 clauses

c finished parsing, read 37826 bytes from proof file

c detected empty clause; start verification via backward checking

c 536 of 19471 clauses in core                            

c 6 of 1191 lemmas in core using 1035 resolution steps

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

s VERIFIED

c verification time: 0.065 seconds
