MAYBE
MAYBE
TRS:
 {
          cons(mark(X1), X2) -> mark(cons(X1, X2)),
        cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
               from(mark(X)) -> mark(from(X)),
                 from(ok(X)) -> ok(from(X)),
                  s(mark(X)) -> mark(s(X)),
                    s(ok(X)) -> ok(s(X)),
        active(cons(X1, X2)) -> cons(active(X1), X2),
             active(from(X)) -> mark(cons(X, from(s(X)))),
             active(from(X)) -> from(active(X)),
                active(s(X)) -> s(active(X)),
  active(length(cons(X, Y))) -> mark(s(length1(Y))),
       active(length(nil())) -> mark(0()),
          active(length1(X)) -> mark(length(X)),
               length(ok(X)) -> ok(length(X)),
              length1(ok(X)) -> ok(length1(X)),
        proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
             proper(from(X)) -> from(proper(X)),
                proper(s(X)) -> s(proper(X)),
                 proper(0()) -> ok(0()),
           proper(length(X)) -> length(proper(X)),
               proper(nil()) -> ok(nil()),
          proper(length1(X)) -> length1(proper(X)),
                top(mark(X)) -> top(proper(X)),
                  top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
            cons(mark(X1), X2) -> mark(cons(X1, X2)),
          cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                 from(mark(X)) -> mark(from(X)),
                   from(ok(X)) -> ok(from(X)),
                    s(mark(X)) -> mark(s(X)),
                      s(ok(X)) -> ok(s(X)),
          active(cons(X1, X2)) -> cons(active(X1), X2),
               active(from(X)) -> mark(cons(X, from(s(X)))),
               active(from(X)) -> from(active(X)),
                  active(s(X)) -> s(active(X)),
    active(length(cons(X, Y))) -> mark(s(length1(Y))),
         active(length(nil())) -> mark(0()),
            active(length1(X)) -> mark(length(X)),
                 length(ok(X)) -> ok(length(X)),
                length1(ok(X)) -> ok(length1(X)),
          proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
               proper(from(X)) -> from(proper(X)),
                  proper(s(X)) -> s(proper(X)),
                   proper(0()) -> ok(0()),
             proper(length(X)) -> length(proper(X)),
                 proper(nil()) -> ok(nil()),
            proper(length1(X)) -> length1(proper(X)),
                  top(mark(X)) -> top(proper(X)),
                    top(ok(X)) -> top(active(X))
   }
  Fail