- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] f(j(x,y),y) -> g(f(x,k(y))) [2] f(x,h1(y,z)) -> h2(0,x,h1(y,z)) [3] g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) [4] h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) [5] i(f(x,h(y))) -> y [6] i(h2(s(x),y,h1(x,z))) -> z [7] k(h(x)) -> h1(0,x) [8] k(h1(x,y)) -> h1(s(x),y) 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: { g(h2(x,y,h1(z,u))) >= h2(s(x),y,h1(z,u)) ; f(j(x,y),y) >= g(f(x,k(y))) ; f(x,h1(y,z)) >= h2(0,x,h1(y,z)) ; k(h1(x,y)) >= h1(s(x),y) ; k(h(x)) >= h1(0,x) ; h2(x,j(y,h1(z,u)),h1(z,u)) >= h2(s(x),y,h1(s(z),u)) ; i(f(x,h(y))) >= y ; i(h2(s(x),y,h1(x,z))) >= z ; Marked_f(j(x,y),y) >= Marked_f(x,k(y)) ; } + Disjunctions:{ { Marked_f(j(x,y),y) > Marked_f(x,k(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: g(h2(x,y,h1(z,u))) >= h2(s(x),y,h1(z,u)) constraint: f(j(x,y),y) >= g(f(x,k(y))) constraint: f(x,h1(y,z)) >= h2(0,x,h1(y,z)) constraint: k(h1(x,y)) >= h1(s(x),y) constraint: k(h(x)) >= h1(0,x) constraint: h2(x,j(y,h1(z,u)),h1(z,u)) >= h2(s(x),y,h1(s(z),u)) constraint: i(f(x,h(y))) >= y constraint: i(h2(s(x),y,h1(x,z))) >= z constraint: Marked_f(j(x,y),y) >= Marked_f(x,k(y)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { g(h2(x,y,h1(z,u))) >= h2(s(x),y,h1(z,u)) ; f(j(x,y),y) >= g(f(x,k(y))) ; f(x,h1(y,z)) >= h2(0,x,h1(y,z)) ; k(h1(x,y)) >= h1(s(x),y) ; k(h(x)) >= h1(0,x) ; h2(x,j(y,h1(z,u)),h1(z,u)) >= h2(s(x),y,h1(s(z),u)) ; i(f(x,h(y))) >= y ; i(h2(s(x),y,h1(x,z))) >= z ; Marked_h2(x,j(y,h1(z,u)),h1(z,u)) >= Marked_h2(s(x),y,h1(s(z),u)) ; } + Disjunctions:{ { Marked_h2(x,j(y,h1(z,u)),h1(z,u)) > Marked_h2(s(x),y,h1(s(z),u)) ; } } === 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: g(h2(x,y,h1(z,u))) >= h2(s(x),y,h1(z,u)) constraint: f(j(x,y),y) >= g(f(x,k(y))) constraint: f(x,h1(y,z)) >= h2(0,x,h1(y,z)) constraint: k(h1(x,y)) >= h1(s(x),y) constraint: k(h(x)) >= h1(0,x) constraint: h2(x,j(y,h1(z,u)),h1(z,u)) >= h2(s(x),y,h1(s(z),u)) constraint: i(f(x,h(y))) >= y constraint: i(h2(s(x),y,h1(x,z))) >= z constraint: Marked_h2(x,j(y,h1(z,u)),h1(z,u)) >= Marked_h2(s(x),y,h1(s(z),u)) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] f(j(x,y),y) -> g(f(x,k(y))) [2] f(x,h1(y,z)) -> h2(0,x,h1(y,z)) [3] g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u)) [4] h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u)) [5] i(f(x,h(y))) -> y [6] i(h2(s(x),y,h1(x,z))) -> z [7] k(h(x)) -> h1(0,x) [8] k(h1(x,y)) -> h1(s(x),y) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ g ] (X0) = 3 + 2*X0 + 0; [ i ] (X0) = 2 + 1*X0 + 0; [ h2 ] (X0,X1,X2) = 3 + 1*X0 + 2*X2 + 0; [ k ] (X0) = 2*X0 + 0; [ h1 ] (X0,X1) = 2 + 2*X0 + 1*X1 + 0; [ Marked_f ] (X0,X1) = 2*X0 + 0; [ f ] (X0,X1) = 3 + 2*X0 + 2*X1 + 0; [ h ] (X0) = 2 + 2*X0 + 0; [ 0 ] () = 0; [ j ] (X0,X1) = 3 + 3*X0 + 3*X1 + 0; [ s ] (X0) = 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ g ] (X0) = 2 + 3*X0 + 0; [ i ] (X0) = 2 + 3*X0 + 0; [ h2 ] (X0,X1,X2) = 1*X0 + 3*X2 + 0; [ Marked_h2 ] (X0,X1,X2) = 2*X1 + 3*X2 + 0; [ k ] (X0) = 1*X0 + 0; [ h1 ] (X0,X1) = 2*X0 + 1*X1 + 0; [ f ] (X0,X1) = 3*X0 + 3*X1 + 0; [ h ] (X0) = 2 + 1*X0 + 0; [ 0 ] () = 0; [ j ] (X0,X1) = 3 + 3*X0 + 3*X1 + 0; [ s ] (X0) = 0; ]} ]} ]} Cime worked for 0.116732 seconds (real time) Cime Exit Status: 0