proof of the lemma:
in a group, if the square of every element is the identity,
the group is commutative.

Axiomas:

equal(Y,X) :> product(e,X,Y).
equal(Y,X) :> product(X,e,Y).

inverse(X1,X) :> product(X1,X,e).
inverse(X1,X),product(X1,X,W) :> equal1(W,e).

associativity:
product(X,Y,U),product(U,Z,V),product(Y,Z,W),product(X,W,W1) :> equal1(V,W1).

equal(X,X) :> equal1(X,X).

product(X,X,W) :> equal1(W,e).

product(a,b,c).
product(b,a,c1).

Query: equal1(c,c1).