- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] active(sel(s(X),cons(Y,Z))) -> mark(sel(X,Z)) [2] active(sel(0,cons(X,Z))) -> mark(X) [3] active(first(0,Z)) -> mark(nil) [4] active(first(s(X),cons(Y,Z))) -> mark(cons(Y,first(X,Z))) [5] active(from(X)) -> mark(cons(X,from(s(X)))) [6] active(sel1(s(X),cons(Y,Z))) -> mark(sel1(X,Z)) [7] active(sel1(0,cons(X,Z))) -> mark(quote(X)) [8] active(first1(0,Z)) -> mark(nil1) [9] active(first1(s(X),cons(Y,Z))) -> mark(cons1(quote(Y),first1(X,Z))) [10] active(quote(0)) -> mark(01) [11] active(quote1(cons(X,Z))) -> mark(cons1(quote(X),quote1(Z))) [12] active(quote1(nil)) -> mark(nil1) [13] active(quote(s(X))) -> mark(s1(quote(X))) [14] active(quote(sel(X,Z))) -> mark(sel1(X,Z)) [15] active(quote1(first(X,Z))) -> mark(first1(X,Z)) [16] active(unquote(01)) -> mark(0) [17] active(unquote(s1(X))) -> mark(s(unquote(X))) [18] active(unquote1(nil1)) -> mark(nil) [19] active(unquote1(cons1(X,Z))) -> mark(fcons(unquote(X),unquote1(Z))) [20] active(fcons(X,Z)) -> mark(cons(X,Z)) [21] mark(sel(X1,X2)) -> active(sel(mark(X1),mark(X2))) [22] mark(s(X)) -> active(s(mark(X))) [23] mark(cons(X1,X2)) -> active(cons(mark(X1),X2)) [24] mark(0) -> active(0) [25] mark(first(X1,X2)) -> active(first(mark(X1),mark(X2))) [26] mark(nil) -> active(nil) [27] mark(from(X)) -> active(from(mark(X))) [28] mark(sel1(X1,X2)) -> active(sel1(mark(X1),mark(X2))) [29] mark(quote(X)) -> active(quote(X)) [30] mark(first1(X1,X2)) -> active(first1(mark(X1),mark(X2))) [31] mark(nil1) -> active(nil1) [32] mark(cons1(X1,X2)) -> active(cons1(mark(X1),mark(X2))) [33] mark(01) -> active(01) [34] mark(quote1(X)) -> active(quote1(X)) [35] mark(s1(X)) -> active(s1(mark(X))) [36] mark(unquote(X)) -> active(unquote(mark(X))) [37] mark(unquote1(X)) -> active(unquote1(mark(X))) [38] mark(fcons(X1,X2)) -> active(fcons(mark(X1),mark(X2))) [39] sel(mark(X1),X2) -> sel(X1,X2) [40] sel(X1,mark(X2)) -> sel(X1,X2) [41] sel(active(X1),X2) -> sel(X1,X2) [42] sel(X1,active(X2)) -> sel(X1,X2) [43] s(mark(X)) -> s(X) [44] s(active(X)) -> s(X) [45] cons(mark(X1),X2) -> cons(X1,X2) [46] cons(X1,mark(X2)) -> cons(X1,X2) [47] cons(active(X1),X2) -> cons(X1,X2) [48] cons(X1,active(X2)) -> cons(X1,X2) [49] first(mark(X1),X2) -> first(X1,X2) [50] first(X1,mark(X2)) -> first(X1,X2) [51] first(active(X1),X2) -> first(X1,X2) [52] first(X1,active(X2)) -> first(X1,X2) [53] from(mark(X)) -> from(X) [54] from(active(X)) -> from(X) [55] sel1(mark(X1),X2) -> sel1(X1,X2) [56] sel1(X1,mark(X2)) -> sel1(X1,X2) [57] sel1(active(X1),X2) -> sel1(X1,X2) [58] sel1(X1,active(X2)) -> sel1(X1,X2) [59] quote(mark(X)) -> quote(X) [60] quote(active(X)) -> quote(X) [61] first1(mark(X1),X2) -> first1(X1,X2) [62] first1(X1,mark(X2)) -> first1(X1,X2) [63] first1(active(X1),X2) -> first1(X1,X2) [64] first1(X1,active(X2)) -> first1(X1,X2) [65] cons1(mark(X1),X2) -> cons1(X1,X2) [66] cons1(X1,mark(X2)) -> cons1(X1,X2) [67] cons1(active(X1),X2) -> cons1(X1,X2) [68] cons1(X1,active(X2)) -> cons1(X1,X2) [69] quote1(mark(X)) -> quote1(X) [70] quote1(active(X)) -> quote1(X) [71] s1(mark(X)) -> s1(X) [72] s1(active(X)) -> s1(X) [73] unquote(mark(X)) -> unquote(X) [74] unquote(active(X)) -> unquote(X) [75] unquote1(mark(X)) -> unquote1(X) [76] unquote1(active(X)) -> unquote1(X) [77] fcons(mark(X1),X2) -> fcons(X1,X2) [78] fcons(X1,mark(X2)) -> fcons(X1,X2) [79] fcons(active(X1),X2) -> fcons(X1,X2) [80] fcons(X1,active(X2)) -> fcons(X1,X2) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 15 components: { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } { --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ; mark(s(X)) >= active(s(mark(X))) ; mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(nil) >= active(nil) ; mark(first(X1,X2)) >= active(first(mark(X1),mark(X2))) ; mark(from(X)) >= active(from(mark(X))) ; mark(sel1(X1,X2)) >= active(sel1(mark(X1),mark(X2))) ; mark(quote(X)) >= active(quote(X)) ; mark(nil1) >= active(nil1) ; mark(first1(X1,X2)) >= active(first1(mark(X1),mark(X2))) ; mark(cons1(X1,X2)) >= active(cons1(mark(X1),mark(X2))) ; mark(01) >= active(01) ; mark(quote1(X)) >= active(quote1(X)) ; mark(s1(X)) >= active(s1(mark(X))) ; mark(unquote(X)) >= active(unquote(mark(X))) ; mark(unquote1(X)) >= active(unquote1(mark(X))) ; mark(fcons(X1,X2)) >= active(fcons(mark(X1),mark(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) ; active(sel(s(X),cons(Y,Z))) >= mark(sel(X,Z)) ; active(sel(0,cons(X,Z))) >= mark(X) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,Z)) >= mark(nil) ; active(from(X)) >= mark(cons(X,from(s(X)))) ; active(sel1(s(X),cons(Y,Z))) >= mark(sel1(X,Z)) ; active(sel1(0,cons(X,Z))) >= mark(quote(X)) ; active(quote(sel(X,Z))) >= mark(sel1(X,Z)) ; active(quote(s(X))) >= mark(s1(quote(X))) ; active(quote(0)) >= mark(01) ; active(first1(s(X),cons(Y,Z))) >= mark(cons1(quote(Y),first1(X,Z))) ; active(first1(0,Z)) >= mark(nil1) ; active(quote1(cons(X,Z))) >= mark(cons1(quote(X),quote1(Z))) ; active(quote1(nil)) >= mark(nil1) ; active(quote1(first(X,Z))) >= mark(first1(X,Z)) ; active(unquote(01)) >= mark(0) ; active(unquote(s1(X))) >= mark(s(unquote(X))) ; active(unquote1(nil1)) >= mark(nil) ; active(unquote1(cons1(X,Z))) >= mark(fcons(unquote(X),unquote1(Z))) ; active(fcons(X,Z)) >= mark(cons(X,Z)) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; first(mark(X1),X2) >= first(X1,X2) ; first(active(X1),X2) >= first(X1,X2) ; first(X1,mark(X2)) >= first(X1,X2) ; first(X1,active(X2)) >= first(X1,X2) ; from(mark(X)) >= from(X) ; from(active(X)) >= from(X) ; sel1(mark(X1),X2) >= sel1(X1,X2) ; sel1(active(X1),X2) >= sel1(X1,X2) ; sel1(X1,mark(X2)) >= sel1(X1,X2) ; sel1(X1,active(X2)) >= sel1(X1,X2) ; quote(mark(X)) >= quote(X) ; quote(active(X)) >= quote(X) ; first1(mark(X1),X2) >= first1(X1,X2) ; first1(active(X1),X2) >= first1(X1,X2) ; first1(X1,mark(X2)) >= first1(X1,X2) ; first1(X1,active(X2)) >= first1(X1,X2) ; cons1(mark(X1),X2) >= cons1(X1,X2) ; cons1(active(X1),X2) >= cons1(X1,X2) ; cons1(X1,mark(X2)) >= cons1(X1,X2) ; cons1(X1,active(X2)) >= cons1(X1,X2) ; quote1(mark(X)) >= quote1(X) ; quote1(active(X)) >= quote1(X) ; s1(mark(X)) >= s1(X) ; s1(active(X)) >= s1(X) ; unquote(mark(X)) >= unquote(X) ; unquote(active(X)) >= unquote(X) ; unquote1(mark(X)) >= unquote1(X) ; unquote1(active(X)) >= unquote1(X) ; fcons(mark(X1),X2) >= fcons(X1,X2) ; fcons(active(X1),X2) >= fcons(X1,X2) ; fcons(X1,mark(X2)) >= fcons(X1,X2) ; fcons(X1,active(X2)) >= fcons(X1,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_mark(s(X)) >= Marked_mark(X) ; Marked_mark(s(X)) >= Marked_active(s(mark(X))) ; Marked_mark(cons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) ; Marked_mark(first(X1,X2)) >= Marked_mark(X1) ; Marked_mark(first(X1,X2)) >= Marked_mark(X2) ; Marked_mark(first(X1,X2)) >= Marked_active(first(mark(X1),mark(X2))) ; Marked_mark(from(X)) >= Marked_mark(X) ; Marked_mark(from(X)) >= Marked_active(from(mark(X))) ; Marked_mark(sel1(X1,X2)) >= Marked_mark(X1) ; Marked_mark(sel1(X1,X2)) >= Marked_mark(X2) ; Marked_mark(sel1(X1,X2)) >= Marked_active(sel1(mark(X1),mark(X2))) ; Marked_mark(quote(X)) >= Marked_active(quote(X)) ; Marked_mark(first1(X1,X2)) >= Marked_mark(X1) ; Marked_mark(first1(X1,X2)) >= Marked_mark(X2) ; Marked_mark(first1(X1,X2)) >= Marked_active(first1(mark(X1),mark(X2))) ; Marked_mark(cons1(X1,X2)) >= Marked_mark(X1) ; Marked_mark(cons1(X1,X2)) >= Marked_mark(X2) ; Marked_mark(cons1(X1,X2)) >= Marked_active(cons1(mark(X1),mark(X2))) ; Marked_mark(quote1(X)) >= Marked_active(quote1(X)) ; Marked_mark(s1(X)) >= Marked_mark(X) ; Marked_mark(s1(X)) >= Marked_active(s1(mark(X))) ; Marked_mark(unquote(X)) >= Marked_mark(X) ; Marked_mark(unquote(X)) >= Marked_active(unquote(mark(X))) ; Marked_mark(unquote1(X)) >= Marked_mark(X) ; Marked_mark(unquote1(X)) >= Marked_active(unquote1(mark(X))) ; Marked_mark(fcons(X1,X2)) >= Marked_mark(X1) ; Marked_mark(fcons(X1,X2)) >= Marked_mark(X2) ; Marked_mark(fcons(X1,X2)) >= Marked_active(fcons(mark(X1),mark(X2))) ; Marked_active(sel(s(X),cons(Y,Z))) >= Marked_mark(sel(X,Z)) ; Marked_active(sel(0,cons(X,Z))) >= Marked_mark(X) ; Marked_active(first(s(X),cons(Y,Z))) >= Marked_mark(cons(Y,first(X,Z))) ; Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X)))) ; Marked_active(sel1(s(X),cons(Y,Z))) >= Marked_mark(sel1(X,Z)) ; Marked_active(sel1(0,cons(X,Z))) >= Marked_mark(quote(X)) ; Marked_active(quote(sel(X,Z))) >= Marked_mark(sel1(X,Z)) ; Marked_active(quote(s(X))) >= Marked_mark(s1(quote(X))) ; Marked_active(first1(s(X),cons(Y,Z))) >= Marked_mark(cons1(quote(Y), first1(X,Z))) ; Marked_active(quote1(cons(X,Z))) >= Marked_mark(cons1(quote(X),quote1(Z))) ; Marked_active(quote1(first(X,Z))) >= Marked_mark(first1(X,Z)) ; Marked_active(unquote(s1(X))) >= Marked_mark(s(unquote(X))) ; Marked_active(unquote1(cons1(X,Z))) >= Marked_mark(fcons(unquote(X), unquote1(Z))) ; Marked_active(fcons(X,Z)) >= Marked_mark(cons(X,Z)) ; } + Disjunctions:{ { 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_mark(s(X)) > Marked_mark(X) ; } { Marked_mark(s(X)) > Marked_active(s(mark(X))) ; } { Marked_mark(cons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons(X1,X2)) > Marked_active(cons(mark(X1),X2)) ; } { Marked_mark(first(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(first(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(first(X1,X2)) > Marked_active(first(mark(X1),mark(X2))) ; } { Marked_mark(from(X)) > Marked_mark(X) ; } { Marked_mark(from(X)) > Marked_active(from(mark(X))) ; } { Marked_mark(sel1(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(sel1(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(sel1(X1,X2)) > Marked_active(sel1(mark(X1),mark(X2))) ; } { Marked_mark(quote(X)) > Marked_active(quote(X)) ; } { Marked_mark(first1(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(first1(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(first1(X1,X2)) > Marked_active(first1(mark(X1),mark(X2))) ; } { Marked_mark(cons1(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(cons1(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(cons1(X1,X2)) > Marked_active(cons1(mark(X1),mark(X2))) ; } { Marked_mark(quote1(X)) > Marked_active(quote1(X)) ; } { Marked_mark(s1(X)) > Marked_mark(X) ; } { Marked_mark(s1(X)) > Marked_active(s1(mark(X))) ; } { Marked_mark(unquote(X)) > Marked_mark(X) ; } { Marked_mark(unquote(X)) > Marked_active(unquote(mark(X))) ; } { Marked_mark(unquote1(X)) > Marked_mark(X) ; } { Marked_mark(unquote1(X)) > Marked_active(unquote1(mark(X))) ; } { Marked_mark(fcons(X1,X2)) > Marked_mark(X1) ; } { Marked_mark(fcons(X1,X2)) > Marked_mark(X2) ; } { Marked_mark(fcons(X1,X2)) > Marked_active(fcons(mark(X1),mark(X2))) ; } { Marked_active(sel(s(X),cons(Y,Z))) > Marked_mark(sel(X,Z)) ; } { Marked_active(sel(0,cons(X,Z))) > Marked_mark(X) ; } { Marked_active(first(s(X),cons(Y,Z))) > Marked_mark(cons(Y,first(X,Z))) ; } { Marked_active(from(X)) > Marked_mark(cons(X,from(s(X)))) ; } { Marked_active(sel1(s(X),cons(Y,Z))) > Marked_mark(sel1(X,Z)) ; } { Marked_active(sel1(0,cons(X,Z))) > Marked_mark(quote(X)) ; } { Marked_active(quote(sel(X,Z))) > Marked_mark(sel1(X,Z)) ; } { Marked_active(quote(s(X))) > Marked_mark(s1(quote(X))) ; } { Marked_active(first1(s(X),cons(Y,Z))) > Marked_mark(cons1(quote(Y), first1(X,Z))) ; } { Marked_active(quote1(cons(X,Z))) > Marked_mark(cons1(quote(X),quote1(Z))) ; } { Marked_active(quote1(first(X,Z))) > Marked_mark(first1(X,Z)) ; } { Marked_active(unquote(s1(X))) > Marked_mark(s(unquote(X))) ; } { Marked_active(unquote1(cons1(X,Z))) > Marked_mark(fcons(unquote(X), unquote1(Z))) ; } { Marked_active(fcons(X,Z)) > Marked_mark(cons(X,Z)) ; } } === 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(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) constraint: mark(s(X)) >= active(s(mark(X))) constraint: mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) constraint: mark(0) >= active(0) constraint: mark(nil) >= active(nil) constraint: mark(first(X1,X2)) >= active(first(mark(X1),mark(X2))) constraint: mark(from(X)) >= active(from(mark(X))) constraint: mark(sel1(X1,X2)) >= active(sel1(mark(X1),mark(X2))) constraint: mark(quote(X)) >= active(quote(X)) constraint: mark(nil1) >= active(nil1) constraint: mark(first1(X1,X2)) >= active(first1(mark(X1),mark(X2))) constraint: mark(cons1(X1,X2)) >= active(cons1(mark(X1),mark(X2))) constraint: mark(01) >= active(01) constraint: mark(quote1(X)) >= active(quote1(X)) constraint: mark(s1(X)) >= active(s1(mark(X))) constraint: mark(unquote(X)) >= active(unquote(mark(X))) constraint: mark(unquote1(X)) >= active(unquote1(mark(X))) constraint: mark(fcons(X1,X2)) >= active(fcons(mark(X1),mark(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: active(sel(s(X),cons(Y,Z))) >= mark(sel(X,Z)) constraint: active(sel(0,cons(X,Z))) >= mark(X) constraint: active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) constraint: active(first(0,Z)) >= mark(nil) constraint: active(from(X)) >= mark(cons(X,from(s(X)))) constraint: active(sel1(s(X),cons(Y,Z))) >= mark(sel1(X,Z)) constraint: active(sel1(0,cons(X,Z))) >= mark(quote(X)) constraint: active(quote(sel(X,Z))) >= mark(sel1(X,Z)) constraint: active(quote(s(X))) >= mark(s1(quote(X))) constraint: active(quote(0)) >= mark(01) constraint: active(first1(s(X),cons(Y,Z))) >= mark(cons1(quote(Y),first1(X,Z))) constraint: active(first1(0,Z)) >= mark(nil1) constraint: active(quote1(cons(X,Z))) >= mark(cons1(quote(X),quote1(Z))) constraint: active(quote1(nil)) >= mark(nil1) constraint: active(quote1(first(X,Z))) >= mark(first1(X,Z)) constraint: active(unquote(01)) >= mark(0) constraint: active(unquote(s1(X))) >= mark(s(unquote(X))) constraint: active(unquote1(nil1)) >= mark(nil) constraint: active(unquote1(cons1(X,Z))) >= mark(fcons(unquote(X),unquote1(Z))) constraint: active(fcons(X,Z)) >= mark(cons(X,Z)) constraint: s(mark(X)) >= s(X) constraint: s(active(X)) >= s(X) 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: first(mark(X1),X2) >= first(X1,X2) constraint: first(active(X1),X2) >= first(X1,X2) constraint: first(X1,mark(X2)) >= first(X1,X2) constraint: first(X1,active(X2)) >= first(X1,X2) constraint: from(mark(X)) >= from(X) constraint: from(active(X)) >= from(X) constraint: sel1(mark(X1),X2) >= sel1(X1,X2) constraint: sel1(active(X1),X2) >= sel1(X1,X2) constraint: sel1(X1,mark(X2)) >= sel1(X1,X2) constraint: sel1(X1,active(X2)) >= sel1(X1,X2) constraint: quote(mark(X)) >= quote(X) constraint: quote(active(X)) >= quote(X) constraint: first1(mark(X1),X2) >= first1(X1,X2) constraint: first1(active(X1),X2) >= first1(X1,X2) constraint: first1(X1,mark(X2)) >= first1(X1,X2) constraint: first1(X1,active(X2)) >= first1(X1,X2) constraint: cons1(mark(X1),X2) >= cons1(X1,X2) constraint: cons1(active(X1),X2) >= cons1(X1,X2) constraint: cons1(X1,mark(X2)) >= cons1(X1,X2) constraint: cons1(X1,active(X2)) >= cons1(X1,X2) constraint: quote1(mark(X)) >= quote1(X) constraint: quote1(active(X)) >= quote1(X) constraint: s1(mark(X)) >= s1(X) constraint: s1(active(X)) >= s1(X) constraint: unquote(mark(X)) >= unquote(X) constraint: unquote(active(X)) >= unquote(X) constraint: unquote1(mark(X)) >= unquote1(X) constraint: unquote1(active(X)) >= unquote1(X) constraint: fcons(mark(X1),X2) >= fcons(X1,X2) constraint: fcons(active(X1),X2) >= fcons(X1,X2) constraint: fcons(X1,mark(X2)) >= fcons(X1,X2) constraint: fcons(X1,active(X2)) >= fcons(X1,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_mark(s(X)) >= Marked_mark(X) constraint: Marked_mark(s(X)) >= Marked_active(s(mark(X))) constraint: Marked_mark(cons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons(X1,X2)) >= Marked_active(cons(mark(X1),X2)) constraint: Marked_mark(first(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(first(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(first(X1,X2)) >= Marked_active(first(mark(X1),mark(X2))) constraint: Marked_mark(from(X)) >= Marked_mark(X) constraint: Marked_mark(from(X)) >= Marked_active(from(mark(X))) constraint: Marked_mark(sel1(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(sel1(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(sel1(X1,X2)) >= Marked_active(sel1(mark(X1),mark(X2))) constraint: Marked_mark(quote(X)) >= Marked_active(quote(X)) constraint: Marked_mark(first1(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(first1(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(first1(X1,X2)) >= Marked_active(first1(mark(X1), mark(X2))) constraint: Marked_mark(cons1(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(cons1(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(cons1(X1,X2)) >= Marked_active(cons1(mark(X1),mark(X2))) constraint: Marked_mark(quote1(X)) >= Marked_active(quote1(X)) constraint: Marked_mark(s1(X)) >= Marked_mark(X) constraint: Marked_mark(s1(X)) >= Marked_active(s1(mark(X))) constraint: Marked_mark(unquote(X)) >= Marked_mark(X) constraint: Marked_mark(unquote(X)) >= Marked_active(unquote(mark(X))) constraint: Marked_mark(unquote1(X)) >= Marked_mark(X) constraint: Marked_mark(unquote1(X)) >= Marked_active(unquote1(mark(X))) constraint: Marked_mark(fcons(X1,X2)) >= Marked_mark(X1) constraint: Marked_mark(fcons(X1,X2)) >= Marked_mark(X2) constraint: Marked_mark(fcons(X1,X2)) >= Marked_active(fcons(mark(X1),mark(X2))) constraint: Marked_active(sel(s(X),cons(Y,Z))) >= Marked_mark(sel(X,Z)) constraint: Marked_active(sel(0,cons(X,Z))) >= Marked_mark(X) constraint: Marked_active(first(s(X),cons(Y,Z))) >= Marked_mark(cons( Y,first(X,Z))) constraint: Marked_active(from(X)) >= Marked_mark(cons(X,from(s(X)))) constraint: Marked_active(sel1(s(X),cons(Y,Z))) >= Marked_mark(sel1(X,Z)) constraint: Marked_active(sel1(0,cons(X,Z))) >= Marked_mark(quote(X)) constraint: Marked_active(quote(sel(X,Z))) >= Marked_mark(sel1(X,Z)) constraint: Marked_active(quote(s(X))) >= Marked_mark(s1(quote(X))) constraint: Marked_active(first1(s(X),cons(Y,Z))) >= Marked_mark(cons1( quote(Y), first1(X,Z))) constraint: Marked_active(quote1(cons(X,Z))) >= Marked_mark(cons1(quote(X), quote1(Z))) constraint: Marked_active(quote1(first(X,Z))) >= Marked_mark(first1(X,Z)) constraint: Marked_active(unquote(s1(X))) >= Marked_mark(s(unquote(X))) constraint: Marked_active(unquote1(cons1(X,Z))) >= Marked_mark(fcons( unquote(X), unquote1(Z))) constraint: Marked_active(fcons(X,Z)) >= Marked_mark(cons(X,Z)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { mark(sel(X1,X2)) >= active(sel(mark(X1),mark(X2))) ; mark(s(X)) >= active(s(mark(X))) ; mark(cons(X1,X2)) >= active(cons(mark(X1),X2)) ; mark(0) >= active(0) ; mark(nil) >= active(nil) ; mark(first(X1,X2)) >= active(first(mark(X1),mark(X2))) ; mark(from(X)) >= active(from(mark(X))) ; mark(sel1(X1,X2)) >= active(sel1(mark(X1),mark(X2))) ; mark(quote(X)) >= active(quote(X)) ; mark(nil1) >= active(nil1) ; mark(first1(X1,X2)) >= active(first1(mark(X1),mark(X2))) ; mark(cons1(X1,X2)) >= active(cons1(mark(X1),mark(X2))) ; mark(01) >= active(01) ; mark(quote1(X)) >= active(quote1(X)) ; mark(s1(X)) >= active(s1(mark(X))) ; mark(unquote(X)) >= active(unquote(mark(X))) ; mark(unquote1(X)) >= active(unquote1(mark(X))) ; mark(fcons(X1,X2)) >= active(fcons(mark(X1),mark(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) ; active(sel(s(X),cons(Y,Z))) >= mark(sel(X,Z)) ; active(sel(0,cons(X,Z))) >= mark(X) ; active(first(s(X),cons(Y,Z))) >= mark(cons(Y,first(X,Z))) ; active(first(0,Z)) >= mark(nil) ; active(from(X)) >= mark(cons(X,from(s(X)))) ; active(sel1(s(X),cons(Y,Z))) >= mark(sel1(X,Z)) ; active(sel1(0,cons(X,Z))) >= mark(quote(X)) ; active(quote(sel(X,Z))) >= mark(sel1(X,Z)) ; active(quote(s(X))) >= mark(s1(quote(X))) ; active(quote(0)) >= mark(01) ; active(first1(s(X),cons(Y,Z))) >= mark(cons1(quote(Y),first1(X,Z))) ; active(first1(0,Z)) >= mark(nil1) ; active(quote1(cons(X,Z))) >= mark(cons1(quote(X),quote1(Z))) ; active(quote1(nil)) >= mark(nil1) ; active(quote1(first(X,Z))) >= mark(first1(X,Z)) ; active(unquote(01)) >= mark(0) ; active(unquote(s1(X))) >= mark(s(unquote(X))) ; active(unquote1(nil1)) >= mark(nil) ; active(unquote1(cons1(X,Z))) >= mark(fcons(unquote(X),unquote1(Z))) ; active(fcons(X,Z)) >= mark(cons(X,Z)) ; s(mark(X)) >= s(X) ; s(active(X)) >= s(X) ; 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) ; first(mark(X1),X2) >= first(X1,X2) ; first(active(X1),X2) >= first(X1,X2) ; first(X1,mark(X2)) >= first(X1,X2) ; first(X1,active(X2)) >= first(X1,X2) ; from(mark(X)) >= from(X) ; from(active(X)) >= from(X) ; sel1(mark(X1),X2) >= sel1(X1,X2) ; sel1(active(X1),X2) >= sel1(X1,X2) ; sel1(X1,mark(X2)) >= sel1(X1,X2) ; sel1(X1,active(X2)) >= sel1(X1,X2) ; quote(mark(X)) >= quote(X) ; quote(active(X)) >= quote(X) ; first1(mark(X1),X2) >= first1(X1,X2) ; first1(active(X1),X2) >= first1(X1,X2) ; first1(X1,mark(X2)) >= first1(X1,X2) ; first1(X1,active(X2)) >= first1(X1,X2) ; cons1(mark(X1),X2) >= cons1(X1,X2) ; cons1(active(X1),X2) >= cons1(X1,X2) ; cons1(X1,mark(X2)) >= cons1(X1,X2) ; cons1(X1,active(X2)) >= cons1(X1,X2) ; quote1(mark(X)) >= quote1(X) ; quote1(active(X)) >= quote1(X) ; s1(mark(X)) >= s1(X) ; s1(active(X)) >= s1(X) ; unquote(mark(X)) >= unquote(X) ; unquote(active(X)) >= unquote(X) ; unquote1(mark(X)) >= unquote1(X) ; unquote1(active(X)) >= unquote1(X) ; fcons(mark(X1),X2) >= fcons(X1,X2) ; fcons(active(X1),X2) >= fcons(X1,X2) ; fcons(X1,mark(X2)) >= fcons(X1,X2) ; fcons(X1,active(X2)) >= fcons(X1,X2) ; Marked_sel(mark(X1),X2) >= Marked_sel(X1,X2) ; Marked_sel(active(X1),X2) >= Marked_sel(X1,X2) ; Marked_sel(X1,mark(X2)) >= Marked_sel(X1,X2) ; Marked_sel(X1,active(X2)) >= Marked_sel(X1,X2) ; } + Disjunctions:{ { Marked_sel(mark(X1),X2) > Marked_sel(X1,X2) ; } { Marked_sel(active(X1),X2) > Marked_sel(X1,X2) ; } { Marked_sel(X1,mark(X2)) > Marked_sel(X1,X2) ; } { Marked_sel(X1,active(X2)) > Marked_sel(X1,X2) ; } } === 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 === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === 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 65.600250 seconds (real time) Cime Exit Status: 0