Add debug messages in classifyProve
Fix singleTermCondOnEachPath computation