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