TRS:
 {    a__f(a(), X, X) -> a__f(X, a__b(), b()),
               a__b() -> a(),
  mark(f(X1, X2, X3)) -> a__f(X1, mark(X2), X3),
            mark(b()) -> a__b(),
            mark(a()) -> a(),
     a__f(X1, X2, X3) -> f(X1, X2, X3),
               a__b() -> b()}
 Cdiprover:
  Interpretation class: pizerosimplemixed
  Complexity bound: POLYTIME COMPUTABLE
  f(X6, X5, X4) = + 1*X4 + 1*X5 + 1*X6 + 2
  mark(X3) = + 2*X3^2 + 0 + 2*X3
  a = + 2
  b = + 1
  a__b = + 3
  a__f(X2, X1, X0) = + 2*X2^2 + 0*X1^2 + 2*X0^2 + 0*X1*X2 + 1*X1 + 3 + 1*X2 + 0*X0*X2 + 1*X0 + 0*X0*X1 + 0*X0*X1*X2
  
  Qed