- provide a method to mark proof attempts as obsolete
  (thus, we can replay a saved tree even if the source
  file hasn't changed)
- cleaning applies to a subtree (like transformations
  and provers), not only at the first level
- obsolete proof attempts do not count as successuful