MAYBE MAYBE TRS: { mark(U102(X1, X2)) -> active(U102(mark(X1), X2)), mark(isNatural(X)) -> active(isNatural(X)), mark(U101(X1, X2, X3)) -> active(U101(mark(X1), X2, X3)), mark(tt()) -> active(tt()), mark(U103(X)) -> active(U103(mark(X))), mark(isLNat(X)) -> active(isLNat(X)), mark(snd(X)) -> active(snd(mark(X))), mark(splitAt(X1, X2)) -> active(splitAt(mark(X1), mark(X2))), mark(U11(X1, X2, X3)) -> active(U11(mark(X1), X2, X3)), mark(U112(X)) -> active(U112(mark(X))), mark(U111(X1, X2)) -> active(U111(mark(X1), X2)), mark(U122(X)) -> active(U122(mark(X))), mark(U121(X1, X2)) -> active(U121(mark(X1), X2)), mark(U132(X1, X2)) -> active(U132(mark(X1), X2)), mark(U131(X1, X2, X3)) -> active(U131(mark(X1), X2, X3)), mark(U133(X)) -> active(U133(mark(X))), mark(U142(X1, X2)) -> active(U142(mark(X1), X2)), mark(U141(X1, X2, X3)) -> active(U141(mark(X1), X2, X3)), mark(U143(X)) -> active(U143(mark(X))), mark(U152(X1, X2)) -> active(U152(mark(X1), X2)), mark(U151(X1, X2, X3)) -> active(U151(mark(X1), X2, X3)), mark(U153(X)) -> active(U153(mark(X))), 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(head(X)) -> active(head(mark(X))), mark(afterNth(X1, X2)) -> active(afterNth(mark(X1), mark(X2))), mark(U171(X1, X2, X3)) -> active(U171(mark(X1), X2, X3)), 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)) -> active(U202(mark(X1), X2)), mark(U201(X1, X2, X3, X4)) -> active(U201(mark(X1), X2, X3, X4)), mark(U21(X1, X2)) -> active(U21(mark(X1), X2)), mark(U211(X1, X2)) -> active(U211(mark(X1), X2)), mark(fst(X)) -> active(fst(mark(X))), mark(U221(X1, X2, X3)) -> active(U221(mark(X1), X2, X3)), mark(U31(X1, X2)) -> active(U31(mark(X1), X2)), mark(U42(X1, X2)) -> active(U42(mark(X1), X2)), mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3)), mark(U43(X)) -> active(U43(mark(X))), mark(U52(X1, X2)) -> active(U52(mark(X1), X2)), mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)), mark(U53(X)) -> active(U53(mark(X))), mark(U62(X)) -> active(U62(mark(X))), mark(isPLNat(X)) -> active(isPLNat(X)), mark(U61(X1, X2)) -> active(U61(mark(X1), X2)), mark(U72(X)) -> active(U72(mark(X))), mark(U71(X1, X2)) -> active(U71(mark(X1), X2)), mark(U82(X)) -> active(U82(mark(X))), mark(U81(X1, X2)) -> active(U81(mark(X1), X2)), mark(U92(X)) -> active(U92(mark(X))), mark(U91(X1, X2)) -> active(U91(mark(X1), X2)), mark(and(X1, X2)) -> active(and(mark(X1), X2)), mark(isNaturalKind(X)) -> active(isNaturalKind(X)), mark(isLNatKind(X)) -> active(isLNatKind(X)), mark(isPLNatKind(X)) -> active(isPLNatKind(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(X1, mark(X2)) -> U102(X1, X2), U102(X1, active(X2)) -> U102(X1, X2), U102(mark(X1), X2) -> U102(X1, X2), U102(active(X1), X2) -> U102(X1, X2), isNatural(mark(X)) -> isNatural(X), isNatural(active(X)) -> isNatural(X), active(U102(tt(), V2)) -> mark(U103(isLNat(V2))), active(isNatural(s(V1))) -> mark(U121(isNaturalKind(V1), V1)), active(isNatural(head(V1))) -> mark(U111(isLNatKind(V1), V1)), active(isNatural(0())) -> mark(tt()), active(isNatural(sel(V1, V2))) -> mark(U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(U101(tt(), V1, V2)) -> mark(U102(isNatural(V1), V2)), active(U103(tt())) -> mark(tt()), active(isLNat(snd(V1))) -> mark(U81(isPLNatKind(V1), V1)), active(isLNat(cons(V1, V2))) -> mark(U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(isLNat(natsFrom(V1))) -> mark(U71(isNaturalKind(V1), V1)), active(isLNat(afterNth(V1, V2))) -> mark(U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(isLNat(nil())) -> mark(tt()), active(isLNat(fst(V1))) -> mark(U61(isPLNatKind(V1), V1)), active(isLNat(tail(V1))) -> mark(U91(isLNatKind(V1), V1)), active(isLNat(take(V1, V2))) -> mark(U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(snd(pair(X, Y))) -> mark( U181( and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y ) ), active(splitAt(s(N), cons(X, XS))) -> mark( U201( and( and(isNatural(N), isNaturalKind(N)), and( and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)) ) ), N, X, XS ) ), active(splitAt(0(), XS)) -> mark(U191(and(isLNat(XS), isLNatKind(XS)), XS)), active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))), active(U112(tt())) -> mark(tt()), active(U111(tt(), V1)) -> mark(U112(isLNat(V1))), active(U122(tt())) -> mark(tt()), active(U121(tt(), V1)) -> mark(U122(isNatural(V1))), active(U132(tt(), V2)) -> mark(U133(isLNat(V2))), active(U131(tt(), V1, V2)) -> mark(U132(isNatural(V1), V2)), active(U133(tt())) -> mark(tt()), active(U142(tt(), V2)) -> mark(U143(isLNat(V2))), active(U141(tt(), V1, V2)) -> mark(U142(isLNat(V1), V2)), active(U143(tt())) -> mark(tt()), active(U152(tt(), V2)) -> mark(U153(isLNat(V2))), active(U151(tt(), V1, V2)) -> mark(U152(isNatural(V1), V2)), active(U153(tt())) -> mark(tt()), active(natsFrom(N)) -> mark(U161(and(isNatural(N), isNaturalKind(N)), N)), active(U161(tt(), N)) -> mark(cons(N, natsFrom(s(N)))), active(head(cons(N, XS))) -> mark( U31( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), N ) ), active(afterNth(N, XS)) -> mark( U11( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), N, XS ) ), active(U171(tt(), N, XS)) -> mark(head(afterNth(N, XS))), active(U181(tt(), Y)) -> mark(Y), active(U191(tt(), XS)) -> mark(pair(nil(), XS)), active(U202(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)), active(U201(tt(), N, X, XS)) -> mark(U202(splitAt(N, XS), X)), active(U21(tt(), X)) -> mark(X), active(U211(tt(), XS)) -> mark(XS), active(fst(pair(X, Y))) -> mark( U21( and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X ) ), active(U221(tt(), N, XS)) -> mark(fst(splitAt(N, XS))), active(U31(tt(), N)) -> mark(N), active(U42(tt(), V2)) -> mark(U43(isLNat(V2))), active(U41(tt(), V1, V2)) -> mark(U42(isNatural(V1), V2)), active(U43(tt())) -> mark(tt()), active(U52(tt(), V2)) -> mark(U53(isLNat(V2))), active(U51(tt(), V1, V2)) -> mark(U52(isNatural(V1), V2)), active(U53(tt())) -> mark(tt()), active(U62(tt())) -> mark(tt()), active(isPLNat(splitAt(V1, V2))) -> mark(U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(isPLNat(pair(V1, V2))) -> mark(U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2)), active(U61(tt(), V1)) -> mark(U62(isPLNat(V1))), active(U72(tt())) -> mark(tt()), active(U71(tt(), V1)) -> mark(U72(isNatural(V1))), active(U82(tt())) -> mark(tt()), active(U81(tt(), V1)) -> mark(U82(isPLNat(V1))), active(U92(tt())) -> mark(tt()), active(U91(tt(), V1)) -> mark(U92(isLNat(V1))), active(and(tt(), X)) -> mark(X), active(isNaturalKind(s(V1))) -> mark(isNaturalKind(V1)), active(isNaturalKind(head(V1))) -> mark(isLNatKind(V1)), active(isNaturalKind(0())) -> mark(tt()), active(isNaturalKind(sel(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isLNatKind(snd(V1))) -> mark(isPLNatKind(V1)), active(isLNatKind(cons(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isLNatKind(natsFrom(V1))) -> mark(isNaturalKind(V1)), active(isLNatKind(afterNth(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isLNatKind(nil())) -> mark(tt()), active(isLNatKind(fst(V1))) -> mark(isPLNatKind(V1)), active(isLNatKind(tail(V1))) -> mark(isLNatKind(V1)), active(isLNatKind(take(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isPLNatKind(splitAt(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isPLNatKind(pair(V1, V2))) -> mark(and(isLNatKind(V1), isLNatKind(V2))), active(tail(cons(N, XS))) -> mark( U211( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), XS ) ), active(take(N, XS)) -> mark( U221( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), N, XS ) ), active(sel(N, XS)) -> mark( U171( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), N, XS ) ), U101(X1, X2, mark(X3)) -> U101(X1, X2, X3), U101(X1, X2, active(X3)) -> U101(X1, X2, X3), U101(X1, mark(X2), X3) -> U101(X1, X2, X3), U101(X1, active(X2), X3) -> U101(X1, X2, X3), U101(mark(X1), X2, X3) -> U101(X1, X2, X3), U101(active(X1), X2, X3) -> U101(X1, X2, X3), U103(mark(X)) -> U103(X), U103(active(X)) -> U103(X), isLNat(mark(X)) -> isLNat(X), isLNat(active(X)) -> isLNat(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), 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), U112(mark(X)) -> U112(X), U112(active(X)) -> U112(X), U111(X1, mark(X2)) -> U111(X1, X2), U111(X1, active(X2)) -> U111(X1, X2), U111(mark(X1), X2) -> U111(X1, X2), U111(active(X1), X2) -> U111(X1, X2), U122(mark(X)) -> U122(X), U122(active(X)) -> U122(X), U121(X1, mark(X2)) -> U121(X1, X2), U121(X1, active(X2)) -> U121(X1, X2), U121(mark(X1), X2) -> U121(X1, X2), U121(active(X1), X2) -> U121(X1, X2), U132(X1, mark(X2)) -> U132(X1, X2), U132(X1, active(X2)) -> U132(X1, X2), U132(mark(X1), X2) -> U132(X1, X2), U132(active(X1), X2) -> U132(X1, X2), U131(X1, X2, mark(X3)) -> U131(X1, X2, X3), U131(X1, X2, active(X3)) -> U131(X1, X2, X3), U131(X1, mark(X2), X3) -> U131(X1, X2, X3), U131(X1, active(X2), X3) -> U131(X1, X2, X3), U131(mark(X1), X2, X3) -> U131(X1, X2, X3), U131(active(X1), X2, X3) -> U131(X1, X2, X3), U133(mark(X)) -> U133(X), U133(active(X)) -> U133(X), U142(X1, mark(X2)) -> U142(X1, X2), U142(X1, active(X2)) -> U142(X1, X2), U142(mark(X1), X2) -> U142(X1, X2), U142(active(X1), X2) -> U142(X1, X2), U141(X1, X2, mark(X3)) -> U141(X1, X2, X3), U141(X1, X2, active(X3)) -> U141(X1, X2, X3), U141(X1, mark(X2), X3) -> U141(X1, X2, X3), U141(X1, active(X2), X3) -> U141(X1, X2, X3), U141(mark(X1), X2, X3) -> U141(X1, X2, X3), U141(active(X1), X2, X3) -> U141(X1, X2, X3), U143(mark(X)) -> U143(X), U143(active(X)) -> U143(X), U152(X1, mark(X2)) -> U152(X1, X2), U152(X1, active(X2)) -> U152(X1, X2), U152(mark(X1), X2) -> U152(X1, X2), U152(active(X1), X2) -> U152(X1, X2), U151(X1, X2, mark(X3)) -> U151(X1, X2, X3), U151(X1, X2, active(X3)) -> U151(X1, X2, X3), U151(X1, mark(X2), X3) -> U151(X1, X2, X3), U151(X1, active(X2), X3) -> U151(X1, X2, X3), U151(mark(X1), X2, X3) -> U151(X1, X2, X3), U151(active(X1), X2, X3) -> U151(X1, X2, X3), U153(mark(X)) -> U153(X), U153(active(X)) -> U153(X), 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), 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), 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), 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, mark(X2)) -> U202(X1, X2), U202(X1, active(X2)) -> U202(X1, X2), U202(mark(X1), X2) -> U202(X1, X2), U202(active(X1), X2) -> U202(X1, X2), 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), 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), 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), fst(mark(X)) -> fst(X), fst(active(X)) -> fst(X), 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), U31(X1, mark(X2)) -> U31(X1, X2), U31(X1, active(X2)) -> U31(X1, X2), U31(mark(X1), X2) -> U31(X1, X2), U31(active(X1), X2) -> U31(X1, X2), U42(X1, mark(X2)) -> U42(X1, X2), U42(X1, active(X2)) -> U42(X1, X2), U42(mark(X1), X2) -> U42(X1, X2), U42(active(X1), X2) -> U42(X1, X2), U41(X1, X2, mark(X3)) -> U41(X1, X2, X3), U41(X1, X2, active(X3)) -> U41(X1, X2, X3), U41(X1, mark(X2), X3) -> U41(X1, X2, X3), U41(X1, active(X2), X3) -> U41(X1, X2, X3), U41(mark(X1), X2, X3) -> U41(X1, X2, X3), U41(active(X1), X2, X3) -> U41(X1, X2, X3), U43(mark(X)) -> U43(X), U43(active(X)) -> U43(X), U52(X1, mark(X2)) -> U52(X1, X2), U52(X1, active(X2)) -> U52(X1, X2), U52(mark(X1), X2) -> U52(X1, X2), U52(active(X1), X2) -> U52(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), U53(mark(X)) -> U53(X), U53(active(X)) -> U53(X), U62(mark(X)) -> U62(X), U62(active(X)) -> U62(X), isPLNat(mark(X)) -> isPLNat(X), isPLNat(active(X)) -> isPLNat(X), U61(X1, mark(X2)) -> U61(X1, X2), U61(X1, active(X2)) -> U61(X1, X2), U61(mark(X1), X2) -> U61(X1, X2), U61(active(X1), X2) -> U61(X1, X2), U72(mark(X)) -> U72(X), U72(active(X)) -> U72(X), U71(X1, mark(X2)) -> U71(X1, X2), U71(X1, active(X2)) -> U71(X1, X2), U71(mark(X1), X2) -> U71(X1, X2), U71(active(X1), X2) -> U71(X1, X2), U82(mark(X)) -> U82(X), U82(active(X)) -> U82(X), U81(X1, mark(X2)) -> U81(X1, X2), U81(X1, active(X2)) -> U81(X1, X2), U81(mark(X1), X2) -> U81(X1, X2), U81(active(X1), X2) -> U81(X1, X2), U92(mark(X)) -> U92(X), U92(active(X)) -> U92(X), U91(X1, mark(X2)) -> U91(X1, X2), U91(X1, active(X2)) -> U91(X1, X2), U91(mark(X1), X2) -> U91(X1, X2), U91(active(X1), X2) -> U91(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), isNaturalKind(mark(X)) -> isNaturalKind(X), isNaturalKind(active(X)) -> isNaturalKind(X), isLNatKind(mark(X)) -> isLNatKind(X), isLNatKind(active(X)) -> isLNatKind(X), isPLNatKind(mark(X)) -> isPLNatKind(X), isPLNatKind(active(X)) -> isPLNatKind(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(X1, X2)) -> active(U102(mark(X1), X2)), mark(isNatural(X)) -> active(isNatural(X)), mark(U101(X1, X2, X3)) -> active(U101(mark(X1), X2, X3)), mark(tt()) -> active(tt()), mark(U103(X)) -> active(U103(mark(X))), mark(isLNat(X)) -> active(isLNat(X)), mark(snd(X)) -> active(snd(mark(X))), mark(splitAt(X1, X2)) -> active(splitAt(mark(X1), mark(X2))), mark(U11(X1, X2, X3)) -> active(U11(mark(X1), X2, X3)), mark(U112(X)) -> active(U112(mark(X))), mark(U111(X1, X2)) -> active(U111(mark(X1), X2)), mark(U122(X)) -> active(U122(mark(X))), mark(U121(X1, X2)) -> active(U121(mark(X1), X2)), mark(U132(X1, X2)) -> active(U132(mark(X1), X2)), mark(U131(X1, X2, X3)) -> active(U131(mark(X1), X2, X3)), mark(U133(X)) -> active(U133(mark(X))), mark(U142(X1, X2)) -> active(U142(mark(X1), X2)), mark(U141(X1, X2, X3)) -> active(U141(mark(X1), X2, X3)), mark(U143(X)) -> active(U143(mark(X))), mark(U152(X1, X2)) -> active(U152(mark(X1), X2)), mark(U151(X1, X2, X3)) -> active(U151(mark(X1), X2, X3)), mark(U153(X)) -> active(U153(mark(X))), 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(head(X)) -> active(head(mark(X))), mark(afterNth(X1, X2)) -> active(afterNth(mark(X1), mark(X2))), mark(U171(X1, X2, X3)) -> active(U171(mark(X1), X2, X3)), 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)) -> active(U202(mark(X1), X2)), mark(U201(X1, X2, X3, X4)) -> active(U201(mark(X1), X2, X3, X4)), mark(U21(X1, X2)) -> active(U21(mark(X1), X2)), mark(U211(X1, X2)) -> active(U211(mark(X1), X2)), mark(fst(X)) -> active(fst(mark(X))), mark(U221(X1, X2, X3)) -> active(U221(mark(X1), X2, X3)), mark(U31(X1, X2)) -> active(U31(mark(X1), X2)), mark(U42(X1, X2)) -> active(U42(mark(X1), X2)), mark(U41(X1, X2, X3)) -> active(U41(mark(X1), X2, X3)), mark(U43(X)) -> active(U43(mark(X))), mark(U52(X1, X2)) -> active(U52(mark(X1), X2)), mark(U51(X1, X2, X3)) -> active(U51(mark(X1), X2, X3)), mark(U53(X)) -> active(U53(mark(X))), mark(U62(X)) -> active(U62(mark(X))), mark(isPLNat(X)) -> active(isPLNat(X)), mark(U61(X1, X2)) -> active(U61(mark(X1), X2)), mark(U72(X)) -> active(U72(mark(X))), mark(U71(X1, X2)) -> active(U71(mark(X1), X2)), mark(U82(X)) -> active(U82(mark(X))), mark(U81(X1, X2)) -> active(U81(mark(X1), X2)), mark(U92(X)) -> active(U92(mark(X))), mark(U91(X1, X2)) -> active(U91(mark(X1), X2)), mark(and(X1, X2)) -> active(and(mark(X1), X2)), mark(isNaturalKind(X)) -> active(isNaturalKind(X)), mark(isLNatKind(X)) -> active(isLNatKind(X)), mark(isPLNatKind(X)) -> active(isPLNatKind(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(X1, mark(X2)) -> U102(X1, X2), U102(X1, active(X2)) -> U102(X1, X2), U102(mark(X1), X2) -> U102(X1, X2), U102(active(X1), X2) -> U102(X1, X2), isNatural(mark(X)) -> isNatural(X), isNatural(active(X)) -> isNatural(X), active(U102(tt(), V2)) -> mark(U103(isLNat(V2))), active(isNatural(s(V1))) -> mark(U121(isNaturalKind(V1), V1)), active(isNatural(head(V1))) -> mark(U111(isLNatKind(V1), V1)), active(isNatural(0())) -> mark(tt()), active(isNatural(sel(V1, V2))) -> mark(U131(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(U101(tt(), V1, V2)) -> mark(U102(isNatural(V1), V2)), active(U103(tt())) -> mark(tt()), active(isLNat(snd(V1))) -> mark(U81(isPLNatKind(V1), V1)), active(isLNat(cons(V1, V2))) -> mark(U51(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(isLNat(natsFrom(V1))) -> mark(U71(isNaturalKind(V1), V1)), active(isLNat(afterNth(V1, V2))) -> mark(U41(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(isLNat(nil())) -> mark(tt()), active(isLNat(fst(V1))) -> mark(U61(isPLNatKind(V1), V1)), active(isLNat(tail(V1))) -> mark(U91(isLNatKind(V1), V1)), active(isLNat(take(V1, V2))) -> mark(U101(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(snd(pair(X, Y))) -> mark( U181( and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), Y ) ), active(splitAt(s(N), cons(X, XS))) -> mark( U201( and( and(isNatural(N), isNaturalKind(N)), and( and(isNatural(X), isNaturalKind(X)), and(isLNat(XS), isLNatKind(XS)) ) ), N, X, XS ) ), active(splitAt(0(), XS)) -> mark(U191(and(isLNat(XS), isLNatKind(XS)), XS)), active(U11(tt(), N, XS)) -> mark(snd(splitAt(N, XS))), active(U112(tt())) -> mark(tt()), active(U111(tt(), V1)) -> mark(U112(isLNat(V1))), active(U122(tt())) -> mark(tt()), active(U121(tt(), V1)) -> mark(U122(isNatural(V1))), active(U132(tt(), V2)) -> mark(U133(isLNat(V2))), active(U131(tt(), V1, V2)) -> mark(U132(isNatural(V1), V2)), active(U133(tt())) -> mark(tt()), active(U142(tt(), V2)) -> mark(U143(isLNat(V2))), active(U141(tt(), V1, V2)) -> mark(U142(isLNat(V1), V2)), active(U143(tt())) -> mark(tt()), active(U152(tt(), V2)) -> mark(U153(isLNat(V2))), active(U151(tt(), V1, V2)) -> mark(U152(isNatural(V1), V2)), active(U153(tt())) -> mark(tt()), active(natsFrom(N)) -> mark(U161(and(isNatural(N), isNaturalKind(N)), N)), active(U161(tt(), N)) -> mark(cons(N, natsFrom(s(N)))), active(head(cons(N, XS))) -> mark( U31( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), N ) ), active(afterNth(N, XS)) -> mark( U11( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), N, XS ) ), active(U171(tt(), N, XS)) -> mark(head(afterNth(N, XS))), active(U181(tt(), Y)) -> mark(Y), active(U191(tt(), XS)) -> mark(pair(nil(), XS)), active(U202(pair(YS, ZS), X)) -> mark(pair(cons(X, YS), ZS)), active(U201(tt(), N, X, XS)) -> mark(U202(splitAt(N, XS), X)), active(U21(tt(), X)) -> mark(X), active(U211(tt(), XS)) -> mark(XS), active(fst(pair(X, Y))) -> mark( U21( and(and(isLNat(X), isLNatKind(X)), and(isLNat(Y), isLNatKind(Y))), X ) ), active(U221(tt(), N, XS)) -> mark(fst(splitAt(N, XS))), active(U31(tt(), N)) -> mark(N), active(U42(tt(), V2)) -> mark(U43(isLNat(V2))), active(U41(tt(), V1, V2)) -> mark(U42(isNatural(V1), V2)), active(U43(tt())) -> mark(tt()), active(U52(tt(), V2)) -> mark(U53(isLNat(V2))), active(U51(tt(), V1, V2)) -> mark(U52(isNatural(V1), V2)), active(U53(tt())) -> mark(tt()), active(U62(tt())) -> mark(tt()), active(isPLNat(splitAt(V1, V2))) -> mark(U151(and(isNaturalKind(V1), isLNatKind(V2)), V1, V2)), active(isPLNat(pair(V1, V2))) -> mark(U141(and(isLNatKind(V1), isLNatKind(V2)), V1, V2)), active(U61(tt(), V1)) -> mark(U62(isPLNat(V1))), active(U72(tt())) -> mark(tt()), active(U71(tt(), V1)) -> mark(U72(isNatural(V1))), active(U82(tt())) -> mark(tt()), active(U81(tt(), V1)) -> mark(U82(isPLNat(V1))), active(U92(tt())) -> mark(tt()), active(U91(tt(), V1)) -> mark(U92(isLNat(V1))), active(and(tt(), X)) -> mark(X), active(isNaturalKind(s(V1))) -> mark(isNaturalKind(V1)), active(isNaturalKind(head(V1))) -> mark(isLNatKind(V1)), active(isNaturalKind(0())) -> mark(tt()), active(isNaturalKind(sel(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isLNatKind(snd(V1))) -> mark(isPLNatKind(V1)), active(isLNatKind(cons(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isLNatKind(natsFrom(V1))) -> mark(isNaturalKind(V1)), active(isLNatKind(afterNth(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isLNatKind(nil())) -> mark(tt()), active(isLNatKind(fst(V1))) -> mark(isPLNatKind(V1)), active(isLNatKind(tail(V1))) -> mark(isLNatKind(V1)), active(isLNatKind(take(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isPLNatKind(splitAt(V1, V2))) -> mark(and(isNaturalKind(V1), isLNatKind(V2))), active(isPLNatKind(pair(V1, V2))) -> mark(and(isLNatKind(V1), isLNatKind(V2))), active(tail(cons(N, XS))) -> mark( U211( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), XS ) ), active(take(N, XS)) -> mark( U221( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), N, XS ) ), active(sel(N, XS)) -> mark( U171( and( and(isNatural(N), isNaturalKind(N)), and(isLNat(XS), isLNatKind(XS)) ), N, XS ) ), U101(X1, X2, mark(X3)) -> U101(X1, X2, X3), U101(X1, X2, active(X3)) -> U101(X1, X2, X3), U101(X1, mark(X2), X3) -> U101(X1, X2, X3), U101(X1, active(X2), X3) -> U101(X1, X2, X3), U101(mark(X1), X2, X3) -> U101(X1, X2, X3), U101(active(X1), X2, X3) -> U101(X1, X2, X3), U103(mark(X)) -> U103(X), U103(active(X)) -> U103(X), isLNat(mark(X)) -> isLNat(X), isLNat(active(X)) -> isLNat(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), 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), U112(mark(X)) -> U112(X), U112(active(X)) -> U112(X), U111(X1, mark(X2)) -> U111(X1, X2), U111(X1, active(X2)) -> U111(X1, X2), U111(mark(X1), X2) -> U111(X1, X2), U111(active(X1), X2) -> U111(X1, X2), U122(mark(X)) -> U122(X), U122(active(X)) -> U122(X), U121(X1, mark(X2)) -> U121(X1, X2), U121(X1, active(X2)) -> U121(X1, X2), U121(mark(X1), X2) -> U121(X1, X2), U121(active(X1), X2) -> U121(X1, X2), U132(X1, mark(X2)) -> U132(X1, X2), U132(X1, active(X2)) -> U132(X1, X2), U132(mark(X1), X2) -> U132(X1, X2), U132(active(X1), X2) -> U132(X1, X2), U131(X1, X2, mark(X3)) -> U131(X1, X2, X3), U131(X1, X2, active(X3)) -> U131(X1, X2, X3), U131(X1, mark(X2), X3) -> U131(X1, X2, X3), U131(X1, active(X2), X3) -> U131(X1, X2, X3), U131(mark(X1), X2, X3) -> U131(X1, X2, X3), U131(active(X1), X2, X3) -> U131(X1, X2, X3), U133(mark(X)) -> U133(X), U133(active(X)) -> U133(X), U142(X1, mark(X2)) -> U142(X1, X2), U142(X1, active(X2)) -> U142(X1, X2), U142(mark(X1), X2) -> U142(X1, X2), U142(active(X1), X2) -> U142(X1, X2), U141(X1, X2, mark(X3)) -> U141(X1, X2, X3), U141(X1, X2, active(X3)) -> U141(X1, X2, X3), U141(X1, mark(X2), X3) -> U141(X1, X2, X3), U141(X1, active(X2), X3) -> U141(X1, X2, X3), U141(mark(X1), X2, X3) -> U141(X1, X2, X3), U141(active(X1), X2, X3) -> U141(X1, X2, X3), U143(mark(X)) -> U143(X), U143(active(X)) -> U143(X), U152(X1, mark(X2)) -> U152(X1, X2), U152(X1, active(X2)) -> U152(X1, X2), U152(mark(X1), X2) -> U152(X1, X2), U152(active(X1), X2) -> U152(X1, X2), U151(X1, X2, mark(X3)) -> U151(X1, X2, X3), U151(X1, X2, active(X3)) -> U151(X1, X2, X3), U151(X1, mark(X2), X3) -> U151(X1, X2, X3), U151(X1, active(X2), X3) -> U151(X1, X2, X3), U151(mark(X1), X2, X3) -> U151(X1, X2, X3), U151(active(X1), X2, X3) -> U151(X1, X2, X3), U153(mark(X)) -> U153(X), U153(active(X)) -> U153(X), 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), 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), 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), 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, mark(X2)) -> U202(X1, X2), U202(X1, active(X2)) -> U202(X1, X2), U202(mark(X1), X2) -> U202(X1, X2), U202(active(X1), X2) -> U202(X1, X2), 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), 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), 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), fst(mark(X)) -> fst(X), fst(active(X)) -> fst(X), 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), U31(X1, mark(X2)) -> U31(X1, X2), U31(X1, active(X2)) -> U31(X1, X2), U31(mark(X1), X2) -> U31(X1, X2), U31(active(X1), X2) -> U31(X1, X2), U42(X1, mark(X2)) -> U42(X1, X2), U42(X1, active(X2)) -> U42(X1, X2), U42(mark(X1), X2) -> U42(X1, X2), U42(active(X1), X2) -> U42(X1, X2), U41(X1, X2, mark(X3)) -> U41(X1, X2, X3), U41(X1, X2, active(X3)) -> U41(X1, X2, X3), U41(X1, mark(X2), X3) -> U41(X1, X2, X3), U41(X1, active(X2), X3) -> U41(X1, X2, X3), U41(mark(X1), X2, X3) -> U41(X1, X2, X3), U41(active(X1), X2, X3) -> U41(X1, X2, X3), U43(mark(X)) -> U43(X), U43(active(X)) -> U43(X), U52(X1, mark(X2)) -> U52(X1, X2), U52(X1, active(X2)) -> U52(X1, X2), U52(mark(X1), X2) -> U52(X1, X2), U52(active(X1), X2) -> U52(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), U53(mark(X)) -> U53(X), U53(active(X)) -> U53(X), U62(mark(X)) -> U62(X), U62(active(X)) -> U62(X), isPLNat(mark(X)) -> isPLNat(X), isPLNat(active(X)) -> isPLNat(X), U61(X1, mark(X2)) -> U61(X1, X2), U61(X1, active(X2)) -> U61(X1, X2), U61(mark(X1), X2) -> U61(X1, X2), U61(active(X1), X2) -> U61(X1, X2), U72(mark(X)) -> U72(X), U72(active(X)) -> U72(X), U71(X1, mark(X2)) -> U71(X1, X2), U71(X1, active(X2)) -> U71(X1, X2), U71(mark(X1), X2) -> U71(X1, X2), U71(active(X1), X2) -> U71(X1, X2), U82(mark(X)) -> U82(X), U82(active(X)) -> U82(X), U81(X1, mark(X2)) -> U81(X1, X2), U81(X1, active(X2)) -> U81(X1, X2), U81(mark(X1), X2) -> U81(X1, X2), U81(active(X1), X2) -> U81(X1, X2), U92(mark(X)) -> U92(X), U92(active(X)) -> U92(X), U91(X1, mark(X2)) -> U91(X1, X2), U91(X1, active(X2)) -> U91(X1, X2), U91(mark(X1), X2) -> U91(X1, X2), U91(active(X1), X2) -> U91(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), isNaturalKind(mark(X)) -> isNaturalKind(X), isNaturalKind(active(X)) -> isNaturalKind(X), isLNatKind(mark(X)) -> isLNatKind(X), isLNatKind(active(X)) -> isLNatKind(X), isPLNatKind(mark(X)) -> isPLNatKind(X), isPLNatKind(active(X)) -> isPLNatKind(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