c cleaning 0 clauses out of 0 for limit 1.7976931348623157E308
c cleaning 0 clauses out of 0 for limit 1.7976931348623157E308
c cleaning 0 clauses out of 0 for limit 1.7976931348623157E308
c cleaning 0 clauses out of 0 for limit 1.7976931348623157E308