MAYBE

Problem:
 active(zeros()) -> mark(cons(0(),zeros()))
 active(U11(tt(),L)) -> mark(U12(tt(),L))
 active(U12(tt(),L)) -> mark(s(length(L)))
 active(length(nil())) -> mark(0())
 active(length(cons(N,L))) -> mark(U11(tt(),L))
 mark(zeros()) -> active(zeros())
 mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
 mark(0()) -> active(0())
 mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
 mark(tt()) -> active(tt())
 mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
 mark(s(X)) -> active(s(mark(X)))
 mark(length(X)) -> active(length(mark(X)))
 mark(nil()) -> active(nil())
 cons(mark(X1),X2) -> cons(X1,X2)
 cons(X1,mark(X2)) -> cons(X1,X2)
 cons(active(X1),X2) -> cons(X1,X2)
 cons(X1,active(X2)) -> cons(X1,X2)
 U11(mark(X1),X2) -> U11(X1,X2)
 U11(X1,mark(X2)) -> U11(X1,X2)
 U11(active(X1),X2) -> U11(X1,X2)
 U11(X1,active(X2)) -> U11(X1,X2)
 U12(mark(X1),X2) -> U12(X1,X2)
 U12(X1,mark(X2)) -> U12(X1,X2)
 U12(active(X1),X2) -> U12(X1,X2)
 U12(X1,active(X2)) -> U12(X1,X2)
 s(mark(X)) -> s(X)
 s(active(X)) -> s(X)
 length(mark(X)) -> length(X)
 length(active(X)) -> length(X)

