Deriving consequences of identities 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, as well as the identities of a $\ast$-ring, 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.
 A: 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, 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.
A: It is not completely clear from the question whether you view the finite set of identities as part of the input or not.  @KeithKearnes answer has the finite list as part of the input (and the identity to be a consequence is fixed).  Murskii proved  (V. L. Murskii, “Some examples of semigroup varieties,” Mat. Zametki, 3, No. 6, 663-670 (1968)) that there is a fixed finite set of semigroup identities so that the consequences of that fixed set of identities is undecidable. The corresponding result for varieties of group was given in Yu. G. KLEIMAN, Identities and some algorithmic problems in groups, Doklady Akademii Nauk
SSSR, vol. 244 (1979), pp. 814-818.
