c formula: header 2545 vars 97524 clauses; read 97524 clauses
c lemmas verified: 1609977; deletion lines ignored: 1515680; clauses skipped as satisfied at top level: 11521
s VERIFIED
real 935.57
user 928.58
sys 2.47
