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