TRS: { a__f(X) -> a__if(mark(X), c(), f(true())), a__if(true(), X, Y) -> mark(X), a__if(false(), X, Y) -> mark(Y), mark(f(X)) -> a__f(mark(X)), mark(if(X1, X2, X3)) -> a__if(mark(X1), mark(X2), X3), mark(c()) -> c(), mark(true()) -> true(), mark(false()) -> false(), a__f(X) -> f(X), a__if(X1, X2, X3) -> if(X1, X2, X3)} Fail