- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] U101(tt,V2) -> U102(isLNat(activate(V2))) [2] U102(tt) -> tt [3] U11(tt,N,XS) -> U12(isLNat(activate(XS)),activate(N),activate(XS)) [4] U111(tt) -> tt [5] U12(tt,N,XS) -> snd(splitAt(activate(N),activate(XS))) [6] U121(tt) -> tt [7] U131(tt,V2) -> U132(isLNat(activate(V2))) [8] U132(tt) -> tt [9] U141(tt,V2) -> U142(isLNat(activate(V2))) [10] U142(tt) -> tt [11] U151(tt,V2) -> U152(isLNat(activate(V2))) [12] U152(tt) -> tt [13] U161(tt,N) -> cons(activate(N),n__natsFrom(n__s(activate(N)))) [14] U171(tt,N,XS) -> U172(isLNat(activate(XS)),activate(N),activate(XS)) [15] U172(tt,N,XS) -> head(afterNth(activate(N),activate(XS))) [16] U181(tt,Y) -> U182(isLNat(activate(Y)),activate(Y)) [17] U182(tt,Y) -> activate(Y) [18] U191(tt,XS) -> pair(nil,activate(XS)) [19] U201(tt,N,X,XS) -> U202(isNatural(activate(X)),activate(N),activate(X),activate(XS)) [20] U202(tt,N,X,XS) -> U203(isLNat(activate(XS)),activate(N),activate(X),activate(XS)) [21] U203(tt,N,X,XS) -> U204(splitAt(activate(N),activate(XS)),activate(X)) [22] U204(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) [23] U21(tt,X,Y) -> U22(isLNat(activate(Y)),activate(X)) [24] U211(tt,XS) -> U212(isLNat(activate(XS)),activate(XS)) [25] U212(tt,XS) -> activate(XS) [26] U22(tt,X) -> activate(X) [27] U221(tt,N,XS) -> U222(isLNat(activate(XS)),activate(N),activate(XS)) [28] U222(tt,N,XS) -> fst(splitAt(activate(N),activate(XS))) [29] U31(tt,N,XS) -> U32(isLNat(activate(XS)),activate(N)) [30] U32(tt,N) -> activate(N) [31] U41(tt,V2) -> U42(isLNat(activate(V2))) [32] U42(tt) -> tt [33] U51(tt,V2) -> U52(isLNat(activate(V2))) [34] U52(tt) -> tt [35] U61(tt) -> tt [36] U71(tt) -> tt [37] U81(tt) -> tt [38] U91(tt) -> tt [39] afterNth(N,XS) -> U11(isNatural(N),N,XS) [40] fst(pair(X,Y)) -> U21(isLNat(X),X,Y) [41] head(cons(N,XS)) -> U31(isNatural(N),N,activate(XS)) [42] isLNat(n__nil) -> tt [43] isLNat(n__afterNth(V1,V2)) -> U41(isNatural(activate(V1)),activate(V2)) [44] isLNat(n__cons(V1,V2)) -> U51(isNatural(activate(V1)),activate(V2)) [45] isLNat(n__fst(V1)) -> U61(isPLNat(activate(V1))) [46] isLNat(n__natsFrom(V1)) -> U71(isNatural(activate(V1))) [47] isLNat(n__snd(V1)) -> U81(isPLNat(activate(V1))) [48] isLNat(n__tail(V1)) -> U91(isLNat(activate(V1))) [49] isLNat(n__take(V1,V2)) -> U101(isNatural(activate(V1)),activate(V2)) [50] isNatural(n__0) -> tt [51] isNatural(n__head(V1)) -> U111(isLNat(activate(V1))) [52] isNatural(n__s(V1)) -> U121(isNatural(activate(V1))) [53] isNatural(n__sel(V1,V2)) -> U131(isNatural(activate(V1)),activate(V2)) [54] isPLNat(n__pair(V1,V2)) -> U141(isLNat(activate(V1)),activate(V2)) [55] isPLNat(n__splitAt(V1,V2)) -> U151(isNatural(activate(V1)),activate(V2)) [56] natsFrom(N) -> U161(isNatural(N),N) [57] sel(N,XS) -> U171(isNatural(N),N,XS) [58] snd(pair(X,Y)) -> U181(isLNat(X),Y) [59] splitAt(0,XS) -> U191(isLNat(XS),XS) [60] splitAt(s(N),cons(X,XS)) -> U201(isNatural(N),N,X,activate(XS)) [61] tail(cons(N,XS)) -> U211(isNatural(N),activate(XS)) [62] take(N,XS) -> U221(isNatural(N),N,XS) [63] natsFrom(X) -> n__natsFrom(X) [64] s(X) -> n__s(X) [65] nil -> n__nil [66] afterNth(X1,X2) -> n__afterNth(X1,X2) [67] cons(X1,X2) -> n__cons(X1,X2) [68] fst(X) -> n__fst(X) [69] snd(X) -> n__snd(X) [70] tail(X) -> n__tail(X) [71] take(X1,X2) -> n__take(X1,X2) [72] 0 -> n__0 [73] head(X) -> n__head(X) [74] sel(X1,X2) -> n__sel(X1,X2) [75] pair(X1,X2) -> n__pair(X1,X2) [76] splitAt(X1,X2) -> n__splitAt(X1,X2) [77] activate(n__natsFrom(X)) -> natsFrom(activate(X)) [78] activate(n__s(X)) -> s(activate(X)) [79] activate(n__nil) -> nil [80] activate(n__afterNth(X1,X2)) -> afterNth(activate(X1),activate(X2)) [81] activate(n__cons(X1,X2)) -> cons(activate(X1),X2) [82] activate(n__fst(X)) -> fst(activate(X)) [83] activate(n__snd(X)) -> snd(activate(X)) [84] activate(n__tail(X)) -> tail(activate(X)) [85] activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) [86] activate(n__0) -> 0 [87] activate(n__head(X)) -> head(activate(X)) [88] activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) [89] activate(n__pair(X1,X2)) -> pair(activate(X1),activate(X2)) [90] activate(n__splitAt(X1,X2)) -> splitAt(activate(X1),activate(X2)) [91] 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) >= tt ; isLNat(n__natsFrom(V1)) >= U71(isNatural(activate(V1))) ; isLNat(n__nil) >= tt ; isLNat(n__afterNth(V1,V2)) >= U41(isNatural(activate(V1)),activate(V2)) ; isLNat(n__cons(V1,V2)) >= U51(isNatural(activate(V1)),activate(V2)) ; isLNat(n__fst(V1)) >= U61(isPLNat(activate(V1))) ; isLNat(n__snd(V1)) >= U81(isPLNat(activate(V1))) ; isLNat(n__tail(V1)) >= U91(isLNat(activate(V1))) ; isLNat(n__take(V1,V2)) >= U101(isNatural(activate(V1)),activate(V2)) ; activate(n__natsFrom(X)) >= natsFrom(activate(X)) ; activate(n__s(X)) >= s(activate(X)) ; activate(n__nil) >= nil ; activate(n__afterNth(X1,X2)) >= afterNth(activate(X1),activate(X2)) ; activate(n__cons(X1,X2)) >= cons(activate(X1),X2) ; activate(n__fst(X)) >= fst(activate(X)) ; activate(n__snd(X)) >= snd(activate(X)) ; activate(n__tail(X)) >= tail(activate(X)) ; activate(n__take(X1,X2)) >= take(activate(X1),activate(X2)) ; activate(n__0) >= 0 ; activate(n__head(X)) >= head(activate(X)) ; activate(n__sel(X1,X2)) >= sel(activate(X1),activate(X2)) ; activate(n__pair(X1,X2)) >= pair(activate(X1),activate(X2)) ; activate(n__splitAt(X1,X2)) >= splitAt(activate(X1),activate(X2)) ; activate(X) >= X ; U101(tt,V2) >= U102(isLNat(activate(V2))) ; U12(tt,N,XS) >= snd(splitAt(activate(N),activate(XS))) ; U11(tt,N,XS) >= U12(isLNat(activate(XS)),activate(N),activate(XS)) ; U111(tt) >= tt ; snd(pair(X,Y)) >= U181(isLNat(X),Y) ; snd(X) >= n__snd(X) ; splitAt(0,XS) >= U191(isLNat(XS),XS) ; splitAt(s(N),cons(X,XS)) >= U201(isNatural(N),N,X,activate(XS)) ; splitAt(X1,X2) >= n__splitAt(X1,X2) ; U121(tt) >= tt ; U132(tt) >= tt ; U131(tt,V2) >= U132(isLNat(activate(V2))) ; U142(tt) >= tt ; U141(tt,V2) >= U142(isLNat(activate(V2))) ; U152(tt) >= tt ; U151(tt,V2) >= U152(isLNat(activate(V2))) ; cons(X1,X2) >= n__cons(X1,X2) ; U161(tt,N) >= cons(activate(N),n__natsFrom(n__s(activate(N)))) ; U172(tt,N,XS) >= head(afterNth(activate(N),activate(XS))) ; U171(tt,N,XS) >= U172(isLNat(activate(XS)),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) ; U182(tt,Y) >= activate(Y) ; U181(tt,Y) >= U182(isLNat(activate(Y)),activate(Y)) ; pair(X1,X2) >= n__pair(X1,X2) ; nil >= n__nil ; U191(tt,XS) >= pair(nil,activate(XS)) ; U202(tt,N,X,XS) >= U203(isLNat(activate(XS)),activate(N),activate(X), activate(XS)) ; isNatural(n__s(V1)) >= U121(isNatural(activate(V1))) ; isNatural(n__0) >= tt ; isNatural(n__head(V1)) >= U111(isLNat(activate(V1))) ; isNatural(n__sel(V1,V2)) >= U131(isNatural(activate(V1)),activate(V2)) ; U201(tt,N,X,XS) >= U202(isNatural(activate(X)),activate(N),activate(X), activate(XS)) ; U203(tt,N,X,XS) >= U204(splitAt(activate(N),activate(XS)),activate(X)) ; U204(pair(YS,ZS),X) >= pair(cons(activate(X),YS),ZS) ; U22(tt,X) >= activate(X) ; U21(tt,X,Y) >= U22(isLNat(activate(Y)),activate(X)) ; U212(tt,XS) >= activate(XS) ; U211(tt,XS) >= U212(isLNat(activate(XS)),activate(XS)) ; U222(tt,N,XS) >= fst(splitAt(activate(N),activate(XS))) ; U221(tt,N,XS) >= U222(isLNat(activate(XS)),activate(N),activate(XS)) ; fst(pair(X,Y)) >= U21(isLNat(X),X,Y) ; fst(X) >= n__fst(X) ; U32(tt,N) >= activate(N) ; U31(tt,N,XS) >= U32(isLNat(activate(XS)),activate(N)) ; U42(tt) >= tt ; U41(tt,V2) >= U42(isLNat(activate(V2))) ; U52(tt) >= tt ; U51(tt,V2) >= U52(isLNat(activate(V2))) ; U61(tt) >= tt ; U71(tt) >= tt ; U81(tt) >= tt ; U91(tt) >= tt ; isPLNat(n__pair(V1,V2)) >= U141(isLNat(activate(V1)),activate(V2)) ; isPLNat(n__splitAt(V1,V2)) >= U151(isNatural(activate(V1)),activate(V2)) ; natsFrom(N) >= U161(isNatural(N),N) ; natsFrom(X) >= n__natsFrom(X) ; sel(N,XS) >= U171(isNatural(N),N,XS) ; sel(X1,X2) >= n__sel(X1,X2) ; 0 >= n__0 ; s(X) >= n__s(X) ; tail(cons(N,XS)) >= U211(isNatural(N),activate(XS)) ; tail(X) >= n__tail(X) ; take(N,XS) >= U221(isNatural(N),N,XS) ; take(X1,X2) >= n__take(X1,X2) ; Marked_activate(n__natsFrom(X)) >= Marked_activate(X) ; Marked_activate(n__natsFrom(X)) >= Marked_natsFrom(activate(X)) ; Marked_activate(n__s(X)) >= Marked_activate(X) ; Marked_activate(n__afterNth(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__afterNth(X1,X2)) >= Marked_activate(X2) ; Marked_activate(n__afterNth(X1,X2)) >= Marked_afterNth(activate(X1), activate(X2)) ; Marked_activate(n__cons(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__fst(X)) >= Marked_activate(X) ; Marked_activate(n__fst(X)) >= Marked_fst(activate(X)) ; Marked_activate(n__snd(X)) >= Marked_activate(X) ; Marked_activate(n__snd(X)) >= Marked_snd(activate(X)) ; Marked_activate(n__tail(X)) >= Marked_activate(X) ; Marked_activate(n__tail(X)) >= Marked_tail(activate(X)) ; Marked_activate(n__take(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__take(X1,X2)) >= Marked_activate(X2) ; Marked_activate(n__take(X1,X2)) >= Marked_take(activate(X1),activate(X2)) ; Marked_activate(n__head(X)) >= Marked_activate(X) ; Marked_activate(n__head(X)) >= Marked_head(activate(X)) ; Marked_activate(n__sel(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__sel(X1,X2)) >= Marked_activate(X2) ; Marked_activate(n__sel(X1,X2)) >= Marked_sel(activate(X1),activate(X2)) ; Marked_activate(n__pair(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__pair(X1,X2)) >= Marked_activate(X2) ; Marked_activate(n__splitAt(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__splitAt(X1,X2)) >= Marked_activate(X2) ; Marked_activate(n__splitAt(X1,X2)) >= Marked_splitAt(activate(X1), activate(X2)) ; Marked_splitAt(0,XS) >= Marked_U191(isLNat(XS),XS) ; Marked_splitAt(0,XS) >= Marked_isLNat(XS) ; 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_U201(isNatural(N),N,X,activate(XS)) ; Marked_sel(N,XS) >= Marked_isNatural(N) ; Marked_sel(N,XS) >= Marked_U171(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_U221(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_U211(isNatural(N),activate(XS)) ; Marked_snd(pair(X,Y)) >= Marked_isLNat(X) ; Marked_snd(pair(X,Y)) >= Marked_U181(isLNat(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_U161(isNatural(N),N) ; Marked_U221(tt,N,XS) >= Marked_activate(N) ; Marked_U221(tt,N,XS) >= Marked_activate(XS) ; Marked_U221(tt,N,XS) >= Marked_isLNat(activate(XS)) ; Marked_U221(tt,N,XS) >= Marked_U222(isLNat(activate(XS)),activate(N), activate(XS)) ; Marked_isNatural(n__s(V1)) >= Marked_activate(V1) ; Marked_isNatural(n__s(V1)) >= Marked_isNatural(activate(V1)) ; Marked_isNatural(n__head(V1)) >= Marked_activate(V1) ; Marked_isNatural(n__head(V1)) >= Marked_isLNat(activate(V1)) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_activate(V2) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_activate(V1) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_isNatural(activate(V1)) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_U131(isNatural(activate(V1)), activate(V2)) ; Marked_U211(tt,XS) >= Marked_activate(XS) ; Marked_U211(tt,XS) >= Marked_isLNat(activate(XS)) ; Marked_U211(tt,XS) >= Marked_U212(isLNat(activate(XS)),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_isNatural(activate(X)) ; Marked_U201(tt,N,X,XS) >= Marked_U202(isNatural(activate(X)),activate(N), activate(X),activate(XS)) ; Marked_U191(tt,XS) >= Marked_activate(XS) ; Marked_isLNat(n__natsFrom(V1)) >= Marked_activate(V1) ; Marked_isLNat(n__natsFrom(V1)) >= Marked_isNatural(activate(V1)) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_activate(V2) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_activate(V1) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_isNatural(activate(V1)) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_U41(isNatural(activate(V1)), activate(V2)) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_activate(V2) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_activate(V1) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_isNatural(activate(V1)) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_U51(isNatural(activate(V1)), activate(V2)) ; Marked_isLNat(n__fst(V1)) >= Marked_activate(V1) ; Marked_isLNat(n__fst(V1)) >= Marked_isPLNat(activate(V1)) ; Marked_isLNat(n__snd(V1)) >= Marked_activate(V1) ; Marked_isLNat(n__snd(V1)) >= Marked_isPLNat(activate(V1)) ; Marked_isLNat(n__tail(V1)) >= Marked_activate(V1) ; Marked_isLNat(n__tail(V1)) >= Marked_isLNat(activate(V1)) ; Marked_isLNat(n__take(V1,V2)) >= Marked_activate(V2) ; Marked_isLNat(n__take(V1,V2)) >= Marked_activate(V1) ; Marked_isLNat(n__take(V1,V2)) >= Marked_isNatural(activate(V1)) ; Marked_isLNat(n__take(V1,V2)) >= Marked_U101(isNatural(activate(V1)), activate(V2)) ; Marked_U181(tt,Y) >= Marked_activate(Y) ; Marked_U181(tt,Y) >= Marked_isLNat(activate(Y)) ; Marked_U181(tt,Y) >= Marked_U182(isLNat(activate(Y)),activate(Y)) ; Marked_U171(tt,N,XS) >= Marked_activate(N) ; Marked_U171(tt,N,XS) >= Marked_activate(XS) ; Marked_U171(tt,N,XS) >= Marked_isLNat(activate(XS)) ; Marked_U171(tt,N,XS) >= Marked_U172(isLNat(activate(XS)),activate(N), activate(XS)) ; Marked_U161(tt,N) >= Marked_activate(N) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_activate(V2) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_activate(V1) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_isLNat(activate(V1)) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_U141(isLNat(activate(V1)), activate(V2)) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_activate(V2) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_activate(V1) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_isNatural(activate(V1)) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_U151(isNatural(activate(V1)), activate(V2)) ; Marked_U151(tt,V2) >= Marked_activate(V2) ; Marked_U151(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U141(tt,V2) >= Marked_activate(V2) ; Marked_U141(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U131(tt,V2) >= Marked_activate(V2) ; Marked_U131(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U101(tt,V2) >= Marked_activate(V2) ; Marked_U101(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U51(tt,V2) >= Marked_activate(V2) ; Marked_U51(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U41(tt,V2) >= Marked_activate(V2) ; Marked_U41(tt,V2) >= Marked_isLNat(activate(V2)) ; Marked_U31(tt,N,XS) >= Marked_activate(N) ; Marked_U31(tt,N,XS) >= Marked_activate(XS) ; Marked_U31(tt,N,XS) >= Marked_isLNat(activate(XS)) ; Marked_U31(tt,N,XS) >= Marked_U32(isLNat(activate(XS)),activate(N)) ; Marked_U21(tt,X,Y) >= Marked_activate(Y) ; Marked_U21(tt,X,Y) >= Marked_activate(X) ; Marked_U21(tt,X,Y) >= Marked_isLNat(activate(Y)) ; Marked_U21(tt,X,Y) >= Marked_U22(isLNat(activate(Y)),activate(X)) ; Marked_U11(tt,N,XS) >= Marked_activate(N) ; Marked_U11(tt,N,XS) >= Marked_activate(XS) ; Marked_U11(tt,N,XS) >= Marked_isLNat(activate(XS)) ; Marked_U11(tt,N,XS) >= Marked_U12(isLNat(activate(XS)),activate(N), activate(XS)) ; Marked_U32(tt,N) >= Marked_activate(N) ; Marked_U222(tt,N,XS) >= Marked_activate(N) ; Marked_U222(tt,N,XS) >= Marked_activate(XS) ; Marked_U222(tt,N,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U222(tt,N,XS) >= Marked_fst(splitAt(activate(N),activate(XS))) ; Marked_U22(tt,X) >= Marked_activate(X) ; Marked_U212(tt,XS) >= Marked_activate(XS) ; Marked_U204(pair(YS,ZS),X) >= Marked_activate(X) ; Marked_U203(tt,N,X,XS) >= Marked_activate(N) ; Marked_U203(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U203(tt,N,X,XS) >= Marked_activate(X) ; Marked_U203(tt,N,X,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U203(tt,N,X,XS) >= Marked_U204(splitAt(activate(N),activate(XS)), activate(X)) ; Marked_U202(tt,N,X,XS) >= Marked_activate(N) ; Marked_U202(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U202(tt,N,X,XS) >= Marked_activate(X) ; Marked_U202(tt,N,X,XS) >= Marked_isLNat(activate(XS)) ; Marked_U202(tt,N,X,XS) >= Marked_U203(isLNat(activate(XS)),activate(N), activate(X),activate(XS)) ; Marked_U182(tt,Y) >= Marked_activate(Y) ; Marked_U172(tt,N,XS) >= Marked_activate(N) ; Marked_U172(tt,N,XS) >= Marked_activate(XS) ; Marked_U172(tt,N,XS) >= Marked_head(afterNth(activate(N),activate(XS))) ; Marked_U172(tt,N,XS) >= Marked_afterNth(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_splitAt(activate(N),activate(XS)) ; Marked_U12(tt,N,XS) >= Marked_snd(splitAt(activate(N),activate(XS))) ; } + Disjunctions:{ { Marked_activate(n__natsFrom(X)) > Marked_activate(X) ; } { Marked_activate(n__natsFrom(X)) > Marked_natsFrom(activate(X)) ; } { Marked_activate(n__s(X)) > Marked_activate(X) ; } { Marked_activate(n__afterNth(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__afterNth(X1,X2)) > Marked_activate(X2) ; } { Marked_activate(n__afterNth(X1,X2)) > Marked_afterNth(activate(X1), activate(X2)) ; } { Marked_activate(n__cons(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__fst(X)) > Marked_activate(X) ; } { Marked_activate(n__fst(X)) > Marked_fst(activate(X)) ; } { Marked_activate(n__snd(X)) > Marked_activate(X) ; } { Marked_activate(n__snd(X)) > Marked_snd(activate(X)) ; } { Marked_activate(n__tail(X)) > Marked_activate(X) ; } { Marked_activate(n__tail(X)) > Marked_tail(activate(X)) ; } { Marked_activate(n__take(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__take(X1,X2)) > Marked_activate(X2) ; } { Marked_activate(n__take(X1,X2)) > Marked_take(activate(X1),activate(X2)) ; } { Marked_activate(n__head(X)) > Marked_activate(X) ; } { Marked_activate(n__head(X)) > Marked_head(activate(X)) ; } { Marked_activate(n__sel(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__sel(X1,X2)) > Marked_activate(X2) ; } { Marked_activate(n__sel(X1,X2)) > Marked_sel(activate(X1),activate(X2)) ; } { Marked_activate(n__pair(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__pair(X1,X2)) > Marked_activate(X2) ; } { Marked_activate(n__splitAt(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__splitAt(X1,X2)) > Marked_activate(X2) ; } { Marked_activate(n__splitAt(X1,X2)) > Marked_splitAt(activate(X1), activate(X2)) ; } { Marked_splitAt(0,XS) > Marked_U191(isLNat(XS),XS) ; } { Marked_splitAt(0,XS) > Marked_isLNat(XS) ; } { 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_U201(isNatural(N),N,X,activate(XS)) ; } { Marked_sel(N,XS) > Marked_isNatural(N) ; } { Marked_sel(N,XS) > Marked_U171(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_U221(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_U211(isNatural(N),activate(XS)) ; } { Marked_snd(pair(X,Y)) > Marked_isLNat(X) ; } { Marked_snd(pair(X,Y)) > Marked_U181(isLNat(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_U161(isNatural(N),N) ; } { Marked_U221(tt,N,XS) > Marked_activate(N) ; } { Marked_U221(tt,N,XS) > Marked_activate(XS) ; } { Marked_U221(tt,N,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U221(tt,N,XS) > Marked_U222(isLNat(activate(XS)),activate(N), activate(XS)) ; } { Marked_isNatural(n__s(V1)) > Marked_activate(V1) ; } { Marked_isNatural(n__s(V1)) > Marked_isNatural(activate(V1)) ; } { Marked_isNatural(n__head(V1)) > Marked_activate(V1) ; } { Marked_isNatural(n__head(V1)) > Marked_isLNat(activate(V1)) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_activate(V1) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_isNatural(activate(V1)) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_U131(isNatural(activate(V1)), activate(V2)) ; } { Marked_U211(tt,XS) > Marked_activate(XS) ; } { Marked_U211(tt,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U211(tt,XS) > Marked_U212(isLNat(activate(XS)),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_isNatural(activate(X)) ; } { Marked_U201(tt,N,X,XS) > Marked_U202(isNatural(activate(X)),activate(N), activate(X),activate(XS)) ; } { Marked_U191(tt,XS) > Marked_activate(XS) ; } { Marked_isLNat(n__natsFrom(V1)) > Marked_activate(V1) ; } { Marked_isLNat(n__natsFrom(V1)) > Marked_isNatural(activate(V1)) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_activate(V1) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_isNatural(activate(V1)) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_U41(isNatural(activate(V1)), activate(V2)) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_activate(V1) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_isNatural(activate(V1)) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_U51(isNatural(activate(V1)), activate(V2)) ; } { Marked_isLNat(n__fst(V1)) > Marked_activate(V1) ; } { Marked_isLNat(n__fst(V1)) > Marked_isPLNat(activate(V1)) ; } { Marked_isLNat(n__snd(V1)) > Marked_activate(V1) ; } { Marked_isLNat(n__snd(V1)) > Marked_isPLNat(activate(V1)) ; } { Marked_isLNat(n__tail(V1)) > Marked_activate(V1) ; } { Marked_isLNat(n__tail(V1)) > Marked_isLNat(activate(V1)) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_activate(V1) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_isNatural(activate(V1)) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_U101(isNatural(activate(V1)), activate(V2)) ; } { Marked_U181(tt,Y) > Marked_activate(Y) ; } { Marked_U181(tt,Y) > Marked_isLNat(activate(Y)) ; } { Marked_U181(tt,Y) > Marked_U182(isLNat(activate(Y)),activate(Y)) ; } { Marked_U171(tt,N,XS) > Marked_activate(N) ; } { Marked_U171(tt,N,XS) > Marked_activate(XS) ; } { Marked_U171(tt,N,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U171(tt,N,XS) > Marked_U172(isLNat(activate(XS)),activate(N), activate(XS)) ; } { Marked_U161(tt,N) > Marked_activate(N) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_activate(V2) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_activate(V1) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_isLNat(activate(V1)) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_U141(isLNat(activate(V1)), activate(V2)) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_activate(V2) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_activate(V1) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_isNatural(activate(V1)) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_U151(isNatural(activate(V1)), activate(V2)) ; } { Marked_U151(tt,V2) > Marked_activate(V2) ; } { Marked_U151(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U141(tt,V2) > Marked_activate(V2) ; } { Marked_U141(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U131(tt,V2) > Marked_activate(V2) ; } { Marked_U131(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U101(tt,V2) > Marked_activate(V2) ; } { Marked_U101(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U51(tt,V2) > Marked_activate(V2) ; } { Marked_U51(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U41(tt,V2) > Marked_activate(V2) ; } { Marked_U41(tt,V2) > Marked_isLNat(activate(V2)) ; } { Marked_U31(tt,N,XS) > Marked_activate(N) ; } { Marked_U31(tt,N,XS) > Marked_activate(XS) ; } { Marked_U31(tt,N,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U31(tt,N,XS) > Marked_U32(isLNat(activate(XS)),activate(N)) ; } { Marked_U21(tt,X,Y) > Marked_activate(Y) ; } { Marked_U21(tt,X,Y) > Marked_activate(X) ; } { Marked_U21(tt,X,Y) > Marked_isLNat(activate(Y)) ; } { Marked_U21(tt,X,Y) > Marked_U22(isLNat(activate(Y)),activate(X)) ; } { Marked_U11(tt,N,XS) > Marked_activate(N) ; } { Marked_U11(tt,N,XS) > Marked_activate(XS) ; } { Marked_U11(tt,N,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U11(tt,N,XS) > Marked_U12(isLNat(activate(XS)),activate(N), activate(XS)) ; } { Marked_U32(tt,N) > Marked_activate(N) ; } { Marked_U222(tt,N,XS) > Marked_activate(N) ; } { Marked_U222(tt,N,XS) > Marked_activate(XS) ; } { Marked_U222(tt,N,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U222(tt,N,XS) > Marked_fst(splitAt(activate(N),activate(XS))) ; } { Marked_U22(tt,X) > Marked_activate(X) ; } { Marked_U212(tt,XS) > Marked_activate(XS) ; } { Marked_U204(pair(YS,ZS),X) > Marked_activate(X) ; } { Marked_U203(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U203(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U203(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U203(tt,N,X,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U203(tt,N,X,XS) > Marked_U204(splitAt(activate(N),activate(XS)), activate(X)) ; } { Marked_U202(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U202(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U202(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U202(tt,N,X,XS) > Marked_isLNat(activate(XS)) ; } { Marked_U202(tt,N,X,XS) > Marked_U203(isLNat(activate(XS)),activate(N), activate(X),activate(XS)) ; } { Marked_U182(tt,Y) > Marked_activate(Y) ; } { Marked_U172(tt,N,XS) > Marked_activate(N) ; } { Marked_U172(tt,N,XS) > Marked_activate(XS) ; } { Marked_U172(tt,N,XS) > Marked_head(afterNth(activate(N),activate(XS))) ; } { Marked_U172(tt,N,XS) > Marked_afterNth(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_splitAt(activate(N),activate(XS)) ; } { Marked_U12(tt,N,XS) > Marked_snd(splitAt(activate(N),activate(XS))) ; } } === 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 Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 15.000000 === === STOPING TIMER real === Sat solver returned === STOPING TIMER real === === STOPING TIMER virtual === No solution found 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 solver returned === STOPING TIMER real === === 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 52.794056 seconds (real time) Cime Exit Status: 0