Dear all, I would like to mention that Rainbow should be able to handle relative termination and termination modulo AC (although I did not test it). Therefore, it would be nice if Aprove, Matchbox or other tools could output Rainbow proofs in these categories too. ;-)