- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] U101(tt,V1,V2) -> U102(isNatural(activate(V1)),activate(V2)) [2] U102(tt,V2) -> U103(isLNat(activate(V2))) [3] U103(tt) -> tt [4] U11(tt,N,XS) -> snd(splitAt(activate(N),activate(XS))) [5] U111(tt,V1) -> U112(isLNat(activate(V1))) [6] U112(tt) -> tt [7] U121(tt,V1) -> U122(isNatural(activate(V1))) [8] U122(tt) -> tt [9] U131(tt,V1,V2) -> U132(isNatural(activate(V1)),activate(V2)) [10] U132(tt,V2) -> U133(isLNat(activate(V2))) [11] U133(tt) -> tt [12] U141(tt,V1,V2) -> U142(isLNat(activate(V1)),activate(V2)) [13] U142(tt,V2) -> U143(isLNat(activate(V2))) [14] U143(tt) -> tt [15] U151(tt,V1,V2) -> U152(isNatural(activate(V1)),activate(V2)) [16] U152(tt,V2) -> U153(isLNat(activate(V2))) [17] U153(tt) -> tt [18] U161(tt,N) -> cons(activate(N),n__natsFrom(s(activate(N)))) [19] U171(tt,N,XS) -> head(afterNth(activate(N),activate(XS))) [20] U181(tt,Y) -> activate(Y) [21] U191(tt,XS) -> pair(nil,activate(XS)) [22] U201(tt,N,X,XS) -> U202(splitAt(activate(N),activate(XS)),activate(X)) [23] U202(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) [24] U21(tt,X) -> activate(X) [25] U211(tt,XS) -> activate(XS) [26] U221(tt,N,XS) -> fst(splitAt(activate(N),activate(XS))) [27] U31(tt,N) -> activate(N) [28] U41(tt,V1,V2) -> U42(isNatural(activate(V1)),activate(V2)) [29] U42(tt,V2) -> U43(isLNat(activate(V2))) [30] U43(tt) -> tt [31] U51(tt,V1,V2) -> U52(isNatural(activate(V1)),activate(V2)) [32] U52(tt,V2) -> U53(isLNat(activate(V2))) [33] U53(tt) -> tt [34] U61(tt,V1) -> U62(isPLNat(activate(V1))) [35] U62(tt) -> tt [36] U71(tt,V1) -> U72(isNatural(activate(V1))) [37] U72(tt) -> tt [38] U81(tt,V1) -> U82(isPLNat(activate(V1))) [39] U82(tt) -> tt [40] U91(tt,V1) -> U92(isLNat(activate(V1))) [41] U92(tt) -> tt [42] afterNth(N,XS) -> U11(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) [43] and(tt,X) -> activate(X) [44] fst(pair(X,Y)) -> U21(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))),X) [45] head(cons(N,XS)) -> U31(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS)))),N) [46] isLNat(n__nil) -> tt [47] isLNat(n__afterNth(V1,V2)) -> U41(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1), activate(V2)) [48] isLNat(n__cons(V1,V2)) -> U51(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1), activate(V2)) [49] isLNat(n__fst(V1)) -> U61(isPLNatKind(activate(V1)),activate(V1)) [50] isLNat(n__natsFrom(V1)) -> U71(isNaturalKind(activate(V1)),activate(V1)) [51] isLNat(n__snd(V1)) -> U81(isPLNatKind(activate(V1)),activate(V1)) [52] isLNat(n__tail(V1)) -> U91(isLNatKind(activate(V1)),activate(V1)) [53] isLNat(n__take(V1,V2)) -> U101(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))), activate(V1),activate(V2)) [54] isLNatKind(n__nil) -> tt [55] isLNatKind(n__afterNth(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) [56] isLNatKind(n__cons(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) [57] isLNatKind(n__fst(V1)) -> isPLNatKind(activate(V1)) [58] isLNatKind(n__natsFrom(V1)) -> isNaturalKind(activate(V1)) [59] isLNatKind(n__snd(V1)) -> isPLNatKind(activate(V1)) [60] isLNatKind(n__tail(V1)) -> isLNatKind(activate(V1)) [61] isLNatKind(n__take(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) [62] isNatural(n__0) -> tt [63] isNatural(n__head(V1)) -> U111(isLNatKind(activate(V1)),activate(V1)) [64] isNatural(n__s(V1)) -> U121(isNaturalKind(activate(V1)),activate(V1)) [65] isNatural(n__sel(V1,V2)) -> U131(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))), activate(V1),activate(V2)) [66] isNaturalKind(n__0) -> tt [67] isNaturalKind(n__head(V1)) -> isLNatKind(activate(V1)) [68] isNaturalKind(n__s(V1)) -> isNaturalKind(activate(V1)) [69] isNaturalKind(n__sel(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) [70] isPLNat(n__pair(V1,V2)) -> U141(and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))),activate(V1), activate(V2)) [71] isPLNat(n__splitAt(V1,V2)) -> U151(and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))), activate(V1),activate(V2)) [72] isPLNatKind(n__pair(V1,V2)) -> and(isLNatKind(activate(V1)),n__isLNatKind(activate(V2))) [73] isPLNatKind(n__splitAt(V1,V2)) -> and(isNaturalKind(activate(V1)),n__isLNatKind(activate(V2))) [74] natsFrom(N) -> U161(and(isNatural(N),n__isNaturalKind(N)),N) [75] sel(N,XS) -> U171(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) [76] snd(pair(X,Y)) -> U181(and(and(isLNat(X),n__isLNatKind(X)),n__and(isLNat(Y),n__isLNatKind(Y))), Y) [77] splitAt(0,XS) -> U191(and(isLNat(XS),n__isLNatKind(XS)),XS) [78] splitAt(s(N),cons(X,XS)) -> U201(and(and(isNatural(N),n__isNaturalKind(N)), n__and(and(isNatural(X),n__isNaturalKind(X)), n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS))))),N, X,activate(XS)) [79] tail(cons(N,XS)) -> U211(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(activate(XS)),n__isLNatKind(activate(XS)))),activate(XS)) [80] take(N,XS) -> U221(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) [81] natsFrom(X) -> n__natsFrom(X) [82] isNaturalKind(X) -> n__isNaturalKind(X) [83] and(X1,X2) -> n__and(X1,X2) [84] isLNatKind(X) -> n__isLNatKind(X) [85] nil -> n__nil [86] afterNth(X1,X2) -> n__afterNth(X1,X2) [87] cons(X1,X2) -> n__cons(X1,X2) [88] fst(X) -> n__fst(X) [89] snd(X) -> n__snd(X) [90] tail(X) -> n__tail(X) [91] take(X1,X2) -> n__take(X1,X2) [92] 0 -> n__0 [93] head(X) -> n__head(X) [94] s(X) -> n__s(X) [95] sel(X1,X2) -> n__sel(X1,X2) [96] pair(X1,X2) -> n__pair(X1,X2) [97] splitAt(X1,X2) -> n__splitAt(X1,X2) [98] activate(n__natsFrom(X)) -> natsFrom(X) [99] activate(n__isNaturalKind(X)) -> isNaturalKind(X) [100] activate(n__and(X1,X2)) -> and(X1,X2) [101] activate(n__isLNatKind(X)) -> isLNatKind(X) [102] activate(n__nil) -> nil [103] activate(n__afterNth(X1,X2)) -> afterNth(X1,X2) [104] activate(n__cons(X1,X2)) -> cons(X1,X2) [105] activate(n__fst(X)) -> fst(X) [106] activate(n__snd(X)) -> snd(X) [107] activate(n__tail(X)) -> tail(X) [108] activate(n__take(X1,X2)) -> take(X1,X2) [109] activate(n__0) -> 0 [110] activate(n__head(X)) -> head(X) [111] activate(n__s(X)) -> s(X) [112] activate(n__sel(X1,X2)) -> sel(X1,X2) [113] activate(n__pair(X1,X2)) -> pair(X1,X2) [114] activate(n__splitAt(X1,X2)) -> splitAt(X1,X2) [115] 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,V2) >= U103(isLNat(activate(V2))) ; isNatural(n__0) >= tt ; isNatural(n__head(V1)) >= U111(isLNatKind(activate(V1)),activate(V1)) ; isNatural(n__s(V1)) >= U121(isNaturalKind(activate(V1)),activate(V1)) ; isNatural(n__sel(V1,V2)) >= U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),activate(V1), activate(V2)) ; activate(n__natsFrom(X)) >= natsFrom(X) ; activate(n__isNaturalKind(X)) >= isNaturalKind(X) ; activate(n__and(X1,X2)) >= and(X1,X2) ; activate(n__isLNatKind(X)) >= isLNatKind(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(isNatural(activate(V1)),activate(V2)) ; U103(tt) >= tt ; isLNat(n__natsFrom(V1)) >= U71(isNaturalKind(activate(V1)),activate(V1)) ; isLNat(n__nil) >= tt ; isLNat(n__afterNth(V1,V2)) >= U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),activate(V1), activate(V2)) ; isLNat(n__cons(V1,V2)) >= U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),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(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))),activate(V1), activate(V2)) ; snd(pair(X,Y)) >= U181(and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))),Y) ; snd(X) >= n__snd(X) ; splitAt(s(N),cons(X,XS)) >= U201(and(and(isNatural(N),n__isNaturalKind(N)), n__and(and(isNatural(X), n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))), N,X,activate(XS)) ; splitAt(0,XS) >= U191(and(isLNat(XS),n__isLNatKind(XS)),XS) ; splitAt(X1,X2) >= n__splitAt(X1,X2) ; U11(tt,N,XS) >= snd(splitAt(activate(N),activate(XS))) ; U112(tt) >= tt ; U111(tt,V1) >= U112(isLNat(activate(V1))) ; U122(tt) >= tt ; U121(tt,V1) >= U122(isNatural(activate(V1))) ; U132(tt,V2) >= U133(isLNat(activate(V2))) ; U131(tt,V1,V2) >= U132(isNatural(activate(V1)),activate(V2)) ; U133(tt) >= tt ; U142(tt,V2) >= U143(isLNat(activate(V2))) ; U141(tt,V1,V2) >= U142(isLNat(activate(V1)),activate(V2)) ; U143(tt) >= tt ; U152(tt,V2) >= U153(isLNat(activate(V2))) ; U151(tt,V1,V2) >= U152(isNatural(activate(V1)),activate(V2)) ; U153(tt) >= tt ; cons(X1,X2) >= n__cons(X1,X2) ; s(X) >= n__s(X) ; U161(tt,N) >= cons(activate(N),n__natsFrom(s(activate(N)))) ; head(cons(N,XS)) >= U31(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),N) ; head(X) >= n__head(X) ; afterNth(N,XS) >= U11(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) ; afterNth(X1,X2) >= n__afterNth(X1,X2) ; U171(tt,N,XS) >= head(afterNth(activate(N),activate(XS))) ; U181(tt,Y) >= activate(Y) ; pair(X1,X2) >= n__pair(X1,X2) ; nil >= n__nil ; U191(tt,XS) >= pair(nil,activate(XS)) ; U202(pair(YS,ZS),X) >= pair(cons(activate(X),YS),ZS) ; U201(tt,N,X,XS) >= U202(splitAt(activate(N),activate(XS)),activate(X)) ; U21(tt,X) >= activate(X) ; U211(tt,XS) >= activate(XS) ; fst(pair(X,Y)) >= U21(and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))),X) ; fst(X) >= n__fst(X) ; U221(tt,N,XS) >= fst(splitAt(activate(N),activate(XS))) ; U31(tt,N) >= activate(N) ; U42(tt,V2) >= U43(isLNat(activate(V2))) ; U41(tt,V1,V2) >= U42(isNatural(activate(V1)),activate(V2)) ; U43(tt) >= tt ; U52(tt,V2) >= U53(isLNat(activate(V2))) ; U51(tt,V1,V2) >= U52(isNatural(activate(V1)),activate(V2)) ; U53(tt) >= tt ; U62(tt) >= tt ; isPLNat(n__pair(V1,V2)) >= U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))),activate(V1), activate(V2)) ; isPLNat(n__splitAt(V1,V2)) >= U151(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1),activate(V2)) ; U61(tt,V1) >= U62(isPLNat(activate(V1))) ; U72(tt) >= tt ; U71(tt,V1) >= U72(isNatural(activate(V1))) ; U82(tt) >= tt ; U81(tt,V1) >= U82(isPLNat(activate(V1))) ; U92(tt) >= tt ; U91(tt,V1) >= U92(isLNat(activate(V1))) ; and(tt,X) >= activate(X) ; and(X1,X2) >= n__and(X1,X2) ; isNaturalKind(n__0) >= tt ; isNaturalKind(n__head(V1)) >= isLNatKind(activate(V1)) ; isNaturalKind(n__s(V1)) >= isNaturalKind(activate(V1)) ; isNaturalKind(n__sel(V1,V2)) >= and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; isNaturalKind(X) >= n__isNaturalKind(X) ; isPLNatKind(n__pair(V1,V2)) >= and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) ; isPLNatKind(n__splitAt(V1,V2)) >= and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; isLNatKind(n__natsFrom(V1)) >= isNaturalKind(activate(V1)) ; isLNatKind(n__nil) >= tt ; isLNatKind(n__afterNth(V1,V2)) >= and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; isLNatKind(n__cons(V1,V2)) >= and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; isLNatKind(n__fst(V1)) >= isPLNatKind(activate(V1)) ; isLNatKind(n__snd(V1)) >= isPLNatKind(activate(V1)) ; isLNatKind(n__tail(V1)) >= isLNatKind(activate(V1)) ; isLNatKind(n__take(V1,V2)) >= and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; isLNatKind(X) >= n__isLNatKind(X) ; natsFrom(N) >= U161(and(isNatural(N),n__isNaturalKind(N)),N) ; natsFrom(X) >= n__natsFrom(X) ; sel(N,XS) >= U171(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) ; sel(X1,X2) >= n__sel(X1,X2) ; 0 >= n__0 ; tail(cons(N,XS)) >= U211(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))),activate(XS)) ; tail(X) >= n__tail(X) ; take(N,XS) >= U221(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))),N,XS) ; take(X1,X2) >= n__take(X1,X2) ; Marked_activate(n__natsFrom(X)) >= Marked_natsFrom(X) ; Marked_activate(n__isNaturalKind(X)) >= Marked_isNaturalKind(X) ; Marked_activate(n__and(X1,X2)) >= Marked_and(X1,X2) ; Marked_activate(n__isLNatKind(X)) >= Marked_isLNatKind(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_and(isNatural(N), n__isNaturalKind(N)) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_and(isNatural(X), n__isNaturalKind(X)) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_and(and(isNatural(N), n__isNaturalKind(N)), n__and(and(isNatural(X), n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_isNatural(N) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_isNatural(X) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_isLNat(activate(XS)) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(and(isNatural(X), n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) ),N,X,activate(XS)) ; Marked_splitAt(0,XS) >= Marked_and(isLNat(XS),n__isLNatKind(XS)) ; Marked_splitAt(0,XS) >= Marked_isLNat(XS) ; Marked_splitAt(0,XS) >= Marked_U191(and(isLNat(XS),n__isLNatKind(XS)),XS) ; Marked_sel(N,XS) >= Marked_and(isNatural(N),n__isNaturalKind(N)) ; Marked_sel(N,XS) >= Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))) ; Marked_sel(N,XS) >= Marked_isNatural(N) ; Marked_sel(N,XS) >= Marked_isLNat(XS) ; Marked_sel(N,XS) >= Marked_U171(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))), N,XS) ; Marked_head(cons(N,XS)) >= Marked_activate(XS) ; Marked_head(cons(N,XS)) >= Marked_and(isNatural(N),n__isNaturalKind(N)) ; Marked_head(cons(N,XS)) >= Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) ; Marked_head(cons(N,XS)) >= Marked_isNatural(N) ; Marked_head(cons(N,XS)) >= Marked_isLNat(activate(XS)) ; Marked_head(cons(N,XS)) >= Marked_U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) ; Marked_take(N,XS) >= Marked_and(isNatural(N),n__isNaturalKind(N)) ; Marked_take(N,XS) >= Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))) ; Marked_take(N,XS) >= Marked_U221(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))), N,XS) ; Marked_take(N,XS) >= Marked_isNatural(N) ; Marked_take(N,XS) >= Marked_isLNat(XS) ; Marked_tail(cons(N,XS)) >= Marked_activate(XS) ; Marked_tail(cons(N,XS)) >= Marked_and(isNatural(N),n__isNaturalKind(N)) ; Marked_tail(cons(N,XS)) >= Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) ; Marked_tail(cons(N,XS)) >= Marked_isNatural(N) ; Marked_tail(cons(N,XS)) >= Marked_isLNat(activate(XS)) ; Marked_tail(cons(N,XS)) >= Marked_U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) ; Marked_snd(pair(X,Y)) >= Marked_and(isLNat(X),n__isLNatKind(X)) ; Marked_snd(pair(X,Y)) >= Marked_and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))) ; Marked_snd(pair(X,Y)) >= Marked_isLNat(Y) ; Marked_snd(pair(X,Y)) >= Marked_isLNat(X) ; Marked_snd(pair(X,Y)) >= Marked_U181(and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))), Y) ; Marked_fst(pair(X,Y)) >= Marked_and(isLNat(X),n__isLNatKind(X)) ; Marked_fst(pair(X,Y)) >= Marked_and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))) ; Marked_fst(pair(X,Y)) >= Marked_isLNat(Y) ; Marked_fst(pair(X,Y)) >= Marked_isLNat(X) ; Marked_fst(pair(X,Y)) >= Marked_U21(and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))), X) ; Marked_afterNth(N,XS) >= Marked_and(isNatural(N),n__isNaturalKind(N)) ; Marked_afterNth(N,XS) >= Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))) ; Marked_afterNth(N,XS) >= Marked_isNatural(N) ; Marked_afterNth(N,XS) >= Marked_isLNat(XS) ; Marked_afterNth(N,XS) >= Marked_U11(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))), N,XS) ; 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_and(isNaturalKind(activate( V1)), n__isLNatKind(activate(V2))) ; Marked_isLNatKind(n__afterNth(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; Marked_isLNatKind(n__cons(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; Marked_isLNatKind(n__take(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_and(tt,X) >= Marked_activate(X) ; 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; Marked_isNaturalKind(n__sel(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_natsFrom(N) >= Marked_and(isNatural(N),n__isNaturalKind(N)) ; Marked_natsFrom(N) >= Marked_isNatural(N) ; Marked_natsFrom(N) >= Marked_U161(and(isNatural(N),n__isNaturalKind(N)),N) ; Marked_U221(tt,N,XS) >= Marked_activate(N) ; Marked_U221(tt,N,XS) >= Marked_activate(XS) ; Marked_U221(tt,N,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U221(tt,N,XS) >= Marked_fst(splitAt(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_U111(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_U121(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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1),activate(V2)) ; 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_U41(and(isNaturalKind(activate( V1)), n__isLNatKind(activate(V2))), 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; Marked_isLNat(n__take(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isLNat(n__take(V1,V2)) >= Marked_U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1),activate(V2)) ; Marked_U211(tt,XS) >= Marked_activate(XS) ; Marked_U201(tt,N,X,XS) >= Marked_activate(N) ; Marked_U201(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U201(tt,N,X,XS) >= Marked_activate(X) ; Marked_U201(tt,N,X,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U201(tt,N,X,XS) >= Marked_U202(splitAt(activate(N),activate(XS)), activate(X)) ; Marked_U191(tt,XS) >= Marked_activate(XS) ; Marked_U181(tt,Y) >= Marked_activate(Y) ; Marked_U171(tt,N,XS) >= Marked_activate(N) ; Marked_U171(tt,N,XS) >= Marked_activate(XS) ; Marked_U171(tt,N,XS) >= Marked_head(afterNth(activate(N),activate(XS))) ; Marked_U171(tt,N,XS) >= Marked_afterNth(activate(N),activate(XS)) ; Marked_U161(tt,N) >= Marked_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_isLNatKind(activate(V1)) ; Marked_isPLNatKind(n__pair(V1,V2)) >= Marked_and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) ; 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_and(isNaturalKind(activate( V1)), n__isLNatKind(activate(V2))) ; Marked_isPLNatKind(n__splitAt(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; 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_and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_isNaturalKind(activate(V1)) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_U151(and(isNaturalKind( activate(V1)), n__isLNatKind(activate(V2))), activate(V1),activate(V2)) ; Marked_U151(tt,V1,V2) >= Marked_activate(V1) ; Marked_U151(tt,V1,V2) >= Marked_activate(V2) ; Marked_U151(tt,V1,V2) >= Marked_isNatural(activate(V1)) ; Marked_U151(tt,V1,V2) >= Marked_U152(isNatural(activate(V1)),activate(V2)) ; Marked_U141(tt,V1,V2) >= Marked_activate(V1) ; Marked_U141(tt,V1,V2) >= Marked_activate(V2) ; Marked_U141(tt,V1,V2) >= Marked_isLNat(activate(V1)) ; Marked_U141(tt,V1,V2) >= Marked_U142(isLNat(activate(V1)),activate(V2)) ; Marked_U131(tt,V1,V2) >= Marked_activate(V1) ; Marked_U131(tt,V1,V2) >= Marked_activate(V2) ; Marked_U131(tt,V1,V2) >= Marked_isNatural(activate(V1)) ; Marked_U131(tt,V1,V2) >= Marked_U132(isNatural(activate(V1)),activate(V2)) ; Marked_U121(tt,V1) >= Marked_activate(V1) ; Marked_U121(tt,V1) >= Marked_isNatural(activate(V1)) ; Marked_U111(tt,V1) >= Marked_activate(V1) ; Marked_U111(tt,V1) >= Marked_isLNat(activate(V1)) ; Marked_U101(tt,V1,V2) >= Marked_activate(V1) ; Marked_U101(tt,V1,V2) >= Marked_activate(V2) ; Marked_U101(tt,V1,V2) >= Marked_isNatural(activate(V1)) ; Marked_U101(tt,V1,V2) >= Marked_U102(isNatural(activate(V1)),activate(V2)) ; Marked_U91(tt,V1) >= Marked_activate(V1) ; Marked_U91(tt,V1) >= Marked_isLNat(activate(V1)) ; Marked_U81(tt,V1) >= Marked_activate(V1) ; Marked_U81(tt,V1) >= Marked_isPLNat(activate(V1)) ; Marked_U71(tt,V1) >= Marked_activate(V1) ; Marked_U71(tt,V1) >= Marked_isNatural(activate(V1)) ; Marked_U61(tt,V1) >= Marked_activate(V1) ; Marked_U61(tt,V1) >= Marked_isPLNat(activate(V1)) ; Marked_U51(tt,V1,V2) >= Marked_activate(V1) ; Marked_U51(tt,V1,V2) >= Marked_activate(V2) ; Marked_U51(tt,V1,V2) >= Marked_isNatural(activate(V1)) ; Marked_U51(tt,V1,V2) >= Marked_U52(isNatural(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_isNatural(activate(V1)) ; Marked_U41(tt,V1,V2) >= Marked_U42(isNatural(activate(V1)),activate(V2)) ; Marked_U31(tt,N) >= Marked_activate(N) ; Marked_U21(tt,X) >= Marked_activate(X) ; Marked_U11(tt,N,XS) >= Marked_activate(N) ; Marked_U11(tt,N,XS) >= Marked_activate(XS) ; Marked_U11(tt,N,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U11(tt,N,XS) >= Marked_snd(splitAt(activate(N),activate(XS))) ; Marked_U52(tt,V2) >= Marked_activate(V2) ; Marked_U52(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U42(tt,V2) >= Marked_activate(V2) ; Marked_U42(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U202(pair(YS,ZS),X) >= Marked_activate(X) ; Marked_U152(tt,V2) >= Marked_activate(V2) ; Marked_U152(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U142(tt,V2) >= Marked_activate(V2) ; Marked_U142(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U132(tt,V2) >= Marked_activate(V2) ; Marked_U132(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U102(tt,V2) >= Marked_activate(V2) ; Marked_U102(tt,V2) >= Marked_isLNat(activate(V2)) ; } + Disjunctions:{ { Marked_activate(n__natsFrom(X)) > Marked_natsFrom(X) ; } { Marked_activate(n__isNaturalKind(X)) > Marked_isNaturalKind(X) ; } { Marked_activate(n__and(X1,X2)) > Marked_and(X1,X2) ; } { Marked_activate(n__isLNatKind(X)) > Marked_isLNatKind(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_and(isNatural(N), n__isNaturalKind(N)) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_and(isNatural(X), n__isNaturalKind(X)) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_and(and(isNatural(N), n__isNaturalKind(N)), n__and(and(isNatural(X), n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_isNatural(N) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_isNatural(X) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_isLNat(activate(XS)) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_U201(and(and(isNatural(N), n__isNaturalKind(N)), n__and(and(isNatural(X), n__isNaturalKind(X)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS))))) ,N,X,activate(XS)) ; } { Marked_splitAt(0,XS) > Marked_and(isLNat(XS),n__isLNatKind(XS)) ; } { Marked_splitAt(0,XS) > Marked_isLNat(XS) ; } { Marked_splitAt(0,XS) > Marked_U191(and(isLNat(XS),n__isLNatKind(XS)),XS) ; } { Marked_sel(N,XS) > Marked_and(isNatural(N),n__isNaturalKind(N)) ; } { Marked_sel(N,XS) > Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))) ; } { Marked_sel(N,XS) > Marked_isNatural(N) ; } { Marked_sel(N,XS) > Marked_isLNat(XS) ; } { Marked_sel(N,XS) > Marked_U171(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))), N,XS) ; } { Marked_head(cons(N,XS)) > Marked_activate(XS) ; } { Marked_head(cons(N,XS)) > Marked_and(isNatural(N),n__isNaturalKind(N)) ; } { Marked_head(cons(N,XS)) > Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) ; } { Marked_head(cons(N,XS)) > Marked_isNatural(N) ; } { Marked_head(cons(N,XS)) > Marked_isLNat(activate(XS)) ; } { Marked_head(cons(N,XS)) > Marked_U31(and(and(isNatural(N), n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))), N) ; } { Marked_take(N,XS) > Marked_and(isNatural(N),n__isNaturalKind(N)) ; } { Marked_take(N,XS) > Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))) ; } { Marked_take(N,XS) > Marked_U221(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))), N,XS) ; } { Marked_take(N,XS) > Marked_isNatural(N) ; } { Marked_take(N,XS) > Marked_isLNat(XS) ; } { Marked_tail(cons(N,XS)) > Marked_activate(XS) ; } { Marked_tail(cons(N,XS)) > Marked_and(isNatural(N),n__isNaturalKind(N)) ; } { Marked_tail(cons(N,XS)) > Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))) ; } { Marked_tail(cons(N,XS)) > Marked_isNatural(N) ; } { Marked_tail(cons(N,XS)) > Marked_isLNat(activate(XS)) ; } { Marked_tail(cons(N,XS)) > Marked_U211(and(and(isNatural(N), n__isNaturalKind(N)), n__and(isLNat(activate(XS)), n__isLNatKind(activate(XS)))), activate(XS)) ; } { Marked_snd(pair(X,Y)) > Marked_and(isLNat(X),n__isLNatKind(X)) ; } { Marked_snd(pair(X,Y)) > Marked_and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))) ; } { Marked_snd(pair(X,Y)) > Marked_isLNat(Y) ; } { Marked_snd(pair(X,Y)) > Marked_isLNat(X) ; } { Marked_snd(pair(X,Y)) > Marked_U181(and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))), Y) ; } { Marked_fst(pair(X,Y)) > Marked_and(isLNat(X),n__isLNatKind(X)) ; } { Marked_fst(pair(X,Y)) > Marked_and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))) ; } { Marked_fst(pair(X,Y)) > Marked_isLNat(Y) ; } { Marked_fst(pair(X,Y)) > Marked_isLNat(X) ; } { Marked_fst(pair(X,Y)) > Marked_U21(and(and(isLNat(X),n__isLNatKind(X)), n__and(isLNat(Y),n__isLNatKind(Y))), X) ; } { Marked_afterNth(N,XS) > Marked_and(isNatural(N),n__isNaturalKind(N)) ; } { Marked_afterNth(N,XS) > Marked_and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))) ; } { Marked_afterNth(N,XS) > Marked_isNatural(N) ; } { Marked_afterNth(N,XS) > Marked_isLNat(XS) ; } { Marked_afterNth(N,XS) > Marked_U11(and(and(isNatural(N),n__isNaturalKind(N)), n__and(isLNat(XS),n__isLNatKind(XS))), N,XS) ; } { 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isLNatKind(n__afterNth(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isLNatKind(n__cons(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isLNatKind(n__take(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_and(tt,X) > Marked_activate(X) ; } { 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isNaturalKind(n__sel(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_natsFrom(N) > Marked_and(isNatural(N),n__isNaturalKind(N)) ; } { Marked_natsFrom(N) > Marked_isNatural(N) ; } { Marked_natsFrom(N) > Marked_U161(and(isNatural(N),n__isNaturalKind(N)),N) ; } { Marked_U221(tt,N,XS) > Marked_activate(N) ; } { Marked_U221(tt,N,XS) > Marked_activate(XS) ; } { Marked_U221(tt,N,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U221(tt,N,XS) > Marked_fst(splitAt(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_U111(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_U121(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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_U131(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1),activate(V2)) ; } { 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_U41(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_U51(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_U101(and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))), activate(V1),activate(V2)) ; } { Marked_U211(tt,XS) > Marked_activate(XS) ; } { Marked_U201(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U201(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U201(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U201(tt,N,X,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U201(tt,N,X,XS) > Marked_U202(splitAt(activate(N),activate(XS)), activate(X)) ; } { Marked_U191(tt,XS) > Marked_activate(XS) ; } { Marked_U181(tt,Y) > Marked_activate(Y) ; } { Marked_U171(tt,N,XS) > Marked_activate(N) ; } { Marked_U171(tt,N,XS) > Marked_activate(XS) ; } { Marked_U171(tt,N,XS) > Marked_head(afterNth(activate(N),activate(XS))) ; } { Marked_U171(tt,N,XS) > Marked_afterNth(activate(N),activate(XS)) ; } { Marked_U161(tt,N) > Marked_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_isLNatKind(activate(V1)) ; } { Marked_isPLNatKind(n__pair(V1,V2)) > Marked_and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isPLNatKind(n__splitAt(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { 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_and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_U141(and(isLNatKind(activate(V1)), n__isLNatKind(activate(V2))), 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_and(isNaturalKind(activate(V1)), n__isLNatKind(activate(V2))) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_isNaturalKind(activate(V1)) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_U151(and(isNaturalKind(activate( V1)), n__isLNatKind(activate(V2))), activate(V1),activate(V2)) ; } { Marked_U151(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U151(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U151(tt,V1,V2) > Marked_isNatural(activate(V1)) ; } { Marked_U151(tt,V1,V2) > Marked_U152(isNatural(activate(V1)),activate(V2)) ; } { Marked_U141(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U141(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U141(tt,V1,V2) > Marked_isLNat(activate(V1)) ; } { Marked_U141(tt,V1,V2) > Marked_U142(isLNat(activate(V1)),activate(V2)) ; } { Marked_U131(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U131(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U131(tt,V1,V2) > Marked_isNatural(activate(V1)) ; } { Marked_U131(tt,V1,V2) > Marked_U132(isNatural(activate(V1)),activate(V2)) ; } { Marked_U121(tt,V1) > Marked_activate(V1) ; } { Marked_U121(tt,V1) > Marked_isNatural(activate(V1)) ; } { Marked_U111(tt,V1) > Marked_activate(V1) ; } { Marked_U111(tt,V1) > Marked_isLNat(activate(V1)) ; } { Marked_U101(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U101(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U101(tt,V1,V2) > Marked_isNatural(activate(V1)) ; } { Marked_U101(tt,V1,V2) > Marked_U102(isNatural(activate(V1)),activate(V2)) ; } { Marked_U91(tt,V1) > Marked_activate(V1) ; } { Marked_U91(tt,V1) > Marked_isLNat(activate(V1)) ; } { Marked_U81(tt,V1) > Marked_activate(V1) ; } { Marked_U81(tt,V1) > Marked_isPLNat(activate(V1)) ; } { Marked_U71(tt,V1) > Marked_activate(V1) ; } { Marked_U71(tt,V1) > Marked_isNatural(activate(V1)) ; } { Marked_U61(tt,V1) > Marked_activate(V1) ; } { Marked_U61(tt,V1) > Marked_isPLNat(activate(V1)) ; } { Marked_U51(tt,V1,V2) > Marked_activate(V1) ; } { Marked_U51(tt,V1,V2) > Marked_activate(V2) ; } { Marked_U51(tt,V1,V2) > Marked_isNatural(activate(V1)) ; } { Marked_U51(tt,V1,V2) > Marked_U52(isNatural(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_isNatural(activate(V1)) ; } { Marked_U41(tt,V1,V2) > Marked_U42(isNatural(activate(V1)),activate(V2)) ; } { Marked_U31(tt,N) > Marked_activate(N) ; } { Marked_U21(tt,X) > Marked_activate(X) ; } { Marked_U11(tt,N,XS) > Marked_activate(N) ; } { Marked_U11(tt,N,XS) > Marked_activate(XS) ; } { Marked_U11(tt,N,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U11(tt,N,XS) > Marked_snd(splitAt(activate(N),activate(XS))) ; } { Marked_U52(tt,V2) > Marked_activate(V2) ; } { Marked_U52(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U42(tt,V2) > Marked_activate(V2) ; } { Marked_U42(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U202(pair(YS,ZS),X) > Marked_activate(X) ; } { Marked_U152(tt,V2) > Marked_activate(V2) ; } { Marked_U152(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U142(tt,V2) > Marked_activate(V2) ; } { Marked_U142(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U132(tt,V2) > Marked_activate(V2) ; } { Marked_U132(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U102(tt,V2) > Marked_activate(V2) ; } { Marked_U102(tt,V2) > Marked_isLNat(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 solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found 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 === 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 === 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 111.377697 seconds (real time) Cime Exit Status: 0