- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] qsort(nil) -> nil [2] qsort(.(x,y)) -> ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) [3] lowers(x,nil) -> nil [4] lowers(x,.(y,z)) -> if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) [5] greaters(x,nil) -> nil [6] greaters(x,.(y,z)) -> if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 3 components: { --> --> --> --> } { --> --> --> --> } { --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { qsort(nil) >= nil ; qsort(.(x,y)) >= ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) ; lowers(x,nil) >= nil ; lowers(x,.(y,z)) >= if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) ; greaters(x,nil) >= nil ; greaters(x,.(y,z)) >= if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) ; Marked_qsort(.(x,y)) >= Marked_qsort(lowers(x,y)) ; Marked_qsort(.(x,y)) >= Marked_qsort(greaters(x,y)) ; } + Disjunctions:{ { Marked_qsort(.(x,y)) > Marked_qsort(lowers(x,y)) ; } { Marked_qsort(.(x,y)) > Marked_qsort(greaters(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: qsort(nil) >= nil constraint: qsort(.(x,y)) >= ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) constraint: lowers(x,nil) >= nil constraint: lowers(x,.(y,z)) >= if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) constraint: greaters(x,nil) >= nil constraint: greaters(x,.(y,z)) >= if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) constraint: Marked_qsort(.(x,y)) >= Marked_qsort(lowers(x,y)) constraint: Marked_qsort(.(x,y)) >= Marked_qsort(greaters(x,y)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { qsort(nil) >= nil ; qsort(.(x,y)) >= ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) ; lowers(x,nil) >= nil ; lowers(x,.(y,z)) >= if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) ; greaters(x,nil) >= nil ; greaters(x,.(y,z)) >= if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) ; Marked_lowers(x,.(y,z)) >= Marked_lowers(x,z) ; } + Disjunctions:{ { Marked_lowers(x,.(y,z)) > Marked_lowers(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: qsort(nil) >= nil constraint: qsort(.(x,y)) >= ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) constraint: lowers(x,nil) >= nil constraint: lowers(x,.(y,z)) >= if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) constraint: greaters(x,nil) >= nil constraint: greaters(x,.(y,z)) >= if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) constraint: Marked_lowers(x,.(y,z)) >= Marked_lowers(x,z) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { qsort(nil) >= nil ; qsort(.(x,y)) >= ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) ; lowers(x,nil) >= nil ; lowers(x,.(y,z)) >= if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) ; greaters(x,nil) >= nil ; greaters(x,.(y,z)) >= if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) ; Marked_greaters(x,.(y,z)) >= Marked_greaters(x,z) ; } + Disjunctions:{ { Marked_greaters(x,.(y,z)) > Marked_greaters(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: qsort(nil) >= nil constraint: qsort(.(x,y)) >= ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) constraint: lowers(x,nil) >= nil constraint: lowers(x,.(y,z)) >= if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) constraint: greaters(x,nil) >= nil constraint: greaters(x,.(y,z)) >= if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) constraint: Marked_greaters(x,.(y,z)) >= Marked_greaters(x,z) 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] qsort(nil) -> nil [2] qsort(.(x,y)) -> ++(qsort(lowers(x,y)),.(x,qsort(greaters(x,y)))) [3] lowers(x,nil) -> nil [4] lowers(x,.(y,z)) -> if(<=(y,x),.(y,lowers(x,z)),lowers(x,z)) [5] greaters(x,nil) -> nil [6] greaters(x,.(y,z)) -> if(<=(y,x),greaters(x,z),.(y,greaters(x,z))) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ nil ] () = 0; [ . ] (X0,X1) = 2 + 2*X0 + 3*X1 + 0; [ ++ ] (X0,X1) = 2 + 0; [ Marked_qsort ] (X0) = 3*X0 + 0; [ if ] (X0,X1,X2) = 0; [ qsort ] (X0) = 2 + 3*X0 + 0; [ greaters ] (X0,X1) = 0; [ lowers ] (X0,X1) = 3*X1 + 0; [ <= ] (X0,X1) = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ nil ] () = 0; [ . ] (X0,X1) = 1 + 2*X1 + 0; [ ++ ] (X0,X1) = 0; [ if ] (X0,X1,X2) = 0; [ qsort ] (X0) = 0; [ Marked_lowers ] (X0,X1) = 3*X1 + 0; [ greaters ] (X0,X1) = 0; [ lowers ] (X0,X1) = 0; [ <= ] (X0,X1) = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ nil ] () = 0; [ Marked_greaters ] (X0,X1) = 3*X1 + 0; [ . ] (X0,X1) = 1 + 1*X1 + 0; [ ++ ] (X0,X1) = 0; [ if ] (X0,X1,X2) = 0; [ qsort ] (X0) = 0; [ greaters ] (X0,X1) = 0; [ lowers ] (X0,X1) = 0; [ <= ] (X0,X1) = 0; ]} ]} ]} Cime worked for 0.217504 seconds (real time) Cime Exit Status: 0