(VAR X X1 X2 X3 Y )
(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)
        
)