TRS:
 {a__f(f(a())) -> c(f(g(f(a())))),
    mark(f(X)) -> a__f(mark(X)),
     mark(a()) -> a(),
    mark(c(X)) -> c(X),
    mark(g(X)) -> g(mark(X)),
       a__f(X) -> f(X)}
 RPO Product:
  Quasi-Precedence:
  mark > a__f
  empty
  
  Qed


TRS:
 {a__f(f(a())) -> c(f(g(f(a())))),
    mark(f(X)) -> a__f(mark(X)),
     mark(a()) -> a(),
    mark(c(X)) -> c(X),
    mark(g(X)) -> g(mark(X)),
       a__f(X) -> f(X)}
 Cdiprover:
  Interpretation class: quasisimplemixed
  Complexity bound: POLYTIME COMPUTABLE IF RPO-TERMINATING
  mark(X4) = + 2*X4^2 + 2 + 1*X4
  a__f(X3) = + 0*X3^2 + 3 + 1*X3
  a = + 0
  g(X2) = + 1*X2 + 1
  f(X1) = + 1*X1 + 1
  c(X0) = + 1*X0 + 1
  
  Qed