MAYBE MAYBE TRS: { mark(f(X)) -> active(f(mark(X))), mark(g(X)) -> active(g(X)), mark(a()) -> active(a()), f(mark(X)) -> f(X), f(active(X)) -> f(X), g(mark(X)) -> g(X), g(active(X)) -> g(X), active(f(f(a()))) -> mark(f(g(f(a())))) } DUP: We consider a non-duplicating system. Trs: { mark(f(X)) -> active(f(mark(X))), mark(g(X)) -> active(g(X)), mark(a()) -> active(a()), f(mark(X)) -> f(X), f(active(X)) -> f(X), g(mark(X)) -> g(X), g(active(X)) -> g(X), active(f(f(a()))) -> mark(f(g(f(a())))) } Fail