MAYBE
MAYBE
TRS:
 {
               U12(tt(), V2) -> U13(isNat(activate(V2))),
               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)),
         isNat(n__x(V1, V2)) ->
  U31(
     and(isNatKind(activate(V1)), n__isNatKind(activate(V2))), activate(V1),
     activate(V2)
  ),
                 activate(X) -> X,
            activate(n__0()) -> 0(),
   activate(n__isNatKind(X)) -> isNatKind(X),
   activate(n__plus(X1, X2)) -> plus(X1, X2),
           activate(n__s(X)) -> s(X),
      activate(n__x(X1, X2)) -> x(X1, X2),
    activate(n__and(X1, X2)) -> and(X1, X2),
           U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)),
                   U13(tt()) -> tt(),
                   U22(tt()) -> tt(),
               U21(tt(), V1) -> U22(isNat(activate(V1))),
               U32(tt(), V2) -> U33(isNat(activate(V2))),
           U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)),
                   U33(tt()) -> tt(),
                U41(tt(), N) -> activate(N),
                        s(X) -> n__s(X),
               plus(N, s(M)) ->
  U51(
     and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))),
     M, N
  ),
                plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N),
                plus(X1, X2) -> n__plus(X1, X2),
             U51(tt(), M, N) -> s(plus(activate(N), activate(M))),
                         0() -> n__0(),
                   U61(tt()) -> 0(),
                  x(N, s(M)) ->
  U71(
     and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))),
     M, N
  ),
                   x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))),
                   x(X1, X2) -> n__x(X1, X2),
             U71(tt(), M, N) ->
  plus(x(activate(N), activate(M)), activate(N)),
                 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)),
     isNatKind(n__x(V1, V2)) ->
  and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                 U12(tt(), V2) -> U13(isNat(activate(V2))),
                 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)),
           isNat(n__x(V1, V2)) ->
    U31(
       and(isNatKind(activate(V1)), n__isNatKind(activate(V2))),
       activate(V1), activate(V2)
    ),
                   activate(X) -> X,
              activate(n__0()) -> 0(),
     activate(n__isNatKind(X)) -> isNatKind(X),
     activate(n__plus(X1, X2)) -> plus(X1, X2),
             activate(n__s(X)) -> s(X),
        activate(n__x(X1, X2)) -> x(X1, X2),
      activate(n__and(X1, X2)) -> and(X1, X2),
             U11(tt(), V1, V2) -> U12(isNat(activate(V1)), activate(V2)),
                     U13(tt()) -> tt(),
                     U22(tt()) -> tt(),
                 U21(tt(), V1) -> U22(isNat(activate(V1))),
                 U32(tt(), V2) -> U33(isNat(activate(V2))),
             U31(tt(), V1, V2) -> U32(isNat(activate(V1)), activate(V2)),
                     U33(tt()) -> tt(),
                  U41(tt(), N) -> activate(N),
                          s(X) -> n__s(X),
                 plus(N, s(M)) ->
    U51(
       and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))),
       M, N
    ),
                  plus(N, 0()) -> U41(and(isNat(N), n__isNatKind(N)), N),
                  plus(X1, X2) -> n__plus(X1, X2),
               U51(tt(), M, N) -> s(plus(activate(N), activate(M))),
                           0() -> n__0(),
                     U61(tt()) -> 0(),
                    x(N, s(M)) ->
    U71(
       and(and(isNat(M), n__isNatKind(M)), n__and(isNat(N), n__isNatKind(N))),
       M, N
    ),
                     x(N, 0()) -> U61(and(isNat(N), n__isNatKind(N))),
                     x(X1, X2) -> n__x(X1, X2),
               U71(tt(), M, N) ->
    plus(x(activate(N), activate(M)), activate(N)),
                   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)),
       isNatKind(n__x(V1, V2)) ->
    and(isNatKind(activate(V1)), n__isNatKind(activate(V2)))
   }
  Fail