(VAR X X1 X2 X3)
(RULES 
active(f(a,X,X)) -> mark(f(X,b,b))
active(b) -> mark(a)
mark(f(X1,X2,X3)) -> active(f(X1,mark(X2),X3))
mark(a) -> active(a)
mark(b) -> active(b)
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)
)