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