twee-2.6.1: tests/wos.p

cnf(a, axiom,
    prod(inv(prod(inv(prod(inv(prod(Xl,X2)),prod(X2,Xl))),prod(inv(prod(Z,Y)), prod(Z,inv(prod(prod(V,inv(X)),inv(Y))))))),X) = V).

%fof(associativity, conjecture, prod(a,prod(b,c)) = prod(prod(a,b),c)).
fof(identity_and_inverse, conjecture,  ?[X]: (![Y]: prod(X,Y)=Y & ![Y]: prod(Y, inv(Y)) = X)).
%fof(commutativity, conjecture, prod(a,b) = prod(b,a)).