%  forall x y z.  plus(plus(x,y),z) = plus(x,plus(y,z))
cnf(associativity_plus,axiom,
    ( plus(plus(X,Y), Z) = plus(X,plus(Y, Z)) )).

% forall x y z.  times(times(x,y),z) = times(x,times(y,z))
cnf(associativity_times,axiom,
    ( times(times(X,Y), Z) = times(X,times(Y, Z)) )).

% forall x y. plus(x,y) = plus(y,x)
cnf(commutativity_plus,axiom,
    ( plus(X,Y) = plus(Y,X) )).

% forall x y. times(x,y) = times(y,x)
cnf(commutativity_times,axiom,
    ( times(X,Y) = times(Y,X) )).

% forall x y, z. times(plus(x,y),z) = plus(times(x,z),times(y,z))
cnf(right_distributivity,axiom,
    ( times(plus(X, Y), Z) = plus(times(X,Z), times(Y,Z)) )).

% forall x y, z. times(x,plus(y,z)) = plus(times(x,y),times(x,z))
cnf(left_distributivity,axiom,
    ( times(X, plus(Y, Z)) = plus(times(X,Y), times(X,Z)) )).

% forall x. plus(zero,x) = x
cnf(left_identity,axiom,
    ( plus(zero, X) = X )).

%forall x. times(one,x) = x
cnf(left_identity,axiom,
    ( times(one,X) = X )).

% forall x. plus(x,x) = zero
cnf(inverse_plus,axiom,
    ( plus(X,X) = zero )).

%forall x. times(x,x) = x
cnf(inverse_times,axiom,
    ( times(X,X) = X )).