proof of the lemma: in a group, if the square of every element is the identity, the group is commutative. Axiomas: equal(X,X) :> product(e,X,X). equal(X,X) :> product(X,e,X). inverse(X1,X) :> product(X1,X,e). product(X1,X,e) :> inverse(X1,X). inverse(X1,X),product(X1,X,W) :> equal(W,e). associativity: product(X,Y,U),product(Y,Z,V),product(U,Z,W) :> product(X,V,W). product(X,Y,U),product(Y,Z,V),product(X,V,W) :> product(U,Z,W). equal(X,X) :> product(X,X,e). product(a,b,c). product(d,f,e). Query: product(b,a,c).