Suppose we are given a variety in the universal algebra sense.


For concreteness, suppose that we have two binary operations $+,\cdot$, three unary operations $-,\ast,'$, and two zeroary operations $0,1$. Also, we have the (unital, associative, noncommutative) [ring identities](https://en.wikipedia.org/wiki/Ring_(mathematics)), as well as the identities of a [$\ast$-ring](https://en.wikipedia.org/wiki/*-algebra), together with the four identities
$$
xx'x=x,\ x'xx'=x',\ (xx')^{\ast}=xx',\ (x'x)^{\ast}=x'x.
$$


There is another, specific identity that I wonder if it is a consequence of the given identities, namely setting $x:=a' + (1 - a'a)(1 + a)'(1 - aa')$, then I wonder if
$$
xx'=1.
$$


My question is whether there is some computer algebra system (in actual existence, I already know that such a system can exist abstractly) that searches for a proof of this new identity (and perhaps, as an added benefit, searches for disproofs too). In other words, is there a decent (hopefully freely available) automatic theorem prover that does the given task; something similar to the program used to show how Robbin's identity in Boolean algebras can be used to get the other identities.



Deriving consequences of identities
The general problem is undecidable, as is shown in


Peter Perkins  

Unsolvable problems for equational theories  

Notre Dame Journal of Formal Logic  

Volume VIII, Number 3, July 1967
Perkins shows that one cannot decide whether an arbitrary finite set of equations in one binary operation symbol entails $x\approx y$.



But there is software that searches for equational proofs.
I have been meaning to experiment with [Prover9](https://en.wikipedia.org/wiki/Prover9), but haven't gotten around to it yet. It is supposed to be able to produce readable proofs in equational logic. Prover9 is used together with Mace4, which searches for countermodels.






