c parsing input formula with 8140 variables and 569020 clauses

c finished parsing

c detected empty clause; start verification via backward checking

c 240951 of 569020 clauses in core

c 1605313 of 3177279 lemmas in core using 87071419 resolution steps

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

s VERIFIED

c verification time: 96.536 seconds