- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] prime(0) -> false [2] prime(s(0)) -> false [3] prime(s(s(x))) -> prime1(s(s(x)),s(x)) [4] prime1(x,0) -> false [5] prime1(x,s(0)) -> true [6] prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y))) [7] divp(x,y) -> =(rem(x,y),0) Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 1 components: { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { prime(0) >= false ; prime(s(0)) >= false ; prime(s(s(x))) >= prime1(s(s(x)),s(x)) ; prime1(x,0) >= false ; prime1(x,s(0)) >= true ; prime1(x,s(s(y))) >= and(not(divp(s(s(y)),x)),prime1(x,s(y))) ; divp(x,y) >= =(rem(x,y),0) ; Marked_prime1(x,s(s(y))) >= Marked_prime1(x,s(y)) ; } + Disjunctions:{ { Marked_prime1(x,s(s(y))) > Marked_prime1(x,s(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: prime(0) >= false constraint: prime(s(0)) >= false constraint: prime(s(s(x))) >= prime1(s(s(x)),s(x)) constraint: prime1(x,0) >= false constraint: prime1(x,s(0)) >= true constraint: prime1(x,s(s(y))) >= and(not(divp(s(s(y)),x)),prime1(x,s(y))) constraint: divp(x,y) >= =(rem(x,y),0) constraint: Marked_prime1(x,s(s(y))) >= Marked_prime1(x,s(y)) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] prime(0) -> false [2] prime(s(0)) -> false [3] prime(s(s(x))) -> prime1(s(s(x)),s(x)) [4] prime1(x,0) -> false [5] prime1(x,s(0)) -> true [6] prime1(x,s(s(y))) -> and(not(divp(s(s(y)),x)),prime1(x,s(y))) [7] divp(x,y) -> =(rem(x,y),0) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ false ] () = 0; [ divp ] (X0,X1) = 0; [ prime1 ] (X0,X1) = 0; [ Marked_prime1 ] (X0,X1) = 3*X1 + 0; [ 0 ] () = 0; [ rem ] (X0,X1) = 3*X0 + 3*X1 + 0; [ and ] (X0,X1) = 0; [ prime ] (X0) = 2 + 0; [ = ] (X0,X1) = 0; [ true ] () = 0; [ s ] (X0) = 1 + 3*X0 + 0; [ not ] (X0) = 0; ]} ]} ]} Cime worked for 0.072296 seconds (real time) Cime Exit Status: 0