
c turning on binary mode checking

c parsing input formula with 959 variables and 19207 clauses

c finished parsing, read 117712 bytes from proof file

c detected empty clause; start verification via backward checking

c 118 of 19207 clauses in core                            

c 71 of 2543 lemmas in core using 430 resolution steps

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

s VERIFIED

c verification time: 0.059 seconds
