% Original problem:
input_clause(axiom,axiom,[++equal(plus(X,plus(Y,Z)),plus(plus(X,Y),Z))]).
input_clause(axiom,axiom,[++equal(plus(X,Y),plus(Y,X))]).
input_clause(axiom,axiom,[++equal(plus(X,zero),X)]).
input_clause(axiom,axiom,[--equal(crypt(plus(X,Y),Z),plus(crypt(X,Z),crypt(Y,Z)))]).
% Domain:
input_clause(axiom,axiom,[++equal(X,c__1),++equal(X,c__2)]).
input_clause(axiom,axiom,[--equal(c__1,c__2)]).
% Model: