c parsing input formula with 111770 variables and 319778 clauses

c finished parsing

c detected empty clause; start verification via backward checking

c 147038 of 319778 clauses in core                            

c 26593 of 60302 lemmas in core using 24548532 resolution steps

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

s VERIFIED

c verification time: 5.092 seconds