MAYBE MAYBE TRS: { mark(U102(X)) -> active(U102(mark(X))), mark(isLNat(X)) -> active(isLNat(X)), mark(U101(X1, X2)) -> active(U101(mark(X1), X2)), mark(tt()) -> active(tt()), mark(U12(X1, X2, X3)) -> active(U12(mark(X1), X2, X3)), mark(U11(X1, X2, X3)) -> active(U11(mark(X1), X2, X3)), mark(U111(X)) -> active(U111(mark(X))), mark(snd(X)) -> active(snd(mark(X))), mark(splitAt(X1, X2)) -> active(splitAt(mark(X1), mark(X2))), mark(U121(X)) -> active(U121(mark(X))), mark(U132(X)) -> active(U132(mark(X))), mark(U131(X1, X2)) -> active(U131(mark(X1), X2)), mark(U142(X)) -> active(U142(mark(X))), mark(U141(X1, X2)) -> active(U141(mark(X1), X2)), mark(U152(X)) -> active(U152(mark(X))), mark(U151(X1, X2)) -> active(U151(mark(X1), X2)), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(natsFrom(X)) -> active(natsFrom(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(U161(X1, X2)) -> active(U161(mark(X1), X2)), mark(U172(X1, X2, X3)) -> active(U172(mark(X1), X2, X3)), mark(U171(X1, X2, X3)) -> active(U171(mark(X1), X2, X3)), mark(head(X)) -> active(head(mark(X))), mark(afterNth(X1, X2)) -> active(afterNth(mark(X1), mark(X2))), mark(U182(X1, X2)) -> active(U182(mark(X1), X2)), mark(U181(X1, X2)) -> active(U181(mark(X1), X2)), mark(pair(X1, X2)) -> active(pair(mark(X1), mark(X2))), mark(nil()) -> active(nil()), mark(U191(X1, X2)) -> active(U191(mark(X1), X2)), mark(U202(X1, X2, X3, X4)) -> active(U202(mark(X1), X2, X3, X4)), mark(isNatural(X)) -> active(isNatural(X)), mark(U201(X1, X2, X3, X4)) -> active(U201(mark(X1), X2, X3, X4)), mark(U203(X1, X2, X3, X4)) -> active(U203(mark(X1), X2, X3, X4)), mark(U204(X1, X2)) -> active(U204(mark(X1), X2)), mark(U22(X1, X2)) -> active(U22(mark(X1), X2)), mark(U21(X1, X2, X3)) -> active(U21(mark(X1), X2, X3)), mark(U212(X1, X2)) -> active(U212(mark(X1), X2)), mark(U211(X1, X2)) -> active(U211(mark(X1), X2)), mark(U222(X1, X2, X3)) -> active(U222(mark(X1), X2, X3)), mark(U221(X1, X2, X3)) -> active(U221(mark(X1), X2, X3)), mark(fst(X)) -> active(fst(mark(X))), mark(U32(X1, X2)) -> active(U32(mark(X1), X2)), mark(U31(X1, X2, X3)) -> active(U31(mark(X1), X2, X3)), mark(U42(X)) -> active(U42(mark(X))), mark(U41(X1, X2)) -> active(U41(mark(X1), X2)), mark(U52(X)) -> active(U52(mark(X))), mark(U51(X1, X2)) -> active(U51(mark(X1), X2)), mark(U61(X)) -> active(U61(mark(X))), mark(U71(X)) -> active(U71(mark(X))), mark(U81(X)) -> active(U81(mark(X))), mark(U91(X)) -> active(U91(mark(X))), mark(isPLNat(X)) -> active(isPLNat(X)), mark(tail(X)) -> active(tail(mark(X))), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), U102(mark(X)) -> U102(X), U102(active(X)) -> U102(X), isLNat(mark(X)) -> isLNat(X), isLNat(active(X)) -> isLNat(X), active(U102(tt())) -> mark(tt()), active(isLNat(snd(V1))) -> mark(U81(isPLNat(V1))), active(isLNat(cons(V1, V2))) -> mark(U51(isNatural(V1), V2)), active(isLNat(natsFrom(V1))) -> mark(U71(isNatural(V1))), active(isLNat(afterNth(V1, V2))) -> mark(U41(isNatural(V1), V2)), active(isLNat(nil())) -> mark(tt()), active(isLNat(fst(V1))) -> mark(U61(isPLNat(V1))), active(isLNat(tail(V1))) -> mark(U91(isLNat(V1))), active(isLNat(take(V1, V2))) -> mark(U101(isNatural(V1), V2)), active(U101(tt(), V2)) -> mark(U102(isLNat(V2))), active(U12(tt(), N, XS)) -> mark(snd(splitAt(N, XS))), active(U11(tt(), N, XS)) -> mark(U12(isLNat(XS), N, XS)), active(U111(tt())) -> mark(tt()), active(snd(pair(X, Y))) -> mark(U181(isLNat(X), Y)), active(splitAt(s(N), cons(X, XS))) -> mark(U201(isNatural(N), N, X, XS)), active(splitAt(0(), XS)) -> mark(U191(isLNat(XS), XS)), active(U121(tt())) -> mark(tt()), active(U132(tt())) -> mark(tt()), active(U131(tt(), V2)) -> mark(U132(isLNat(V2))), active(U142(tt())) -> mark(tt()), active(U141(tt(), V2)) -> mark(U142(isLNat(V2))), active(U152(tt())) -> mark(tt()), active(U151(tt(), V2)) -> mark(U152(isLNat(V2))), active(natsFrom(N)) -> mark(U161(isNatural(N), N)), active(U161(tt(), N)) -> mark(cons(N, natsFrom(s(N)))), active(U172(tt(), N, XS)) -> mark(head(afterNth(N, XS))), active(U171(tt(), N, XS)) -> mark(U172(isLNat(XS), N, XS)), active(head(cons(N, XS))) -> mark(U31(isNatural(N), N, XS)), active(afterNth(N, XS)) -> mark(U11(isNatural(N), N, XS)), active(U182(tt(), Y)) -> mark(Y), active(U181(tt(), Y)) -> mark(U182(isLNat(Y), Y)), active(U191(tt(), XS)) -> mark(pair(nil(), XS)), active(U202(tt(), N, X, XS)) -> mark(U203(isLNat(XS), N, X, XS)), active(isNatural(s(V1))) -> mark(U121(isNatural(V1))), active(isNatural(head(V1))) -> mark(U111(isLNat(V1))), active(isNatural(0())) -> mark(tt()), active(isNatural(sel(V1, V2))) -> mark(U131(isNatural(V1), V2)), active(U201(tt(), N, X, XS)) -> mark(U202(isNatural(X), N, X, XS)), active(U203(tt(), N, X, XS)) -> mark(U204(splitAt(N, XS), X)), active(U204(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)), active(U22(tt(), X)) -> mark(X), active(U21(tt(), X, Y)) -> mark(U22(isLNat(Y), X)), active(U212(tt(), XS)) -> mark(XS), active(U211(tt(), XS)) -> mark(U212(isLNat(XS), XS)), active(U222(tt(), N, XS)) -> mark(fst(splitAt(N, XS))), active(U221(tt(), N, XS)) -> mark(U222(isLNat(XS), N, XS)), active(fst(pair(X, Y))) -> mark(U21(isLNat(X), X, Y)), active(U32(tt(), N)) -> mark(N), active(U31(tt(), N, XS)) -> mark(U32(isLNat(XS), N)), active(U42(tt())) -> mark(tt()), active(U41(tt(), V2)) -> mark(U42(isLNat(V2))), active(U52(tt())) -> mark(tt()), active(U51(tt(), V2)) -> mark(U52(isLNat(V2))), active(U61(tt())) -> mark(tt()), active(U71(tt())) -> mark(tt()), active(U81(tt())) -> mark(tt()), active(U91(tt())) -> mark(tt()), active(isPLNat(splitAt(V1, V2))) -> mark(U151(isNatural(V1), V2)), active(isPLNat(pair(V1, V2))) -> mark(U141(isLNat(V1), V2)), active(tail(cons(N, XS))) -> mark(U211(isNatural(N), XS)), active(take(N, XS)) -> mark(U221(isNatural(N), N, XS)), active(sel(N, XS)) -> mark(U171(isNatural(N), N, XS)), U101(X1, mark(X2)) -> U101(X1, X2), U101(X1, active(X2)) -> U101(X1, X2), U101(mark(X1), X2) -> U101(X1, X2), U101(active(X1), X2) -> U101(X1, X2), U12(X1, X2, mark(X3)) -> U12(X1, X2, X3), U12(X1, X2, active(X3)) -> U12(X1, X2, X3), U12(X1, mark(X2), X3) -> U12(X1, X2, X3), U12(X1, active(X2), X3) -> U12(X1, X2, X3), U12(mark(X1), X2, X3) -> U12(X1, X2, X3), U12(active(X1), X2, X3) -> U12(X1, X2, X3), 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), U111(mark(X)) -> U111(X), U111(active(X)) -> U111(X), snd(mark(X)) -> snd(X), snd(active(X)) -> snd(X), splitAt(X1, mark(X2)) -> splitAt(X1, X2), splitAt(X1, active(X2)) -> splitAt(X1, X2), splitAt(mark(X1), X2) -> splitAt(X1, X2), splitAt(active(X1), X2) -> splitAt(X1, X2), U121(mark(X)) -> U121(X), U121(active(X)) -> U121(X), U132(mark(X)) -> U132(X), U132(active(X)) -> U132(X), U131(X1, mark(X2)) -> U131(X1, X2), U131(X1, active(X2)) -> U131(X1, X2), U131(mark(X1), X2) -> U131(X1, X2), U131(active(X1), X2) -> U131(X1, X2), U142(mark(X)) -> U142(X), U142(active(X)) -> U142(X), U141(X1, mark(X2)) -> U141(X1, X2), U141(X1, active(X2)) -> U141(X1, X2), U141(mark(X1), X2) -> U141(X1, X2), U141(active(X1), X2) -> U141(X1, X2), U152(mark(X)) -> U152(X), U152(active(X)) -> U152(X), U151(X1, mark(X2)) -> U151(X1, X2), U151(X1, active(X2)) -> U151(X1, X2), U151(mark(X1), X2) -> U151(X1, X2), U151(active(X1), X2) -> U151(X1, X2), 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), natsFrom(mark(X)) -> natsFrom(X), natsFrom(active(X)) -> natsFrom(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), U161(X1, mark(X2)) -> U161(X1, X2), U161(X1, active(X2)) -> U161(X1, X2), U161(mark(X1), X2) -> U161(X1, X2), U161(active(X1), X2) -> U161(X1, X2), U172(X1, X2, mark(X3)) -> U172(X1, X2, X3), U172(X1, X2, active(X3)) -> U172(X1, X2, X3), U172(X1, mark(X2), X3) -> U172(X1, X2, X3), U172(X1, active(X2), X3) -> U172(X1, X2, X3), U172(mark(X1), X2, X3) -> U172(X1, X2, X3), U172(active(X1), X2, X3) -> U172(X1, X2, X3), U171(X1, X2, mark(X3)) -> U171(X1, X2, X3), U171(X1, X2, active(X3)) -> U171(X1, X2, X3), U171(X1, mark(X2), X3) -> U171(X1, X2, X3), U171(X1, active(X2), X3) -> U171(X1, X2, X3), U171(mark(X1), X2, X3) -> U171(X1, X2, X3), U171(active(X1), X2, X3) -> U171(X1, X2, X3), head(mark(X)) -> head(X), head(active(X)) -> head(X), afterNth(X1, mark(X2)) -> afterNth(X1, X2), afterNth(X1, active(X2)) -> afterNth(X1, X2), afterNth(mark(X1), X2) -> afterNth(X1, X2), afterNth(active(X1), X2) -> afterNth(X1, X2), U182(X1, mark(X2)) -> U182(X1, X2), U182(X1, active(X2)) -> U182(X1, X2), U182(mark(X1), X2) -> U182(X1, X2), U182(active(X1), X2) -> U182(X1, X2), U181(X1, mark(X2)) -> U181(X1, X2), U181(X1, active(X2)) -> U181(X1, X2), U181(mark(X1), X2) -> U181(X1, X2), U181(active(X1), X2) -> U181(X1, X2), pair(X1, mark(X2)) -> pair(X1, X2), pair(X1, active(X2)) -> pair(X1, X2), pair(mark(X1), X2) -> pair(X1, X2), pair(active(X1), X2) -> pair(X1, X2), U191(X1, mark(X2)) -> U191(X1, X2), U191(X1, active(X2)) -> U191(X1, X2), U191(mark(X1), X2) -> U191(X1, X2), U191(active(X1), X2) -> U191(X1, X2), U202(X1, X2, X3, mark(X4)) -> U202(X1, X2, X3, X4), U202(X1, X2, X3, active(X4)) -> U202(X1, X2, X3, X4), U202(X1, X2, mark(X3), X4) -> U202(X1, X2, X3, X4), U202(X1, X2, active(X3), X4) -> U202(X1, X2, X3, X4), U202(X1, mark(X2), X3, X4) -> U202(X1, X2, X3, X4), U202(X1, active(X2), X3, X4) -> U202(X1, X2, X3, X4), U202(mark(X1), X2, X3, X4) -> U202(X1, X2, X3, X4), U202(active(X1), X2, X3, X4) -> U202(X1, X2, X3, X4), isNatural(mark(X)) -> isNatural(X), isNatural(active(X)) -> isNatural(X), U201(X1, X2, X3, mark(X4)) -> U201(X1, X2, X3, X4), U201(X1, X2, X3, active(X4)) -> U201(X1, X2, X3, X4), U201(X1, X2, mark(X3), X4) -> U201(X1, X2, X3, X4), U201(X1, X2, active(X3), X4) -> U201(X1, X2, X3, X4), U201(X1, mark(X2), X3, X4) -> U201(X1, X2, X3, X4), U201(X1, active(X2), X3, X4) -> U201(X1, X2, X3, X4), U201(mark(X1), X2, X3, X4) -> U201(X1, X2, X3, X4), U201(active(X1), X2, X3, X4) -> U201(X1, X2, X3, X4), U203(X1, X2, X3, mark(X4)) -> U203(X1, X2, X3, X4), U203(X1, X2, X3, active(X4)) -> U203(X1, X2, X3, X4), U203(X1, X2, mark(X3), X4) -> U203(X1, X2, X3, X4), U203(X1, X2, active(X3), X4) -> U203(X1, X2, X3, X4), U203(X1, mark(X2), X3, X4) -> U203(X1, X2, X3, X4), U203(X1, active(X2), X3, X4) -> U203(X1, X2, X3, X4), U203(mark(X1), X2, X3, X4) -> U203(X1, X2, X3, X4), U203(active(X1), X2, X3, X4) -> U203(X1, X2, X3, X4), U204(X1, mark(X2)) -> U204(X1, X2), U204(X1, active(X2)) -> U204(X1, X2), U204(mark(X1), X2) -> U204(X1, X2), U204(active(X1), X2) -> U204(X1, X2), U22(X1, mark(X2)) -> U22(X1, X2), U22(X1, active(X2)) -> U22(X1, X2), U22(mark(X1), X2) -> U22(X1, X2), U22(active(X1), X2) -> U22(X1, X2), U21(X1, X2, mark(X3)) -> U21(X1, X2, X3), U21(X1, X2, active(X3)) -> U21(X1, X2, X3), U21(X1, mark(X2), X3) -> U21(X1, X2, X3), U21(X1, active(X2), X3) -> U21(X1, X2, X3), U21(mark(X1), X2, X3) -> U21(X1, X2, X3), U21(active(X1), X2, X3) -> U21(X1, X2, X3), U212(X1, mark(X2)) -> U212(X1, X2), U212(X1, active(X2)) -> U212(X1, X2), U212(mark(X1), X2) -> U212(X1, X2), U212(active(X1), X2) -> U212(X1, X2), U211(X1, mark(X2)) -> U211(X1, X2), U211(X1, active(X2)) -> U211(X1, X2), U211(mark(X1), X2) -> U211(X1, X2), U211(active(X1), X2) -> U211(X1, X2), U222(X1, X2, mark(X3)) -> U222(X1, X2, X3), U222(X1, X2, active(X3)) -> U222(X1, X2, X3), U222(X1, mark(X2), X3) -> U222(X1, X2, X3), U222(X1, active(X2), X3) -> U222(X1, X2, X3), U222(mark(X1), X2, X3) -> U222(X1, X2, X3), U222(active(X1), X2, X3) -> U222(X1, X2, X3), U221(X1, X2, mark(X3)) -> U221(X1, X2, X3), U221(X1, X2, active(X3)) -> U221(X1, X2, X3), U221(X1, mark(X2), X3) -> U221(X1, X2, X3), U221(X1, active(X2), X3) -> U221(X1, X2, X3), U221(mark(X1), X2, X3) -> U221(X1, X2, X3), U221(active(X1), X2, X3) -> U221(X1, X2, X3), fst(mark(X)) -> fst(X), fst(active(X)) -> fst(X), 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), U42(mark(X)) -> U42(X), U42(active(X)) -> U42(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), U52(mark(X)) -> U52(X), U52(active(X)) -> U52(X), U51(X1, mark(X2)) -> U51(X1, X2), U51(X1, active(X2)) -> U51(X1, X2), U51(mark(X1), X2) -> U51(X1, X2), U51(active(X1), X2) -> U51(X1, X2), U61(mark(X)) -> U61(X), U61(active(X)) -> U61(X), U71(mark(X)) -> U71(X), U71(active(X)) -> U71(X), U81(mark(X)) -> U81(X), U81(active(X)) -> U81(X), U91(mark(X)) -> U91(X), U91(active(X)) -> U91(X), isPLNat(mark(X)) -> isPLNat(X), isPLNat(active(X)) -> isPLNat(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2) } DUP: We consider a duplicating system. Trs: { mark(U102(X)) -> active(U102(mark(X))), mark(isLNat(X)) -> active(isLNat(X)), mark(U101(X1, X2)) -> active(U101(mark(X1), X2)), mark(tt()) -> active(tt()), mark(U12(X1, X2, X3)) -> active(U12(mark(X1), X2, X3)), mark(U11(X1, X2, X3)) -> active(U11(mark(X1), X2, X3)), mark(U111(X)) -> active(U111(mark(X))), mark(snd(X)) -> active(snd(mark(X))), mark(splitAt(X1, X2)) -> active(splitAt(mark(X1), mark(X2))), mark(U121(X)) -> active(U121(mark(X))), mark(U132(X)) -> active(U132(mark(X))), mark(U131(X1, X2)) -> active(U131(mark(X1), X2)), mark(U142(X)) -> active(U142(mark(X))), mark(U141(X1, X2)) -> active(U141(mark(X1), X2)), mark(U152(X)) -> active(U152(mark(X))), mark(U151(X1, X2)) -> active(U151(mark(X1), X2)), mark(cons(X1, X2)) -> active(cons(mark(X1), X2)), mark(natsFrom(X)) -> active(natsFrom(mark(X))), mark(s(X)) -> active(s(mark(X))), mark(U161(X1, X2)) -> active(U161(mark(X1), X2)), mark(U172(X1, X2, X3)) -> active(U172(mark(X1), X2, X3)), mark(U171(X1, X2, X3)) -> active(U171(mark(X1), X2, X3)), mark(head(X)) -> active(head(mark(X))), mark(afterNth(X1, X2)) -> active(afterNth(mark(X1), mark(X2))), mark(U182(X1, X2)) -> active(U182(mark(X1), X2)), mark(U181(X1, X2)) -> active(U181(mark(X1), X2)), mark(pair(X1, X2)) -> active(pair(mark(X1), mark(X2))), mark(nil()) -> active(nil()), mark(U191(X1, X2)) -> active(U191(mark(X1), X2)), mark(U202(X1, X2, X3, X4)) -> active(U202(mark(X1), X2, X3, X4)), mark(isNatural(X)) -> active(isNatural(X)), mark(U201(X1, X2, X3, X4)) -> active(U201(mark(X1), X2, X3, X4)), mark(U203(X1, X2, X3, X4)) -> active(U203(mark(X1), X2, X3, X4)), mark(U204(X1, X2)) -> active(U204(mark(X1), X2)), mark(U22(X1, X2)) -> active(U22(mark(X1), X2)), mark(U21(X1, X2, X3)) -> active(U21(mark(X1), X2, X3)), mark(U212(X1, X2)) -> active(U212(mark(X1), X2)), mark(U211(X1, X2)) -> active(U211(mark(X1), X2)), mark(U222(X1, X2, X3)) -> active(U222(mark(X1), X2, X3)), mark(U221(X1, X2, X3)) -> active(U221(mark(X1), X2, X3)), mark(fst(X)) -> active(fst(mark(X))), mark(U32(X1, X2)) -> active(U32(mark(X1), X2)), mark(U31(X1, X2, X3)) -> active(U31(mark(X1), X2, X3)), mark(U42(X)) -> active(U42(mark(X))), mark(U41(X1, X2)) -> active(U41(mark(X1), X2)), mark(U52(X)) -> active(U52(mark(X))), mark(U51(X1, X2)) -> active(U51(mark(X1), X2)), mark(U61(X)) -> active(U61(mark(X))), mark(U71(X)) -> active(U71(mark(X))), mark(U81(X)) -> active(U81(mark(X))), mark(U91(X)) -> active(U91(mark(X))), mark(isPLNat(X)) -> active(isPLNat(X)), mark(tail(X)) -> active(tail(mark(X))), mark(take(X1, X2)) -> active(take(mark(X1), mark(X2))), mark(0()) -> active(0()), mark(sel(X1, X2)) -> active(sel(mark(X1), mark(X2))), U102(mark(X)) -> U102(X), U102(active(X)) -> U102(X), isLNat(mark(X)) -> isLNat(X), isLNat(active(X)) -> isLNat(X), active(U102(tt())) -> mark(tt()), active(isLNat(snd(V1))) -> mark(U81(isPLNat(V1))), active(isLNat(cons(V1, V2))) -> mark(U51(isNatural(V1), V2)), active(isLNat(natsFrom(V1))) -> mark(U71(isNatural(V1))), active(isLNat(afterNth(V1, V2))) -> mark(U41(isNatural(V1), V2)), active(isLNat(nil())) -> mark(tt()), active(isLNat(fst(V1))) -> mark(U61(isPLNat(V1))), active(isLNat(tail(V1))) -> mark(U91(isLNat(V1))), active(isLNat(take(V1, V2))) -> mark(U101(isNatural(V1), V2)), active(U101(tt(), V2)) -> mark(U102(isLNat(V2))), active(U12(tt(), N, XS)) -> mark(snd(splitAt(N, XS))), active(U11(tt(), N, XS)) -> mark(U12(isLNat(XS), N, XS)), active(U111(tt())) -> mark(tt()), active(snd(pair(X, Y))) -> mark(U181(isLNat(X), Y)), active(splitAt(s(N), cons(X, XS))) -> mark(U201(isNatural(N), N, X, XS)), active(splitAt(0(), XS)) -> mark(U191(isLNat(XS), XS)), active(U121(tt())) -> mark(tt()), active(U132(tt())) -> mark(tt()), active(U131(tt(), V2)) -> mark(U132(isLNat(V2))), active(U142(tt())) -> mark(tt()), active(U141(tt(), V2)) -> mark(U142(isLNat(V2))), active(U152(tt())) -> mark(tt()), active(U151(tt(), V2)) -> mark(U152(isLNat(V2))), active(natsFrom(N)) -> mark(U161(isNatural(N), N)), active(U161(tt(), N)) -> mark(cons(N, natsFrom(s(N)))), active(U172(tt(), N, XS)) -> mark(head(afterNth(N, XS))), active(U171(tt(), N, XS)) -> mark(U172(isLNat(XS), N, XS)), active(head(cons(N, XS))) -> mark(U31(isNatural(N), N, XS)), active(afterNth(N, XS)) -> mark(U11(isNatural(N), N, XS)), active(U182(tt(), Y)) -> mark(Y), active(U181(tt(), Y)) -> mark(U182(isLNat(Y), Y)), active(U191(tt(), XS)) -> mark(pair(nil(), XS)), active(U202(tt(), N, X, XS)) -> mark(U203(isLNat(XS), N, X, XS)), active(isNatural(s(V1))) -> mark(U121(isNatural(V1))), active(isNatural(head(V1))) -> mark(U111(isLNat(V1))), active(isNatural(0())) -> mark(tt()), active(isNatural(sel(V1, V2))) -> mark(U131(isNatural(V1), V2)), active(U201(tt(), N, X, XS)) -> mark(U202(isNatural(X), N, X, XS)), active(U203(tt(), N, X, XS)) -> mark(U204(splitAt(N, XS), X)), active(U204(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)), active(U22(tt(), X)) -> mark(X), active(U21(tt(), X, Y)) -> mark(U22(isLNat(Y), X)), active(U212(tt(), XS)) -> mark(XS), active(U211(tt(), XS)) -> mark(U212(isLNat(XS), XS)), active(U222(tt(), N, XS)) -> mark(fst(splitAt(N, XS))), active(U221(tt(), N, XS)) -> mark(U222(isLNat(XS), N, XS)), active(fst(pair(X, Y))) -> mark(U21(isLNat(X), X, Y)), active(U32(tt(), N)) -> mark(N), active(U31(tt(), N, XS)) -> mark(U32(isLNat(XS), N)), active(U42(tt())) -> mark(tt()), active(U41(tt(), V2)) -> mark(U42(isLNat(V2))), active(U52(tt())) -> mark(tt()), active(U51(tt(), V2)) -> mark(U52(isLNat(V2))), active(U61(tt())) -> mark(tt()), active(U71(tt())) -> mark(tt()), active(U81(tt())) -> mark(tt()), active(U91(tt())) -> mark(tt()), active(isPLNat(splitAt(V1, V2))) -> mark(U151(isNatural(V1), V2)), active(isPLNat(pair(V1, V2))) -> mark(U141(isLNat(V1), V2)), active(tail(cons(N, XS))) -> mark(U211(isNatural(N), XS)), active(take(N, XS)) -> mark(U221(isNatural(N), N, XS)), active(sel(N, XS)) -> mark(U171(isNatural(N), N, XS)), U101(X1, mark(X2)) -> U101(X1, X2), U101(X1, active(X2)) -> U101(X1, X2), U101(mark(X1), X2) -> U101(X1, X2), U101(active(X1), X2) -> U101(X1, X2), U12(X1, X2, mark(X3)) -> U12(X1, X2, X3), U12(X1, X2, active(X3)) -> U12(X1, X2, X3), U12(X1, mark(X2), X3) -> U12(X1, X2, X3), U12(X1, active(X2), X3) -> U12(X1, X2, X3), U12(mark(X1), X2, X3) -> U12(X1, X2, X3), U12(active(X1), X2, X3) -> U12(X1, X2, X3), 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), U111(mark(X)) -> U111(X), U111(active(X)) -> U111(X), snd(mark(X)) -> snd(X), snd(active(X)) -> snd(X), splitAt(X1, mark(X2)) -> splitAt(X1, X2), splitAt(X1, active(X2)) -> splitAt(X1, X2), splitAt(mark(X1), X2) -> splitAt(X1, X2), splitAt(active(X1), X2) -> splitAt(X1, X2), U121(mark(X)) -> U121(X), U121(active(X)) -> U121(X), U132(mark(X)) -> U132(X), U132(active(X)) -> U132(X), U131(X1, mark(X2)) -> U131(X1, X2), U131(X1, active(X2)) -> U131(X1, X2), U131(mark(X1), X2) -> U131(X1, X2), U131(active(X1), X2) -> U131(X1, X2), U142(mark(X)) -> U142(X), U142(active(X)) -> U142(X), U141(X1, mark(X2)) -> U141(X1, X2), U141(X1, active(X2)) -> U141(X1, X2), U141(mark(X1), X2) -> U141(X1, X2), U141(active(X1), X2) -> U141(X1, X2), U152(mark(X)) -> U152(X), U152(active(X)) -> U152(X), U151(X1, mark(X2)) -> U151(X1, X2), U151(X1, active(X2)) -> U151(X1, X2), U151(mark(X1), X2) -> U151(X1, X2), U151(active(X1), X2) -> U151(X1, X2), 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), natsFrom(mark(X)) -> natsFrom(X), natsFrom(active(X)) -> natsFrom(X), s(mark(X)) -> s(X), s(active(X)) -> s(X), U161(X1, mark(X2)) -> U161(X1, X2), U161(X1, active(X2)) -> U161(X1, X2), U161(mark(X1), X2) -> U161(X1, X2), U161(active(X1), X2) -> U161(X1, X2), U172(X1, X2, mark(X3)) -> U172(X1, X2, X3), U172(X1, X2, active(X3)) -> U172(X1, X2, X3), U172(X1, mark(X2), X3) -> U172(X1, X2, X3), U172(X1, active(X2), X3) -> U172(X1, X2, X3), U172(mark(X1), X2, X3) -> U172(X1, X2, X3), U172(active(X1), X2, X3) -> U172(X1, X2, X3), U171(X1, X2, mark(X3)) -> U171(X1, X2, X3), U171(X1, X2, active(X3)) -> U171(X1, X2, X3), U171(X1, mark(X2), X3) -> U171(X1, X2, X3), U171(X1, active(X2), X3) -> U171(X1, X2, X3), U171(mark(X1), X2, X3) -> U171(X1, X2, X3), U171(active(X1), X2, X3) -> U171(X1, X2, X3), head(mark(X)) -> head(X), head(active(X)) -> head(X), afterNth(X1, mark(X2)) -> afterNth(X1, X2), afterNth(X1, active(X2)) -> afterNth(X1, X2), afterNth(mark(X1), X2) -> afterNth(X1, X2), afterNth(active(X1), X2) -> afterNth(X1, X2), U182(X1, mark(X2)) -> U182(X1, X2), U182(X1, active(X2)) -> U182(X1, X2), U182(mark(X1), X2) -> U182(X1, X2), U182(active(X1), X2) -> U182(X1, X2), U181(X1, mark(X2)) -> U181(X1, X2), U181(X1, active(X2)) -> U181(X1, X2), U181(mark(X1), X2) -> U181(X1, X2), U181(active(X1), X2) -> U181(X1, X2), pair(X1, mark(X2)) -> pair(X1, X2), pair(X1, active(X2)) -> pair(X1, X2), pair(mark(X1), X2) -> pair(X1, X2), pair(active(X1), X2) -> pair(X1, X2), U191(X1, mark(X2)) -> U191(X1, X2), U191(X1, active(X2)) -> U191(X1, X2), U191(mark(X1), X2) -> U191(X1, X2), U191(active(X1), X2) -> U191(X1, X2), U202(X1, X2, X3, mark(X4)) -> U202(X1, X2, X3, X4), U202(X1, X2, X3, active(X4)) -> U202(X1, X2, X3, X4), U202(X1, X2, mark(X3), X4) -> U202(X1, X2, X3, X4), U202(X1, X2, active(X3), X4) -> U202(X1, X2, X3, X4), U202(X1, mark(X2), X3, X4) -> U202(X1, X2, X3, X4), U202(X1, active(X2), X3, X4) -> U202(X1, X2, X3, X4), U202(mark(X1), X2, X3, X4) -> U202(X1, X2, X3, X4), U202(active(X1), X2, X3, X4) -> U202(X1, X2, X3, X4), isNatural(mark(X)) -> isNatural(X), isNatural(active(X)) -> isNatural(X), U201(X1, X2, X3, mark(X4)) -> U201(X1, X2, X3, X4), U201(X1, X2, X3, active(X4)) -> U201(X1, X2, X3, X4), U201(X1, X2, mark(X3), X4) -> U201(X1, X2, X3, X4), U201(X1, X2, active(X3), X4) -> U201(X1, X2, X3, X4), U201(X1, mark(X2), X3, X4) -> U201(X1, X2, X3, X4), U201(X1, active(X2), X3, X4) -> U201(X1, X2, X3, X4), U201(mark(X1), X2, X3, X4) -> U201(X1, X2, X3, X4), U201(active(X1), X2, X3, X4) -> U201(X1, X2, X3, X4), U203(X1, X2, X3, mark(X4)) -> U203(X1, X2, X3, X4), U203(X1, X2, X3, active(X4)) -> U203(X1, X2, X3, X4), U203(X1, X2, mark(X3), X4) -> U203(X1, X2, X3, X4), U203(X1, X2, active(X3), X4) -> U203(X1, X2, X3, X4), U203(X1, mark(X2), X3, X4) -> U203(X1, X2, X3, X4), U203(X1, active(X2), X3, X4) -> U203(X1, X2, X3, X4), U203(mark(X1), X2, X3, X4) -> U203(X1, X2, X3, X4), U203(active(X1), X2, X3, X4) -> U203(X1, X2, X3, X4), U204(X1, mark(X2)) -> U204(X1, X2), U204(X1, active(X2)) -> U204(X1, X2), U204(mark(X1), X2) -> U204(X1, X2), U204(active(X1), X2) -> U204(X1, X2), U22(X1, mark(X2)) -> U22(X1, X2), U22(X1, active(X2)) -> U22(X1, X2), U22(mark(X1), X2) -> U22(X1, X2), U22(active(X1), X2) -> U22(X1, X2), U21(X1, X2, mark(X3)) -> U21(X1, X2, X3), U21(X1, X2, active(X3)) -> U21(X1, X2, X3), U21(X1, mark(X2), X3) -> U21(X1, X2, X3), U21(X1, active(X2), X3) -> U21(X1, X2, X3), U21(mark(X1), X2, X3) -> U21(X1, X2, X3), U21(active(X1), X2, X3) -> U21(X1, X2, X3), U212(X1, mark(X2)) -> U212(X1, X2), U212(X1, active(X2)) -> U212(X1, X2), U212(mark(X1), X2) -> U212(X1, X2), U212(active(X1), X2) -> U212(X1, X2), U211(X1, mark(X2)) -> U211(X1, X2), U211(X1, active(X2)) -> U211(X1, X2), U211(mark(X1), X2) -> U211(X1, X2), U211(active(X1), X2) -> U211(X1, X2), U222(X1, X2, mark(X3)) -> U222(X1, X2, X3), U222(X1, X2, active(X3)) -> U222(X1, X2, X3), U222(X1, mark(X2), X3) -> U222(X1, X2, X3), U222(X1, active(X2), X3) -> U222(X1, X2, X3), U222(mark(X1), X2, X3) -> U222(X1, X2, X3), U222(active(X1), X2, X3) -> U222(X1, X2, X3), U221(X1, X2, mark(X3)) -> U221(X1, X2, X3), U221(X1, X2, active(X3)) -> U221(X1, X2, X3), U221(X1, mark(X2), X3) -> U221(X1, X2, X3), U221(X1, active(X2), X3) -> U221(X1, X2, X3), U221(mark(X1), X2, X3) -> U221(X1, X2, X3), U221(active(X1), X2, X3) -> U221(X1, X2, X3), fst(mark(X)) -> fst(X), fst(active(X)) -> fst(X), 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), U42(mark(X)) -> U42(X), U42(active(X)) -> U42(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), U52(mark(X)) -> U52(X), U52(active(X)) -> U52(X), U51(X1, mark(X2)) -> U51(X1, X2), U51(X1, active(X2)) -> U51(X1, X2), U51(mark(X1), X2) -> U51(X1, X2), U51(active(X1), X2) -> U51(X1, X2), U61(mark(X)) -> U61(X), U61(active(X)) -> U61(X), U71(mark(X)) -> U71(X), U71(active(X)) -> U71(X), U81(mark(X)) -> U81(X), U81(active(X)) -> U81(X), U91(mark(X)) -> U91(X), U91(active(X)) -> U91(X), isPLNat(mark(X)) -> isPLNat(X), isPLNat(active(X)) -> isPLNat(X), tail(mark(X)) -> tail(X), tail(active(X)) -> tail(X), take(X1, mark(X2)) -> take(X1, X2), take(X1, active(X2)) -> take(X1, X2), take(mark(X1), X2) -> take(X1, X2), take(active(X1), X2) -> take(X1, X2), sel(X1, mark(X2)) -> sel(X1, X2), sel(X1, active(X2)) -> sel(X1, X2), sel(mark(X1), X2) -> sel(X1, X2), sel(active(X1), X2) -> sel(X1, X2) } Fail