(VAR X Y X1 X2 X3)
(RULES 
active(f(X)) -> mark(if(X,c,f(true)))
active(if(true,X,Y)) -> mark(X)
active(if(false,X,Y)) -> mark(Y)
mark(f(X)) -> active(f(mark(X)))
mark(if(X1,X2,X3)) -> active(if(mark(X1),mark(X2),X3))
mark(c) -> active(c)
mark(true) -> active(true)
mark(false) -> active(false)
f(mark(X)) -> f(X)
f(active(X)) -> f(X)
if(mark(X1),X2,X3) -> if(X1,X2,X3)
if(X1,mark(X2),X3) -> if(X1,X2,X3)
if(X1,X2,mark(X3)) -> if(X1,X2,X3)
if(active(X1),X2,X3) -> if(X1,X2,X3)
if(X1,active(X2),X3) -> if(X1,X2,X3)
if(X1,X2,active(X3)) -> if(X1,X2,X3)
)