cnf(multiply_add_property, axiom, ( multiply(X,add(Y,Z)) = add(multiply(Y,X),multiply(Z,X)) )).
cnf(additive_inverse, axiom, ( add(X,inverse(X)) = one )).
cnf(pixley1, axiom, ( add(multiply(X,inverse(X)),add(multiply(X,Y),multiply(inverse(X),Y))) = Y )).
cnf(pixley2, axiom, ( add(multiply(X,inverse(Y)),add(multiply(X,Y),multiply(inverse(Y),Y))) = X )).
cnf(pixley3, axiom, ( add(multiply(X,inverse(Y)),add(multiply(X,X),multiply(inverse(Y),X))) = X )).