- : unit = () - : 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] lessleaves(X,leaf) -> false [4] lessleaves(leaf,cons(W,Z)) -> true [5] lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(concat(U,V),concat(W,Z)) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 2 components: { --> } { --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { concat(leaf,Y) >= Y ; concat(cons(U,V),Y) >= cons(U,concat(V,Y)) ; lessleaves(leaf,cons(W,Z)) >= true ; lessleaves(cons(U,V),cons(W,Z)) >= lessleaves(concat(U,V),concat(W,Z)) ; lessleaves(X,leaf) >= false ; Marked_lessleaves(cons(U,V),cons(W,Z)) >= Marked_lessleaves(concat(U,V), concat(W,Z)) ; } + Disjunctions:{ { Marked_lessleaves(cons(U,V),cons(W,Z)) > Marked_lessleaves(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: lessleaves(leaf,cons(W,Z)) >= true constraint: lessleaves(cons(U,V),cons(W,Z)) >= lessleaves(concat(U,V), concat(W,Z)) constraint: lessleaves(X,leaf) >= false constraint: Marked_lessleaves(cons(U,V),cons(W,Z)) >= Marked_lessleaves( concat(U,V),concat(W,Z)) APPLY CRITERIA (Subterm criterion) ST: Marked_concat -> 1 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] lessleaves(X,leaf) -> false [4] lessleaves(leaf,cons(W,Z)) -> true [5] lessleaves(cons(U,V),cons(W,Z)) -> lessleaves(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; [ lessleaves ] (X0,X1) = 3 + 1*X1 + 0; [ cons ] (X0,X1) = 2 + 2*X0 + 1*X1 + 0; [ Marked_lessleaves ] (X0,X1) = 2*X0 + 0; [ leaf ] () = 3 + 0; [ true ] () = 0; [ false ] () = 2 + 0; ]} { DP termination of: , CRITERION: ST [ { DP termination of: , CRITERION: SG [ ]} ]} ]} ]} Cime worked for 0.039917 seconds (real time) Cime Exit Status: 0