MAYBE MAYBE TRS: { c(X) -> d(activate(X)), f(X) -> n__f(X), f(f(X)) -> c(n__f(n__g(n__f(X)))), d(X) -> n__d(X), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__g(X)) -> g(X), activate(n__d(X)) -> d(X), h(X) -> c(n__d(X)), g(X) -> n__g(X) } DUP: We consider a non-duplicating system. Trs: { c(X) -> d(activate(X)), f(X) -> n__f(X), f(f(X)) -> c(n__f(n__g(n__f(X)))), d(X) -> n__d(X), activate(X) -> X, activate(n__f(X)) -> f(activate(X)), activate(n__g(X)) -> g(X), activate(n__d(X)) -> d(X), h(X) -> c(n__d(X)), g(X) -> n__g(X) } Fail