- : unit = () - : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] p(m,n,s(r)) -> p(m,r,n) [2] p(m,s(n),0) -> p(0,n,m) [3] p(m,0,0) -> m Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> --> --> --> } APPLY CRITERIA (Subterm criterion) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { p(m,s(n),0) >= p(0,n,m) ; p(m,0,0) >= m ; p(m,n,s(r)) >= p(m,r,n) ; Marked_p(m,s(n),0) >= Marked_p(0,n,m) ; Marked_p(m,n,s(r)) >= Marked_p(m,r,n) ; } + Disjunctions:{ { Marked_p(m,s(n),0) > Marked_p(0,n,m) ; } { Marked_p(m,n,s(r)) > Marked_p(m,r,n) ; } } === 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: p(m,s(n),0) >= p(0,n,m) constraint: p(m,0,0) >= m constraint: p(m,n,s(r)) >= p(m,r,n) constraint: Marked_p(m,s(n),0) >= Marked_p(0,n,m) constraint: Marked_p(m,n,s(r)) >= Marked_p(m,r,n) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] p(m,n,s(r)) -> p(m,r,n) [2] p(m,s(n),0) -> p(0,n,m) [3] p(m,0,0) -> m , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ p ] (X0,X1,X2) = 2 + 2*X0 + 0; [ 0 ] () = 0; [ s ] (X0) = 2 + 2*X0 + 0; [ Marked_p ] (X0,X1,X2) = 2*X0 + 2*X1 + 2*X2 + 0; ]} ]} ]} Cime worked for 0.021579 seconds (real time) Cime Exit Status: 0