MAYBE
MAYBE
TRS:
 {
                   cons(mark(X1), X2) -> mark(cons(X1, X2)),
                 cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                 active(cons(X1, X2)) -> cons(active(X1), X2),
                      active(zeros()) -> mark(cons(0(), zeros())),
                       active(U11(X)) -> U11(active(X)),
                    active(U11(tt())) -> mark(tt()),
                       active(U21(X)) -> U21(active(X)),
                    active(U21(tt())) -> mark(tt()),
                       active(U31(X)) -> U31(active(X)),
                    active(U31(tt())) -> mark(tt()),
                       active(U42(X)) -> U42(active(X)),
                    active(U42(tt())) -> mark(tt()),
                active(isNatIList(V)) -> mark(U31(isNatList(V))),
     active(isNatIList(cons(V1, V2))) -> mark(U41(isNat(V1), V2)),
          active(isNatIList(zeros())) -> mark(tt()),
                  active(U41(X1, X2)) -> U41(active(X1), X2),
                active(U41(tt(), V2)) -> mark(U42(isNatIList(V2))),
                       active(U52(X)) -> U52(active(X)),
                    active(U52(tt())) -> mark(tt()),
      active(isNatList(cons(V1, V2))) -> mark(U51(isNat(V1), V2)),
             active(isNatList(nil())) -> mark(tt()),
      active(isNatList(take(V1, V2))) -> mark(U61(isNat(V1), V2)),
                  active(U51(X1, X2)) -> U51(active(X1), X2),
                active(U51(tt(), V2)) -> mark(U52(isNatList(V2))),
                       active(U62(X)) -> U62(active(X)),
                    active(U62(tt())) -> mark(tt()),
                  active(U61(X1, X2)) -> U61(active(X1), X2),
                active(U61(tt(), V2)) -> mark(U62(isNatIList(V2))),
                  active(U72(X1, X2)) -> U72(active(X1), X2),
                 active(U72(tt(), L)) -> mark(s(length(L))),
                   active(isNat(0())) -> mark(tt()),
                 active(isNat(s(V1))) -> mark(U21(isNat(V1))),
            active(isNat(length(V1))) -> mark(U11(isNatList(V1))),
              active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3),
              active(U71(tt(), L, N)) -> mark(U72(isNat(N), L)),
                         active(s(X)) -> s(active(X)),
                    active(length(X)) -> length(active(X)),
           active(length(cons(N, L))) -> mark(U71(isNatList(L), L, N)),
                active(length(nil())) -> mark(0()),
                       active(U81(X)) -> U81(active(X)),
                    active(U81(tt())) -> mark(nil()),
          active(U92(X1, X2, X3, X4)) -> U92(active(X1), X2, X3, X4),
          active(U92(tt(), IL, M, N)) -> mark(U93(isNat(N), IL, M, N)),
          active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4),
          active(U91(tt(), IL, M, N)) -> mark(U92(isNat(M), IL, M, N)),
          active(U93(X1, X2, X3, X4)) -> U93(active(X1), X2, X3, X4),
          active(U93(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))),
                 active(take(X1, X2)) -> take(X1, active(X2)),
                 active(take(X1, X2)) -> take(active(X1), X2),
                active(take(0(), IL)) -> mark(U81(isNatIList(IL))),
      active(take(s(M), cons(N, IL))) -> mark(U91(isNatIList(IL), IL, M, N)),
                         U11(mark(X)) -> mark(U11(X)),
                           U11(ok(X)) -> ok(U11(X)),
                         U21(mark(X)) -> mark(U21(X)),
                           U21(ok(X)) -> ok(U21(X)),
                         U31(mark(X)) -> mark(U31(X)),
                           U31(ok(X)) -> ok(U31(X)),
                         U42(mark(X)) -> mark(U42(X)),
                           U42(ok(X)) -> ok(U42(X)),
                    isNatIList(ok(X)) -> ok(isNatIList(X)),
                    U41(mark(X1), X2) -> mark(U41(X1, X2)),
                  U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)),
                         U52(mark(X)) -> mark(U52(X)),
                           U52(ok(X)) -> ok(U52(X)),
                     isNatList(ok(X)) -> ok(isNatList(X)),
                    U51(mark(X1), X2) -> mark(U51(X1, X2)),
                  U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)),
                         U62(mark(X)) -> mark(U62(X)),
                           U62(ok(X)) -> ok(U62(X)),
                    U61(mark(X1), X2) -> mark(U61(X1, X2)),
                  U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)),
                    U72(mark(X1), X2) -> mark(U72(X1, X2)),
                  U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)),
                         isNat(ok(X)) -> ok(isNat(X)),
                U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)),
          U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)),
                           s(mark(X)) -> mark(s(X)),
                             s(ok(X)) -> ok(s(X)),
                      length(mark(X)) -> mark(length(X)),
                        length(ok(X)) -> ok(length(X)),
                         U81(mark(X)) -> mark(U81(X)),
                           U81(ok(X)) -> ok(U81(X)),
            U92(mark(X1), X2, X3, X4) -> mark(U92(X1, X2, X3, X4)),
  U92(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U92(X1, X2, X3, X4)),
            U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)),
  U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)),
            U93(mark(X1), X2, X3, X4) -> mark(U93(X1, X2, X3, X4)),
  U93(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U93(X1, X2, X3, X4)),
                   take(X1, mark(X2)) -> mark(take(X1, X2)),
                   take(mark(X1), X2) -> mark(take(X1, X2)),
                 take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                 proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                          proper(0()) -> ok(0()),
                      proper(zeros()) -> ok(zeros()),
                         proper(tt()) -> ok(tt()),
                       proper(U11(X)) -> U11(proper(X)),
                       proper(U21(X)) -> U21(proper(X)),
                       proper(U31(X)) -> U31(proper(X)),
                       proper(U42(X)) -> U42(proper(X)),
                proper(isNatIList(X)) -> isNatIList(proper(X)),
                  proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)),
                       proper(U52(X)) -> U52(proper(X)),
                 proper(isNatList(X)) -> isNatList(proper(X)),
                  proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)),
                       proper(U62(X)) -> U62(proper(X)),
                  proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)),
                  proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)),
                     proper(isNat(X)) -> isNat(proper(X)),
              proper(U71(X1, X2, X3)) ->
  U71(proper(X1), proper(X2), proper(X3)),
                         proper(s(X)) -> s(proper(X)),
                    proper(length(X)) -> length(proper(X)),
                        proper(nil()) -> ok(nil()),
                       proper(U81(X)) -> U81(proper(X)),
          proper(U92(X1, X2, X3, X4)) ->
  U92(proper(X1), proper(X2), proper(X3), proper(X4)),
          proper(U91(X1, X2, X3, X4)) ->
  U91(proper(X1), proper(X2), proper(X3), proper(X4)),
          proper(U93(X1, X2, X3, X4)) ->
  U93(proper(X1), proper(X2), proper(X3), proper(X4)),
                 proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                         top(mark(X)) -> top(proper(X)),
                           top(ok(X)) -> top(active(X))
 }
 DUP: We consider a duplicating system.
  Trs:
   {
                     cons(mark(X1), X2) -> mark(cons(X1, X2)),
                   cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)),
                   active(cons(X1, X2)) -> cons(active(X1), X2),
                        active(zeros()) -> mark(cons(0(), zeros())),
                         active(U11(X)) -> U11(active(X)),
                      active(U11(tt())) -> mark(tt()),
                         active(U21(X)) -> U21(active(X)),
                      active(U21(tt())) -> mark(tt()),
                         active(U31(X)) -> U31(active(X)),
                      active(U31(tt())) -> mark(tt()),
                         active(U42(X)) -> U42(active(X)),
                      active(U42(tt())) -> mark(tt()),
                  active(isNatIList(V)) -> mark(U31(isNatList(V))),
       active(isNatIList(cons(V1, V2))) -> mark(U41(isNat(V1), V2)),
            active(isNatIList(zeros())) -> mark(tt()),
                    active(U41(X1, X2)) -> U41(active(X1), X2),
                  active(U41(tt(), V2)) -> mark(U42(isNatIList(V2))),
                         active(U52(X)) -> U52(active(X)),
                      active(U52(tt())) -> mark(tt()),
        active(isNatList(cons(V1, V2))) -> mark(U51(isNat(V1), V2)),
               active(isNatList(nil())) -> mark(tt()),
        active(isNatList(take(V1, V2))) -> mark(U61(isNat(V1), V2)),
                    active(U51(X1, X2)) -> U51(active(X1), X2),
                  active(U51(tt(), V2)) -> mark(U52(isNatList(V2))),
                         active(U62(X)) -> U62(active(X)),
                      active(U62(tt())) -> mark(tt()),
                    active(U61(X1, X2)) -> U61(active(X1), X2),
                  active(U61(tt(), V2)) -> mark(U62(isNatIList(V2))),
                    active(U72(X1, X2)) -> U72(active(X1), X2),
                   active(U72(tt(), L)) -> mark(s(length(L))),
                     active(isNat(0())) -> mark(tt()),
                   active(isNat(s(V1))) -> mark(U21(isNat(V1))),
              active(isNat(length(V1))) -> mark(U11(isNatList(V1))),
                active(U71(X1, X2, X3)) -> U71(active(X1), X2, X3),
                active(U71(tt(), L, N)) -> mark(U72(isNat(N), L)),
                           active(s(X)) -> s(active(X)),
                      active(length(X)) -> length(active(X)),
             active(length(cons(N, L))) -> mark(U71(isNatList(L), L, N)),
                  active(length(nil())) -> mark(0()),
                         active(U81(X)) -> U81(active(X)),
                      active(U81(tt())) -> mark(nil()),
            active(U92(X1, X2, X3, X4)) -> U92(active(X1), X2, X3, X4),
            active(U92(tt(), IL, M, N)) -> mark(U93(isNat(N), IL, M, N)),
            active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4),
            active(U91(tt(), IL, M, N)) -> mark(U92(isNat(M), IL, M, N)),
            active(U93(X1, X2, X3, X4)) -> U93(active(X1), X2, X3, X4),
            active(U93(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))),
                   active(take(X1, X2)) -> take(X1, active(X2)),
                   active(take(X1, X2)) -> take(active(X1), X2),
                  active(take(0(), IL)) -> mark(U81(isNatIList(IL))),
        active(take(s(M), cons(N, IL))) ->
    mark(U91(isNatIList(IL), IL, M, N)),
                           U11(mark(X)) -> mark(U11(X)),
                             U11(ok(X)) -> ok(U11(X)),
                           U21(mark(X)) -> mark(U21(X)),
                             U21(ok(X)) -> ok(U21(X)),
                           U31(mark(X)) -> mark(U31(X)),
                             U31(ok(X)) -> ok(U31(X)),
                           U42(mark(X)) -> mark(U42(X)),
                             U42(ok(X)) -> ok(U42(X)),
                      isNatIList(ok(X)) -> ok(isNatIList(X)),
                      U41(mark(X1), X2) -> mark(U41(X1, X2)),
                    U41(ok(X1), ok(X2)) -> ok(U41(X1, X2)),
                           U52(mark(X)) -> mark(U52(X)),
                             U52(ok(X)) -> ok(U52(X)),
                       isNatList(ok(X)) -> ok(isNatList(X)),
                      U51(mark(X1), X2) -> mark(U51(X1, X2)),
                    U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)),
                           U62(mark(X)) -> mark(U62(X)),
                             U62(ok(X)) -> ok(U62(X)),
                      U61(mark(X1), X2) -> mark(U61(X1, X2)),
                    U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)),
                      U72(mark(X1), X2) -> mark(U72(X1, X2)),
                    U72(ok(X1), ok(X2)) -> ok(U72(X1, X2)),
                           isNat(ok(X)) -> ok(isNat(X)),
                  U71(mark(X1), X2, X3) -> mark(U71(X1, X2, X3)),
            U71(ok(X1), ok(X2), ok(X3)) -> ok(U71(X1, X2, X3)),
                             s(mark(X)) -> mark(s(X)),
                               s(ok(X)) -> ok(s(X)),
                        length(mark(X)) -> mark(length(X)),
                          length(ok(X)) -> ok(length(X)),
                           U81(mark(X)) -> mark(U81(X)),
                             U81(ok(X)) -> ok(U81(X)),
              U92(mark(X1), X2, X3, X4) -> mark(U92(X1, X2, X3, X4)),
    U92(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U92(X1, X2, X3, X4)),
              U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)),
    U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)),
              U93(mark(X1), X2, X3, X4) -> mark(U93(X1, X2, X3, X4)),
    U93(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U93(X1, X2, X3, X4)),
                     take(X1, mark(X2)) -> mark(take(X1, X2)),
                     take(mark(X1), X2) -> mark(take(X1, X2)),
                   take(ok(X1), ok(X2)) -> ok(take(X1, X2)),
                   proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)),
                            proper(0()) -> ok(0()),
                        proper(zeros()) -> ok(zeros()),
                           proper(tt()) -> ok(tt()),
                         proper(U11(X)) -> U11(proper(X)),
                         proper(U21(X)) -> U21(proper(X)),
                         proper(U31(X)) -> U31(proper(X)),
                         proper(U42(X)) -> U42(proper(X)),
                  proper(isNatIList(X)) -> isNatIList(proper(X)),
                    proper(U41(X1, X2)) -> U41(proper(X1), proper(X2)),
                         proper(U52(X)) -> U52(proper(X)),
                   proper(isNatList(X)) -> isNatList(proper(X)),
                    proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)),
                         proper(U62(X)) -> U62(proper(X)),
                    proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)),
                    proper(U72(X1, X2)) -> U72(proper(X1), proper(X2)),
                       proper(isNat(X)) -> isNat(proper(X)),
                proper(U71(X1, X2, X3)) ->
    U71(proper(X1), proper(X2), proper(X3)),
                           proper(s(X)) -> s(proper(X)),
                      proper(length(X)) -> length(proper(X)),
                          proper(nil()) -> ok(nil()),
                         proper(U81(X)) -> U81(proper(X)),
            proper(U92(X1, X2, X3, X4)) ->
    U92(proper(X1), proper(X2), proper(X3), proper(X4)),
            proper(U91(X1, X2, X3, X4)) ->
    U91(proper(X1), proper(X2), proper(X3), proper(X4)),
            proper(U93(X1, X2, X3, X4)) ->
    U93(proper(X1), proper(X2), proper(X3), proper(X4)),
                   proper(take(X1, X2)) -> take(proper(X1), proper(X2)),
                           top(mark(X)) -> top(proper(X)),
                             top(ok(X)) -> top(active(X))
   }
  Fail