EQP

EQP, an abbreviation for Equational Prover is an automated theorem-proving program for first-order equational logic, developed by the Mathematics and Computer Science Division of the Argonne National Laboratory and among other used for solving the problem proposed by Herbert Robbins whether all Robbins algebras are Boolean, the problem arised from the Huntington's equation from 1933:

$n(n(x) + y) + n(n(x) + n(y)) = x \; .$