MAYBE
MAYBE
TRS:
 {
               U12(tt(), V2) -> U13(isNat(activate(V2))),
                    isNat(X) -> n__isNat(X),
               isNat(n__0()) -> tt(),
      isNat(n__plus(V1, V2)) ->
  U11(
     and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1),
     activate(V2)
  ),
             isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)),
                 activate(X) -> X,
            activate(n__0()) -> 0(),
   activate(n__isNatKind(X)) -> isNatKind(X),
   activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
           activate(n__s(X)) -> s(activate(X)),
    activate(n__and(X1, X2)) -> and(activate(X1), X2),
       activate(n__isNat(X)) -> isNat(X),
           U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)),
                   U13(tt()) -> tt(),
                   U22(tt()) -> tt(),
               U21(tt(), V1) -> U22(isNat(activate(V1))),
                U31(tt(), N) -> activate(N),
                        s(X) -> n__s(X),
               plus(N, s(M)) ->
  U41(
     and(and(isNat(M), n__isNatKind(M)), n__and(n__isNat(N), n__isNatKind(N))
     ), M, N
  ),
                plus(N, 0()) -> U31(and(isNat(N), n__isNatKind(N)), N),
                plus(X1, X2) -> n__plus(X1, X2),
             U41(tt(), M, N) -> s(plus(activate(N), activate(M))),
                 and(X1, X2) -> n__and(X1, X2),
                and(tt(), X) -> activate(X),
                isNatKind(X) -> n__isNatKind(X),
           isNatKind(n__0()) -> tt(),
  isNatKind(n__plus(V1, V2)) ->
  and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
         isNatKind(n__s(V1)) -> isNatKind(activate(V1)),
                         0() -> n__0()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                 U12(tt(), V2) -> U13(isNat(activate(V2))),
                      isNat(X) -> n__isNat(X),
                 isNat(n__0()) -> tt(),
        isNat(n__plus(V1, V2)) ->
    U11(
       and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
       activate(V1), activate(V2)
    ),
               isNat(n__s(V1)) -> U21(isNatKind(activate(V1)), activate(V1)),
                   activate(X) -> X,
              activate(n__0()) -> 0(),
     activate(n__isNatKind(X)) -> isNatKind(X),
     activate(n__plus(X1, X2)) -> plus(activate(X1), activate(X2)),
             activate(n__s(X)) -> s(activate(X)),
      activate(n__and(X1, X2)) -> and(activate(X1), X2),
         activate(n__isNat(X)) -> isNat(X),
             U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)),
                     U13(tt()) -> tt(),
                     U22(tt()) -> tt(),
                 U21(tt(), V1) -> U22(isNat(activate(V1))),
                  U31(tt(), N) -> activate(N),
                          s(X) -> n__s(X),
                 plus(N, s(M)) ->
    U41(
       and(
          and(isNat(M), n__isNatKind(M)),
          n__and(n__isNat(N), n__isNatKind(N))
       ), M, N
    ),
                  plus(N, 0()) -> U31(and(isNat(N), n__isNatKind(N)), N),
                  plus(X1, X2) -> n__plus(X1, X2),
               U41(tt(), M, N) -> s(plus(activate(N), activate(M))),
                   and(X1, X2) -> n__and(X1, X2),
                  and(tt(), X) -> activate(X),
                  isNatKind(X) -> n__isNatKind(X),
             isNatKind(n__0()) -> tt(),
    isNatKind(n__plus(V1, V2)) ->
    and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
           isNatKind(n__s(V1)) -> isNatKind(activate(V1)),
                           0() -> n__0()
   }
  Fail