MAYBE
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:
  Strict:
   {         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))}
  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)))}
  EDG:
   {
    (isNat#(n__x(V1, V2)) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (isNat#(n__x(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(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__isNat(X)) -> isNat#(X))
    (isNat#(n__x(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#())
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__plus(X1, X2)) -> plus#(X1, X2))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(X))
    (isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#())
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__x(V1, V2)) -> isNat#(activate(V1)))
    (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)) -> activate#(V2))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__x(V1, V2)) -> activate#(V1))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> isNat#(activate(V1)))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__s(V1)) -> activate#(V1))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
    (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)) -> activate#(V2))
    (activate#(n__isNat(X)) -> isNat#(X), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (and#(tt(), X) -> activate#(X), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (and#(tt(), X) -> activate#(X), activate#(n__s(X)) -> s#(X))
    (and#(tt(), X) -> activate#(X), activate#(n__plus(X1, X2)) -> plus#(X1, X2))
    (and#(tt(), X) -> activate#(X), activate#(n__isNat(X)) -> isNat#(X))
    (and#(tt(), X) -> activate#(X), activate#(n__0()) -> 0#())
    (U21#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__isNat(X)) -> isNat#(X))
    (U21#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#())
    (U41#(tt(), M, N) -> activate#(M), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (U41#(tt(), M, N) -> activate#(M), activate#(n__s(X)) -> s#(X))
    (U41#(tt(), M, N) -> activate#(M), activate#(n__plus(X1, X2)) -> plus#(X1, X2))
    (U41#(tt(), M, N) -> activate#(M), activate#(n__isNat(X)) -> isNat#(X))
    (U41#(tt(), M, N) -> activate#(M), activate#(n__0()) -> 0#())
    (plus#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> isNat#(activate(V1)))
    (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)) -> activate#(V2))
    (plus#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> activate#(V1))
    (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))
    (x#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> isNat#(activate(V1)))
    (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)) -> activate#(V2))
    (x#(N, 0()) -> isNat#(N), isNat#(n__x(V1, V2)) -> activate#(V1))
    (x#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> isNat#(activate(V1)))
    (x#(N, 0()) -> isNat#(N), isNat#(n__s(V1)) -> activate#(V1))
    (x#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
    (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)) -> activate#(V2))
    (x#(N, 0()) -> isNat#(N), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> isNat#(activate(V1)))
    (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)) -> activate#(V2))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> 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__s(V1)) -> activate#(V1))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)))
    (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)) -> activate#(V2))
    (isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (plus#(N, 0()) -> U11#(isNat(N), N), U11#(tt(), N) -> activate#(N))
    (plus#(N, s(M)) -> and#(isNat(M), n__isNat(N)), and#(tt(), X) -> activate#(X))
    (x#(N, s(M)) -> and#(isNat(M), n__isNat(N)), and#(tt(), X) -> activate#(X))
    (U41#(tt(), M, N) -> x#(activate(N), activate(M)), x#(N, 0()) -> isNat#(N))
    (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, s(M)) -> isNat#(M))
    (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)) -> U41#(and(isNat(M), n__isNat(N)), M, N))
    (activate#(n__x(X1, X2)) -> x#(X1, X2), x#(N, 0()) -> isNat#(N))
    (activate#(n__x(X1, X2)) -> x#(X1, X2), x#(N, 0()) -> U31#(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, s(M)) -> and#(isNat(M), n__isNat(N)))
    (activate#(n__x(X1, X2)) -> x#(X1, X2), x#(N, s(M)) -> U41#(and(isNat(M), n__isNat(N)), M, N))
    (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)) -> 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) -> activate#(M))
    (x#(N, s(M)) -> U41#(and(isNat(M), n__isNat(N)), M, N), U41#(tt(), M, N) -> activate#(N))
    (isNat#(n__x(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))), and#(tt(), X) -> activate#(X))
    (isNat#(n__plus(V1, V2)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))), and#(tt(), X) -> 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)))
    (activate#(n__plus(X1, X2)) -> plus#(X1, X2), plus#(N, s(M)) -> U21#(and(isNat(M), n__isNat(N)), M, N))
    (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)) -> isNat#(M))
    (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, 0()) -> 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))
    (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)) -> isNat#(M))
    (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, 0()) -> isNat#(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) -> 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)) -> isNat#(M))
    (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, 0()) -> isNat#(N))
    (x#(N, 0()) -> U31#(isNat(N)), U31#(tt()) -> 0#())
    (isNat#(n__x(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (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)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
    (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__s(V1)) -> 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__x(V1, V2)) -> activate#(V1))
    (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)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
    (isNat#(n__x(V1, V2)) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> isNat#(activate(V1)))
    (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (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)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
    (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__s(V1)) -> 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__x(V1, V2)) -> activate#(V1))
    (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)) -> and#(isNat(activate(V1)), n__isNat(activate(V2))))
    (isNat#(n__plus(V1, V2)) -> isNat#(activate(V1)), isNat#(n__x(V1, V2)) -> isNat#(activate(V1)))
    (U41#(tt(), M, N) -> activate#(N), activate#(n__0()) -> 0#())
    (U41#(tt(), M, N) -> activate#(N), activate#(n__isNat(X)) -> isNat#(X))
    (U41#(tt(), M, N) -> activate#(N), activate#(n__plus(X1, X2)) -> plus#(X1, X2))
    (U41#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X))
    (U41#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (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)) -> plus#(X1, X2))
    (U21#(tt(), M, N) -> activate#(N), activate#(n__s(X)) -> s#(X))
    (U21#(tt(), M, N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (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)) -> plus#(X1, X2))
    (U11#(tt(), N) -> activate#(N), activate#(n__s(X)) -> s#(X))
    (U11#(tt(), N) -> activate#(N), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (x#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (x#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V2))
    (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)) -> isNat#(activate(V1)))
    (x#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> activate#(V1))
    (x#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> isNat#(activate(V1)))
    (x#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> activate#(V1))
    (x#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> activate#(V2))
    (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)) -> isNat#(activate(V1)))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V1))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__plus(V1, V2)) -> activate#(V2))
    (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)) -> isNat#(activate(V1)))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> activate#(V1))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__s(V1)) -> isNat#(activate(V1)))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> activate#(V1))
    (plus#(N, s(M)) -> isNat#(M), isNat#(n__x(V1, V2)) -> activate#(V2))
    (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)) -> isNat#(activate(V1)))
    (isNat#(n__x(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#())
    (isNat#(n__x(V1, V2)) -> activate#(V1), activate#(n__isNat(X)) -> isNat#(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__s(X)) -> s#(X))
    (isNat#(n__x(V1, V2)) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (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)) -> plus#(X1, X2))
    (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X))
    (isNat#(n__plus(V1, V2)) -> activate#(V1), activate#(n__x(X1, X2)) -> x#(X1, X2))
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#())
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__isNat(X)) -> isNat#(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__s(X)) -> s#(X))
    (isNat#(n__plus(V1, V2)) -> activate#(V2), activate#(n__x(X1, X2)) -> x#(X1, X2))
   }
   SCCS:
    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:
     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)))}
     Fail