- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] sort(nil) -> nil [2] sort(cons(x,y)) -> insert(x,sort(y)) [3] insert(x,nil) -> cons(x,nil) [4] insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) [5] choose(x,cons(v,w),y,0) -> cons(x,cons(v,w)) [6] choose(x,cons(v,w),0,s(z)) -> cons(v,insert(x,w)) [7] choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 2 components: { --> } { --> --> --> --> --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { sort(nil) >= nil ; sort(cons(x,y)) >= insert(x,sort(y)) ; insert(x,nil) >= cons(x,nil) ; insert(x,cons(v,w)) >= choose(x,cons(v,w),x,v) ; choose(x,cons(v,w),0,s(z)) >= cons(v,insert(x,w)) ; choose(x,cons(v,w),s(y),s(z)) >= choose(x,cons(v,w),y,z) ; choose(x,cons(v,w),y,0) >= cons(x,cons(v,w)) ; Marked_sort(cons(x,y)) >= Marked_sort(y) ; } + Disjunctions:{ { Marked_sort(cons(x,y)) > Marked_sort(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: sort(nil) >= nil constraint: sort(cons(x,y)) >= insert(x,sort(y)) constraint: insert(x,nil) >= cons(x,nil) constraint: insert(x,cons(v,w)) >= choose(x,cons(v,w),x,v) constraint: choose(x,cons(v,w),0,s(z)) >= cons(v,insert(x,w)) constraint: choose(x,cons(v,w),s(y),s(z)) >= choose(x,cons(v,w),y,z) constraint: choose(x,cons(v,w),y,0) >= cons(x,cons(v,w)) constraint: Marked_sort(cons(x,y)) >= Marked_sort(y) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { sort(nil) >= nil ; sort(cons(x,y)) >= insert(x,sort(y)) ; insert(x,nil) >= cons(x,nil) ; insert(x,cons(v,w)) >= choose(x,cons(v,w),x,v) ; choose(x,cons(v,w),0,s(z)) >= cons(v,insert(x,w)) ; choose(x,cons(v,w),s(y),s(z)) >= choose(x,cons(v,w),y,z) ; choose(x,cons(v,w),y,0) >= cons(x,cons(v,w)) ; Marked_choose(x,cons(v,w),0,s(z)) >= Marked_insert(x,w) ; Marked_choose(x,cons(v,w),s(y),s(z)) >= Marked_choose(x,cons(v,w),y,z) ; Marked_insert(x,cons(v,w)) >= Marked_choose(x,cons(v,w),x,v) ; } + Disjunctions:{ { Marked_choose(x,cons(v,w),0,s(z)) > Marked_insert(x,w) ; } { Marked_choose(x,cons(v,w),s(y),s(z)) > Marked_choose(x,cons(v,w),y,z) ; } { Marked_insert(x,cons(v,w)) > Marked_choose(x,cons(v,w),x,v) ; } } === 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: sort(nil) >= nil constraint: sort(cons(x,y)) >= insert(x,sort(y)) constraint: insert(x,nil) >= cons(x,nil) constraint: insert(x,cons(v,w)) >= choose(x,cons(v,w),x,v) constraint: choose(x,cons(v,w),0,s(z)) >= cons(v,insert(x,w)) constraint: choose(x,cons(v,w),s(y),s(z)) >= choose(x,cons(v,w),y,z) constraint: choose(x,cons(v,w),y,0) >= cons(x,cons(v,w)) constraint: Marked_choose(x,cons(v,w),0,s(z)) >= Marked_insert(x,w) constraint: Marked_choose(x,cons(v,w),s(y),s(z)) >= Marked_choose(x,cons(v,w), y,z) constraint: Marked_insert(x,cons(v,w)) >= Marked_choose(x,cons(v,w),x,v) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { sort(nil) >= nil ; sort(cons(x,y)) >= insert(x,sort(y)) ; insert(x,nil) >= cons(x,nil) ; insert(x,cons(v,w)) >= choose(x,cons(v,w),x,v) ; choose(x,cons(v,w),0,s(z)) >= cons(v,insert(x,w)) ; choose(x,cons(v,w),s(y),s(z)) >= choose(x,cons(v,w),y,z) ; choose(x,cons(v,w),y,0) >= cons(x,cons(v,w)) ; Marked_choose(x,cons(v,w),s(y),s(z)) >= Marked_choose(x,cons(v,w),y,z) ; } + Disjunctions:{ { Marked_choose(x,cons(v,w),s(y),s(z)) > Marked_choose(x,cons(v,w),y,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: sort(nil) >= nil constraint: sort(cons(x,y)) >= insert(x,sort(y)) constraint: insert(x,nil) >= cons(x,nil) constraint: insert(x,cons(v,w)) >= choose(x,cons(v,w),x,v) constraint: choose(x,cons(v,w),0,s(z)) >= cons(v,insert(x,w)) constraint: choose(x,cons(v,w),s(y),s(z)) >= choose(x,cons(v,w),y,z) constraint: choose(x,cons(v,w),y,0) >= cons(x,cons(v,w)) constraint: Marked_choose(x,cons(v,w),s(y),s(z)) >= Marked_choose(x,cons(v,w), y,z) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] sort(nil) -> nil [2] sort(cons(x,y)) -> insert(x,sort(y)) [3] insert(x,nil) -> cons(x,nil) [4] insert(x,cons(v,w)) -> choose(x,cons(v,w),x,v) [5] choose(x,cons(v,w),y,0) -> cons(x,cons(v,w)) [6] choose(x,cons(v,w),0,s(z)) -> cons(v,insert(x,w)) [7] choose(x,cons(v,w),s(y),s(z)) -> choose(x,cons(v,w),y,z) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ nil ] () = 0; [ choose ] (X0,X1,X2,X3) = 2 + 1*X1 + 0; [ insert ] (X0,X1) = 2 + 1*X1 + 0; [ s ] (X0) = 3*X0 + 0; [ sort ] (X0) = 1*X0 + 0; [ Marked_sort ] (X0) = 3*X0 + 0; [ 0 ] () = 0; [ cons ] (X0,X1) = 2 + 1*X1 + 0; ]} { DP termination of: , CRITERION: CG using polynomial interpretation = [ nil ] () = 3; [ Marked_insert ] (X0,X1) = 3*X1 + 3*X0 + 1; [ choose ] (X0,X1,X2,X3) = 1*X1 + 3; [ insert ] (X0,X1) = 1*X1 + 3; [ s ] (X0) = 3*X0; [ sort ] (X0) = 3*X0; [ 0 ] () = 0; [ cons ] (X0,X1) = 1*X1 + 1; [ Marked_choose ] (X0,X1,X2,X3) = 3*X1 + 3*X0; removing < Marked_choose(x,cons(v,w),0,s(z)),Marked_insert(x,w)> [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ nil ] () = 0; [ choose ] (X0,X1,X2,X3) = 0; [ insert ] (X0,X1) = 0; [ s ] (X0) = 1 + 3*X0 + 0; [ sort ] (X0) = 0; [ 0 ] () = 0; [ cons ] (X0,X1) = 0; [ Marked_choose ] (X0,X1,X2,X3) = 1*X3 + 0; ]} ]} ]} ]} ]} Cime worked for 0.126881 seconds (real time) Cime Exit Status: 0