MAYBE MAYBE TRS: { if(true(), X, Y) -> X, if(false(), X, Y) -> activate(Y), f(X) -> if(X, c(), n__f(n__true())), f(X) -> n__f(X), true() -> n__true(), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__true()) -> true() } DUP: We consider a non-duplicating system. Trs: { if(true(), X, Y) -> X, if(false(), X, Y) -> activate(Y), f(X) -> if(X, c(), n__f(n__true())), f(X) -> n__f(X), true() -> n__true(), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__true()) -> true() } Fail