
c turning on binary mode checking

c parsing input formula with 618 variables and 13095 clauses

c finished parsing, read 117514 bytes from proof file

c detected empty clause; start verification via backward checking

c 1020 of 13095 clauses in core                            

c 1084 of 3771 lemmas in core using 15248 resolution steps

c 434 RAT lemmas in core; 209 redundant literals in core lemmas

s VERIFIED

c verification time: 0.059 seconds
