MAYBE
MAYBE
TRS:
 {
                mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                         mark(0()) -> active(0()),
                     mark(zeros()) -> active(zeros()),
                        mark(s(X)) -> active(s(mark(X))),
                   mark(length(X)) -> active(length(mark(X))),
                 mark(U11(X1, X2)) -> active(U11(mark(X1), X2)),
                        mark(tt()) -> active(tt()),
                 mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                    mark(isNat(X)) -> active(isNat(X)),
                mark(isNatList(X)) -> active(isNatList(X)),
               mark(isNatIList(X)) -> active(isNatIList(X)),
                       mark(nil()) -> active(nil()),
                cons(X1, mark(X2)) -> cons(X1, X2),
              cons(X1, active(X2)) -> cons(X1, X2),
                cons(mark(X1), X2) -> cons(X1, X2),
              cons(active(X1), X2) -> cons(X1, X2),
                   active(zeros()) -> mark(cons(0(), zeros())),
        active(length(cons(N, L))) ->
  mark(U11(and(isNatList(L), isNat(N)), L)),
             active(length(nil())) -> mark(0()),
              active(U11(tt(), L)) -> mark(s(length(L))),
              active(and(tt(), X)) -> mark(X),
                active(isNat(0())) -> mark(tt()),
              active(isNat(s(V1))) -> mark(isNat(V1)),
         active(isNat(length(V1))) -> mark(isNatList(V1)),
   active(isNatList(cons(V1, V2))) -> mark(and(isNat(V1), isNatList(V2))),
          active(isNatList(nil())) -> mark(tt()),
             active(isNatIList(V)) -> mark(isNatList(V)),
  active(isNatIList(cons(V1, V2))) -> mark(and(isNat(V1), isNatIList(V2))),
       active(isNatIList(zeros())) -> mark(tt()),
                        s(mark(X)) -> s(X),
                      s(active(X)) -> s(X),
                   length(mark(X)) -> length(X),
                 length(active(X)) -> length(X),
                 U11(X1, mark(X2)) -> U11(X1, X2),
               U11(X1, active(X2)) -> U11(X1, X2),
                 U11(mark(X1), X2) -> U11(X1, X2),
               U11(active(X1), X2) -> U11(X1, X2),
                 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),
                    isNat(mark(X)) -> isNat(X),
                  isNat(active(X)) -> isNat(X),
                isNatList(mark(X)) -> isNatList(X),
              isNatList(active(X)) -> isNatList(X),
               isNatIList(mark(X)) -> isNatIList(X),
             isNatIList(active(X)) -> isNatIList(X)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                  mark(cons(X1, X2)) -> active(cons(mark(X1), X2)),
                           mark(0()) -> active(0()),
                       mark(zeros()) -> active(zeros()),
                          mark(s(X)) -> active(s(mark(X))),
                     mark(length(X)) -> active(length(mark(X))),
                   mark(U11(X1, X2)) -> active(U11(mark(X1), X2)),
                          mark(tt()) -> active(tt()),
                   mark(and(X1, X2)) -> active(and(mark(X1), X2)),
                      mark(isNat(X)) -> active(isNat(X)),
                  mark(isNatList(X)) -> active(isNatList(X)),
                 mark(isNatIList(X)) -> active(isNatIList(X)),
                         mark(nil()) -> active(nil()),
                  cons(X1, mark(X2)) -> cons(X1, X2),
                cons(X1, active(X2)) -> cons(X1, X2),
                  cons(mark(X1), X2) -> cons(X1, X2),
                cons(active(X1), X2) -> cons(X1, X2),
                     active(zeros()) -> mark(cons(0(), zeros())),
          active(length(cons(N, L))) ->
    mark(U11(and(isNatList(L), isNat(N)), L)),
               active(length(nil())) -> mark(0()),
                active(U11(tt(), L)) -> mark(s(length(L))),
                active(and(tt(), X)) -> mark(X),
                  active(isNat(0())) -> mark(tt()),
                active(isNat(s(V1))) -> mark(isNat(V1)),
           active(isNat(length(V1))) -> mark(isNatList(V1)),
     active(isNatList(cons(V1, V2))) -> mark(and(isNat(V1), isNatList(V2))),
            active(isNatList(nil())) -> mark(tt()),
               active(isNatIList(V)) -> mark(isNatList(V)),
    active(isNatIList(cons(V1, V2))) -> mark(and(isNat(V1), isNatIList(V2))),
         active(isNatIList(zeros())) -> mark(tt()),
                          s(mark(X)) -> s(X),
                        s(active(X)) -> s(X),
                     length(mark(X)) -> length(X),
                   length(active(X)) -> length(X),
                   U11(X1, mark(X2)) -> U11(X1, X2),
                 U11(X1, active(X2)) -> U11(X1, X2),
                   U11(mark(X1), X2) -> U11(X1, X2),
                 U11(active(X1), X2) -> U11(X1, X2),
                   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),
                      isNat(mark(X)) -> isNat(X),
                    isNat(active(X)) -> isNat(X),
                  isNatList(mark(X)) -> isNatList(X),
                isNatList(active(X)) -> isNatList(X),
                 isNatIList(mark(X)) -> isNatIList(X),
               isNatIList(active(X)) -> isNatIList(X)
   }
  Fail