MAYBE

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

Proof:
 DP Processor:
  DPs:
   active#(zeros()) -> cons#(0(),zeros())
   active#(zeros()) -> mark#(cons(0(),zeros()))
   active#(U11(tt(),L)) -> length#(L)
   active#(U11(tt(),L)) -> s#(length(L))
   active#(U11(tt(),L)) -> mark#(s(length(L)))
   active#(and(tt(),X)) -> mark#(X)
   active#(isNat(0())) -> mark#(tt())
   active#(isNat(length(V1))) -> isNatList#(V1)
   active#(isNat(length(V1))) -> mark#(isNatList(V1))
   active#(isNat(s(V1))) -> isNat#(V1)
   active#(isNat(s(V1))) -> mark#(isNat(V1))
   active#(isNatIList(V)) -> isNatList#(V)
   active#(isNatIList(V)) -> mark#(isNatList(V))
   active#(isNatIList(zeros())) -> mark#(tt())
   active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
   active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
   active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
   active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
   active#(isNatList(nil())) -> mark#(tt())
   active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
   active#(isNatList(cons(V1,V2))) -> isNat#(V1)
   active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
   active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
   active#(length(nil())) -> mark#(0())
   active#(length(cons(N,L))) -> isNat#(N)
   active#(length(cons(N,L))) -> isNatList#(L)
   active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
   active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
   active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),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#(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#(and(X1,X2)) -> mark#(X1)
   mark#(and(X1,X2)) -> and#(mark(X1),X2)
   mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
   mark#(isNat(X)) -> active#(isNat(X))
   mark#(isNatList(X)) -> active#(isNatList(X))
   mark#(isNatIList(X)) -> active#(isNatIList(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)
   s#(mark(X)) -> s#(X)
   s#(active(X)) -> s#(X)
   length#(mark(X)) -> length#(X)
   length#(active(X)) -> length#(X)
   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)
   isNat#(mark(X)) -> isNat#(X)
   isNat#(active(X)) -> isNat#(X)
   isNatList#(mark(X)) -> isNatList#(X)
   isNatList#(active(X)) -> isNatList#(X)
   isNatIList#(mark(X)) -> isNatIList#(X)
   isNatIList#(active(X)) -> isNatIList#(X)
  TRS:
   active(zeros()) -> mark(cons(0(),zeros()))
   active(U11(tt(),L)) -> mark(s(length(L)))
   active(and(tt(),X)) -> mark(X)
   active(isNat(0())) -> mark(tt())
   active(isNat(length(V1))) -> mark(isNatList(V1))
   active(isNat(s(V1))) -> mark(isNat(V1))
   active(isNatIList(V)) -> mark(isNatList(V))
   active(isNatIList(zeros())) -> mark(tt())
   active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
   active(isNatList(nil())) -> mark(tt())
   active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
   active(length(nil())) -> mark(0())
   active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
   mark(length(X)) -> active(length(mark(X)))
   mark(and(X1,X2)) -> active(and(mark(X1),X2))
   mark(isNat(X)) -> active(isNat(X))
   mark(isNatList(X)) -> active(isNatList(X))
   mark(isNatIList(X)) -> active(isNatIList(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)
   s(mark(X)) -> s(X)
   s(active(X)) -> s(X)
   length(mark(X)) -> length(X)
   length(active(X)) -> length(X)
   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)
   isNat(mark(X)) -> isNat(X)
   isNat(active(X)) -> isNat(X)
   isNatList(mark(X)) -> isNatList(X)
   isNatList(active(X)) -> isNatList(X)
   isNatIList(mark(X)) -> isNatIList(X)
   isNatIList(active(X)) -> isNatIList(X)
  TDG Processor:
   DPs:
    active#(zeros()) -> cons#(0(),zeros())
    active#(zeros()) -> mark#(cons(0(),zeros()))
    active#(U11(tt(),L)) -> length#(L)
    active#(U11(tt(),L)) -> s#(length(L))
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    active#(and(tt(),X)) -> mark#(X)
    active#(isNat(0())) -> mark#(tt())
    active#(isNat(length(V1))) -> isNatList#(V1)
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    active#(isNat(s(V1))) -> isNat#(V1)
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    active#(isNatIList(V)) -> isNatList#(V)
    active#(isNatIList(V)) -> mark#(isNatList(V))
    active#(isNatIList(zeros())) -> mark#(tt())
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    active#(isNatList(nil())) -> mark#(tt())
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    active#(length(nil())) -> mark#(0())
    active#(length(cons(N,L))) -> isNat#(N)
    active#(length(cons(N,L))) -> isNatList#(L)
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),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#(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#(and(X1,X2)) -> mark#(X1)
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(isNat(X)) -> active#(isNat(X))
    mark#(isNatList(X)) -> active#(isNatList(X))
    mark#(isNatIList(X)) -> active#(isNatIList(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)
    s#(mark(X)) -> s#(X)
    s#(active(X)) -> s#(X)
    length#(mark(X)) -> length#(X)
    length#(active(X)) -> length#(X)
    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)
    isNat#(mark(X)) -> isNat#(X)
    isNat#(active(X)) -> isNat#(X)
    isNatList#(mark(X)) -> isNatList#(X)
    isNatList#(active(X)) -> isNatList#(X)
    isNatIList#(mark(X)) -> isNatIList#(X)
    isNatIList#(active(X)) -> isNatIList#(X)
   TRS:
    active(zeros()) -> mark(cons(0(),zeros()))
    active(U11(tt(),L)) -> mark(s(length(L)))
    active(and(tt(),X)) -> mark(X)
    active(isNat(0())) -> mark(tt())
    active(isNat(length(V1))) -> mark(isNatList(V1))
    active(isNat(s(V1))) -> mark(isNat(V1))
    active(isNatIList(V)) -> mark(isNatList(V))
    active(isNatIList(zeros())) -> mark(tt())
    active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
    active(isNatList(nil())) -> mark(tt())
    active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
    active(length(nil())) -> mark(0())
    active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
    mark(length(X)) -> active(length(mark(X)))
    mark(and(X1,X2)) -> active(and(mark(X1),X2))
    mark(isNat(X)) -> active(isNat(X))
    mark(isNatList(X)) -> active(isNatList(X))
    mark(isNatIList(X)) -> active(isNatIList(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)
    s(mark(X)) -> s(X)
    s(active(X)) -> s(X)
    length(mark(X)) -> length(X)
    length(active(X)) -> length(X)
    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)
    isNat(mark(X)) -> isNat(X)
    isNat(active(X)) -> isNat(X)
    isNatList(mark(X)) -> isNatList(X)
    isNatList(active(X)) -> isNatList(X)
    isNatIList(mark(X)) -> isNatIList(X)
    isNatIList(active(X)) -> isNatIList(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)
    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)
    isNatIList#(mark(X)) -> isNatIList#(X) ->
    isNatIList#(active(X)) -> isNatIList#(X)
    isNatIList#(mark(X)) -> isNatIList#(X) ->
    isNatIList#(mark(X)) -> isNatIList#(X)
    isNatIList#(active(X)) -> isNatIList#(X) ->
    isNatIList#(active(X)) -> isNatIList#(X)
    isNatIList#(active(X)) -> isNatIList#(X) ->
    isNatIList#(mark(X)) -> isNatIList#(X)
    isNat#(mark(X)) -> isNat#(X) -> isNat#(active(X)) -> isNat#(X)
    isNat#(mark(X)) -> isNat#(X) -> isNat#(mark(X)) -> isNat#(X)
    isNat#(active(X)) -> isNat#(X) -> isNat#(active(X)) -> isNat#(X)
    isNat#(active(X)) -> isNat#(X) ->
    isNat#(mark(X)) -> isNat#(X)
    isNatList#(mark(X)) -> isNatList#(X) ->
    isNatList#(active(X)) -> isNatList#(X)
    isNatList#(mark(X)) -> isNatList#(X) ->
    isNatList#(mark(X)) -> isNatList#(X)
    isNatList#(active(X)) -> isNatList#(X) ->
    isNatList#(active(X)) -> isNatList#(X)
    isNatList#(active(X)) -> isNatList#(X) ->
    isNatList#(mark(X)) -> isNatList#(X)
    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#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L))
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(nil()) -> active#(nil()) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(nil()) -> active#(nil()) ->
    active#(length(nil())) -> mark#(0())
    mark#(nil()) -> active#(nil()) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(nil()) -> active#(nil()) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(nil()) -> active#(nil()) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(nil()) -> active#(nil()) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(nil()) -> active#(nil()) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(nil()) -> active#(nil()) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(nil()) -> active#(nil()) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(nil()) -> active#(nil()) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(nil()) -> active#(nil()) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(nil()) -> active#(nil()) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(nil()) -> active#(nil()) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(nil()) -> active#(nil()) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(nil()) -> active#(nil()) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(nil()) -> active#(nil()) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(nil()) -> active#(nil()) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(nil()) -> active#(nil()) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(nil()) -> active#(nil()) ->
    active#(isNat(0())) -> mark#(tt())
    mark#(nil()) -> active#(nil()) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(nil()) -> active#(nil()) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(nil()) -> active#(nil()) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(nil()) -> active#(nil()) ->
    active#(U11(tt(),L)) -> length#(L)
    mark#(nil()) -> active#(nil()) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(nil()) -> active#(nil()) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(length(nil())) -> mark#(0())
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(isNat(0())) -> mark#(tt())
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(U11(tt(),L)) -> length#(L)
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(isNatIList(X)) -> active#(isNatIList(X)) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(length(nil())) -> mark#(0())
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(isNat(0())) -> mark#(tt())
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(U11(tt(),L)) -> length#(L)
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(isNatList(X)) -> active#(isNatList(X)) ->
    active#(zeros()) -> cons#(0(),zeros())
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(length(nil())) -> mark#(0())
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(isNat(0())) -> mark#(tt())
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(U11(tt(),L)) -> length#(L)
    mark#(isNat(X)) -> active#(isNat(X)) ->
    active#(zeros()) -> mark#(cons(0(),zeros()))
    mark#(isNat(X)) -> active#(isNat(X)) ->
    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#(nil()) -> active#(nil())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(isNat(X)) -> active#(isNat(X))
    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#(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#(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#(tt()) -> active#(tt())
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    mark#(and(X1,X2)) -> mark#(X1) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    mark#(and(X1,X2)) -> mark#(X1) -> mark#(U11(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#(U11(and(isNatList(L),isNat(N)),L))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(length(nil())) -> mark#(0())
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(isNat(0())) -> mark#(tt())
    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#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> length#(L)
    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#(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#(isNatIList(X)) -> active#(isNatIList(X))
    mark#(s(X)) -> mark#(X) -> mark#(isNatList(X)) -> active#(isNatList(X))
    mark#(s(X)) -> mark#(X) -> mark#(isNat(X)) -> active#(isNat(X))
    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#(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#(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(and(isNatList(L),isNat(N)),L))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(length(nil())) -> mark#(0())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(isNat(0())) -> mark#(tt())
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(s(X)) -> active#(s(mark(X))) ->
    active#(U11(tt(),L)) -> length#(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#(isNatIList(X)) -> active#(isNatIList(X))
    mark#(length(X)) -> mark#(X) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    mark#(length(X)) -> mark#(X) ->
    mark#(isNat(X)) -> active#(isNat(X))
    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#(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#(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(and(isNatList(L),isNat(N)),L))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(length(nil())) -> mark#(0())
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(isNat(0())) -> mark#(tt())
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(length(X)) -> active#(length(mark(X))) ->
    active#(U11(tt(),L)) -> length#(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#(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#(isNatIList(X)) -> active#(isNatIList(X))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(isNat(X)) -> active#(isNat(X))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    mark#(U11(X1,X2)) -> mark#(X1) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    mark#(U11(X1,X2)) -> mark#(X1) -> mark#(and(X1,X2)) -> mark#(X1)
    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#(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(and(isNatList(L),isNat(N)),L))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(length(nil())) -> mark#(0())
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(isNat(0())) -> mark#(tt())
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> length#(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(and(isNatList(L),isNat(N)),L))
    mark#(tt()) -> active#(tt()) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(tt()) -> active#(tt()) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(tt()) -> active#(tt()) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(tt()) -> active#(tt()) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(tt()) -> active#(tt()) ->
    active#(length(nil())) -> mark#(0())
    mark#(tt()) -> active#(tt()) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(tt()) -> active#(tt()) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(tt()) -> active#(tt()) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(tt()) -> active#(tt()) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(tt()) -> active#(tt()) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(tt()) -> active#(tt()) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(tt()) -> active#(tt()) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(tt()) -> active#(tt()) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(tt()) -> active#(tt()) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(tt()) -> active#(tt()) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(tt()) -> active#(tt()) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(tt()) -> active#(tt()) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(tt()) -> active#(tt()) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(tt()) -> active#(tt()) -> active#(isNat(s(V1))) -> isNat#(V1)
    mark#(tt()) -> active#(tt()) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(tt()) -> active#(tt()) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(tt()) -> active#(tt()) -> active#(isNat(0())) -> mark#(tt())
    mark#(tt()) -> active#(tt()) -> active#(and(tt(),X)) -> mark#(X)
    mark#(tt()) -> active#(tt()) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(tt()) -> active#(tt()) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(tt()) -> active#(tt()) -> active#(U11(tt(),L)) -> length#(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#(isNatIList(X)) -> active#(isNatIList(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    mark#(cons(X1,X2)) -> mark#(X1) ->
    mark#(isNat(X)) -> active#(isNat(X))
    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#(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#(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(and(isNatList(L),isNat(N)),L))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(length(nil())) -> mark#(0())
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(isNat(0())) -> mark#(tt())
    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#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2)) ->
    active#(U11(tt(),L)) -> length#(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(and(isNatList(L),isNat(N)),L))
    mark#(0()) -> active#(0()) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(0()) -> active#(0()) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(0()) -> active#(0()) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(0()) -> active#(0()) -> active#(length(cons(N,L))) -> isNat#(N)
    mark#(0()) -> active#(0()) -> active#(length(nil())) -> mark#(0())
    mark#(0()) -> active#(0()) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(0()) -> active#(0()) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(0()) -> active#(0()) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(0()) -> active#(0()) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(0()) -> active#(0()) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(0()) -> active#(0()) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(0()) -> active#(0()) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(0()) -> active#(0()) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(0()) -> active#(0()) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(0()) -> active#(0()) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(0()) -> active#(0()) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(0()) -> active#(0()) -> active#(isNatIList(V)) -> isNatList#(V)
    mark#(0()) -> active#(0()) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(0()) -> active#(0()) -> active#(isNat(s(V1))) -> isNat#(V1)
    mark#(0()) -> active#(0()) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(0()) -> active#(0()) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(0()) -> active#(0()) -> active#(isNat(0())) -> mark#(tt())
    mark#(0()) -> active#(0()) -> active#(and(tt(),X)) -> mark#(X)
    mark#(0()) -> active#(0()) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(0()) -> active#(0()) -> active#(U11(tt(),L)) -> s#(length(L))
    mark#(0()) -> active#(0()) -> active#(U11(tt(),L)) -> length#(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(and(isNatList(L),isNat(N)),L))
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(cons(N,L))) -> isNat#(N)
    mark#(zeros()) -> active#(zeros()) ->
    active#(length(nil())) -> mark#(0())
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatList(nil())) -> mark#(tt())
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatIList(zeros())) -> mark#(tt())
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatIList(V)) -> mark#(isNatList(V))
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNatIList(V)) -> isNatList#(V)
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNat(s(V1))) -> mark#(isNat(V1))
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNat(length(V1))) -> mark#(isNatList(V1))
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    mark#(zeros()) -> active#(zeros()) ->
    active#(isNat(0())) -> mark#(tt())
    mark#(zeros()) -> active#(zeros()) ->
    active#(and(tt(),X)) -> mark#(X)
    mark#(zeros()) -> active#(zeros()) ->
    active#(U11(tt(),L)) -> mark#(s(length(L)))
    mark#(zeros()) -> active#(zeros()) ->
    active#(U11(tt(),L)) -> s#(length(L))
    mark#(zeros()) -> active#(zeros()) ->
    active#(U11(tt(),L)) -> length#(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#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) ->
    and#(active(X1),X2) -> and#(X1,X2)
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) ->
    isNatIList#(active(X)) -> isNatIList#(X)
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) ->
    isNatIList#(mark(X)) -> isNatIList#(X)
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1) ->
    isNat#(active(X)) -> isNat#(X)
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1) ->
    isNat#(mark(X)) -> isNat#(X)
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(nil()) -> active#(nil())
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(length(X)) -> length#(mark(X))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(length(X)) -> mark#(X)
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(s(X)) -> mark#(X)
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(tt()) -> active#(tt())
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(0()) -> active#(0())
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2))) ->
    mark#(zeros()) -> active#(zeros())
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(nil()) -> active#(nil())
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(length(X)) -> length#(mark(X))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(length(X)) -> mark#(X)
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(s(X)) -> s#(mark(X))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(s(X)) -> mark#(X)
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(tt()) -> active#(tt())
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(0()) -> active#(0())
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(isNatIList(zeros())) -> mark#(tt()) ->
    mark#(zeros()) -> active#(zeros())
    active#(isNatIList(V)) -> isNatList#(V) ->
    isNatList#(active(X)) -> isNatList#(X)
    active#(isNatIList(V)) -> isNatList#(V) ->
    isNatList#(mark(X)) -> isNatList#(X)
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(nil()) -> active#(nil())
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(length(X)) -> length#(mark(X))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(length(X)) -> mark#(X)
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(s(X)) -> mark#(X)
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(tt()) -> active#(tt())
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(0()) -> active#(0())
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(isNatIList(V)) -> mark#(isNatList(V)) ->
    mark#(zeros()) -> active#(zeros())
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(nil()) -> active#(nil())
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(length(X)) -> length#(mark(X))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(length(X)) -> mark#(X)
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(s(X)) -> s#(mark(X))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(s(X)) -> mark#(X)
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(tt()) -> active#(tt())
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(0()) -> active#(0())
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(isNatList(nil())) -> mark#(tt()) ->
    mark#(zeros()) -> active#(zeros())
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) ->
    and#(active(X1),X2) -> and#(X1,X2)
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    active#(isNatList(cons(V1,V2))) -> isNat#(V1) ->
    isNat#(active(X)) -> isNat#(X)
    active#(isNatList(cons(V1,V2))) -> isNat#(V1) ->
    isNat#(mark(X)) -> isNat#(X)
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2) ->
    isNatList#(active(X)) -> isNatList#(X)
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2) ->
    isNatList#(mark(X)) -> isNatList#(X)
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(nil()) -> active#(nil())
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(length(X)) -> length#(mark(X))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(length(X)) -> mark#(X)
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(s(X)) -> mark#(X)
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(tt()) -> active#(tt())
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(0()) -> active#(0())
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2))) ->
    mark#(zeros()) -> active#(zeros())
    active#(isNat(s(V1))) -> isNat#(V1) ->
    isNat#(active(X)) -> isNat#(X)
    active#(isNat(s(V1))) -> isNat#(V1) ->
    isNat#(mark(X)) -> isNat#(X)
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(nil()) -> active#(nil())
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(length(X)) -> length#(mark(X))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(length(X)) -> mark#(X)
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(s(X)) -> mark#(X)
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(tt()) -> active#(tt())
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(0()) -> active#(0())
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(isNat(s(V1))) -> mark#(isNat(V1)) ->
    mark#(zeros()) -> active#(zeros())
    active#(isNat(length(V1))) -> isNatList#(V1) ->
    isNatList#(active(X)) -> isNatList#(X)
    active#(isNat(length(V1))) -> isNatList#(V1) ->
    isNatList#(mark(X)) -> isNatList#(X)
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(nil()) -> active#(nil())
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(length(X)) -> length#(mark(X))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(length(X)) -> mark#(X)
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(s(X)) -> mark#(X)
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(tt()) -> active#(tt())
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(0()) -> active#(0())
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(isNat(length(V1))) -> mark#(isNatList(V1)) ->
    mark#(zeros()) -> active#(zeros())
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(nil()) -> active#(nil())
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(length(X)) -> length#(mark(X))
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(length(X)) -> mark#(X)
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(s(X)) -> s#(mark(X))
    active#(isNat(0())) -> mark#(tt()) -> mark#(s(X)) -> mark#(X)
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(tt()) -> active#(tt())
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(0()) -> active#(0())
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(isNat(0())) -> mark#(tt()) ->
    mark#(zeros()) -> active#(zeros())
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(nil()) -> active#(nil())
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(isNat(X)) -> active#(isNat(X))
    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#(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#(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#(tt()) -> active#(tt())
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(and(tt(),X)) -> mark#(X) ->
    mark#(U11(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#(length(nil())) -> mark#(0()) ->
    mark#(nil()) -> active#(nil())
    active#(length(nil())) -> mark#(0()) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(length(nil())) -> mark#(0()) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(length(nil())) -> mark#(0()) ->
    mark#(isNat(X)) -> active#(isNat(X))
    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#(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#(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#(and(isNatList(L),isNat(N)),L) ->
    U11#(X1,active(X2)) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) ->
    U11#(active(X1),X2) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) ->
    U11#(X1,mark(X2)) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) ->
    and#(X1,active(X2)) -> and#(X1,X2)
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) ->
    and#(active(X1),X2) -> and#(X1,X2)
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) ->
    and#(X1,mark(X2)) -> and#(X1,X2)
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    active#(length(cons(N,L))) -> isNat#(N) ->
    isNat#(active(X)) -> isNat#(X)
    active#(length(cons(N,L))) -> isNat#(N) ->
    isNat#(mark(X)) -> isNat#(X)
    active#(length(cons(N,L))) -> isNatList#(L) ->
    isNatList#(active(X)) -> isNatList#(X)
    active#(length(cons(N,L))) -> isNatList#(L) ->
    isNatList#(mark(X)) -> isNatList#(X)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(nil()) -> active#(nil())
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(length(X)) -> length#(mark(X))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(length(X)) -> mark#(X)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(s(X)) -> s#(mark(X))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(s(X)) -> mark#(X)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(tt()) -> active#(tt())
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(0()) -> active#(0())
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L)) ->
    mark#(zeros()) -> active#(zeros())
    active#(U11(tt(),L)) -> s#(length(L)) ->
    s#(active(X)) -> s#(X)
    active#(U11(tt(),L)) -> s#(length(L)) -> s#(mark(X)) -> s#(X)
    active#(U11(tt(),L)) -> length#(L) ->
    length#(active(X)) -> length#(X)
    active#(U11(tt(),L)) -> length#(L) ->
    length#(mark(X)) -> length#(X)
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(nil()) -> active#(nil())
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(isNat(X)) -> active#(isNat(X))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(and(X1,X2)) -> and#(mark(X1),X2)
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(and(X1,X2)) -> mark#(X1)
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(length(X)) -> active#(length(mark(X)))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(length(X)) -> length#(mark(X))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(length(X)) -> mark#(X)
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(s(X)) -> active#(s(mark(X)))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(s(X)) -> s#(mark(X))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(s(X)) -> mark#(X)
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(tt()) -> active#(tt())
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(U11(X1,X2)) -> U11#(mark(X1),X2)
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(U11(X1,X2)) -> mark#(X1)
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(0()) -> active#(0())
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(cons(X1,X2)) -> active#(cons(mark(X1),X2))
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(cons(X1,X2)) -> cons#(mark(X1),X2)
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(cons(X1,X2)) -> mark#(X1)
    active#(U11(tt(),L)) -> mark#(s(length(L))) ->
    mark#(zeros()) -> active#(zeros())
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(nil()) -> active#(nil())
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(isNatIList(X)) -> active#(isNatIList(X))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(isNatList(X)) -> active#(isNatList(X))
    active#(zeros()) -> mark#(cons(0(),zeros())) ->
    mark#(isNat(X)) -> active#(isNat(X))
    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#(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#(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)
   Restore Modifier:
    DPs:
     active#(zeros()) -> cons#(0(),zeros())
     active#(zeros()) -> mark#(cons(0(),zeros()))
     active#(U11(tt(),L)) -> length#(L)
     active#(U11(tt(),L)) -> s#(length(L))
     active#(U11(tt(),L)) -> mark#(s(length(L)))
     active#(and(tt(),X)) -> mark#(X)
     active#(isNat(0())) -> mark#(tt())
     active#(isNat(length(V1))) -> isNatList#(V1)
     active#(isNat(length(V1))) -> mark#(isNatList(V1))
     active#(isNat(s(V1))) -> isNat#(V1)
     active#(isNat(s(V1))) -> mark#(isNat(V1))
     active#(isNatIList(V)) -> isNatList#(V)
     active#(isNatIList(V)) -> mark#(isNatList(V))
     active#(isNatIList(zeros())) -> mark#(tt())
     active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
     active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
     active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
     active#(isNatList(nil())) -> mark#(tt())
     active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
     active#(isNatList(cons(V1,V2))) -> isNat#(V1)
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
     active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
     active#(length(nil())) -> mark#(0())
     active#(length(cons(N,L))) -> isNat#(N)
     active#(length(cons(N,L))) -> isNatList#(L)
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
     active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),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#(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#(and(X1,X2)) -> mark#(X1)
     mark#(and(X1,X2)) -> and#(mark(X1),X2)
     mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
     mark#(isNat(X)) -> active#(isNat(X))
     mark#(isNatList(X)) -> active#(isNatList(X))
     mark#(isNatIList(X)) -> active#(isNatIList(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)
     s#(mark(X)) -> s#(X)
     s#(active(X)) -> s#(X)
     length#(mark(X)) -> length#(X)
     length#(active(X)) -> length#(X)
     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)
     isNat#(mark(X)) -> isNat#(X)
     isNat#(active(X)) -> isNat#(X)
     isNatList#(mark(X)) -> isNatList#(X)
     isNatList#(active(X)) -> isNatList#(X)
     isNatIList#(mark(X)) -> isNatIList#(X)
     isNatIList#(active(X)) -> isNatIList#(X)
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(U11(tt(),L)) -> mark(s(length(L)))
     active(and(tt(),X)) -> mark(X)
     active(isNat(0())) -> mark(tt())
     active(isNat(length(V1))) -> mark(isNatList(V1))
     active(isNat(s(V1))) -> mark(isNat(V1))
     active(isNatIList(V)) -> mark(isNatList(V))
     active(isNatIList(zeros())) -> mark(tt())
     active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
     active(isNatList(nil())) -> mark(tt())
     active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
     active(length(nil())) -> mark(0())
     active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
     mark(length(X)) -> active(length(mark(X)))
     mark(and(X1,X2)) -> active(and(mark(X1),X2))
     mark(isNat(X)) -> active(isNat(X))
     mark(isNatList(X)) -> active(isNatList(X))
     mark(isNatIList(X)) -> active(isNatIList(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)
     s(mark(X)) -> s(X)
     s(active(X)) -> s(X)
     length(mark(X)) -> length(X)
     length(active(X)) -> length(X)
     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)
     isNat(mark(X)) -> isNat(X)
     isNat(active(X)) -> isNat(X)
     isNatList(mark(X)) -> isNatList(X)
     isNatList(active(X)) -> isNatList(X)
     isNatIList(mark(X)) -> isNatIList(X)
     isNatIList(active(X)) -> isNatIList(X)
    SCC Processor:
     #sccs: 9
     #rules: 52
     #arcs: 870/5329
     DPs:
      mark#(nil()) -> active#(nil())
      active#(zeros()) -> mark#(cons(0(),zeros()))
      mark#(zeros()) -> active#(zeros())
      active#(U11(tt(),L)) -> mark#(s(length(L)))
      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#(isNat(0())) -> mark#(tt())
      mark#(U11(X1,X2)) -> mark#(X1)
      mark#(U11(X1,X2)) -> active#(U11(mark(X1),X2))
      active#(isNat(length(V1))) -> mark#(isNatList(V1))
      mark#(tt()) -> active#(tt())
      active#(isNat(s(V1))) -> mark#(isNat(V1))
      mark#(s(X)) -> mark#(X)
      mark#(s(X)) -> active#(s(mark(X)))
      active#(isNatIList(V)) -> mark#(isNatList(V))
      mark#(length(X)) -> mark#(X)
      mark#(length(X)) -> active#(length(mark(X)))
      active#(isNatIList(zeros())) -> mark#(tt())
      mark#(and(X1,X2)) -> mark#(X1)
      mark#(and(X1,X2)) -> active#(and(mark(X1),X2))
      active#(isNatIList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatIList(V2)))
      mark#(isNat(X)) -> active#(isNat(X))
      active#(isNatList(nil())) -> mark#(tt())
      mark#(isNatList(X)) -> active#(isNatList(X))
      active#(isNatList(cons(V1,V2))) -> mark#(and(isNat(V1),isNatList(V2)))
      mark#(isNatIList(X)) -> active#(isNatIList(X))
      active#(length(nil())) -> mark#(0())
      active#(length(cons(N,L))) -> mark#(U11(and(isNatList(L),isNat(N)),L))
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(length(V1))) -> mark(isNatList(V1))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNatIList(V)) -> mark(isNatList(V))
      active(isNatIList(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      mark(isNatList(X)) -> active(isNatList(X))
      mark(isNatIList(X)) -> active(isNatIList(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
      isNatList(mark(X)) -> isNatList(X)
      isNatList(active(X)) -> isNatList(X)
      isNatIList(mark(X)) -> isNatIList(X)
      isNatIList(active(X)) -> isNatIList(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(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(length(V1))) -> mark(isNatList(V1))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNatIList(V)) -> mark(isNatList(V))
      active(isNatIList(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      mark(isNatList(X)) -> active(isNatList(X))
      mark(isNatIList(X)) -> active(isNatIList(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
      isNatList(mark(X)) -> isNatList(X)
      isNatList(active(X)) -> isNatList(X)
      isNatIList(mark(X)) -> isNatIList(X)
      isNatIList(active(X)) -> isNatIList(X)
     Open
     
     DPs:
      length#(mark(X)) -> length#(X)
      length#(active(X)) -> length#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(length(V1))) -> mark(isNatList(V1))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNatIList(V)) -> mark(isNatList(V))
      active(isNatIList(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      mark(isNatList(X)) -> active(isNatList(X))
      mark(isNatIList(X)) -> active(isNatIList(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
      isNatList(mark(X)) -> isNatList(X)
      isNatList(active(X)) -> isNatList(X)
      isNatIList(mark(X)) -> isNatIList(X)
      isNatIList(active(X)) -> isNatIList(X)
     Open
     
     DPs:
      s#(mark(X)) -> s#(X)
      s#(active(X)) -> s#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(length(V1))) -> mark(isNatList(V1))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNatIList(V)) -> mark(isNatList(V))
      active(isNatIList(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      mark(isNatList(X)) -> active(isNatList(X))
      mark(isNatIList(X)) -> active(isNatIList(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
      isNatList(mark(X)) -> isNatList(X)
      isNatList(active(X)) -> isNatList(X)
      isNatIList(mark(X)) -> isNatIList(X)
      isNatIList(active(X)) -> isNatIList(X)
     Open
     
     DPs:
      isNatList#(mark(X)) -> isNatList#(X)
      isNatList#(active(X)) -> isNatList#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(length(V1))) -> mark(isNatList(V1))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNatIList(V)) -> mark(isNatList(V))
      active(isNatIList(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      mark(isNatList(X)) -> active(isNatList(X))
      mark(isNatIList(X)) -> active(isNatIList(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
      isNatList(mark(X)) -> isNatList(X)
      isNatList(active(X)) -> isNatList(X)
      isNatIList(mark(X)) -> isNatIList(X)
      isNatIList(active(X)) -> isNatIList(X)
     Open
     
     DPs:
      isNat#(mark(X)) -> isNat#(X)
      isNat#(active(X)) -> isNat#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(length(V1))) -> mark(isNatList(V1))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNatIList(V)) -> mark(isNatList(V))
      active(isNatIList(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      mark(isNatList(X)) -> active(isNatList(X))
      mark(isNatIList(X)) -> active(isNatIList(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
      isNatList(mark(X)) -> isNatList(X)
      isNatList(active(X)) -> isNatList(X)
      isNatIList(mark(X)) -> isNatIList(X)
      isNatIList(active(X)) -> isNatIList(X)
     Open
     
     DPs:
      isNatIList#(mark(X)) -> isNatIList#(X)
      isNatIList#(active(X)) -> isNatIList#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(length(V1))) -> mark(isNatList(V1))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNatIList(V)) -> mark(isNatList(V))
      active(isNatIList(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      mark(isNatList(X)) -> active(isNatList(X))
      mark(isNatIList(X)) -> active(isNatIList(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
      isNatList(mark(X)) -> isNatList(X)
      isNatList(active(X)) -> isNatList(X)
      isNatIList(mark(X)) -> isNatIList(X)
      isNatIList(active(X)) -> isNatIList(X)
     Open
     
     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(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(length(V1))) -> mark(isNatList(V1))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNatIList(V)) -> mark(isNatList(V))
      active(isNatIList(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      mark(isNatList(X)) -> active(isNatList(X))
      mark(isNatIList(X)) -> active(isNatIList(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
      isNatList(mark(X)) -> isNatList(X)
      isNatList(active(X)) -> isNatList(X)
      isNatIList(mark(X)) -> isNatIList(X)
      isNatIList(active(X)) -> isNatIList(X)
     Open
     
     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(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      active(isNat(0())) -> mark(tt())
      active(isNat(length(V1))) -> mark(isNatList(V1))
      active(isNat(s(V1))) -> mark(isNat(V1))
      active(isNatIList(V)) -> mark(isNatList(V))
      active(isNatIList(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),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(s(X)) -> active(s(mark(X)))
      mark(length(X)) -> active(length(mark(X)))
      mark(and(X1,X2)) -> active(and(mark(X1),X2))
      mark(isNat(X)) -> active(isNat(X))
      mark(isNatList(X)) -> active(isNatList(X))
      mark(isNatIList(X)) -> active(isNatIList(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)
      s(mark(X)) -> s(X)
      s(active(X)) -> s(X)
      length(mark(X)) -> length(X)
      length(active(X)) -> length(X)
      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)
      isNat(mark(X)) -> isNat(X)
      isNat(active(X)) -> isNat(X)
      isNatList(mark(X)) -> isNatList(X)
      isNatList(active(X)) -> isNatList(X)
      isNatIList(mark(X)) -> isNatIList(X)
      isNatIList(active(X)) -> isNatIList(X)
     Open