
c turning on binary mode checking

c parsing input formula with 622 variables and 13128 clauses

c finished parsing, read 99348 bytes from proof file

c detected empty clause; start verification via backward checking

c 427 of 13128 clauses in core                            

c 402 of 1602 lemmas in core using 2171 resolution steps

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

s VERIFIED

c verification time: 0.050 seconds
