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