YES(?,O(n^2)) TRS: { f(g(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())), f(g(i(a(), b(), b'()), c()), d()) -> if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())) } DUP: We consider a non-duplicating system. Trs: { f(g(h(a(), b()), c()), d()) -> if(e(), f(.(b(), g(h(a(), b()), c())), d()), f(c(), d'())), f(g(i(a(), b(), b'()), c()), d()) -> if(e(), f(.(b(), c()), d'()), f(.(b'(), c()), d'())) } Matrix Interpretation: Interpretation class: triangular [2] [d] = [0] [0] [a] = [0] [X5] [X3] [X1] [1 0][X5] [1 0][X3] [1 0][X1] [0] [i]([X4], [X2], [X0]) = [0 0][X4] + [0 0][X2] + [0 0][X0] + [0] [0] [b'] = [0] [0] [d'] = [0] [0] [c] = [0] [0] [b] = [1] [X3] [X1] [1 0][X3] [1 0][X1] [0] [.]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [0] [0] [e] = [0] [X5] [X3] [X1] [1 0][X5] [1 0][X3] [1 0][X1] [0] [if]([X4], [X2], [X0]) = [0 0][X4] + [0 0][X2] + [0 0][X0] + [0] [X3] [X1] [1 0][X3] [1 0][X1] [0] [h]([X2], [X0]) = [0 0][X2] + [0 1][X0] + [0] [X3] [X1] [1 0][X3] [1 0][X1] [0] [g]([X2], [X0]) = [0 1][X2] + [0 0][X0] + [2] [X3] [X1] [1 2][X3] [1 0][X1] [0] [f]([X2], [X0]) = [0 0][X2] + [0 0][X0] + [0] Qed