
c turning on binary mode checking

c parsing input formula with 955 variables and 19174 clauses

c finished parsing, read 117578 bytes from proof file

c detected empty clause; start verification via backward checking

c 134 of 19174 clauses in core                            

c 76 of 2552 lemmas in core using 454 resolution steps

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

s VERIFIED

c verification time: 0.066 seconds