Proof:
 DP Processor:
  DPs:
   active#(zeros()) -> cons#(0(),zeros())
   active#(zeros()) -> mark#(cons(0(),zeros()))
   active#(U11(tt(),L)) -> U12#(tt(),L)
   active#(U11(tt(),L)) -> mark#(U12(tt(),L))
   active#(U12(tt(),L)) -> length#(L)
   active#(U12(tt(),L)) -> s#(length(L))
   active#(U12(tt(),L)) -> mark#(s(length(L)))
   active#(length(nil())) -> mark#(0())
   active#(length(cons(N,L))) -> U11#(tt(),L)
   active#(length(cons(N,L))) -> mark#(U11(tt(),L))
   mark#(zeros()) -> active#(zeros())
   mark#(cons(X1,X2)) -> mark#(X1)
   mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
   mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
   mark#(0()) -> active#(0())
   mark#(U11(X1,X2)) -> mark#(X1)
   mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
   mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
   mark#(tt()) -> active#(tt())
   mark#(U12(X1,X2)) -> mark#(X1)
   mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
   mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
   mark#(s(X)) -> mark#(X)
   mark#(s(X)) -> s#(mark(X))
   mark#(s(X)) -> active#(s(mark(X)))
   mark#(length(X)) -> mark#(X)
   mark#(length(X)) -> length#(mark(X))
   mark#(length(X)) -> active#(length(mark(X)))
   mark#(nil()) -> active#(nil())
   cons#(mark(X1),X2) -> cons#(X1,X2)
   cons#(X1,mark(X2)) -> cons#(X1,X2)
   cons#(active(X1),X2) -> cons#(X1,X2)
   cons#(X1,active(X2)) -> cons#(X1,X2)
   U11#(mark(X1),X2) -> U11#(X1,X2)
   U11#(X1,mark(X2)) -> U11#(X1,X2)
   U11#(active(X1),X2) -> U11#(X1,X2)
   U11#(X1,active(X2)) -> U11#(X1,X2)
   U12#(mark(X1),X2) -> U12#(X1,X2)
   U12#(X1,mark(X2)) -> U12#(X1,X2)
   U12#(active(X1),X2) -> U12#(X1,X2)
   U12#(X1,active(X2)) -> U12#(X1,X2)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   length#(mark(X)) -> length#(X)
   length#(active(X)) -> length#(X)
  TRS:
   active(zeros()) -> mark(cons(0(),zeros()))
   active(U11(tt(),L)) -> mark(U12(tt(),L))
   active(U12(tt(),L)) -> mark(s(length(L)))
   active(length(nil())) -> mark(0())
   active(length(cons(N,L))) -> mark(U11(tt(),L))
   mark(zeros()) -> active(zeros())
   mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
   mark(0()) -> active(0())
   mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
   mark(tt()) -> active(tt())
   mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
   mark(s(X)) -> active(s(mark(X)))
   mark(length(X)) -> active(length(mark(X)))
   mark(nil()) -> active(nil())
   cons(mark(X1),X2) -> cons(X1,X2)
   cons(X1,mark(X2)) -> cons(X1,X2)
   cons(active(X1),X2) -> cons(X1,X2)
   cons(X1,active(X2)) -> cons(X1,X2)
   U11(mark(X1),X2) -> U11(X1,X2)
   U11(X1,mark(X2)) -> U11(X1,X2)
   U11(active(X1),X2) -> U11(X1,X2)
   U11(X1,active(X2)) -> U11(X1,X2)
   U12(mark(X1),X2) -> U12(X1,X2)
   U12(X1,mark(X2)) -> U12(X1,X2)
   U12(active(X1),X2) -> U12(X1,X2)
   U12(X1,active(X2)) -> U12(X1,X2)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   length(mark(X)) -> length(X)
   length(active(X)) -> length(X)
  CDG Processor:
   DPs:
    active#(zeros()) -> cons#(0(),zeros())
    active#(zeros()) -> mark#(cons(0(),zeros()))
    active#(U11(tt(),L)) -> U12#(tt(),L)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    active#(U12(tt(),L)) -> length#(L)
    active#(U12(tt(),L)) -> s#(length(L))
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    active#(length(nil())) -> mark#(0())
    active#(length(cons(N,L))) -> U11#(tt(),L)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(zeros()) -> active#(zeros())
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(0()) -> active#(0())
    mark#(U11(X1,X2)) -> mark#(X1)
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(tt()) -> active#(tt())
    mark#(U12(X1,X2)) -> mark#(X1)
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(length(X)) -> mark#(X)
    mark#(length(X)) -> length#(mark(X))
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(nil()) -> active#(nil())
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2)
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    U11#(active(X1),X2) -> U11#(X1,X2)
    U11#(X1,active(X2)) -> U11#(X1,X2)
    U12#(mark(X1),X2) -> U12#(X1,X2)
    U12#(X1,mark(X2)) -> U12#(X1,X2)
    U12#(active(X1),X2) -> U12#(X1,X2)
    U12#(X1,active(X2)) -> U12#(X1,X2)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    length#(mark(X)) -> length#(X)
    length#(active(X)) -> length#(X)
   TRS:
    active(zeros()) -> mark(cons(0(),zeros()))
    active(U11(tt(),L)) -> mark(U12(tt(),L))
    active(U12(tt(),L)) -> mark(s(length(L)))
    active(length(nil())) -> mark(0())
    active(length(cons(N,L))) -> mark(U11(tt(),L))
    mark(zeros()) -> active(zeros())
    mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    mark(0()) -> active(0())
    mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
    mark(tt()) -> active(tt())
    mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
    mark(s(X)) -> active(s(mark(X)))
    mark(length(X)) -> active(length(mark(X)))
    mark(nil()) -> active(nil())
    cons(mark(X1),X2) -> cons(X1,X2)
    cons(X1,mark(X2)) -> cons(X1,X2)
    cons(active(X1),X2) -> cons(X1,X2)
    cons(X1,active(X2)) -> cons(X1,X2)
    U11(mark(X1),X2) -> U11(X1,X2)
    U11(X1,mark(X2)) -> U11(X1,X2)
    U11(active(X1),X2) -> U11(X1,X2)
    U11(X1,active(X2)) -> U11(X1,X2)
    U12(mark(X1),X2) -> U12(X1,X2)
    U12(X1,mark(X2)) -> U12(X1,X2)
    U12(active(X1),X2) -> U12(X1,X2)
    U12(X1,active(X2)) -> U12(X1,X2)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    length(mark(X)) -> length(X)
    length(active(X)) -> length(X)
   graph:
    U11#(mark(X1),X2) -> U11#(X1,X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(mark(X1),X2) -> U11#(X1,X2) ->
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    U11#(mark(X1),X2) -> U11#(X1,X2) ->
    U11#(active(X1),X2) -> U11#(X1,X2)
    U11#(mark(X1),X2) -> U11#(X1,X2) ->
    U11#(X1,active(X2)) -> U11#(X1,X2)
    U11#(active(X1),X2) -> U11#(X1,X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(active(X1),X2) -> U11#(X1,X2) ->
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    U11#(active(X1),X2) -> U11#(X1,X2) ->
    U11#(active(X1),X2) -> U11#(X1,X2)
    U11#(active(X1),X2) -> U11#(X1,X2) ->
    U11#(X1,active(X2)) -> U11#(X1,X2)
    U11#(X1,mark(X2)) -> U11#(X1,X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(X1,mark(X2)) -> U11#(X1,X2) ->
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    U11#(X1,mark(X2)) -> U11#(X1,X2) ->
    U11#(active(X1),X2) -> U11#(X1,X2)
    U11#(X1,mark(X2)) -> U11#(X1,X2) ->
    U11#(X1,active(X2)) -> U11#(X1,X2)
    U11#(X1,active(X2)) -> U11#(X1,X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(X1,active(X2)) -> U11#(X1,X2) ->
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    U11#(X1,active(X2)) -> U11#(X1,X2) ->
    U11#(active(X1),X2) -> U11#(X1,X2)
    U11#(X1,active(X2)) -> U11#(X1,X2) -> U11#(X1,active(X2)) -> U11#(X1,X2)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    length#(mark(X)) -> length#(X) -> length#(mark(X)) -> length#(X)
    length#(mark(X)) -> length#(X) ->
    length#(active(X)) -> length#(X)
    length#(active(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    length#(active(X)) -> length#(X) ->
    length#(active(X)) -> length#(X)
    U12#(mark(X1),X2) -> U12#(X1,X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    U12#(mark(X1),X2) -> U12#(X1,X2) ->
    U12#(X1,mark(X2)) -> U12#(X1,X2)
    U12#(mark(X1),X2) -> U12#(X1,X2) ->
    U12#(active(X1),X2) -> U12#(X1,X2)
    U12#(mark(X1),X2) -> U12#(X1,X2) ->
    U12#(X1,active(X2)) -> U12#(X1,X2)
    U12#(active(X1),X2) -> U12#(X1,X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    U12#(active(X1),X2) -> U12#(X1,X2) ->
    U12#(X1,mark(X2)) -> U12#(X1,X2)
    U12#(active(X1),X2) -> U12#(X1,X2) ->
    U12#(active(X1),X2) -> U12#(X1,X2)
    U12#(active(X1),X2) -> U12#(X1,X2) ->
    U12#(X1,active(X2)) -> U12#(X1,X2)
    U12#(X1,mark(X2)) -> U12#(X1,X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    U12#(X1,mark(X2)) -> U12#(X1,X2) ->
    U12#(X1,mark(X2)) -> U12#(X1,X2)
    U12#(X1,mark(X2)) -> U12#(X1,X2) ->
    U12#(active(X1),X2) -> U12#(X1,X2)
    U12#(X1,mark(X2)) -> U12#(X1,X2) ->
    U12#(X1,active(X2)) -> U12#(X1,X2)
    U12#(X1,active(X2)) -> U12#(X1,X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    U12#(X1,active(X2)) -> U12#(X1,X2) ->
    U12#(X1,mark(X2)) -> U12#(X1,X2)
    U12#(X1,active(X2)) -> U12#(X1,X2) ->
    U12#(active(X1),X2) -> U12#(X1,X2)
    U12#(X1,active(X2)) -> U12#(X1,X2) ->
    U12#(X1,active(X2)) -> U12#(X1,X2)
    mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
    mark#(s(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
    mark#(s(X)) -> mark#(X) -> mark#(U12(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> length#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> active#(length(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(length(X)) -> length#(mark(X)) ->
    length#(mark(X)) -> length#(X)
    mark#(length(X)) -> length#(mark(X)) ->
    length#(active(X)) -> length#(X)
    mark#(length(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(length(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(length(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(length(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(length(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(length(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> mark#(X1)
    mark#(length(X)) -> mark#(X) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(length(X)) -> mark#(X) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(length(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
    mark#(length(X)) -> mark#(X) -> mark#(U12(X1,X2)) -> mark#(X1)
    mark#(length(X)) -> mark#(X) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(length(X)) -> mark#(X) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(length(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X)
    mark#(length(X)) -> mark#(X) ->
    mark#(length(X)) -> length#(mark(X))
    mark#(length(X)) -> mark#(X) ->
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(length(X)) -> mark#(X) ->
    mark#(nil()) -> active#(nil())
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(nil())) -> mark#(0())
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2) ->
    U12#(X1,mark(X2)) -> U12#(X1,X2)
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2) ->
    U12#(active(X1),X2) -> U12#(X1,X2)
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2) ->
    U12#(X1,active(X2)) -> U12#(X1,X2)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(zeros()) -> active#(zeros())
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> mark#(X1)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(U12(X1,X2)) -> mark#(X1)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> length#(mark(X))
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> length#(L)
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> s#(length(L))
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2) ->
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2) ->
    U11#(active(X1),X2) -> U11#(X1,X2)
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2) ->
    U11#(X1,active(X2)) -> U11#(X1,X2)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(zeros()) -> active#(zeros())
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> mark#(X1)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(U12(X1,X2)) -> mark#(X1)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> length#(mark(X))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> U12#(tt(),L)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(zeros()) -> active#(zeros())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> length#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    mark#(zeros()) -> active#(zeros()) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(zeros()) -> active#(zeros()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(length(nil())) -> mark#(0()) ->
    mark#(0()) -> active#(0())
    active#(length(cons(N,L))) -> U11#(tt(),L) ->
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> U11#(tt(),L) ->
    U11#(X1,active(X2)) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(U12(tt(),L)) -> length#(L) ->
    length#(mark(X)) -> length#(X)
    active#(U12(tt(),L)) -> length#(L) ->
    length#(active(X)) -> length#(X)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(s(X)) -> mark#(X)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(U11(tt(),L)) -> U12#(tt(),L) ->
    U12#(X1,mark(X2)) -> U12#(X1,X2)
    active#(U11(tt(),L)) -> U12#(tt(),L) ->
    U12#(X1,active(X2)) -> U12#(X1,X2)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(U12(X1,X2)) -> mark#(X1)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
   Restore Modifier:
    DPs:
     active#(zeros()) -> cons#(0(),zeros())
     active#(zeros()) -> mark#(cons(0(),zeros()))
     active#(U11(tt(),L)) -> U12#(tt(),L)
     active#(U11(tt(),L)) -> mark#(U12(tt(),L))
     active#(U12(tt(),L)) -> length#(L)
     active#(U12(tt(),L)) -> s#(length(L))
     active#(U12(tt(),L)) -> mark#(s(length(L)))
     active#(length(nil())) -> mark#(0())
     active#(length(cons(N,L))) -> U11#(tt(),L)
     active#(length(cons(N,L))) -> mark#(U11(tt(),L))
     mark#(zeros()) -> active#(zeros())
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     mark#(0()) -> active#(0())
     mark#(U11(X1,X2)) -> mark#(X1)
     mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
     mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
     mark#(tt()) -> active#(tt())
     mark#(U12(X1,X2)) -> mark#(X1)
     mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
     mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> s#(mark(X))
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(length(X)) -> mark#(X)
     mark#(length(X)) -> length#(mark(X))
     mark#(length(X)) -> active#(length(mark(X)))
     mark#(nil()) -> active#(nil())
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(X1,mark(X2)) -> cons#(X1,X2)
     cons#(active(X1),X2) -> cons#(X1,X2)
     cons#(X1,active(X2)) -> cons#(X1,X2)
     U11#(mark(X1),X2) -> U11#(X1,X2)
     U11#(X1,mark(X2)) -> U11#(X1,X2)
     U11#(active(X1),X2) -> U11#(X1,X2)
     U11#(X1,active(X2)) -> U11#(X1,X2)
     U12#(mark(X1),X2) -> U12#(X1,X2)
     U12#(X1,mark(X2)) -> U12#(X1,X2)
     U12#(active(X1),X2) -> U12#(X1,X2)
     U12#(X1,active(X2)) -> U12#(X1,X2)
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
     length#(mark(X)) -> length#(X)
     length#(active(X)) -> length#(X)
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(U11(tt(),L)) -> mark(U12(tt(),L))
     active(U12(tt(),L)) -> mark(s(length(L)))
     active(length(nil())) -> mark(0())
     active(length(cons(N,L))) -> mark(U11(tt(),L))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(0()) -> active(0())
     mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
     mark(tt()) -> active(tt())
     mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
     mark(s(X)) -> active(s(mark(X)))
     mark(length(X)) -> active(length(mark(X)))
     mark(nil()) -> active(nil())
     cons(mark(X1),X2) -> cons(X1,X2)
     cons(X1,mark(X2)) -> cons(X1,X2)
     cons(active(X1),X2) -> cons(X1,X2)
     cons(X1,active(X2)) -> cons(X1,X2)
     U11(mark(X1),X2) -> U11(X1,X2)
     U11(X1,mark(X2)) -> U11(X1,X2)
     U11(active(X1),X2) -> U11(X1,X2)
     U11(X1,active(X2)) -> U11(X1,X2)
     U12(mark(X1),X2) -> U12(X1,X2)
     U12(X1,mark(X2)) -> U12(X1,X2)
     U12(active(X1),X2) -> U12(X1,X2)
     U12(X1,active(X2)) -> U12(X1,X2)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     length(mark(X)) -> length(X)
     length(active(X)) -> length(X)
    SCC Processor:
     #sccs: 6
     #rules: 29
     #arcs: 196/2025
     DPs:
      mark#(s(X)) -> mark#(X)
      mark#(length(X)) -> active#(length(mark(X)))
      active#(length(cons(N,L))) -> mark#(U11(tt(),L))
      mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
      active#(U11(tt(),L)) -> mark#(U12(tt(),L))
      mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
      active#(U12(tt(),L)) -> mark#(s(length(L)))
      mark#(U12(X1,X2)) -> mark#(X1)
      mark#(length(X)) -> mark#(X)
      mark#(U11(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(zeros()) -> active#(zeros())
      active#(zeros()) -> mark#(cons(0(),zeros()))
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(U12(tt(),L))
      active(U12(tt(),L)) -> mark(s(length(L)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(tt(),L))
      mark(zeros()) -> active(zeros())
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(0()) -> active(0())
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(nil()) -> active(nil())
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U12(mark(X1),X2) -> U12(X1,X2)
      U12(X1,mark(X2)) -> U12(X1,X2)
      U12(active(X1),X2) -> U12(X1,X2)
      U12(X1,active(X2)) -> U12(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
     Open
     
     DPs:
      cons#(X1,active(X2)) -> cons#(X1,X2)
      cons#(active(X1),X2) -> cons#(X1,X2)
      cons#(X1,mark(X2)) -> cons#(X1,X2)
      cons#(mark(X1),X2) -> cons#(X1,X2)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(U12(tt(),L))
      active(U12(tt(),L)) -> mark(s(length(L)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(tt(),L))
      mark(zeros()) -> active(zeros())
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(0()) -> active(0())
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(nil()) -> active(nil())
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U12(mark(X1),X2) -> U12(X1,X2)
      U12(X1,mark(X2)) -> U12(X1,X2)
      U12(active(X1),X2) -> U12(X1,X2)
      U12(X1,active(X2)) -> U12(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
     Open
     
     DPs:
      U12#(mark(X1),X2) -> U12#(X1,X2)
      U12#(X1,active(X2)) -> U12#(X1,X2)
      U12#(active(X1),X2) -> U12#(X1,X2)
      U12#(X1,mark(X2)) -> U12#(X1,X2)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(U12(tt(),L))
      active(U12(tt(),L)) -> mark(s(length(L)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(tt(),L))
      mark(zeros()) -> active(zeros())
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(0()) -> active(0())
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(nil()) -> active(nil())
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U12(mark(X1),X2) -> U12(X1,X2)
      U12(X1,mark(X2)) -> U12(X1,X2)
      U12(active(X1),X2) -> U12(X1,X2)
      U12(X1,active(X2)) -> U12(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
     Open
     
     DPs:
      length#(mark(X)) -> length#(X)
      length#(active(X)) -> length#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(U12(tt(),L))
      active(U12(tt(),L)) -> mark(s(length(L)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(tt(),L))
      mark(zeros()) -> active(zeros())
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(0()) -> active(0())
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(nil()) -> active(nil())
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U12(mark(X1),X2) -> U12(X1,X2)
      U12(X1,mark(X2)) -> U12(X1,X2)
      U12(active(X1),X2) -> U12(X1,X2)
      U12(X1,active(X2)) -> U12(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
     Open
     
     DPs:
      s#(mark(X)) -> s#(X)
      s#(active(X)) -> s#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(U12(tt(),L))
      active(U12(tt(),L)) -> mark(s(length(L)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(tt(),L))
      mark(zeros()) -> active(zeros())
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(0()) -> active(0())
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(nil()) -> active(nil())
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U12(mark(X1),X2) -> U12(X1,X2)
      U12(X1,mark(X2)) -> U12(X1,X2)
      U12(active(X1),X2) -> U12(X1,X2)
      U12(X1,active(X2)) -> U12(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
     Open
     
     DPs:
      U11#(mark(X1),X2) -> U11#(X1,X2)
      U11#(X1,active(X2)) -> U11#(X1,X2)
      U11#(active(X1),X2) -> U11#(X1,X2)
      U11#(X1,mark(X2)) -> U11#(X1,X2)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(U12(tt(),L))
      active(U12(tt(),L)) -> mark(s(length(L)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(tt(),L))
      mark(zeros()) -> active(zeros())
      mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
      mark(0()) -> active(0())
      mark(U11(X1,X2)) -> active(U11(mark(X1),X2))
      mark(tt()) -> active(tt())
      mark(U12(X1,X2)) -> active(U12(mark(X1),X2))
      mark(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(nil()) -> active(nil())
      cons(mark(X1),X2) -> cons(X1,X2)
      cons(X1,mark(X2)) -> cons(X1,X2)
      cons(active(X1),X2) -> cons(X1,X2)
      cons(X1,active(X2)) -> cons(X1,X2)
      U11(mark(X1),X2) -> U11(X1,X2)
      U11(X1,mark(X2)) -> U11(X1,X2)
      U11(active(X1),X2) -> U11(X1,X2)
      U11(X1,active(X2)) -> U11(X1,X2)
      U12(mark(X1),X2) -> U12(X1,X2)
      U12(X1,mark(X2)) -> U12(X1,X2)
      U12(active(X1),X2) -> U12(X1,X2)
      U12(X1,active(X2)) -> U12(X1,X2)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
     Open