MAYBE MAYBE TRS: { mark(c(X)) -> active(c(X)), mark(f(X)) -> active(f(mark(X))), mark(g(X)) -> active(g(mark(X))), mark(a()) -> active(a()), c(mark(X)) -> c(X), c(active(X)) -> c(X), 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(c(f(g(f(a()))))) } DUP: We consider a non-duplicating system. Trs: { mark(c(X)) -> active(c(X)), mark(f(X)) -> active(f(mark(X))), mark(g(X)) -> active(g(mark(X))), mark(a()) -> active(a()), c(mark(X)) -> c(X), c(active(X)) -> c(X), 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(c(f(g(f(a()))))) } Fail