
c turning on binary mode checking

c parsing input formula with 971 variables and 19306 clauses

c finished parsing, read 260611 bytes from proof file

c detected empty clause; start verification via backward checking

c 3261 of 19306 clauses in core                            

c 4258 of 9552 lemmas in core using 86925 resolution steps

c 1652 RAT lemmas in core; 1527 redundant literals in core lemmas

s VERIFIED

c verification time: 0.202 seconds
