cnf(associativity, axiom, ( multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) )).
cnf(left_identity, axiom, ( multiply(identity,X) = X )).
cnf(left_inverse, axiom, ( multiply(inverse(X),X) = identity )).
cnf(product_equality, hypothesis, ( multiply(b,c) = multiply(d,c) )).