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}
 RPO Product:
  Quasi-Precedence:
  g2 > h, 
  g1 > h, 
  f > g2, 
  f > g1
  empty
  
  Qed


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: quasisimplemixed
  Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING
  h(X9, X8) = + 0*X9^2 + 0*X8^2 + 1*X9 + 0 + 1*X8 + 0*X8*X9
  g2(X7, X6, X5) = + 0*X7^2 + 0*X6^2 + 0*X5^2 + 0*X6*X7 + 1*X6 + 0 + 1*X7 + 0*X5*X7 + 1*X5 + 0*X5*X6 + 0*X5*X6*X7
  f(X4, X3) = + 0*X4^2 + 0*X3^2 + 3*X4 + 0 + 2*X3 + 0*X3*X4
  g1(X2, X1, X0) = + 0*X2^2 + 0*X1^2 + 0*X0^2 + 0*X1*X2 + 2*X1 + 0 + 1*X2 + 0*X0*X2 + 1*X0 + 0*X0*X1 + 0*X0*X1*X2
  
  Qed