Rework RecycleUnits and implement a different replace traversal

New replace traversal checks if current node has unit clause as subclause instead of comparing to pivot elements. Also dagifies the proof on the way.