MAYBE
MAYBE
TRS:
 {
          mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(0()) -> active(0()),
               mark(zeros()) -> active(zeros()),
           mark(U12(X1, X2)) -> active(U12(mark(X1), X2)),
                  mark(tt()) -> active(tt()),
           mark(U11(X1, X2)) -> active(U11(mark(X1), X2)),
                  mark(s(X)) -> active(s(mark(X))),
             mark(length(X)) -> active(length(mark(X))),
                 mark(nil()) -> active(nil()),
          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),
             active(zeros()) -> mark(cons(0(), zeros())),
        active(U12(tt(), L)) -> mark(s(length(L))),
        active(U11(tt(), L)) -> mark(U12(tt(), L)),
  active(length(cons(N, L))) -> mark(U11(tt(), L)),
       active(length(nil())) -> mark(0()),
           U12(X1, mark(X2)) -> U12(X1, X2),
         U12(X1, active(X2)) -> U12(X1, X2),
           U12(mark(X1), X2) -> U12(X1, X2),
         U12(active(X1), X2) -> U12(X1, X2),
           U11(X1, mark(X2)) -> U11(X1, X2),
         U11(X1, active(X2)) -> U11(X1, X2),
           U11(mark(X1), X2) -> U11(X1, X2),
         U11(active(X1), X2) -> U11(X1, X2),
                  s(mark(X)) -> s(X),
                s(active(X)) -> s(X),
             length(mark(X)) -> length(X),
           length(active(X)) -> length(X)
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
            mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                     mark(0()) -> active(0()),
                 mark(zeros()) -> active(zeros()),
             mark(U12(X1, X2)) -> active(U12(mark(X1), X2)),
                    mark(tt()) -> active(tt()),
             mark(U11(X1, X2)) -> active(U11(mark(X1), X2)),
                    mark(s(X)) -> active(s(mark(X))),
               mark(length(X)) -> active(length(mark(X))),
                   mark(nil()) -> active(nil()),
            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),
               active(zeros()) -> mark(cons(0(), zeros())),
          active(U12(tt(), L)) -> mark(s(length(L))),
          active(U11(tt(), L)) -> mark(U12(tt(), L)),
    active(length(cons(N, L))) -> mark(U11(tt(), L)),
         active(length(nil())) -> mark(0()),
             U12(X1, mark(X2)) -> U12(X1, X2),
           U12(X1, active(X2)) -> U12(X1, X2),
             U12(mark(X1), X2) -> U12(X1, X2),
           U12(active(X1), X2) -> U12(X1, X2),
             U11(X1, mark(X2)) -> U11(X1, X2),
           U11(X1, active(X2)) -> U11(X1, X2),
             U11(mark(X1), X2) -> U11(X1, X2),
           U11(active(X1), X2) -> U11(X1, X2),
                    s(mark(X)) -> s(X),
                  s(active(X)) -> s(X),
               length(mark(X)) -> length(X),
             length(active(X)) -> length(X)
   }
  Fail