MAYBE
MAYBE
TRS:
 {
         f(mark(x)) -> mark(f(x)),
       f(active(x)) -> active(f(x)),
           f(no(x)) -> no(f(x)),
       active(f(x)) -> mark(f(f(x))),
      chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
       chk(no(c())) -> active(c()),
  mat(f(x), f(y())) -> f(mat(x, y())),
     mat(f(x), c()) -> no(c()),
        tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
           f(mark(x)) -> mark(f(x)),
         f(active(x)) -> active(f(x)),
             f(no(x)) -> no(f(x)),
         active(f(x)) -> mark(f(f(x))),
        chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))),
         chk(no(c())) -> active(c()),
    mat(f(x), f(y())) -> f(mat(x, y())),
       mat(f(x), c()) -> no(c()),
          tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x)))
   }
  Fail