- : unit = () - : 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 (Subterm criterion) 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 (Subterm criterion) ST: Marked_app -> 1 APPLY CRITERIA (Subterm criterion) ST: Marked_iflow -> 3 Marked_low -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_ifhigh -> 3 Marked_high -> 2 APPLY CRITERIA (Subterm criterion) ST: Marked_le -> 1 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: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 0.256672 seconds (real time) Cime Exit Status: 0