- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] U101(tt,N,XS) -> fst(splitAt(activate(N),activate(XS))) [2] U11(tt,N,XS) -> snd(splitAt(activate(N),activate(XS))) [3] U21(tt,X) -> activate(X) [4] U31(tt,N) -> activate(N) [5] U41(tt,N) -> cons(activate(N),n__natsFrom(n__s(activate(N)))) [6] U51(tt,N,XS) -> head(afterNth(activate(N),activate(XS))) [7] U61(tt,Y) -> activate(Y) [8] U71(tt,XS) -> pair(nil,activate(XS)) [9] U81(tt,N,X,XS) -> U82(splitAt(activate(N),activate(XS)),activate(X)) [10] U82(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS) [11] U91(tt,XS) -> activate(XS) [12] afterNth(N,XS) -> U11(and(isNatural(N),n__isLNat(XS)),N,XS) [13] and(tt,X) -> activate(X) [14] fst(pair(X,Y)) -> U21(and(isLNat(X),n__isLNat(Y)),X) [15] head(cons(N,XS)) -> U31(and(isNatural(N),n__isLNat(activate(XS))),N) [16] isLNat(n__nil) -> tt [17] isLNat(n__afterNth(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) [18] isLNat(n__cons(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) [19] isLNat(n__fst(V1)) -> isPLNat(activate(V1)) [20] isLNat(n__natsFrom(V1)) -> isNatural(activate(V1)) [21] isLNat(n__snd(V1)) -> isPLNat(activate(V1)) [22] isLNat(n__tail(V1)) -> isLNat(activate(V1)) [23] isLNat(n__take(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) [24] isNatural(n__0) -> tt [25] isNatural(n__head(V1)) -> isLNat(activate(V1)) [26] isNatural(n__s(V1)) -> isNatural(activate(V1)) [27] isNatural(n__sel(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) [28] isPLNat(n__pair(V1,V2)) -> and(isLNat(activate(V1)),n__isLNat(activate(V2))) [29] isPLNat(n__splitAt(V1,V2)) -> and(isNatural(activate(V1)),n__isLNat(activate(V2))) [30] natsFrom(N) -> U41(isNatural(N),N) [31] sel(N,XS) -> U51(and(isNatural(N),n__isLNat(XS)),N,XS) [32] snd(pair(X,Y)) -> U61(and(isLNat(X),n__isLNat(Y)),Y) [33] splitAt(0,XS) -> U71(isLNat(XS),XS) [34] splitAt(s(N),cons(X,XS)) -> U81(and(isNatural(N),n__and(n__isNatural(X),n__isLNat(activate(XS)))), N,X,activate(XS)) [35] tail(cons(N,XS)) -> U91(and(isNatural(N),n__isLNat(activate(XS))),activate(XS)) [36] take(N,XS) -> U101(and(isNatural(N),n__isLNat(XS)),N,XS) [37] natsFrom(X) -> n__natsFrom(X) [38] s(X) -> n__s(X) [39] isLNat(X) -> n__isLNat(X) [40] nil -> n__nil [41] afterNth(X1,X2) -> n__afterNth(X1,X2) [42] cons(X1,X2) -> n__cons(X1,X2) [43] fst(X) -> n__fst(X) [44] snd(X) -> n__snd(X) [45] tail(X) -> n__tail(X) [46] take(X1,X2) -> n__take(X1,X2) [47] 0 -> n__0 [48] head(X) -> n__head(X) [49] sel(X1,X2) -> n__sel(X1,X2) [50] pair(X1,X2) -> n__pair(X1,X2) [51] splitAt(X1,X2) -> n__splitAt(X1,X2) [52] and(X1,X2) -> n__and(X1,X2) [53] isNatural(X) -> n__isNatural(X) [54] activate(n__natsFrom(X)) -> natsFrom(activate(X)) [55] activate(n__s(X)) -> s(activate(X)) [56] activate(n__isLNat(X)) -> isLNat(X) [57] activate(n__nil) -> nil [58] activate(n__afterNth(X1,X2)) -> afterNth(activate(X1),activate(X2)) [59] activate(n__cons(X1,X2)) -> cons(activate(X1),X2) [60] activate(n__fst(X)) -> fst(activate(X)) [61] activate(n__snd(X)) -> snd(activate(X)) [62] activate(n__tail(X)) -> tail(activate(X)) [63] activate(n__take(X1,X2)) -> take(activate(X1),activate(X2)) [64] activate(n__0) -> 0 [65] activate(n__head(X)) -> head(activate(X)) [66] activate(n__sel(X1,X2)) -> sel(activate(X1),activate(X2)) [67] activate(n__pair(X1,X2)) -> pair(activate(X1),activate(X2)) [68] activate(n__splitAt(X1,X2)) -> splitAt(activate(X1),activate(X2)) [69] activate(n__and(X1,X2)) -> and(activate(X1),X2) [70] activate(n__isNatural(X)) -> isNatural(X) [71] 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: { fst(pair(X,Y)) >= U21(and(isLNat(X),n__isLNat(Y)),X) ; fst(X) >= n__fst(X) ; splitAt(0,XS) >= U71(isLNat(XS),XS) ; splitAt(s(N),cons(X,XS)) >= U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))),N,X,activate(XS)) ; splitAt(X1,X2) >= n__splitAt(X1,X2) ; activate(n__natsFrom(X)) >= natsFrom(activate(X)) ; activate(n__s(X)) >= s(activate(X)) ; activate(n__isLNat(X)) >= isLNat(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(n__and(X1,X2)) >= and(activate(X1),X2) ; activate(n__isNatural(X)) >= isNatural(X) ; activate(X) >= X ; U101(tt,N,XS) >= fst(splitAt(activate(N),activate(XS))) ; snd(pair(X,Y)) >= U61(and(isLNat(X),n__isLNat(Y)),Y) ; snd(X) >= n__snd(X) ; U11(tt,N,XS) >= snd(splitAt(activate(N),activate(XS))) ; U21(tt,X) >= activate(X) ; U31(tt,N) >= activate(N) ; cons(X1,X2) >= n__cons(X1,X2) ; U41(tt,N) >= cons(activate(N),n__natsFrom(n__s(activate(N)))) ; head(cons(N,XS)) >= U31(and(isNatural(N),n__isLNat(activate(XS))),N) ; head(X) >= n__head(X) ; afterNth(N,XS) >= U11(and(isNatural(N),n__isLNat(XS)),N,XS) ; afterNth(X1,X2) >= n__afterNth(X1,X2) ; U51(tt,N,XS) >= head(afterNth(activate(N),activate(XS))) ; U61(tt,Y) >= activate(Y) ; pair(X1,X2) >= n__pair(X1,X2) ; nil >= n__nil ; U71(tt,XS) >= pair(nil,activate(XS)) ; U82(pair(YS,ZS),X) >= pair(cons(activate(X),YS),ZS) ; U81(tt,N,X,XS) >= U82(splitAt(activate(N),activate(XS)),activate(X)) ; U91(tt,XS) >= activate(XS) ; and(tt,X) >= activate(X) ; and(X1,X2) >= n__and(X1,X2) ; isNatural(n__s(V1)) >= isNatural(activate(V1)) ; isNatural(n__0) >= tt ; isNatural(n__head(V1)) >= isLNat(activate(V1)) ; isNatural(n__sel(V1,V2)) >= and(isNatural(activate(V1)), n__isLNat(activate(V2))) ; isNatural(X) >= n__isNatural(X) ; isLNat(n__natsFrom(V1)) >= isNatural(activate(V1)) ; isLNat(n__nil) >= tt ; isLNat(n__afterNth(V1,V2)) >= and(isNatural(activate(V1)), n__isLNat(activate(V2))) ; isLNat(n__cons(V1,V2)) >= and(isNatural(activate(V1)), n__isLNat(activate(V2))) ; isLNat(n__fst(V1)) >= isPLNat(activate(V1)) ; isLNat(n__snd(V1)) >= isPLNat(activate(V1)) ; isLNat(n__tail(V1)) >= isLNat(activate(V1)) ; isLNat(n__take(V1,V2)) >= and(isNatural(activate(V1)), n__isLNat(activate(V2))) ; isLNat(X) >= n__isLNat(X) ; isPLNat(n__pair(V1,V2)) >= and(isLNat(activate(V1)),n__isLNat(activate(V2))) ; isPLNat(n__splitAt(V1,V2)) >= and(isNatural(activate(V1)), n__isLNat(activate(V2))) ; natsFrom(N) >= U41(isNatural(N),N) ; natsFrom(X) >= n__natsFrom(X) ; sel(N,XS) >= U51(and(isNatural(N),n__isLNat(XS)),N,XS) ; sel(X1,X2) >= n__sel(X1,X2) ; 0 >= n__0 ; s(X) >= n__s(X) ; tail(cons(N,XS)) >= U91(and(isNatural(N),n__isLNat(activate(XS))), activate(XS)) ; tail(X) >= n__tail(X) ; take(N,XS) >= U101(and(isNatural(N),n__isLNat(XS)),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__isLNat(X)) >= Marked_isLNat(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_activate(n__and(X1,X2)) >= Marked_activate(X1) ; Marked_activate(n__and(X1,X2)) >= Marked_and(activate(X1),X2) ; Marked_activate(n__isNatural(X)) >= Marked_isNatural(X) ; 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(V1) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_activate(V2) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_isNatural(activate(V1)) ; Marked_isNatural(n__sel(V1,V2)) >= Marked_and(isNatural(activate(V1)), n__isLNat(activate(V2))) ; Marked_and(tt,X) >= Marked_activate(X) ; Marked_splitAt(0,XS) >= Marked_isLNat(XS) ; Marked_splitAt(0,XS) >= Marked_U71(isLNat(XS),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_and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) ; Marked_splitAt(s(N),cons(X,XS)) >= Marked_U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N,X,activate(XS)) ; Marked_sel(N,XS) >= Marked_isNatural(N) ; Marked_sel(N,XS) >= Marked_and(isNatural(N),n__isLNat(XS)) ; Marked_sel(N,XS) >= Marked_U51(and(isNatural(N),n__isLNat(XS)),N,XS) ; Marked_head(cons(N,XS)) >= Marked_activate(XS) ; Marked_head(cons(N,XS)) >= Marked_isNatural(N) ; Marked_head(cons(N,XS)) >= Marked_and(isNatural(N),n__isLNat(activate(XS))) ; Marked_head(cons(N,XS)) >= Marked_U31(and(isNatural(N), n__isLNat(activate(XS))),N) ; Marked_take(N,XS) >= Marked_isNatural(N) ; Marked_take(N,XS) >= Marked_and(isNatural(N),n__isLNat(XS)) ; Marked_take(N,XS) >= Marked_U101(and(isNatural(N),n__isLNat(XS)),N,XS) ; Marked_tail(cons(N,XS)) >= Marked_activate(XS) ; Marked_tail(cons(N,XS)) >= Marked_isNatural(N) ; Marked_tail(cons(N,XS)) >= Marked_and(isNatural(N),n__isLNat(activate(XS))) ; Marked_tail(cons(N,XS)) >= Marked_U91(and(isNatural(N), n__isLNat(activate(XS))),activate(XS)) ; Marked_snd(pair(X,Y)) >= Marked_and(isLNat(X),n__isLNat(Y)) ; Marked_snd(pair(X,Y)) >= Marked_isLNat(X) ; Marked_snd(pair(X,Y)) >= Marked_U61(and(isLNat(X),n__isLNat(Y)),Y) ; Marked_fst(pair(X,Y)) >= Marked_and(isLNat(X),n__isLNat(Y)) ; Marked_fst(pair(X,Y)) >= Marked_isLNat(X) ; Marked_fst(pair(X,Y)) >= Marked_U21(and(isLNat(X),n__isLNat(Y)),X) ; Marked_afterNth(N,XS) >= Marked_isNatural(N) ; Marked_afterNth(N,XS) >= Marked_and(isNatural(N),n__isLNat(XS)) ; Marked_afterNth(N,XS) >= Marked_U11(and(isNatural(N),n__isLNat(XS)),N,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(V1) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_activate(V2) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_isNatural(activate(V1)) ; Marked_isLNat(n__afterNth(V1,V2)) >= Marked_and(isNatural(activate(V1)), n__isLNat(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_isNatural(activate(V1)) ; Marked_isLNat(n__cons(V1,V2)) >= Marked_and(isNatural(activate(V1)), n__isLNat(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(V1) ; Marked_isLNat(n__take(V1,V2)) >= Marked_activate(V2) ; Marked_isLNat(n__take(V1,V2)) >= Marked_isNatural(activate(V1)) ; Marked_isLNat(n__take(V1,V2)) >= Marked_and(isNatural(activate(V1)), n__isLNat(activate(V2))) ; Marked_natsFrom(N) >= Marked_isNatural(N) ; Marked_natsFrom(N) >= Marked_U41(isNatural(N),N) ; Marked_U101(tt,N,XS) >= Marked_activate(N) ; Marked_U101(tt,N,XS) >= Marked_activate(XS) ; Marked_U101(tt,N,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U101(tt,N,XS) >= Marked_fst(splitAt(activate(N),activate(XS))) ; Marked_U91(tt,XS) >= Marked_activate(XS) ; Marked_U81(tt,N,X,XS) >= Marked_activate(N) ; Marked_U81(tt,N,X,XS) >= Marked_activate(XS) ; Marked_U81(tt,N,X,XS) >= Marked_activate(X) ; Marked_U81(tt,N,X,XS) >= Marked_splitAt(activate(N),activate(XS)) ; Marked_U81(tt,N,X,XS) >= Marked_U82(splitAt(activate(N),activate(XS)), activate(X)) ; Marked_U71(tt,XS) >= Marked_activate(XS) ; Marked_U61(tt,Y) >= Marked_activate(Y) ; Marked_U51(tt,N,XS) >= Marked_activate(N) ; Marked_U51(tt,N,XS) >= Marked_activate(XS) ; Marked_U51(tt,N,XS) >= Marked_head(afterNth(activate(N),activate(XS))) ; Marked_U51(tt,N,XS) >= Marked_afterNth(activate(N),activate(XS)) ; Marked_U41(tt,N) >= Marked_activate(N) ; 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_and(isLNat(activate(V1)), n__isLNat(activate(V2))) ; Marked_isPLNat(n__pair(V1,V2)) >= Marked_isLNat(activate(V1)) ; 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_isNatural(activate(V1)) ; Marked_isPLNat(n__splitAt(V1,V2)) >= Marked_and(isNatural(activate(V1)), n__isLNat(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_U82(pair(YS,ZS),X) >= Marked_activate(X) ; } + 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__isLNat(X)) > Marked_isLNat(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_activate(n__and(X1,X2)) > Marked_activate(X1) ; } { Marked_activate(n__and(X1,X2)) > Marked_and(activate(X1),X2) ; } { Marked_activate(n__isNatural(X)) > Marked_isNatural(X) ; } { 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(V1) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_activate(V2) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_isNatural(activate(V1)) ; } { Marked_isNatural(n__sel(V1,V2)) > Marked_and(isNatural(activate(V1)), n__isLNat(activate(V2))) ; } { Marked_and(tt,X) > Marked_activate(X) ; } { Marked_splitAt(0,XS) > Marked_isLNat(XS) ; } { Marked_splitAt(0,XS) > Marked_U71(isLNat(XS),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_and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))) ; } { Marked_splitAt(s(N),cons(X,XS)) > Marked_U81(and(isNatural(N), n__and(n__isNatural(X), n__isLNat(activate(XS)))), N,X,activate(XS)) ; } { Marked_sel(N,XS) > Marked_isNatural(N) ; } { Marked_sel(N,XS) > Marked_and(isNatural(N),n__isLNat(XS)) ; } { Marked_sel(N,XS) > Marked_U51(and(isNatural(N),n__isLNat(XS)),N,XS) ; } { Marked_head(cons(N,XS)) > Marked_activate(XS) ; } { Marked_head(cons(N,XS)) > Marked_isNatural(N) ; } { Marked_head(cons(N,XS)) > Marked_and(isNatural(N),n__isLNat(activate(XS))) ; } { Marked_head(cons(N,XS)) > Marked_U31(and(isNatural(N), n__isLNat(activate(XS))),N) ; } { Marked_take(N,XS) > Marked_isNatural(N) ; } { Marked_take(N,XS) > Marked_and(isNatural(N),n__isLNat(XS)) ; } { Marked_take(N,XS) > Marked_U101(and(isNatural(N),n__isLNat(XS)),N,XS) ; } { Marked_tail(cons(N,XS)) > Marked_activate(XS) ; } { Marked_tail(cons(N,XS)) > Marked_isNatural(N) ; } { Marked_tail(cons(N,XS)) > Marked_and(isNatural(N),n__isLNat(activate(XS))) ; } { Marked_tail(cons(N,XS)) > Marked_U91(and(isNatural(N), n__isLNat(activate(XS))),activate(XS)) ; } { Marked_snd(pair(X,Y)) > Marked_and(isLNat(X),n__isLNat(Y)) ; } { Marked_snd(pair(X,Y)) > Marked_isLNat(X) ; } { Marked_snd(pair(X,Y)) > Marked_U61(and(isLNat(X),n__isLNat(Y)),Y) ; } { Marked_fst(pair(X,Y)) > Marked_and(isLNat(X),n__isLNat(Y)) ; } { Marked_fst(pair(X,Y)) > Marked_isLNat(X) ; } { Marked_fst(pair(X,Y)) > Marked_U21(and(isLNat(X),n__isLNat(Y)),X) ; } { Marked_afterNth(N,XS) > Marked_isNatural(N) ; } { Marked_afterNth(N,XS) > Marked_and(isNatural(N),n__isLNat(XS)) ; } { Marked_afterNth(N,XS) > Marked_U11(and(isNatural(N),n__isLNat(XS)),N,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(V1) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_isNatural(activate(V1)) ; } { Marked_isLNat(n__afterNth(V1,V2)) > Marked_and(isNatural(activate(V1)), n__isLNat(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_isNatural(activate(V1)) ; } { Marked_isLNat(n__cons(V1,V2)) > Marked_and(isNatural(activate(V1)), n__isLNat(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(V1) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_activate(V2) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_isNatural(activate(V1)) ; } { Marked_isLNat(n__take(V1,V2)) > Marked_and(isNatural(activate(V1)), n__isLNat(activate(V2))) ; } { Marked_natsFrom(N) > Marked_isNatural(N) ; } { Marked_natsFrom(N) > Marked_U41(isNatural(N),N) ; } { Marked_U101(tt,N,XS) > Marked_activate(N) ; } { Marked_U101(tt,N,XS) > Marked_activate(XS) ; } { Marked_U101(tt,N,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U101(tt,N,XS) > Marked_fst(splitAt(activate(N),activate(XS))) ; } { Marked_U91(tt,XS) > Marked_activate(XS) ; } { Marked_U81(tt,N,X,XS) > Marked_activate(N) ; } { Marked_U81(tt,N,X,XS) > Marked_activate(XS) ; } { Marked_U81(tt,N,X,XS) > Marked_activate(X) ; } { Marked_U81(tt,N,X,XS) > Marked_splitAt(activate(N),activate(XS)) ; } { Marked_U81(tt,N,X,XS) > Marked_U82(splitAt(activate(N),activate(XS)), activate(X)) ; } { Marked_U71(tt,XS) > Marked_activate(XS) ; } { Marked_U61(tt,Y) > Marked_activate(Y) ; } { Marked_U51(tt,N,XS) > Marked_activate(N) ; } { Marked_U51(tt,N,XS) > Marked_activate(XS) ; } { Marked_U51(tt,N,XS) > Marked_head(afterNth(activate(N),activate(XS))) ; } { Marked_U51(tt,N,XS) > Marked_afterNth(activate(N),activate(XS)) ; } { Marked_U41(tt,N) > Marked_activate(N) ; } { 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_and(isLNat(activate(V1)), n__isLNat(activate(V2))) ; } { Marked_isPLNat(n__pair(V1,V2)) > Marked_isLNat(activate(V1)) ; } { 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_isNatural(activate(V1)) ; } { Marked_isPLNat(n__splitAt(V1,V2)) > Marked_and(isNatural(activate(V1)), n__isLNat(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_U82(pair(YS,ZS),X) > Marked_activate(X) ; } } === 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 timeout reached === STOPING TIMER virtual === Time out for these parameters. === TIMER virtual : 50.000000 === trying sub matrices of size: 1 Matrix interpretation constraints generated. Search parameters: LINEAR MATRIX 3x3 (strict=1x1) ; time limit: 50.. Termination constraints generated. Starting Sat solver initialization Calling Sat solver... === STOPING TIMER virtual === === TIMER real : 50.000000 === === STOPING TIMER real === Sat timeout reached === STOPING TIMER virtual === No solution found for these parameters. No solution found for these constraints. APPLY CRITERIA (ID_CRIT) NOT SOLVED No proof found Cime worked for 114.287985 seconds (real time) Cime Exit Status: 0