Fixes to the term abduction optimization aka. "step 6" from last commit. Should work after quantifier handling overhaul that will come next.