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(U32(X1, X2)) -> active(U32(mark(X1), X2)),
            mark(U31(X1, X2, X3)) -> active(U31(mark(X1), X2, X3)),
                     mark(U33(X)) -> active(U33(mark(X))),
                mark(U41(X1, X2)) -> active(U41(mark(X1), X2)),
                       mark(s(X)) -> active(s(mark(X))),
               mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))),
            mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)),
                        mark(0()) -> active(0()),
                     mark(U61(X)) -> active(U61(mark(X))),
                  mark(x(X1, X2)) -> active(x(mark(X1), mark(X2))),
            mark(U71(X1, X2, X3)) -> active(U71(mark(X1), X2, X3)),
                mark(and(X1, X2)) -> active(and(mark(X1), X2)),
               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(isNat(x(V1, V2))) ->
  mark(U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)),
        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(U32(tt(), V2)) -> mark(U33(isNat(V2))),
        active(U31(tt(), V1, V2)) -> mark(U32(isNat(V1), V2)),
                active(U33(tt())) -> mark(tt()),
             active(U41(tt(), N)) -> mark(N),
            active(plus(N, s(M))) ->
  mark(
      U51(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N
      )
  ),
             active(plus(N, 0())) ->
  mark(U41(and(isNat(N), isNatKind(N)), N)),
          active(U51(tt(), M, N)) -> mark(s(plus(N, M))),
                active(U61(tt())) -> mark(0()),
               active(x(N, s(M))) ->
  mark(
      U71(and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), M, N
      )
  ),
                active(x(N, 0())) -> mark(U61(and(isNat(N), isNatKind(N)))),
          active(U71(tt(), M, N)) -> mark(plus(x(N, M), N)),
             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()),
     active(isNatKind(x(V1, V2))) -> mark(and(isNatKind(V1), isNatKind(V2))),
            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),
                U32(X1, mark(X2)) -> U32(X1, X2),
              U32(X1, active(X2)) -> U32(X1, X2),
                U32(mark(X1), X2) -> U32(X1, X2),
              U32(active(X1), X2) -> U32(X1, X2),
            U31(X1, X2, mark(X3)) -> U31(X1, X2, X3),
          U31(X1, X2, active(X3)) -> U31(X1, X2, X3),
            U31(X1, mark(X2), X3) -> U31(X1, X2, X3),
          U31(X1, active(X2), X3) -> U31(X1, X2, X3),
            U31(mark(X1), X2, X3) -> U31(X1, X2, X3),
          U31(active(X1), X2, X3) -> U31(X1, X2, X3),
                     U33(mark(X)) -> U33(X),
                   U33(active(X)) -> U33(X),
                U41(X1, mark(X2)) -> U41(X1, X2),
              U41(X1, active(X2)) -> U41(X1, X2),
                U41(mark(X1), X2) -> U41(X1, X2),
              U41(active(X1), X2) -> U41(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),
            U51(X1, X2, mark(X3)) -> U51(X1, X2, X3),
          U51(X1, X2, active(X3)) -> U51(X1, X2, X3),
            U51(X1, mark(X2), X3) -> U51(X1, X2, X3),
          U51(X1, active(X2), X3) -> U51(X1, X2, X3),
            U51(mark(X1), X2, X3) -> U51(X1, X2, X3),
          U51(active(X1), X2, X3) -> U51(X1, X2, X3),
                     U61(mark(X)) -> U61(X),
                   U61(active(X)) -> U61(X),
                  x(X1, mark(X2)) -> x(X1, X2),
                x(X1, active(X2)) -> x(X1, X2),
                  x(mark(X1), X2) -> x(X1, X2),
                x(active(X1), X2) -> x(X1, X2),
            U71(X1, X2, mark(X3)) -> U71(X1, X2, X3),
          U71(X1, X2, active(X3)) -> U71(X1, X2, X3),
            U71(X1, mark(X2), X3) -> U71(X1, X2, X3),
          U71(X1, active(X2), X3) -> U71(X1, X2, X3),
            U71(mark(X1), X2, X3) -> U71(X1, X2, X3),
          U71(active(X1), X2, X3) -> U71(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(U32(X1, X2)) -> active(U32(mark(X1), X2)),
              mark(U31(X1, X2, X3)) -> active(U31(mark(X1), X2, X3)),
                       mark(U33(X)) -> active(U33(mark(X))),
                  mark(U41(X1, X2)) -> active(U41(mark(X1), X2)),
                         mark(s(X)) -> active(s(mark(X))),
                 mark(plus(X1, X2)) -> active(plus(mark(X1), mark(X2))),
              mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)),
                          mark(0()) -> active(0()),
                       mark(U61(X)) -> active(U61(mark(X))),
                    mark(x(X1, X2)) -> active(x(mark(X1), mark(X2))),
              mark(U71(X1, X2, X3)) -> active(U71(mark(X1), X2, X3)),
                  mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                 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(isNat(x(V1, V2))) ->
    mark(U31(and(isNatKind(V1), isNatKind(V2)), V1, V2)),
          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(U32(tt(), V2)) -> mark(U33(isNat(V2))),
          active(U31(tt(), V1, V2)) -> mark(U32(isNat(V1), V2)),
                  active(U33(tt())) -> mark(tt()),
               active(U41(tt(), N)) -> mark(N),
              active(plus(N, s(M))) ->
    mark(
        U51(
           and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), 
           M, N
        )
    ),
               active(plus(N, 0())) ->
    mark(U41(and(isNat(N), isNatKind(N)), N)),
            active(U51(tt(), M, N)) -> mark(s(plus(N, M))),
                  active(U61(tt())) -> mark(0()),
                 active(x(N, s(M))) ->
    mark(
        U71(
           and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N))), 
           M, N
        )
    ),
                  active(x(N, 0())) -> mark(U61(and(isNat(N), isNatKind(N)))),
            active(U71(tt(), M, N)) -> mark(plus(x(N, M), N)),
               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()),
       active(isNatKind(x(V1, V2))) ->
    mark(and(isNatKind(V1), isNatKind(V2))),
              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),
                  U32(X1, mark(X2)) -> U32(X1, X2),
                U32(X1, active(X2)) -> U32(X1, X2),
                  U32(mark(X1), X2) -> U32(X1, X2),
                U32(active(X1), X2) -> U32(X1, X2),
              U31(X1, X2, mark(X3)) -> U31(X1, X2, X3),
            U31(X1, X2, active(X3)) -> U31(X1, X2, X3),
              U31(X1, mark(X2), X3) -> U31(X1, X2, X3),
            U31(X1, active(X2), X3) -> U31(X1, X2, X3),
              U31(mark(X1), X2, X3) -> U31(X1, X2, X3),
            U31(active(X1), X2, X3) -> U31(X1, X2, X3),
                       U33(mark(X)) -> U33(X),
                     U33(active(X)) -> U33(X),
                  U41(X1, mark(X2)) -> U41(X1, X2),
                U41(X1, active(X2)) -> U41(X1, X2),
                  U41(mark(X1), X2) -> U41(X1, X2),
                U41(active(X1), X2) -> U41(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),
              U51(X1, X2, mark(X3)) -> U51(X1, X2, X3),
            U51(X1, X2, active(X3)) -> U51(X1, X2, X3),
              U51(X1, mark(X2), X3) -> U51(X1, X2, X3),
            U51(X1, active(X2), X3) -> U51(X1, X2, X3),
              U51(mark(X1), X2, X3) -> U51(X1, X2, X3),
            U51(active(X1), X2, X3) -> U51(X1, X2, X3),
                       U61(mark(X)) -> U61(X),
                     U61(active(X)) -> U61(X),
                    x(X1, mark(X2)) -> x(X1, X2),
                  x(X1, active(X2)) -> x(X1, X2),
                    x(mark(X1), X2) -> x(X1, X2),
                  x(active(X1), X2) -> x(X1, X2),
              U71(X1, X2, mark(X3)) -> U71(X1, X2, X3),
            U71(X1, X2, active(X3)) -> U71(X1, X2, X3),
              U71(X1, mark(X2), X3) -> U71(X1, X2, X3),
            U71(X1, active(X2), X3) -> U71(X1, X2, X3),
              U71(mark(X1), X2, X3) -> U71(X1, X2, X3),
            U71(active(X1), X2, X3) -> U71(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