- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] concat(leaf,y) -> y [2] concat(cons(u,v),y) -> cons(u,concat(v,y)) [3] less_leaves(x,leaf) -> false [4] less_leaves(leaf,cons(w,z)) -> true [5] less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,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: { concat(leaf,y) >= y ; concat(cons(u,v),y) >= cons(u,concat(v,y)) ; less_leaves(leaf,cons(w,z)) >= true ; less_leaves(cons(u,v),cons(w,z)) >= less_leaves(concat(u,v),concat(w,z)) ; less_leaves(x,leaf) >= false ; Marked_less_leaves(cons(u,v),cons(w,z)) >= Marked_less_leaves(concat(u,v), concat(w,z)) ; } + Disjunctions:{ { Marked_less_leaves(cons(u,v),cons(w,z)) > Marked_less_leaves(concat(u,v), concat(w,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: concat(leaf,y) >= y constraint: concat(cons(u,v),y) >= cons(u,concat(v,y)) constraint: less_leaves(leaf,cons(w,z)) >= true constraint: less_leaves(cons(u,v),cons(w,z)) >= less_leaves(concat(u,v), concat(w,z)) constraint: less_leaves(x,leaf) >= false constraint: Marked_less_leaves(cons(u,v),cons(w,z)) >= Marked_less_leaves( concat(u,v), concat(w,z)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { concat(leaf,y) >= y ; concat(cons(u,v),y) >= cons(u,concat(v,y)) ; less_leaves(leaf,cons(w,z)) >= true ; less_leaves(cons(u,v),cons(w,z)) >= less_leaves(concat(u,v),concat(w,z)) ; less_leaves(x,leaf) >= false ; Marked_concat(cons(u,v),y) >= Marked_concat(v,y) ; } + Disjunctions:{ { Marked_concat(cons(u,v),y) > Marked_concat(v,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: concat(leaf,y) >= y constraint: concat(cons(u,v),y) >= cons(u,concat(v,y)) constraint: less_leaves(leaf,cons(w,z)) >= true constraint: less_leaves(cons(u,v),cons(w,z)) >= less_leaves(concat(u,v), concat(w,z)) constraint: less_leaves(x,leaf) >= false constraint: Marked_concat(cons(u,v),y) >= Marked_concat(v,y) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] concat(leaf,y) -> y [2] concat(cons(u,v),y) -> cons(u,concat(v,y)) [3] less_leaves(x,leaf) -> false [4] less_leaves(leaf,cons(w,z)) -> true [5] less_leaves(cons(u,v),cons(w,z)) -> less_leaves(concat(u,v),concat(w,z)) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ concat ] (X0,X1) = 1*X0 + 1*X1 + 0; [ less_leaves ] (X0,X1) = 3 + 1*X1 + 0; [ cons ] (X0,X1) = 2 + 2*X0 + 1*X1 + 0; [ Marked_less_leaves ] (X0,X1) = 2*X0 + 0; [ leaf ] () = 3 + 0; [ true ] () = 0; [ false ] () = 2 + 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ concat ] (X0,X1) = 2*X0 + 2*X1 + 0; [ less_leaves ] (X0,X1) = 3 + 0; [ cons ] (X0,X1) = 2 + 1*X1 + 0; [ leaf ] () = 3 + 0; [ true ] () = 3 + 0; [ false ] () = 3 + 0; [ Marked_concat ] (X0,X1) = 3*X0 + 0; ]} ]} ]} Cime worked for 0.060086 seconds (real time) Cime Exit Status: 0