:-option(ac(off)).

(X-Y)-X=0.
X-0=X.
(X-Y)-(Z-Y) = (X-Z)-(Y-Z).
X-(X-Y)=Y-(Y-X).
f(X,Y)=f(Y,X).
f(X,Y)=X-(X-Y).

:-sarp([1-4,6-9]).  % usual simplifications + case analysis
:-option([term_var_weight,var_depth(3),memo_constraints(on)]).
precedence([-,f,0]).