MAYBE
MAYBE
TRS:
 {
          mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                   mark(0()) -> active(0()),
               mark(zeros()) -> active(zeros()),
           mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                  mark(tt()) -> active(tt()),
             mark(length(X)) -> active(length(mark(X))),
                 mark(nil()) -> active(nil()),
                  mark(s(X)) -> active(s(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),
             active(zeros()) -> mark(cons(0(), zeros())),
        active(and(tt(), X)) -> mark(X),
  active(length(cons(N, L))) -> mark(s(length(L))),
       active(length(nil())) -> mark(0()),
           and(X1, mark(X2)) -> and(X1, X2),
         and(X1, active(X2)) -> and(X1, X2),
           and(mark(X1), X2) -> and(X1, X2),
         and(active(X1), X2) -> and(X1, X2),
             length(mark(X)) -> length(X),
           length(active(X)) -> length(X),
                  s(mark(X)) -> s(X),
                s(active(X)) -> s(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(and(X1, X2)) -> active(and(mark(X1), X2)),
                    mark(tt()) -> active(tt()),
               mark(length(X)) -> active(length(mark(X))),
                   mark(nil()) -> active(nil()),
                    mark(s(X)) -> active(s(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),
               active(zeros()) -> mark(cons(0(), zeros())),
          active(and(tt(), X)) -> mark(X),
    active(length(cons(N, L))) -> mark(s(length(L))),
         active(length(nil())) -> mark(0()),
             and(X1, mark(X2)) -> and(X1, X2),
           and(X1, active(X2)) -> and(X1, X2),
             and(mark(X1), X2) -> and(X1, X2),
           and(active(X1), X2) -> and(X1, X2),
               length(mark(X)) -> length(X),
             length(active(X)) -> length(X),
                    s(mark(X)) -> s(X),
                  s(active(X)) -> s(X)
   }
  Fail