c formula: header 2665 vars 99960 clauses; read 99960 clauses
c lemmas verified: 1448064; deletion lines ignored: 1415422; clauses skipped as satisfied at top level: 11743
s VERIFIED
real 805.66
user 799.35
sys 2.06
