proper handling of usable rules (they are only considered inside redPairUrProc)
show proof outline
print proof outline at the end
re-enable semantic labelling