MAYBE
Time: 14.557292
TRS:
 {              activate X -> X,
           activate n__0() -> 0(),
       activate n__isNat X -> isNat X,
  activate n__plus(X1, X2) -> plus(activate X1, activate X2),
           activate n__s X -> s activate X,
              U11(tt(), N) -> activate N,
                       s X -> n__s X,
              plus(N, s M) -> U21(and(isNat M, n__isNat N), M, N),
              plus(N, 0()) -> U11(isNat N, N),
              plus(X1, X2) -> n__plus(X1, X2),
           U21(tt(), M, N) -> s plus(activate N, activate M),
              and(tt(), X) -> activate X,
                   isNat X -> n__isNat X,
              isNat n__0() -> tt(),
     isNat n__plus(V1, V2) -> and(isNat activate V1, n__isNat activate V2),
             isNat n__s V1 -> isNat activate V1,
                       0() -> n__0()}
 DP:
  DP:
   {         activate# n__0() -> 0#(),
         activate# n__isNat X -> isNat# X,
    activate# n__plus(X1, X2) -> activate# X1,
    activate# n__plus(X1, X2) -> activate# X2,
    activate# n__plus(X1, X2) -> plus#(activate X1, activate X2),
             activate# n__s X -> activate# X,
             activate# n__s X -> s# activate X,
                U11#(tt(), N) -> activate# N,
                plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N),
                plus#(N, s M) -> and#(isNat M, n__isNat N),
                plus#(N, s M) -> isNat# M,
                plus#(N, 0()) -> U11#(isNat N, N),
                plus#(N, 0()) -> isNat# N,
             U21#(tt(), M, N) -> activate# N,
             U21#(tt(), M, N) -> activate# M,
             U21#(tt(), M, N) -> s# plus(activate N, activate M),
             U21#(tt(), M, N) -> plus#(activate N, activate M),
                and#(tt(), X) -> activate# X,
       isNat# n__plus(V1, V2) -> activate# V1,
       isNat# n__plus(V1, V2) -> activate# V2,
       isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2),
       isNat# n__plus(V1, V2) -> isNat# activate V1,
               isNat# n__s V1 -> activate# V1,
               isNat# n__s V1 -> isNat# activate V1}
  TRS:
  {              activate X -> X,
            activate n__0() -> 0(),
        activate n__isNat X -> isNat X,
   activate n__plus(X1, X2) -> plus(activate X1, activate X2),
            activate n__s X -> s activate X,
               U11(tt(), N) -> activate N,
                        s X -> n__s X,
               plus(N, s M) -> U21(and(isNat M, n__isNat N), M, N),
               plus(N, 0()) -> U11(isNat N, N),
               plus(X1, X2) -> n__plus(X1, X2),
            U21(tt(), M, N) -> s plus(activate N, activate M),
               and(tt(), X) -> activate X,
                    isNat X -> n__isNat X,
               isNat n__0() -> tt(),
      isNat n__plus(V1, V2) -> and(isNat activate V1, n__isNat activate V2),
              isNat n__s V1 -> isNat activate V1,
                        0() -> n__0()}
  UR:
   {              activate X -> X,
             activate n__0() -> 0(),
         activate n__isNat X -> isNat X,
    activate n__plus(X1, X2) -> plus(activate X1, activate X2),
             activate n__s X -> s activate X,
                U11(tt(), N) -> activate N,
                         s X -> n__s X,
                plus(N, s M) -> U21(and(isNat M, n__isNat N), M, N),
                plus(N, 0()) -> U11(isNat N, N),
                plus(X1, X2) -> n__plus(X1, X2),
             U21(tt(), M, N) -> s plus(activate N, activate M),
                and(tt(), X) -> activate X,
                     isNat X -> n__isNat X,
                isNat n__0() -> tt(),
       isNat n__plus(V1, V2) -> and(isNat activate V1, n__isNat activate V2),
               isNat n__s V1 -> isNat activate V1,
                         0() -> n__0(),
                     a(x, y) -> x,
                     a(x, y) -> y}
   EDG:
    {(activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
     (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X1)
     (activate# n__s X -> activate# X, activate# n__isNat X -> isNat# X)
     (activate# n__s X -> activate# X, activate# n__0() -> 0#())
     (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> isNat# activate V1)
     (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> activate# V1)
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> isNat# activate V1)
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V2)
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V1)
     (isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2), and#(tt(), X) -> activate# X)
     (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> isNat# activate V1)
     (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> activate# V1)
     (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> isNat# activate V1)
     (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
     (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V2)
     (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V1)
     (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1)
     (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
     (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNat# activate V1)
     (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
     (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2)
     (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V1)
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> isNat# N)
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> U11#(isNat N, N))
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> isNat# M)
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> and#(isNat M, n__isNat N))
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N))
     (U21#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, 0()) -> isNat# N)
     (U21#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, 0()) -> U11#(isNat N, N))
     (U21#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> isNat# M)
     (U21#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> and#(isNat M, n__isNat N))
     (U21#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N))
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> activate# X)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (plus#(N, 0()) -> U11#(isNat N, N), U11#(tt(), N) -> activate# N)
     (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# activate X)
     (isNat# n__s V1 -> activate# V1, activate# n__s X -> activate# X)
     (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
     (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
     (isNat# n__s V1 -> activate# V1, activate# n__isNat X -> isNat# X)
     (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#())
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> activate# X)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__0() -> 0#())
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__isNat X -> isNat# X)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X1)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X2)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
     (plus#(N, s M) -> and#(isNat M, n__isNat N), and#(tt(), X) -> activate# X)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__0() -> 0#())
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__isNat X -> isNat# X)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X1)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X2)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> activate# X)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> s# activate X)
     (plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N), U21#(tt(), M, N) -> activate# N)
     (plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N), U21#(tt(), M, N) -> activate# M)
     (plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N), U21#(tt(), M, N) -> s# plus(activate N, activate M))
     (plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N), U21#(tt(), M, N) -> plus#(activate N, activate M))
     (isNat# n__s V1 -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V1)
     (isNat# n__s V1 -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2)
     (isNat# n__s V1 -> isNat# activate V1, isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
     (isNat# n__s V1 -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNat# activate V1)
     (isNat# n__s V1 -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
     (isNat# n__s V1 -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1)
     (U21#(tt(), M, N) -> activate# N, activate# n__0() -> 0#())
     (U21#(tt(), M, N) -> activate# N, activate# n__isNat X -> isNat# X)
     (U21#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> activate# X1)
     (U21#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
     (U21#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U21#(tt(), M, N) -> activate# N, activate# n__s X -> activate# X)
     (U21#(tt(), M, N) -> activate# N, activate# n__s X -> s# activate X)
     (U11#(tt(), N) -> activate# N, activate# n__0() -> 0#())
     (U11#(tt(), N) -> activate# N, activate# n__isNat X -> isNat# X)
     (U11#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X1)
     (U11#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
     (U11#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U11#(tt(), N) -> activate# N, activate# n__s X -> activate# X)
     (U11#(tt(), N) -> activate# N, activate# n__s X -> s# activate X)
     (U21#(tt(), M, N) -> activate# M, activate# n__0() -> 0#())
     (U21#(tt(), M, N) -> activate# M, activate# n__isNat X -> isNat# X)
     (U21#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X1)
     (U21#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X2)
     (U21#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U21#(tt(), M, N) -> activate# M, activate# n__s X -> activate# X)
     (U21#(tt(), M, N) -> activate# M, activate# n__s X -> s# activate X)
     (and#(tt(), X) -> activate# X, activate# n__0() -> 0#())
     (and#(tt(), X) -> activate# X, activate# n__isNat X -> isNat# X)
     (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> activate# X1)
     (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
     (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (and#(tt(), X) -> activate# X, activate# n__s X -> activate# X)
     (and#(tt(), X) -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V1)
     (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V2)
     (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
     (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> isNat# activate V1)
     (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> activate# V1)
     (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> isNat# activate V1)}
    STATUS:
     arrows: 0.796875
     SCCS (1):
      Scc:
       {     activate# n__isNat X -> isNat# X,
        activate# n__plus(X1, X2) -> activate# X1,
        activate# n__plus(X1, X2) -> activate# X2,
        activate# n__plus(X1, X2) -> plus#(activate X1, activate X2),
                 activate# n__s X -> activate# X,
                    U11#(tt(), N) -> activate# N,
                    plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N),
                    plus#(N, s M) -> and#(isNat M, n__isNat N),
                    plus#(N, s M) -> isNat# M,
                    plus#(N, 0()) -> U11#(isNat N, N),
                    plus#(N, 0()) -> isNat# N,
                 U21#(tt(), M, N) -> activate# N,
                 U21#(tt(), M, N) -> activate# M,
                 U21#(tt(), M, N) -> plus#(activate N, activate M),
                    and#(tt(), X) -> activate# X,
           isNat# n__plus(V1, V2) -> activate# V1,
           isNat# n__plus(V1, V2) -> activate# V2,
           isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2),
           isNat# n__plus(V1, V2) -> isNat# activate V1,
                   isNat# n__s V1 -> activate# V1,
                   isNat# n__s V1 -> isNat# activate V1}
      
      SCC (21):
       Strict:
        {     activate# n__isNat X -> isNat# X,
         activate# n__plus(X1, X2) -> activate# X1,
         activate# n__plus(X1, X2) -> activate# X2,
         activate# n__plus(X1, X2) -> plus#(activate X1, activate X2),
                  activate# n__s X -> activate# X,
                     U11#(tt(), N) -> activate# N,
                     plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N),
                     plus#(N, s M) -> and#(isNat M, n__isNat N),
                     plus#(N, s M) -> isNat# M,
                     plus#(N, 0()) -> U11#(isNat N, N),
                     plus#(N, 0()) -> isNat# N,
                  U21#(tt(), M, N) -> activate# N,
                  U21#(tt(), M, N) -> activate# M,
                  U21#(tt(), M, N) -> plus#(activate N, activate M),
                     and#(tt(), X) -> activate# X,
            isNat# n__plus(V1, V2) -> activate# V1,
            isNat# n__plus(V1, V2) -> activate# V2,
            isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2),
            isNat# n__plus(V1, V2) -> isNat# activate V1,
                    isNat# n__s V1 -> activate# V1,
                    isNat# n__s V1 -> isNat# activate V1}
       Weak:
       {              activate X -> X,
                 activate n__0() -> 0(),
             activate n__isNat X -> isNat X,
        activate n__plus(X1, X2) -> plus(activate X1, activate X2),
                 activate n__s X -> s activate X,
                    U11(tt(), N) -> activate N,
                             s X -> n__s X,
                    plus(N, s M) -> U21(and(isNat M, n__isNat N), M, N),
                    plus(N, 0()) -> U11(isNat N, N),
                    plus(X1, X2) -> n__plus(X1, X2),
                 U21(tt(), M, N) -> s plus(activate N, activate M),
                    and(tt(), X) -> activate X,
                         isNat X -> n__isNat X,
                    isNat n__0() -> tt(),
           isNat n__plus(V1, V2) -> and(isNat activate V1, n__isNat activate V2),
                   isNat n__s V1 -> isNat activate V1,
                             0() -> n__0()}
       Open