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