YES O(n^5) 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) } Matrix Interpretation: Interpretation class: triangular [X4] [1 0 0 0 0][X4] [6] [X3] [0 0 0 0 0][X3] [1] [g]([X2]) = [0 0 0 0 0][X2] + [0] [X1] [0 0 0 0 0][X1] [0] [X0] [0 0 0 0 0][X0] [0] [X4] [1 2 0 0 0][X4] [7] [X3] [0 0 0 0 0][X3] [0] [h]([X2]) = [0 0 0 0 0][X2] + [1] [X1] [0 0 0 0 0][X1] [0] [X0] [0 0 0 0 0][X0] [0] [X4] [1 2 0 0 0][X4] [0] [X3] [0 0 0 0 0][X3] [0] [n__d]([X2]) = [0 0 0 0 0][X2] + [1] [X1] [0 0 0 0 0][X1] [0] [X0] [0 0 0 0 0][X0] [0] [X4] [1 3 2 0 0][X4] [1] [X3] [0 1 0 0 0][X3] [0] [activate]([X2]) = [0 0 1 0 0][X2] + [0] [X1] [0 0 0 1 3][X1] [0] [X0] [0 0 0 0 1][X0] [0] [X4] [1 2 0 0 0][X4] [1] [X3] [0 0 0 0 0][X3] [0] [d]([X2]) = [0 0 0 0 0][X2] + [1] [X1] [0 0 0 0 0][X1] [0] [X0] [0 0 0 0 0][X0] [0] [X4] [1 0 0 0 4][X4] [1] [X3] [0 1 0 0 6][X3] [1] [f]([X2]) = [0 0 1 0 6][X2] + [0] [X1] [0 0 0 0 0][X1] [0] [X0] [0 0 0 0 0][X0] [6] [X4] [1 0 0 0 0][X4] [5] [X3] [0 0 0 0 0][X3] [1] [n__g]([X2]) = [0 0 0 0 0][X2] + [0] [X1] [0 0 0 0 0][X1] [0] [X0] [0 0 0 0 0][X0] [0] [X4] [1 0 0 0 4][X4] [0] [X3] [0 1 0 0 6][X3] [1] [n__f]([X2]) = [0 0 1 0 6][X2] + [0] [X1] [0 0 0 0 0][X1] [0] [X0] [0 0 0 0 0][X0] [6] [X4] [1 5 2 0 0][X4] [3] [X3] [0 0 0 2 0][X3] [0] [c]([X2]) = [0 0 0 2 0][X2] + [1] [X1] [0 0 0 1 0][X1] [0] [X0] [0 0 0 0 0][X0] [0] Qed