
c turning on binary mode checking

c parsing input formula with 967 variables and 19273 clauses

c finished parsing, read 240982 bytes from proof file

c detected empty clause; start verification via backward checking

c 3505 of 19273 clauses in core                            

c 3846 of 8880 lemmas in core using 102260 resolution steps

c 2017 RAT lemmas in core; 1187 redundant literals in core lemmas

s VERIFIED

c verification time: 0.198 seconds
