MAYBE
Time: 0.190765
TRS:
 {         mark U11(X1, X2) -> active U11(mark X1, X2),
                  mark tt() -> active tt(),
                   mark s X -> active s mark X,
          mark plus(X1, X2) -> active plus(mark X1, mark X2),
       mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
           mark and(X1, X2) -> active and(mark X1, X2),
               mark isNat X -> active isNat X,
                   mark 0() -> active 0(),
        active U11(tt(), N) -> mark N,
        active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
        active plus(N, 0()) -> mark U11(isNat N, N),
     active U21(tt(), M, N) -> mark s plus(N, M),
        active and(tt(), X) -> mark X,
          active isNat s V1 -> mark isNat V1,
  active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
           active isNat 0() -> mark tt(),
           U11(X1, mark 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),
                   s mark X -> s X,
                 s active X -> s X,
          plus(X1, mark X2) -> plus(X1, X2),
        plus(X1, active X2) -> plus(X1, X2),
          plus(mark X1, X2) -> plus(X1, X2),
        plus(active X1, X2) -> plus(X1, X2),
       U21(X1, X2, mark X3) -> U21(X1, X2, X3),
     U21(X1, X2, active X3) -> U21(X1, X2, X3),
       U21(X1, mark X2, X3) -> U21(X1, X2, X3),
     U21(X1, active X2, X3) -> U21(X1, X2, X3),
       U21(mark X1, X2, X3) -> U21(X1, X2, X3),
     U21(active X1, X2, X3) -> U21(X1, X2, X3),
           and(X1, mark 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),
               isNat mark X -> isNat X,
             isNat active X -> isNat X}
 DP:
  DP:
   {         mark# U11(X1, X2) -> mark# X1,
             mark# U11(X1, X2) -> active# U11(mark X1, X2),
             mark# U11(X1, X2) -> U11#(mark X1, X2),
                    mark# tt() -> active# tt(),
                     mark# s X -> mark# X,
                     mark# s X -> active# s mark X,
                     mark# s X -> s# mark X,
            mark# plus(X1, X2) -> mark# X1,
            mark# plus(X1, X2) -> mark# X2,
            mark# plus(X1, X2) -> active# plus(mark X1, mark X2),
            mark# plus(X1, X2) -> plus#(mark X1, mark X2),
         mark# U21(X1, X2, X3) -> mark# X1,
         mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3),
         mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3),
             mark# and(X1, X2) -> mark# X1,
             mark# and(X1, X2) -> active# and(mark X1, X2),
             mark# and(X1, X2) -> and#(mark X1, X2),
                 mark# isNat X -> active# isNat X,
                     mark# 0() -> active# 0(),
          active# U11(tt(), N) -> mark# N,
          active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N),
          active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N),
          active# plus(N, s M) -> and#(isNat M, isNat N),
          active# plus(N, s M) -> isNat# N,
          active# plus(N, s M) -> isNat# M,
          active# plus(N, 0()) -> mark# U11(isNat N, N),
          active# plus(N, 0()) -> U11#(isNat N, N),
          active# plus(N, 0()) -> isNat# N,
       active# U21(tt(), M, N) -> mark# s plus(N, M),
       active# U21(tt(), M, N) -> s# plus(N, M),
       active# U21(tt(), M, N) -> plus#(N, M),
          active# and(tt(), X) -> mark# X,
            active# isNat s V1 -> mark# isNat V1,
            active# isNat s V1 -> isNat# V1,
    active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2),
    active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2),
    active# isNat plus(V1, V2) -> isNat# V1,
    active# isNat plus(V1, V2) -> isNat# V2,
             active# isNat 0() -> mark# tt(),
             U11#(X1, mark 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),
                     s# mark X -> s# X,
                   s# active X -> s# X,
            plus#(X1, mark X2) -> plus#(X1, X2),
          plus#(X1, active X2) -> plus#(X1, X2),
            plus#(mark X1, X2) -> plus#(X1, X2),
          plus#(active X1, X2) -> plus#(X1, X2),
         U21#(X1, X2, mark X3) -> U21#(X1, X2, X3),
       U21#(X1, X2, active X3) -> U21#(X1, X2, X3),
         U21#(X1, mark X2, X3) -> U21#(X1, X2, X3),
       U21#(X1, active X2, X3) -> U21#(X1, X2, X3),
         U21#(mark X1, X2, X3) -> U21#(X1, X2, X3),
       U21#(active X1, X2, X3) -> U21#(X1, X2, X3),
             and#(X1, mark 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),
                 isNat# mark X -> isNat# X,
               isNat# active X -> isNat# X}
  TRS:
  {         mark U11(X1, X2) -> active U11(mark X1, X2),
                   mark tt() -> active tt(),
                    mark s X -> active s mark X,
           mark plus(X1, X2) -> active plus(mark X1, mark X2),
        mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
            mark and(X1, X2) -> active and(mark X1, X2),
                mark isNat X -> active isNat X,
                    mark 0() -> active 0(),
         active U11(tt(), N) -> mark N,
         active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
         active plus(N, 0()) -> mark U11(isNat N, N),
      active U21(tt(), M, N) -> mark s plus(N, M),
         active and(tt(), X) -> mark X,
           active isNat s V1 -> mark isNat V1,
   active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
            active isNat 0() -> mark tt(),
            U11(X1, mark 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),
                    s mark X -> s X,
                  s active X -> s X,
           plus(X1, mark X2) -> plus(X1, X2),
         plus(X1, active X2) -> plus(X1, X2),
           plus(mark X1, X2) -> plus(X1, X2),
         plus(active X1, X2) -> plus(X1, X2),
        U21(X1, X2, mark X3) -> U21(X1, X2, X3),
      U21(X1, X2, active X3) -> U21(X1, X2, X3),
        U21(X1, mark X2, X3) -> U21(X1, X2, X3),
      U21(X1, active X2, X3) -> U21(X1, X2, X3),
        U21(mark X1, X2, X3) -> U21(X1, X2, X3),
      U21(active X1, X2, X3) -> U21(X1, X2, X3),
            and(X1, mark 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),
                isNat mark X -> isNat X,
              isNat active X -> isNat X}
  UR:
   {         mark U11(X1, X2) -> active U11(mark X1, X2),
                    mark tt() -> active tt(),
                     mark s X -> active s mark X,
            mark plus(X1, X2) -> active plus(mark X1, mark X2),
         mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
             mark and(X1, X2) -> active and(mark X1, X2),
                 mark isNat X -> active isNat X,
                     mark 0() -> active 0(),
          active U11(tt(), N) -> mark N,
          active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
          active plus(N, 0()) -> mark U11(isNat N, N),
       active U21(tt(), M, N) -> mark s plus(N, M),
          active and(tt(), X) -> mark X,
            active isNat s V1 -> mark isNat V1,
    active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
             active isNat 0() -> mark tt(),
             U11(X1, mark 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),
                     s mark X -> s X,
                   s active X -> s X,
            plus(X1, mark X2) -> plus(X1, X2),
          plus(X1, active X2) -> plus(X1, X2),
            plus(mark X1, X2) -> plus(X1, X2),
          plus(active X1, X2) -> plus(X1, X2),
         U21(X1, X2, mark X3) -> U21(X1, X2, X3),
       U21(X1, X2, active X3) -> U21(X1, X2, X3),
         U21(X1, mark X2, X3) -> U21(X1, X2, X3),
       U21(X1, active X2, X3) -> U21(X1, X2, X3),
         U21(mark X1, X2, X3) -> U21(X1, X2, X3),
       U21(active X1, X2, X3) -> U21(X1, X2, X3),
             and(X1, mark 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),
                 isNat mark X -> isNat X,
               isNat active X -> isNat X}
   EDG:
    {
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# isNat X -> active# isNat X)
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# and(X1, X2) -> and#(mark X1, X2))
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# and(X1, X2) -> mark# X1)
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# U21(X1, X2, X3) -> mark# X1)
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# plus(X1, X2) -> active# plus(mark X1, mark X2))
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# plus(X1, X2) -> mark# X2)
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# plus(X1, X2) -> mark# X1)
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# s X -> s# mark X)
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# s X -> active# s mark X)
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# s X -> mark# X)
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# U11(X1, X2) -> U11#(mark X1, X2))
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2), mark# U11(X1, X2) -> mark# X1)
     (U11#(X1, mark X2) -> U11#(X1, X2), U11#(active X1, X2) -> U11#(X1, X2))
     (U11#(X1, mark X2) -> U11#(X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
     (U11#(X1, mark X2) -> U11#(X1, X2), U11#(X1, active 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#(active X1, X2) -> U11#(X1, X2))
     (U11#(mark X1, X2) -> U11#(X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
     (U11#(mark X1, X2) -> U11#(X1, X2), U11#(X1, active X2) -> U11#(X1, X2))
     (U11#(mark X1, X2) -> U11#(X1, X2), U11#(X1, mark X2) -> U11#(X1, X2))
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2))
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2))
     (plus#(X1, mark X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2))
     (plus#(mark X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (and#(X1, mark 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#(X1, mark 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#(mark X1, X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# isNat 0() -> mark# tt())
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# isNat plus(V1, V2) -> isNat# V2)
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# isNat plus(V1, V2) -> isNat# V1)
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2))
     (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 s V1 -> mark# isNat V1)
     (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# U21(tt(), M, N) -> plus#(N, M))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# U21(tt(), M, N) -> s# plus(N, M))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# U21(tt(), M, N) -> mark# s plus(N, M))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# plus(N, 0()) -> isNat# N)
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# plus(N, 0()) -> U11#(isNat N, N))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# plus(N, 0()) -> mark# U11(isNat N, N))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# plus(N, s M) -> isNat# M)
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# plus(N, s M) -> isNat# N)
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# plus(N, s M) -> and#(isNat M, isNat N))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N))
     (mark# U11(X1, X2) -> active# U11(mark X1, X2), active# U11(tt(), N) -> mark# N)
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# isNat X -> active# isNat X)
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# and(X1, X2) -> and#(mark X1, X2))
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# and(X1, X2) -> mark# X1)
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# U21(X1, X2, X3) -> mark# X1)
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# plus(X1, X2) -> active# plus(mark X1, mark X2))
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# plus(X1, X2) -> mark# X2)
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# plus(X1, X2) -> mark# X1)
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# s X -> s# mark X)
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# s X -> active# s mark X)
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# s X -> mark# X)
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# U11(X1, X2) -> U11#(mark X1, X2))
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (active# plus(N, 0()) -> mark# U11(isNat N, N), mark# U11(X1, X2) -> mark# X1)
     (active# isNat 0() -> mark# tt(), mark# tt() -> active# tt())
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# isNat X -> active# isNat X)
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# and(X1, X2) -> and#(mark X1, X2))
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# and(X1, X2) -> mark# X1)
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# U21(X1, X2, X3) -> mark# X1)
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# plus(X1, X2) -> active# plus(mark X1, mark X2))
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# plus(X1, X2) -> mark# X2)
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# plus(X1, X2) -> mark# X1)
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# s X -> s# mark X)
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# s X -> active# s mark X)
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# s X -> mark# X)
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# U11(X1, X2) -> U11#(mark X1, X2))
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N), mark# U11(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> active# isNat X)
     (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2))
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
     (mark# plus(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# plus(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# plus(X1, X2) -> mark# X1, mark# tt() -> active# tt())
     (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> U11#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (mark# plus(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# isNat X -> active# isNat X)
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
     (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) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> active# 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# plus(X1, X2) -> plus#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# plus(X1, X2) -> active# 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# s X -> s# mark X)
     (mark# and(X1, X2) -> mark# X1, mark# s X -> active# 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) -> U11#(mark X1, X2))
     (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) -> mark# X1)
     (mark# s X -> s# mark X, s# active X -> s# X)
     (mark# s X -> s# mark X, s# mark X -> s# X)
     (active# plus(N, s M) -> and#(isNat M, isNat N), and#(active X1, X2) -> and#(X1, X2))
     (active# plus(N, s M) -> and#(isNat M, isNat N), and#(mark X1, X2) -> and#(X1, X2))
     (active# plus(N, s M) -> and#(isNat M, isNat N), and#(X1, active X2) -> and#(X1, X2))
     (active# plus(N, s M) -> and#(isNat M, isNat N), and#(X1, mark X2) -> and#(X1, X2))
     (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3))
     (mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, active X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3))
     (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3))
     (U21#(X1, active X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3))
     (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3))
     (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3))
     (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3))
     (U21#(active X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3))
     (active# plus(N, 0()) -> U11#(isNat N, N), U11#(active X1, X2) -> U11#(X1, X2))
     (active# plus(N, 0()) -> U11#(isNat N, N), U11#(mark X1, X2) -> U11#(X1, X2))
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# isNat X -> active# isNat X)
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# and(X1, X2) -> and#(mark X1, X2))
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# and(X1, X2) -> mark# X1)
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# U21(X1, X2, X3) -> mark# X1)
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# plus(X1, X2) -> active# plus(mark X1, mark X2))
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# plus(X1, X2) -> mark# X2)
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# plus(X1, X2) -> mark# X1)
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# s X -> s# mark X)
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# s X -> active# s mark X)
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# s X -> mark# X)
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# U11(X1, X2) -> U11#(mark X1, X2))
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (active# U21(tt(), M, N) -> mark# s plus(N, M), mark# U11(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# 0() -> active# 0())
     (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> active# isNat X)
     (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (mark# plus(X1, X2) -> mark# X2, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (mark# plus(X1, X2) -> mark# X2, mark# plus(X1, X2) -> active# plus(mark X1, mark X2))
     (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# s X -> s# mark X)
     (mark# plus(X1, X2) -> mark# X2, mark# s X -> active# s mark X)
     (mark# plus(X1, X2) -> mark# X2, mark# s X -> mark# X)
     (mark# plus(X1, X2) -> mark# X2, mark# tt() -> active# tt())
     (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> U11#(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (mark# plus(X1, X2) -> mark# X2, mark# U11(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> and#(mark X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (mark# and(X1, X2) -> and#(mark X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (mark# s X -> mark# X, mark# 0() -> active# 0())
     (mark# s X -> mark# X, mark# isNat X -> active# isNat X)
     (mark# s X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# s X -> mark# X, mark# and(X1, X2) -> active# 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) -> U21#(mark X1, X2, X3))
     (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (mark# s X -> mark# X, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# s X -> mark# X, mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (mark# s X -> mark# X, mark# plus(X1, X2) -> active# 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# s X -> s# mark X)
     (mark# s X -> mark# X, mark# s X -> active# 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) -> U11#(mark X1, X2))
     (mark# s X -> mark# X, mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (mark# s X -> mark# X, mark# U11(X1, X2) -> mark# X1)
     (s# mark X -> s# X, s# active X -> s# X)
     (s# mark X -> s# X, s# mark X -> s# 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# mark X -> isNat# X)
     (isNat# active X -> isNat# X, isNat# active X -> isNat# X)
     (s# active X -> s# X, s# mark X -> s# X)
     (s# active X -> s# X, s# active X -> s# X)
     (active# and(tt(), X) -> mark# X, mark# U11(X1, X2) -> mark# X1)
     (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# tt() -> active# tt())
     (active# and(tt(), X) -> mark# X, mark# s 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# plus(X1, X2) -> mark# X1)
     (active# and(tt(), X) -> mark# X, mark# plus(X1, X2) -> mark# X2)
     (active# and(tt(), X) -> mark# X, mark# plus(X1, X2) -> active# plus(mark X1, mark X2))
     (active# and(tt(), X) -> mark# X, mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (active# and(tt(), X) -> mark# X, mark# U21(X1, X2, X3) -> mark# X1)
     (active# and(tt(), X) -> mark# X, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (active# and(tt(), X) -> mark# X, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (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# isNat X -> active# isNat X)
     (active# and(tt(), X) -> mark# X, mark# 0() -> active# 0())
     (mark# U11(X1, X2) -> U11#(mark X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
     (mark# U11(X1, X2) -> U11#(mark X1, X2), U11#(active X1, X2) -> U11#(X1, X2))
     (mark# s X -> active# s mark X, active# U11(tt(), N) -> mark# N)
     (mark# s X -> active# s mark X, active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N))
     (mark# s X -> active# s mark X, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (mark# s X -> active# s mark X, active# plus(N, s M) -> and#(isNat M, isNat N))
     (mark# s X -> active# s mark X, active# plus(N, s M) -> isNat# N)
     (mark# s X -> active# s mark X, active# plus(N, s M) -> isNat# M)
     (mark# s X -> active# s mark X, active# plus(N, 0()) -> mark# U11(isNat N, N))
     (mark# s X -> active# s mark X, active# plus(N, 0()) -> U11#(isNat N, N))
     (mark# s X -> active# s mark X, active# plus(N, 0()) -> isNat# N)
     (mark# s X -> active# s mark X, active# U21(tt(), M, N) -> mark# s plus(N, M))
     (mark# s X -> active# s mark X, active# U21(tt(), M, N) -> s# plus(N, M))
     (mark# s X -> active# s mark X, active# U21(tt(), M, N) -> plus#(N, M))
     (mark# s X -> active# s mark X, active# and(tt(), X) -> mark# X)
     (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 plus(V1, V2) -> mark# and(isNat V1, isNat V2))
     (mark# s X -> active# s mark X, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (mark# s X -> active# s mark X, active# isNat plus(V1, V2) -> isNat# V1)
     (mark# s X -> active# s mark X, active# isNat plus(V1, V2) -> isNat# V2)
     (mark# s X -> active# s mark X, active# isNat 0() -> mark# tt())
     (active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N), U21#(active X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(mark X1, X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3))
     (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3))
     (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, mark X2, X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, mark X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, X2, active X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, mark X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(X1, active X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(mark X1, X2, X3) -> U21#(X1, X2, X3))
     (U21#(X1, X2, mark X3) -> U21#(X1, X2, X3), U21#(active X1, X2, X3) -> U21#(X1, X2, X3))
     (active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2), and#(X1, mark X2) -> and#(X1, X2))
     (active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2), and#(X1, active X2) -> and#(X1, X2))
     (active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2), and#(mark X1, X2) -> and#(X1, X2))
     (active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2), and#(active X1, X2) -> and#(X1, X2))
     (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(X1, active X2) -> plus#(X1, X2))
     (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (mark# plus(X1, X2) -> plus#(mark X1, mark X2), plus#(active X1, X2) -> plus#(X1, X2))
     (mark# isNat X -> active# isNat X, active# U11(tt(), N) -> mark# N)
     (mark# isNat X -> active# isNat X, active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N))
     (mark# isNat X -> active# isNat X, active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (mark# isNat X -> active# isNat X, active# plus(N, s M) -> and#(isNat M, isNat N))
     (mark# isNat X -> active# isNat X, active# plus(N, s M) -> isNat# N)
     (mark# isNat X -> active# isNat X, active# plus(N, s M) -> isNat# M)
     (mark# isNat X -> active# isNat X, active# plus(N, 0()) -> mark# U11(isNat N, N))
     (mark# isNat X -> active# isNat X, active# plus(N, 0()) -> U11#(isNat N, N))
     (mark# isNat X -> active# isNat X, active# plus(N, 0()) -> isNat# N)
     (mark# isNat X -> active# isNat X, active# U21(tt(), M, N) -> mark# s plus(N, M))
     (mark# isNat X -> active# isNat X, active# U21(tt(), M, N) -> s# plus(N, M))
     (mark# isNat X -> active# isNat X, active# U21(tt(), M, N) -> plus#(N, M))
     (mark# isNat X -> active# isNat X, active# and(tt(), X) -> mark# X)
     (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 plus(V1, V2) -> mark# and(isNat V1, isNat V2))
     (mark# isNat X -> active# isNat X, active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (mark# isNat X -> active# isNat X, active# isNat plus(V1, V2) -> isNat# V1)
     (mark# isNat X -> active# isNat X, active# isNat plus(V1, V2) -> isNat# V2)
     (mark# isNat X -> active# isNat X, active# isNat 0() -> mark# tt())
     (active# isNat s V1 -> mark# isNat V1, mark# U11(X1, X2) -> mark# X1)
     (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# s 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# plus(X1, X2) -> mark# X1)
     (active# isNat s V1 -> mark# isNat V1, mark# plus(X1, X2) -> mark# X2)
     (active# isNat s V1 -> mark# isNat V1, mark# plus(X1, X2) -> active# plus(mark X1, mark X2))
     (active# isNat s V1 -> mark# isNat V1, mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (active# isNat s V1 -> mark# isNat V1, mark# U21(X1, X2, X3) -> mark# X1)
     (active# isNat s V1 -> mark# isNat V1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (active# isNat s V1 -> mark# isNat V1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (active# isNat s V1 -> mark# isNat V1, mark# and(X1, X2) -> mark# X1)
     (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# isNat X -> active# isNat X)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> U11#(mark X1, X2))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# tt() -> active# tt())
     (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> active# s mark X)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# s X -> s# mark 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) -> active# plus(mark X1, mark X2))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark 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) -> active# U21(mark X1, X2, X3))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# U21(X1, X2, X3) -> 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) -> active# and(mark X1, X2))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# U21(X1, X2, X3) -> mark# X1, mark# isNat X -> active# isNat X)
     (mark# U21(X1, X2, X3) -> mark# X1, mark# 0() -> active# 0())
     (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
     (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> U11#(mark X1, X2))
     (mark# U11(X1, X2) -> mark# X1, mark# tt() -> active# tt())
     (mark# U11(X1, X2) -> mark# X1, mark# s X -> mark# X)
     (mark# U11(X1, X2) -> mark# X1, mark# s X -> active# s mark X)
     (mark# U11(X1, X2) -> mark# X1, mark# s X -> s# mark X)
     (mark# U11(X1, X2) -> mark# X1, mark# plus(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) -> active# plus(mark X1, mark X2))
     (mark# U11(X1, X2) -> mark# X1, mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (mark# U11(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> mark# X1)
     (mark# U11(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (mark# U11(X1, X2) -> mark# X1, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (mark# U11(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (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# isNat X -> active# isNat X)
     (mark# U11(X1, X2) -> mark# X1, mark# 0() -> active# 0())
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U11(tt(), N) -> mark# N)
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, s M) -> and#(isNat M, isNat N))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, s M) -> isNat# N)
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, s M) -> isNat# M)
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, 0()) -> mark# U11(isNat N, N))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, 0()) -> U11#(isNat N, N))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# plus(N, 0()) -> isNat# N)
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U21(tt(), M, N) -> mark# s plus(N, M))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U21(tt(), M, N) -> s# plus(N, M))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# U21(tt(), M, N) -> plus#(N, M))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# and(tt(), X) -> mark# X)
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# isNat s V1 -> mark# isNat V1)
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# isNat s V1 -> isNat# V1)
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# isNat plus(V1, V2) -> isNat# V1)
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# isNat plus(V1, V2) -> isNat# V2)
     (mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3), active# isNat 0() -> mark# tt())
     (active# U21(tt(), M, N) -> s# plus(N, M), s# mark X -> s# X)
     (active# U21(tt(), M, N) -> s# plus(N, M), s# active X -> s# X)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# U11(tt(), N) -> mark# N)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# plus(N, s M) -> and#(isNat M, isNat N))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# plus(N, s M) -> isNat# N)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# plus(N, s M) -> isNat# M)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# plus(N, 0()) -> mark# U11(isNat N, N))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# plus(N, 0()) -> U11#(isNat N, N))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# plus(N, 0()) -> isNat# N)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# U21(tt(), M, N) -> mark# s plus(N, M))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# U21(tt(), M, N) -> s# plus(N, M))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# U21(tt(), M, N) -> plus#(N, M))
     (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# 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 plus(V1, V2) -> mark# and(isNat V1, isNat V2))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# isNat plus(V1, V2) -> isNat# V1)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# isNat plus(V1, V2) -> isNat# V2)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# isNat 0() -> mark# tt())
     (and#(active 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))
     (and#(active X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (and#(active X1, 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#(X1, active X2) -> and#(X1, X2))
     (and#(X1, active X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (and#(X1, active X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (plus#(active X1, X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (plus#(active X1, X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2))
     (plus#(active X1, X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(active X1, X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2))
     (plus#(X1, active X2) -> plus#(X1, X2), plus#(X1, mark X2) -> plus#(X1, X2))
     (plus#(X1, active X2) -> plus#(X1, X2), plus#(X1, active X2) -> plus#(X1, X2))
     (plus#(X1, active X2) -> plus#(X1, X2), plus#(mark X1, X2) -> plus#(X1, X2))
     (plus#(X1, active X2) -> plus#(X1, X2), plus#(active X1, X2) -> plus#(X1, X2))
     (U11#(active 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))
     (U11#(active X1, X2) -> U11#(X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
     (U11#(active X1, X2) -> U11#(X1, X2), U11#(active X1, X2) -> U11#(X1, X2))
     (U11#(X1, active X2) -> U11#(X1, X2), U11#(X1, mark X2) -> U11#(X1, X2))
     (U11#(X1, active X2) -> U11#(X1, X2), U11#(X1, active X2) -> U11#(X1, X2))
     (U11#(X1, active X2) -> U11#(X1, X2), U11#(mark X1, X2) -> U11#(X1, X2))
     (U11#(X1, active X2) -> U11#(X1, X2), U11#(active X1, X2) -> U11#(X1, X2))
     (active# U11(tt(), N) -> mark# N, mark# U11(X1, X2) -> mark# X1)
     (active# U11(tt(), N) -> mark# N, mark# U11(X1, X2) -> active# U11(mark X1, X2))
     (active# U11(tt(), N) -> mark# N, mark# U11(X1, X2) -> U11#(mark X1, X2))
     (active# U11(tt(), N) -> mark# N, mark# tt() -> active# tt())
     (active# U11(tt(), N) -> mark# N, mark# s X -> mark# X)
     (active# U11(tt(), N) -> mark# N, mark# s X -> active# s mark X)
     (active# U11(tt(), N) -> mark# N, mark# s X -> s# mark X)
     (active# U11(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1)
     (active# U11(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2)
     (active# U11(tt(), N) -> mark# N, mark# plus(X1, X2) -> active# plus(mark X1, mark X2))
     (active# U11(tt(), N) -> mark# N, mark# plus(X1, X2) -> plus#(mark X1, mark X2))
     (active# U11(tt(), N) -> mark# N, mark# U21(X1, X2, X3) -> mark# X1)
     (active# U11(tt(), N) -> mark# N, mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3))
     (active# U11(tt(), N) -> mark# N, mark# U21(X1, X2, X3) -> U21#(mark X1, X2, X3))
     (active# U11(tt(), N) -> mark# N, mark# and(X1, X2) -> mark# X1)
     (active# U11(tt(), N) -> mark# N, mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# U11(tt(), N) -> mark# N, mark# and(X1, X2) -> and#(mark X1, X2))
     (active# U11(tt(), N) -> mark# N, mark# isNat X -> active# isNat X)
     (active# U11(tt(), N) -> mark# N, mark# 0() -> active# 0())
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U11(tt(), N) -> mark# N)
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> U21#(and(isNat M, isNat N), M, N))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> and#(isNat M, isNat N))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> isNat# N)
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, s M) -> isNat# M)
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, 0()) -> mark# U11(isNat N, N))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, 0()) -> U11#(isNat N, N))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# plus(N, 0()) -> isNat# N)
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U21(tt(), M, N) -> mark# s plus(N, M))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U21(tt(), M, N) -> s# plus(N, M))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# U21(tt(), M, N) -> plus#(N, M))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# and(tt(), X) -> mark# X)
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# isNat s V1 -> mark# isNat V1)
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# isNat s V1 -> isNat# V1)
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# isNat plus(V1, V2) -> and#(isNat V1, isNat V2))
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# isNat plus(V1, V2) -> isNat# V1)
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# isNat plus(V1, V2) -> isNat# V2)
     (mark# plus(X1, X2) -> active# plus(mark X1, mark X2), active# isNat 0() -> mark# tt())
    }
    STATUS:
     arrows: 0.872077
     SCCS (7):
      Scc:
       {  isNat# mark X -> isNat# X,
        isNat# active X -> isNat# X}
      Scc:
       {         mark# U11(X1, X2) -> mark# X1,
                 mark# U11(X1, X2) -> active# U11(mark X1, X2),
                         mark# s X -> mark# X,
                         mark# s X -> active# s mark X,
                mark# plus(X1, X2) -> mark# X1,
                mark# plus(X1, X2) -> mark# X2,
                mark# plus(X1, X2) -> active# plus(mark X1, mark X2),
             mark# U21(X1, X2, X3) -> mark# X1,
             mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3),
                 mark# and(X1, X2) -> mark# X1,
                 mark# and(X1, X2) -> active# and(mark X1, X2),
                     mark# isNat X -> active# isNat X,
              active# U11(tt(), N) -> mark# N,
              active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N),
              active# plus(N, 0()) -> mark# U11(isNat N, N),
           active# U21(tt(), M, N) -> mark# s plus(N, M),
              active# and(tt(), X) -> mark# X,
                active# isNat s V1 -> mark# isNat V1,
        active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2)}
      Scc:
       {  plus#(X1, mark X2) -> plus#(X1, X2),
        plus#(X1, active X2) -> plus#(X1, X2),
          plus#(mark X1, X2) -> plus#(X1, X2),
        plus#(active X1, X2) -> plus#(X1, X2)}
      Scc:
       {  s# mark X -> s# X,
        s# active X -> s# X}
      Scc:
       {  and#(X1, mark 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)}
      Scc:
       {  U21#(X1, X2, mark X3) -> U21#(X1, X2, X3),
        U21#(X1, X2, active X3) -> U21#(X1, X2, X3),
          U21#(X1, mark X2, X3) -> U21#(X1, X2, X3),
        U21#(X1, active X2, X3) -> U21#(X1, X2, X3),
          U21#(mark X1, X2, X3) -> U21#(X1, X2, X3),
        U21#(active X1, X2, X3) -> U21#(X1, X2, X3)}
      Scc:
       {  U11#(X1, mark 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)}
      
      SCC (2):
       Strict:
        {  isNat# mark X -> isNat# X,
         isNat# active X -> isNat# X}
       Weak:
       {         mark U11(X1, X2) -> active U11(mark X1, X2),
                        mark tt() -> active tt(),
                         mark s X -> active s mark X,
                mark plus(X1, X2) -> active plus(mark X1, mark X2),
             mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
                 mark and(X1, X2) -> active and(mark X1, X2),
                     mark isNat X -> active isNat X,
                         mark 0() -> active 0(),
              active U11(tt(), N) -> mark N,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
           active U21(tt(), M, N) -> mark s plus(N, M),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
                 U11(X1, mark 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),
                         s mark X -> s X,
                       s active X -> s X,
                plus(X1, mark X2) -> plus(X1, X2),
              plus(X1, active X2) -> plus(X1, X2),
                plus(mark X1, X2) -> plus(X1, X2),
              plus(active X1, X2) -> plus(X1, X2),
             U21(X1, X2, mark X3) -> U21(X1, X2, X3),
           U21(X1, X2, active X3) -> U21(X1, X2, X3),
             U21(X1, mark X2, X3) -> U21(X1, X2, X3),
           U21(X1, active X2, X3) -> U21(X1, X2, X3),
             U21(mark X1, X2, X3) -> U21(X1, X2, X3),
           U21(active X1, X2, X3) -> U21(X1, X2, X3),
                 and(X1, mark 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),
                     isNat mark X -> isNat X,
                   isNat active X -> isNat X}
       Open
      SCC (19):
       Strict:
        {         mark# U11(X1, X2) -> mark# X1,
                  mark# U11(X1, X2) -> active# U11(mark X1, X2),
                          mark# s X -> mark# X,
                          mark# s X -> active# s mark X,
                 mark# plus(X1, X2) -> mark# X1,
                 mark# plus(X1, X2) -> mark# X2,
                 mark# plus(X1, X2) -> active# plus(mark X1, mark X2),
              mark# U21(X1, X2, X3) -> mark# X1,
              mark# U21(X1, X2, X3) -> active# U21(mark X1, X2, X3),
                  mark# and(X1, X2) -> mark# X1,
                  mark# and(X1, X2) -> active# and(mark X1, X2),
                      mark# isNat X -> active# isNat X,
               active# U11(tt(), N) -> mark# N,
               active# plus(N, s M) -> mark# U21(and(isNat M, isNat N), M, N),
               active# plus(N, 0()) -> mark# U11(isNat N, N),
            active# U21(tt(), M, N) -> mark# s plus(N, M),
               active# and(tt(), X) -> mark# X,
                 active# isNat s V1 -> mark# isNat V1,
         active# isNat plus(V1, V2) -> mark# and(isNat V1, isNat V2)}
       Weak:
       {         mark U11(X1, X2) -> active U11(mark X1, X2),
                        mark tt() -> active tt(),
                         mark s X -> active s mark X,
                mark plus(X1, X2) -> active plus(mark X1, mark X2),
             mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
                 mark and(X1, X2) -> active and(mark X1, X2),
                     mark isNat X -> active isNat X,
                         mark 0() -> active 0(),
              active U11(tt(), N) -> mark N,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
           active U21(tt(), M, N) -> mark s plus(N, M),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
                 U11(X1, mark 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),
                         s mark X -> s X,
                       s active X -> s X,
                plus(X1, mark X2) -> plus(X1, X2),
              plus(X1, active X2) -> plus(X1, X2),
                plus(mark X1, X2) -> plus(X1, X2),
              plus(active X1, X2) -> plus(X1, X2),
             U21(X1, X2, mark X3) -> U21(X1, X2, X3),
           U21(X1, X2, active X3) -> U21(X1, X2, X3),
             U21(X1, mark X2, X3) -> U21(X1, X2, X3),
           U21(X1, active X2, X3) -> U21(X1, X2, X3),
             U21(mark X1, X2, X3) -> U21(X1, X2, X3),
           U21(active X1, X2, X3) -> U21(X1, X2, X3),
                 and(X1, mark 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),
                     isNat mark X -> isNat X,
                   isNat active X -> isNat X}
       Open
      
      
      
      
      
      
      
      
      
      
      
      
      
      SCC (4):
       Strict:
        {  plus#(X1, mark X2) -> plus#(X1, X2),
         plus#(X1, active X2) -> plus#(X1, X2),
           plus#(mark X1, X2) -> plus#(X1, X2),
         plus#(active X1, X2) -> plus#(X1, X2)}
       Weak:
       {         mark U11(X1, X2) -> active U11(mark X1, X2),
                        mark tt() -> active tt(),
                         mark s X -> active s mark X,
                mark plus(X1, X2) -> active plus(mark X1, mark X2),
             mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
                 mark and(X1, X2) -> active and(mark X1, X2),
                     mark isNat X -> active isNat X,
                         mark 0() -> active 0(),
              active U11(tt(), N) -> mark N,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
           active U21(tt(), M, N) -> mark s plus(N, M),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
                 U11(X1, mark 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),
                         s mark X -> s X,
                       s active X -> s X,
                plus(X1, mark X2) -> plus(X1, X2),
              plus(X1, active X2) -> plus(X1, X2),
                plus(mark X1, X2) -> plus(X1, X2),
              plus(active X1, X2) -> plus(X1, X2),
             U21(X1, X2, mark X3) -> U21(X1, X2, X3),
           U21(X1, X2, active X3) -> U21(X1, X2, X3),
             U21(X1, mark X2, X3) -> U21(X1, X2, X3),
           U21(X1, active X2, X3) -> U21(X1, X2, X3),
             U21(mark X1, X2, X3) -> U21(X1, X2, X3),
           U21(active X1, X2, X3) -> U21(X1, X2, X3),
                 and(X1, mark 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),
                     isNat mark X -> isNat X,
                   isNat active X -> isNat X}
       Open
      
      SCC (2):
       Strict:
        {  s# mark X -> s# X,
         s# active X -> s# X}
       Weak:
       {         mark U11(X1, X2) -> active U11(mark X1, X2),
                        mark tt() -> active tt(),
                         mark s X -> active s mark X,
                mark plus(X1, X2) -> active plus(mark X1, mark X2),
             mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
                 mark and(X1, X2) -> active and(mark X1, X2),
                     mark isNat X -> active isNat X,
                         mark 0() -> active 0(),
              active U11(tt(), N) -> mark N,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
           active U21(tt(), M, N) -> mark s plus(N, M),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
                 U11(X1, mark 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),
                         s mark X -> s X,
                       s active X -> s X,
                plus(X1, mark X2) -> plus(X1, X2),
              plus(X1, active X2) -> plus(X1, X2),
                plus(mark X1, X2) -> plus(X1, X2),
              plus(active X1, X2) -> plus(X1, X2),
             U21(X1, X2, mark X3) -> U21(X1, X2, X3),
           U21(X1, X2, active X3) -> U21(X1, X2, X3),
             U21(X1, mark X2, X3) -> U21(X1, X2, X3),
           U21(X1, active X2, X3) -> U21(X1, X2, X3),
             U21(mark X1, X2, X3) -> U21(X1, X2, X3),
           U21(active X1, X2, X3) -> U21(X1, X2, X3),
                 and(X1, mark 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),
                     isNat mark X -> isNat X,
                   isNat active X -> isNat X}
       Open
      
      
      
      SCC (4):
       Strict:
        {  and#(X1, mark 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)}
       Weak:
       {         mark U11(X1, X2) -> active U11(mark X1, X2),
                        mark tt() -> active tt(),
                         mark s X -> active s mark X,
                mark plus(X1, X2) -> active plus(mark X1, mark X2),
             mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
                 mark and(X1, X2) -> active and(mark X1, X2),
                     mark isNat X -> active isNat X,
                         mark 0() -> active 0(),
              active U11(tt(), N) -> mark N,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
           active U21(tt(), M, N) -> mark s plus(N, M),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
                 U11(X1, mark 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),
                         s mark X -> s X,
                       s active X -> s X,
                plus(X1, mark X2) -> plus(X1, X2),
              plus(X1, active X2) -> plus(X1, X2),
                plus(mark X1, X2) -> plus(X1, X2),
              plus(active X1, X2) -> plus(X1, X2),
             U21(X1, X2, mark X3) -> U21(X1, X2, X3),
           U21(X1, X2, active X3) -> U21(X1, X2, X3),
             U21(X1, mark X2, X3) -> U21(X1, X2, X3),
           U21(X1, active X2, X3) -> U21(X1, X2, X3),
             U21(mark X1, X2, X3) -> U21(X1, X2, X3),
           U21(active X1, X2, X3) -> U21(X1, X2, X3),
                 and(X1, mark 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),
                     isNat mark X -> isNat X,
                   isNat active X -> isNat X}
       Open
      
      SCC (6):
       Strict:
        {  U21#(X1, X2, mark X3) -> U21#(X1, X2, X3),
         U21#(X1, X2, active X3) -> U21#(X1, X2, X3),
           U21#(X1, mark X2, X3) -> U21#(X1, X2, X3),
         U21#(X1, active X2, X3) -> U21#(X1, X2, X3),
           U21#(mark X1, X2, X3) -> U21#(X1, X2, X3),
         U21#(active X1, X2, X3) -> U21#(X1, X2, X3)}
       Weak:
       {         mark U11(X1, X2) -> active U11(mark X1, X2),
                        mark tt() -> active tt(),
                         mark s X -> active s mark X,
                mark plus(X1, X2) -> active plus(mark X1, mark X2),
             mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
                 mark and(X1, X2) -> active and(mark X1, X2),
                     mark isNat X -> active isNat X,
                         mark 0() -> active 0(),
              active U11(tt(), N) -> mark N,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
           active U21(tt(), M, N) -> mark s plus(N, M),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
                 U11(X1, mark 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),
                         s mark X -> s X,
                       s active X -> s X,
                plus(X1, mark X2) -> plus(X1, X2),
              plus(X1, active X2) -> plus(X1, X2),
                plus(mark X1, X2) -> plus(X1, X2),
              plus(active X1, X2) -> plus(X1, X2),
             U21(X1, X2, mark X3) -> U21(X1, X2, X3),
           U21(X1, X2, active X3) -> U21(X1, X2, X3),
             U21(X1, mark X2, X3) -> U21(X1, X2, X3),
           U21(X1, active X2, X3) -> U21(X1, X2, X3),
             U21(mark X1, X2, X3) -> U21(X1, X2, X3),
           U21(active X1, X2, X3) -> U21(X1, X2, X3),
                 and(X1, mark 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),
                     isNat mark X -> isNat X,
                   isNat active X -> isNat X}
       Open
      
      
      SCC (4):
       Strict:
        {  U11#(X1, mark 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)}
       Weak:
       {         mark U11(X1, X2) -> active U11(mark X1, X2),
                        mark tt() -> active tt(),
                         mark s X -> active s mark X,
                mark plus(X1, X2) -> active plus(mark X1, mark X2),
             mark U21(X1, X2, X3) -> active U21(mark X1, X2, X3),
                 mark and(X1, X2) -> active and(mark X1, X2),
                     mark isNat X -> active isNat X,
                         mark 0() -> active 0(),
              active U11(tt(), N) -> mark N,
              active plus(N, s M) -> mark U21(and(isNat M, isNat N), M, N),
              active plus(N, 0()) -> mark U11(isNat N, N),
           active U21(tt(), M, N) -> mark s plus(N, M),
              active and(tt(), X) -> mark X,
                active isNat s V1 -> mark isNat V1,
        active isNat plus(V1, V2) -> mark and(isNat V1, isNat V2),
                 active isNat 0() -> mark tt(),
                 U11(X1, mark 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),
                         s mark X -> s X,
                       s active X -> s X,
                plus(X1, mark X2) -> plus(X1, X2),
              plus(X1, active X2) -> plus(X1, X2),
                plus(mark X1, X2) -> plus(X1, X2),
              plus(active X1, X2) -> plus(X1, X2),
             U21(X1, X2, mark X3) -> U21(X1, X2, X3),
           U21(X1, X2, active X3) -> U21(X1, X2, X3),
             U21(X1, mark X2, X3) -> U21(X1, X2, X3),
           U21(X1, active X2, X3) -> U21(X1, X2, X3),
             U21(mark X1, X2, X3) -> U21(X1, X2, X3),
           U21(active X1, X2, X3) -> U21(X1, X2, X3),
                 and(X1, mark 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),
                     isNat mark X -> isNat X,
                   isNat active X -> isNat X}
       Open