I am looking for some mathematical software that can help me with a very common task in the realm of universal algebra (as far as I know programs like prover9/mace4 and uacalc do not help with this issue).
The input of this software should be two different finite algebras, each of them given through the table of its operations. Thus, particular cases are considering two finite groups, two Boolean algebras, etc.
The answer (in case the computer search finds something) of this software should be an equation that can distinguish these two finite algebras in the sense that it is valid in one of them, while not valid in the other algebra. The idea is that the software automatically searches for an equation in the corresponding algebraic signature such that it is valid in one of these algebras but not valid in the other one. For instance, if we consider the two finite algebras to be the additive groups of $\mathbb{Z}/2$ and $\mathbb{Z}/3$ an equation that is valid in $\mathbb{Z}/2$ but not in $\mathbb{Z}/3$ is $x + x = y + y$; hence $x+x = y+y$ is an example of the kind of answer I am looking for. On the other hand, there is not such an equation to distinguish the $2$ elements Boolean algebra from the $4$ elements Boolean one; hence, in this case, the computer search will run forever without providing an answer.
In case anyone knows a software to do the previous task, let me point out that I am also interested in getting answers bounding the number of variables appearing in the equations. Here I refer to getting answers of the following kind: with equations that only use $3$ variables there is no way distinguish these two finite algebras, with equations that only use $4$ variables there is no way distinguish these two finite algebras, and with equations that only use $5$ variables we can distinguish them using this explicit equation (the one given by the software as answer).