Recently, we have developed a new concept of "power-like function" generalizing the standard notion of power-maps in a group or a semigroup. This idea can be applied for a large of class of commutativity theorems. Our proof belongs to first-order logic and uses a first-order theorem-prover "Prover9". Normally, first-order theorem provers cannot handle sentences involving arbitrary integer variables, This is the first time that Prover9 has been augmented by power-like functions to enable the software to prove new theorems in this area.
In this paper, using Prover9 and power-like functions, we prove and extend a well-known theorem by Neumann (2001). In these automated proofs, the integer variable never explicitly appears and hence the lengths of the proofs as well as the lengths of the longest clause in these proofs remain the same irrespective of the value of n. It is also possible to use similar automated proofs in equational theory of rings.