- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(U101(tt,N,XS)) -> mark(fst(splitAt(N,XS))) [2] active(U11(tt,N,XS)) -> mark(snd(splitAt(N,XS))) [3] active(U21(tt,X)) -> mark(X) [4] active(U31(tt,N)) -> mark(N) [5] active(U41(tt,N)) -> mark(cons(N,natsFrom(s(N)))) [6] active(U51(tt,N,XS)) -> mark(head(afterNth(N,XS))) [7] active(U61(tt,Y)) -> mark(Y) [8] active(U71(tt,XS)) -> mark(pair(nil,XS)) [9] active(U81(tt,N,X,XS)) -> mark(U82(splitAt(N,XS),X)) [10] active(U82(pair(YS,ZS),X)) -> mark(pair(cons(X,YS),ZS)) [11] active(U91(tt,XS)) -> mark(XS) [12] active(afterNth(N,XS)) -> mark(U11(and(isNatural(N),isLNat(XS)),N,XS)) [13] active(and(tt,X)) -> mark(X) [14] active(fst(pair(X,Y))) -> mark(U21(and(isLNat(X),isLNat(Y)),X)) [15] active(head(cons(N,XS))) -> mark(U31(and(isNatural(N),isLNat(XS)),N)) [16] active(isLNat(nil)) -> mark(tt) [17] active(isLNat(afterNth(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) [18] active(isLNat(cons(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) [19] active(isLNat(fst(V1))) -> mark(isPLNat(V1)) [20] active(isLNat(natsFrom(V1))) -> mark(isNatural(V1)) [21] active(isLNat(snd(V1))) -> mark(isPLNat(V1)) [22] active(isLNat(tail(V1))) -> mark(isLNat(V1)) [23] active(isLNat(take(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) [24] active(isNatural(0)) -> mark(tt) [25] active(isNatural(head(V1))) -> mark(isLNat(V1)) [26] active(isNatural(s(V1))) -> mark(isNatural(V1)) [27] active(isNatural(sel(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) [28] active(isPLNat(pair(V1,V2))) -> mark(and(isLNat(V1),isLNat(V2))) [29] active(isPLNat(splitAt(V1,V2))) -> mark(and(isNatural(V1),isLNat(V2))) [30] active(natsFrom(N)) -> mark(U41(isNatural(N),N)) [31] active(sel(N,XS)) -> mark(U51(and(isNatural(N),isLNat(XS)),N,XS)) [32] active(snd(pair(X,Y))) -> mark(U61(and(isLNat(X),isLNat(Y)),Y)) [33] active(splitAt(0,XS)) -> mark(U71(isLNat(XS),XS)) [34] active(splitAt(s(N),cons(X,XS))) -> mark(U81(and(isNatural(N),and(isNatural(X),isLNat(XS))),N,X,XS)) [35] active(tail(cons(N,XS))) -> mark(U91(and(isNatural(N),isLNat(XS)),XS)) [36] active(take(N,XS)) -> mark(U101(and(isNatural(N),isLNat(XS)),N,XS)) [37] mark(U101(X1,X2,X3)) -> active(U101(mark(X1),X2,X3)) [38] mark(tt) -> active(tt) [39] mark(fst(X)) -> active(fst(mark(X))) [40] mark(splitAt(X1,X2)) -> active(splitAt(mark(X1),mark(X2))) [41] mark(U11(X1,X2,X3)) -> active(U11(mark(X1),X2,X3)) [42] mark(snd(X)) -> active(snd(mark(X))) [43] mark(U21(X1,X2)) -> active(U21(mark(X1),X2)) [44] mark(U31(X1,X2)) -> active(U31(mark(X1),X2)) [45] mark(U41(X1,X2)) -> active(U41(mark(X1),X2)) [46] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [47] mark(natsFrom(X)) -> active(natsFrom(mark(X))) [48] mark(s(X)) -> active(s(mark(X))) [49] mark(U51(X1,X2,X3)) -> active(U51(mark(X1),X2,X3)) [50] mark(head(X)) -> active(head(mark(X))) [51] mark(afterNth(X1,X2)) -> active(afterNth(mark(X1),mark(X2))) [52] mark(U61(X1,X2)) -> active(U61(mark(X1),X2)) [53] mark(U71(X1,X2)) -> active(U71(mark(X1),X2)) [54] mark(pair(X1,X2)) -> active(pair(mark(X1),mark(X2))) [55] mark(nil) -> active(nil) [56] mark(U81(X1,X2,X3,X4)) -> active(U81(mark(X1),X2,X3,X4)) [57] mark(U82(X1,X2)) -> active(U82(mark(X1),X2)) [58] mark(U91(X1,X2)) -> active(U91(mark(X1),X2)) [59] mark(and(X1,X2)) -> active(and(mark(X1),X2)) [60] mark(isNatural(X)) -> active(isNatural(X)) [61] mark(isLNat(X)) -> active(isLNat(X)) [62] mark(isPLNat(X)) -> active(isPLNat(X)) [63] mark(tail(X)) -> active(tail(mark(X))) [64] mark(take(X1,X2)) -> active(take(mark(X1),mark(X2))) [65] mark(0) -> active(0) [66] mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2))) [67] U101(mark(X1),X2,X3) -> U101(X1,X2,X3) [68] U101(X1,mark(X2),X3) -> U101(X1,X2,X3) [69] U101(X1,X2,mark(X3)) -> U101(X1,X2,X3) [70] U101(active(X1),X2,X3) -> U101(X1,X2,X3) [71] U101(X1,active(X2),X3) -> U101(X1,X2,X3) [72] U101(X1,X2,active(X3)) -> U101(X1,X2,X3) [73] fst(mark(X)) -> fst(X) [74] fst(active(X)) -> fst(X) [75] splitAt(mark(X1),X2) -> splitAt(X1,X2) [76] splitAt(X1,mark(X2)) -> splitAt(X1,X2) [77] splitAt(active(X1),X2) -> splitAt(X1,X2) [78] splitAt(X1,active(X2)) -> splitAt(X1,X2) [79] U11(mark(X1),X2,X3) -> U11(X1,X2,X3) [80] U11(X1,mark(X2),X3) -> U11(X1,X2,X3) [81] U11(X1,X2,mark(X3)) -> U11(X1,X2,X3) [82] U11(active(X1),X2,X3) -> U11(X1,X2,X3) [83] U11(X1,active(X2),X3) -> U11(X1,X2,X3) [84] U11(X1,X2,active(X3)) -> U11(X1,X2,X3) [85] snd(mark(X)) -> snd(X) [86] snd(active(X)) -> snd(X) [87] U21(mark(X1),X2) -> U21(X1,X2) [88] U21(X1,mark(X2)) -> U21(X1,X2) [89] U21(active(X1),X2) -> U21(X1,X2) [90] U21(X1,active(X2)) -> U21(X1,X2) [91] U31(mark(X1),X2) -> U31(X1,X2) [92] U31(X1,mark(X2)) -> U31(X1,X2) [93] U31(active(X1),X2) -> U31(X1,X2) [94] U31(X1,active(X2)) -> U31(X1,X2) [95] U41(mark(X1),X2) -> U41(X1,X2) [96] U41(X1,mark(X2)) -> U41(X1,X2) [97] U41(active(X1),X2) -> U41(X1,X2) [98] U41(X1,active(X2)) -> U41(X1,X2) [99] cons(mark(X1),X2) -> cons(X1,X2) [100] cons(X1,mark(X2)) -> cons(X1,X2) [101] cons(active(X1),X2) -> cons(X1,X2) [102] cons(X1,active(X2)) -> cons(X1,X2) [103] natsFrom(mark(X)) -> natsFrom(X) [104] natsFrom(active(X)) -> natsFrom(X) [105] s(mark(X)) -> s(X) [106] s(active(X)) -> s(X) [107] U51(mark(X1),X2,X3) -> U51(X1,X2,X3) [108] U51(X1,mark(X2),X3) -> U51(X1,X2,X3) [109] U51(X1,X2,mark(X3)) -> U51(X1,X2,X3) [110] U51(active(X1),X2,X3) -> U51(X1,X2,X3) [111] U51(X1,active(X2),X3) -> U51(X1,X2,X3) [112] U51(X1,X2,active(X3)) -> U51(X1,X2,X3) [113] head(mark(X)) -> head(X) [114] head(active(X)) -> head(X) [115] afterNth(mark(X1),X2) -> afterNth(X1,X2) [116] afterNth(X1,mark(X2)) -> afterNth(X1,X2) [117] afterNth(active(X1),X2) -> afterNth(X1,X2) [118] afterNth(X1,active(X2)) -> afterNth(X1,X2) [119] U61(mark(X1),X2) -> U61(X1,X2) [120] U61(X1,mark(X2)) -> U61(X1,X2) [121] U61(active(X1),X2) -> U61(X1,X2) [122] U61(X1,active(X2)) -> U61(X1,X2) [123] U71(mark(X1),X2) -> U71(X1,X2) [124] U71(X1,mark(X2)) -> U71(X1,X2) [125] U71(active(X1),X2) -> U71(X1,X2) [126] U71(X1,active(X2)) -> U71(X1,X2) [127] pair(mark(X1),X2) -> pair(X1,X2) [128] pair(X1,mark(X2)) -> pair(X1,X2) [129] pair(active(X1),X2) -> pair(X1,X2) [130] pair(X1,active(X2)) -> pair(X1,X2) [131] U81(mark(X1),X2,X3,X4) -> U81(X1,X2,X3,X4) [132] U81(X1,mark(X2),X3,X4) -> U81(X1,X2,X3,X4) [133] U81(X1,X2,mark(X3),X4) -> U81(X1,X2,X3,X4) [134] U81(X1,X2,X3,mark(X4)) -> U81(X1,X2,X3,X4) [135] U81(active(X1),X2,X3,X4) -> U81(X1,X2,X3,X4) [136] U81(X1,active(X2),X3,X4) -> U81(X1,X2,X3,X4) [137] U81(X1,X2,active(X3),X4) -> U81(X1,X2,X3,X4) [138] U81(X1,X2,X3,active(X4)) -> U81(X1,X2,X3,X4) [139] U82(mark(X1),X2) -> U82(X1,X2) [140] U82(X1,mark(X2)) -> U82(X1,X2) [141] U82(active(X1),X2) -> U82(X1,X2) [142] U82(X1,active(X2)) -> U82(X1,X2) [143] U91(mark(X1),X2) -> U91(X1,X2) [144] U91(X1,mark(X2)) -> U91(X1,X2) [145] U91(active(X1),X2) -> U91(X1,X2) [146] U91(X1,active(X2)) -> U91(X1,X2) [147] and(mark(X1),X2) -> and(X1,X2) [148] and(X1,mark(X2)) -> and(X1,X2) [149] and(active(X1),X2) -> and(X1,X2) [150] and(X1,active(X2)) -> and(X1,X2) [151] isNatural(mark(X)) -> isNatural(X) [152] isNatural(active(X)) -> isNatural(X) [153] isLNat(mark(X)) -> isLNat(X) [154] isLNat(active(X)) -> isLNat(X) [155] isPLNat(mark(X)) -> isPLNat(X) [156] isPLNat(active(X)) -> isPLNat(X) [157] tail(mark(X)) -> tail(X) [158] tail(active(X)) -> tail(X) [159] take(mark(X1),X2) -> take(X1,X2) [160] take(X1,mark(X2)) -> take(X1,X2) [161] take(active(X1),X2) -> take(X1,X2) [162] take(X1,active(X2)) -> take(X1,X2) [163] sel(mark(X1),X2) -> sel(X1,X2) [164] sel(X1,mark(X2)) -> sel(X1,X2) [165] sel(active(X1),X2) -> sel(X1,X2) [166] sel(X1,active(X2)) -> sel(X1,X2) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 28 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(fst(X)) >= active(fst(mark(X))) ; mark(splitAt(X1,X2)) >= active(splitAt(mark(X1),mark(X2))) ; mark(U101(X1,X2,X3)) >= active(U101(mark(X1),X2,X3)) ; mark(tt) >= active(tt) ; mark(snd(X)) >= active(snd(mark(X))) ; mark(U11(X1,X2,X3)) >= active(U11(mark(X1),X2,X3)) ; mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) ; mark(U31(X1,X2)) >= active(U31(mark(X1),X2)) ; mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(natsFrom(X)) >= active(natsFrom(mark(X))) ; mark(s(X)) >= active(s(mark(X))) ; mark(U41(X1,X2)) >= active(U41(mark(X1),X2)) ; mark(head(X)) >= active(head(mark(X))) ; mark(afterNth(X1,X2)) >= active(afterNth(mark(X1),mark(X2))) ; mark(U51(X1,X2,X3)) >= active(U51(mark(X1),X2,X3)) ; mark(U61(X1,X2)) >= active(U61(mark(X1),X2)) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; mark(U71(X1,X2)) >= active(U71(mark(X1),X2)) ; mark(U82(X1,X2)) >= active(U82(mark(X1),X2)) ; mark(U81(X1,X2,X3,X4)) >= active(U81(mark(X1),X2,X3,X4)) ; mark(U91(X1,X2)) >= active(U91(mark(X1),X2)) ; mark(and(X1,X2)) >= active(and(mark(X1),X2)) ; mark(isNatural(X)) >= active(isNatural(X)) ; mark(isLNat(X)) >= active(isLNat(X)) ; mark(isPLNat(X)) >= active(isPLNat(X)) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(0) >= active(0) ; mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ; fst(mark(X)) >= fst(X) ; fst(active(X)) >= fst(X) ; splitAt(mark(X1),X2) >= splitAt(X1,X2) ; splitAt(active(X1),X2) >= splitAt(X1,X2) ; splitAt(X1,mark(X2)) >= splitAt(X1,X2) ; splitAt(X1,active(X2)) >= splitAt(X1,X2) ; active(fst(pair(X,Y))) >= mark(U21(and(isLNat(X),isLNat(Y)),X)) ; active(splitAt(s(N),cons(X,XS))) >= mark(U81(and(isNatural(N), and(isNatural(X),isLNat(XS))), N,X,XS)) ; active(splitAt(0,XS)) >= mark(U71(isLNat(XS),XS)) ; active(U101(tt,N,XS)) >= mark(fst(splitAt(N,XS))) ; active(snd(pair(X,Y))) >= mark(U61(and(isLNat(X),isLNat(Y)),Y)) ; active(U11(tt,N,XS)) >= mark(snd(splitAt(N,XS))) ; active(U21(tt,X)) >= mark(X) ; active(U31(tt,N)) >= mark(N) ; active(natsFrom(N)) >= mark(U41(isNatural(N),N)) ; active(U41(tt,N)) >= mark(cons(N,natsFrom(s(N)))) ; active(head(cons(N,XS))) >= mark(U31(and(isNatural(N),isLNat(XS)),N)) ; active(afterNth(N,XS)) >= mark(U11(and(isNatural(N),isLNat(XS)),N,XS)) ; active(U51(tt,N,XS)) >= mark(head(afterNth(N,XS))) ; active(U61(tt,Y)) >= mark(Y) ; active(U71(tt,XS)) >= mark(pair(nil,XS)) ; active(U82(pair(YS,ZS),X)) >= mark(pair(cons(X,YS),ZS)) ; active(U81(tt,N,X,XS)) >= mark(U82(splitAt(N,XS),X)) ; active(U91(tt,XS)) >= mark(XS) ; active(and(tt,X)) >= mark(X) ; active(isNatural(s(V1))) >= mark(isNatural(V1)) ; active(isNatural(head(V1))) >= mark(isLNat(V1)) ; active(isNatural(0)) >= mark(tt) ; active(isNatural(sel(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isLNat(fst(V1))) >= mark(isPLNat(V1)) ; active(isLNat(snd(V1))) >= mark(isPLNat(V1)) ; active(isLNat(cons(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isLNat(natsFrom(V1))) >= mark(isNatural(V1)) ; active(isLNat(afterNth(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isLNat(nil)) >= mark(tt) ; active(isLNat(tail(V1))) >= mark(isLNat(V1)) ; active(isLNat(take(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isPLNat(splitAt(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isPLNat(pair(V1,V2))) >= mark(and(isLNat(V1),isLNat(V2))) ; active(tail(cons(N,XS))) >= mark(U91(and(isNatural(N),isLNat(XS)),XS)) ; active(take(N,XS)) >= mark(U101(and(isNatural(N),isLNat(XS)),N,XS)) ; active(sel(N,XS)) >= mark(U51(and(isNatural(N),isLNat(XS)),N,XS)) ; U101(mark(X1),X2,X3) >= U101(X1,X2,X3) ; U101(active(X1),X2,X3) >= U101(X1,X2,X3) ; U101(X1,mark(X2),X3) >= U101(X1,X2,X3) ; U101(X1,active(X2),X3) >= U101(X1,X2,X3) ; U101(X1,X2,mark(X3)) >= U101(X1,X2,X3) ; U101(X1,X2,active(X3)) >= U101(X1,X2,X3) ; snd(mark(X)) >= snd(X) ; snd(active(X)) >= snd(X) ; U11(mark(X1),X2,X3) >= U11(X1,X2,X3) ; U11(active(X1),X2,X3) >= U11(X1,X2,X3) ; U11(X1,mark(X2),X3) >= U11(X1,X2,X3) ; U11(X1,active(X2),X3) >= U11(X1,X2,X3) ; U11(X1,X2,mark(X3)) >= U11(X1,X2,X3) ; U11(X1,X2,active(X3)) >= U11(X1,X2,X3) ; U21(mark(X1),X2) >= U21(X1,X2) ; U21(active(X1),X2) >= U21(X1,X2) ; U21(X1,mark(X2)) >= U21(X1,X2) ; U21(X1,active(X2)) >= U21(X1,X2) ; U31(mark(X1),X2) >= U31(X1,X2) ; U31(active(X1),X2) >= U31(X1,X2) ; U31(X1,mark(X2)) >= U31(X1,X2) ; U31(X1,active(X2)) >= U31(X1,X2) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; natsFrom(mark(X)) >= natsFrom(X) ; natsFrom(active(X)) >= natsFrom(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; U41(mark(X1),X2) >= U41(X1,X2) ; U41(active(X1),X2) >= U41(X1,X2) ; U41(X1,mark(X2)) >= U41(X1,X2) ; U41(X1,active(X2)) >= U41(X1,X2) ; head(mark(X)) >= head(X) ; head(active(X)) >= head(X) ; afterNth(mark(X1),X2) >= afterNth(X1,X2) ; afterNth(active(X1),X2) >= afterNth(X1,X2) ; afterNth(X1,mark(X2)) >= afterNth(X1,X2) ; afterNth(X1,active(X2)) >= afterNth(X1,X2) ; U51(mark(X1),X2,X3) >= U51(X1,X2,X3) ; U51(active(X1),X2,X3) >= U51(X1,X2,X3) ; U51(X1,mark(X2),X3) >= U51(X1,X2,X3) ; U51(X1,active(X2),X3) >= U51(X1,X2,X3) ; U51(X1,X2,mark(X3)) >= U51(X1,X2,X3) ; U51(X1,X2,active(X3)) >= U51(X1,X2,X3) ; U61(mark(X1),X2) >= U61(X1,X2) ; U61(active(X1),X2) >= U61(X1,X2) ; U61(X1,mark(X2)) >= U61(X1,X2) ; U61(X1,active(X2)) >= U61(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; U71(mark(X1),X2) >= U71(X1,X2) ; U71(active(X1),X2) >= U71(X1,X2) ; U71(X1,mark(X2)) >= U71(X1,X2) ; U71(X1,active(X2)) >= U71(X1,X2) ; U82(mark(X1),X2) >= U82(X1,X2) ; U82(active(X1),X2) >= U82(X1,X2) ; U82(X1,mark(X2)) >= U82(X1,X2) ; U82(X1,active(X2)) >= U82(X1,X2) ; U81(mark(X1),X2,X3,X4) >= U81(X1,X2,X3,X4) ; U81(active(X1),X2,X3,X4) >= U81(X1,X2,X3,X4) ; U81(X1,mark(X2),X3,X4) >= U81(X1,X2,X3,X4) ; U81(X1,active(X2),X3,X4) >= U81(X1,X2,X3,X4) ; U81(X1,X2,mark(X3),X4) >= U81(X1,X2,X3,X4) ; U81(X1,X2,active(X3),X4) >= U81(X1,X2,X3,X4) ; U81(X1,X2,X3,mark(X4)) >= U81(X1,X2,X3,X4) ; U81(X1,X2,X3,active(X4)) >= U81(X1,X2,X3,X4) ; U91(mark(X1),X2) >= U91(X1,X2) ; U91(active(X1),X2) >= U91(X1,X2) ; U91(X1,mark(X2)) >= U91(X1,X2) ; U91(X1,active(X2)) >= U91(X1,X2) ; and(mark(X1),X2) >= and(X1,X2) ; and(active(X1),X2) >= and(X1,X2) ; and(X1,mark(X2)) >= and(X1,X2) ; and(X1,active(X2)) >= and(X1,X2) ; isNatural(mark(X)) >= isNatural(X) ; isNatural(active(X)) >= isNatural(X) ; isLNat(mark(X)) >= isLNat(X) ; isLNat(active(X)) >= isLNat(X) ; isPLNat(mark(X)) >= isPLNat(X) ; isPLNat(active(X)) >= isPLNat(X) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; take(mark(X1),X2) >= take(X1,X2) ; take(active(X1),X2) >= take(X1,X2) ; take(X1,mark(X2)) >= take(X1,X2) ; take(X1,active(X2)) >= take(X1,X2) ; sel(mark(X1),X2) >= sel(X1,X2) ; sel(active(X1),X2) >= sel(X1,X2) ; sel(X1,mark(X2)) >= sel(X1,X2) ; sel(X1,active(X2)) >= sel(X1,X2) ; Marked_mark(fst(X)) >= Marked_mark(X) ; Marked_mark(fst(X)) >= Marked_active(fst(mark(X))) ; Marked_mark(splitAt(X1,X2)) >= Marked_mark(X1) ; Marked_mark(splitAt(X1,X2)) >= Marked_mark(X2) ; Marked_mark(splitAt(X1,X2)) >= Marked_active(splitAt(mark(X1),mark(X2))) ; Marked_mark(U101(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U101(X1,X2,X3)) >= Marked_active(U101(mark(X1),X2,X3)) ; Marked_mark(snd(X)) >= Marked_mark(X) ; Marked_mark(snd(X)) >= Marked_active(snd(mark(X))) ; Marked_mark(U11(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U11(X1,X2,X3)) >= Marked_active(U11(mark(X1),X2,X3)) ; Marked_mark(U21(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) ; Marked_mark(U31(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U31(X1,X2)) >= Marked_active(U31(mark(X1),X2)) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ; Marked_mark(natsFrom(X)) >= Marked_mark(X) ; Marked_mark(natsFrom(X)) >= Marked_active(natsFrom(mark(X))) ; Marked_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(U41(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U41(X1,X2)) >= Marked_active(U41(mark(X1),X2)) ; Marked_mark(head(X)) >= Marked_mark(X) ; Marked_mark(head(X)) >= Marked_active(head(mark(X))) ; Marked_mark(afterNth(X1,X2)) >= Marked_mark(X1) ; Marked_mark(afterNth(X1,X2)) >= Marked_mark(X2) ; Marked_mark(afterNth(X1,X2)) >= Marked_active(afterNth(mark(X1),mark(X2))) ; Marked_mark(U51(X1,X2,X3)) >= Marked_mark(X1) ; Marked_mark(U51(X1,X2,X3)) >= Marked_active(U51(mark(X1),X2,X3)) ; Marked_mark(U61(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U61(X1,X2)) >= Marked_active(U61(mark(X1),X2)) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X1) ; Marked_mark(pair(X1,X2)) >= Marked_mark(X2) ; Marked_mark(pair(X1,X2)) >= Marked_active(pair(mark(X1),mark(X2))) ; Marked_mark(U71(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U71(X1,X2)) >= Marked_active(U71(mark(X1),X2)) ; Marked_mark(U82(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U82(X1,X2)) >= Marked_active(U82(mark(X1),X2)) ; Marked_mark(U81(X1,X2,X3,X4)) >= Marked_mark(X1) ; Marked_mark(U81(X1,X2,X3,X4)) >= Marked_active(U81(mark(X1),X2,X3,X4)) ; Marked_mark(U91(X1,X2)) >= Marked_mark(X1) ; Marked_mark(U91(X1,X2)) >= Marked_active(U91(mark(X1),X2)) ; Marked_mark(and(X1,X2)) >= Marked_mark(X1) ; Marked_mark(and(X1,X2)) >= Marked_active(and(mark(X1),X2)) ; Marked_mark(isNatural(X)) >= Marked_active(isNatural(X)) ; Marked_mark(isLNat(X)) >= Marked_active(isLNat(X)) ; Marked_mark(isPLNat(X)) >= Marked_active(isPLNat(X)) ; Marked_mark(tail(X)) >= Marked_mark(X) ; Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) ; Marked_mark(take(X1,X2)) >= Marked_mark(X1) ; Marked_mark(take(X1,X2)) >= Marked_mark(X2) ; Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) ; Marked_mark(sel(X1,X2)) >= Marked_mark(X1) ; Marked_mark(sel(X1,X2)) >= Marked_mark(X2) ; Marked_mark(sel(X1,X2)) >= Marked_active(sel(mark(X1),mark(X2))) ; Marked_active(fst(pair(X,Y))) >= Marked_mark(U21(and(isLNat(X),isLNat(Y)),X)) ; Marked_active(splitAt(s(N),cons(X,XS))) >= Marked_mark(U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N,X,XS)) ; Marked_active(splitAt(0,XS)) >= Marked_mark(U71(isLNat(XS),XS)) ; Marked_active(U101(tt,N,XS)) >= Marked_mark(fst(splitAt(N,XS))) ; Marked_active(snd(pair(X,Y))) >= Marked_mark(U61(and(isLNat(X),isLNat(Y)),Y)) ; Marked_active(U11(tt,N,XS)) >= Marked_mark(snd(splitAt(N,XS))) ; Marked_active(U21(tt,X)) >= Marked_mark(X) ; Marked_active(U31(tt,N)) >= Marked_mark(N) ; Marked_active(natsFrom(N)) >= Marked_mark(U41(isNatural(N),N)) ; Marked_active(U41(tt,N)) >= Marked_mark(cons(N,natsFrom(s(N)))) ; Marked_active(head(cons(N,XS))) >= Marked_mark(U31(and(isNatural(N), isLNat(XS)),N)) ; Marked_active(afterNth(N,XS)) >= Marked_mark(U11(and(isNatural(N),isLNat(XS)), N,XS)) ; Marked_active(U51(tt,N,XS)) >= Marked_mark(head(afterNth(N,XS))) ; Marked_active(U61(tt,Y)) >= Marked_mark(Y) ; Marked_active(U71(tt,XS)) >= Marked_mark(pair(nil,XS)) ; Marked_active(U82(pair(YS,ZS),X)) >= Marked_mark(pair(cons(X,YS),ZS)) ; Marked_active(U81(tt,N,X,XS)) >= Marked_mark(U82(splitAt(N,XS),X)) ; Marked_active(U91(tt,XS)) >= Marked_mark(XS) ; Marked_active(and(tt,X)) >= Marked_mark(X) ; Marked_active(isNatural(s(V1))) >= Marked_mark(isNatural(V1)) ; Marked_active(isNatural(head(V1))) >= Marked_mark(isLNat(V1)) ; Marked_active(isNatural(sel(V1,V2))) >= Marked_mark(and(isNatural(V1), isLNat(V2))) ; Marked_active(isLNat(fst(V1))) >= Marked_mark(isPLNat(V1)) ; Marked_active(isLNat(snd(V1))) >= Marked_mark(isPLNat(V1)) ; Marked_active(isLNat(cons(V1,V2))) >= Marked_mark(and(isNatural(V1), isLNat(V2))) ; Marked_active(isLNat(natsFrom(V1))) >= Marked_mark(isNatural(V1)) ; Marked_active(isLNat(afterNth(V1,V2))) >= Marked_mark(and(isNatural(V1), isLNat(V2))) ; Marked_active(isLNat(tail(V1))) >= Marked_mark(isLNat(V1)) ; Marked_active(isLNat(take(V1,V2))) >= Marked_mark(and(isNatural(V1), isLNat(V2))) ; Marked_active(isPLNat(splitAt(V1,V2))) >= Marked_mark(and(isNatural(V1), isLNat(V2))) ; Marked_active(isPLNat(pair(V1,V2))) >= Marked_mark(and(isLNat(V1),isLNat(V2))) ; Marked_active(tail(cons(N,XS))) >= Marked_mark(U91(and(isNatural(N), isLNat(XS)),XS)) ; Marked_active(take(N,XS)) >= Marked_mark(U101(and(isNatural(N),isLNat(XS)), N,XS)) ; Marked_active(sel(N,XS)) >= Marked_mark(U51(and(isNatural(N),isLNat(XS)), N,XS)) ; } + Disjunctions:{ { Marked_mark(fst(X)) > Marked_mark(X) ; } { Marked_mark(fst(X)) > Marked_active(fst(mark(X))) ; } { Marked_mark(splitAt(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(splitAt(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(splitAt(X1,X2)) > Marked_active(splitAt(mark(X1),mark(X2))) ; } { Marked_mark(U101(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U101(X1,X2,X3)) > Marked_active(U101(mark(X1),X2,X3)) ; } { Marked_mark(snd(X)) > Marked_mark(X) ; } { Marked_mark(snd(X)) > Marked_active(snd(mark(X))) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U11(X1,X2,X3)) > Marked_active(U11(mark(X1),X2,X3)) ; } { Marked_mark(U21(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U21(X1,X2)) > Marked_active(U21(mark(X1),X2)) ; } { Marked_mark(U31(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U31(X1,X2)) > Marked_active(U31(mark(X1),X2)) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ; } { Marked_mark(natsFrom(X)) > Marked_mark(X) ; } { Marked_mark(natsFrom(X)) > Marked_active(natsFrom(mark(X))) ; } { Marked_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(U41(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U41(X1,X2)) > Marked_active(U41(mark(X1),X2)) ; } { Marked_mark(head(X)) > Marked_mark(X) ; } { Marked_mark(head(X)) > Marked_active(head(mark(X))) ; } { Marked_mark(afterNth(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(afterNth(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(afterNth(X1,X2)) > Marked_active(afterNth(mark(X1),mark(X2))) ; } { Marked_mark(U51(X1,X2,X3)) > Marked_mark(X1) ; } { Marked_mark(U51(X1,X2,X3)) > Marked_active(U51(mark(X1),X2,X3)) ; } { Marked_mark(U61(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U61(X1,X2)) > Marked_active(U61(mark(X1),X2)) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(pair(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(pair(X1,X2)) > Marked_active(pair(mark(X1),mark(X2))) ; } { Marked_mark(U71(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U71(X1,X2)) > Marked_active(U71(mark(X1),X2)) ; } { Marked_mark(U82(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U82(X1,X2)) > Marked_active(U82(mark(X1),X2)) ; } { Marked_mark(U81(X1,X2,X3,X4)) > Marked_mark(X1) ; } { Marked_mark(U81(X1,X2,X3,X4)) > Marked_active(U81(mark(X1),X2,X3,X4)) ; } { Marked_mark(U91(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(U91(X1,X2)) > Marked_active(U91(mark(X1),X2)) ; } { Marked_mark(and(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(and(X1,X2)) > Marked_active(and(mark(X1),X2)) ; } { Marked_mark(isNatural(X)) > Marked_active(isNatural(X)) ; } { Marked_mark(isLNat(X)) > Marked_active(isLNat(X)) ; } { Marked_mark(isPLNat(X)) > Marked_active(isPLNat(X)) ; } { Marked_mark(tail(X)) > Marked_mark(X) ; } { Marked_mark(tail(X)) > Marked_active(tail(mark(X))) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(take(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(take(X1,X2)) > Marked_active(take(mark(X1),mark(X2))) ; } { Marked_mark(sel(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(sel(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(sel(X1,X2)) > Marked_active(sel(mark(X1),mark(X2))) ; } { Marked_active(fst(pair(X,Y))) > Marked_mark(U21(and(isLNat(X),isLNat(Y)),X)) ; } { Marked_active(splitAt(s(N),cons(X,XS))) > Marked_mark(U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N,X,XS)) ; } { Marked_active(splitAt(0,XS)) > Marked_mark(U71(isLNat(XS),XS)) ; } { Marked_active(U101(tt,N,XS)) > Marked_mark(fst(splitAt(N,XS))) ; } { Marked_active(snd(pair(X,Y))) > Marked_mark(U61(and(isLNat(X),isLNat(Y)),Y)) ; } { Marked_active(U11(tt,N,XS)) > Marked_mark(snd(splitAt(N,XS))) ; } { Marked_active(U21(tt,X)) > Marked_mark(X) ; } { Marked_active(U31(tt,N)) > Marked_mark(N) ; } { Marked_active(natsFrom(N)) > Marked_mark(U41(isNatural(N),N)) ; } { Marked_active(U41(tt,N)) > Marked_mark(cons(N,natsFrom(s(N)))) ; } { Marked_active(head(cons(N,XS))) > Marked_mark(U31(and(isNatural(N), isLNat(XS)),N)) ; } { Marked_active(afterNth(N,XS)) > Marked_mark(U11(and(isNatural(N),isLNat(XS)), N,XS)) ; } { Marked_active(U51(tt,N,XS)) > Marked_mark(head(afterNth(N,XS))) ; } { Marked_active(U61(tt,Y)) > Marked_mark(Y) ; } { Marked_active(U71(tt,XS)) > Marked_mark(pair(nil,XS)) ; } { Marked_active(U82(pair(YS,ZS),X)) > Marked_mark(pair(cons(X,YS),ZS)) ; } { Marked_active(U81(tt,N,X,XS)) > Marked_mark(U82(splitAt(N,XS),X)) ; } { Marked_active(U91(tt,XS)) > Marked_mark(XS) ; } { Marked_active(and(tt,X)) > Marked_mark(X) ; } { Marked_active(isNatural(s(V1))) > Marked_mark(isNatural(V1)) ; } { Marked_active(isNatural(head(V1))) > Marked_mark(isLNat(V1)) ; } { Marked_active(isNatural(sel(V1,V2))) > Marked_mark(and(isNatural(V1), isLNat(V2))) ; } { Marked_active(isLNat(fst(V1))) > Marked_mark(isPLNat(V1)) ; } { Marked_active(isLNat(snd(V1))) > Marked_mark(isPLNat(V1)) ; } { Marked_active(isLNat(cons(V1,V2))) > Marked_mark(and(isNatural(V1), isLNat(V2))) ; } { Marked_active(isLNat(natsFrom(V1))) > Marked_mark(isNatural(V1)) ; } { Marked_active(isLNat(afterNth(V1,V2))) > Marked_mark(and(isNatural(V1), isLNat(V2))) ; } { Marked_active(isLNat(tail(V1))) > Marked_mark(isLNat(V1)) ; } { Marked_active(isLNat(take(V1,V2))) > Marked_mark(and(isNatural(V1), isLNat(V2))) ; } { Marked_active(isPLNat(splitAt(V1,V2))) > Marked_mark(and(isNatural(V1), isLNat(V2))) ; } { Marked_active(isPLNat(pair(V1,V2))) > Marked_mark(and(isLNat(V1),isLNat(V2))) ; } { Marked_active(tail(cons(N,XS))) > Marked_mark(U91(and(isNatural(N), isLNat(XS)),XS)) ; } { Marked_active(take(N,XS)) > Marked_mark(U101(and(isNatural(N),isLNat(XS)), N,XS)) ; } { Marked_active(sel(N,XS)) > Marked_mark(U51(and(isNatural(N),isLNat(XS)),N,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 Sat solver result read === STOPING TIMER real === === STOPING TIMER virtual === constraint: mark(fst(X)) >= active(fst(mark(X))) constraint: mark(splitAt(X1,X2)) >= active(splitAt(mark(X1),mark(X2))) constraint: mark(U101(X1,X2,X3)) >= active(U101(mark(X1),X2,X3)) constraint: mark(tt) >= active(tt) constraint: mark(snd(X)) >= active(snd(mark(X))) constraint: mark(U11(X1,X2,X3)) >= active(U11(mark(X1),X2,X3)) constraint: mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) constraint: mark(U31(X1,X2)) >= active(U31(mark(X1),X2)) constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(natsFrom(X)) >= active(natsFrom(mark(X))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(U41(X1,X2)) >= active(U41(mark(X1),X2)) constraint: mark(head(X)) >= active(head(mark(X))) constraint: mark(afterNth(X1,X2)) >= active(afterNth(mark(X1),mark(X2))) constraint: mark(U51(X1,X2,X3)) >= active(U51(mark(X1),X2,X3)) constraint: mark(U61(X1,X2)) >= active(U61(mark(X1),X2)) constraint: mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) constraint: mark(nil) >= active(nil) constraint: mark(U71(X1,X2)) >= active(U71(mark(X1),X2)) constraint: mark(U82(X1,X2)) >= active(U82(mark(X1),X2)) constraint: mark(U81(X1,X2,X3,X4)) >= active(U81(mark(X1),X2,X3,X4)) constraint: mark(U91(X1,X2)) >= active(U91(mark(X1),X2)) constraint: mark(and(X1,X2)) >= active(and(mark(X1),X2)) constraint: mark(isNatural(X)) >= active(isNatural(X)) constraint: mark(isLNat(X)) >= active(isLNat(X)) constraint: mark(isPLNat(X)) >= active(isPLNat(X)) constraint: mark(tail(X)) >= active(tail(mark(X))) constraint: mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) constraint: mark(0) >= active(0) constraint: mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) constraint: fst(mark(X)) >= fst(X) constraint: fst(active(X)) >= fst(X) constraint: splitAt(mark(X1),X2) >= splitAt(X1,X2) constraint: splitAt(active(X1),X2) >= splitAt(X1,X2) constraint: splitAt(X1,mark(X2)) >= splitAt(X1,X2) constraint: splitAt(X1,active(X2)) >= splitAt(X1,X2) constraint: active(fst(pair(X,Y))) >= mark(U21(and(isLNat(X),isLNat(Y)),X)) constraint: active(splitAt(s(N),cons(X,XS))) >= mark(U81(and(isNatural(N), and(isNatural(X), isLNat(XS))), N,X,XS)) constraint: active(splitAt(0,XS)) >= mark(U71(isLNat(XS),XS)) constraint: active(U101(tt,N,XS)) >= mark(fst(splitAt(N,XS))) constraint: active(snd(pair(X,Y))) >= mark(U61(and(isLNat(X),isLNat(Y)),Y)) constraint: active(U11(tt,N,XS)) >= mark(snd(splitAt(N,XS))) constraint: active(U21(tt,X)) >= mark(X) constraint: active(U31(tt,N)) >= mark(N) constraint: active(natsFrom(N)) >= mark(U41(isNatural(N),N)) constraint: active(U41(tt,N)) >= mark(cons(N,natsFrom(s(N)))) constraint: active(head(cons(N,XS))) >= mark(U31(and(isNatural(N),isLNat(XS)), N)) constraint: active(afterNth(N,XS)) >= mark(U11(and(isNatural(N),isLNat(XS)), N,XS)) constraint: active(U51(tt,N,XS)) >= mark(head(afterNth(N,XS))) constraint: active(U61(tt,Y)) >= mark(Y) constraint: active(U71(tt,XS)) >= mark(pair(nil,XS)) constraint: active(U82(pair(YS,ZS),X)) >= mark(pair(cons(X,YS),ZS)) constraint: active(U81(tt,N,X,XS)) >= mark(U82(splitAt(N,XS),X)) constraint: active(U91(tt,XS)) >= mark(XS) constraint: active(and(tt,X)) >= mark(X) constraint: active(isNatural(s(V1))) >= mark(isNatural(V1)) constraint: active(isNatural(head(V1))) >= mark(isLNat(V1)) constraint: active(isNatural(0)) >= mark(tt) constraint: active(isNatural(sel(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) constraint: active(isLNat(fst(V1))) >= mark(isPLNat(V1)) constraint: active(isLNat(snd(V1))) >= mark(isPLNat(V1)) constraint: active(isLNat(cons(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) constraint: active(isLNat(natsFrom(V1))) >= mark(isNatural(V1)) constraint: active(isLNat(afterNth(V1,V2))) >= mark(and(isNatural(V1), isLNat(V2))) constraint: active(isLNat(nil)) >= mark(tt) constraint: active(isLNat(tail(V1))) >= mark(isLNat(V1)) constraint: active(isLNat(take(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) constraint: active(isPLNat(splitAt(V1,V2))) >= mark(and(isNatural(V1), isLNat(V2))) constraint: active(isPLNat(pair(V1,V2))) >= mark(and(isLNat(V1),isLNat(V2))) constraint: active(tail(cons(N,XS))) >= mark(U91(and(isNatural(N),isLNat(XS)), XS)) constraint: active(take(N,XS)) >= mark(U101(and(isNatural(N),isLNat(XS)),N,XS)) constraint: active(sel(N,XS)) >= mark(U51(and(isNatural(N),isLNat(XS)),N,XS)) constraint: U101(mark(X1),X2,X3) >= U101(X1,X2,X3) constraint: U101(active(X1),X2,X3) >= U101(X1,X2,X3) constraint: U101(X1,mark(X2),X3) >= U101(X1,X2,X3) constraint: U101(X1,active(X2),X3) >= U101(X1,X2,X3) constraint: U101(X1,X2,mark(X3)) >= U101(X1,X2,X3) constraint: U101(X1,X2,active(X3)) >= U101(X1,X2,X3) constraint: snd(mark(X)) >= snd(X) constraint: snd(active(X)) >= snd(X) constraint: U11(mark(X1),X2,X3) >= U11(X1,X2,X3) constraint: U11(active(X1),X2,X3) >= U11(X1,X2,X3) constraint: U11(X1,mark(X2),X3) >= U11(X1,X2,X3) constraint: U11(X1,active(X2),X3) >= U11(X1,X2,X3) constraint: U11(X1,X2,mark(X3)) >= U11(X1,X2,X3) constraint: U11(X1,X2,active(X3)) >= U11(X1,X2,X3) constraint: U21(mark(X1),X2) >= U21(X1,X2) constraint: U21(active(X1),X2) >= U21(X1,X2) constraint: U21(X1,mark(X2)) >= U21(X1,X2) constraint: U21(X1,active(X2)) >= U21(X1,X2) constraint: U31(mark(X1),X2) >= U31(X1,X2) constraint: U31(active(X1),X2) >= U31(X1,X2) constraint: U31(X1,mark(X2)) >= U31(X1,X2) constraint: U31(X1,active(X2)) >= U31(X1,X2) constraint: cons(mark(X1),X2) >= cons(X1,X2) constraint: cons(active(X1),X2) >= cons(X1,X2) constraint: cons(X1,mark(X2)) >= cons(X1,X2) constraint: cons(X1,active(X2)) >= cons(X1,X2) constraint: natsFrom(mark(X)) >= natsFrom(X) constraint: natsFrom(active(X)) >= natsFrom(X) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) constraint: U41(mark(X1),X2) >= U41(X1,X2) constraint: U41(active(X1),X2) >= U41(X1,X2) constraint: U41(X1,mark(X2)) >= U41(X1,X2) constraint: U41(X1,active(X2)) >= U41(X1,X2) constraint: head(mark(X)) >= head(X) constraint: head(active(X)) >= head(X) constraint: afterNth(mark(X1),X2) >= afterNth(X1,X2) constraint: afterNth(active(X1),X2) >= afterNth(X1,X2) constraint: afterNth(X1,mark(X2)) >= afterNth(X1,X2) constraint: afterNth(X1,active(X2)) >= afterNth(X1,X2) constraint: U51(mark(X1),X2,X3) >= U51(X1,X2,X3) constraint: U51(active(X1),X2,X3) >= U51(X1,X2,X3) constraint: U51(X1,mark(X2),X3) >= U51(X1,X2,X3) constraint: U51(X1,active(X2),X3) >= U51(X1,X2,X3) constraint: U51(X1,X2,mark(X3)) >= U51(X1,X2,X3) constraint: U51(X1,X2,active(X3)) >= U51(X1,X2,X3) constraint: U61(mark(X1),X2) >= U61(X1,X2) constraint: U61(active(X1),X2) >= U61(X1,X2) constraint: U61(X1,mark(X2)) >= U61(X1,X2) constraint: U61(X1,active(X2)) >= U61(X1,X2) constraint: pair(mark(X1),X2) >= pair(X1,X2) constraint: pair(active(X1),X2) >= pair(X1,X2) constraint: pair(X1,mark(X2)) >= pair(X1,X2) constraint: pair(X1,active(X2)) >= pair(X1,X2) constraint: U71(mark(X1),X2) >= U71(X1,X2) constraint: U71(active(X1),X2) >= U71(X1,X2) constraint: U71(X1,mark(X2)) >= U71(X1,X2) constraint: U71(X1,active(X2)) >= U71(X1,X2) constraint: U82(mark(X1),X2) >= U82(X1,X2) constraint: U82(active(X1),X2) >= U82(X1,X2) constraint: U82(X1,mark(X2)) >= U82(X1,X2) constraint: U82(X1,active(X2)) >= U82(X1,X2) constraint: U81(mark(X1),X2,X3,X4) >= U81(X1,X2,X3,X4) constraint: U81(active(X1),X2,X3,X4) >= U81(X1,X2,X3,X4) constraint: U81(X1,mark(X2),X3,X4) >= U81(X1,X2,X3,X4) constraint: U81(X1,active(X2),X3,X4) >= U81(X1,X2,X3,X4) constraint: U81(X1,X2,mark(X3),X4) >= U81(X1,X2,X3,X4) constraint: U81(X1,X2,active(X3),X4) >= U81(X1,X2,X3,X4) constraint: U81(X1,X2,X3,mark(X4)) >= U81(X1,X2,X3,X4) constraint: U81(X1,X2,X3,active(X4)) >= U81(X1,X2,X3,X4) constraint: U91(mark(X1),X2) >= U91(X1,X2) constraint: U91(active(X1),X2) >= U91(X1,X2) constraint: U91(X1,mark(X2)) >= U91(X1,X2) constraint: U91(X1,active(X2)) >= U91(X1,X2) constraint: and(mark(X1),X2) >= and(X1,X2) constraint: and(active(X1),X2) >= and(X1,X2) constraint: and(X1,mark(X2)) >= and(X1,X2) constraint: and(X1,active(X2)) >= and(X1,X2) constraint: isNatural(mark(X)) >= isNatural(X) constraint: isNatural(active(X)) >= isNatural(X) constraint: isLNat(mark(X)) >= isLNat(X) constraint: isLNat(active(X)) >= isLNat(X) constraint: isPLNat(mark(X)) >= isPLNat(X) constraint: isPLNat(active(X)) >= isPLNat(X) constraint: tail(mark(X)) >= tail(X) constraint: tail(active(X)) >= tail(X) constraint: take(mark(X1),X2) >= take(X1,X2) constraint: take(active(X1),X2) >= take(X1,X2) constraint: take(X1,mark(X2)) >= take(X1,X2) constraint: take(X1,active(X2)) >= take(X1,X2) constraint: sel(mark(X1),X2) >= sel(X1,X2) constraint: sel(active(X1),X2) >= sel(X1,X2) constraint: sel(X1,mark(X2)) >= sel(X1,X2) constraint: sel(X1,active(X2)) >= sel(X1,X2) constraint: Marked_mark(fst(X)) >= Marked_mark(X) constraint: Marked_mark(fst(X)) >= Marked_active(fst(mark(X))) constraint: Marked_mark(splitAt(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(splitAt(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(splitAt(X1,X2)) >= Marked_active(splitAt(mark(X1), mark(X2))) constraint: Marked_mark(U101(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U101(X1,X2,X3)) >= Marked_active(U101(mark(X1),X2,X3)) constraint: Marked_mark(snd(X)) >= Marked_mark(X) constraint: Marked_mark(snd(X)) >= Marked_active(snd(mark(X))) constraint: Marked_mark(U11(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U11(X1,X2,X3)) >= Marked_active(U11(mark(X1),X2,X3)) constraint: Marked_mark(U21(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U21(X1,X2)) >= Marked_active(U21(mark(X1),X2)) constraint: Marked_mark(U31(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U31(X1,X2)) >= Marked_active(U31(mark(X1),X2)) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) constraint: Marked_mark(natsFrom(X)) >= Marked_mark(X) constraint: Marked_mark(natsFrom(X)) >= Marked_active(natsFrom(mark(X))) constraint: Marked_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(U41(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U41(X1,X2)) >= Marked_active(U41(mark(X1),X2)) constraint: Marked_mark(head(X)) >= Marked_mark(X) constraint: Marked_mark(head(X)) >= Marked_active(head(mark(X))) constraint: Marked_mark(afterNth(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(afterNth(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(afterNth(X1,X2)) >= Marked_active(afterNth(mark(X1), mark(X2))) constraint: Marked_mark(U51(X1,X2,X3)) >= Marked_mark(X1) constraint: Marked_mark(U51(X1,X2,X3)) >= Marked_active(U51(mark(X1),X2,X3)) constraint: Marked_mark(U61(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U61(X1,X2)) >= Marked_active(U61(mark(X1),X2)) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(pair(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(pair(X1,X2)) >= Marked_active(pair(mark(X1),mark(X2))) constraint: Marked_mark(U71(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U71(X1,X2)) >= Marked_active(U71(mark(X1),X2)) constraint: Marked_mark(U82(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U82(X1,X2)) >= Marked_active(U82(mark(X1),X2)) constraint: Marked_mark(U81(X1,X2,X3,X4)) >= Marked_mark(X1) constraint: Marked_mark(U81(X1,X2,X3,X4)) >= Marked_active(U81(mark(X1), X2,X3,X4)) constraint: Marked_mark(U91(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(U91(X1,X2)) >= Marked_active(U91(mark(X1),X2)) constraint: Marked_mark(and(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(and(X1,X2)) >= Marked_active(and(mark(X1),X2)) constraint: Marked_mark(isNatural(X)) >= Marked_active(isNatural(X)) constraint: Marked_mark(isLNat(X)) >= Marked_active(isLNat(X)) constraint: Marked_mark(isPLNat(X)) >= Marked_active(isPLNat(X)) constraint: Marked_mark(tail(X)) >= Marked_mark(X) constraint: Marked_mark(tail(X)) >= Marked_active(tail(mark(X))) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(take(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(take(X1,X2)) >= Marked_active(take(mark(X1),mark(X2))) constraint: Marked_mark(sel(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(sel(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(sel(X1,X2)) >= Marked_active(sel(mark(X1),mark(X2))) constraint: Marked_active(fst(pair(X,Y))) >= Marked_mark(U21(and(isLNat(X), isLNat(Y)), X)) constraint: Marked_active(splitAt(s(N),cons(X,XS))) >= Marked_mark(U81( and( isNatural( N), and( isNatural( X), isLNat(XS))), N, X, XS)) constraint: Marked_active(splitAt(0,XS)) >= Marked_mark(U71(isLNat(XS),XS)) constraint: Marked_active(U101(tt,N,XS)) >= Marked_mark(fst(splitAt(N,XS))) constraint: Marked_active(snd(pair(X,Y))) >= Marked_mark(U61(and(isLNat(X), isLNat(Y)), Y)) constraint: Marked_active(U11(tt,N,XS)) >= Marked_mark(snd(splitAt(N,XS))) constraint: Marked_active(U21(tt,X)) >= Marked_mark(X) constraint: Marked_active(U31(tt,N)) >= Marked_mark(N) constraint: Marked_active(natsFrom(N)) >= Marked_mark(U41(isNatural(N),N)) constraint: Marked_active(U41(tt,N)) >= Marked_mark(cons(N,natsFrom(s(N)))) constraint: Marked_active(head(cons(N,XS))) >= Marked_mark(U31(and(isNatural(N), isLNat(XS)), N)) constraint: Marked_active(afterNth(N,XS)) >= Marked_mark(U11(and(isNatural(N), isLNat(XS)), N,XS)) constraint: Marked_active(U51(tt,N,XS)) >= Marked_mark(head(afterNth(N,XS))) constraint: Marked_active(U61(tt,Y)) >= Marked_mark(Y) constraint: Marked_active(U71(tt,XS)) >= Marked_mark(pair(nil,XS)) constraint: Marked_active(U82(pair(YS,ZS),X)) >= Marked_mark(pair(cons(X,YS), ZS)) constraint: Marked_active(U81(tt,N,X,XS)) >= Marked_mark(U82(splitAt(N,XS),X)) constraint: Marked_active(U91(tt,XS)) >= Marked_mark(XS) constraint: Marked_active(and(tt,X)) >= Marked_mark(X) constraint: Marked_active(isNatural(s(V1))) >= Marked_mark(isNatural(V1)) constraint: Marked_active(isNatural(head(V1))) >= Marked_mark(isLNat(V1)) constraint: Marked_active(isNatural(sel(V1,V2))) >= Marked_mark(and(isNatural( V1), isLNat(V2))) constraint: Marked_active(isLNat(fst(V1))) >= Marked_mark(isPLNat(V1)) constraint: Marked_active(isLNat(snd(V1))) >= Marked_mark(isPLNat(V1)) constraint: Marked_active(isLNat(cons(V1,V2))) >= Marked_mark(and(isNatural(V1), isLNat(V2))) constraint: Marked_active(isLNat(natsFrom(V1))) >= Marked_mark(isNatural(V1)) constraint: Marked_active(isLNat(afterNth(V1,V2))) >= Marked_mark(and( isNatural( V1), isLNat(V2))) constraint: Marked_active(isLNat(tail(V1))) >= Marked_mark(isLNat(V1)) constraint: Marked_active(isLNat(take(V1,V2))) >= Marked_mark(and(isNatural(V1), isLNat(V2))) constraint: Marked_active(isPLNat(splitAt(V1,V2))) >= Marked_mark(and( isNatural( V1), isLNat(V2))) constraint: Marked_active(isPLNat(pair(V1,V2))) >= Marked_mark(and(isLNat(V1), isLNat(V2))) constraint: Marked_active(tail(cons(N,XS))) >= Marked_mark(U91(and(isNatural(N), isLNat(XS)), XS)) constraint: Marked_active(take(N,XS)) >= Marked_mark(U101(and(isNatural(N), isLNat(XS)), N,XS)) constraint: Marked_active(sel(N,XS)) >= Marked_mark(U51(and(isNatural(N), isLNat(XS)), N,XS)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(fst(X)) >= active(fst(mark(X))) ; mark(splitAt(X1,X2)) >= active(splitAt(mark(X1),mark(X2))) ; mark(U101(X1,X2,X3)) >= active(U101(mark(X1),X2,X3)) ; mark(tt) >= active(tt) ; mark(snd(X)) >= active(snd(mark(X))) ; mark(U11(X1,X2,X3)) >= active(U11(mark(X1),X2,X3)) ; mark(U21(X1,X2)) >= active(U21(mark(X1),X2)) ; mark(U31(X1,X2)) >= active(U31(mark(X1),X2)) ; mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(natsFrom(X)) >= active(natsFrom(mark(X))) ; mark(s(X)) >= active(s(mark(X))) ; mark(U41(X1,X2)) >= active(U41(mark(X1),X2)) ; mark(head(X)) >= active(head(mark(X))) ; mark(afterNth(X1,X2)) >= active(afterNth(mark(X1),mark(X2))) ; mark(U51(X1,X2,X3)) >= active(U51(mark(X1),X2,X3)) ; mark(U61(X1,X2)) >= active(U61(mark(X1),X2)) ; mark(pair(X1,X2)) >= active(pair(mark(X1),mark(X2))) ; mark(nil) >= active(nil) ; mark(U71(X1,X2)) >= active(U71(mark(X1),X2)) ; mark(U82(X1,X2)) >= active(U82(mark(X1),X2)) ; mark(U81(X1,X2,X3,X4)) >= active(U81(mark(X1),X2,X3,X4)) ; mark(U91(X1,X2)) >= active(U91(mark(X1),X2)) ; mark(and(X1,X2)) >= active(and(mark(X1),X2)) ; mark(isNatural(X)) >= active(isNatural(X)) ; mark(isLNat(X)) >= active(isLNat(X)) ; mark(isPLNat(X)) >= active(isPLNat(X)) ; mark(tail(X)) >= active(tail(mark(X))) ; mark(take(X1,X2)) >= active(take(mark(X1),mark(X2))) ; mark(0) >= active(0) ; mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ; fst(mark(X)) >= fst(X) ; fst(active(X)) >= fst(X) ; splitAt(mark(X1),X2) >= splitAt(X1,X2) ; splitAt(active(X1),X2) >= splitAt(X1,X2) ; splitAt(X1,mark(X2)) >= splitAt(X1,X2) ; splitAt(X1,active(X2)) >= splitAt(X1,X2) ; active(fst(pair(X,Y))) >= mark(U21(and(isLNat(X),isLNat(Y)),X)) ; active(splitAt(s(N),cons(X,XS))) >= mark(U81(and(isNatural(N), and(isNatural(X),isLNat(XS))), N,X,XS)) ; active(splitAt(0,XS)) >= mark(U71(isLNat(XS),XS)) ; active(U101(tt,N,XS)) >= mark(fst(splitAt(N,XS))) ; active(snd(pair(X,Y))) >= mark(U61(and(isLNat(X),isLNat(Y)),Y)) ; active(U11(tt,N,XS)) >= mark(snd(splitAt(N,XS))) ; active(U21(tt,X)) >= mark(X) ; active(U31(tt,N)) >= mark(N) ; active(natsFrom(N)) >= mark(U41(isNatural(N),N)) ; active(U41(tt,N)) >= mark(cons(N,natsFrom(s(N)))) ; active(head(cons(N,XS))) >= mark(U31(and(isNatural(N),isLNat(XS)),N)) ; active(afterNth(N,XS)) >= mark(U11(and(isNatural(N),isLNat(XS)),N,XS)) ; active(U51(tt,N,XS)) >= mark(head(afterNth(N,XS))) ; active(U61(tt,Y)) >= mark(Y) ; active(U71(tt,XS)) >= mark(pair(nil,XS)) ; active(U82(pair(YS,ZS),X)) >= mark(pair(cons(X,YS),ZS)) ; active(U81(tt,N,X,XS)) >= mark(U82(splitAt(N,XS),X)) ; active(U91(tt,XS)) >= mark(XS) ; active(and(tt,X)) >= mark(X) ; active(isNatural(s(V1))) >= mark(isNatural(V1)) ; active(isNatural(head(V1))) >= mark(isLNat(V1)) ; active(isNatural(0)) >= mark(tt) ; active(isNatural(sel(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isLNat(fst(V1))) >= mark(isPLNat(V1)) ; active(isLNat(snd(V1))) >= mark(isPLNat(V1)) ; active(isLNat(cons(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isLNat(natsFrom(V1))) >= mark(isNatural(V1)) ; active(isLNat(afterNth(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isLNat(nil)) >= mark(tt) ; active(isLNat(tail(V1))) >= mark(isLNat(V1)) ; active(isLNat(take(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isPLNat(splitAt(V1,V2))) >= mark(and(isNatural(V1),isLNat(V2))) ; active(isPLNat(pair(V1,V2))) >= mark(and(isLNat(V1),isLNat(V2))) ; active(tail(cons(N,XS))) >= mark(U91(and(isNatural(N),isLNat(XS)),XS)) ; active(take(N,XS)) >= mark(U101(and(isNatural(N),isLNat(XS)),N,XS)) ; active(sel(N,XS)) >= mark(U51(and(isNatural(N),isLNat(XS)),N,XS)) ; U101(mark(X1),X2,X3) >= U101(X1,X2,X3) ; U101(active(X1),X2,X3) >= U101(X1,X2,X3) ; U101(X1,mark(X2),X3) >= U101(X1,X2,X3) ; U101(X1,active(X2),X3) >= U101(X1,X2,X3) ; U101(X1,X2,mark(X3)) >= U101(X1,X2,X3) ; U101(X1,X2,active(X3)) >= U101(X1,X2,X3) ; snd(mark(X)) >= snd(X) ; snd(active(X)) >= snd(X) ; U11(mark(X1),X2,X3) >= U11(X1,X2,X3) ; U11(active(X1),X2,X3) >= U11(X1,X2,X3) ; U11(X1,mark(X2),X3) >= U11(X1,X2,X3) ; U11(X1,active(X2),X3) >= U11(X1,X2,X3) ; U11(X1,X2,mark(X3)) >= U11(X1,X2,X3) ; U11(X1,X2,active(X3)) >= U11(X1,X2,X3) ; U21(mark(X1),X2) >= U21(X1,X2) ; U21(active(X1),X2) >= U21(X1,X2) ; U21(X1,mark(X2)) >= U21(X1,X2) ; U21(X1,active(X2)) >= U21(X1,X2) ; U31(mark(X1),X2) >= U31(X1,X2) ; U31(active(X1),X2) >= U31(X1,X2) ; U31(X1,mark(X2)) >= U31(X1,X2) ; U31(X1,active(X2)) >= U31(X1,X2) ; cons(mark(X1),X2) >= cons(X1,X2) ; cons(active(X1),X2) >= cons(X1,X2) ; cons(X1,mark(X2)) >= cons(X1,X2) ; cons(X1,active(X2)) >= cons(X1,X2) ; natsFrom(mark(X)) >= natsFrom(X) ; natsFrom(active(X)) >= natsFrom(X) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; U41(mark(X1),X2) >= U41(X1,X2) ; U41(active(X1),X2) >= U41(X1,X2) ; U41(X1,mark(X2)) >= U41(X1,X2) ; U41(X1,active(X2)) >= U41(X1,X2) ; head(mark(X)) >= head(X) ; head(active(X)) >= head(X) ; afterNth(mark(X1),X2) >= afterNth(X1,X2) ; afterNth(active(X1),X2) >= afterNth(X1,X2) ; afterNth(X1,mark(X2)) >= afterNth(X1,X2) ; afterNth(X1,active(X2)) >= afterNth(X1,X2) ; U51(mark(X1),X2,X3) >= U51(X1,X2,X3) ; U51(active(X1),X2,X3) >= U51(X1,X2,X3) ; U51(X1,mark(X2),X3) >= U51(X1,X2,X3) ; U51(X1,active(X2),X3) >= U51(X1,X2,X3) ; U51(X1,X2,mark(X3)) >= U51(X1,X2,X3) ; U51(X1,X2,active(X3)) >= U51(X1,X2,X3) ; U61(mark(X1),X2) >= U61(X1,X2) ; U61(active(X1),X2) >= U61(X1,X2) ; U61(X1,mark(X2)) >= U61(X1,X2) ; U61(X1,active(X2)) >= U61(X1,X2) ; pair(mark(X1),X2) >= pair(X1,X2) ; pair(active(X1),X2) >= pair(X1,X2) ; pair(X1,mark(X2)) >= pair(X1,X2) ; pair(X1,active(X2)) >= pair(X1,X2) ; U71(mark(X1),X2) >= U71(X1,X2) ; U71(active(X1),X2) >= U71(X1,X2) ; U71(X1,mark(X2)) >= U71(X1,X2) ; U71(X1,active(X2)) >= U71(X1,X2) ; U82(mark(X1),X2) >= U82(X1,X2) ; U82(active(X1),X2) >= U82(X1,X2) ; U82(X1,mark(X2)) >= U82(X1,X2) ; U82(X1,active(X2)) >= U82(X1,X2) ; U81(mark(X1),X2,X3,X4) >= U81(X1,X2,X3,X4) ; U81(active(X1),X2,X3,X4) >= U81(X1,X2,X3,X4) ; U81(X1,mark(X2),X3,X4) >= U81(X1,X2,X3,X4) ; U81(X1,active(X2),X3,X4) >= U81(X1,X2,X3,X4) ; U81(X1,X2,mark(X3),X4) >= U81(X1,X2,X3,X4) ; U81(X1,X2,active(X3),X4) >= U81(X1,X2,X3,X4) ; U81(X1,X2,X3,mark(X4)) >= U81(X1,X2,X3,X4) ; U81(X1,X2,X3,active(X4)) >= U81(X1,X2,X3,X4) ; U91(mark(X1),X2) >= U91(X1,X2) ; U91(active(X1),X2) >= U91(X1,X2) ; U91(X1,mark(X2)) >= U91(X1,X2) ; U91(X1,active(X2)) >= U91(X1,X2) ; and(mark(X1),X2) >= and(X1,X2) ; and(active(X1),X2) >= and(X1,X2) ; and(X1,mark(X2)) >= and(X1,X2) ; and(X1,active(X2)) >= and(X1,X2) ; isNatural(mark(X)) >= isNatural(X) ; isNatural(active(X)) >= isNatural(X) ; isLNat(mark(X)) >= isLNat(X) ; isLNat(active(X)) >= isLNat(X) ; isPLNat(mark(X)) >= isPLNat(X) ; isPLNat(active(X)) >= isPLNat(X) ; tail(mark(X)) >= tail(X) ; tail(active(X)) >= tail(X) ; take(mark(X1),X2) >= take(X1,X2) ; take(active(X1),X2) >= take(X1,X2) ; take(X1,mark(X2)) >= take(X1,X2) ; take(X1,active(X2)) >= take(X1,X2) ; sel(mark(X1),X2) >= sel(X1,X2) ; sel(active(X1),X2) >= sel(X1,X2) ; sel(X1,mark(X2)) >= sel(X1,X2) ; sel(X1,active(X2)) >= sel(X1,X2) ; Marked_U101(mark(X1),X2,X3) >= Marked_U101(X1,X2,X3) ; Marked_U101(active(X1),X2,X3) >= Marked_U101(X1,X2,X3) ; Marked_U101(X1,mark(X2),X3) >= Marked_U101(X1,X2,X3) ; Marked_U101(X1,active(X2),X3) >= Marked_U101(X1,X2,X3) ; Marked_U101(X1,X2,mark(X3)) >= Marked_U101(X1,X2,X3) ; Marked_U101(X1,X2,active(X3)) >= Marked_U101(X1,X2,X3) ; } + Disjunctions:{ { Marked_U101(mark(X1),X2,X3) > Marked_U101(X1,X2,X3) ; } { Marked_U101(active(X1),X2,X3) > Marked_U101(X1,X2,X3) ; } { Marked_U101(X1,mark(X2),X3) > Marked_U101(X1,X2,X3) ; } { Marked_U101(X1,active(X2),X3) > Marked_U101(X1,X2,X3) ; } { Marked_U101(X1,X2,mark(X3)) > Marked_U101(X1,X2,X3) ; } { Marked_U101(X1,X2,active(X3)) > Marked_U101(X1,X2,X3) ; } } === 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 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 93.471844 seconds (real time) Cime Exit Status: 0