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