Good report!
On the benchmark examples:
>> First example. Prove from the following axioms of group theory:
>> x(y.z) = (x.y).z
>> x.1 = x
>> x.i(x) = 1
>> the theorem
>> 1.x = x
In this sort of purely equational reasoning, computers often outdo
humans; for example, Otter gets a proof in < 1 second.
Otter's proof is somewhat shorter that the one quoted from Hall.
A word of caution when we go to sell this area to mathematicians:
I quote, without comment, from "Algebra" by I. Martin Isaacs
(Brooks/Cole 1994), where this result is Theorem 1.6:
We should mention that the "elementwise" calculations in the
preceding proof are not typical of most algebra. The proof of
Theorem 1.6, in fact, could almost serve as a model of what algebra
is not, or at least should not be, in the opinion of the author.
Ken Kunen