MAYBE
MAYBE
TRS:
 {
    mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
             mark(0()) -> active(0()),
            mark(f(X)) -> active(f(mark(X))),
            mark(s(X)) -> active(s(mark(X))),
            mark(p(X)) -> active(p(mark(X))),
    cons(X1, mark(X2)) -> cons(X1, X2),
  cons(X1, active(X2)) -> cons(X1, X2),
    cons(mark(X1), X2) -> cons(X1, X2),
  cons(active(X1), X2) -> cons(X1, X2),
            f(mark(X)) -> f(X),
          f(active(X)) -> f(X),
            s(mark(X)) -> s(X),
          s(active(X)) -> s(X),
        active(f(0())) -> mark(cons(0(), f(s(0())))),
     active(f(s(0()))) -> mark(f(p(s(0())))),
       active(p(s(X))) -> mark(X),
            p(mark(X)) -> p(X),
          p(active(X)) -> p(X)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
      mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
               mark(0()) -> active(0()),
              mark(f(X)) -> active(f(mark(X))),
              mark(s(X)) -> active(s(mark(X))),
              mark(p(X)) -> active(p(mark(X))),
      cons(X1, mark(X2)) -> cons(X1, X2),
    cons(X1, active(X2)) -> cons(X1, X2),
      cons(mark(X1), X2) -> cons(X1, X2),
    cons(active(X1), X2) -> cons(X1, X2),
              f(mark(X)) -> f(X),
            f(active(X)) -> f(X),
              s(mark(X)) -> s(X),
            s(active(X)) -> s(X),
          active(f(0())) -> mark(cons(0(), f(s(0())))),
       active(f(s(0()))) -> mark(f(p(s(0())))),
         active(p(s(X))) -> mark(X),
              p(mark(X)) -> p(X),
            p(active(X)) -> p(X)
   }
  Fail