MAYBE

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

Proof:
 DP Processor:
  DPs:
   active#(zeros()) -> cons#(0(),zeros())
   active#(zeros()) -> mark#(cons(0(),zeros()))
   active#(and(tt(),X)) -> mark#(X)
   active#(length(nil())) -> mark#(0())
   active#(length(cons(N,L))) -> length#(L)
   active#(length(cons(N,L))) -> s#(length(L))
   active#(length(cons(N,L))) -> mark#(s(length(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#(and(X1,X2)) -> mark#(X1)
   mark#(and(X1,X2)) -> and#(mark(X1),X2)
   mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
   mark#(tt()) -> active#(tt())
   mark#(length(X)) -> mark#(X)
   mark#(length(X)) -> length#(mark(X))
   mark#(length(X)) -> active#(length(mark(X)))
   mark#(nil()) -> active#(nil())
   mark#(s(X)) -> mark#(X)
   mark#(s(X)) -> s#(mark(X))
   mark#(s(X)) -> active#(s(mark(X)))
   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)
   and#(mark(X1),X2) -> and#(X1,X2)
   and#(X1,mark(X2)) -> and#(X1,X2)
   and#(active(X1),X2) -> and#(X1,X2)
   and#(X1,active(X2)) -> and#(X1,X2)
   length#(mark(X)) -> length#(X)
   length#(active(X)) -> length#(X)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
  TRS:
   active(zeros()) -> mark(cons(0(),zeros()))
   active(and(tt(),X)) -> mark(X)
   active(length(nil())) -> mark(0())
   active(length(cons(N,L))) -> mark(s(length(L)))
   mark(zeros()) -> active(zeros())
   mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
   mark(0()) -> active(0())
   mark(and(X1,X2)) -> active(and(mark(X1),X2))
   mark(tt()) -> active(tt())
   mark(length(X)) -> active(length(mark(X)))
   mark(nil()) -> active(nil())
   mark(s(X)) -> active(s(mark(X)))
   cons(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)
   and(mark(X1),X2) -> and(X1,X2)
   and(X1,mark(X2)) -> and(X1,X2)
   and(active(X1),X2) -> and(X1,X2)
   and(X1,active(X2)) -> and(X1,X2)
   length(mark(X)) -> length(X)
   length(active(X)) -> length(X)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
  TDG Processor:
   DPs:
    active#(zeros()) -> cons#(0(),zeros())
    active#(zeros()) -> mark#(cons(0(),zeros()))
    active#(and(tt(),X)) -> mark#(X)
    active#(length(nil())) -> mark#(0())
    active#(length(cons(N,L))) -> length#(L)
    active#(length(cons(N,L))) -> s#(length(L))
    active#(length(cons(N,L))) -> mark#(s(length(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#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(tt()) -> active#(tt())
    mark#(length(X)) -> mark#(X)
    mark#(length(X)) -> length#(mark(X))
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(nil()) -> active#(nil())
    mark#(s(X)) -> mark#(X)
    mark#(s(X)) -> s#(mark(X))
    mark#(s(X)) -> active#(s(mark(X)))
    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)
    and#(mark(X1),X2) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(X1,X2)
    length#(mark(X)) -> length#(X)
    length#(active(X)) -> length#(X)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
   TRS:
    active(zeros()) -> mark(cons(0(),zeros()))
    active(and(tt(),X)) -> mark(X)
    active(length(nil())) -> mark(0())
    active(length(cons(N,L))) -> mark(s(length(L)))
    mark(zeros()) -> active(zeros())
    mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
    mark(0()) -> active(0())
    mark(and(X1,X2)) -> active(and(mark(X1),X2))
    mark(tt()) -> active(tt())
    mark(length(X)) -> active(length(mark(X)))
    mark(nil()) -> active(nil())
    mark(s(X)) -> active(s(mark(X)))
    cons(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)
    and(mark(X1),X2) -> and(X1,X2)
    and(X1,mark(X2)) -> and(X1,X2)
    and(active(X1),X2) -> and(X1,X2)
    and(X1,active(X2)) -> and(X1,X2)
    length(mark(X)) -> length(X)
    length(active(X)) -> length(X)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
   graph:
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(active(X1),X2) -> and#(X1,X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(X1,mark(X2)) -> and#(X1,X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(X1,X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(X1,X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(X1,X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    and#(X1,active(X2)) -> and#(X1,X2) -> and#(mark(X1),X2) -> and#(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)
    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#(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#(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#(tt()) -> active#(tt())
    mark#(s(X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(s(X)) -> mark#(X) -> mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(s(X)) -> mark#(X) -> mark#(and(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#(s(length(L)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(N,L))) -> s#(length(L))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(N,L))) -> length#(L)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(nil())) -> mark#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(and(tt(),X)) -> mark#(X)
    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#(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#(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#(tt()) -> active#(tt())
    mark#(length(X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(length(X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(length(X)) -> mark#(X) -> mark#(and(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#(s(length(L)))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> s#(length(L))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> length#(L)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(nil())) -> mark#(0())
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(and(tt(),X)) -> mark#(X)
    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#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> mark#(s(length(L)))
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> s#(length(L))
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> length#(L)
    mark#(nil()) -> active#(nil()) ->
    active#(length(nil())) -> mark#(0())
    mark#(nil()) -> active#(nil()) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(nil()) -> active#(nil()) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
    and#(active(X1),X2) -> and#(X1,X2)
    mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    mark#(and(X1,X2)) -> and#(mark(X1),X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(s(X)) -> active#(s(mark(X)))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> s#(mark(X))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(s(X)) -> mark#(X)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(nil()) -> active#(nil())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> active#(length(mark(X)))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(length(X)) -> length#(mark(X))
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(length(X)) -> mark#(X)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(tt()) -> active#(tt())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(0()) -> active#(0())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(cons(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(zeros()) -> active#(zeros())
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> mark#(s(length(L)))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> s#(length(L))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> length#(L)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(length(nil())) -> mark#(0())
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(tt()) -> active#(tt()) ->
    active#(length(cons(N,L))) -> mark#(s(length(L)))
    mark#(tt()) -> active#(tt()) ->
    active#(length(cons(N,L))) -> s#(length(L))
    mark#(tt()) -> active#(tt()) ->
    active#(length(cons(N,L))) -> length#(L)
    mark#(tt()) -> active#(tt()) ->
    active#(length(nil())) -> mark#(0())
    mark#(tt()) -> active#(tt()) -> active#(and(tt(),X)) -> mark#(X)
    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#(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#(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#(tt()) -> active#(tt())
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(and(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#(s(length(L)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> s#(length(L))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> 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#(and(tt(),X)) -> mark#(X)
    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#(s(length(L)))
    mark#(0()) -> active#(0()) ->
    active#(length(cons(N,L))) -> s#(length(L))
    mark#(0()) -> active#(0()) ->
    active#(length(cons(N,L))) -> length#(L)
    mark#(0()) -> active#(0()) -> active#(length(nil())) -> mark#(0())
    mark#(0()) -> active#(0()) -> active#(and(tt(),X)) -> mark#(X)
    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#(s(length(L)))
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(cons(N,L))) -> s#(length(L))
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(cons(N,L))) -> length#(L)
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(nil())) -> mark#(0())
    mark#(zeros()) -> active#(zeros()) ->
    active#(and(tt(),X)) -> mark#(X)
    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#(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#(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#(tt()) -> active#(tt())
    active#(length(nil())) -> mark#(0()) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(length(nil())) -> mark#(0()) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(length(nil())) -> mark#(0()) ->
    mark#(and(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))) -> s#(length(L)) ->
    s#(active(X)) -> s#(X)
    active#(length(cons(N,L))) -> s#(length(L)) ->
    s#(mark(X)) -> s#(X)
    active#(length(cons(N,L))) -> length#(L) ->
    length#(active(X)) -> length#(X)
    active#(length(cons(N,L))) -> length#(L) ->
    length#(mark(X)) -> length#(X)
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(s(X)) -> mark#(X)
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(nil()) -> active#(nil())
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(length(X)) -> length#(mark(X))
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(length(X)) -> mark#(X)
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(tt()) -> active#(tt())
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(0()) -> active#(0())
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(length(cons(N,L))) -> mark#(s(length(L))) ->
    mark#(zeros()) -> active#(zeros())
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(and(tt(),X)) -> mark#(X) -> mark#(s(X)) -> s#(mark(X))
    active#(and(tt(),X)) -> mark#(X) -> mark#(s(X)) -> mark#(X)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(nil()) -> active#(nil())
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(length(X)) -> length#(mark(X))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(length(X)) -> mark#(X)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(tt()) -> active#(tt())
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(and(tt(),X)) -> mark#(X) -> mark#(0()) -> active#(0())
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(zeros()) -> active#(zeros())
    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#(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#(tt()) -> active#(tt())
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(and(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: 5
    #rules: 28
    #arcs: 244/1225
    DPs:
     mark#(s(X)) -> mark#(X)
     mark#(zeros()) -> active#(zeros())
     active#(zeros()) -> mark#(cons(0(),zeros()))
     mark#(cons(X1,X2)) -> mark#(X1)
     mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
     active#(and(tt(),X)) -> mark#(X)
     mark#(0()) -> active#(0())
     active#(length(nil())) -> mark#(0())
     mark#(and(X1,X2)) -> mark#(X1)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     active#(length(cons(N,L))) -> mark#(s(length(L)))
     mark#(tt()) -> active#(tt())
     mark#(length(X)) -> mark#(X)
     mark#(length(X)) -> active#(length(mark(X)))
     mark#(nil()) -> active#(nil())
     mark#(s(X)) -> active#(s(mark(X)))
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(and(tt(),X)) -> mark(X)
     active(length(nil())) -> mark(0())
     active(length(cons(N,L))) -> mark(s(length(L)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(0()) -> active(0())
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(tt()) -> active(tt())
     mark(length(X)) -> active(length(mark(X)))
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(mark(X)))
     cons(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)
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(X1,X2)
     length(mark(X)) -> length(X)
     length(active(X)) -> length(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [mark#](x0) = x0 + 1,
      
      [active#](x0) = x0 + 1,
      
      [s](x0) = x0,
      
      [length](x0) = x0 + 1,
      
      [nil] = 0,
      
      [and](x0, x1) = x0 + x1,
      
      [tt] = 0,
      
      [mark](x0) = x0,
      
      [cons](x0, x1) = x0 + x1,
      
      [0] = 0,
      
      [active](x0) = x0,
      
      [zeros] = 1
     orientation:
      mark#(s(X)) = X + 1 >= X + 1 = mark#(X)
      
      mark#(zeros()) = 2 >= 2 = active#(zeros())
      
      active#(zeros()) = 2 >= 2 = mark#(cons(0(),zeros()))
      
      mark#(cons(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = mark#(X1)
      
      mark#(cons(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = active#(cons(mark(X1),X2))
      
      active#(and(tt(),X)) = X + 1 >= X + 1 = mark#(X)
      
      mark#(0()) = 1 >= 1 = active#(0())
      
      active#(length(nil())) = 2 >= 1 = mark#(0())
      
      mark#(and(X1,X2)) = X1 + X2 + 1 >= X1 + 1 = mark#(X1)
      
      mark#(and(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = active#(and(mark(X1),X2))
      
      active#(length(cons(N,L))) = L + N + 2 >= L + 2 = mark#(s(length(L)))
      
      mark#(tt()) = 1 >= 1 = active#(tt())
      
      mark#(length(X)) = X + 2 >= X + 1 = mark#(X)
      
      mark#(length(X)) = X + 2 >= X + 2 = active#(length(mark(X)))
      
      mark#(nil()) = 1 >= 1 = active#(nil())
      
      mark#(s(X)) = X + 1 >= X + 1 = active#(s(mark(X)))
      
      active(zeros()) = 1 >= 1 = mark(cons(0(),zeros()))
      
      active(and(tt(),X)) = X >= X = mark(X)
      
      active(length(nil())) = 1 >= 0 = mark(0())
      
      active(length(cons(N,L))) = L + N + 1 >= L + 1 = mark(s(length(L)))
      
      mark(zeros()) = 1 >= 1 = active(zeros())
      
      mark(cons(X1,X2)) = X1 + X2 >= X1 + X2 = active(cons(mark(X1),X2))
      
      mark(0()) = 0 >= 0 = active(0())
      
      mark(and(X1,X2)) = X1 + X2 >= X1 + X2 = active(and(mark(X1),X2))
      
      mark(tt()) = 0 >= 0 = active(tt())
      
      mark(length(X)) = X + 1 >= X + 1 = active(length(mark(X)))
      
      mark(nil()) = 0 >= 0 = active(nil())
      
      mark(s(X)) = X >= X = active(s(mark(X)))
      
      cons(mark(X1),X2) = X1 + X2 >= X1 + X2 = cons(X1,X2)
      
      cons(X1,mark(X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
      
      cons(active(X1),X2) = X1 + X2 >= X1 + X2 = cons(X1,X2)
      
      cons(X1,active(X2)) = X1 + X2 >= X1 + X2 = cons(X1,X2)
      
      and(mark(X1),X2) = X1 + X2 >= X1 + X2 = and(X1,X2)
      
      and(X1,mark(X2)) = X1 + X2 >= X1 + X2 = and(X1,X2)
      
      and(active(X1),X2) = X1 + X2 >= X1 + X2 = and(X1,X2)
      
      and(X1,active(X2)) = X1 + X2 >= X1 + X2 = and(X1,X2)
      
      length(mark(X)) = X + 1 >= X + 1 = length(X)
      
      length(active(X)) = X + 1 >= X + 1 = length(X)
      
      s(mark(X)) = X >= X = s(X)
      
      s(active(X)) = X >= X = s(X)
     problem:
      DPs:
       mark#(s(X)) -> mark#(X)
       mark#(zeros()) -> active#(zeros())
       active#(zeros()) -> mark#(cons(0(),zeros()))
       mark#(cons(X1,X2)) -> mark#(X1)
       mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
       active#(and(tt(),X)) -> mark#(X)
       mark#(0()) -> active#(0())
       mark#(and(X1,X2)) -> mark#(X1)
       mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
       active#(length(cons(N,L))) -> mark#(s(length(L)))
       mark#(tt()) -> active#(tt())
       mark#(length(X)) -> active#(length(mark(X)))
       mark#(nil()) -> active#(nil())
       mark#(s(X)) -> active#(s(mark(X)))
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(and(tt(),X)) -> mark(X)
       active(length(nil())) -> mark(0())
       active(length(cons(N,L))) -> mark(s(length(L)))
       mark(zeros()) -> active(zeros())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(0()) -> active(0())
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(tt()) -> active(tt())
       mark(length(X)) -> active(length(mark(X)))
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(mark(X)))
       cons(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)
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(X1,X2)
       length(mark(X)) -> length(X)
       length(active(X)) -> length(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [mark#](x0) = x0,
       
       [active#](x0) = x0,
       
       [s](x0) = x0,
       
       [length](x0) = 0,
       
       [nil] = 1,
       
       [and](x0, x1) = x0 + x1 + 1,
       
       [tt] = 0,
       
       [mark](x0) = x0,
       
       [cons](x0, x1) = x0,
       
       [0] = 0,
       
       [active](x0) = x0,
       
       [zeros] = 0
      orientation:
       mark#(s(X)) = X >= X = mark#(X)
       
       mark#(zeros()) = 0 >= 0 = active#(zeros())
       
       active#(zeros()) = 0 >= 0 = mark#(cons(0(),zeros()))
       
       mark#(cons(X1,X2)) = X1 >= X1 = mark#(X1)
       
       mark#(cons(X1,X2)) = X1 >= X1 = active#(cons(mark(X1),X2))
       
       active#(and(tt(),X)) = X + 1 >= X = mark#(X)
       
       mark#(0()) = 0 >= 0 = active#(0())
       
       mark#(and(X1,X2)) = X1 + X2 + 1 >= X1 = mark#(X1)
       
       mark#(and(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = active#(and(mark(X1),X2))
       
       active#(length(cons(N,L))) = 0 >= 0 = mark#(s(length(L)))
       
       mark#(tt()) = 0 >= 0 = active#(tt())
       
       mark#(length(X)) = 0 >= 0 = active#(length(mark(X)))
       
       mark#(nil()) = 1 >= 1 = active#(nil())
       
       mark#(s(X)) = X >= X = active#(s(mark(X)))
       
       active(zeros()) = 0 >= 0 = mark(cons(0(),zeros()))
       
       active(and(tt(),X)) = X + 1 >= X = mark(X)
       
       active(length(nil())) = 0 >= 0 = mark(0())
       
       active(length(cons(N,L))) = 0 >= 0 = mark(s(length(L)))
       
       mark(zeros()) = 0 >= 0 = active(zeros())
       
       mark(cons(X1,X2)) = X1 >= X1 = active(cons(mark(X1),X2))
       
       mark(0()) = 0 >= 0 = active(0())
       
       mark(and(X1,X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = active(and(mark(X1),X2))
       
       mark(tt()) = 0 >= 0 = active(tt())
       
       mark(length(X)) = 0 >= 0 = active(length(mark(X)))
       
       mark(nil()) = 1 >= 1 = active(nil())
       
       mark(s(X)) = X >= X = active(s(mark(X)))
       
       cons(mark(X1),X2) = X1 >= X1 = cons(X1,X2)
       
       cons(X1,mark(X2)) = X1 >= X1 = cons(X1,X2)
       
       cons(active(X1),X2) = X1 >= X1 = cons(X1,X2)
       
       cons(X1,active(X2)) = X1 >= X1 = cons(X1,X2)
       
       and(mark(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = and(X1,X2)
       
       and(X1,mark(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = and(X1,X2)
       
       and(active(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = and(X1,X2)
       
       and(X1,active(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = and(X1,X2)
       
       length(mark(X)) = 0 >= 0 = length(X)
       
       length(active(X)) = 0 >= 0 = length(X)
       
       s(mark(X)) = X >= X = s(X)
       
       s(active(X)) = X >= X = s(X)
      problem:
       DPs:
        mark#(s(X)) -> mark#(X)
        mark#(zeros()) -> active#(zeros())
        active#(zeros()) -> mark#(cons(0(),zeros()))
        mark#(cons(X1,X2)) -> mark#(X1)
        mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
        mark#(0()) -> active#(0())
        mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
        active#(length(cons(N,L))) -> mark#(s(length(L)))
        mark#(tt()) -> active#(tt())
        mark#(length(X)) -> active#(length(mark(X)))
        mark#(nil()) -> active#(nil())
        mark#(s(X)) -> active#(s(mark(X)))
       TRS:
        active(zeros()) -> mark(cons(0(),zeros()))
        active(and(tt(),X)) -> mark(X)
        active(length(nil())) -> mark(0())
        active(length(cons(N,L))) -> mark(s(length(L)))
        mark(zeros()) -> active(zeros())
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(0()) -> active(0())
        mark(and(X1,X2)) -> active(and(mark(X1),X2))
        mark(tt()) -> active(tt())
        mark(length(X)) -> active(length(mark(X)))
        mark(nil()) -> active(nil())
        mark(s(X)) -> active(s(mark(X)))
        cons(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)
        and(mark(X1),X2) -> and(X1,X2)
        and(X1,mark(X2)) -> and(X1,X2)
        and(active(X1),X2) -> and(X1,X2)
        and(X1,active(X2)) -> and(X1,X2)
        length(mark(X)) -> length(X)
        length(active(X)) -> length(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
      Matrix Interpretation Processor:
       dimension: 1
       interpretation:
        [mark#](x0) = x0,
        
        [active#](x0) = 0,
        
        [s](x0) = x0,
        
        [length](x0) = 0,
        
        [nil] = 0,
        
        [and](x0, x1) = x1,
        
        [tt] = 1,
        
        [mark](x0) = x0,
        
        [cons](x0, x1) = x0,
        
        [0] = 0,
        
        [active](x0) = x0,
        
        [zeros] = 0
       orientation:
        mark#(s(X)) = X >= X = mark#(X)
        
        mark#(zeros()) = 0 >= 0 = active#(zeros())
        
        active#(zeros()) = 0 >= 0 = mark#(cons(0(),zeros()))
        
        mark#(cons(X1,X2)) = X1 >= X1 = mark#(X1)
        
        mark#(cons(X1,X2)) = X1 >= 0 = active#(cons(mark(X1),X2))
        
        mark#(0()) = 0 >= 0 = active#(0())
        
        mark#(and(X1,X2)) = X2 >= 0 = active#(and(mark(X1),X2))
        
        active#(length(cons(N,L))) = 0 >= 0 = mark#(s(length(L)))
        
        mark#(tt()) = 1 >= 0 = active#(tt())
        
        mark#(length(X)) = 0 >= 0 = active#(length(mark(X)))
        
        mark#(nil()) = 0 >= 0 = active#(nil())
        
        mark#(s(X)) = X >= 0 = active#(s(mark(X)))
        
        active(zeros()) = 0 >= 0 = mark(cons(0(),zeros()))
        
        active(and(tt(),X)) = X >= X = mark(X)
        
        active(length(nil())) = 0 >= 0 = mark(0())
        
        active(length(cons(N,L))) = 0 >= 0 = mark(s(length(L)))
        
        mark(zeros()) = 0 >= 0 = active(zeros())
        
        mark(cons(X1,X2)) = X1 >= X1 = active(cons(mark(X1),X2))
        
        mark(0()) = 0 >= 0 = active(0())
        
        mark(and(X1,X2)) = X2 >= X2 = active(and(mark(X1),X2))
        
        mark(tt()) = 1 >= 1 = active(tt())
        
        mark(length(X)) = 0 >= 0 = active(length(mark(X)))
        
        mark(nil()) = 0 >= 0 = active(nil())
        
        mark(s(X)) = X >= X = active(s(mark(X)))
        
        cons(mark(X1),X2) = X1 >= X1 = cons(X1,X2)
        
        cons(X1,mark(X2)) = X1 >= X1 = cons(X1,X2)
        
        cons(active(X1),X2) = X1 >= X1 = cons(X1,X2)
        
        cons(X1,active(X2)) = X1 >= X1 = cons(X1,X2)
        
        and(mark(X1),X2) = X2 >= X2 = and(X1,X2)
        
        and(X1,mark(X2)) = X2 >= X2 = and(X1,X2)
        
        and(active(X1),X2) = X2 >= X2 = and(X1,X2)
        
        and(X1,active(X2)) = X2 >= X2 = and(X1,X2)
        
        length(mark(X)) = 0 >= 0 = length(X)
        
        length(active(X)) = 0 >= 0 = length(X)
        
        s(mark(X)) = X >= X = s(X)
        
        s(active(X)) = X >= X = s(X)
       problem:
        DPs:
         mark#(s(X)) -> mark#(X)
         mark#(zeros()) -> active#(zeros())
         active#(zeros()) -> mark#(cons(0(),zeros()))
         mark#(cons(X1,X2)) -> mark#(X1)
         mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
         mark#(0()) -> active#(0())
         mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
         active#(length(cons(N,L))) -> mark#(s(length(L)))
         mark#(length(X)) -> active#(length(mark(X)))
         mark#(nil()) -> active#(nil())
         mark#(s(X)) -> active#(s(mark(X)))
        TRS:
         active(zeros()) -> mark(cons(0(),zeros()))
         active(and(tt(),X)) -> mark(X)
         active(length(nil())) -> mark(0())
         active(length(cons(N,L))) -> mark(s(length(L)))
         mark(zeros()) -> active(zeros())
         mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
         mark(0()) -> active(0())
         mark(and(X1,X2)) -> active(and(mark(X1),X2))
         mark(tt()) -> active(tt())
         mark(length(X)) -> active(length(mark(X)))
         mark(nil()) -> active(nil())
         mark(s(X)) -> active(s(mark(X)))
         cons(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)
         and(mark(X1),X2) -> and(X1,X2)
         and(X1,mark(X2)) -> and(X1,X2)
         and(active(X1),X2) -> and(X1,X2)
         and(X1,active(X2)) -> and(X1,X2)
         length(mark(X)) -> length(X)
         length(active(X)) -> length(X)
         s(mark(X)) -> s(X)
         s(active(X)) -> s(X)
       Matrix Interpretation Processor:
        dimension: 1
        interpretation:
         [mark#](x0) = 1,
         
         [active#](x0) = x0,
         
         [s](x0) = 0,
         
         [length](x0) = 1,
         
         [nil] = 1,
         
         [and](x0, x1) = 0,
         
         [tt] = 0,
         
         [mark](x0) = 0,
         
         [cons](x0, x1) = 1,
         
         [0] = 1,
         
         [active](x0) = 0,
         
         [zeros] = 1
        orientation:
         mark#(s(X)) = 1 >= 1 = mark#(X)
         
         mark#(zeros()) = 1 >= 1 = active#(zeros())
         
         active#(zeros()) = 1 >= 1 = mark#(cons(0(),zeros()))
         
         mark#(cons(X1,X2)) = 1 >= 1 = mark#(X1)
         
         mark#(cons(X1,X2)) = 1 >= 1 = active#(cons(mark(X1),X2))
         
         mark#(0()) = 1 >= 1 = active#(0())
         
         mark#(and(X1,X2)) = 1 >= 0 = active#(and(mark(X1),X2))
         
         active#(length(cons(N,L))) = 1 >= 1 = mark#(s(length(L)))
         
         mark#(length(X)) = 1 >= 1 = active#(length(mark(X)))
         
         mark#(nil()) = 1 >= 1 = active#(nil())
         
         mark#(s(X)) = 1 >= 0 = active#(s(mark(X)))
         
         active(zeros()) = 0 >= 0 = mark(cons(0(),zeros()))
         
         active(and(tt(),X)) = 0 >= 0 = mark(X)
         
         active(length(nil())) = 0 >= 0 = mark(0())
         
         active(length(cons(N,L))) = 0 >= 0 = mark(s(length(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(and(X1,X2)) = 0 >= 0 = active(and(mark(X1),X2))
         
         mark(tt()) = 0 >= 0 = active(tt())
         
         mark(length(X)) = 0 >= 0 = active(length(mark(X)))
         
         mark(nil()) = 0 >= 0 = active(nil())
         
         mark(s(X)) = 0 >= 0 = active(s(mark(X)))
         
         cons(mark(X1),X2) = 1 >= 1 = cons(X1,X2)
         
         cons(X1,mark(X2)) = 1 >= 1 = cons(X1,X2)
         
         cons(active(X1),X2) = 1 >= 1 = cons(X1,X2)
         
         cons(X1,active(X2)) = 1 >= 1 = cons(X1,X2)
         
         and(mark(X1),X2) = 0 >= 0 = and(X1,X2)
         
         and(X1,mark(X2)) = 0 >= 0 = and(X1,X2)
         
         and(active(X1),X2) = 0 >= 0 = and(X1,X2)
         
         and(X1,active(X2)) = 0 >= 0 = and(X1,X2)
         
         length(mark(X)) = 1 >= 1 = length(X)
         
         length(active(X)) = 1 >= 1 = length(X)
         
         s(mark(X)) = 0 >= 0 = s(X)
         
         s(active(X)) = 0 >= 0 = s(X)
        problem:
         DPs:
          mark#(s(X)) -> mark#(X)
          mark#(zeros()) -> active#(zeros())
          active#(zeros()) -> mark#(cons(0(),zeros()))
          mark#(cons(X1,X2)) -> mark#(X1)
          mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
          mark#(0()) -> active#(0())
          active#(length(cons(N,L))) -> mark#(s(length(L)))
          mark#(length(X)) -> active#(length(mark(X)))
          mark#(nil()) -> active#(nil())
         TRS:
          active(zeros()) -> mark(cons(0(),zeros()))
          active(and(tt(),X)) -> mark(X)
          active(length(nil())) -> mark(0())
          active(length(cons(N,L))) -> mark(s(length(L)))
          mark(zeros()) -> active(zeros())
          mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
          mark(0()) -> active(0())
          mark(and(X1,X2)) -> active(and(mark(X1),X2))
          mark(tt()) -> active(tt())
          mark(length(X)) -> active(length(mark(X)))
          mark(nil()) -> active(nil())
          mark(s(X)) -> active(s(mark(X)))
          cons(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)
          and(mark(X1),X2) -> and(X1,X2)
          and(X1,mark(X2)) -> and(X1,X2)
          and(active(X1),X2) -> and(X1,X2)
          and(X1,active(X2)) -> and(X1,X2)
          length(mark(X)) -> length(X)
          length(active(X)) -> length(X)
          s(mark(X)) -> s(X)
          s(active(X)) -> s(X)
        Matrix Interpretation Processor:
         dimension: 1
         interpretation:
          [mark#](x0) = 1,
          
          [active#](x0) = x0,
          
          [s](x0) = 0,
          
          [length](x0) = 1,
          
          [nil] = 0,
          
          [and](x0, x1) = 0,
          
          [tt] = 0,
          
          [mark](x0) = 0,
          
          [cons](x0, x1) = 0,
          
          [0] = 1,
          
          [active](x0) = 0,
          
          [zeros] = 1
         orientation:
          mark#(s(X)) = 1 >= 1 = mark#(X)
          
          mark#(zeros()) = 1 >= 1 = active#(zeros())
          
          active#(zeros()) = 1 >= 1 = mark#(cons(0(),zeros()))
          
          mark#(cons(X1,X2)) = 1 >= 1 = mark#(X1)
          
          mark#(cons(X1,X2)) = 1 >= 0 = active#(cons(mark(X1),X2))
          
          mark#(0()) = 1 >= 1 = active#(0())
          
          active#(length(cons(N,L))) = 1 >= 1 = mark#(s(length(L)))
          
          mark#(length(X)) = 1 >= 1 = active#(length(mark(X)))
          
          mark#(nil()) = 1 >= 0 = active#(nil())
          
          active(zeros()) = 0 >= 0 = mark(cons(0(),zeros()))
          
          active(and(tt(),X)) = 0 >= 0 = mark(X)
          
          active(length(nil())) = 0 >= 0 = mark(0())
          
          active(length(cons(N,L))) = 0 >= 0 = mark(s(length(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(and(X1,X2)) = 0 >= 0 = active(and(mark(X1),X2))
          
          mark(tt()) = 0 >= 0 = active(tt())
          
          mark(length(X)) = 0 >= 0 = active(length(mark(X)))
          
          mark(nil()) = 0 >= 0 = active(nil())
          
          mark(s(X)) = 0 >= 0 = active(s(mark(X)))
          
          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)
          
          and(mark(X1),X2) = 0 >= 0 = and(X1,X2)
          
          and(X1,mark(X2)) = 0 >= 0 = and(X1,X2)
          
          and(active(X1),X2) = 0 >= 0 = and(X1,X2)
          
          and(X1,active(X2)) = 0 >= 0 = and(X1,X2)
          
          length(mark(X)) = 1 >= 1 = length(X)
          
          length(active(X)) = 1 >= 1 = length(X)
          
          s(mark(X)) = 0 >= 0 = s(X)
          
          s(active(X)) = 0 >= 0 = s(X)
         problem:
          DPs:
           mark#(s(X)) -> mark#(X)
           mark#(zeros()) -> active#(zeros())
           active#(zeros()) -> mark#(cons(0(),zeros()))
           mark#(cons(X1,X2)) -> mark#(X1)
           mark#(0()) -> active#(0())
           active#(length(cons(N,L))) -> mark#(s(length(L)))
           mark#(length(X)) -> active#(length(mark(X)))
          TRS:
           active(zeros()) -> mark(cons(0(),zeros()))
           active(and(tt(),X)) -> mark(X)
           active(length(nil())) -> mark(0())
           active(length(cons(N,L))) -> mark(s(length(L)))
           mark(zeros()) -> active(zeros())
           mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
           mark(0()) -> active(0())
           mark(and(X1,X2)) -> active(and(mark(X1),X2))
           mark(tt()) -> active(tt())
           mark(length(X)) -> active(length(mark(X)))
           mark(nil()) -> active(nil())
           mark(s(X)) -> active(s(mark(X)))
           cons(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)
           and(mark(X1),X2) -> and(X1,X2)
           and(X1,mark(X2)) -> and(X1,X2)
           and(active(X1),X2) -> and(X1,X2)
           and(X1,active(X2)) -> and(X1,X2)
           length(mark(X)) -> length(X)
           length(active(X)) -> length(X)
           s(mark(X)) -> s(X)
           s(active(X)) -> s(X)
         Matrix Interpretation Processor:
          dimension: 1
          interpretation:
           [mark#](x0) = x0,
           
           [active#](x0) = 0,
           
           [s](x0) = x0,
           
           [length](x0) = 0,
           
           [nil] = 0,
           
           [and](x0, x1) = x1,
           
           [tt] = 0,
           
           [mark](x0) = x0,
           
           [cons](x0, x1) = x0,
           
           [0] = 0,
           
           [active](x0) = x0,
           
           [zeros] = 1
          orientation:
           mark#(s(X)) = X >= X = mark#(X)
           
           mark#(zeros()) = 1 >= 0 = active#(zeros())
           
           active#(zeros()) = 0 >= 0 = mark#(cons(0(),zeros()))
           
           mark#(cons(X1,X2)) = X1 >= X1 = mark#(X1)
           
           mark#(0()) = 0 >= 0 = active#(0())
           
           active#(length(cons(N,L))) = 0 >= 0 = mark#(s(length(L)))
           
           mark#(length(X)) = 0 >= 0 = active#(length(mark(X)))
           
           active(zeros()) = 1 >= 0 = mark(cons(0(),zeros()))
           
           active(and(tt(),X)) = X >= X = mark(X)
           
           active(length(nil())) = 0 >= 0 = mark(0())
           
           active(length(cons(N,L))) = 0 >= 0 = mark(s(length(L)))
           
           mark(zeros()) = 1 >= 1 = active(zeros())
           
           mark(cons(X1,X2)) = X1 >= X1 = active(cons(mark(X1),X2))
           
           mark(0()) = 0 >= 0 = active(0())
           
           mark(and(X1,X2)) = X2 >= X2 = active(and(mark(X1),X2))
           
           mark(tt()) = 0 >= 0 = active(tt())
           
           mark(length(X)) = 0 >= 0 = active(length(mark(X)))
           
           mark(nil()) = 0 >= 0 = active(nil())
           
           mark(s(X)) = X >= X = active(s(mark(X)))
           
           cons(mark(X1),X2) = X1 >= X1 = cons(X1,X2)
           
           cons(X1,mark(X2)) = X1 >= X1 = cons(X1,X2)
           
           cons(active(X1),X2) = X1 >= X1 = cons(X1,X2)
           
           cons(X1,active(X2)) = X1 >= X1 = cons(X1,X2)
           
           and(mark(X1),X2) = X2 >= X2 = and(X1,X2)
           
           and(X1,mark(X2)) = X2 >= X2 = and(X1,X2)
           
           and(active(X1),X2) = X2 >= X2 = and(X1,X2)
           
           and(X1,active(X2)) = X2 >= X2 = and(X1,X2)
           
           length(mark(X)) = 0 >= 0 = length(X)
           
           length(active(X)) = 0 >= 0 = length(X)
           
           s(mark(X)) = X >= X = s(X)
           
           s(active(X)) = X >= X = s(X)
          problem:
           DPs:
            mark#(s(X)) -> mark#(X)
            active#(zeros()) -> mark#(cons(0(),zeros()))
            mark#(cons(X1,X2)) -> mark#(X1)
            mark#(0()) -> active#(0())
            active#(length(cons(N,L))) -> mark#(s(length(L)))
            mark#(length(X)) -> active#(length(mark(X)))
           TRS:
            active(zeros()) -> mark(cons(0(),zeros()))
            active(and(tt(),X)) -> mark(X)
            active(length(nil())) -> mark(0())
            active(length(cons(N,L))) -> mark(s(length(L)))
            mark(zeros()) -> active(zeros())
            mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
            mark(0()) -> active(0())
            mark(and(X1,X2)) -> active(and(mark(X1),X2))
            mark(tt()) -> active(tt())
            mark(length(X)) -> active(length(mark(X)))
            mark(nil()) -> active(nil())
            mark(s(X)) -> active(s(mark(X)))
            cons(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)
            and(mark(X1),X2) -> and(X1,X2)
            and(X1,mark(X2)) -> and(X1,X2)
            and(active(X1),X2) -> and(X1,X2)
            and(X1,active(X2)) -> and(X1,X2)
            length(mark(X)) -> length(X)
            length(active(X)) -> length(X)
            s(mark(X)) -> s(X)
            s(active(X)) -> s(X)
          Matrix Interpretation Processor:
           dimension: 1
           interpretation:
            [mark#](x0) = 0,
            
            [active#](x0) = x0,
            
            [s](x0) = 0,
            
            [length](x0) = 0,
            
            [nil] = 0,
            
            [and](x0, x1) = 0,
            
            [tt] = 0,
            
            [mark](x0) = 0,
            
            [cons](x0, x1) = 0,
            
            [0] = 0,
            
            [active](x0) = 0,
            
            [zeros] = 1
           orientation:
            mark#(s(X)) = 0 >= 0 = mark#(X)
            
            active#(zeros()) = 1 >= 0 = mark#(cons(0(),zeros()))
            
            mark#(cons(X1,X2)) = 0 >= 0 = mark#(X1)
            
            mark#(0()) = 0 >= 0 = active#(0())
            
            active#(length(cons(N,L))) = 0 >= 0 = mark#(s(length(L)))
            
            mark#(length(X)) = 0 >= 0 = active#(length(mark(X)))
            
            active(zeros()) = 0 >= 0 = mark(cons(0(),zeros()))
            
            active(and(tt(),X)) = 0 >= 0 = mark(X)
            
            active(length(nil())) = 0 >= 0 = mark(0())
            
            active(length(cons(N,L))) = 0 >= 0 = mark(s(length(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(and(X1,X2)) = 0 >= 0 = active(and(mark(X1),X2))
            
            mark(tt()) = 0 >= 0 = active(tt())
            
            mark(length(X)) = 0 >= 0 = active(length(mark(X)))
            
            mark(nil()) = 0 >= 0 = active(nil())
            
            mark(s(X)) = 0 >= 0 = active(s(mark(X)))
            
            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)
            
            and(mark(X1),X2) = 0 >= 0 = and(X1,X2)
            
            and(X1,mark(X2)) = 0 >= 0 = and(X1,X2)
            
            and(active(X1),X2) = 0 >= 0 = and(X1,X2)
            
            and(X1,active(X2)) = 0 >= 0 = and(X1,X2)
            
            length(mark(X)) = 0 >= 0 = length(X)
            
            length(active(X)) = 0 >= 0 = length(X)
            
            s(mark(X)) = 0 >= 0 = s(X)
            
            s(active(X)) = 0 >= 0 = s(X)
           problem:
            DPs:
             mark#(s(X)) -> mark#(X)
             mark#(cons(X1,X2)) -> mark#(X1)
             mark#(0()) -> active#(0())
             active#(length(cons(N,L))) -> mark#(s(length(L)))
             mark#(length(X)) -> active#(length(mark(X)))
            TRS:
             active(zeros()) -> mark(cons(0(),zeros()))
             active(and(tt(),X)) -> mark(X)
             active(length(nil())) -> mark(0())
             active(length(cons(N,L))) -> mark(s(length(L)))
             mark(zeros()) -> active(zeros())
             mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
             mark(0()) -> active(0())
             mark(and(X1,X2)) -> active(and(mark(X1),X2))
             mark(tt()) -> active(tt())
             mark(length(X)) -> active(length(mark(X)))
             mark(nil()) -> active(nil())
             mark(s(X)) -> active(s(mark(X)))
             cons(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)
             and(mark(X1),X2) -> and(X1,X2)
             and(X1,mark(X2)) -> and(X1,X2)
             and(active(X1),X2) -> and(X1,X2)
             and(X1,active(X2)) -> and(X1,X2)
             length(mark(X)) -> length(X)
             length(active(X)) -> length(X)
             s(mark(X)) -> s(X)
             s(active(X)) -> s(X)
           Matrix Interpretation Processor:
            dimension: 1
            interpretation:
             [mark#](x0) = 1,
             
             [active#](x0) = x0,
             
             [s](x0) = 0,
             
             [length](x0) = 1,
             
             [nil] = 0,
             
             [and](x0, x1) = 0,
             
             [tt] = 0,
             
             [mark](x0) = 0,
             
             [cons](x0, x1) = 0,
             
             [0] = 0,
             
             [active](x0) = 0,
             
             [zeros] = 0
            orientation:
             mark#(s(X)) = 1 >= 1 = mark#(X)
             
             mark#(cons(X1,X2)) = 1 >= 1 = mark#(X1)
             
             mark#(0()) = 1 >= 0 = active#(0())
             
             active#(length(cons(N,L))) = 1 >= 1 = mark#(s(length(L)))
             
             mark#(length(X)) = 1 >= 1 = active#(length(mark(X)))
             
             active(zeros()) = 0 >= 0 = mark(cons(0(),zeros()))
             
             active(and(tt(),X)) = 0 >= 0 = mark(X)
             
             active(length(nil())) = 0 >= 0 = mark(0())
             
             active(length(cons(N,L))) = 0 >= 0 = mark(s(length(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(and(X1,X2)) = 0 >= 0 = active(and(mark(X1),X2))
             
             mark(tt()) = 0 >= 0 = active(tt())
             
             mark(length(X)) = 0 >= 0 = active(length(mark(X)))
             
             mark(nil()) = 0 >= 0 = active(nil())
             
             mark(s(X)) = 0 >= 0 = active(s(mark(X)))
             
             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)
             
             and(mark(X1),X2) = 0 >= 0 = and(X1,X2)
             
             and(X1,mark(X2)) = 0 >= 0 = and(X1,X2)
             
             and(active(X1),X2) = 0 >= 0 = and(X1,X2)
             
             and(X1,active(X2)) = 0 >= 0 = and(X1,X2)
             
             length(mark(X)) = 1 >= 1 = length(X)
             
             length(active(X)) = 1 >= 1 = length(X)
             
             s(mark(X)) = 0 >= 0 = s(X)
             
             s(active(X)) = 0 >= 0 = s(X)
            problem:
             DPs:
              mark#(s(X)) -> mark#(X)
              mark#(cons(X1,X2)) -> mark#(X1)
              active#(length(cons(N,L))) -> mark#(s(length(L)))
              mark#(length(X)) -> active#(length(mark(X)))
             TRS:
              active(zeros()) -> mark(cons(0(),zeros()))
              active(and(tt(),X)) -> mark(X)
              active(length(nil())) -> mark(0())
              active(length(cons(N,L))) -> mark(s(length(L)))
              mark(zeros()) -> active(zeros())
              mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
              mark(0()) -> active(0())
              mark(and(X1,X2)) -> active(and(mark(X1),X2))
              mark(tt()) -> active(tt())
              mark(length(X)) -> active(length(mark(X)))
              mark(nil()) -> active(nil())
              mark(s(X)) -> active(s(mark(X)))
              cons(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)
              and(mark(X1),X2) -> and(X1,X2)
              and(X1,mark(X2)) -> and(X1,X2)
              and(active(X1),X2) -> and(X1,X2)
              and(X1,active(X2)) -> and(X1,X2)
              length(mark(X)) -> length(X)
              length(active(X)) -> length(X)
              s(mark(X)) -> s(X)
              s(active(X)) -> s(X)
            Matrix Interpretation Processor:
             dimension: 1
             interpretation:
              [mark#](x0) = x0,
              
              [active#](x0) = 0,
              
              [s](x0) = x0,
              
              [length](x0) = 0,
              
              [nil] = 0,
              
              [and](x0, x1) = x1,
              
              [tt] = 0,
              
              [mark](x0) = x0,
              
              [cons](x0, x1) = x0 + 1,
              
              [0] = 0,
              
              [active](x0) = x0,
              
              [zeros] = 1
             orientation:
              mark#(s(X)) = X >= X = mark#(X)
              
              mark#(cons(X1,X2)) = X1 + 1 >= X1 = mark#(X1)
              
              active#(length(cons(N,L))) = 0 >= 0 = mark#(s(length(L)))
              
              mark#(length(X)) = 0 >= 0 = active#(length(mark(X)))
              
              active(zeros()) = 1 >= 1 = mark(cons(0(),zeros()))
              
              active(and(tt(),X)) = X >= X = mark(X)
              
              active(length(nil())) = 0 >= 0 = mark(0())
              
              active(length(cons(N,L))) = 0 >= 0 = mark(s(length(L)))
              
              mark(zeros()) = 1 >= 1 = active(zeros())
              
              mark(cons(X1,X2)) = X1 + 1 >= X1 + 1 = active(cons(mark(X1),X2))
              
              mark(0()) = 0 >= 0 = active(0())
              
              mark(and(X1,X2)) = X2 >= X2 = active(and(mark(X1),X2))
              
              mark(tt()) = 0 >= 0 = active(tt())
              
              mark(length(X)) = 0 >= 0 = active(length(mark(X)))
              
              mark(nil()) = 0 >= 0 = active(nil())
              
              mark(s(X)) = X >= X = active(s(mark(X)))
              
              cons(mark(X1),X2) = X1 + 1 >= X1 + 1 = cons(X1,X2)
              
              cons(X1,mark(X2)) = X1 + 1 >= X1 + 1 = cons(X1,X2)
              
              cons(active(X1),X2) = X1 + 1 >= X1 + 1 = cons(X1,X2)
              
              cons(X1,active(X2)) = X1 + 1 >= X1 + 1 = cons(X1,X2)
              
              and(mark(X1),X2) = X2 >= X2 = and(X1,X2)
              
              and(X1,mark(X2)) = X2 >= X2 = and(X1,X2)
              
              and(active(X1),X2) = X2 >= X2 = and(X1,X2)
              
              and(X1,active(X2)) = X2 >= X2 = and(X1,X2)
              
              length(mark(X)) = 0 >= 0 = length(X)
              
              length(active(X)) = 0 >= 0 = length(X)
              
              s(mark(X)) = X >= X = s(X)
              
              s(active(X)) = X >= X = s(X)
             problem:
              DPs:
               mark#(s(X)) -> mark#(X)
               active#(length(cons(N,L))) -> mark#(s(length(L)))
               mark#(length(X)) -> active#(length(mark(X)))
              TRS:
               active(zeros()) -> mark(cons(0(),zeros()))
               active(and(tt(),X)) -> mark(X)
               active(length(nil())) -> mark(0())
               active(length(cons(N,L))) -> mark(s(length(L)))
               mark(zeros()) -> active(zeros())
               mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
               mark(0()) -> active(0())
               mark(and(X1,X2)) -> active(and(mark(X1),X2))
               mark(tt()) -> active(tt())
               mark(length(X)) -> active(length(mark(X)))
               mark(nil()) -> active(nil())
               mark(s(X)) -> active(s(mark(X)))
               cons(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)
               and(mark(X1),X2) -> and(X1,X2)
               and(X1,mark(X2)) -> and(X1,X2)
               and(active(X1),X2) -> and(X1,X2)
               and(X1,active(X2)) -> and(X1,X2)
               length(mark(X)) -> length(X)
               length(active(X)) -> length(X)
               s(mark(X)) -> s(X)
               s(active(X)) -> s(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(and(tt(),X)) -> mark(X)
     active(length(nil())) -> mark(0())
     active(length(cons(N,L))) -> mark(s(length(L)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(0()) -> active(0())
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(tt()) -> active(tt())
     mark(length(X)) -> active(length(mark(X)))
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(mark(X)))
     cons(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)
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(X1,X2)
     length(mark(X)) -> length(X)
     length(active(X)) -> length(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [cons#](x0, x1) = x0 + x1 + 1,
      
      [s](x0) = 0,
      
      [length](x0) = 1,
      
      [nil] = 0,
      
      [and](x0, x1) = x0 + x1 + 1,
      
      [tt] = 1,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 0,
      
      [0] = 0,
      
      [active](x0) = x0,
      
      [zeros] = 1
     orientation:
      cons#(mark(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = cons#(X1,X2)
      
      cons#(X1,mark(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = cons#(X1,X2)
      
      cons#(active(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = cons#(X1,X2)
      
      cons#(X1,active(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = cons#(X1,X2)
      
      active(zeros()) = 1 >= 1 = mark(cons(0(),zeros()))
      
      active(and(tt(),X)) = X + 2 >= X + 1 = mark(X)
      
      active(length(nil())) = 1 >= 1 = mark(0())
      
      active(length(cons(N,L))) = 1 >= 1 = mark(s(length(L)))
      
      mark(zeros()) = 2 >= 1 = active(zeros())
      
      mark(cons(X1,X2)) = 1 >= 0 = active(cons(mark(X1),X2))
      
      mark(0()) = 1 >= 0 = active(0())
      
      mark(and(X1,X2)) = X1 + X2 + 2 >= X1 + X2 + 2 = active(and(mark(X1),X2))
      
      mark(tt()) = 2 >= 1 = active(tt())
      
      mark(length(X)) = 2 >= 1 = active(length(mark(X)))
      
      mark(nil()) = 1 >= 0 = active(nil())
      
      mark(s(X)) = 1 >= 0 = active(s(mark(X)))
      
      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)
      
      and(mark(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = and(X1,X2)
      
      and(X1,mark(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = and(X1,X2)
      
      and(active(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = and(X1,X2)
      
      and(X1,active(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = and(X1,X2)
      
      length(mark(X)) = 1 >= 1 = length(X)
      
      length(active(X)) = 1 >= 1 = length(X)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
     problem:
      DPs:
       cons#(active(X1),X2) -> cons#(X1,X2)
       cons#(X1,active(X2)) -> cons#(X1,X2)
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(and(tt(),X)) -> mark(X)
       active(length(nil())) -> mark(0())
       active(length(cons(N,L))) -> mark(s(length(L)))
       mark(zeros()) -> active(zeros())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(0()) -> active(0())
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(tt()) -> active(tt())
       mark(length(X)) -> active(length(mark(X)))
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(mark(X)))
       cons(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)
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(X1,X2)
       length(mark(X)) -> length(X)
       length(active(X)) -> length(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [cons#](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = 0,
       
       [length](x0) = 0,
       
       [nil] = 0,
       
       [and](x0, x1) = 0,
       
       [tt] = 0,
       
       [mark](x0) = 1,
       
       [cons](x0, x1) = 0,
       
       [0] = 0,
       
       [active](x0) = x0 + 1,
       
       [zeros] = 0
      orientation:
       cons#(active(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = cons#(X1,X2)
       
       cons#(X1,active(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = cons#(X1,X2)
       
       active(zeros()) = 1 >= 1 = mark(cons(0(),zeros()))
       
       active(and(tt(),X)) = 1 >= 1 = mark(X)
       
       active(length(nil())) = 1 >= 1 = mark(0())
       
       active(length(cons(N,L))) = 1 >= 1 = mark(s(length(L)))
       
       mark(zeros()) = 1 >= 1 = active(zeros())
       
       mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2))
       
       mark(0()) = 1 >= 1 = active(0())
       
       mark(and(X1,X2)) = 1 >= 1 = active(and(mark(X1),X2))
       
       mark(tt()) = 1 >= 1 = active(tt())
       
       mark(length(X)) = 1 >= 1 = active(length(mark(X)))
       
       mark(nil()) = 1 >= 1 = active(nil())
       
       mark(s(X)) = 1 >= 1 = active(s(mark(X)))
       
       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)
       
       and(mark(X1),X2) = 0 >= 0 = and(X1,X2)
       
       and(X1,mark(X2)) = 0 >= 0 = and(X1,X2)
       
       and(active(X1),X2) = 0 >= 0 = and(X1,X2)
       
       and(X1,active(X2)) = 0 >= 0 = and(X1,X2)
       
       length(mark(X)) = 0 >= 0 = length(X)
       
       length(active(X)) = 0 >= 0 = length(X)
       
       s(mark(X)) = 0 >= 0 = s(X)
       
       s(active(X)) = 0 >= 0 = s(X)
      problem:
       DPs:
        
       TRS:
        active(zeros()) -> mark(cons(0(),zeros()))
        active(and(tt(),X)) -> mark(X)
        active(length(nil())) -> mark(0())
        active(length(cons(N,L))) -> mark(s(length(L)))
        mark(zeros()) -> active(zeros())
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(0()) -> active(0())
        mark(and(X1,X2)) -> active(and(mark(X1),X2))
        mark(tt()) -> active(tt())
        mark(length(X)) -> active(length(mark(X)))
        mark(nil()) -> active(nil())
        mark(s(X)) -> active(s(mark(X)))
        cons(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)
        and(mark(X1),X2) -> and(X1,X2)
        and(X1,mark(X2)) -> and(X1,X2)
        and(active(X1),X2) -> and(X1,X2)
        and(X1,active(X2)) -> and(X1,X2)
        length(mark(X)) -> length(X)
        length(active(X)) -> length(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
      Qed
    
    DPs:
     length#(mark(X)) -> length#(X)
     length#(active(X)) -> length#(X)
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(and(tt(),X)) -> mark(X)
     active(length(nil())) -> mark(0())
     active(length(cons(N,L))) -> mark(s(length(L)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(0()) -> active(0())
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(tt()) -> active(tt())
     mark(length(X)) -> active(length(mark(X)))
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(mark(X)))
     cons(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)
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(X1,X2)
     length(mark(X)) -> length(X)
     length(active(X)) -> length(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [length#](x0) = x0 + 1,
      
      [s](x0) = 1,
      
      [length](x0) = 1,
      
      [nil] = 0,
      
      [and](x0, x1) = x1,
      
      [tt] = 0,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 0,
      
      [0] = 1,
      
      [active](x0) = x0 + 1,
      
      [zeros] = 0
     orientation:
      length#(mark(X)) = X + 2 >= X + 1 = length#(X)
      
      length#(active(X)) = X + 2 >= X + 1 = length#(X)
      
      active(zeros()) = 1 >= 1 = mark(cons(0(),zeros()))
      
      active(and(tt(),X)) = X + 1 >= X + 1 = mark(X)
      
      active(length(nil())) = 2 >= 2 = mark(0())
      
      active(length(cons(N,L))) = 2 >= 2 = mark(s(length(L)))
      
      mark(zeros()) = 1 >= 1 = active(zeros())
      
      mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2))
      
      mark(0()) = 2 >= 2 = active(0())
      
      mark(and(X1,X2)) = X2 + 1 >= X2 + 1 = active(and(mark(X1),X2))
      
      mark(tt()) = 1 >= 1 = active(tt())
      
      mark(length(X)) = 2 >= 2 = active(length(mark(X)))
      
      mark(nil()) = 1 >= 1 = active(nil())
      
      mark(s(X)) = 2 >= 2 = active(s(mark(X)))
      
      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)
      
      and(mark(X1),X2) = X2 >= X2 = and(X1,X2)
      
      and(X1,mark(X2)) = X2 + 1 >= X2 = and(X1,X2)
      
      and(active(X1),X2) = X2 >= X2 = and(X1,X2)
      
      and(X1,active(X2)) = X2 + 1 >= X2 = and(X1,X2)
      
      length(mark(X)) = 1 >= 1 = length(X)
      
      length(active(X)) = 1 >= 1 = length(X)
      
      s(mark(X)) = 1 >= 1 = s(X)
      
      s(active(X)) = 1 >= 1 = s(X)
     problem:
      DPs:
       
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(and(tt(),X)) -> mark(X)
       active(length(nil())) -> mark(0())
       active(length(cons(N,L))) -> mark(s(length(L)))
       mark(zeros()) -> active(zeros())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(0()) -> active(0())
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(tt()) -> active(tt())
       mark(length(X)) -> active(length(mark(X)))
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(mark(X)))
       cons(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)
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(X1,X2)
       length(mark(X)) -> length(X)
       length(active(X)) -> length(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
     Qed
    
    DPs:
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(and(tt(),X)) -> mark(X)
     active(length(nil())) -> mark(0())
     active(length(cons(N,L))) -> mark(s(length(L)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(0()) -> active(0())
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(tt()) -> active(tt())
     mark(length(X)) -> active(length(mark(X)))
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(mark(X)))
     cons(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)
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(X1,X2)
     length(mark(X)) -> length(X)
     length(active(X)) -> length(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [s#](x0) = x0 + 1,
      
      [s](x0) = 1,
      
      [length](x0) = 1,
      
      [nil] = 0,
      
      [and](x0, x1) = x1,
      
      [tt] = 0,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 0,
      
      [0] = 1,
      
      [active](x0) = x0 + 1,
      
      [zeros] = 0
     orientation:
      s#(mark(X)) = X + 2 >= X + 1 = s#(X)
      
      s#(active(X)) = X + 2 >= X + 1 = s#(X)
      
      active(zeros()) = 1 >= 1 = mark(cons(0(),zeros()))
      
      active(and(tt(),X)) = X + 1 >= X + 1 = mark(X)
      
      active(length(nil())) = 2 >= 2 = mark(0())
      
      active(length(cons(N,L))) = 2 >= 2 = mark(s(length(L)))
      
      mark(zeros()) = 1 >= 1 = active(zeros())
      
      mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2))
      
      mark(0()) = 2 >= 2 = active(0())
      
      mark(and(X1,X2)) = X2 + 1 >= X2 + 1 = active(and(mark(X1),X2))
      
      mark(tt()) = 1 >= 1 = active(tt())
      
      mark(length(X)) = 2 >= 2 = active(length(mark(X)))
      
      mark(nil()) = 1 >= 1 = active(nil())
      
      mark(s(X)) = 2 >= 2 = active(s(mark(X)))
      
      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)
      
      and(mark(X1),X2) = X2 >= X2 = and(X1,X2)
      
      and(X1,mark(X2)) = X2 + 1 >= X2 = and(X1,X2)
      
      and(active(X1),X2) = X2 >= X2 = and(X1,X2)
      
      and(X1,active(X2)) = X2 + 1 >= X2 = and(X1,X2)
      
      length(mark(X)) = 1 >= 1 = length(X)
      
      length(active(X)) = 1 >= 1 = length(X)
      
      s(mark(X)) = 1 >= 1 = s(X)
      
      s(active(X)) = 1 >= 1 = s(X)
     problem:
      DPs:
       
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(and(tt(),X)) -> mark(X)
       active(length(nil())) -> mark(0())
       active(length(cons(N,L))) -> mark(s(length(L)))
       mark(zeros()) -> active(zeros())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(0()) -> active(0())
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(tt()) -> active(tt())
       mark(length(X)) -> active(length(mark(X)))
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(mark(X)))
       cons(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)
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(X1,X2)
       length(mark(X)) -> length(X)
       length(active(X)) -> length(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
     Qed
    
    DPs:
     and#(mark(X1),X2) -> and#(X1,X2)
     and#(X1,mark(X2)) -> and#(X1,X2)
     and#(active(X1),X2) -> and#(X1,X2)
     and#(X1,active(X2)) -> and#(X1,X2)
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(and(tt(),X)) -> mark(X)
     active(length(nil())) -> mark(0())
     active(length(cons(N,L))) -> mark(s(length(L)))
     mark(zeros()) -> active(zeros())
     mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
     mark(0()) -> active(0())
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(tt()) -> active(tt())
     mark(length(X)) -> active(length(mark(X)))
     mark(nil()) -> active(nil())
     mark(s(X)) -> active(s(mark(X)))
     cons(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)
     and(mark(X1),X2) -> and(X1,X2)
     and(X1,mark(X2)) -> and(X1,X2)
     and(active(X1),X2) -> and(X1,X2)
     and(X1,active(X2)) -> and(X1,X2)
     length(mark(X)) -> length(X)
     length(active(X)) -> length(X)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
    Matrix Interpretation Processor:
     dimension: 1
     interpretation:
      [and#](x0, x1) = x0 + x1 + 1,
      
      [s](x0) = 0,
      
      [length](x0) = 1,
      
      [nil] = 0,
      
      [and](x0, x1) = x0 + x1 + 1,
      
      [tt] = 1,
      
      [mark](x0) = x0 + 1,
      
      [cons](x0, x1) = 0,
      
      [0] = 0,
      
      [active](x0) = x0,
      
      [zeros] = 1
     orientation:
      and#(mark(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = and#(X1,X2)
      
      and#(X1,mark(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = and#(X1,X2)
      
      and#(active(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = and#(X1,X2)
      
      and#(X1,active(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = and#(X1,X2)
      
      active(zeros()) = 1 >= 1 = mark(cons(0(),zeros()))
      
      active(and(tt(),X)) = X + 2 >= X + 1 = mark(X)
      
      active(length(nil())) = 1 >= 1 = mark(0())
      
      active(length(cons(N,L))) = 1 >= 1 = mark(s(length(L)))
      
      mark(zeros()) = 2 >= 1 = active(zeros())
      
      mark(cons(X1,X2)) = 1 >= 0 = active(cons(mark(X1),X2))
      
      mark(0()) = 1 >= 0 = active(0())
      
      mark(and(X1,X2)) = X1 + X2 + 2 >= X1 + X2 + 2 = active(and(mark(X1),X2))
      
      mark(tt()) = 2 >= 1 = active(tt())
      
      mark(length(X)) = 2 >= 1 = active(length(mark(X)))
      
      mark(nil()) = 1 >= 0 = active(nil())
      
      mark(s(X)) = 1 >= 0 = active(s(mark(X)))
      
      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)
      
      and(mark(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = and(X1,X2)
      
      and(X1,mark(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = and(X1,X2)
      
      and(active(X1),X2) = X1 + X2 + 1 >= X1 + X2 + 1 = and(X1,X2)
      
      and(X1,active(X2)) = X1 + X2 + 1 >= X1 + X2 + 1 = and(X1,X2)
      
      length(mark(X)) = 1 >= 1 = length(X)
      
      length(active(X)) = 1 >= 1 = length(X)
      
      s(mark(X)) = 0 >= 0 = s(X)
      
      s(active(X)) = 0 >= 0 = s(X)
     problem:
      DPs:
       and#(active(X1),X2) -> and#(X1,X2)
       and#(X1,active(X2)) -> and#(X1,X2)
      TRS:
       active(zeros()) -> mark(cons(0(),zeros()))
       active(and(tt(),X)) -> mark(X)
       active(length(nil())) -> mark(0())
       active(length(cons(N,L))) -> mark(s(length(L)))
       mark(zeros()) -> active(zeros())
       mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
       mark(0()) -> active(0())
       mark(and(X1,X2)) -> active(and(mark(X1),X2))
       mark(tt()) -> active(tt())
       mark(length(X)) -> active(length(mark(X)))
       mark(nil()) -> active(nil())
       mark(s(X)) -> active(s(mark(X)))
       cons(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)
       and(mark(X1),X2) -> and(X1,X2)
       and(X1,mark(X2)) -> and(X1,X2)
       and(active(X1),X2) -> and(X1,X2)
       and(X1,active(X2)) -> and(X1,X2)
       length(mark(X)) -> length(X)
       length(active(X)) -> length(X)
       s(mark(X)) -> s(X)
       s(active(X)) -> s(X)
     Matrix Interpretation Processor:
      dimension: 1
      interpretation:
       [and#](x0, x1) = x0 + x1 + 1,
       
       [s](x0) = 0,
       
       [length](x0) = 0,
       
       [nil] = 0,
       
       [and](x0, x1) = 0,
       
       [tt] = 0,
       
       [mark](x0) = 1,
       
       [cons](x0, x1) = 0,
       
       [0] = 0,
       
       [active](x0) = x0 + 1,
       
       [zeros] = 0
      orientation:
       and#(active(X1),X2) = X1 + X2 + 2 >= X1 + X2 + 1 = and#(X1,X2)
       
       and#(X1,active(X2)) = X1 + X2 + 2 >= X1 + X2 + 1 = and#(X1,X2)
       
       active(zeros()) = 1 >= 1 = mark(cons(0(),zeros()))
       
       active(and(tt(),X)) = 1 >= 1 = mark(X)
       
       active(length(nil())) = 1 >= 1 = mark(0())
       
       active(length(cons(N,L))) = 1 >= 1 = mark(s(length(L)))
       
       mark(zeros()) = 1 >= 1 = active(zeros())
       
       mark(cons(X1,X2)) = 1 >= 1 = active(cons(mark(X1),X2))
       
       mark(0()) = 1 >= 1 = active(0())
       
       mark(and(X1,X2)) = 1 >= 1 = active(and(mark(X1),X2))
       
       mark(tt()) = 1 >= 1 = active(tt())
       
       mark(length(X)) = 1 >= 1 = active(length(mark(X)))
       
       mark(nil()) = 1 >= 1 = active(nil())
       
       mark(s(X)) = 1 >= 1 = active(s(mark(X)))
       
       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)
       
       and(mark(X1),X2) = 0 >= 0 = and(X1,X2)
       
       and(X1,mark(X2)) = 0 >= 0 = and(X1,X2)
       
       and(active(X1),X2) = 0 >= 0 = and(X1,X2)
       
       and(X1,active(X2)) = 0 >= 0 = and(X1,X2)
       
       length(mark(X)) = 0 >= 0 = length(X)
       
       length(active(X)) = 0 >= 0 = length(X)
       
       s(mark(X)) = 0 >= 0 = s(X)
       
       s(active(X)) = 0 >= 0 = s(X)
      problem:
       DPs:
        
       TRS:
        active(zeros()) -> mark(cons(0(),zeros()))
        active(and(tt(),X)) -> mark(X)
        active(length(nil())) -> mark(0())
        active(length(cons(N,L))) -> mark(s(length(L)))
        mark(zeros()) -> active(zeros())
        mark(cons(X1,X2)) -> active(cons(mark(X1),X2))
        mark(0()) -> active(0())
        mark(and(X1,X2)) -> active(and(mark(X1),X2))
        mark(tt()) -> active(tt())
        mark(length(X)) -> active(length(mark(X)))
        mark(nil()) -> active(nil())
        mark(s(X)) -> active(s(mark(X)))
        cons(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)
        and(mark(X1),X2) -> and(X1,X2)
        and(X1,mark(X2)) -> and(X1,X2)
        and(active(X1),X2) -> and(X1,X2)
        and(X1,active(X2)) -> and(X1,X2)
        length(mark(X)) -> length(X)
        length(active(X)) -> length(X)
        s(mark(X)) -> s(X)
        s(active(X)) -> s(X)
      Qed