TRS: { f(x, y) -> g1(x, x, y), f(x, y) -> g1(y, x, x), f(x, y) -> g2(x, y, y), f(x, y) -> g2(y, y, x), g1(x, x, y) -> h(x, y), g1(y, x, x) -> h(x, y), g2(x, y, y) -> h(x, y), g2(y, y, x) -> h(x, y), h(x, x) -> x} Cdiprover: Interpretation class: pizerosimplemixed Complexity bound: POLYTIME COMPUTABLE h(X9, X8) = + 0*X9^2 + 0*X8^2 + 1*X9 + 1 + 1*X8 + 0*X8*X9 g2(X7, X6, X5) = + 0*X7^2 + 0*X6^2 + 0*X5^2 + 0*X6*X7 + 1*X6 + 2 + 1*X7 + 0*X5*X7 + 1*X5 + 0*X5*X6 + 0*X5*X6*X7 f(X4, X3) = + 2*X4^2 + 2*X3^2 + 3*X4 + 3 + 2*X3 + 0*X3*X4 g1(X2, X1, X0) = + 2*X2^2 + 0*X1^2 + 0*X0^2 + 0*X1*X2 + 2*X1 + 2 + 1*X2 + 0*X0*X2 + 1*X0 + 0*X0*X1 + 0*X0*X1*X2 Qed