MAYBE
MAYBE
TRS:
 {
          mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
               mark(from(X)) -> active(from(mark(X))),
                  mark(s(X)) -> active(s(mark(X))),
                   mark(0()) -> active(0()),
             mark(length(X)) -> active(length(X)),
                 mark(nil()) -> active(nil()),
            mark(length1(X)) -> active(length1(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),
               from(mark(X)) -> from(X),
             from(active(X)) -> from(X),
                  s(mark(X)) -> s(X),
                s(active(X)) -> s(X),
             active(from(X)) -> mark(cons(X, from(s(X)))),
  active(length(cons(X, Y))) -> mark(s(length1(Y))),
       active(length(nil())) -> mark(0()),
          active(length1(X)) -> mark(length(X)),
             length(mark(X)) -> length(X),
           length(active(X)) -> length(X),
            length1(mark(X)) -> length1(X),
          length1(active(X)) -> length1(X)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
            mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                 mark(from(X)) -> active(from(mark(X))),
                    mark(s(X)) -> active(s(mark(X))),
                     mark(0()) -> active(0()),
               mark(length(X)) -> active(length(X)),
                   mark(nil()) -> active(nil()),
              mark(length1(X)) -> active(length1(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),
                 from(mark(X)) -> from(X),
               from(active(X)) -> from(X),
                    s(mark(X)) -> s(X),
                  s(active(X)) -> s(X),
               active(from(X)) -> mark(cons(X, from(s(X)))),
    active(length(cons(X, Y))) -> mark(s(length1(Y))),
         active(length(nil())) -> mark(0()),
            active(length1(X)) -> mark(length(X)),
               length(mark(X)) -> length(X),
             length(active(X)) -> length(X),
              length1(mark(X)) -> length1(X),
            length1(active(X)) -> length1(X)
   }
  Fail