
c turning on binary mode checking

c parsing input formula with 975 variables and 19339 clauses

c finished parsing, read 237208 bytes from proof file

c detected empty clause; start verification via backward checking

c 2139 of 19339 clauses in core                            

c 3119 of 7672 lemmas in core using 48324 resolution steps

c 783 RAT lemmas in core; 967 redundant literals in core lemmas

s VERIFIED

c verification time: 0.119 seconds
