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)
  TDG 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#(X1,active(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,mark(X2)) -> U11#(X1,X2)
    U11#(mark(X1),X2) -> U11#(X1,X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(active(X1),X2) -> U11#(X1,X2) ->
    U11#(X1,active(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,mark(X2)) -> U11#(X1,X2)
    U11#(active(X1),X2) -> U11#(X1,X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(X1,mark(X2)) -> U11#(X1,X2) ->
    U11#(X1,active(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,mark(X2)) -> U11#(X1,X2)
    U11#(X1,mark(X2)) -> U11#(X1,X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(X1,active(X2)) -> U11#(X1,X2) ->
    U11#(X1,active(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,mark(X2)) -> U11#(X1,X2)
    U11#(X1,active(X2)) -> U11#(X1,X2) -> U11#(mark(X1),X2) -> U11#(X1,X2)
    s#(mark(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(active(X)) -> s#(X)
    s#(active(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    length#(mark(X)) -> length#(X) ->
    length#(active(X)) -> length#(X)
    length#(mark(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    length#(active(X)) -> length#(X) ->
    length#(active(X)) -> length#(X)
    length#(active(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    U12#(mark(X1),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)
    U12#(mark(X1),X2) -> U12#(X1,X2) ->
    U12#(X1,mark(X2)) -> U12#(X1,X2)
    U12#(mark(X1),X2) -> U12#(X1,X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    U12#(active(X1),X2) -> U12#(X1,X2) ->
    U12#(X1,active(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,mark(X2)) -> U12#(X1,X2)
    U12#(active(X1),X2) -> U12#(X1,X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    U12#(X1,mark(X2)) -> U12#(X1,X2) ->
    U12#(X1,active(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,mark(X2)) -> U12#(X1,X2)
    U12#(X1,mark(X2)) -> U12#(X1,X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    U12#(X1,active(X2)) -> U12#(X1,X2) ->
    U12#(X1,active(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,mark(X2)) -> U12#(X1,X2)
    U12#(X1,active(X2)) -> U12#(X1,X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(nil()) -> active#(nil()) ->
    active#(length(nil())) -> mark#(0())
    mark#(nil()) -> active#(nil()) ->
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    mark#(nil()) -> active#(nil()) ->
    active#(U12(tt(),L)) -> s#(length(L))
    mark#(nil()) -> active#(nil()) ->
    active#(U12(tt(),L)) -> length#(L)
    mark#(nil()) -> active#(nil()) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    mark#(nil()) -> active#(nil()) ->
    active#(U11(tt(),L)) -> U12#(tt(),L)
    mark#(nil()) -> active#(nil()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(nil()) -> active#(nil()) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(s(X)) -> s#(mark(X)) -> s#(active(X)) -> s#(X)
    mark#(s(X)) -> s#(mark(X)) -> s#(mark(X)) -> s#(X)
    mark#(s(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> active#(length(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> length#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> mark#(X) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) -> mark#(U12(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
    mark#(s(X)) -> mark#(X) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(s(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(s(X)) -> mark#(X) -> mark#(zeros()) -> active#(zeros())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(nil())) -> mark#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U12(tt(),L)) -> s#(length(L))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U12(tt(),L)) -> length#(L)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U11(tt(),L)) -> U12#(tt(),L)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(length(X)) -> length#(mark(X)) ->
    length#(active(X)) -> length#(X)
    mark#(length(X)) -> length#(mark(X)) ->
    length#(mark(X)) -> length#(X)
    mark#(length(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
    mark#(length(X)) -> mark#(X) ->
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(length(X)) -> mark#(X) ->
    mark#(length(X)) -> length#(mark(X))
    mark#(length(X)) -> mark#(X) -> mark#(length(X)) -> mark#(X)
    mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> active#(s(mark(X)))
    mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    mark#(length(X)) -> mark#(X) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(length(X)) -> mark#(X) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(length(X)) -> mark#(X) -> mark#(U12(X1,X2)) -> mark#(X1)
    mark#(length(X)) -> mark#(X) -> mark#(tt()) -> active#(tt())
    mark#(length(X)) -> mark#(X) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(length(X)) -> mark#(X) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(length(X)) -> mark#(X) -> mark#(U11(X1,X2)) -> mark#(X1)
    mark#(length(X)) -> mark#(X) -> mark#(0()) -> active#(0())
    mark#(length(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(length(X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(length(X)) -> mark#(X) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(length(X)) -> mark#(X) ->
    mark#(zeros()) -> active#(zeros())
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(nil())) -> mark#(0())
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(U12(tt(),L)) -> s#(length(L))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(U12(tt(),L)) -> length#(L)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(U11(tt(),L)) -> U12#(tt(),L)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2) ->
    U12#(X1,active(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,mark(X2)) -> U12#(X1,X2)
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil())
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> length#(mark(X))
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(U12(X1,X2)) -> mark#(X1)
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> mark#(X1)
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(U12(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(U12(X1,X2)) -> mark#(X1) ->
    mark#(zeros()) -> active#(zeros())
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(length(nil())) -> mark#(0())
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> mark#(s(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)) -> length#(L)
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> U12#(tt(),L)
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2) ->
    U11#(X1,active(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,mark(X2)) -> U11#(X1,X2)
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil())
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> length#(mark(X))
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(U12(X1,X2)) -> mark#(X1)
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(U11(X1,X2)) -> mark#(X1)
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(zeros()) -> active#(zeros())
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(length(nil())) -> mark#(0())
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> s#(length(L))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> length#(L)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    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#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(tt()) -> active#(tt()) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(tt()) -> active#(tt()) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(tt()) -> active#(tt()) ->
    active#(length(nil())) -> mark#(0())
    mark#(tt()) -> active#(tt()) ->
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    mark#(tt()) -> active#(tt()) ->
    active#(U12(tt(),L)) -> s#(length(L))
    mark#(tt()) -> active#(tt()) -> active#(U12(tt(),L)) -> length#(L)
    mark#(tt()) -> active#(tt()) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    mark#(tt()) -> active#(tt()) ->
    active#(U11(tt(),L)) -> U12#(tt(),L)
    mark#(tt()) -> active#(tt()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(tt()) -> active#(tt()) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(nil()) -> active#(nil())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> length#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U12(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(zeros()) -> active#(zeros())
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(X1,active(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,mark(X2)) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(nil())) -> mark#(0())
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> s#(length(L))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(U12(tt(),L)) -> length#(L)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> U12#(tt(),L)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(0()) -> active#(0()) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(0()) -> active#(0()) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(0()) -> active#(0()) -> active#(length(nil())) -> mark#(0())
    mark#(0()) -> active#(0()) ->
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    mark#(0()) -> active#(0()) -> active#(U12(tt(),L)) -> s#(length(L))
    mark#(0()) -> active#(0()) -> active#(U12(tt(),L)) -> length#(L)
    mark#(0()) -> active#(0()) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    mark#(0()) -> active#(0()) -> active#(U11(tt(),L)) -> U12#(tt(),L)
    mark#(0()) -> active#(0()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(0()) -> active#(0()) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(cons(N,L))) -> mark#(U11(tt(),L))
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(cons(N,L))) -> U11#(tt(),L)
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(nil())) -> mark#(0())
    mark#(zeros()) -> active#(zeros()) ->
    active#(U12(tt(),L)) -> mark#(s(length(L)))
    mark#(zeros()) -> active#(zeros()) ->
    active#(U12(tt(),L)) -> s#(length(L))
    mark#(zeros()) -> active#(zeros()) ->
    active#(U12(tt(),L)) -> length#(L)
    mark#(zeros()) -> active#(zeros()) ->
    active#(U11(tt(),L)) -> mark#(U12(tt(),L))
    mark#(zeros()) -> active#(zeros()) ->
    active#(U11(tt(),L)) -> U12#(tt(),L)
    mark#(zeros()) -> active#(zeros()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(zeros()) -> active#(zeros()) ->
    active#(zeros()) -> cons#(0(),zeros())
    cons#(mark(X1),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)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(X1,active(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,mark(X2)) -> cons#(X1,X2)
    cons#(active(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(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,mark(X2)) -> cons#(X1,X2)
    cons#(X1,mark(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(X1,active(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,mark(X2)) -> cons#(X1,X2)
    cons#(X1,active(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(length(nil())) -> mark#(0()) ->
    mark#(nil()) -> active#(nil())
    active#(length(nil())) -> mark#(0()) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(length(nil())) -> mark#(0()) ->
    mark#(length(X)) -> length#(mark(X))
    active#(length(nil())) -> mark#(0()) ->
    mark#(length(X)) -> mark#(X)
    active#(length(nil())) -> mark#(0()) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(length(nil())) -> mark#(0()) ->
    mark#(s(X)) -> s#(mark(X))
    active#(length(nil())) -> mark#(0()) ->
    mark#(s(X)) -> mark#(X)
    active#(length(nil())) -> mark#(0()) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    active#(length(nil())) -> mark#(0()) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    active#(length(nil())) -> mark#(0()) ->
    mark#(U12(X1,X2)) -> mark#(X1)
    active#(length(nil())) -> mark#(0()) ->
    mark#(tt()) -> active#(tt())
    active#(length(nil())) -> mark#(0()) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(length(nil())) -> mark#(0()) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(length(nil())) -> mark#(0()) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(length(nil())) -> mark#(0()) ->
    mark#(0()) -> active#(0())
    active#(length(nil())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(length(nil())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(length(nil())) -> mark#(0()) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(length(nil())) -> mark#(0()) ->
    mark#(zeros()) -> active#(zeros())
    active#(length(cons(N,L))) -> U11#(tt(),L) ->
    U11#(X1,active(X2)) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> U11#(tt(),L) ->
    U11#(active(X1),X2) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> U11#(tt(),L) ->
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> U11#(tt(),L) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(nil()) -> active#(nil())
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(length(X)) -> length#(mark(X))
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(length(X)) -> mark#(X)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(s(X)) -> mark#(X)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(U12(X1,X2)) -> mark#(X1)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(tt()) -> active#(tt())
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    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)) -> mark#(X1)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(0()) -> active#(0())
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
    mark#(zeros()) -> active#(zeros())
    active#(U12(tt(),L)) -> s#(length(L)) ->
    s#(active(X)) -> s#(X)
    active#(U12(tt(),L)) -> s#(length(L)) -> s#(mark(X)) -> s#(X)
    active#(U12(tt(),L)) -> length#(L) ->
    length#(active(X)) -> length#(X)
    active#(U12(tt(),L)) -> length#(L) ->
    length#(mark(X)) -> length#(X)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(nil()) -> active#(nil())
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(length(X)) -> length#(mark(X))
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(length(X)) -> mark#(X)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(s(X)) -> active#(s(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)) -> mark#(X)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(U12(X1,X2)) -> mark#(X1)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(tt()) -> active#(tt())
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(0()) -> active#(0())
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(U12(tt(),L)) -> mark#(s(length(L))) ->
    mark#(zeros()) -> active#(zeros())
    active#(U11(tt(),L)) -> U12#(tt(),L) ->
    U12#(X1,active(X2)) -> U12#(X1,X2)
    active#(U11(tt(),L)) -> U12#(tt(),L) ->
    U12#(active(X1),X2) -> U12#(X1,X2)
    active#(U11(tt(),L)) -> U12#(tt(),L) ->
    U12#(X1,mark(X2)) -> U12#(X1,X2)
    active#(U11(tt(),L)) -> U12#(tt(),L) ->
    U12#(mark(X1),X2) -> U12#(X1,X2)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(nil()) -> active#(nil())
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(length(X)) -> length#(mark(X))
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(length(X)) -> mark#(X)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(s(X)) -> mark#(X)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    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)) -> mark#(X1)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(tt()) -> active#(tt())
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(0()) -> active#(0())
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
    mark#(zeros()) -> active#(zeros())
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(nil()) -> active#(nil())
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(length(X)) -> length#(mark(X))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(length(X)) -> mark#(X)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(s(X)) -> s#(mark(X))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(s(X)) -> mark#(X)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(U12(X1,X2)) -> U12#(mark(X1),X2)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(U12(X1,X2)) -> mark#(X1)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(tt()) -> active#(tt())
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(0()) -> active#(0())
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(zeros()) -> active#(zeros())
    active#(zeros()) -> cons#(0(),zeros()) ->
    cons#(X1,active(X2)) -> cons#(X1,X2)
    active#(zeros()) -> cons#(0(),zeros()) ->
    cons#(active(X1),X2) -> cons#(X1,X2)
    active#(zeros()) -> cons#(0(),zeros()) ->
    cons#(X1,mark(X2)) -> cons#(X1,X2)
    active#(zeros()) -> cons#(0(),zeros()) -> cons#(mark(X1),X2) -> cons#(X1,X2)
   SCC Processor:
    #sccs: 6
    #rules: 35
    #arcs: 368/2025
    DPs:
     mark#(nil()) -> active#(nil())
     active#(zeros()) -> mark#(cons(0(),zeros()))
     mark#(zeros()) -> active#(zeros())
     active#(U11(tt(),L)) -> mark#(U12(tt(),L))
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     active#(U12(tt(),L)) -> mark#(s(length(L)))
     mark#(0()) -> active#(0())
     active#(length(nil())) -> mark#(0())
     mark#(U11(X1,X2)) -> mark#(X1)
     mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
     active#(length(cons(N,L))) -> mark#(U11(tt(),L))
     mark#(tt()) -> active#(tt())
     mark#(U12(X1,X2)) -> mark#(X1)
     mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
     mark#(s(X)) -> mark#(X)
     mark#(s(X)) -> active#(s(mark(X)))
     mark#(length(X)) -> mark#(X)
     mark#(length(X)) -> active#(length(mark(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)
    EDG Processor:
     DPs:
      mark#(nil()) -> active#(nil())
      active#(zeros()) -> mark#(cons(0(),zeros()))
      mark#(zeros()) -> active#(zeros())
      active#(U11(tt(),L)) -> mark#(U12(tt(),L))
      mark#(cons(X1,X2)) -> mark#(X1)
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(U12(tt(),L)) -> mark#(s(length(L)))
      mark#(0()) -> active#(0())
      active#(length(nil())) -> mark#(0())
      mark#(U11(X1,X2)) -> mark#(X1)
      mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
      active#(length(cons(N,L))) -> mark#(U11(tt(),L))
      mark#(tt()) -> active#(tt())
      mark#(U12(X1,X2)) -> mark#(X1)
      mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
      mark#(s(X)) -> mark#(X)
      mark#(s(X)) -> active#(s(mark(X)))
      mark#(length(X)) -> mark#(X)
      mark#(length(X)) -> active#(length(mark(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:
      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)) -> 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)) -> 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)) -> active#(U12(mark(X1),X2))
      mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> 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)) -> active#(length(mark(X)))
      mark#(s(X)) -> mark#(X) -> mark#(nil()) -> active#(nil())
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(U11(tt(),L)) -> mark#(U12(tt(),L))
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(U12(tt(),L)) -> mark#(s(length(L)))
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(length(nil())) -> mark#(0())
      mark#(s(X)) -> active#(s(mark(X))) ->
      active#(length(cons(N,L))) -> mark#(U11(tt(),L))
      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)) -> 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)) -> 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)) -> active#(U12(mark(X1),X2))
      mark#(length(X)) -> mark#(X) -> mark#(s(X)) -> 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)) -> active#(length(mark(X)))
      mark#(length(X)) -> mark#(X) ->
      mark#(nil()) -> active#(nil())
      mark#(length(X)) -> active#(length(mark(X))) ->
      active#(U11(tt(),L)) -> mark#(U12(tt(),L))
      mark#(length(X)) -> active#(length(mark(X))) ->
      active#(U12(tt(),L)) -> mark#(s(length(L)))
      mark#(length(X)) -> active#(length(mark(X))) ->
      active#(length(nil())) -> mark#(0())
      mark#(length(X)) -> active#(length(mark(X))) ->
      active#(length(cons(N,L))) -> mark#(U11(tt(),L))
      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)) -> 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)) -> 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)) -> 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)) -> active#(s(mark(X)))
      mark#(U12(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> 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#(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)) -> active#(U12(mark(X1),X2)) ->
      active#(length(nil())) -> mark#(0())
      mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2)) ->
      active#(length(cons(N,L))) -> mark#(U11(tt(),L))
      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)) -> 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)) -> 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)) -> 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)) -> active#(s(mark(X)))
      mark#(U11(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> 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)) -> mark#(U12(tt(),L))
      mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
      active#(U12(tt(),L)) -> mark#(s(length(L)))
      mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
      active#(length(nil())) -> mark#(0())
      mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
      active#(length(cons(N,L))) -> mark#(U11(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)) -> 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)) -> 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)) -> 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)) -> active#(s(mark(X)))
      mark#(cons(X1,X2)) -> mark#(X1) ->
      mark#(length(X)) -> 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)) -> active#(cons(mark(X1),X2)) ->
      active#(U11(tt(),L)) -> mark#(U12(tt(),L))
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(U12(tt(),L)) -> mark#(s(length(L)))
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(length(nil())) -> mark#(0())
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
      active#(length(cons(N,L))) -> mark#(U11(tt(),L))
      mark#(zeros()) -> active#(zeros()) ->
      active#(zeros()) -> mark#(cons(0(),zeros()))
      active#(length(nil())) -> mark#(0()) ->
      mark#(0()) -> active#(0())
      active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(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)) -> active#(U11(mark(X1),X2))
      active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
      mark#(U12(X1,X2)) -> mark#(X1)
      active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
      mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
      active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
      mark#(s(X)) -> mark#(X)
      active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
      mark#(length(X)) -> mark#(X)
      active#(length(cons(N,L))) -> mark#(U11(tt(),L)) ->
      mark#(length(X)) -> active#(length(mark(X)))
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(U11(X1,X2)) -> mark#(X1)
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(U12(X1,X2)) -> mark#(X1)
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(s(X)) -> mark#(X)
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(length(X)) -> mark#(X)
      active#(U12(tt(),L)) -> mark#(s(length(L))) ->
      mark#(length(X)) -> active#(length(mark(X)))
      active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
      active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
      mark#(U11(X1,X2)) -> mark#(X1)
      active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
      mark#(U11(X1,X2)) -> active#(U11(mark(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)) -> active#(U12(mark(X1),X2))
      active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
      mark#(s(X)) -> mark#(X)
      active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
      mark#(s(X)) -> active#(s(mark(X)))
      active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
      mark#(length(X)) -> mark#(X)
      active#(U11(tt(),L)) -> mark#(U12(tt(),L)) ->
      mark#(length(X)) -> active#(length(mark(X)))
      active#(zeros()) -> mark#(cons(0(),zeros())) ->
      mark#(cons(X1,X2)) -> mark#(X1)
      active#(zeros()) -> mark#(cons(0(),zeros())) ->
      mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     SCC Processor:
      #sccs: 1
      #rules: 15
      #arcs: 124/361
      DPs:
       mark#(s(X)) -> mark#(X)
       mark#(length(X)) -> active#(length(mark(X)))
       active#(length(cons(N,L))) -> mark#(U11(tt(),L))
       mark#(length(X)) -> mark#(X)
       mark#(s(X)) -> active#(s(mark(X)))
       active#(U12(tt(),L)) -> mark#(s(length(L)))
       mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
       active#(U11(tt(),L)) -> mark#(U12(tt(),L))
       mark#(U12(X1,X2)) -> mark#(X1)
       mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
       mark#(U11(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       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)
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [mark#](x0) = x0 + 0,
        
        [active#](x0) = x0 + 0,
        
        [nil] = 5,
        
        [s](x0) = x0 + 0,
        
        [length](x0) = x0 + 4,
        
        [U12](x0, x1) = x0 + x1 + 4,
        
        [U11](x0, x1) = 1x0 + x1 + 4,
        
        [tt] = 0,
        
        [mark](x0) = x0 + 0,
        
        [cons](x0, x1) = x0 + x1 + 0,
        
        [0] = 0,
        
        [active](x0) = x0 + 0,
        
        [zeros] = 2
       orientation:
        mark#(s(X)) = X + 0 >= X + 0 = mark#(X)
        
        mark#(length(X)) = X + 4 >= X + 4 = active#(length(mark(X)))
        
        active#(length(cons(N,L))) = L + N + 4 >= L + 4 = mark#(U11(tt(),L))
        
        mark#(length(X)) = X + 4 >= X + 0 = mark#(X)
        
        mark#(s(X)) = X + 0 >= X + 0 = active#(s(mark(X)))
        
        active#(U12(tt(),L)) = L + 4 >= L + 4 = mark#(s(length(L)))
        
        mark#(U12(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = active#(U12(mark(X1),X2))
        
        active#(U11(tt(),L)) = L + 4 >= L + 4 = mark#(U12(tt(),L))
        
        mark#(U12(X1,X2)) = X1 + X2 + 4 >= X1 + 0 = mark#(X1)
        
        mark#(U11(X1,X2)) = 1X1 + X2 + 4 >= 1X1 + X2 + 4 = active#(U11(mark(X1),X2))
        
        mark#(U11(X1,X2)) = 1X1 + X2 + 4 >= X1 + 0 = mark#(X1)
        
        mark#(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active#(cons(mark(X1),X2))
        
        mark#(cons(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = mark#(X1)
        
        mark#(zeros()) = 2 >= 2 = active#(zeros())
        
        active#(zeros()) = 2 >= 2 = mark#(cons(0(),zeros()))
        
        active(zeros()) = 2 >= 2 = mark(cons(0(),zeros()))
        
        active(U11(tt(),L)) = L + 4 >= L + 4 = mark(U12(tt(),L))
        
        active(U12(tt(),L)) = L + 4 >= L + 4 = mark(s(length(L)))
        
        active(length(nil())) = 5 >= 0 = mark(0())
        
        active(length(cons(N,L))) = L + N + 4 >= L + 4 = mark(U11(tt(),L))
        
        mark(zeros()) = 2 >= 2 = active(zeros())
        
        mark(cons(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active(cons(mark(X1),X2))
        
        mark(0()) = 0 >= 0 = active(0())
        
        mark(U11(X1,X2)) = 1X1 + X2 + 4 >= 1X1 + X2 + 4 = active(U11(mark(X1),X2))
        
        mark(tt()) = 0 >= 0 = active(tt())
        
        mark(U12(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = active(U12(mark(X1),X2))
        
        mark(s(X)) = X + 0 >= X + 0 = active(s(mark(X)))
        
        mark(length(X)) = X + 4 >= X + 4 = active(length(mark(X)))
        
        mark(nil()) = 5 >= 5 = active(nil())
        
        cons(mark(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
        
        cons(X1,mark(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
        
        cons(active(X1),X2) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
        
        cons(X1,active(X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = cons(X1,X2)
        
        U11(mark(X1),X2) = 1X1 + X2 + 4 >= 1X1 + X2 + 4 = U11(X1,X2)
        
        U11(X1,mark(X2)) = 1X1 + X2 + 4 >= 1X1 + X2 + 4 = U11(X1,X2)
        
        U11(active(X1),X2) = 1X1 + X2 + 4 >= 1X1 + X2 + 4 = U11(X1,X2)
        
        U11(X1,active(X2)) = 1X1 + X2 + 4 >= 1X1 + X2 + 4 = U11(X1,X2)
        
        U12(mark(X1),X2) = X1 + X2 + 4 >= X1 + X2 + 4 = U12(X1,X2)
        
        U12(X1,mark(X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = U12(X1,X2)
        
        U12(active(X1),X2) = X1 + X2 + 4 >= X1 + X2 + 4 = U12(X1,X2)
        
        U12(X1,active(X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = U12(X1,X2)
        
        s(mark(X)) = X + 0 >= X + 0 = s(X)
        
        s(active(X)) = X + 0 >= X + 0 = s(X)
        
        length(mark(X)) = X + 4 >= X + 4 = length(X)
        
        length(active(X)) = X + 4 >= X + 4 = length(X)
       problem:
        DPs:
         mark#(s(X)) -> mark#(X)
         mark#(length(X)) -> active#(length(mark(X)))
         active#(length(cons(N,L))) -> mark#(U11(tt(),L))
         mark#(length(X)) -> mark#(X)
         mark#(s(X)) -> active#(s(mark(X)))
         active#(U12(tt(),L)) -> mark#(s(length(L)))
         mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
         active#(U11(tt(),L)) -> mark#(U12(tt(),L))
         mark#(U12(X1,X2)) -> mark#(X1)
         mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
         mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
         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)
       Arctic Interpretation Processor:
        dimension: 1
        interpretation:
         [mark#](x0) = x0 + 4,
         
         [active#](x0) = x0 + 4,
         
         [nil] = 3,
         
         [s](x0) = x0 + 4,
         
         [length](x0) = 2x0 + 6,
         
         [U12](x0, x1) = 2x0 + 2x1 + 6,
         
         [U11](x0, x1) = x0 + 2x1 + 6,
         
         [tt] = 2,
         
         [mark](x0) = x0 + 4,
         
         [cons](x0, x1) = x0 + x1 + 0,
         
         [0] = 3,
         
         [active](x0) = x0 + 4,
         
         [zeros] = 0
        orientation:
         mark#(s(X)) = X + 4 >= X + 4 = mark#(X)
         
         mark#(length(X)) = 2X + 6 >= 2X + 6 = active#(length(mark(X)))
         
         active#(length(cons(N,L))) = 2L + 2N + 6 >= 2L + 6 = mark#(U11(tt(),L))
         
         mark#(length(X)) = 2X + 6 >= X + 4 = mark#(X)
         
         mark#(s(X)) = X + 4 >= X + 4 = active#(s(mark(X)))
         
         active#(U12(tt(),L)) = 2L + 6 >= 2L + 6 = mark#(s(length(L)))
         
         mark#(U12(X1,X2)) = 2X1 + 2X2 + 6 >= 2X1 + 2X2 + 6 = active#(U12(mark(X1),X2))
         
         active#(U11(tt(),L)) = 2L + 6 >= 2L + 6 = mark#(U12(tt(),L))
         
         mark#(U12(X1,X2)) = 2X1 + 2X2 + 6 >= X1 + 4 = mark#(X1)
         
         mark#(U11(X1,X2)) = X1 + 2X2 + 6 >= X1 + 2X2 + 6 = active#(U11(mark(X1),X2))
         
         mark#(cons(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = active#(cons(mark(X1),X2))
         
         mark#(cons(X1,X2)) = X1 + X2 + 4 >= X1 + 4 = mark#(X1)
         
         mark#(zeros()) = 4 >= 4 = active#(zeros())
         
         active#(zeros()) = 4 >= 4 = mark#(cons(0(),zeros()))
         
         active(zeros()) = 4 >= 4 = mark(cons(0(),zeros()))
         
         active(U11(tt(),L)) = 2L + 6 >= 2L + 6 = mark(U12(tt(),L))
         
         active(U12(tt(),L)) = 2L + 6 >= 2L + 6 = mark(s(length(L)))
         
         active(length(nil())) = 6 >= 4 = mark(0())
         
         active(length(cons(N,L))) = 2L + 2N + 6 >= 2L + 6 = mark(U11(tt(),L))
         
         mark(zeros()) = 4 >= 4 = active(zeros())
         
         mark(cons(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = active(cons(mark(X1),X2))
         
         mark(0()) = 4 >= 4 = active(0())
         
         mark(U11(X1,X2)) = X1 + 2X2 + 6 >= X1 + 2X2 + 6 = active(U11(mark(X1),X2))
         
         mark(tt()) = 4 >= 4 = active(tt())
         
         mark(U12(X1,X2)) = 2X1 + 2X2 + 6 >= 2X1 + 2X2 + 6 = active(U12(mark(X1),X2))
         
         mark(s(X)) = X + 4 >= X + 4 = active(s(mark(X)))
         
         mark(length(X)) = 2X + 6 >= 2X + 6 = active(length(mark(X)))
         
         mark(nil()) = 4 >= 4 = active(nil())
         
         cons(mark(X1),X2) = X1 + X2 + 4 >= X1 + X2 + 0 = cons(X1,X2)
         
         cons(X1,mark(X2)) = X1 + X2 + 4 >= X1 + X2 + 0 = cons(X1,X2)
         
         cons(active(X1),X2) = X1 + X2 + 4 >= X1 + X2 + 0 = cons(X1,X2)
         
         cons(X1,active(X2)) = X1 + X2 + 4 >= X1 + X2 + 0 = cons(X1,X2)
         
         U11(mark(X1),X2) = X1 + 2X2 + 6 >= X1 + 2X2 + 6 = U11(X1,X2)
         
         U11(X1,mark(X2)) = X1 + 2X2 + 6 >= X1 + 2X2 + 6 = U11(X1,X2)
         
         U11(active(X1),X2) = X1 + 2X2 + 6 >= X1 + 2X2 + 6 = U11(X1,X2)
         
         U11(X1,active(X2)) = X1 + 2X2 + 6 >= X1 + 2X2 + 6 = U11(X1,X2)
         
         U12(mark(X1),X2) = 2X1 + 2X2 + 6 >= 2X1 + 2X2 + 6 = U12(X1,X2)
         
         U12(X1,mark(X2)) = 2X1 + 2X2 + 6 >= 2X1 + 2X2 + 6 = U12(X1,X2)
         
         U12(active(X1),X2) = 2X1 + 2X2 + 6 >= 2X1 + 2X2 + 6 = U12(X1,X2)
         
         U12(X1,active(X2)) = 2X1 + 2X2 + 6 >= 2X1 + 2X2 + 6 = U12(X1,X2)
         
         s(mark(X)) = X + 4 >= X + 4 = s(X)
         
         s(active(X)) = X + 4 >= X + 4 = s(X)
         
         length(mark(X)) = 2X + 6 >= 2X + 6 = length(X)
         
         length(active(X)) = 2X + 6 >= 2X + 6 = length(X)
        problem:
         DPs:
          mark#(s(X)) -> mark#(X)
          mark#(length(X)) -> active#(length(mark(X)))
          active#(length(cons(N,L))) -> mark#(U11(tt(),L))
          mark#(s(X)) -> active#(s(mark(X)))
          active#(U12(tt(),L)) -> mark#(s(length(L)))
          mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
          active#(U11(tt(),L)) -> mark#(U12(tt(),L))
          mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
          mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
          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)
        Arctic Interpretation Processor:
         dimension: 1
         interpretation:
          [mark#](x0) = x0 + 0,
          
          [active#](x0) = x0 + 0,
          
          [nil] = 4,
          
          [s](x0) = x0 + 0,
          
          [length](x0) = x0 + 0,
          
          [U12](x0, x1) = x0 + x1,
          
          [U11](x0, x1) = x0 + x1 + 4,
          
          [tt] = 0,
          
          [mark](x0) = x0 + 0,
          
          [cons](x0, x1) = 4x0 + x1 + 5,
          
          [0] = 3,
          
          [active](x0) = x0 + 0,
          
          [zeros] = 7
         orientation:
          mark#(s(X)) = X + 0 >= X + 0 = mark#(X)
          
          mark#(length(X)) = X + 0 >= X + 0 = active#(length(mark(X)))
          
          active#(length(cons(N,L))) = L + 4N + 5 >= L + 4 = mark#(U11(tt(),L))
          
          mark#(s(X)) = X + 0 >= X + 0 = active#(s(mark(X)))
          
          active#(U12(tt(),L)) = L + 0 >= L + 0 = mark#(s(length(L)))
          
          mark#(U12(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active#(U12(mark(X1),X2))
          
          active#(U11(tt(),L)) = L + 4 >= L + 0 = mark#(U12(tt(),L))
          
          mark#(U11(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = active#(U11(mark(X1),X2))
          
          mark#(cons(X1,X2)) = 4X1 + X2 + 5 >= 4X1 + X2 + 5 = active#(cons(mark(X1),X2))
          
          mark#(cons(X1,X2)) = 4X1 + X2 + 5 >= X1 + 0 = mark#(X1)
          
          mark#(zeros()) = 7 >= 7 = active#(zeros())
          
          active#(zeros()) = 7 >= 7 = mark#(cons(0(),zeros()))
          
          active(zeros()) = 7 >= 7 = mark(cons(0(),zeros()))
          
          active(U11(tt(),L)) = L + 4 >= L + 0 = mark(U12(tt(),L))
          
          active(U12(tt(),L)) = L + 0 >= L + 0 = mark(s(length(L)))
          
          active(length(nil())) = 4 >= 3 = mark(0())
          
          active(length(cons(N,L))) = L + 4N + 5 >= L + 4 = mark(U11(tt(),L))
          
          mark(zeros()) = 7 >= 7 = active(zeros())
          
          mark(cons(X1,X2)) = 4X1 + X2 + 5 >= 4X1 + X2 + 5 = active(cons(mark(X1),X2))
          
          mark(0()) = 3 >= 3 = active(0())
          
          mark(U11(X1,X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = active(U11(mark(X1),X2))
          
          mark(tt()) = 0 >= 0 = active(tt())
          
          mark(U12(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = active(U12(mark(X1),X2))
          
          mark(s(X)) = X + 0 >= X + 0 = active(s(mark(X)))
          
          mark(length(X)) = X + 0 >= X + 0 = active(length(mark(X)))
          
          mark(nil()) = 4 >= 4 = active(nil())
          
          cons(mark(X1),X2) = 4X1 + X2 + 5 >= 4X1 + X2 + 5 = cons(X1,X2)
          
          cons(X1,mark(X2)) = 4X1 + X2 + 5 >= 4X1 + X2 + 5 = cons(X1,X2)
          
          cons(active(X1),X2) = 4X1 + X2 + 5 >= 4X1 + X2 + 5 = cons(X1,X2)
          
          cons(X1,active(X2)) = 4X1 + X2 + 5 >= 4X1 + X2 + 5 = cons(X1,X2)
          
          U11(mark(X1),X2) = X1 + X2 + 4 >= X1 + X2 + 4 = U11(X1,X2)
          
          U11(X1,mark(X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = U11(X1,X2)
          
          U11(active(X1),X2) = X1 + X2 + 4 >= X1 + X2 + 4 = U11(X1,X2)
          
          U11(X1,active(X2)) = X1 + X2 + 4 >= X1 + X2 + 4 = U11(X1,X2)
          
          U12(mark(X1),X2) = X1 + X2 + 0 >= X1 + X2 = U12(X1,X2)
          
          U12(X1,mark(X2)) = X1 + X2 + 0 >= X1 + X2 = U12(X1,X2)
          
          U12(active(X1),X2) = X1 + X2 + 0 >= X1 + X2 = U12(X1,X2)
          
          U12(X1,active(X2)) = X1 + X2 + 0 >= X1 + X2 = U12(X1,X2)
          
          s(mark(X)) = X + 0 >= X + 0 = s(X)
          
          s(active(X)) = X + 0 >= X + 0 = s(X)
          
          length(mark(X)) = X + 0 >= X + 0 = length(X)
          
          length(active(X)) = X + 0 >= X + 0 = length(X)
         problem:
          DPs:
           mark#(s(X)) -> mark#(X)
           mark#(length(X)) -> active#(length(mark(X)))
           active#(length(cons(N,L))) -> mark#(U11(tt(),L))
           mark#(s(X)) -> active#(s(mark(X)))
           active#(U12(tt(),L)) -> mark#(s(length(L)))
           mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
           active#(U11(tt(),L)) -> mark#(U12(tt(),L))
           mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
           mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
           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)
         Arctic Interpretation Processor:
          dimension: 1
          interpretation:
           [mark#](x0) = 1,
           
           [active#](x0) = x0 + 0,
           
           [nil] = 1,
           
           [s](x0) = 0,
           
           [length](x0) = 1,
           
           [U12](x0, x1) = 1,
           
           [U11](x0, x1) = 1,
           
           [tt] = 0,
           
           [mark](x0) = 0,
           
           [cons](x0, x1) = 0,
           
           [0] = 0,
           
           [active](x0) = 0,
           
           [zeros] = 1
          orientation:
           mark#(s(X)) = 1 >= 1 = mark#(X)
           
           mark#(length(X)) = 1 >= 1 = active#(length(mark(X)))
           
           active#(length(cons(N,L))) = 1 >= 1 = mark#(U11(tt(),L))
           
           mark#(s(X)) = 1 >= 0 = active#(s(mark(X)))
           
           active#(U12(tt(),L)) = 1 >= 1 = mark#(s(length(L)))
           
           mark#(U12(X1,X2)) = 1 >= 1 = active#(U12(mark(X1),X2))
           
           active#(U11(tt(),L)) = 1 >= 1 = mark#(U12(tt(),L))
           
           mark#(U11(X1,X2)) = 1 >= 1 = active#(U11(mark(X1),X2))
           
           mark#(cons(X1,X2)) = 1 >= 0 = active#(cons(mark(X1),X2))
           
           mark#(zeros()) = 1 >= 1 = active#(zeros())
           
           active#(zeros()) = 1 >= 1 = mark#(cons(0(),zeros()))
           
           active(zeros()) = 0 >= 0 = mark(cons(0(),zeros()))
           
           active(U11(tt(),L)) = 0 >= 0 = mark(U12(tt(),L))
           
           active(U12(tt(),L)) = 0 >= 0 = mark(s(length(L)))
           
           active(length(nil())) = 0 >= 0 = mark(0())
           
           active(length(cons(N,L))) = 0 >= 0 = mark(U11(tt(),L))
           
           mark(zeros()) = 0 >= 0 = active(zeros())
           
           mark(cons(X1,X2)) = 0 >= 0 = active(cons(mark(X1),X2))
           
           mark(0()) = 0 >= 0 = active(0())
           
           mark(U11(X1,X2)) = 0 >= 0 = active(U11(mark(X1),X2))
           
           mark(tt()) = 0 >= 0 = active(tt())
           
           mark(U12(X1,X2)) = 0 >= 0 = active(U12(mark(X1),X2))
           
           mark(s(X)) = 0 >= 0 = active(s(mark(X)))
           
           mark(length(X)) = 0 >= 0 = active(length(mark(X)))
           
           mark(nil()) = 0 >= 0 = active(nil())
           
           cons(mark(X1),X2) = 0 >= 0 = cons(X1,X2)
           
           cons(X1,mark(X2)) = 0 >= 0 = cons(X1,X2)
           
           cons(active(X1),X2) = 0 >= 0 = cons(X1,X2)
           
           cons(X1,active(X2)) = 0 >= 0 = cons(X1,X2)
           
           U11(mark(X1),X2) = 1 >= 1 = U11(X1,X2)
           
           U11(X1,mark(X2)) = 1 >= 1 = U11(X1,X2)
           
           U11(active(X1),X2) = 1 >= 1 = U11(X1,X2)
           
           U11(X1,active(X2)) = 1 >= 1 = U11(X1,X2)
           
           U12(mark(X1),X2) = 1 >= 1 = U12(X1,X2)
           
           U12(X1,mark(X2)) = 1 >= 1 = U12(X1,X2)
           
           U12(active(X1),X2) = 1 >= 1 = U12(X1,X2)
           
           U12(X1,active(X2)) = 1 >= 1 = U12(X1,X2)
           
           s(mark(X)) = 0 >= 0 = s(X)
           
           s(active(X)) = 0 >= 0 = s(X)
           
           length(mark(X)) = 1 >= 1 = length(X)
           
           length(active(X)) = 1 >= 1 = length(X)
          problem:
           DPs:
            mark#(s(X)) -> mark#(X)
            mark#(length(X)) -> active#(length(mark(X)))
            active#(length(cons(N,L))) -> mark#(U11(tt(),L))
            active#(U12(tt(),L)) -> mark#(s(length(L)))
            mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
            active#(U11(tt(),L)) -> mark#(U12(tt(),L))
            mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
            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)
          SCC Processor:
           #sccs: 1
           #rules: 7
           #arcs: 103/81
           DPs:
            mark#(s(X)) -> mark#(X)
            mark#(length(X)) -> active#(length(mark(X)))
            active#(length(cons(N,L))) -> mark#(U11(tt(),L))
            mark#(U12(X1,X2)) -> active#(U12(mark(X1),X2))
            active#(U12(tt(),L)) -> mark#(s(length(L)))
            mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
            active#(U11(tt(),L)) -> mark#(U12(tt(),L))
           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#(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)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(cons#) = 1
     problem:
      DPs:
       cons#(mark(X1),X2) -> cons#(X1,X2)
       cons#(active(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)
     Subterm Criterion Processor:
      simple projection:
       pi(cons#) = 0
      problem:
       DPs:
        
       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)
      Qed
    
    DPs:
     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)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(U12#) = 1
     problem:
      DPs:
       U12#(mark(X1),X2) -> U12#(X1,X2)
       U12#(active(X1),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)
     Subterm Criterion Processor:
      simple projection:
       pi(U12#) = 0
      problem:
       DPs:
        
       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)
      Qed
    
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(length#) = 0
     problem:
      DPs:
       
      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)
     Qed
    
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(s#) = 0
     problem:
      DPs:
       
      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)
     Qed
    
    DPs:
     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)
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(U11#) = 1
     problem:
      DPs:
       U11#(mark(X1),X2) -> U11#(X1,X2)
       U11#(active(X1),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)
     Subterm Criterion Processor:
      simple projection:
       pi(U11#) = 0
      problem:
       DPs:
        
       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)
      Qed