input_clause(assoc_plus,axiom,
	     [++equal(plus(X,plus(Y,Z)),plus(plus(X,Y),Z))]).
input_clause(comm_plus,axiom,
	     [++equal(plus(X,Y),plus(Y,X))]).
input_clause(plus_zero,axiom,
	     [++equal(plus(X,zero),X)]).

input_clause(zero_plus,axiom,
	     [--equal(plus(zero,a),a)]).