MAYBE
Time: 0.015066
TRS:
 {              activate X -> X,
           activate n__0() -> 0(),
       activate n__isNat X -> isNat X,
  activate n__plus(X1, X2) -> plus(X1, X2),
           activate n__s X -> s X,
     activate n__x(X1, X2) -> x(X1, X2),
              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),
                       0() -> n__0(),
                  U31 tt() -> 0(),
                 x(N, s M) -> U41(and(isNat M, n__isNat N), M, N),
                 x(N, 0()) -> U31 isNat N,
                 x(X1, X2) -> n__x(X1, X2),
           U41(tt(), M, N) -> plus(x(activate N, activate M), activate N),
              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,
        isNat n__x(V1, V2) -> and(isNat activate V1, n__isNat activate V2)}
 DP:
  DP:
   {         activate# n__0() -> 0#(),
         activate# n__isNat X -> isNat# X,
    activate# n__plus(X1, X2) -> plus#(X1, X2),
             activate# n__s X -> s# X,
       activate# n__x(X1, X2) -> x#(X1, X2),
                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),
                    U31# tt() -> 0#(),
                   x#(N, s M) -> U41#(and(isNat M, n__isNat N), M, N),
                   x#(N, s M) -> and#(isNat M, n__isNat N),
                   x#(N, s M) -> isNat# M,
                   x#(N, 0()) -> U31# isNat N,
                   x#(N, 0()) -> isNat# N,
             U41#(tt(), M, N) -> activate# N,
             U41#(tt(), M, N) -> activate# M,
             U41#(tt(), M, N) -> plus#(x(activate N, activate M), activate N),
             U41#(tt(), M, N) -> x#(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,
          isNat# n__x(V1, V2) -> activate# V1,
          isNat# n__x(V1, V2) -> activate# V2,
          isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2),
          isNat# n__x(V1, V2) -> isNat# activate V1}
  TRS:
  {              activate X -> X,
            activate n__0() -> 0(),
        activate n__isNat X -> isNat X,
   activate n__plus(X1, X2) -> plus(X1, X2),
            activate n__s X -> s X,
      activate n__x(X1, X2) -> x(X1, X2),
               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),
                        0() -> n__0(),
                   U31 tt() -> 0(),
                  x(N, s M) -> U41(and(isNat M, n__isNat N), M, N),
                  x(N, 0()) -> U31 isNat N,
                  x(X1, X2) -> n__x(X1, X2),
            U41(tt(), M, N) -> plus(x(activate N, activate M), activate N),
               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,
         isNat n__x(V1, V2) -> and(isNat activate V1, n__isNat activate V2)}
  EDG:
   {
    (plus#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> isNat# activate V1)
    (plus#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (plus#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> activate# V2)
    (plus#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> activate# V1)
    (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)
    (x#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> isNat# activate V1)
    (x#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (x#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> activate# V2)
    (x#(N, s M) -> isNat# M, isNat# n__x(V1, V2) -> activate# V1)
    (x#(N, s M) -> isNat# M, isNat# n__s V1 -> isNat# activate V1)
    (x#(N, s M) -> isNat# M, isNat# n__s V1 -> activate# V1)
    (x#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> isNat# activate V1)
    (x#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (x#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V2)
    (x#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V1)
    (U11#(tt(), N) -> activate# N, activate# n__x(X1, X2) -> x#(X1, X2))
    (U11#(tt(), N) -> activate# N, activate# n__s X -> s# X)
    (U11#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2))
    (U11#(tt(), N) -> activate# N, activate# n__isNat X -> isNat# X)
    (U11#(tt(), N) -> activate# N, activate# n__0() -> 0#())
    (U21#(tt(), M, N) -> activate# N, activate# n__x(X1, X2) -> x#(X1, X2))
    (U21#(tt(), M, N) -> activate# N, activate# n__s X -> s# X)
    (U21#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2))
    (U21#(tt(), M, N) -> activate# N, activate# n__isNat X -> isNat# X)
    (U21#(tt(), M, N) -> activate# N, activate# n__0() -> 0#())
    (U41#(tt(), M, N) -> activate# N, activate# n__x(X1, X2) -> x#(X1, X2))
    (U41#(tt(), M, N) -> activate# N, activate# n__s X -> s# X)
    (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2))
    (U41#(tt(), M, N) -> activate# N, activate# n__isNat X -> isNat# X)
    (U41#(tt(), M, N) -> activate# N, activate# n__0() -> 0#())
    (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__x(V1, V2) -> isNat# activate V1)
    (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__x(V1, V2) -> activate# V2)
    (isNat# n__plus(V1, V2) -> isNat# activate V1, isNat# n__x(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)
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__x(V1, V2) -> isNat# activate V1)
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__x(V1, V2) -> activate# V2)
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__x(V1, V2) -> activate# V1)
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1)
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNat# activate V1)
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2)
    (isNat# n__x(V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V1)
    (plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N), U21#(tt(), M, N) -> plus#(activate 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) -> activate# M)
    (plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N), U21#(tt(), M, N) -> activate# N)
    (x#(N, 0()) -> U31# isNat N, U31# tt() -> 0#())
    (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))
    (U41#(tt(), M, N) -> plus#(x(activate N, activate M), activate N), plus#(N, 0()) -> isNat# N)
    (U41#(tt(), M, N) -> plus#(x(activate N, activate M), activate N), plus#(N, 0()) -> U11#(isNat N, N))
    (U41#(tt(), M, N) -> plus#(x(activate N, activate M), activate N), plus#(N, s M) -> isNat# M)
    (U41#(tt(), M, N) -> plus#(x(activate N, activate M), activate N), plus#(N, s M) -> and#(isNat M, n__isNat N))
    (U41#(tt(), M, N) -> plus#(x(activate N, activate M), activate N), plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N))
    (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, 0()) -> isNat# N)
    (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, 0()) -> U11#(isNat N, N))
    (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, s M) -> isNat# M)
    (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, s M) -> and#(isNat M, n__isNat N))
    (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, s M) -> U21#(and(isNat M, n__isNat N), M, N))
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2))
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# X)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2))
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
    (isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2), and#(tt(), X) -> activate# X)
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2))
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# X)
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2))
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__0() -> 0#())
    (isNat# n__x(V1, V2) -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2))
    (isNat# n__x(V1, V2) -> activate# V1, activate# n__s X -> s# X)
    (isNat# n__x(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2))
    (isNat# n__x(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNat# n__x(V1, V2) -> activate# V1, activate# n__0() -> 0#())
    (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#())
    (isNat# n__s V1 -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2))
    (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X)
    (isNat# n__s V1 -> activate# V1, activate# n__x(X1, X2) -> x#(X1, X2))
    (isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2), and#(tt(), X) -> activate# X)
    (isNat# n__x(V1, V2) -> activate# V2, activate# n__0() -> 0#())
    (isNat# n__x(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
    (isNat# n__x(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2))
    (isNat# n__x(V1, V2) -> activate# V2, activate# n__s X -> s# X)
    (isNat# n__x(V1, V2) -> activate# V2, activate# n__x(X1, X2) -> x#(X1, X2))
    (activate# n__x(X1, X2) -> x#(X1, X2), x#(N, s M) -> U41#(and(isNat M, n__isNat N), M, N))
    (activate# n__x(X1, X2) -> x#(X1, X2), x#(N, s M) -> and#(isNat M, n__isNat N))
    (activate# n__x(X1, X2) -> x#(X1, X2), x#(N, s M) -> isNat# M)
    (activate# n__x(X1, X2) -> x#(X1, X2), x#(N, 0()) -> U31# isNat N)
    (activate# n__x(X1, X2) -> x#(X1, X2), x#(N, 0()) -> isNat# N)
    (U41#(tt(), M, N) -> x#(activate N, activate M), x#(N, s M) -> U41#(and(isNat M, n__isNat N), M, N))
    (U41#(tt(), M, N) -> x#(activate N, activate M), x#(N, s M) -> and#(isNat M, n__isNat N))
    (U41#(tt(), M, N) -> x#(activate N, activate M), x#(N, s M) -> isNat# M)
    (U41#(tt(), M, N) -> x#(activate N, activate M), x#(N, 0()) -> U31# isNat N)
    (U41#(tt(), M, N) -> x#(activate N, activate M), x#(N, 0()) -> isNat# N)
    (x#(N, s M) -> and#(isNat M, n__isNat N), and#(tt(), X) -> activate# X)
    (plus#(N, s M) -> and#(isNat M, n__isNat N), and#(tt(), X) -> activate# X)
    (x#(N, s M) -> U41#(and(isNat M, n__isNat N), M, N), U41#(tt(), M, N) -> activate# N)
    (x#(N, s M) -> U41#(and(isNat M, n__isNat N), M, N), U41#(tt(), M, N) -> activate# M)
    (x#(N, s M) -> U41#(and(isNat M, n__isNat N), M, N), U41#(tt(), M, N) -> plus#(x(activate N, activate M), activate N))
    (x#(N, s M) -> U41#(and(isNat M, n__isNat N), M, N), U41#(tt(), M, N) -> x#(activate N, activate M))
    (plus#(N, 0()) -> U11#(isNat N, N), U11#(tt(), N) -> activate# N)
    (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)
    (isNat# n__s V1 -> isNat# activate V1, isNat# n__x(V1, V2) -> activate# V1)
    (isNat# n__s V1 -> isNat# activate V1, isNat# n__x(V1, V2) -> activate# V2)
    (isNat# n__s V1 -> isNat# activate V1, isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (isNat# n__s V1 -> isNat# activate V1, isNat# n__x(V1, V2) -> isNat# activate V1)
    (x#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V1)
    (x#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V2)
    (x#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (x#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> isNat# activate V1)
    (x#(N, 0()) -> isNat# N, isNat# n__s V1 -> activate# V1)
    (x#(N, 0()) -> isNat# N, isNat# n__s V1 -> isNat# activate V1)
    (x#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> activate# V1)
    (x#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> activate# V2)
    (x#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (x#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> isNat# activate V1)
    (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V1)
    (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V2)
    (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) -> isNat# activate V1)
    (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> activate# V1)
    (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> isNat# activate V1)
    (plus#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> activate# V1)
    (plus#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> activate# V2)
    (plus#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (plus#(N, 0()) -> isNat# N, isNat# n__x(V1, V2) -> isNat# activate V1)
    (U41#(tt(), M, N) -> activate# M, activate# n__0() -> 0#())
    (U41#(tt(), M, N) -> activate# M, activate# n__isNat X -> isNat# X)
    (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(X1, X2))
    (U41#(tt(), M, N) -> activate# M, activate# n__s X -> s# X)
    (U41#(tt(), M, N) -> activate# M, activate# n__x(X1, X2) -> x#(X1, X2))
    (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) -> plus#(X1, X2))
    (U21#(tt(), M, N) -> activate# M, activate# n__s X -> s# X)
    (U21#(tt(), M, N) -> activate# M, activate# n__x(X1, X2) -> x#(X1, X2))
    (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) -> plus#(X1, X2))
    (and#(tt(), X) -> activate# X, activate# n__s X -> s# X)
    (and#(tt(), X) -> activate# X, activate# n__x(X1, X2) -> x#(X1, X2))
    (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)
    (activate# n__isNat X -> isNat# X, isNat# n__x(V1, V2) -> activate# V1)
    (activate# n__isNat X -> isNat# X, isNat# n__x(V1, V2) -> activate# V2)
    (activate# n__isNat X -> isNat# X, isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2))
    (activate# n__isNat X -> isNat# X, isNat# n__x(V1, V2) -> isNat# activate V1)
   }
   STATUS:
    arrows: 0.865741
    SCCS (1):
     Scc:
      {     activate# n__isNat X -> isNat# X,
       activate# n__plus(X1, X2) -> plus#(X1, X2),
          activate# n__x(X1, X2) -> x#(X1, X2),
                   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),
                      x#(N, s M) -> U41#(and(isNat M, n__isNat N), M, N),
                      x#(N, s M) -> and#(isNat M, n__isNat N),
                      x#(N, s M) -> isNat# M,
                      x#(N, 0()) -> isNat# N,
                U41#(tt(), M, N) -> activate# N,
                U41#(tt(), M, N) -> activate# M,
                U41#(tt(), M, N) -> plus#(x(activate N, activate M), activate N),
                U41#(tt(), M, N) -> x#(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,
             isNat# n__x(V1, V2) -> activate# V1,
             isNat# n__x(V1, V2) -> activate# V2,
             isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2),
             isNat# n__x(V1, V2) -> isNat# activate V1}
     
     SCC (31):
      Strict:
       {     activate# n__isNat X -> isNat# X,
        activate# n__plus(X1, X2) -> plus#(X1, X2),
           activate# n__x(X1, X2) -> x#(X1, X2),
                    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),
                       x#(N, s M) -> U41#(and(isNat M, n__isNat N), M, N),
                       x#(N, s M) -> and#(isNat M, n__isNat N),
                       x#(N, s M) -> isNat# M,
                       x#(N, 0()) -> isNat# N,
                 U41#(tt(), M, N) -> activate# N,
                 U41#(tt(), M, N) -> activate# M,
                 U41#(tt(), M, N) -> plus#(x(activate N, activate M), activate N),
                 U41#(tt(), M, N) -> x#(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,
              isNat# n__x(V1, V2) -> activate# V1,
              isNat# n__x(V1, V2) -> activate# V2,
              isNat# n__x(V1, V2) -> and#(isNat activate V1, n__isNat activate V2),
              isNat# n__x(V1, V2) -> isNat# activate V1}
      Weak:
      {              activate X -> X,
                activate n__0() -> 0(),
            activate n__isNat X -> isNat X,
       activate n__plus(X1, X2) -> plus(X1, X2),
                activate n__s X -> s X,
          activate n__x(X1, X2) -> x(X1, X2),
                   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),
                            0() -> n__0(),
                       U31 tt() -> 0(),
                      x(N, s M) -> U41(and(isNat M, n__isNat N), M, N),
                      x(N, 0()) -> U31 isNat N,
                      x(X1, X2) -> n__x(X1, X2),
                U41(tt(), M, N) -> plus(x(activate N, activate M), activate N),
                   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,
             isNat n__x(V1, V2) -> and(isNat activate V1, n__isNat activate V2)}
      Open