KBlab: an equational theorem prover for the Macintosh