- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] U101(tt,V1,V2) -> U102(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [2] U102(tt,V1,V2) -> U103(isLNatKind(activate(V2)),activate(V1),activate(V2)) [3] U103(tt,V1,V2) -> U104(isLNatKind(activate(V2)),activate(V1),activate(V2)) [4] U104(tt,V1,V2) -> U105(isNatural(activate(V1)),activate(V2)) [5] U105(tt,V2) -> U106(isLNat(activate(V2))) [6] U106(tt) -> tt [7] U11(tt,N,XS) -> U12(isNaturalKind(activate(N)),activate(N),activate(XS)) [8] U111(tt,V2) -> U112(isLNatKind(activate(V2))) [9] U112(tt) -> tt [10] U12(tt,N,XS) -> U13(isLNat(activate(XS)),activate(N),activate(XS)) [11] U121(tt,V2) -> U122(isLNatKind(activate(V2))) [12] U122(tt) -> tt [13] U13(tt,N,XS) -> U14(isLNatKind(activate(XS)),activate(N),activate(XS)) [14] U131(tt) -> tt [15] U14(tt,N,XS) -> snd(splitAt(activate(N),activate(XS))) [16] U141(tt) -> tt [17] U151(tt) -> tt [18] U161(tt) -> tt [19] U171(tt,V2) -> U172(isLNatKind(activate(V2))) [20] U172(tt) -> tt [21] U181(tt,V1) -> U182(isLNatKind(activate(V1)),activate(V1)) [22] U182(tt,V1) -> U183(isLNat(activate(V1))) [23] U183(tt) -> tt [24] U191(tt,V1) -> U192(isNaturalKind(activate(V1)),activate(V1)) [25] U192(tt,V1) -> U193(isNatural(activate(V1))) [26] U193(tt) -> tt [27] U201(tt,V1,V2) -> U202(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [28] U202(tt,V1,V2) -> U203(isLNatKind(activate(V2)),activate(V1),activate(V2)) [29] U203(tt,V1,V2) -> U204(isLNatKind(activate(V2)),activate(V1),activate(V2)) [30] U204(tt,V1,V2) -> U205(isNatural(activate(V1)),activate(V2)) [31] U205(tt,V2) -> U206(isLNat(activate(V2))) [32] U206(tt) -> tt [33] U21(tt,X,Y) -> U22(isLNatKind(activate(X)),activate(X),activate(Y)) [34] U211(tt) -> tt [35] U22(tt,X,Y) -> U23(isLNat(activate(Y)),activate(X),activate(Y)) [36] U221(tt) -> tt [37] U23(tt,X,Y) -> U24(isLNatKind(activate(Y)),activate(X)) [38] U231(tt,V2) -> U232(isLNatKind(activate(V2))) [39] U232(tt) -> tt [40] U24(tt,X) -> activate(X) [41] U241(tt,V1,V2) -> U242(isLNatKind(activate(V1)),activate(V1),activate(V2)) [42] U242(tt,V1,V2) -> U243(isLNatKind(activate(V2)),activate(V1),activate(V2)) [43] U243(tt,V1,V2) -> U244(isLNatKind(activate(V2)),activate(V1),activate(V2)) [44] U244(tt,V1,V2) -> U245(isLNat(activate(V1)),activate(V2)) [45] U245(tt,V2) -> U246(isLNat(activate(V2))) [46] U246(tt) -> tt [47] U251(tt,V1,V2) -> U252(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [48] U252(tt,V1,V2) -> U253(isLNatKind(activate(V2)),activate(V1),activate(V2)) [49] U253(tt,V1,V2) -> U254(isLNatKind(activate(V2)),activate(V1),activate(V2)) [50] U254(tt,V1,V2) -> U255(isNatural(activate(V1)),activate(V2)) [51] U255(tt,V2) -> U256(isLNat(activate(V2))) [52] U256(tt) -> tt [53] U261(tt,V2) -> U262(isLNatKind(activate(V2))) [54] U262(tt) -> tt [55] U271(tt,V2) -> U272(isLNatKind(activate(V2))) [56] U272(tt) -> tt [57] U281(tt,N) -> U282(isNaturalKind(activate(N)),activate(N)) [58] U282(tt,N) -> cons(activate(N),n__natsFrom(s(activate(N)))) [59] U291(tt,N,XS) -> U292(isNaturalKind(activate(N)),activate(N),activate(XS)) [60] U292(tt,N,XS) -> U293(isLNat(activate(XS)),activate(N),activate(XS)) [61] U293(tt,N,XS) -> U294(isLNatKind(activate(XS)),activate(N),activate(XS)) [62] U294(tt,N,XS) -> head(afterNth(activate(N),activate(XS))) [63] U301(tt,X,Y) -> U302(isLNatKind(activate(X)),activate(Y)) [64] U302(tt,Y) -> U303(isLNat(activate(Y)),activate(Y)) [65] U303(tt,Y) -> U304(isLNatKind(activate(Y)),activate(Y)) [66] U304(tt,Y) -> activate(Y) [67] U31(tt,N,XS) -> U32(isNaturalKind(activate(N)),activate(N),activate(XS)) [68] U311(tt,XS) -> U312(isLNatKind(activate(XS)),activate(XS)) [69] U312(tt,XS) -> pair(nil,activate(XS)) [70] U32(tt,N,XS) -> U33(isLNat(activate(XS)),activate(N),activate(XS)) [71] U321(tt,N,X,XS) -> U322(isNaturalKind(activate(N)),activate(N),activate(X),activate(XS)) [72] U322(tt,N,X,XS) -> U323(isNatural(activate(X)),activate(N),activate(X),activate(XS)) [73] U323(tt,N,X,XS) -> U324(isNaturalKind(activate(X)),activate(N),activate(X),activate(XS)) [74] U324(tt,N,X,XS) -> U325(isLNat(activate(XS)),activate(N),activate(X),activate(XS)) [75] U325(tt,N,X,XS) -> U326(isLNatKind(activate(XS)),activate(N),activate(X),activate(XS)) [76] U326(tt,N,X,XS) -> U327(splitAt(activate(N),activate(XS)),activate(X)) [77] U327(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) [78] U33(tt,N,XS) -> U34(isLNatKind(activate(XS)),activate(N)) [79] U331(tt,N,XS) -> U332(isNaturalKind(activate(N)),activate(XS)) [80] U332(tt,XS) -> U333(isLNat(activate(XS)),activate(XS)) [81] U333(tt,XS) -> U334(isLNatKind(activate(XS)),activate(XS)) [82] U334(tt,XS) -> activate(XS) [83] U34(tt,N) -> activate(N) [84] U341(tt,N,XS) -> U342(isNaturalKind(activate(N)),activate(N),activate(XS)) [85] U342(tt,N,XS) -> U343(isLNat(activate(XS)),activate(N),activate(XS)) [86] U343(tt,N,XS) -> U344(isLNatKind(activate(XS)),activate(N),activate(XS)) [87] U344(tt,N,XS) -> fst(splitAt(activate(N),activate(XS))) [88] U41(tt,V1,V2) -> U42(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [89] U42(tt,V1,V2) -> U43(isLNatKind(activate(V2)),activate(V1),activate(V2)) [90] U43(tt,V1,V2) -> U44(isLNatKind(activate(V2)),activate(V1),activate(V2)) [91] U44(tt,V1,V2) -> U45(isNatural(activate(V1)),activate(V2)) [92] U45(tt,V2) -> U46(isLNat(activate(V2))) [93] U46(tt) -> tt [94] U51(tt,V1,V2) -> U52(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [95] U52(tt,V1,V2) -> U53(isLNatKind(activate(V2)),activate(V1),activate(V2)) [96] U53(tt,V1,V2) -> U54(isLNatKind(activate(V2)),activate(V1),activate(V2)) [97] U54(tt,V1,V2) -> U55(isNatural(activate(V1)),activate(V2)) [98] U55(tt,V2) -> U56(isLNat(activate(V2))) [99] U56(tt) -> tt [100] U61(tt,V1) -> U62(isPLNatKind(activate(V1)),activate(V1)) [101] U62(tt,V1) -> U63(isPLNat(activate(V1))) [102] U63(tt) -> tt [103] U71(tt,V1) -> U72(isNaturalKind(activate(V1)),activate(V1)) [104] U72(tt,V1) -> U73(isNatural(activate(V1))) [105] U73(tt) -> tt [106] U81(tt,V1) -> U82(isPLNatKind(activate(V1)),activate(V1)) [107] U82(tt,V1) -> U83(isPLNat(activate(V1))) [108] U83(tt) -> tt [109] U91(tt,V1) -> U92(isLNatKind(activate(V1)),activate(V1)) [110] U92(tt,V1) -> U93(isLNat(activate(V1))) [111] U93(tt) -> tt [112] afterNth(N,XS) -> U11(isNatural(N),N,XS) [113] fst(pair(X,Y)) -> U21(isLNat(X),X,Y) [114] head(cons(N,XS)) -> U31(isNatural(N),N,activate(XS)) [115] isLNat(n__nil) -> tt [116] isLNat(n__afterNth(V1,V2)) -> U41(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [117] isLNat(n__cons(V1,V2)) -> U51(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [118] isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1)) [119] isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1)) [120] isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1)) [121] isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1)) [122] isLNat(n__take(V1,V2)) -> U101(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [123] isLNatKind(n__nil) -> tt [124] isLNatKind(n__afterNth(V1,V2)) -> U111(isNaturalKind(activate(V1)),activate(V2)) [125] isLNatKind(n__cons(V1,V2)) -> U121(isNaturalKind(activate(V1)),activate(V2)) [126] isLNatKind(n__fst(V1)) -> U131(isPLNatKind(activate(V1))) [127] isLNatKind(n__natsFrom(V1)) -> U141(isNaturalKind(activate(V1))) [128] isLNatKind(n__snd(V1)) -> U151(isPLNatKind(activate(V1))) [129] isLNatKind(n__tail(V1)) -> U161(isLNatKind(activate(V1))) [130] isLNatKind(n__take(V1,V2)) -> U171(isNaturalKind(activate(V1)),activate(V2)) [131] isNatural(n__0) -> tt [132] isNatural(n__head(V1)) -> U181(isLNatKind(activate(V1)),activate(V1)) [133] isNatural(n__s(V1)) -> U191(isNaturalKind(activate(V1)),activate(V1)) [134] isNatural(n__sel(V1,V2)) -> U201(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [135] isNaturalKind(n__0) -> tt [136] isNaturalKind(n__head(V1)) -> U211(isLNatKind(activate(V1))) [137] isNaturalKind(n__s(V1)) -> U221(isNaturalKind(activate(V1))) [138] isNaturalKind(n__sel(V1,V2)) -> U231(isNaturalKind(activate(V1)),activate(V2)) [139] isPLNat(n__pair(V1,V2)) -> U241(isLNatKind(activate(V1)),activate(V1),activate(V2)) [140] isPLNat(n__splitAt(V1,V2)) -> U251(isNaturalKind(activate(V1)),activate(V1),activate(V2)) [141] isPLNatKind(n__pair(V1,V2)) -> U261(isLNatKind(activate(V1)),activate(V2)) [142] isPLNatKind(n__splitAt(V1,V2)) -> U271(isNaturalKind(activate(V1)),activate(V2)) [143] natsFrom(N) -> U281(isNatural(N),N) [144] sel(N,XS) -> U291(isNatural(N),N,XS) [145] snd(pair(X,Y)) -> U301(isLNat(X),X,Y) [146] splitAt(0,XS) -> U311(isLNat(XS),XS) [147] splitAt(s(N),cons(X,XS)) -> U321(isNatural(N),N,X,activate(XS)) [148] tail(cons(N,XS)) -> U331(isNatural(N),N,activate(XS)) [149] take(N,XS) -> U341(isNatural(N),N,XS) [150] natsFrom(X) -> n__natsFrom(X) [151] nil -> n__nil [152] afterNth(X1,X2) -> n__afterNth(X1,X2) [153] cons(X1,X2) -> n__cons(X1,X2) [154] fst(X) -> n__fst(X) [155] snd(X) -> n__snd(X) [156] tail(X) -> n__tail(X) [157] take(X1,X2) -> n__take(X1,X2) [158] 0 -> n__0 [159] head(X) -> n__head(X) [160] s(X) -> n__s(X) [161] sel(X1,X2) -> n__sel(X1,X2) [162] pair(X1,X2) -> n__pair(X1,X2) [163] splitAt(X1,X2) -> n__splitAt(X1,X2) [164] activate(n__natsFrom(X)) -> natsFrom(X) [165] activate(n__nil) -> nil [166] activate(n__afterNth(X1,X2)) -> afterNth(X1,X2) [167] activate(n__cons(X1,X2)) -> cons(X1,X2) [168] activate(n__fst(X)) -> fst(X) [169] activate(n__snd(X)) -> snd(X) [170] activate(n__tail(X)) -> tail(X) [171] activate(n__take(X1,X2)) -> take(X1,X2) [172] activate(n__0) -> 0 [173] activate(n__head(X)) -> head(X) [174] activate(n__s(X)) -> s(X) [175] activate(n__sel(X1,X2)) -> sel(X1,X2) [176] activate(n__pair(X1,X2)) -> pair(X1,X2) [177] activate(n__splitAt(X1,X2)) -> splitAt(X1,X2) [178] activate(X) -> X Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { U102(tt,V1,V2) >= U103(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; isNaturalKind(n__0) >= tt ; isNaturalKind(n__head(V1)) >= U211(isLNatKind(activate(V1))) ; isNaturalKind(n__s(V1)) >= U221(isNaturalKind(activate(V1))) ; isNaturalKind(n__sel(V1,V2)) >= U231(isNaturalKind(activate(V1)), activate(V2)) ; activate(n__natsFrom(X)) >= natsFrom(X) ; activate(n__nil) >= nil ; activate(n__afterNth(X1,X2)) >= afterNth(X1,X2) ; activate(n__cons(X1,X2)) >= cons(X1,X2) ; activate(n__fst(X)) >= fst(X) ; activate(n__snd(X)) >= snd(X) ; activate(n__tail(X)) >= tail(X) ; activate(n__take(X1,X2)) >= take(X1,X2) ; activate(n__0) >= 0 ; activate(n__head(X)) >= head(X) ; activate(n__s(X)) >= s(X) ; activate(n__sel(X1,X2)) >= sel(X1,X2) ; activate(n__pair(X1,X2)) >= pair(X1,X2) ; activate(n__splitAt(X1,X2)) >= splitAt(X1,X2) ; activate(X) >= X ; U101(tt,V1,V2) >= U102(isNaturalKind(activate(V1)),activate(V1),activate(V2)) ; U103(tt,V1,V2) >= U104(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; isLNatKind(n__natsFrom(V1)) >= U141(isNaturalKind(activate(V1))) ; isLNatKind(n__nil) >= tt ; isLNatKind(n__afterNth(V1,V2)) >= U111(isNaturalKind(activate(V1)), activate(V2)) ; isLNatKind(n__cons(V1,V2)) >= U121(isNaturalKind(activate(V1)),activate(V2)) ; isLNatKind(n__fst(V1)) >= U131(isPLNatKind(activate(V1))) ; isLNatKind(n__snd(V1)) >= U151(isPLNatKind(activate(V1))) ; isLNatKind(n__tail(V1)) >= U161(isLNatKind(activate(V1))) ; isLNatKind(n__take(V1,V2)) >= U171(isNaturalKind(activate(V1)),activate(V2)) ; U104(tt,V1,V2) >= U105(isNatural(activate(V1)),activate(V2)) ; U105(tt,V2) >= U106(isLNat(activate(V2))) ; isNatural(n__0) >= tt ; isNatural(n__head(V1)) >= U181(isLNatKind(activate(V1)),activate(V1)) ; isNatural(n__s(V1)) >= U191(isNaturalKind(activate(V1)),activate(V1)) ; isNatural(n__sel(V1,V2)) >= U201(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; U106(tt) >= tt ; isLNat(n__natsFrom(V1)) >= U71(isNaturalKind(activate(V1)),activate(V1)) ; isLNat(n__nil) >= tt ; isLNat(n__afterNth(V1,V2)) >= U41(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; isLNat(n__cons(V1,V2)) >= U51(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; isLNat(n__fst(V1)) >= U61(isPLNatKind(activate(V1)),activate(V1)) ; isLNat(n__snd(V1)) >= U81(isPLNatKind(activate(V1)),activate(V1)) ; isLNat(n__tail(V1)) >= U91(isLNatKind(activate(V1)),activate(V1)) ; isLNat(n__take(V1,V2)) >= U101(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; U12(tt,N,XS) >= U13(isLNat(activate(XS)),activate(N),activate(XS)) ; U11(tt,N,XS) >= U12(isNaturalKind(activate(N)),activate(N),activate(XS)) ; U112(tt) >= tt ; U111(tt,V2) >= U112(isLNatKind(activate(V2))) ; U13(tt,N,XS) >= U14(isLNatKind(activate(XS)),activate(N),activate(XS)) ; U122(tt) >= tt ; U121(tt,V2) >= U122(isLNatKind(activate(V2))) ; U14(tt,N,XS) >= snd(splitAt(activate(N),activate(XS))) ; U131(tt) >= tt ; snd(pair(X,Y)) >= U301(isLNat(X),X,Y) ; snd(X) >= n__snd(X) ; splitAt(s(N),cons(X,XS)) >= U321(isNatural(N),N,X,activate(XS)) ; splitAt(0,XS) >= U311(isLNat(XS),XS) ; splitAt(X1,X2) >= n__splitAt(X1,X2) ; U141(tt) >= tt ; U151(tt) >= tt ; U161(tt) >= tt ; U172(tt) >= tt ; U171(tt,V2) >= U172(isLNatKind(activate(V2))) ; U182(tt,V1) >= U183(isLNat(activate(V1))) ; U181(tt,V1) >= U182(isLNatKind(activate(V1)),activate(V1)) ; U183(tt) >= tt ; U192(tt,V1) >= U193(isNatural(activate(V1))) ; U191(tt,V1) >= U192(isNaturalKind(activate(V1)),activate(V1)) ; U193(tt) >= tt ; U202(tt,V1,V2) >= U203(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U201(tt,V1,V2) >= U202(isNaturalKind(activate(V1)),activate(V1),activate(V2)) ; U203(tt,V1,V2) >= U204(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U204(tt,V1,V2) >= U205(isNatural(activate(V1)),activate(V2)) ; U205(tt,V2) >= U206(isLNat(activate(V2))) ; U206(tt) >= tt ; U22(tt,X,Y) >= U23(isLNat(activate(Y)),activate(X),activate(Y)) ; U21(tt,X,Y) >= U22(isLNatKind(activate(X)),activate(X),activate(Y)) ; U211(tt) >= tt ; U23(tt,X,Y) >= U24(isLNatKind(activate(Y)),activate(X)) ; U221(tt) >= tt ; U24(tt,X) >= activate(X) ; U232(tt) >= tt ; U231(tt,V2) >= U232(isLNatKind(activate(V2))) ; U242(tt,V1,V2) >= U243(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U241(tt,V1,V2) >= U242(isLNatKind(activate(V1)),activate(V1),activate(V2)) ; U243(tt,V1,V2) >= U244(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U244(tt,V1,V2) >= U245(isLNat(activate(V1)),activate(V2)) ; U245(tt,V2) >= U246(isLNat(activate(V2))) ; U246(tt) >= tt ; U252(tt,V1,V2) >= U253(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U251(tt,V1,V2) >= U252(isNaturalKind(activate(V1)),activate(V1),activate(V2)) ; U253(tt,V1,V2) >= U254(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U254(tt,V1,V2) >= U255(isNatural(activate(V1)),activate(V2)) ; U255(tt,V2) >= U256(isLNat(activate(V2))) ; U256(tt) >= tt ; U262(tt) >= tt ; U261(tt,V2) >= U262(isLNatKind(activate(V2))) ; U272(tt) >= tt ; U271(tt,V2) >= U272(isLNatKind(activate(V2))) ; U282(tt,N) >= cons(activate(N),n__natsFrom(s(activate(N)))) ; U281(tt,N) >= U282(isNaturalKind(activate(N)),activate(N)) ; cons(X1,X2) >= n__cons(X1,X2) ; s(X) >= n__s(X) ; U292(tt,N,XS) >= U293(isLNat(activate(XS)),activate(N),activate(XS)) ; U291(tt,N,XS) >= U292(isNaturalKind(activate(N)),activate(N),activate(XS)) ; U293(tt,N,XS) >= U294(isLNatKind(activate(XS)),activate(N),activate(XS)) ; U294(tt,N,XS) >= head(afterNth(activate(N),activate(XS))) ; head(cons(N,XS)) >= U31(isNatural(N),N,activate(XS)) ; head(X) >= n__head(X) ; afterNth(N,XS) >= U11(isNatural(N),N,XS) ; afterNth(X1,X2) >= n__afterNth(X1,X2) ; U302(tt,Y) >= U303(isLNat(activate(Y)),activate(Y)) ; U301(tt,X,Y) >= U302(isLNatKind(activate(X)),activate(Y)) ; U303(tt,Y) >= U304(isLNatKind(activate(Y)),activate(Y)) ; U304(tt,Y) >= activate(Y) ; U32(tt,N,XS) >= U33(isLNat(activate(XS)),activate(N),activate(XS)) ; U31(tt,N,XS) >= U32(isNaturalKind(activate(N)),activate(N),activate(XS)) ; U312(tt,XS) >= pair(nil,activate(XS)) ; U311(tt,XS) >= U312(isLNatKind(activate(XS)),activate(XS)) ; pair(X1,X2) >= n__pair(X1,X2) ; nil >= n__nil ; U33(tt,N,XS) >= U34(isLNatKind(activate(XS)),activate(N)) ; U322(tt,N,X,XS) >= U323(isNatural(activate(X)),activate(N),activate(X), activate(XS)) ; U321(tt,N,X,XS) >= U322(isNaturalKind(activate(N)),activate(N),activate(X), activate(XS)) ; U323(tt,N,X,XS) >= U324(isNaturalKind(activate(X)),activate(N),activate(X), activate(XS)) ; U324(tt,N,X,XS) >= U325(isLNat(activate(XS)),activate(N),activate(X), activate(XS)) ; U325(tt,N,X,XS) >= U326(isLNatKind(activate(XS)),activate(N),activate(X), activate(XS)) ; U326(tt,N,X,XS) >= U327(splitAt(activate(N),activate(XS)),activate(X)) ; U327(pair(YS,ZS),X) >= pair(cons(activate(X),YS),ZS) ; U34(tt,N) >= activate(N) ; U332(tt,XS) >= U333(isLNat(activate(XS)),activate(XS)) ; U331(tt,N,XS) >= U332(isNaturalKind(activate(N)),activate(XS)) ; U333(tt,XS) >= U334(isLNatKind(activate(XS)),activate(XS)) ; U334(tt,XS) >= activate(XS) ; U342(tt,N,XS) >= U343(isLNat(activate(XS)),activate(N),activate(XS)) ; U341(tt,N,XS) >= U342(isNaturalKind(activate(N)),activate(N),activate(XS)) ; U343(tt,N,XS) >= U344(isLNatKind(activate(XS)),activate(N),activate(XS)) ; U344(tt,N,XS) >= fst(splitAt(activate(N),activate(XS))) ; fst(pair(X,Y)) >= U21(isLNat(X),X,Y) ; fst(X) >= n__fst(X) ; U42(tt,V1,V2) >= U43(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U41(tt,V1,V2) >= U42(isNaturalKind(activate(V1)),activate(V1),activate(V2)) ; U43(tt,V1,V2) >= U44(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U44(tt,V1,V2) >= U45(isNatural(activate(V1)),activate(V2)) ; U45(tt,V2) >= U46(isLNat(activate(V2))) ; U46(tt) >= tt ; U52(tt,V1,V2) >= U53(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U51(tt,V1,V2) >= U52(isNaturalKind(activate(V1)),activate(V1),activate(V2)) ; U53(tt,V1,V2) >= U54(isLNatKind(activate(V2)),activate(V1),activate(V2)) ; U54(tt,V1,V2) >= U55(isNatural(activate(V1)),activate(V2)) ; U55(tt,V2) >= U56(isLNat(activate(V2))) ; U56(tt) >= tt ; U62(tt,V1) >= U63(isPLNat(activate(V1))) ; isPLNatKind(n__pair(V1,V2)) >= U261(isLNatKind(activate(V1)),activate(V2)) ; isPLNatKind(n__splitAt(V1,V2)) >= U271(isNaturalKind(activate(V1)), activate(V2)) ; U61(tt,V1) >= U62(isPLNatKind(activate(V1)),activate(V1)) ; U63(tt) >= tt ; isPLNat(n__pair(V1,V2)) >= U241(isLNatKind(activate(V1)),activate(V1), activate(V2)) ; isPLNat(n__splitAt(V1,V2)) >= U251(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; U72(tt,V1) >= U73(isNatural(activate(V1))) ; U71(tt,V1) >= U72(isNaturalKind(activate(V1)),activate(V1)) ; U73(tt) >= tt ; U82(tt,V1) >= U83(isPLNat(activate(V1))) ; U81(tt,V1) >= U82(isPLNatKind(activate(V1)),activate(V1)) ; U83(tt) >= tt ; U92(tt,V1) >= U93(isLNat(activate(V1))) ; U91(tt,V1) >= U92(isLNatKind(activate(V1)),activate(V1)) ; U93(tt) >= tt ; natsFrom(N) >= U281(isNatural(N),N) ; natsFrom(X) >= n__natsFrom(X) ; sel(N,XS) >= U291(isNatural(N),N,XS) ; sel(X1,X2) >= n__sel(X1,X2) ; 0 >= n__0 ; tail(cons(N,XS)) >= U331(isNatural(N),N,activate(XS)) ; tail(X) >= n__tail(X) ; take(N,XS) >= U341(isNatural(N),N,XS) ; take(X1,X2) >= n__take(X1,X2) ; Marked_activate(n__natsFrom(X)) >= Marked_natsFrom(X) ; Marked_activate(n__afterNth(X1,X2)) >= Marked_afterNth(X1,X2) ; Marked_activate(n__fst(X)) >= Marked_fst(X) ; Marked_activate(n__snd(X)) >= Marked_snd(X) ; Marked_activate(n__tail(X)) >= Marked_tail(X) ; Marked_activate(n__take(X1,X2)) >= Marked_take(X1,X2) ; Marked_activate(n__head(X)) >= Marked_head(X) ; Marked_activate(n__sel(X1,X2)) >= Marked_sel(X1,X2) ; Marked_activate(n__splitAt(X1,X2)) >= Marked_splitAt(X1,X2) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_activate(XS) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_isNatural(N) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_U321(isNatural(N),N,X,activate(XS)) ; Marked_splitAt(0,XS) >= Marked_U311(isLNat(XS),XS) ; Marked_splitAt(0,XS) >= Marked_isLNat(XS) ; Marked_sel(N,XS) >= Marked_isNatural(N) ; Marked_sel(N,XS) >= Marked_U291(isNatural(N),N,XS) ; Marked_head(cons(N,XS)) >= Marked_activate(XS) ; Marked_head(cons(N,XS)) >= Marked_isNatural(N) ; Marked_head(cons(N,XS)) >= Marked_U31(isNatural(N),N,activate(XS)) ; Marked_take(N,XS) >= Marked_U341(isNatural(N),N,XS) ; Marked_take(N,XS) >= Marked_isNatural(N) ; Marked_tail(cons(N,XS)) >= Marked_activate(XS) ; Marked_tail(cons(N,XS)) >= Marked_isNatural(N) ; Marked_tail(cons(N,XS)) >= Marked_U331(isNatural(N),N,activate(XS)) ; Marked_snd(pair(X,Y)) >= Marked_isLNat(X) ; Marked_snd(pair(X,Y)) >= Marked_U301(isLNat(X),X,Y) ; Marked_fst(pair(X,Y)) >= Marked_isLNat(X) ; Marked_fst(pair(X,Y)) >= Marked_U21(isLNat(X),X,Y) ; Marked_afterNth(N,XS) >= Marked_isNatural(N) ; Marked_afterNth(N,XS) >= Marked_U11(isNatural(N),N,XS) ; Marked_natsFrom(N) >= Marked_isNatural(N) ; Marked_natsFrom(N) >= Marked_U281(isNatural(N),N) ; Marked_U341(tt,N,XS) >= Marked_activate(N) ; Marked_U341(tt,N,XS) >= Marked_activate(XS) ; Marked_U341(tt,N,XS) >= Marked_isNaturalKind(activate(N)) ; Marked_U341(tt,N,XS) >= Marked_U342(isNaturalKind(activate(N)),activate(N), activate(XS)) ; Marked_isNatural(n__head(V1)) >= Marked_activate(V1) ; Marked_isNatural(n__head(V1)) >= Marked_isLNatKind(activate(V1)) ; Marked_isNatural(n__head(V1)) >= Marked_U181(isLNatKind(activate(V1)), activate(V1)) ; Marked_isNatural(n__s(V1)) >= Marked_activate(V1) ; Marked_isNatural(n__s(V1)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isNatural(n__s(V1)) >= Marked_U191(isNaturalKind(activate(V1)), activate(V1)) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_activate(V1) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_activate(V2) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_U201(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; Marked_U331(tt,N,XS) >= Marked_activate(N) ; Marked_U331(tt,N,XS) >= Marked_activate(XS) ; Marked_U331(tt,N,XS) >= Marked_isNaturalKind(activate(N)) ; Marked_U331(tt,N,XS) >= Marked_U332(isNaturalKind(activate(N)),activate(XS)) ; Marked_U321(tt,N,X,XS) >= Marked_activate(N) ; Marked_U321(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U321(tt,N,X,XS) >= Marked_activate(X) ; Marked_U321(tt,N,X,XS) >= Marked_isNaturalKind(activate(N)) ; Marked_U321(tt,N,X,XS) >= Marked_U322(isNaturalKind(activate(N)),activate(N), activate(X),activate(XS)) ; Marked_U311(tt,XS) >= Marked_activate(XS) ; Marked_U311(tt,XS) >= Marked_isLNatKind(activate(XS)) ; Marked_U311(tt,XS) >= Marked_U312(isLNatKind(activate(XS)),activate(XS)) ; Marked_isLNat(n__natsFrom(V1)) >= Marked_activate(V1) ; Marked_isLNat(n__natsFrom(V1)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNat(n__natsFrom(V1)) >= Marked_U71(isNaturalKind(activate(V1)), activate(V1)) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_activate(V1) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_activate(V2) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_U41(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_U51(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; Marked_isLNat(n__fst(V1)) >= Marked_activate(V1) ; Marked_isLNat(n__fst(V1)) >= Marked_isPLNatKind(activate(V1)) ; Marked_isLNat(n__fst(V1)) >= Marked_U61(isPLNatKind(activate(V1)), activate(V1)) ; Marked_isLNat(n__snd(V1)) >= Marked_activate(V1) ; Marked_isLNat(n__snd(V1)) >= Marked_isPLNatKind(activate(V1)) ; Marked_isLNat(n__snd(V1)) >= Marked_U81(isPLNatKind(activate(V1)), activate(V1)) ; Marked_isLNat(n__tail(V1)) >= Marked_activate(V1) ; Marked_isLNat(n__tail(V1)) >= Marked_isLNatKind(activate(V1)) ; Marked_isLNat(n__tail(V1)) >= Marked_U91(isLNatKind(activate(V1)), activate(V1)) ; Marked_isLNat(n__take(V1,V2)) >= Marked_activate(V1) ; Marked_isLNat(n__take(V1,V2)) >= Marked_activate(V2) ; Marked_isLNat(n__take(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNat(n__take(V1,V2)) >= Marked_U101(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; Marked_U301(tt,X,Y) >= Marked_activate(X) ; Marked_U301(tt,X,Y) >= Marked_activate(Y) ; Marked_U301(tt,X,Y) >= Marked_isLNatKind(activate(X)) ; Marked_U301(tt,X,Y) >= Marked_U302(isLNatKind(activate(X)),activate(Y)) ; Marked_U291(tt,N,XS) >= Marked_activate(N) ; Marked_U291(tt,N,XS) >= Marked_activate(XS) ; Marked_U291(tt,N,XS) >= Marked_isNaturalKind(activate(N)) ; Marked_U291(tt,N,XS) >= Marked_U292(isNaturalKind(activate(N)),activate(N), activate(XS)) ; Marked_U281(tt,N) >= Marked_activate(N) ; Marked_U281(tt,N) >= Marked_isNaturalKind(activate(N)) ; Marked_U281(tt,N) >= Marked_U282(isNaturalKind(activate(N)),activate(N)) ; Marked_isPLNatKind(n__pair(V1,V2)) >= Marked_activate(V1) ; Marked_isPLNatKind(n__pair(V1,V2)) >= Marked_activate(V2) ; Marked_isPLNatKind(n__pair(V1,V2)) >= Marked_U261(isLNatKind(activate(V1)), activate(V2)) ; Marked_isPLNatKind(n__pair(V1,V2)) >= Marked_isLNatKind(activate(V1)) ; Marked_isPLNatKind(n__splitAt(V1,V2)) >= Marked_activate(V1) ; Marked_isPLNatKind(n__splitAt(V1,V2)) >= Marked_activate(V2) ; Marked_isPLNatKind(n__splitAt(V1,V2)) >= Marked_U271(isNaturalKind( activate(V1)), activate(V2)) ; Marked_isPLNatKind(n__splitAt(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_U271(tt,V2) >= Marked_activate(V2) ; Marked_U271(tt,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_isNaturalKind(n__head(V1)) >= Marked_activate(V1) ; Marked_isNaturalKind(n__head(V1)) >= Marked_isLNatKind(activate(V1)) ; Marked_isNaturalKind(n__s(V1)) >= Marked_activate(V1) ; Marked_isNaturalKind(n__s(V1)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isNaturalKind(n__sel(V1,V2)) >= Marked_activate(V1) ; Marked_isNaturalKind(n__sel(V1,V2)) >= Marked_activate(V2) ; Marked_isNaturalKind(n__sel(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isNaturalKind(n__sel(V1,V2)) >= Marked_U231(isNaturalKind(activate(V1)), activate(V2)) ; Marked_U261(tt,V2) >= Marked_activate(V2) ; Marked_U261(tt,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_isLNatKind(n__natsFrom(V1)) >= Marked_activate(V1) ; Marked_isLNatKind(n__natsFrom(V1)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNatKind(n__afterNth(V1,V2)) >= Marked_activate(V1) ; Marked_isLNatKind(n__afterNth(V1,V2)) >= Marked_activate(V2) ; Marked_isLNatKind(n__afterNth(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNatKind(n__afterNth(V1,V2)) >= Marked_U111(isNaturalKind( activate(V1)), activate(V2)) ; Marked_isLNatKind(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isLNatKind(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isLNatKind(n__cons(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNatKind(n__cons(V1,V2)) >= Marked_U121(isNaturalKind(activate(V1)), activate(V2)) ; Marked_isLNatKind(n__fst(V1)) >= Marked_activate(V1) ; Marked_isLNatKind(n__fst(V1)) >= Marked_isPLNatKind(activate(V1)) ; Marked_isLNatKind(n__snd(V1)) >= Marked_activate(V1) ; Marked_isLNatKind(n__snd(V1)) >= Marked_isPLNatKind(activate(V1)) ; Marked_isLNatKind(n__tail(V1)) >= Marked_activate(V1) ; Marked_isLNatKind(n__tail(V1)) >= Marked_isLNatKind(activate(V1)) ; Marked_isLNatKind(n__take(V1,V2)) >= Marked_activate(V1) ; Marked_isLNatKind(n__take(V1,V2)) >= Marked_activate(V2) ; Marked_isLNatKind(n__take(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNatKind(n__take(V1,V2)) >= Marked_U171(isNaturalKind(activate(V1)), activate(V2)) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_activate(V1) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_activate(V2) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_isLNatKind(activate(V1)) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_U241(isLNatKind(activate(V1)), activate(V1),activate(V2)) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_activate(V1) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_activate(V2) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_U251(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; Marked_U251(tt,V1,V2) >= Marked_activate(V1) ; Marked_U251(tt,V1,V2) >= Marked_activate(V2) ; Marked_U251(tt,V1,V2) >= Marked_isNaturalKind(activate(V1)) ; Marked_U251(tt,V1,V2) >= Marked_U252(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; Marked_U241(tt,V1,V2) >= Marked_activate(V1) ; Marked_U241(tt,V1,V2) >= Marked_activate(V2) ; Marked_U241(tt,V1,V2) >= Marked_isLNatKind(activate(V1)) ; Marked_U241(tt,V1,V2) >= Marked_U242(isLNatKind(activate(V1)),activate(V1), activate(V2)) ; Marked_U231(tt,V2) >= Marked_activate(V2) ; Marked_U231(tt,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U201(tt,V1,V2) >= Marked_activate(V1) ; Marked_U201(tt,V1,V2) >= Marked_activate(V2) ; Marked_U201(tt,V1,V2) >= Marked_isNaturalKind(activate(V1)) ; Marked_U201(tt,V1,V2) >= Marked_U202(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; Marked_U191(tt,V1) >= Marked_activate(V1) ; Marked_U191(tt,V1) >= Marked_isNaturalKind(activate(V1)) ; Marked_U191(tt,V1) >= Marked_U192(isNaturalKind(activate(V1)),activate(V1)) ; Marked_U181(tt,V1) >= Marked_activate(V1) ; Marked_U181(tt,V1) >= Marked_isLNatKind(activate(V1)) ; Marked_U181(tt,V1) >= Marked_U182(isLNatKind(activate(V1)),activate(V1)) ; Marked_U171(tt,V2) >= Marked_activate(V2) ; Marked_U171(tt,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U121(tt,V2) >= Marked_activate(V2) ; Marked_U121(tt,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U111(tt,V2) >= Marked_activate(V2) ; Marked_U111(tt,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U101(tt,V1,V2) >= Marked_activate(V1) ; Marked_U101(tt,V1,V2) >= Marked_activate(V2) ; Marked_U101(tt,V1,V2) >= Marked_isNaturalKind(activate(V1)) ; Marked_U101(tt,V1,V2) >= Marked_U102(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; Marked_U91(tt,V1) >= Marked_activate(V1) ; Marked_U91(tt,V1) >= Marked_isLNatKind(activate(V1)) ; Marked_U91(tt,V1) >= Marked_U92(isLNatKind(activate(V1)),activate(V1)) ; Marked_U81(tt,V1) >= Marked_activate(V1) ; Marked_U81(tt,V1) >= Marked_isPLNatKind(activate(V1)) ; Marked_U81(tt,V1) >= Marked_U82(isPLNatKind(activate(V1)),activate(V1)) ; Marked_U71(tt,V1) >= Marked_activate(V1) ; Marked_U71(tt,V1) >= Marked_isNaturalKind(activate(V1)) ; Marked_U71(tt,V1) >= Marked_U72(isNaturalKind(activate(V1)),activate(V1)) ; Marked_U61(tt,V1) >= Marked_activate(V1) ; Marked_U61(tt,V1) >= Marked_isPLNatKind(activate(V1)) ; Marked_U61(tt,V1) >= Marked_U62(isPLNatKind(activate(V1)),activate(V1)) ; Marked_U51(tt,V1,V2) >= Marked_activate(V1) ; Marked_U51(tt,V1,V2) >= Marked_activate(V2) ; Marked_U51(tt,V1,V2) >= Marked_isNaturalKind(activate(V1)) ; Marked_U51(tt,V1,V2) >= Marked_U52(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; Marked_U41(tt,V1,V2) >= Marked_activate(V1) ; Marked_U41(tt,V1,V2) >= Marked_activate(V2) ; Marked_U41(tt,V1,V2) >= Marked_isNaturalKind(activate(V1)) ; Marked_U41(tt,V1,V2) >= Marked_U42(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; Marked_U31(tt,N,XS) >= Marked_activate(N) ; Marked_U31(tt,N,XS) >= Marked_activate(XS) ; Marked_U31(tt,N,XS) >= Marked_isNaturalKind(activate(N)) ; Marked_U31(tt,N,XS) >= Marked_U32(isNaturalKind(activate(N)),activate(N), activate(XS)) ; Marked_U21(tt,X,Y) >= Marked_activate(X) ; Marked_U21(tt,X,Y) >= Marked_activate(Y) ; Marked_U21(tt,X,Y) >= Marked_isLNatKind(activate(X)) ; Marked_U21(tt,X,Y) >= Marked_U22(isLNatKind(activate(X)),activate(X), activate(Y)) ; Marked_U11(tt,N,XS) >= Marked_activate(N) ; Marked_U11(tt,N,XS) >= Marked_activate(XS) ; Marked_U11(tt,N,XS) >= Marked_isNaturalKind(activate(N)) ; Marked_U11(tt,N,XS) >= Marked_U12(isNaturalKind(activate(N)),activate(N), activate(XS)) ; Marked_U92(tt,V1) >= Marked_activate(V1) ; Marked_U92(tt,V1) >= Marked_isLNat(activate(V1)) ; Marked_U82(tt,V1) >= Marked_activate(V1) ; Marked_U82(tt,V1) >= Marked_isPLNat(activate(V1)) ; Marked_U72(tt,V1) >= Marked_activate(V1) ; Marked_U72(tt,V1) >= Marked_isNatural(activate(V1)) ; Marked_U62(tt,V1) >= Marked_activate(V1) ; Marked_U62(tt,V1) >= Marked_isPLNat(activate(V1)) ; Marked_U55(tt,V2) >= Marked_activate(V2) ; Marked_U55(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U54(tt,V1,V2) >= Marked_activate(V1) ; Marked_U54(tt,V1,V2) >= Marked_activate(V2) ; Marked_U54(tt,V1,V2) >= Marked_isNatural(activate(V1)) ; Marked_U54(tt,V1,V2) >= Marked_U55(isNatural(activate(V1)),activate(V2)) ; Marked_U53(tt,V1,V2) >= Marked_activate(V1) ; Marked_U53(tt,V1,V2) >= Marked_activate(V2) ; Marked_U53(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U53(tt,V1,V2) >= Marked_U54(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U52(tt,V1,V2) >= Marked_activate(V1) ; Marked_U52(tt,V1,V2) >= Marked_activate(V2) ; Marked_U52(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U52(tt,V1,V2) >= Marked_U53(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U45(tt,V2) >= Marked_activate(V2) ; Marked_U45(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U44(tt,V1,V2) >= Marked_activate(V1) ; Marked_U44(tt,V1,V2) >= Marked_activate(V2) ; Marked_U44(tt,V1,V2) >= Marked_isNatural(activate(V1)) ; Marked_U44(tt,V1,V2) >= Marked_U45(isNatural(activate(V1)),activate(V2)) ; Marked_U43(tt,V1,V2) >= Marked_activate(V1) ; Marked_U43(tt,V1,V2) >= Marked_activate(V2) ; Marked_U43(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U43(tt,V1,V2) >= Marked_U44(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U42(tt,V1,V2) >= Marked_activate(V1) ; Marked_U42(tt,V1,V2) >= Marked_activate(V2) ; Marked_U42(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U42(tt,V1,V2) >= Marked_U43(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U344(tt,N,XS) >= Marked_activate(N) ; Marked_U344(tt,N,XS) >= Marked_activate(XS) ; Marked_U344(tt,N,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U344(tt,N,XS) >= Marked_fst(splitAt(activate(N),activate(XS))) ; Marked_U343(tt,N,XS) >= Marked_activate(N) ; Marked_U343(tt,N,XS) >= Marked_activate(XS) ; Marked_U343(tt,N,XS) >= Marked_isLNatKind(activate(XS)) ; Marked_U343(tt,N,XS) >= Marked_U344(isLNatKind(activate(XS)),activate(N), activate(XS)) ; Marked_U342(tt,N,XS) >= Marked_activate(N) ; Marked_U342(tt,N,XS) >= Marked_activate(XS) ; Marked_U342(tt,N,XS) >= Marked_isLNat(activate(XS)) ; Marked_U342(tt,N,XS) >= Marked_U343(isLNat(activate(XS)),activate(N), activate(XS)) ; Marked_U34(tt,N) >= Marked_activate(N) ; Marked_U334(tt,XS) >= Marked_activate(XS) ; Marked_U333(tt,XS) >= Marked_activate(XS) ; Marked_U333(tt,XS) >= Marked_isLNatKind(activate(XS)) ; Marked_U333(tt,XS) >= Marked_U334(isLNatKind(activate(XS)),activate(XS)) ; Marked_U332(tt,XS) >= Marked_activate(XS) ; Marked_U332(tt,XS) >= Marked_isLNat(activate(XS)) ; Marked_U332(tt,XS) >= Marked_U333(isLNat(activate(XS)),activate(XS)) ; Marked_U33(tt,N,XS) >= Marked_activate(N) ; Marked_U33(tt,N,XS) >= Marked_activate(XS) ; Marked_U33(tt,N,XS) >= Marked_isLNatKind(activate(XS)) ; Marked_U33(tt,N,XS) >= Marked_U34(isLNatKind(activate(XS)),activate(N)) ; Marked_U327(pair(YS,ZS),X) >= Marked_activate(X) ; Marked_U326(tt,N,X,XS) >= Marked_activate(N) ; Marked_U326(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U326(tt,N,X,XS) >= Marked_activate(X) ; Marked_U326(tt,N,X,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U326(tt,N,X,XS) >= Marked_U327(splitAt(activate(N),activate(XS)), activate(X)) ; Marked_U325(tt,N,X,XS) >= Marked_activate(N) ; Marked_U325(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U325(tt,N,X,XS) >= Marked_activate(X) ; Marked_U325(tt,N,X,XS) >= Marked_isLNatKind(activate(XS)) ; Marked_U325(tt,N,X,XS) >= Marked_U326(isLNatKind(activate(XS)),activate(N), activate(X),activate(XS)) ; Marked_U324(tt,N,X,XS) >= Marked_activate(N) ; Marked_U324(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U324(tt,N,X,XS) >= Marked_activate(X) ; Marked_U324(tt,N,X,XS) >= Marked_isLNat(activate(XS)) ; Marked_U324(tt,N,X,XS) >= Marked_U325(isLNat(activate(XS)),activate(N), activate(X),activate(XS)) ; Marked_U323(tt,N,X,XS) >= Marked_activate(N) ; Marked_U323(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U323(tt,N,X,XS) >= Marked_activate(X) ; Marked_U323(tt,N,X,XS) >= Marked_isNaturalKind(activate(X)) ; Marked_U323(tt,N,X,XS) >= Marked_U324(isNaturalKind(activate(X)),activate(N), activate(X),activate(XS)) ; Marked_U322(tt,N,X,XS) >= Marked_activate(N) ; Marked_U322(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U322(tt,N,X,XS) >= Marked_activate(X) ; Marked_U322(tt,N,X,XS) >= Marked_isNatural(activate(X)) ; Marked_U322(tt,N,X,XS) >= Marked_U323(isNatural(activate(X)),activate(N), activate(X),activate(XS)) ; Marked_U32(tt,N,XS) >= Marked_activate(N) ; Marked_U32(tt,N,XS) >= Marked_activate(XS) ; Marked_U32(tt,N,XS) >= Marked_isLNat(activate(XS)) ; Marked_U32(tt,N,XS) >= Marked_U33(isLNat(activate(XS)),activate(N), activate(XS)) ; Marked_U312(tt,XS) >= Marked_activate(XS) ; Marked_U304(tt,Y) >= Marked_activate(Y) ; Marked_U303(tt,Y) >= Marked_activate(Y) ; Marked_U303(tt,Y) >= Marked_isLNatKind(activate(Y)) ; Marked_U303(tt,Y) >= Marked_U304(isLNatKind(activate(Y)),activate(Y)) ; Marked_U302(tt,Y) >= Marked_activate(Y) ; Marked_U302(tt,Y) >= Marked_isLNat(activate(Y)) ; Marked_U302(tt,Y) >= Marked_U303(isLNat(activate(Y)),activate(Y)) ; Marked_U294(tt,N,XS) >= Marked_activate(N) ; Marked_U294(tt,N,XS) >= Marked_activate(XS) ; Marked_U294(tt,N,XS) >= Marked_head(afterNth(activate(N),activate(XS))) ; Marked_U294(tt,N,XS) >= Marked_afterNth(activate(N),activate(XS)) ; Marked_U293(tt,N,XS) >= Marked_activate(N) ; Marked_U293(tt,N,XS) >= Marked_activate(XS) ; Marked_U293(tt,N,XS) >= Marked_isLNatKind(activate(XS)) ; Marked_U293(tt,N,XS) >= Marked_U294(isLNatKind(activate(XS)),activate(N), activate(XS)) ; Marked_U292(tt,N,XS) >= Marked_activate(N) ; Marked_U292(tt,N,XS) >= Marked_activate(XS) ; Marked_U292(tt,N,XS) >= Marked_isLNat(activate(XS)) ; Marked_U292(tt,N,XS) >= Marked_U293(isLNat(activate(XS)),activate(N), activate(XS)) ; Marked_U282(tt,N) >= Marked_activate(N) ; Marked_U255(tt,V2) >= Marked_activate(V2) ; Marked_U255(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U254(tt,V1,V2) >= Marked_activate(V1) ; Marked_U254(tt,V1,V2) >= Marked_activate(V2) ; Marked_U254(tt,V1,V2) >= Marked_isNatural(activate(V1)) ; Marked_U254(tt,V1,V2) >= Marked_U255(isNatural(activate(V1)),activate(V2)) ; Marked_U253(tt,V1,V2) >= Marked_activate(V1) ; Marked_U253(tt,V1,V2) >= Marked_activate(V2) ; Marked_U253(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U253(tt,V1,V2) >= Marked_U254(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U252(tt,V1,V2) >= Marked_activate(V1) ; Marked_U252(tt,V1,V2) >= Marked_activate(V2) ; Marked_U252(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U252(tt,V1,V2) >= Marked_U253(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U245(tt,V2) >= Marked_activate(V2) ; Marked_U245(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U244(tt,V1,V2) >= Marked_activate(V1) ; Marked_U244(tt,V1,V2) >= Marked_activate(V2) ; Marked_U244(tt,V1,V2) >= Marked_isLNat(activate(V1)) ; Marked_U244(tt,V1,V2) >= Marked_U245(isLNat(activate(V1)),activate(V2)) ; Marked_U243(tt,V1,V2) >= Marked_activate(V1) ; Marked_U243(tt,V1,V2) >= Marked_activate(V2) ; Marked_U243(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U243(tt,V1,V2) >= Marked_U244(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U242(tt,V1,V2) >= Marked_activate(V1) ; Marked_U242(tt,V1,V2) >= Marked_activate(V2) ; Marked_U242(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U242(tt,V1,V2) >= Marked_U243(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U24(tt,X) >= Marked_activate(X) ; Marked_U23(tt,X,Y) >= Marked_activate(X) ; Marked_U23(tt,X,Y) >= Marked_activate(Y) ; Marked_U23(tt,X,Y) >= Marked_isLNatKind(activate(Y)) ; Marked_U23(tt,X,Y) >= Marked_U24(isLNatKind(activate(Y)),activate(X)) ; Marked_U22(tt,X,Y) >= Marked_activate(X) ; Marked_U22(tt,X,Y) >= Marked_activate(Y) ; Marked_U22(tt,X,Y) >= Marked_isLNat(activate(Y)) ; Marked_U22(tt,X,Y) >= Marked_U23(isLNat(activate(Y)),activate(X),activate(Y)) ; Marked_U205(tt,V2) >= Marked_activate(V2) ; Marked_U205(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U204(tt,V1,V2) >= Marked_activate(V1) ; Marked_U204(tt,V1,V2) >= Marked_activate(V2) ; Marked_U204(tt,V1,V2) >= Marked_isNatural(activate(V1)) ; Marked_U204(tt,V1,V2) >= Marked_U205(isNatural(activate(V1)),activate(V2)) ; Marked_U203(tt,V1,V2) >= Marked_activate(V1) ; Marked_U203(tt,V1,V2) >= Marked_activate(V2) ; Marked_U203(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U203(tt,V1,V2) >= Marked_U204(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U202(tt,V1,V2) >= Marked_activate(V1) ; Marked_U202(tt,V1,V2) >= Marked_activate(V2) ; Marked_U202(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U202(tt,V1,V2) >= Marked_U203(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U192(tt,V1) >= Marked_activate(V1) ; Marked_U192(tt,V1) >= Marked_isNatural(activate(V1)) ; Marked_U182(tt,V1) >= Marked_activate(V1) ; Marked_U182(tt,V1) >= Marked_isLNat(activate(V1)) ; Marked_U14(tt,N,XS) >= Marked_activate(N) ; Marked_U14(tt,N,XS) >= Marked_activate(XS) ; Marked_U14(tt,N,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U14(tt,N,XS) >= Marked_snd(splitAt(activate(N),activate(XS))) ; Marked_U13(tt,N,XS) >= Marked_activate(N) ; Marked_U13(tt,N,XS) >= Marked_activate(XS) ; Marked_U13(tt,N,XS) >= Marked_isLNatKind(activate(XS)) ; Marked_U13(tt,N,XS) >= Marked_U14(isLNatKind(activate(XS)),activate(N), activate(XS)) ; Marked_U12(tt,N,XS) >= Marked_activate(N) ; Marked_U12(tt,N,XS) >= Marked_activate(XS) ; Marked_U12(tt,N,XS) >= Marked_isLNat(activate(XS)) ; Marked_U12(tt,N,XS) >= Marked_U13(isLNat(activate(XS)),activate(N), activate(XS)) ; Marked_U105(tt,V2) >= Marked_activate(V2) ; Marked_U105(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U104(tt,V1,V2) >= Marked_activate(V1) ; Marked_U104(tt,V1,V2) >= Marked_activate(V2) ; Marked_U104(tt,V1,V2) >= Marked_isNatural(activate(V1)) ; Marked_U104(tt,V1,V2) >= Marked_U105(isNatural(activate(V1)),activate(V2)) ; Marked_U103(tt,V1,V2) >= Marked_activate(V1) ; Marked_U103(tt,V1,V2) >= Marked_activate(V2) ; Marked_U103(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U103(tt,V1,V2) >= Marked_U104(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; Marked_U102(tt,V1,V2) >= Marked_activate(V1) ; Marked_U102(tt,V1,V2) >= Marked_activate(V2) ; Marked_U102(tt,V1,V2) >= Marked_isLNatKind(activate(V2)) ; Marked_U102(tt,V1,V2) >= Marked_U103(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } + Disjunctions:{ { Marked_activate(n__natsFrom(X)) > Marked_natsFrom(X) ; } { Marked_activate(n__afterNth(X1,X2)) > Marked_afterNth(X1,X2) ; } { Marked_activate(n__fst(X)) > Marked_fst(X) ; } { Marked_activate(n__snd(X)) > Marked_snd(X) ; } { Marked_activate(n__tail(X)) > Marked_tail(X) ; } { Marked_activate(n__take(X1,X2)) > Marked_take(X1,X2) ; } { Marked_activate(n__head(X)) > Marked_head(X) ; } { Marked_activate(n__sel(X1,X2)) > Marked_sel(X1,X2) ; } { Marked_activate(n__splitAt(X1,X2)) > Marked_splitAt(X1,X2) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_activate(XS) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_isNatural(N) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_U321(isNatural(N),N,X,activate(XS)) ; } { Marked_splitAt(0,XS) > Marked_U311(isLNat(XS),XS) ; } { Marked_splitAt(0,XS) > Marked_isLNat(XS) ; } { Marked_sel(N,XS) > Marked_isNatural(N) ; } { Marked_sel(N,XS) > Marked_U291(isNatural(N),N,XS) ; } { Marked_head(cons(N,XS)) > Marked_activate(XS) ; } { Marked_head(cons(N,XS)) > Marked_isNatural(N) ; } { Marked_head(cons(N,XS)) > Marked_U31(isNatural(N),N,activate(XS)) ; } { Marked_take(N,XS) > Marked_U341(isNatural(N),N,XS) ; } { Marked_take(N,XS) > Marked_isNatural(N) ; } { Marked_tail(cons(N,XS)) > Marked_activate(XS) ; } { Marked_tail(cons(N,XS)) > Marked_isNatural(N) ; } { Marked_tail(cons(N,XS)) > Marked_U331(isNatural(N),N,activate(XS)) ; } { Marked_snd(pair(X,Y)) > Marked_isLNat(X) ; } { Marked_snd(pair(X,Y)) > Marked_U301(isLNat(X),X,Y) ; } { Marked_fst(pair(X,Y)) > Marked_isLNat(X) ; } { Marked_fst(pair(X,Y)) > Marked_U21(isLNat(X),X,Y) ; } { Marked_afterNth(N,XS) > Marked_isNatural(N) ; } { Marked_afterNth(N,XS) > Marked_U11(isNatural(N),N,XS) ; } { Marked_natsFrom(N) > Marked_isNatural(N) ; } { Marked_natsFrom(N) > Marked_U281(isNatural(N),N) ; } { Marked_U341(tt,N,XS) > Marked_activate(N) ; } { Marked_U341(tt,N,XS) > Marked_activate(XS) ; } { Marked_U341(tt,N,XS) > Marked_isNaturalKind(activate(N)) ; } { Marked_U341(tt,N,XS) > Marked_U342(isNaturalKind(activate(N)),activate(N), activate(XS)) ; } { Marked_isNatural(n__head(V1)) > Marked_activate(V1) ; } { Marked_isNatural(n__head(V1)) > Marked_isLNatKind(activate(V1)) ; } { Marked_isNatural(n__head(V1)) > Marked_U181(isLNatKind(activate(V1)), activate(V1)) ; } { Marked_isNatural(n__s(V1)) > Marked_activate(V1) ; } { Marked_isNatural(n__s(V1)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isNatural(n__s(V1)) > Marked_U191(isNaturalKind(activate(V1)), activate(V1)) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_U201(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_U331(tt,N,XS) > Marked_activate(N) ; } { Marked_U331(tt,N,XS) > Marked_activate(XS) ; } { Marked_U331(tt,N,XS) > Marked_isNaturalKind(activate(N)) ; } { Marked_U331(tt,N,XS) > Marked_U332(isNaturalKind(activate(N)),activate(XS)) ; } { Marked_U321(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U321(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U321(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U321(tt,N,X,XS) > Marked_isNaturalKind(activate(N)) ; } { Marked_U321(tt,N,X,XS) > Marked_U322(isNaturalKind(activate(N)),activate(N), activate(X),activate(XS)) ; } { Marked_U311(tt,XS) > Marked_activate(XS) ; } { Marked_U311(tt,XS) > Marked_isLNatKind(activate(XS)) ; } { Marked_U311(tt,XS) > Marked_U312(isLNatKind(activate(XS)),activate(XS)) ; } { Marked_isLNat(n__natsFrom(V1)) > Marked_activate(V1) ; } { Marked_isLNat(n__natsFrom(V1)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNat(n__natsFrom(V1)) > Marked_U71(isNaturalKind(activate(V1)), activate(V1)) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_activate(V1) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_U41(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_U51(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_isLNat(n__fst(V1)) > Marked_activate(V1) ; } { Marked_isLNat(n__fst(V1)) > Marked_isPLNatKind(activate(V1)) ; } { Marked_isLNat(n__fst(V1)) > Marked_U61(isPLNatKind(activate(V1)), activate(V1)) ; } { Marked_isLNat(n__snd(V1)) > Marked_activate(V1) ; } { Marked_isLNat(n__snd(V1)) > Marked_isPLNatKind(activate(V1)) ; } { Marked_isLNat(n__snd(V1)) > Marked_U81(isPLNatKind(activate(V1)), activate(V1)) ; } { Marked_isLNat(n__tail(V1)) > Marked_activate(V1) ; } { Marked_isLNat(n__tail(V1)) > Marked_isLNatKind(activate(V1)) ; } { Marked_isLNat(n__tail(V1)) > Marked_U91(isLNatKind(activate(V1)), activate(V1)) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_activate(V1) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_U101(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_U301(tt,X,Y) > Marked_activate(X) ; } { Marked_U301(tt,X,Y) > Marked_activate(Y) ; } { Marked_U301(tt,X,Y) > Marked_isLNatKind(activate(X)) ; } { Marked_U301(tt,X,Y) > Marked_U302(isLNatKind(activate(X)),activate(Y)) ; } { Marked_U291(tt,N,XS) > Marked_activate(N) ; } { Marked_U291(tt,N,XS) > Marked_activate(XS) ; } { Marked_U291(tt,N,XS) > Marked_isNaturalKind(activate(N)) ; } { Marked_U291(tt,N,XS) > Marked_U292(isNaturalKind(activate(N)),activate(N), activate(XS)) ; } { Marked_U281(tt,N) > Marked_activate(N) ; } { Marked_U281(tt,N) > Marked_isNaturalKind(activate(N)) ; } { Marked_U281(tt,N) > Marked_U282(isNaturalKind(activate(N)),activate(N)) ; } { Marked_isPLNatKind(n__pair(V1,V2)) > Marked_activate(V1) ; } { Marked_isPLNatKind(n__pair(V1,V2)) > Marked_activate(V2) ; } { Marked_isPLNatKind(n__pair(V1,V2)) > Marked_U261(isLNatKind(activate(V1)), activate(V2)) ; } { Marked_isPLNatKind(n__pair(V1,V2)) > Marked_isLNatKind(activate(V1)) ; } { Marked_isPLNatKind(n__splitAt(V1,V2)) > Marked_activate(V1) ; } { Marked_isPLNatKind(n__splitAt(V1,V2)) > Marked_activate(V2) ; } { Marked_isPLNatKind(n__splitAt(V1,V2)) > Marked_U271(isNaturalKind(activate( V1)), activate(V2)) ; } { Marked_isPLNatKind(n__splitAt(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_U271(tt,V2) > Marked_activate(V2) ; } { Marked_U271(tt,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_isNaturalKind(n__head(V1)) > Marked_activate(V1) ; } { Marked_isNaturalKind(n__head(V1)) > Marked_isLNatKind(activate(V1)) ; } { Marked_isNaturalKind(n__s(V1)) > Marked_activate(V1) ; } { Marked_isNaturalKind(n__s(V1)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isNaturalKind(n__sel(V1,V2)) > Marked_activate(V1) ; } { Marked_isNaturalKind(n__sel(V1,V2)) > Marked_activate(V2) ; } { Marked_isNaturalKind(n__sel(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isNaturalKind(n__sel(V1,V2)) > Marked_U231(isNaturalKind(activate(V1)), activate(V2)) ; } { Marked_U261(tt,V2) > Marked_activate(V2) ; } { Marked_U261(tt,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_isLNatKind(n__natsFrom(V1)) > Marked_activate(V1) ; } { Marked_isLNatKind(n__natsFrom(V1)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNatKind(n__afterNth(V1,V2)) > Marked_activate(V1) ; } { Marked_isLNatKind(n__afterNth(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNatKind(n__afterNth(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNatKind(n__afterNth(V1,V2)) > Marked_U111(isNaturalKind(activate( V1)), activate(V2)) ; } { Marked_isLNatKind(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isLNatKind(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNatKind(n__cons(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNatKind(n__cons(V1,V2)) > Marked_U121(isNaturalKind(activate(V1)), activate(V2)) ; } { Marked_isLNatKind(n__fst(V1)) > Marked_activate(V1) ; } { Marked_isLNatKind(n__fst(V1)) > Marked_isPLNatKind(activate(V1)) ; } { Marked_isLNatKind(n__snd(V1)) > Marked_activate(V1) ; } { Marked_isLNatKind(n__snd(V1)) > Marked_isPLNatKind(activate(V1)) ; } { Marked_isLNatKind(n__tail(V1)) > Marked_activate(V1) ; } { Marked_isLNatKind(n__tail(V1)) > Marked_isLNatKind(activate(V1)) ; } { Marked_isLNatKind(n__take(V1,V2)) > Marked_activate(V1) ; } { Marked_isLNatKind(n__take(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNatKind(n__take(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNatKind(n__take(V1,V2)) > Marked_U171(isNaturalKind(activate(V1)), activate(V2)) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_activate(V1) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_activate(V2) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_isLNatKind(activate(V1)) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_U241(isLNatKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_activate(V1) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_activate(V2) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_U251(isNaturalKind(activate(V1)), activate(V1),activate(V2)) ; } { Marked_U251(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U251(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U251(tt,V1,V2) > Marked_isNaturalKind(activate(V1)) ; } { Marked_U251(tt,V1,V2) > Marked_U252(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_U241(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U241(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U241(tt,V1,V2) > Marked_isLNatKind(activate(V1)) ; } { Marked_U241(tt,V1,V2) > Marked_U242(isLNatKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_U231(tt,V2) > Marked_activate(V2) ; } { Marked_U231(tt,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U201(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U201(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U201(tt,V1,V2) > Marked_isNaturalKind(activate(V1)) ; } { Marked_U201(tt,V1,V2) > Marked_U202(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_U191(tt,V1) > Marked_activate(V1) ; } { Marked_U191(tt,V1) > Marked_isNaturalKind(activate(V1)) ; } { Marked_U191(tt,V1) > Marked_U192(isNaturalKind(activate(V1)),activate(V1)) ; } { Marked_U181(tt,V1) > Marked_activate(V1) ; } { Marked_U181(tt,V1) > Marked_isLNatKind(activate(V1)) ; } { Marked_U181(tt,V1) > Marked_U182(isLNatKind(activate(V1)),activate(V1)) ; } { Marked_U171(tt,V2) > Marked_activate(V2) ; } { Marked_U171(tt,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U121(tt,V2) > Marked_activate(V2) ; } { Marked_U121(tt,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U111(tt,V2) > Marked_activate(V2) ; } { Marked_U111(tt,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U101(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U101(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U101(tt,V1,V2) > Marked_isNaturalKind(activate(V1)) ; } { Marked_U101(tt,V1,V2) > Marked_U102(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_U91(tt,V1) > Marked_activate(V1) ; } { Marked_U91(tt,V1) > Marked_isLNatKind(activate(V1)) ; } { Marked_U91(tt,V1) > Marked_U92(isLNatKind(activate(V1)),activate(V1)) ; } { Marked_U81(tt,V1) > Marked_activate(V1) ; } { Marked_U81(tt,V1) > Marked_isPLNatKind(activate(V1)) ; } { Marked_U81(tt,V1) > Marked_U82(isPLNatKind(activate(V1)),activate(V1)) ; } { Marked_U71(tt,V1) > Marked_activate(V1) ; } { Marked_U71(tt,V1) > Marked_isNaturalKind(activate(V1)) ; } { Marked_U71(tt,V1) > Marked_U72(isNaturalKind(activate(V1)),activate(V1)) ; } { Marked_U61(tt,V1) > Marked_activate(V1) ; } { Marked_U61(tt,V1) > Marked_isPLNatKind(activate(V1)) ; } { Marked_U61(tt,V1) > Marked_U62(isPLNatKind(activate(V1)),activate(V1)) ; } { Marked_U51(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U51(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U51(tt,V1,V2) > Marked_isNaturalKind(activate(V1)) ; } { Marked_U51(tt,V1,V2) > Marked_U52(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_U41(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U41(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U41(tt,V1,V2) > Marked_isNaturalKind(activate(V1)) ; } { Marked_U41(tt,V1,V2) > Marked_U42(isNaturalKind(activate(V1)),activate(V1), activate(V2)) ; } { Marked_U31(tt,N,XS) > Marked_activate(N) ; } { Marked_U31(tt,N,XS) > Marked_activate(XS) ; } { Marked_U31(tt,N,XS) > Marked_isNaturalKind(activate(N)) ; } { Marked_U31(tt,N,XS) > Marked_U32(isNaturalKind(activate(N)),activate(N), activate(XS)) ; } { Marked_U21(tt,X,Y) > Marked_activate(X) ; } { Marked_U21(tt,X,Y) > Marked_activate(Y) ; } { Marked_U21(tt,X,Y) > Marked_isLNatKind(activate(X)) ; } { Marked_U21(tt,X,Y) > Marked_U22(isLNatKind(activate(X)),activate(X), activate(Y)) ; } { Marked_U11(tt,N,XS) > Marked_activate(N) ; } { Marked_U11(tt,N,XS) > Marked_activate(XS) ; } { Marked_U11(tt,N,XS) > Marked_isNaturalKind(activate(N)) ; } { Marked_U11(tt,N,XS) > Marked_U12(isNaturalKind(activate(N)),activate(N), activate(XS)) ; } { Marked_U92(tt,V1) > Marked_activate(V1) ; } { Marked_U92(tt,V1) > Marked_isLNat(activate(V1)) ; } { Marked_U82(tt,V1) > Marked_activate(V1) ; } { Marked_U82(tt,V1) > Marked_isPLNat(activate(V1)) ; } { Marked_U72(tt,V1) > Marked_activate(V1) ; } { Marked_U72(tt,V1) > Marked_isNatural(activate(V1)) ; } { Marked_U62(tt,V1) > Marked_activate(V1) ; } { Marked_U62(tt,V1) > Marked_isPLNat(activate(V1)) ; } { Marked_U55(tt,V2) > Marked_activate(V2) ; } { Marked_U55(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U54(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U54(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U54(tt,V1,V2) > Marked_isNatural(activate(V1)) ; } { Marked_U54(tt,V1,V2) > Marked_U55(isNatural(activate(V1)),activate(V2)) ; } { Marked_U53(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U53(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U53(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U53(tt,V1,V2) > Marked_U54(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U52(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U52(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U52(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U52(tt,V1,V2) > Marked_U53(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U45(tt,V2) > Marked_activate(V2) ; } { Marked_U45(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U44(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U44(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U44(tt,V1,V2) > Marked_isNatural(activate(V1)) ; } { Marked_U44(tt,V1,V2) > Marked_U45(isNatural(activate(V1)),activate(V2)) ; } { Marked_U43(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U43(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U43(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U43(tt,V1,V2) > Marked_U44(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U42(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U42(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U42(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U42(tt,V1,V2) > Marked_U43(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U344(tt,N,XS) > Marked_activate(N) ; } { Marked_U344(tt,N,XS) > Marked_activate(XS) ; } { Marked_U344(tt,N,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U344(tt,N,XS) > Marked_fst(splitAt(activate(N),activate(XS))) ; } { Marked_U343(tt,N,XS) > Marked_activate(N) ; } { Marked_U343(tt,N,XS) > Marked_activate(XS) ; } { Marked_U343(tt,N,XS) > Marked_isLNatKind(activate(XS)) ; } { Marked_U343(tt,N,XS) > Marked_U344(isLNatKind(activate(XS)),activate(N), activate(XS)) ; } { Marked_U342(tt,N,XS) > Marked_activate(N) ; } { Marked_U342(tt,N,XS) > Marked_activate(XS) ; } { Marked_U342(tt,N,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U342(tt,N,XS) > Marked_U343(isLNat(activate(XS)),activate(N), activate(XS)) ; } { Marked_U34(tt,N) > Marked_activate(N) ; } { Marked_U334(tt,XS) > Marked_activate(XS) ; } { Marked_U333(tt,XS) > Marked_activate(XS) ; } { Marked_U333(tt,XS) > Marked_isLNatKind(activate(XS)) ; } { Marked_U333(tt,XS) > Marked_U334(isLNatKind(activate(XS)),activate(XS)) ; } { Marked_U332(tt,XS) > Marked_activate(XS) ; } { Marked_U332(tt,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U332(tt,XS) > Marked_U333(isLNat(activate(XS)),activate(XS)) ; } { Marked_U33(tt,N,XS) > Marked_activate(N) ; } { Marked_U33(tt,N,XS) > Marked_activate(XS) ; } { Marked_U33(tt,N,XS) > Marked_isLNatKind(activate(XS)) ; } { Marked_U33(tt,N,XS) > Marked_U34(isLNatKind(activate(XS)),activate(N)) ; } { Marked_U327(pair(YS,ZS),X) > Marked_activate(X) ; } { Marked_U326(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U326(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U326(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U326(tt,N,X,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U326(tt,N,X,XS) > Marked_U327(splitAt(activate(N),activate(XS)), activate(X)) ; } { Marked_U325(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U325(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U325(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U325(tt,N,X,XS) > Marked_isLNatKind(activate(XS)) ; } { Marked_U325(tt,N,X,XS) > Marked_U326(isLNatKind(activate(XS)),activate(N), activate(X),activate(XS)) ; } { Marked_U324(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U324(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U324(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U324(tt,N,X,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U324(tt,N,X,XS) > Marked_U325(isLNat(activate(XS)),activate(N), activate(X),activate(XS)) ; } { Marked_U323(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U323(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U323(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U323(tt,N,X,XS) > Marked_isNaturalKind(activate(X)) ; } { Marked_U323(tt,N,X,XS) > Marked_U324(isNaturalKind(activate(X)),activate(N), activate(X),activate(XS)) ; } { Marked_U322(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U322(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U322(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U322(tt,N,X,XS) > Marked_isNatural(activate(X)) ; } { Marked_U322(tt,N,X,XS) > Marked_U323(isNatural(activate(X)),activate(N), activate(X),activate(XS)) ; } { Marked_U32(tt,N,XS) > Marked_activate(N) ; } { Marked_U32(tt,N,XS) > Marked_activate(XS) ; } { Marked_U32(tt,N,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U32(tt,N,XS) > Marked_U33(isLNat(activate(XS)),activate(N), activate(XS)) ; } { Marked_U312(tt,XS) > Marked_activate(XS) ; } { Marked_U304(tt,Y) > Marked_activate(Y) ; } { Marked_U303(tt,Y) > Marked_activate(Y) ; } { Marked_U303(tt,Y) > Marked_isLNatKind(activate(Y)) ; } { Marked_U303(tt,Y) > Marked_U304(isLNatKind(activate(Y)),activate(Y)) ; } { Marked_U302(tt,Y) > Marked_activate(Y) ; } { Marked_U302(tt,Y) > Marked_isLNat(activate(Y)) ; } { Marked_U302(tt,Y) > Marked_U303(isLNat(activate(Y)),activate(Y)) ; } { Marked_U294(tt,N,XS) > Marked_activate(N) ; } { Marked_U294(tt,N,XS) > Marked_activate(XS) ; } { Marked_U294(tt,N,XS) > Marked_head(afterNth(activate(N),activate(XS))) ; } { Marked_U294(tt,N,XS) > Marked_afterNth(activate(N),activate(XS)) ; } { Marked_U293(tt,N,XS) > Marked_activate(N) ; } { Marked_U293(tt,N,XS) > Marked_activate(XS) ; } { Marked_U293(tt,N,XS) > Marked_isLNatKind(activate(XS)) ; } { Marked_U293(tt,N,XS) > Marked_U294(isLNatKind(activate(XS)),activate(N), activate(XS)) ; } { Marked_U292(tt,N,XS) > Marked_activate(N) ; } { Marked_U292(tt,N,XS) > Marked_activate(XS) ; } { Marked_U292(tt,N,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U292(tt,N,XS) > Marked_U293(isLNat(activate(XS)),activate(N), activate(XS)) ; } { Marked_U282(tt,N) > Marked_activate(N) ; } { Marked_U255(tt,V2) > Marked_activate(V2) ; } { Marked_U255(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U254(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U254(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U254(tt,V1,V2) > Marked_isNatural(activate(V1)) ; } { Marked_U254(tt,V1,V2) > Marked_U255(isNatural(activate(V1)),activate(V2)) ; } { Marked_U253(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U253(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U253(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U253(tt,V1,V2) > Marked_U254(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U252(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U252(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U252(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U252(tt,V1,V2) > Marked_U253(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U245(tt,V2) > Marked_activate(V2) ; } { Marked_U245(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U244(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U244(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U244(tt,V1,V2) > Marked_isLNat(activate(V1)) ; } { Marked_U244(tt,V1,V2) > Marked_U245(isLNat(activate(V1)),activate(V2)) ; } { Marked_U243(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U243(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U243(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U243(tt,V1,V2) > Marked_U244(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U242(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U242(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U242(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U242(tt,V1,V2) > Marked_U243(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U24(tt,X) > Marked_activate(X) ; } { Marked_U23(tt,X,Y) > Marked_activate(X) ; } { Marked_U23(tt,X,Y) > Marked_activate(Y) ; } { Marked_U23(tt,X,Y) > Marked_isLNatKind(activate(Y)) ; } { Marked_U23(tt,X,Y) > Marked_U24(isLNatKind(activate(Y)),activate(X)) ; } { Marked_U22(tt,X,Y) > Marked_activate(X) ; } { Marked_U22(tt,X,Y) > Marked_activate(Y) ; } { Marked_U22(tt,X,Y) > Marked_isLNat(activate(Y)) ; } { Marked_U22(tt,X,Y) > Marked_U23(isLNat(activate(Y)),activate(X),activate(Y)) ; } { Marked_U205(tt,V2) > Marked_activate(V2) ; } { Marked_U205(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U204(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U204(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U204(tt,V1,V2) > Marked_isNatural(activate(V1)) ; } { Marked_U204(tt,V1,V2) > Marked_U205(isNatural(activate(V1)),activate(V2)) ; } { Marked_U203(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U203(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U203(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U203(tt,V1,V2) > Marked_U204(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U202(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U202(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U202(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U202(tt,V1,V2) > Marked_U203(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U192(tt,V1) > Marked_activate(V1) ; } { Marked_U192(tt,V1) > Marked_isNatural(activate(V1)) ; } { Marked_U182(tt,V1) > Marked_activate(V1) ; } { Marked_U182(tt,V1) > Marked_isLNat(activate(V1)) ; } { Marked_U14(tt,N,XS) > Marked_activate(N) ; } { Marked_U14(tt,N,XS) > Marked_activate(XS) ; } { Marked_U14(tt,N,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U14(tt,N,XS) > Marked_snd(splitAt(activate(N),activate(XS))) ; } { Marked_U13(tt,N,XS) > Marked_activate(N) ; } { Marked_U13(tt,N,XS) > Marked_activate(XS) ; } { Marked_U13(tt,N,XS) > Marked_isLNatKind(activate(XS)) ; } { Marked_U13(tt,N,XS) > Marked_U14(isLNatKind(activate(XS)),activate(N), activate(XS)) ; } { Marked_U12(tt,N,XS) > Marked_activate(N) ; } { Marked_U12(tt,N,XS) > Marked_activate(XS) ; } { Marked_U12(tt,N,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U12(tt,N,XS) > Marked_U13(isLNat(activate(XS)),activate(N), activate(XS)) ; } { Marked_U105(tt,V2) > Marked_activate(V2) ; } { Marked_U105(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U104(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U104(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U104(tt,V1,V2) > Marked_isNatural(activate(V1)) ; } { Marked_U104(tt,V1,V2) > Marked_U105(isNatural(activate(V1)),activate(V2)) ; } { Marked_U103(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U103(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U103(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U103(tt,V1,V2) > Marked_U104(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } { Marked_U102(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U102(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U102(tt,V1,V2) > Marked_isLNatKind(activate(V2)) ; } { Marked_U102(tt,V1,V2) > Marked_U103(isLNatKind(activate(V2)),activate(V1), activate(V2)) ; } } === TIMER virtual : 10.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 10.000000 === === STOPING TIMER real === Sat timeout reached === STOPING TIMER virtual === Time out for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === Time out for these parameters. === TIMER virtual : 15.000000 === Entering poly_solver Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat timeout reached === STOPING TIMER virtual === Time out for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat timeout reached === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (ID_CRIT) NOT SOLVED No proof found Cime worked for 139.956665 seconds (real time) Cime Exit Status: 0