YES
TRS:
 {            mark(tt()) -> tt(),
              mark(s(X)) -> s(mark(X)),
               mark(0()) -> 0(),
          mark(isNat(X)) -> a__isNat(X),
      mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
       mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
   mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
       mark(and(X1, X2)) -> a__and(mark(X1), X2),
          a__U11(X1, X2) -> U11(X1, X2),
         a__U11(tt(), N) -> mark(N),
        a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
         a__plus(N, 0()) -> a__U11(a__isNat(N), N),
         a__plus(X1, X2) -> plus(X1, X2),
      a__U21(X1, X2, X3) -> U21(X1, X2, X3),
      a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
          a__and(X1, X2) -> and(X1, X2),
         a__and(tt(), X) -> mark(X),
             a__isNat(X) -> isNat(X),
         a__isNat(s(V1)) -> a__isNat(V1),
           a__isNat(0()) -> tt(),
  a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
 DP:
  Strict:
   {            mark#(s(X)) -> mark#(X),
            mark#(isNat(X)) -> a__isNat#(X),
        mark#(plus(X1, X2)) -> mark#(X1),
        mark#(plus(X1, X2)) -> mark#(X2),
        mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
         mark#(U11(X1, X2)) -> mark#(X1),
         mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2),
     mark#(U21(X1, X2, X3)) -> mark#(X1),
     mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3),
         mark#(and(X1, X2)) -> mark#(X1),
         mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
           a__U11#(tt(), N) -> mark#(N),
          a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N),
          a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)),
          a__plus#(N, s(M)) -> a__isNat#(M),
           a__plus#(N, 0()) -> a__U11#(a__isNat(N), N),
           a__plus#(N, 0()) -> a__isNat#(N),
        a__U21#(tt(), M, N) -> mark#(N),
        a__U21#(tt(), M, N) -> mark#(M),
        a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)),
           a__and#(tt(), X) -> mark#(X),
           a__isNat#(s(V1)) -> a__isNat#(V1),
    a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)),
    a__isNat#(plus(V1, V2)) -> a__isNat#(V1)}
  Weak:
  {            mark(tt()) -> tt(),
               mark(s(X)) -> s(mark(X)),
                mark(0()) -> 0(),
           mark(isNat(X)) -> a__isNat(X),
       mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
        mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
    mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
        mark(and(X1, X2)) -> a__and(mark(X1), X2),
           a__U11(X1, X2) -> U11(X1, X2),
          a__U11(tt(), N) -> mark(N),
         a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
          a__plus(N, 0()) -> a__U11(a__isNat(N), N),
          a__plus(X1, X2) -> plus(X1, X2),
       a__U21(X1, X2, X3) -> U21(X1, X2, X3),
       a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
           a__and(X1, X2) -> and(X1, X2),
          a__and(tt(), X) -> mark(X),
              a__isNat(X) -> isNat(X),
          a__isNat(s(V1)) -> a__isNat(V1),
            a__isNat(0()) -> tt(),
   a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
  EDG:
   {
    (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
    (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
    (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1))
    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (mark#(s(X)) -> mark#(X), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
    (a__and#(tt(), X) -> mark#(X), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (a__and#(tt(), X) -> mark#(X), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (a__and#(tt(), X) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (a__and#(tt(), X) -> mark#(X), mark#(U11(X1, X2)) -> mark#(X1))
    (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2))
    (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1))
    (a__and#(tt(), X) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
    (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X))
    (a__plus#(N, 0()) -> a__U11#(a__isNat(N), N), a__U11#(tt(), N) -> mark#(N))
    (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
    (a__U11#(tt(), N) -> mark#(N), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (a__U11#(tt(), N) -> mark#(N), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (a__U11#(tt(), N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (a__U11#(tt(), N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1))
    (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2))
    (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1))
    (a__U11#(tt(), N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X))
    (a__U11#(tt(), N) -> mark#(N), mark#(s(X)) -> mark#(X))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X))
    (a__U21#(tt(), M, N) -> mark#(N), mark#(s(X)) -> mark#(X))
    (a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__and#(tt(), X) -> mark#(X))
    (a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__and#(tt(), X) -> mark#(X))
    (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)))
    (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> mark#(M))
    (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> mark#(N))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(U11(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X2))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
    (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N))
    (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)))
    (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__isNat#(M))
    (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, 0()) -> a__U11#(a__isNat(N), N))
    (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, 0()) -> a__isNat#(N))
    (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N))
    (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)))
    (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__isNat#(M))
    (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, 0()) -> a__U11#(a__isNat(N), N))
    (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, 0()) -> a__isNat#(N))
    (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(s(V1)) -> a__isNat#(V1))
    (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
    (a__plus#(N, 0()) -> a__isNat#(N), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(s(X)) -> mark#(X))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(isNat(X)) -> a__isNat#(X))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X1))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X2))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> mark#(X1))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2, X3)) -> mark#(X1))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> mark#(X1))
    (a__U21#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
    (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(s(V1)) -> a__isNat#(V1))
    (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
    (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
    (mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), a__U11#(tt(), N) -> mark#(N))
    (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(V1)) -> a__isNat#(V1))
    (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
    (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
    (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1))
    (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
    (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
    (mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), a__U21#(tt(), M, N) -> mark#(N))
    (mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), a__U21#(tt(), M, N) -> mark#(M))
    (mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)))
   }
   SCCS:
    Scc:
     {            mark#(s(X)) -> mark#(X),
              mark#(isNat(X)) -> a__isNat#(X),
          mark#(plus(X1, X2)) -> mark#(X1),
          mark#(plus(X1, X2)) -> mark#(X2),
          mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
           mark#(U11(X1, X2)) -> mark#(X1),
           mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2),
       mark#(U21(X1, X2, X3)) -> mark#(X1),
       mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3),
           mark#(and(X1, X2)) -> mark#(X1),
           mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
             a__U11#(tt(), N) -> mark#(N),
            a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N),
            a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)),
            a__plus#(N, s(M)) -> a__isNat#(M),
             a__plus#(N, 0()) -> a__U11#(a__isNat(N), N),
             a__plus#(N, 0()) -> a__isNat#(N),
          a__U21#(tt(), M, N) -> mark#(N),
          a__U21#(tt(), M, N) -> mark#(M),
          a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)),
             a__and#(tt(), X) -> mark#(X),
             a__isNat#(s(V1)) -> a__isNat#(V1),
      a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)),
      a__isNat#(plus(V1, V2)) -> a__isNat#(V1)}
    SCC:
     Strict:
      {            mark#(s(X)) -> mark#(X),
               mark#(isNat(X)) -> a__isNat#(X),
           mark#(plus(X1, X2)) -> mark#(X1),
           mark#(plus(X1, X2)) -> mark#(X2),
           mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
            mark#(U11(X1, X2)) -> mark#(X1),
            mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2),
        mark#(U21(X1, X2, X3)) -> mark#(X1),
        mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3),
            mark#(and(X1, X2)) -> mark#(X1),
            mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
              a__U11#(tt(), N) -> mark#(N),
             a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N),
             a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)),
             a__plus#(N, s(M)) -> a__isNat#(M),
              a__plus#(N, 0()) -> a__U11#(a__isNat(N), N),
              a__plus#(N, 0()) -> a__isNat#(N),
           a__U21#(tt(), M, N) -> mark#(N),
           a__U21#(tt(), M, N) -> mark#(M),
           a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)),
              a__and#(tt(), X) -> mark#(X),
              a__isNat#(s(V1)) -> a__isNat#(V1),
       a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)),
       a__isNat#(plus(V1, V2)) -> a__isNat#(V1)}
     Weak:
     {            mark(tt()) -> tt(),
                  mark(s(X)) -> s(mark(X)),
                   mark(0()) -> 0(),
              mark(isNat(X)) -> a__isNat(X),
          mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
           mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
       mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
           mark(and(X1, X2)) -> a__and(mark(X1), X2),
              a__U11(X1, X2) -> U11(X1, X2),
             a__U11(tt(), N) -> mark(N),
            a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
             a__plus(N, 0()) -> a__U11(a__isNat(N), N),
             a__plus(X1, X2) -> plus(X1, X2),
          a__U21(X1, X2, X3) -> U21(X1, X2, X3),
          a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
              a__and(X1, X2) -> and(X1, X2),
             a__and(tt(), X) -> mark(X),
                 a__isNat(X) -> isNat(X),
             a__isNat(s(V1)) -> a__isNat(V1),
               a__isNat(0()) -> tt(),
      a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
     POLY:
      Argument Filtering:
       pi(and) = [0,1], pi(U21) = [0,1,2], pi(U11) = [0,1], pi(plus) = [0,1], pi(isNat) = [], pi(0) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__and#) = 1, pi(a__and) = [0,1], pi(a__U21#) = [1,2], pi(a__U21) = [0,1,2], pi(a__plus#) = [0,1], pi(a__plus) = [0,1], pi(s) = 0, pi(tt) = [], pi(a__U11#) = 1, pi(a__U11) = [0,1], pi(mark#) = 0, pi(mark) = 0
      Usable Rules:
       {}
      Interpretation:
       [a__U21#](x0, x1) = x0 + x1,
       [a__plus#](x0, x1) = x0 + x1,
       [a__isNat#] = 0,
       [U21](x0, x1, x2) = x0 + x1 + x2,
       [and](x0, x1) = x0 + x1,
       [U11](x0, x1) = x0 + x1,
       [plus](x0, x1) = x0 + x1,
       [isNat] = 0,
       [0] = 1
      Strict:
       {            mark#(s(X)) -> mark#(X),
                mark#(isNat(X)) -> a__isNat#(X),
            mark#(plus(X1, X2)) -> mark#(X1),
            mark#(plus(X1, X2)) -> mark#(X2),
            mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
             mark#(U11(X1, X2)) -> mark#(X1),
             mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2),
         mark#(U21(X1, X2, X3)) -> mark#(X1),
         mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3),
             mark#(and(X1, X2)) -> mark#(X1),
             mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
               a__U11#(tt(), N) -> mark#(N),
              a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N),
              a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)),
              a__plus#(N, s(M)) -> a__isNat#(M),
            a__U21#(tt(), M, N) -> mark#(N),
            a__U21#(tt(), M, N) -> mark#(M),
            a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)),
               a__and#(tt(), X) -> mark#(X),
               a__isNat#(s(V1)) -> a__isNat#(V1),
        a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)),
        a__isNat#(plus(V1, V2)) -> a__isNat#(V1)}
      Weak:
       {            mark(tt()) -> tt(),
                    mark(s(X)) -> s(mark(X)),
                     mark(0()) -> 0(),
                mark(isNat(X)) -> a__isNat(X),
            mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
             mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
         mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
             mark(and(X1, X2)) -> a__and(mark(X1), X2),
                a__U11(X1, X2) -> U11(X1, X2),
               a__U11(tt(), N) -> mark(N),
              a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
               a__plus(N, 0()) -> a__U11(a__isNat(N), N),
               a__plus(X1, X2) -> plus(X1, X2),
            a__U21(X1, X2, X3) -> U21(X1, X2, X3),
            a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
                a__and(X1, X2) -> and(X1, X2),
               a__and(tt(), X) -> mark(X),
                   a__isNat(X) -> isNat(X),
               a__isNat(s(V1)) -> a__isNat(V1),
                 a__isNat(0()) -> tt(),
        a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
      EDG:
       {
        (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
        (a__U11#(tt(), N) -> mark#(N), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (a__U11#(tt(), N) -> mark#(N), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (a__U11#(tt(), N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (a__U11#(tt(), N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1))
        (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2))
        (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1))
        (a__U11#(tt(), N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X))
        (a__U11#(tt(), N) -> mark#(N), mark#(s(X)) -> mark#(X))
        (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
        (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
        (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(s(V1)) -> a__isNat#(V1))
        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(s(X)) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (mark#(s(X)) -> mark#(X), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (mark#(s(X)) -> mark#(X), mark#(U11(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(s(X)) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
        (a__and#(tt(), X) -> mark#(X), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (a__and#(tt(), X) -> mark#(X), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (a__and#(tt(), X) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (a__and#(tt(), X) -> mark#(X), mark#(U11(X1, X2)) -> mark#(X1))
        (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2))
        (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1))
        (a__and#(tt(), X) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
        (a__and#(tt(), X) -> mark#(X), mark#(s(X)) -> mark#(X))
        (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
        (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
        (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(U11(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(and(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), a__U11#(tt(), N) -> mark#(N))
        (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__isNat#(M))
        (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)))
        (mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N))
        (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__isNat#(M))
        (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)))
        (a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)), a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N))
        (mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)))
        (mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), a__U21#(tt(), M, N) -> mark#(M))
        (mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3), a__U21#(tt(), M, N) -> mark#(N))
        (a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__and#(tt(), X) -> mark#(X))
        (a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__and#(tt(), X) -> mark#(X))
        (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(U21(X1, X2, X3)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
        (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1))
        (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
        (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
        (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(V1)) -> a__isNat#(V1))
        (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
        (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(s(X)) -> mark#(X))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(isNat(X)) -> a__isNat#(X))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X1))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X2))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> mark#(X1))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> mark#(X1))
        (a__U21#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(s(X)) -> mark#(X))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2, X3)) -> mark#(X1))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
        (a__U21#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
        (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> mark#(N))
        (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> mark#(M))
        (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)))
       }
       SCCS:
        Scc:
         {            mark#(s(X)) -> mark#(X),
                  mark#(isNat(X)) -> a__isNat#(X),
              mark#(plus(X1, X2)) -> mark#(X1),
              mark#(plus(X1, X2)) -> mark#(X2),
              mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
               mark#(U11(X1, X2)) -> mark#(X1),
               mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2),
           mark#(U21(X1, X2, X3)) -> mark#(X1),
           mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3),
               mark#(and(X1, X2)) -> mark#(X1),
               mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                 a__U11#(tt(), N) -> mark#(N),
                a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N),
                a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)),
                a__plus#(N, s(M)) -> a__isNat#(M),
              a__U21#(tt(), M, N) -> mark#(N),
              a__U21#(tt(), M, N) -> mark#(M),
              a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)),
                 a__and#(tt(), X) -> mark#(X),
                 a__isNat#(s(V1)) -> a__isNat#(V1),
          a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)),
          a__isNat#(plus(V1, V2)) -> a__isNat#(V1)}
        SCC:
         Strict:
          {            mark#(s(X)) -> mark#(X),
                   mark#(isNat(X)) -> a__isNat#(X),
               mark#(plus(X1, X2)) -> mark#(X1),
               mark#(plus(X1, X2)) -> mark#(X2),
               mark#(plus(X1, X2)) -> a__plus#(mark(X1), mark(X2)),
                mark#(U11(X1, X2)) -> mark#(X1),
                mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2),
            mark#(U21(X1, X2, X3)) -> mark#(X1),
            mark#(U21(X1, X2, X3)) -> a__U21#(mark(X1), X2, X3),
                mark#(and(X1, X2)) -> mark#(X1),
                mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                  a__U11#(tt(), N) -> mark#(N),
                 a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N),
                 a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)),
                 a__plus#(N, s(M)) -> a__isNat#(M),
               a__U21#(tt(), M, N) -> mark#(N),
               a__U21#(tt(), M, N) -> mark#(M),
               a__U21#(tt(), M, N) -> a__plus#(mark(N), mark(M)),
                  a__and#(tt(), X) -> mark#(X),
                  a__isNat#(s(V1)) -> a__isNat#(V1),
           a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)),
           a__isNat#(plus(V1, V2)) -> a__isNat#(V1)}
         Weak:
         {            mark(tt()) -> tt(),
                      mark(s(X)) -> s(mark(X)),
                       mark(0()) -> 0(),
                  mark(isNat(X)) -> a__isNat(X),
              mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
               mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
           mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
               mark(and(X1, X2)) -> a__and(mark(X1), X2),
                  a__U11(X1, X2) -> U11(X1, X2),
                 a__U11(tt(), N) -> mark(N),
                a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
                 a__plus(N, 0()) -> a__U11(a__isNat(N), N),
                 a__plus(X1, X2) -> plus(X1, X2),
              a__U21(X1, X2, X3) -> U21(X1, X2, X3),
              a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
                  a__and(X1, X2) -> and(X1, X2),
                 a__and(tt(), X) -> mark(X),
                     a__isNat(X) -> isNat(X),
                 a__isNat(s(V1)) -> a__isNat(V1),
                   a__isNat(0()) -> tt(),
          a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
         POLY:
          Argument Filtering:
           pi(and) = [0,1], pi(U21) = [0,1,2], pi(U11) = [0,1], pi(plus) = [0,1], pi(isNat) = [], pi(0) = [], pi(a__isNat#) = [], pi(a__isNat) = [], pi(a__and#) = [1], pi(a__and) = [0,1], pi(a__U21#) = [1,2], pi(a__U21) = [0,1,2], pi(a__plus#) = [0,1], pi(a__plus) = [0,1], pi(s) = [0], pi(tt) = [], pi(a__U11#) = [1], pi(a__U11) = [0,1], pi(mark#) = [0], pi(mark) = 0
          Usable Rules:
           {}
          Interpretation:
           [a__U21#](x0, x1) = x0 + x1 + 1,
           [a__and#](x0) = x0 + 1,
           [a__plus#](x0, x1) = x0 + x1,
           [a__U11#](x0) = x0 + 1,
           [a__isNat#] = 1,
           [mark#](x0) = x0 + 1,
           [U21](x0, x1, x2) = x0 + x1 + x2 + 1,
           [and](x0, x1) = x0 + x1,
           [U11](x0, x1) = x0 + x1,
           [plus](x0, x1) = x0 + x1,
           [isNat] = 0,
           [s](x0) = x0 + 1
          Strict:
           {        mark#(isNat(X)) -> a__isNat#(X),
                mark#(plus(X1, X2)) -> mark#(X1),
                mark#(plus(X1, X2)) -> mark#(X2),
                 mark#(U11(X1, X2)) -> mark#(X1),
                 mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2),
                 mark#(and(X1, X2)) -> mark#(X1),
                 mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                   a__U11#(tt(), N) -> mark#(N),
                  a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N),
                  a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)),
                  a__plus#(N, s(M)) -> a__isNat#(M),
                a__U21#(tt(), M, N) -> mark#(N),
                a__U21#(tt(), M, N) -> mark#(M),
                   a__and#(tt(), X) -> mark#(X),
                   a__isNat#(s(V1)) -> a__isNat#(V1),
            a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)),
            a__isNat#(plus(V1, V2)) -> a__isNat#(V1)}
          Weak:
           {            mark(tt()) -> tt(),
                        mark(s(X)) -> s(mark(X)),
                         mark(0()) -> 0(),
                    mark(isNat(X)) -> a__isNat(X),
                mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
                 mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
             mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
                 mark(and(X1, X2)) -> a__and(mark(X1), X2),
                    a__U11(X1, X2) -> U11(X1, X2),
                   a__U11(tt(), N) -> mark(N),
                  a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
                   a__plus(N, 0()) -> a__U11(a__isNat(N), N),
                   a__plus(X1, X2) -> plus(X1, X2),
                a__U21(X1, X2, X3) -> U21(X1, X2, X3),
                a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
                    a__and(X1, X2) -> and(X1, X2),
                   a__and(tt(), X) -> mark(X),
                       a__isNat(X) -> isNat(X),
                   a__isNat(s(V1)) -> a__isNat(V1),
                     a__isNat(0()) -> tt(),
            a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
          EDG:
           {(a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)), a__and#(tt(), X) -> mark#(X))
            (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
            (mark#(plus(X1, X2)) -> mark#(X2), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
            (mark#(plus(X1, X2)) -> mark#(X2), mark#(U11(X1, X2)) -> mark#(X1))
            (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X2))
            (mark#(plus(X1, X2)) -> mark#(X2), mark#(plus(X1, X2)) -> mark#(X1))
            (mark#(plus(X1, X2)) -> mark#(X2), mark#(isNat(X)) -> a__isNat#(X))
            (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
            (mark#(U11(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
            (mark#(U11(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
            (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
            (mark#(U11(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
            (mark#(U11(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
            (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
            (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
            (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1))
            (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
            (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
            (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(V1)) -> a__isNat#(V1))
            (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
            (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
            (a__plus#(N, s(M)) -> a__isNat#(M), a__isNat#(s(V1)) -> a__isNat#(V1))
            (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
            (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
            (a__U11#(tt(), N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
            (a__U11#(tt(), N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1))
            (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2))
            (a__U11#(tt(), N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1))
            (a__U11#(tt(), N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X))
            (mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2), a__U11#(tt(), N) -> mark#(N))
            (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X))
            (a__U21#(tt(), M, N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X))
            (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X1))
            (a__U21#(tt(), M, N) -> mark#(N), mark#(plus(X1, X2)) -> mark#(X2))
            (a__U21#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> mark#(X1))
            (a__U21#(tt(), M, N) -> mark#(N), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
            (a__U21#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
            (a__U21#(tt(), M, N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
            (a__U21#(tt(), M, N) -> mark#(M), mark#(isNat(X)) -> a__isNat#(X))
            (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X1))
            (a__U21#(tt(), M, N) -> mark#(M), mark#(plus(X1, X2)) -> mark#(X2))
            (a__U21#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> mark#(X1))
            (a__U21#(tt(), M, N) -> mark#(M), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
            (a__U21#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> mark#(X1))
            (a__U21#(tt(), M, N) -> mark#(M), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
            (a__and#(tt(), X) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
            (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X1))
            (a__and#(tt(), X) -> mark#(X), mark#(plus(X1, X2)) -> mark#(X2))
            (a__and#(tt(), X) -> mark#(X), mark#(U11(X1, X2)) -> mark#(X1))
            (a__and#(tt(), X) -> mark#(X), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
            (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
            (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
            (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1))
            (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)))
            (a__isNat#(plus(V1, V2)) -> a__isNat#(V1), a__isNat#(plus(V1, V2)) -> a__isNat#(V1))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
            (mark#(plus(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
            (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X1))
            (mark#(plus(X1, X2)) -> mark#(X1), mark#(plus(X1, X2)) -> mark#(X2))
            (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> mark#(X1))
            (mark#(plus(X1, X2)) -> mark#(X1), mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2))
            (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
            (mark#(plus(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
            (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> mark#(N))
            (a__plus#(N, s(M)) -> a__U21#(a__and(a__isNat(M), isNat(N)), M, N), a__U21#(tt(), M, N) -> mark#(M))
            (a__plus#(N, s(M)) -> a__and#(a__isNat(M), isNat(N)), a__and#(tt(), X) -> mark#(X))}
           SCCS:
            Scc:
             {        mark#(isNat(X)) -> a__isNat#(X),
                  mark#(plus(X1, X2)) -> mark#(X1),
                  mark#(plus(X1, X2)) -> mark#(X2),
                   mark#(U11(X1, X2)) -> mark#(X1),
                   mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2),
                   mark#(and(X1, X2)) -> mark#(X1),
                   mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                     a__U11#(tt(), N) -> mark#(N),
                     a__and#(tt(), X) -> mark#(X),
                     a__isNat#(s(V1)) -> a__isNat#(V1),
              a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)),
              a__isNat#(plus(V1, V2)) -> a__isNat#(V1)}
            SCC:
             Strict:
              {        mark#(isNat(X)) -> a__isNat#(X),
                   mark#(plus(X1, X2)) -> mark#(X1),
                   mark#(plus(X1, X2)) -> mark#(X2),
                    mark#(U11(X1, X2)) -> mark#(X1),
                    mark#(U11(X1, X2)) -> a__U11#(mark(X1), X2),
                    mark#(and(X1, X2)) -> mark#(X1),
                    mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                      a__U11#(tt(), N) -> mark#(N),
                      a__and#(tt(), X) -> mark#(X),
                      a__isNat#(s(V1)) -> a__isNat#(V1),
               a__isNat#(plus(V1, V2)) -> a__and#(a__isNat(V1), isNat(V2)),
               a__isNat#(plus(V1, V2)) -> a__isNat#(V1)}
             Weak:
             {            mark(tt()) -> tt(),
                          mark(s(X)) -> s(mark(X)),
                           mark(0()) -> 0(),
                      mark(isNat(X)) -> a__isNat(X),
                  mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
                   mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
               mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
                   mark(and(X1, X2)) -> a__and(mark(X1), X2),
                      a__U11(X1, X2) -> U11(X1, X2),
                     a__U11(tt(), N) -> mark(N),
                    a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
                     a__plus(N, 0()) -> a__U11(a__isNat(N), N),
                     a__plus(X1, X2) -> plus(X1, X2),
                  a__U21(X1, X2, X3) -> U21(X1, X2, X3),
                  a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
                      a__and(X1, X2) -> and(X1, X2),
                     a__and(tt(), X) -> mark(X),
                         a__isNat(X) -> isNat(X),
                     a__isNat(s(V1)) -> a__isNat(V1),
                       a__isNat(0()) -> tt(),
              a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
             POLY:
              Argument Filtering:
               pi(and) = [0,1], pi(U21) = [], pi(U11) = [0,1], pi(plus) = [0,1], pi(isNat) = [0], pi(0) = [], pi(a__isNat#) = [0], pi(a__isNat) = [], pi(a__and#) = 1, pi(a__and) = [], pi(a__U21) = [], pi(a__plus) = [], pi(s) = 0, pi(tt) = [], pi(a__U11#) = 1, pi(a__U11) = [], pi(mark#) = 0, pi(mark) = []
              Usable Rules:
               {}
              Interpretation:
               [a__isNat#](x0) = x0 + 1,
               [and](x0, x1) = x0 + x1,
               [U11](x0, x1) = x0 + x1 + 1,
               [plus](x0, x1) = x0 + x1 + 1,
               [isNat](x0) = x0 + 1
              Strict:
               {   mark#(isNat(X)) -> a__isNat#(X),
                mark#(and(X1, X2)) -> mark#(X1),
                mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                  a__U11#(tt(), N) -> mark#(N),
                  a__and#(tt(), X) -> mark#(X),
                  a__isNat#(s(V1)) -> a__isNat#(V1)}
              Weak:
               {            mark(tt()) -> tt(),
                            mark(s(X)) -> s(mark(X)),
                             mark(0()) -> 0(),
                        mark(isNat(X)) -> a__isNat(X),
                    mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
                     mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
                 mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
                     mark(and(X1, X2)) -> a__and(mark(X1), X2),
                        a__U11(X1, X2) -> U11(X1, X2),
                       a__U11(tt(), N) -> mark(N),
                      a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
                       a__plus(N, 0()) -> a__U11(a__isNat(N), N),
                       a__plus(X1, X2) -> plus(X1, X2),
                    a__U21(X1, X2, X3) -> U21(X1, X2, X3),
                    a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
                        a__and(X1, X2) -> and(X1, X2),
                       a__and(tt(), X) -> mark(X),
                           a__isNat(X) -> isNat(X),
                       a__isNat(s(V1)) -> a__isNat(V1),
                         a__isNat(0()) -> tt(),
                a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
              EDG:
               {(a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
                (a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
                (a__and#(tt(), X) -> mark#(X), mark#(isNat(X)) -> a__isNat#(X))
                (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
                (a__U11#(tt(), N) -> mark#(N), mark#(and(X1, X2)) -> mark#(X1))
                (a__U11#(tt(), N) -> mark#(N), mark#(isNat(X)) -> a__isNat#(X))
                (a__isNat#(s(V1)) -> a__isNat#(V1), a__isNat#(s(V1)) -> a__isNat#(V1))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(isNat(X)) -> a__isNat#(X))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))
                (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> a__and#(mark(X1), X2))
                (mark#(and(X1, X2)) -> a__and#(mark(X1), X2), a__and#(tt(), X) -> mark#(X))
                (mark#(isNat(X)) -> a__isNat#(X), a__isNat#(s(V1)) -> a__isNat#(V1))}
               SCCS:
                Scc:
                 {a__isNat#(s(V1)) -> a__isNat#(V1)}
                Scc:
                 {mark#(and(X1, X2)) -> mark#(X1),
                  mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                    a__and#(tt(), X) -> mark#(X)}
                SCC:
                 Strict:
                  {a__isNat#(s(V1)) -> a__isNat#(V1)}
                 Weak:
                 {            mark(tt()) -> tt(),
                              mark(s(X)) -> s(mark(X)),
                               mark(0()) -> 0(),
                          mark(isNat(X)) -> a__isNat(X),
                      mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
                       mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
                   mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
                       mark(and(X1, X2)) -> a__and(mark(X1), X2),
                          a__U11(X1, X2) -> U11(X1, X2),
                         a__U11(tt(), N) -> mark(N),
                        a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
                         a__plus(N, 0()) -> a__U11(a__isNat(N), N),
                         a__plus(X1, X2) -> plus(X1, X2),
                      a__U21(X1, X2, X3) -> U21(X1, X2, X3),
                      a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
                          a__and(X1, X2) -> and(X1, X2),
                         a__and(tt(), X) -> mark(X),
                             a__isNat(X) -> isNat(X),
                         a__isNat(s(V1)) -> a__isNat(V1),
                           a__isNat(0()) -> tt(),
                  a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
                 SPSC:
                  Simple Projection:
                   pi(a__isNat#) = 0
                  Strict:
                   {}
                  Qed
                SCC:
                 Strict:
                  {mark#(and(X1, X2)) -> mark#(X1),
                   mark#(and(X1, X2)) -> a__and#(mark(X1), X2),
                     a__and#(tt(), X) -> mark#(X)}
                 Weak:
                 {            mark(tt()) -> tt(),
                              mark(s(X)) -> s(mark(X)),
                               mark(0()) -> 0(),
                          mark(isNat(X)) -> a__isNat(X),
                      mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
                       mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
                   mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
                       mark(and(X1, X2)) -> a__and(mark(X1), X2),
                          a__U11(X1, X2) -> U11(X1, X2),
                         a__U11(tt(), N) -> mark(N),
                        a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
                         a__plus(N, 0()) -> a__U11(a__isNat(N), N),
                         a__plus(X1, X2) -> plus(X1, X2),
                      a__U21(X1, X2, X3) -> U21(X1, X2, X3),
                      a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
                          a__and(X1, X2) -> and(X1, X2),
                         a__and(tt(), X) -> mark(X),
                             a__isNat(X) -> isNat(X),
                         a__isNat(s(V1)) -> a__isNat(V1),
                           a__isNat(0()) -> tt(),
                  a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
                 SPSC:
                  Simple Projection:
                   pi(a__and#) = 1, pi(mark#) = 0
                  Strict:
                   {mark#(and(X1, X2)) -> mark#(X1),
                      a__and#(tt(), X) -> mark#(X)}
                  EDG:
                   {(a__and#(tt(), X) -> mark#(X), mark#(and(X1, X2)) -> mark#(X1))
                    (mark#(and(X1, X2)) -> mark#(X1), mark#(and(X1, X2)) -> mark#(X1))}
                   SCCS:
                    Scc:
                     {mark#(and(X1, X2)) -> mark#(X1)}
                    SCC:
                     Strict:
                      {mark#(and(X1, X2)) -> mark#(X1)}
                     Weak:
                     {            mark(tt()) -> tt(),
                                  mark(s(X)) -> s(mark(X)),
                                   mark(0()) -> 0(),
                              mark(isNat(X)) -> a__isNat(X),
                          mark(plus(X1, X2)) -> a__plus(mark(X1), mark(X2)),
                           mark(U11(X1, X2)) -> a__U11(mark(X1), X2),
                       mark(U21(X1, X2, X3)) -> a__U21(mark(X1), X2, X3),
                           mark(and(X1, X2)) -> a__and(mark(X1), X2),
                              a__U11(X1, X2) -> U11(X1, X2),
                             a__U11(tt(), N) -> mark(N),
                            a__plus(N, s(M)) -> a__U21(a__and(a__isNat(M), isNat(N)), M, N),
                             a__plus(N, 0()) -> a__U11(a__isNat(N), N),
                             a__plus(X1, X2) -> plus(X1, X2),
                          a__U21(X1, X2, X3) -> U21(X1, X2, X3),
                          a__U21(tt(), M, N) -> s(a__plus(mark(N), mark(M))),
                              a__and(X1, X2) -> and(X1, X2),
                             a__and(tt(), X) -> mark(X),
                                 a__isNat(X) -> isNat(X),
                             a__isNat(s(V1)) -> a__isNat(V1),
                               a__isNat(0()) -> tt(),
                      a__isNat(plus(V1, V2)) -> a__and(a__isNat(V1), isNat(V2))}
                     SPSC:
                      Simple Projection:
                       pi(mark#) = 0
                      Strict:
                       {}
                      Qed