MAYBE
Time: 0.014406
TRS:
 {             a__U12 X -> U12 X,
            a__U12 tt() -> tt(),
             a__isNat X -> isNat X,
          a__isNat s V1 -> a__U21 a__isNat V1,
           a__isNat 0() -> tt(),
  a__isNat plus(V1, V2) -> a__U11(a__isNat V1, V2),
         a__U11(X1, X2) -> U11(X1, X2),
       a__U11(tt(), V2) -> a__U12 a__isNat V2,
               a__U21 X -> U21 X,
            a__U21 tt() -> tt(),
              mark tt() -> tt(),
               mark s X -> s mark X,
               mark 0() -> 0(),
      mark plus(X1, X2) -> a__plus(mark X1, mark X2),
       mark U11(X1, X2) -> a__U11(mark X1, X2),
             mark U12 X -> a__U12 mark X,
           mark isNat X -> a__isNat X,
             mark U21 X -> a__U21 mark X,
       mark U31(X1, X2) -> a__U31(mark X1, X2),
   mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3),
   mark U42(X1, X2, X3) -> a__U42(mark X1, X2, X3),
         a__U31(X1, X2) -> U31(X1, X2),
        a__U31(tt(), N) -> mark N,
     a__U42(X1, X2, X3) -> U42(X1, X2, X3),
     a__U42(tt(), M, N) -> s a__plus(mark N, mark M),
     a__U41(X1, X2, X3) -> U41(X1, X2, X3),
     a__U41(tt(), M, N) -> a__U42(a__isNat N, M, N),
        a__plus(N, s M) -> a__U41(a__isNat M, M, N),
        a__plus(N, 0()) -> a__U31(a__isNat N, N),
        a__plus(X1, X2) -> plus(X1, X2)}
 DP:
  DP:
   {        a__isNat# s V1 -> a__isNat# V1,
            a__isNat# s V1 -> a__U21# a__isNat V1,
    a__isNat# plus(V1, V2) -> a__isNat# V1,
    a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2),
         a__U11#(tt(), V2) -> a__U12# a__isNat V2,
         a__U11#(tt(), V2) -> a__isNat# V2,
                 mark# s X -> mark# 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) -> a__U11#(mark X1, X2),
         mark# U11(X1, X2) -> mark# X1,
               mark# U12 X -> a__U12# mark X,
               mark# U12 X -> mark# X,
             mark# isNat X -> a__isNat# X,
               mark# U21 X -> a__U21# mark X,
               mark# U21 X -> mark# X,
         mark# U31(X1, X2) -> mark# X1,
         mark# U31(X1, X2) -> a__U31#(mark X1, X2),
     mark# U41(X1, X2, X3) -> mark# X1,
     mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3),
     mark# U42(X1, X2, X3) -> mark# X1,
     mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3),
          a__U31#(tt(), N) -> mark# N,
       a__U42#(tt(), M, N) -> mark# N,
       a__U42#(tt(), M, N) -> mark# M,
       a__U42#(tt(), M, N) -> a__plus#(mark N, mark M),
       a__U41#(tt(), M, N) -> a__isNat# N,
       a__U41#(tt(), M, N) -> a__U42#(a__isNat N, M, N),
          a__plus#(N, s M) -> a__isNat# M,
          a__plus#(N, s M) -> a__U41#(a__isNat M, M, N),
          a__plus#(N, 0()) -> a__isNat# N,
          a__plus#(N, 0()) -> a__U31#(a__isNat N, N)}
  TRS:
  {             a__U12 X -> U12 X,
             a__U12 tt() -> tt(),
              a__isNat X -> isNat X,
           a__isNat s V1 -> a__U21 a__isNat V1,
            a__isNat 0() -> tt(),
   a__isNat plus(V1, V2) -> a__U11(a__isNat V1, V2),
          a__U11(X1, X2) -> U11(X1, X2),
        a__U11(tt(), V2) -> a__U12 a__isNat V2,
                a__U21 X -> U21 X,
             a__U21 tt() -> tt(),
               mark tt() -> tt(),
                mark s X -> s mark X,
                mark 0() -> 0(),
       mark plus(X1, X2) -> a__plus(mark X1, mark X2),
        mark U11(X1, X2) -> a__U11(mark X1, X2),
              mark U12 X -> a__U12 mark X,
            mark isNat X -> a__isNat X,
              mark U21 X -> a__U21 mark X,
        mark U31(X1, X2) -> a__U31(mark X1, X2),
    mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3),
    mark U42(X1, X2, X3) -> a__U42(mark X1, X2, X3),
          a__U31(X1, X2) -> U31(X1, X2),
         a__U31(tt(), N) -> mark N,
      a__U42(X1, X2, X3) -> U42(X1, X2, X3),
      a__U42(tt(), M, N) -> s a__plus(mark N, mark M),
      a__U41(X1, X2, X3) -> U41(X1, X2, X3),
      a__U41(tt(), M, N) -> a__U42(a__isNat N, M, N),
         a__plus(N, s M) -> a__U41(a__isNat M, M, N),
         a__plus(N, 0()) -> a__U31(a__isNat N, N),
         a__plus(X1, X2) -> plus(X1, X2)}
  EDG:
   {
    (mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3), a__U42#(tt(), M, N) -> a__plus#(mark N, mark M))
    (mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3), a__U42#(tt(), M, N) -> mark# M)
    (mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3), a__U42#(tt(), M, N) -> mark# N)
    (a__plus#(N, s M) -> a__isNat# M, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2))
    (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# s V1 -> a__U21# a__isNat V1)
    (a__plus#(N, s M) -> a__isNat# M, a__isNat# s V1 -> a__isNat# V1)
    (mark# plus(X1, X2) -> mark# X2, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (mark# plus(X1, X2) -> mark# X2, mark# U42(X1, X2, X3) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (mark# plus(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (mark# plus(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X2, mark# U21 X -> mark# X)
    (mark# plus(X1, X2) -> mark# X2, mark# U21 X -> a__U21# mark X)
    (mark# plus(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X)
    (mark# plus(X1, X2) -> mark# X2, mark# U12 X -> mark# X)
    (mark# plus(X1, X2) -> mark# X2, mark# U12 X -> a__U12# mark X)
    (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# plus(X1, X2) -> a__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 -> mark# X)
    (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), N) -> mark# N)
    (a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2))
    (a__isNat# s V1 -> a__isNat# V1, a__isNat# plus(V1, V2) -> a__isNat# V1)
    (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__U21# a__isNat V1)
    (a__isNat# s V1 -> a__isNat# V1, a__isNat# s V1 -> a__isNat# V1)
    (mark# s X -> mark# X, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (mark# s X -> mark# X, mark# U42(X1, X2, X3) -> mark# X1)
    (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1)
    (mark# s X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (mark# s X -> mark# X, mark# U31(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# U21 X -> mark# X)
    (mark# s X -> mark# X, mark# U21 X -> a__U21# mark X)
    (mark# s X -> mark# X, mark# isNat X -> a__isNat# X)
    (mark# s X -> mark# X, mark# U12 X -> mark# X)
    (mark# s X -> mark# X, mark# U12 X -> a__U12# mark X)
    (mark# s X -> mark# X, mark# U11(X1, X2) -> mark# X1)
    (mark# s X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
    (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# s X -> mark# X)
    (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2))
    (mark# isNat X -> a__isNat# X, a__isNat# plus(V1, V2) -> a__isNat# V1)
    (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__U21# a__isNat V1)
    (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__isNat# V1)
    (a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2), a__U11#(tt(), V2) -> a__isNat# V2)
    (a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2), a__U11#(tt(), V2) -> a__U12# a__isNat V2)
    (a__U42#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__U31#(a__isNat N, N))
    (a__U42#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, 0()) -> a__isNat# N)
    (a__U42#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__U41#(a__isNat M, M, N))
    (a__U42#(tt(), M, N) -> a__plus#(mark N, mark M), a__plus#(N, s M) -> a__isNat# M)
    (a__U42#(tt(), M, N) -> mark# N, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (a__U42#(tt(), M, N) -> mark# N, mark# U42(X1, X2, X3) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (a__U42#(tt(), M, N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (a__U42#(tt(), M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# N, mark# U21 X -> mark# X)
    (a__U42#(tt(), M, N) -> mark# N, mark# U21 X -> a__U21# mark X)
    (a__U42#(tt(), M, N) -> mark# N, mark# isNat X -> a__isNat# X)
    (a__U42#(tt(), M, N) -> mark# N, mark# U12 X -> mark# X)
    (a__U42#(tt(), M, N) -> mark# N, mark# U12 X -> a__U12# mark X)
    (a__U42#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
    (a__U42#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (a__U42#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X2)
    (a__U42#(tt(), M, N) -> mark# N, mark# plus(X1, X2) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# N, mark# s X -> mark# X)
    (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2))
    (a__plus#(N, 0()) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1)
    (a__plus#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1)
    (a__plus#(N, 0()) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1)
    (a__plus#(N, s M) -> a__U41#(a__isNat M, M, N), a__U41#(tt(), M, N) -> a__U42#(a__isNat N, M, N))
    (a__plus#(N, s M) -> a__U41#(a__isNat M, M, N), a__U41#(tt(), M, N) -> a__isNat# N)
    (mark# U11(X1, X2) -> mark# X1, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (mark# U11(X1, X2) -> mark# X1, mark# U42(X1, X2, X3) -> mark# X1)
    (mark# U11(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (mark# U11(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1)
    (mark# U11(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (mark# U11(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1)
    (mark# U11(X1, X2) -> mark# X1, mark# U21 X -> mark# X)
    (mark# U11(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X)
    (mark# U11(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X)
    (mark# U11(X1, X2) -> mark# X1, mark# U12 X -> mark# X)
    (mark# U11(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X)
    (mark# U11(X1, X2) -> mark# X1, mark# U11(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# 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# s X -> mark# X)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U42(X1, X2, X3) -> mark# X1)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
    (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
    (mark# U41(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# s X -> mark# X)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U21 X -> a__U21# mark X)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U21 X -> mark# X)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U42(X1, X2, X3) -> mark# X1)
    (mark# U42(X1, X2, X3) -> mark# X1, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (mark# U31(X1, X2) -> mark# X1, mark# s X -> mark# X)
    (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X1)
    (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> mark# X2)
    (mark# U31(X1, X2) -> mark# X1, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
    (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
    (mark# U31(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X)
    (mark# U31(X1, X2) -> mark# X1, mark# U12 X -> mark# X)
    (mark# U31(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X)
    (mark# U31(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X)
    (mark# U31(X1, X2) -> mark# X1, mark# U21 X -> mark# X)
    (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1)
    (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1)
    (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (mark# U31(X1, X2) -> mark# X1, mark# U42(X1, X2, X3) -> mark# X1)
    (mark# U31(X1, X2) -> mark# X1, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (mark# plus(X1, X2) -> mark# X1, mark# s X -> mark# 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) -> a__U11#(mark X1, X2))
    (mark# plus(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X)
    (mark# plus(X1, X2) -> mark# X1, mark# U12 X -> mark# X)
    (mark# plus(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X)
    (mark# plus(X1, X2) -> mark# X1, mark# U21 X -> a__U21# mark X)
    (mark# plus(X1, X2) -> mark# X1, mark# U21 X -> mark# X)
    (mark# plus(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (mark# plus(X1, X2) -> mark# X1, mark# U42(X1, X2, X3) -> mark# X1)
    (mark# plus(X1, X2) -> mark# X1, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (a__U41#(tt(), M, N) -> a__U42#(a__isNat N, M, N), a__U42#(tt(), M, N) -> mark# N)
    (a__U41#(tt(), M, N) -> a__U42#(a__isNat N, M, N), a__U42#(tt(), M, N) -> mark# M)
    (a__U41#(tt(), M, N) -> a__U42#(a__isNat N, M, N), a__U42#(tt(), M, N) -> a__plus#(mark N, mark M))
    (a__U41#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__isNat# V1)
    (a__U41#(tt(), M, N) -> a__isNat# N, a__isNat# s V1 -> a__U21# a__isNat V1)
    (a__U41#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__isNat# V1)
    (a__U41#(tt(), M, N) -> a__isNat# N, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2))
    (a__U31#(tt(), N) -> mark# N, mark# s X -> mark# X)
    (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X1)
    (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> mark# X2)
    (a__U31#(tt(), N) -> mark# N, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
    (a__U31#(tt(), N) -> mark# N, mark# U11(X1, X2) -> mark# X1)
    (a__U31#(tt(), N) -> mark# N, mark# U12 X -> a__U12# mark X)
    (a__U31#(tt(), N) -> mark# N, mark# U12 X -> mark# X)
    (a__U31#(tt(), N) -> mark# N, mark# isNat X -> a__isNat# X)
    (a__U31#(tt(), N) -> mark# N, mark# U21 X -> a__U21# mark X)
    (a__U31#(tt(), N) -> mark# N, mark# U21 X -> mark# X)
    (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> mark# X1)
    (a__U31#(tt(), N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1)
    (a__U31#(tt(), N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (a__U31#(tt(), N) -> mark# N, mark# U42(X1, X2, X3) -> mark# X1)
    (a__U31#(tt(), N) -> mark# N, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (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__U41#(a__isNat M, M, N))
    (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__isNat# N)
    (mark# plus(X1, X2) -> a__plus#(mark X1, mark X2), a__plus#(N, 0()) -> a__U31#(a__isNat N, N))
    (mark# U21 X -> mark# X, mark# s X -> mark# X)
    (mark# U21 X -> mark# X, mark# plus(X1, X2) -> mark# X1)
    (mark# U21 X -> mark# X, mark# plus(X1, X2) -> mark# X2)
    (mark# U21 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (mark# U21 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
    (mark# U21 X -> mark# X, mark# U11(X1, X2) -> mark# X1)
    (mark# U21 X -> mark# X, mark# U12 X -> a__U12# mark X)
    (mark# U21 X -> mark# X, mark# U12 X -> mark# X)
    (mark# U21 X -> mark# X, mark# isNat X -> a__isNat# X)
    (mark# U21 X -> mark# X, mark# U21 X -> a__U21# mark X)
    (mark# U21 X -> mark# X, mark# U21 X -> mark# X)
    (mark# U21 X -> mark# X, mark# U31(X1, X2) -> mark# X1)
    (mark# U21 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (mark# U21 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1)
    (mark# U21 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (mark# U21 X -> mark# X, mark# U42(X1, X2, X3) -> mark# X1)
    (mark# U21 X -> mark# X, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (mark# U12 X -> mark# X, mark# s X -> mark# X)
    (mark# U12 X -> mark# X, mark# plus(X1, X2) -> mark# X1)
    (mark# U12 X -> mark# X, mark# plus(X1, X2) -> mark# X2)
    (mark# U12 X -> mark# X, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (mark# U12 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
    (mark# U12 X -> mark# X, mark# U11(X1, X2) -> mark# X1)
    (mark# U12 X -> mark# X, mark# U12 X -> a__U12# mark X)
    (mark# U12 X -> mark# X, mark# U12 X -> mark# X)
    (mark# U12 X -> mark# X, mark# isNat X -> a__isNat# X)
    (mark# U12 X -> mark# X, mark# U21 X -> a__U21# mark X)
    (mark# U12 X -> mark# X, mark# U21 X -> mark# X)
    (mark# U12 X -> mark# X, mark# U31(X1, X2) -> mark# X1)
    (mark# U12 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (mark# U12 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1)
    (mark# U12 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (mark# U12 X -> mark# X, mark# U42(X1, X2, X3) -> mark# X1)
    (mark# U12 X -> mark# X, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (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# s V1 -> a__U21# 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__isNat# V1, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2))
    (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__isNat# V1)
    (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# s V1 -> a__U21# a__isNat V1)
    (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__isNat# V1)
    (a__U11#(tt(), V2) -> a__isNat# V2, a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2))
    (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), V2) -> a__U12# a__isNat V2)
    (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), V2) -> a__isNat# V2)
    (a__plus#(N, 0()) -> a__U31#(a__isNat N, N), a__U31#(tt(), N) -> mark# N)
    (a__U42#(tt(), M, N) -> mark# M, mark# s X -> mark# X)
    (a__U42#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> mark# X2)
    (a__U42#(tt(), M, N) -> mark# M, mark# plus(X1, X2) -> a__plus#(mark X1, mark X2))
    (a__U42#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> a__U11#(mark X1, X2))
    (a__U42#(tt(), M, N) -> mark# M, mark# U11(X1, X2) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# M, mark# U12 X -> a__U12# mark X)
    (a__U42#(tt(), M, N) -> mark# M, mark# U12 X -> mark# X)
    (a__U42#(tt(), M, N) -> mark# M, mark# isNat X -> a__isNat# X)
    (a__U42#(tt(), M, N) -> mark# M, mark# U21 X -> a__U21# mark X)
    (a__U42#(tt(), M, N) -> mark# M, mark# U21 X -> mark# X)
    (a__U42#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# M, mark# U31(X1, X2) -> a__U31#(mark X1, X2))
    (a__U42#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# M, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3))
    (a__U42#(tt(), M, N) -> mark# M, mark# U42(X1, X2, X3) -> mark# X1)
    (a__U42#(tt(), M, N) -> mark# M, mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3))
    (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> a__isNat# N)
    (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), M, N) -> a__U42#(a__isNat N, M, N))
   }
   STATUS:
    arrows: 0.764922
    SCCS (2):
     Scc:
      {            mark# s X -> mark# 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# U12 X -> mark# X,
                 mark# U21 X -> mark# X,
           mark# U31(X1, X2) -> mark# X1,
           mark# U31(X1, X2) -> a__U31#(mark X1, X2),
       mark# U41(X1, X2, X3) -> mark# X1,
       mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3),
       mark# U42(X1, X2, X3) -> mark# X1,
       mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3),
            a__U31#(tt(), N) -> mark# N,
         a__U42#(tt(), M, N) -> mark# N,
         a__U42#(tt(), M, N) -> mark# M,
         a__U42#(tt(), M, N) -> a__plus#(mark N, mark M),
         a__U41#(tt(), M, N) -> a__U42#(a__isNat N, M, N),
            a__plus#(N, s M) -> a__U41#(a__isNat M, M, N),
            a__plus#(N, 0()) -> a__U31#(a__isNat N, N)}
     Scc:
      {        a__isNat# s V1 -> a__isNat# V1,
       a__isNat# plus(V1, V2) -> a__isNat# V1,
       a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2),
            a__U11#(tt(), V2) -> a__isNat# V2}
     
     SCC (20):
      Strict:
       {            mark# s X -> mark# 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# U12 X -> mark# X,
                  mark# U21 X -> mark# X,
            mark# U31(X1, X2) -> mark# X1,
            mark# U31(X1, X2) -> a__U31#(mark X1, X2),
        mark# U41(X1, X2, X3) -> mark# X1,
        mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3),
        mark# U42(X1, X2, X3) -> mark# X1,
        mark# U42(X1, X2, X3) -> a__U42#(mark X1, X2, X3),
             a__U31#(tt(), N) -> mark# N,
          a__U42#(tt(), M, N) -> mark# N,
          a__U42#(tt(), M, N) -> mark# M,
          a__U42#(tt(), M, N) -> a__plus#(mark N, mark M),
          a__U41#(tt(), M, N) -> a__U42#(a__isNat N, M, N),
             a__plus#(N, s M) -> a__U41#(a__isNat M, M, N),
             a__plus#(N, 0()) -> a__U31#(a__isNat N, N)}
      Weak:
      {             a__U12 X -> U12 X,
                 a__U12 tt() -> tt(),
                  a__isNat X -> isNat X,
               a__isNat s V1 -> a__U21 a__isNat V1,
                a__isNat 0() -> tt(),
       a__isNat plus(V1, V2) -> a__U11(a__isNat V1, V2),
              a__U11(X1, X2) -> U11(X1, X2),
            a__U11(tt(), V2) -> a__U12 a__isNat V2,
                    a__U21 X -> U21 X,
                 a__U21 tt() -> tt(),
                   mark tt() -> tt(),
                    mark s X -> s mark X,
                    mark 0() -> 0(),
           mark plus(X1, X2) -> a__plus(mark X1, mark X2),
            mark U11(X1, X2) -> a__U11(mark X1, X2),
                  mark U12 X -> a__U12 mark X,
                mark isNat X -> a__isNat X,
                  mark U21 X -> a__U21 mark X,
            mark U31(X1, X2) -> a__U31(mark X1, X2),
        mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3),
        mark U42(X1, X2, X3) -> a__U42(mark X1, X2, X3),
              a__U31(X1, X2) -> U31(X1, X2),
             a__U31(tt(), N) -> mark N,
          a__U42(X1, X2, X3) -> U42(X1, X2, X3),
          a__U42(tt(), M, N) -> s a__plus(mark N, mark M),
          a__U41(X1, X2, X3) -> U41(X1, X2, X3),
          a__U41(tt(), M, N) -> a__U42(a__isNat N, M, N),
             a__plus(N, s M) -> a__U41(a__isNat M, M, N),
             a__plus(N, 0()) -> a__U31(a__isNat N, N),
             a__plus(X1, X2) -> plus(X1, X2)}
      Open
     
     
     
     
     
     
     
     SCC (4):
      Strict:
       {        a__isNat# s V1 -> a__isNat# V1,
        a__isNat# plus(V1, V2) -> a__isNat# V1,
        a__isNat# plus(V1, V2) -> a__U11#(a__isNat V1, V2),
             a__U11#(tt(), V2) -> a__isNat# V2}
      Weak:
      {             a__U12 X -> U12 X,
                 a__U12 tt() -> tt(),
                  a__isNat X -> isNat X,
               a__isNat s V1 -> a__U21 a__isNat V1,
                a__isNat 0() -> tt(),
       a__isNat plus(V1, V2) -> a__U11(a__isNat V1, V2),
              a__U11(X1, X2) -> U11(X1, X2),
            a__U11(tt(), V2) -> a__U12 a__isNat V2,
                    a__U21 X -> U21 X,
                 a__U21 tt() -> tt(),
                   mark tt() -> tt(),
                    mark s X -> s mark X,
                    mark 0() -> 0(),
           mark plus(X1, X2) -> a__plus(mark X1, mark X2),
            mark U11(X1, X2) -> a__U11(mark X1, X2),
                  mark U12 X -> a__U12 mark X,
                mark isNat X -> a__isNat X,
                  mark U21 X -> a__U21 mark X,
            mark U31(X1, X2) -> a__U31(mark X1, X2),
        mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3),
        mark U42(X1, X2, X3) -> a__U42(mark X1, X2, X3),
              a__U31(X1, X2) -> U31(X1, X2),
             a__U31(tt(), N) -> mark N,
          a__U42(X1, X2, X3) -> U42(X1, X2, X3),
          a__U42(tt(), M, N) -> s a__plus(mark N, mark M),
          a__U41(X1, X2, X3) -> U41(X1, X2, X3),
          a__U41(tt(), M, N) -> a__U42(a__isNat N, M, N),
             a__plus(N, s M) -> a__U41(a__isNat M, M, N),
             a__plus(N, 0()) -> a__U31(a__isNat N, N),
             a__plus(X1, X2) -> plus(X1, X2)}
      Open