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