(VAR X X1 X2) (RULES a__f(X,X) -> a__f(a,b) a__b -> a mark(f(X1,X2)) -> a__f(mark(X1),X2) mark(b) -> a__b mark(a) -> a a__f(X1,X2) -> f(X1,X2) a__b -> b )