- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] le(0,Y) -> true [2] le(s(X),0) -> false [3] le(s(X),s(Y)) -> le(X,Y) [4] app(nil,Y) -> Y [5] app(cons(N,L),Y) -> cons(N,app(L,Y)) [6] low(N,nil) -> nil [7] low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) [8] iflow(true,N,cons(M,L)) -> cons(M,low(N,L)) [9] iflow(false,N,cons(M,L)) -> low(N,L) [10] high(N,nil) -> nil [11] high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) [12] ifhigh(true,N,cons(M,L)) -> high(N,L) [13] ifhigh(false,N,cons(M,L)) -> cons(M,high(N,L)) [14] quicksort(nil) -> nil [15] quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 5 components: { --> --> --> --> } { --> } { --> --> --> --> } { --> --> --> --> } { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { le(0,Y) >= true ; le(s(X),0) >= false ; le(s(X),s(Y)) >= le(X,Y) ; app(nil,Y) >= Y ; app(cons(N,L),Y) >= cons(N,app(L,Y)) ; low(N,nil) >= nil ; low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) ; iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) ; iflow(false,N,cons(M,L)) >= low(N,L) ; high(N,nil) >= nil ; high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) ; ifhigh(true,N,cons(M,L)) >= high(N,L) ; ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) ; quicksort(nil) >= nil ; quicksort(cons(N,L)) >= app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ; Marked_quicksort(cons(N,L)) >= Marked_quicksort(low(N,L)) ; Marked_quicksort(cons(N,L)) >= Marked_quicksort(high(N,L)) ; } + Disjunctions:{ { Marked_quicksort(cons(N,L)) > Marked_quicksort(low(N,L)) ; } { Marked_quicksort(cons(N,L)) > Marked_quicksort(high(N,L)) ; } } === 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 === === STOPING TIMER virtual === constraint: le(0,Y) >= true constraint: le(s(X),0) >= false constraint: le(s(X),s(Y)) >= le(X,Y) constraint: app(nil,Y) >= Y constraint: app(cons(N,L),Y) >= cons(N,app(L,Y)) constraint: low(N,nil) >= nil constraint: low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) constraint: iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) constraint: iflow(false,N,cons(M,L)) >= low(N,L) constraint: high(N,nil) >= nil constraint: high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) constraint: ifhigh(true,N,cons(M,L)) >= high(N,L) constraint: ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) constraint: quicksort(nil) >= nil constraint: quicksort(cons(N,L)) >= app(quicksort(low(N,L)), cons(N,quicksort(high(N,L)))) constraint: Marked_quicksort(cons(N,L)) >= Marked_quicksort(low(N,L)) constraint: Marked_quicksort(cons(N,L)) >= Marked_quicksort(high(N,L)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { le(0,Y) >= true ; le(s(X),0) >= false ; le(s(X),s(Y)) >= le(X,Y) ; app(nil,Y) >= Y ; app(cons(N,L),Y) >= cons(N,app(L,Y)) ; low(N,nil) >= nil ; low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) ; iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) ; iflow(false,N,cons(M,L)) >= low(N,L) ; high(N,nil) >= nil ; high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) ; ifhigh(true,N,cons(M,L)) >= high(N,L) ; ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) ; quicksort(nil) >= nil ; quicksort(cons(N,L)) >= app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ; Marked_app(cons(N,L),Y) >= Marked_app(L,Y) ; } + Disjunctions:{ { Marked_app(cons(N,L),Y) > Marked_app(L,Y) ; } } === 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 === === STOPING TIMER virtual === constraint: le(0,Y) >= true constraint: le(s(X),0) >= false constraint: le(s(X),s(Y)) >= le(X,Y) constraint: app(nil,Y) >= Y constraint: app(cons(N,L),Y) >= cons(N,app(L,Y)) constraint: low(N,nil) >= nil constraint: low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) constraint: iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) constraint: iflow(false,N,cons(M,L)) >= low(N,L) constraint: high(N,nil) >= nil constraint: high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) constraint: ifhigh(true,N,cons(M,L)) >= high(N,L) constraint: ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) constraint: quicksort(nil) >= nil constraint: quicksort(cons(N,L)) >= app(quicksort(low(N,L)), cons(N,quicksort(high(N,L)))) constraint: Marked_app(cons(N,L),Y) >= Marked_app(L,Y) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { le(0,Y) >= true ; le(s(X),0) >= false ; le(s(X),s(Y)) >= le(X,Y) ; app(nil,Y) >= Y ; app(cons(N,L),Y) >= cons(N,app(L,Y)) ; low(N,nil) >= nil ; low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) ; iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) ; iflow(false,N,cons(M,L)) >= low(N,L) ; high(N,nil) >= nil ; high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) ; ifhigh(true,N,cons(M,L)) >= high(N,L) ; ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) ; quicksort(nil) >= nil ; quicksort(cons(N,L)) >= app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ; Marked_low(N,cons(M,L)) >= Marked_iflow(le(M,N),N,cons(M,L)) ; Marked_iflow(true,N,cons(M,L)) >= Marked_low(N,L) ; Marked_iflow(false,N,cons(M,L)) >= Marked_low(N,L) ; } + Disjunctions:{ { Marked_low(N,cons(M,L)) > Marked_iflow(le(M,N),N,cons(M,L)) ; } { Marked_iflow(true,N,cons(M,L)) > Marked_low(N,L) ; } { Marked_iflow(false,N,cons(M,L)) > Marked_low(N,L) ; } } === 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 === === STOPING TIMER virtual === constraint: le(0,Y) >= true constraint: le(s(X),0) >= false constraint: le(s(X),s(Y)) >= le(X,Y) constraint: app(nil,Y) >= Y constraint: app(cons(N,L),Y) >= cons(N,app(L,Y)) constraint: low(N,nil) >= nil constraint: low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) constraint: iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) constraint: iflow(false,N,cons(M,L)) >= low(N,L) constraint: high(N,nil) >= nil constraint: high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) constraint: ifhigh(true,N,cons(M,L)) >= high(N,L) constraint: ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) constraint: quicksort(nil) >= nil constraint: quicksort(cons(N,L)) >= app(quicksort(low(N,L)), cons(N,quicksort(high(N,L)))) constraint: Marked_low(N,cons(M,L)) >= Marked_iflow(le(M,N),N,cons(M,L)) constraint: Marked_iflow(true,N,cons(M,L)) >= Marked_low(N,L) constraint: Marked_iflow(false,N,cons(M,L)) >= Marked_low(N,L) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { le(0,Y) >= true ; le(s(X),0) >= false ; le(s(X),s(Y)) >= le(X,Y) ; app(nil,Y) >= Y ; app(cons(N,L),Y) >= cons(N,app(L,Y)) ; low(N,nil) >= nil ; low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) ; iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) ; iflow(false,N,cons(M,L)) >= low(N,L) ; high(N,nil) >= nil ; high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) ; ifhigh(true,N,cons(M,L)) >= high(N,L) ; ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) ; quicksort(nil) >= nil ; quicksort(cons(N,L)) >= app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ; Marked_high(N,cons(M,L)) >= Marked_ifhigh(le(M,N),N,cons(M,L)) ; Marked_ifhigh(true,N,cons(M,L)) >= Marked_high(N,L) ; Marked_ifhigh(false,N,cons(M,L)) >= Marked_high(N,L) ; } + Disjunctions:{ { Marked_high(N,cons(M,L)) > Marked_ifhigh(le(M,N),N,cons(M,L)) ; } { Marked_ifhigh(true,N,cons(M,L)) > Marked_high(N,L) ; } { Marked_ifhigh(false,N,cons(M,L)) > Marked_high(N,L) ; } } === 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 === === STOPING TIMER virtual === constraint: le(0,Y) >= true constraint: le(s(X),0) >= false constraint: le(s(X),s(Y)) >= le(X,Y) constraint: app(nil,Y) >= Y constraint: app(cons(N,L),Y) >= cons(N,app(L,Y)) constraint: low(N,nil) >= nil constraint: low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) constraint: iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) constraint: iflow(false,N,cons(M,L)) >= low(N,L) constraint: high(N,nil) >= nil constraint: high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) constraint: ifhigh(true,N,cons(M,L)) >= high(N,L) constraint: ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) constraint: quicksort(nil) >= nil constraint: quicksort(cons(N,L)) >= app(quicksort(low(N,L)), cons(N,quicksort(high(N,L)))) constraint: Marked_high(N,cons(M,L)) >= Marked_ifhigh(le(M,N),N,cons(M,L)) constraint: Marked_ifhigh(true,N,cons(M,L)) >= Marked_high(N,L) constraint: Marked_ifhigh(false,N,cons(M,L)) >= Marked_high(N,L) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { le(0,Y) >= true ; le(s(X),0) >= false ; le(s(X),s(Y)) >= le(X,Y) ; app(nil,Y) >= Y ; app(cons(N,L),Y) >= cons(N,app(L,Y)) ; low(N,nil) >= nil ; low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) ; iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) ; iflow(false,N,cons(M,L)) >= low(N,L) ; high(N,nil) >= nil ; high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) ; ifhigh(true,N,cons(M,L)) >= high(N,L) ; ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) ; quicksort(nil) >= nil ; quicksort(cons(N,L)) >= app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) ; Marked_le(s(X),s(Y)) >= Marked_le(X,Y) ; } + Disjunctions:{ { Marked_le(s(X),s(Y)) > Marked_le(X,Y) ; } } === 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: le(0,Y) >= true constraint: le(s(X),0) >= false constraint: le(s(X),s(Y)) >= le(X,Y) constraint: app(nil,Y) >= Y constraint: app(cons(N,L),Y) >= cons(N,app(L,Y)) constraint: low(N,nil) >= nil constraint: low(N,cons(M,L)) >= iflow(le(M,N),N,cons(M,L)) constraint: iflow(true,N,cons(M,L)) >= cons(M,low(N,L)) constraint: iflow(false,N,cons(M,L)) >= low(N,L) constraint: high(N,nil) >= nil constraint: high(N,cons(M,L)) >= ifhigh(le(M,N),N,cons(M,L)) constraint: ifhigh(true,N,cons(M,L)) >= high(N,L) constraint: ifhigh(false,N,cons(M,L)) >= cons(M,high(N,L)) constraint: quicksort(nil) >= nil constraint: quicksort(cons(N,L)) >= app(quicksort(low(N,L)), cons(N,quicksort(high(N,L)))) constraint: Marked_le(s(X),s(Y)) >= Marked_le(X,Y) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] le(0,Y) -> true [2] le(s(X),0) -> false [3] le(s(X),s(Y)) -> le(X,Y) [4] app(nil,Y) -> Y [5] app(cons(N,L),Y) -> cons(N,app(L,Y)) [6] low(N,nil) -> nil [7] low(N,cons(M,L)) -> iflow(le(M,N),N,cons(M,L)) [8] iflow(true,N,cons(M,L)) -> cons(M,low(N,L)) [9] iflow(false,N,cons(M,L)) -> low(N,L) [10] high(N,nil) -> nil [11] high(N,cons(M,L)) -> ifhigh(le(M,N),N,cons(M,L)) [12] ifhigh(true,N,cons(M,L)) -> high(N,L) [13] ifhigh(false,N,cons(M,L)) -> cons(M,high(N,L)) [14] quicksort(nil) -> nil [15] quicksort(cons(N,L)) -> app(quicksort(low(N,L)),cons(N,quicksort(high(N,L)))) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: RPO with AFS = AFS: low -> 1high -> 1iflow -> 2ifhigh -> 2 and precedence: prec (All symbols are Lex.): { true < le ; le > true ; le > false ; false < le ; app > cons ; app < quicksort ; cons < app ; cons < quicksort ; quicksort > app ; quicksort > cons ; } ]} { DP termination of: , CRITERION: ORD [ Solution found: RPO with AFS = AFS: low -> 1high -> 1iflow -> 2ifhigh -> 2 and precedence: prec (All symbols are Lex.): { true < le ; le > true ; le > false ; false < le ; app > cons ; app < quicksort ; cons < app ; cons < quicksort ; quicksort > app ; quicksort > cons ; } ]} { DP termination of: , CRITERION: CG using RPO with AFS = AFS: low -> 1high -> 1iflow -> 2Marked_iflow -> 2ifhigh -> 2Marked_low -> 1 and precedence: prec (All symbols are Lex.): { true < le ; le > true ; le > false ; false < le ; app > cons ; app < quicksort ; cons < app ; cons < quicksort ; quicksort > app ; quicksort > cons ; } removing [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: CG using RPO with AFS = AFS: Marked_high -> 1low -> 1high -> 1Marked_ifhigh -> 2iflow -> 2ifhigh -> 2 and precedence: prec (All symbols are Lex.): { true < le ; le > true ; le > false ; false < le ; app > cons ; app < quicksort ; cons < app ; cons < quicksort ; quicksort > app ; quicksort > cons ; } removing [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ true ] () = 0; [ low ] (X0,X1) = 0; [ s ] (X0) = 2 + 3*X0 + 0; [ quicksort ] (X0) = 0; [ 0 ] () = 0; [ Marked_le ] (X0,X1) = 1*X0 + 0; [ high ] (X0,X1) = 0; [ nil ] () = 0; [ le ] (X0,X1) = 0; [ iflow ] (X0,X1,X2) = 0; [ app ] (X0,X1) = 2*X1 + 0; [ false ] () = 0; [ ifhigh ] (X0,X1,X2) = 0; [ cons ] (X0,X1) = 0; ]} ]} ]} Cime worked for 10.381484 seconds (real time) Cime Exit Status: 0