- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] minus(0,Y) -> 0 [2] minus(s(X),s(Y)) -> minus(X,Y) [3] geq(X,0) -> true [4] geq(0,s(Y)) -> false [5] geq(s(X),s(Y)) -> geq(X,Y) [6] div(0,s(Y)) -> 0 [7] div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) [8] if(true,X,Y) -> X [9] if(false,X,Y) -> Y Sub problem: guided: DP termination of: END GUIDED APPLY CRITERIA (Graph splitting) Found 3 components: { --> } { --> } { --> } APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { minus(0,Y) >= 0 ; minus(s(X),s(Y)) >= minus(X,Y) ; geq(0,s(Y)) >= false ; geq(s(X),s(Y)) >= geq(X,Y) ; geq(X,0) >= true ; div(0,s(Y)) >= 0 ; div(s(X),s(Y)) >= if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) ; if(true,X,Y) >= X ; if(false,X,Y) >= Y ; Marked_div(s(X),s(Y)) >= Marked_div(minus(X,Y),s(Y)) ; } + Disjunctions:{ { Marked_div(s(X),s(Y)) > Marked_div(minus(X,Y),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: minus(0,Y) >= 0 constraint: minus(s(X),s(Y)) >= minus(X,Y) constraint: geq(0,s(Y)) >= false constraint: geq(s(X),s(Y)) >= geq(X,Y) constraint: geq(X,0) >= true constraint: div(0,s(Y)) >= 0 constraint: div(s(X),s(Y)) >= if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) constraint: if(true,X,Y) >= X constraint: if(false,X,Y) >= Y constraint: Marked_div(s(X),s(Y)) >= Marked_div(minus(X,Y),s(Y)) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { minus(0,Y) >= 0 ; minus(s(X),s(Y)) >= minus(X,Y) ; geq(0,s(Y)) >= false ; geq(s(X),s(Y)) >= geq(X,Y) ; geq(X,0) >= true ; div(0,s(Y)) >= 0 ; div(s(X),s(Y)) >= if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) ; if(true,X,Y) >= X ; if(false,X,Y) >= Y ; Marked_geq(s(X),s(Y)) >= Marked_geq(X,Y) ; } + Disjunctions:{ { Marked_geq(s(X),s(Y)) > Marked_geq(X,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: minus(0,Y) >= 0 constraint: minus(s(X),s(Y)) >= minus(X,Y) constraint: geq(0,s(Y)) >= false constraint: geq(s(X),s(Y)) >= geq(X,Y) constraint: geq(X,0) >= true constraint: div(0,s(Y)) >= 0 constraint: div(s(X),s(Y)) >= if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) constraint: if(true,X,Y) >= X constraint: if(false,X,Y) >= Y constraint: Marked_geq(s(X),s(Y)) >= Marked_geq(X,Y) APPLY CRITERIA (Choosing graph) Trying to solve the following constraints: { minus(0,Y) >= 0 ; minus(s(X),s(Y)) >= minus(X,Y) ; geq(0,s(Y)) >= false ; geq(s(X),s(Y)) >= geq(X,Y) ; geq(X,0) >= true ; div(0,s(Y)) >= 0 ; div(s(X),s(Y)) >= if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) ; if(true,X,Y) >= X ; if(false,X,Y) >= Y ; Marked_minus(s(X),s(Y)) >= Marked_minus(X,Y) ; } + Disjunctions:{ { Marked_minus(s(X),s(Y)) > Marked_minus(X,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: minus(0,Y) >= 0 constraint: minus(s(X),s(Y)) >= minus(X,Y) constraint: geq(0,s(Y)) >= false constraint: geq(s(X),s(Y)) >= geq(X,Y) constraint: geq(X,0) >= true constraint: div(0,s(Y)) >= 0 constraint: div(s(X),s(Y)) >= if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) constraint: if(true,X,Y) >= X constraint: if(false,X,Y) >= Y constraint: Marked_minus(s(X),s(Y)) >= Marked_minus(X,Y) APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] minus(0,Y) -> 0 [2] minus(s(X),s(Y)) -> minus(X,Y) [3] geq(X,0) -> true [4] geq(0,s(Y)) -> false [5] geq(s(X),s(Y)) -> geq(X,Y) [6] div(0,s(Y)) -> 0 [7] div(s(X),s(Y)) -> if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) [8] if(true,X,Y) -> X [9] if(false,X,Y) -> Y , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ 0 ] () = 0; [ geq ] (X0,X1) = 0; [ s ] (X0) = 2 + 0; [ div ] (X0,X1) = 2*X0 + 0; [ minus ] (X0,X1) = 0; [ Marked_div ] (X0,X1) = 3*X0 + 0; [ false ] () = 0; [ true ] () = 0; [ if ] (X0,X1,X2) = 2 + 1*X1 + 1*X2 + 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ 0 ] () = 0; [ geq ] (X0,X1) = 0; [ s ] (X0) = 1 + 1*X0 + 0; [ Marked_geq ] (X0,X1) = 1*X1 + 0; [ div ] (X0,X1) = 1*X0 + 0; [ minus ] (X0,X1) = 1*X0 + 0; [ false ] () = 0; [ true ] () = 0; [ if ] (X0,X1,X2) = 1*X1 + 1*X2 + 0; ]} { DP termination of: , CRITERION: ORD [ Solution found: polynomial interpretation = [ 0 ] () = 0; [ geq ] (X0,X1) = 0; [ s ] (X0) = 1 + 3*X0 + 0; [ div ] (X0,X1) = 2*X0 + 0; [ minus ] (X0,X1) = 0; [ false ] () = 0; [ true ] () = 0; [ Marked_minus ] (X0,X1) = 1*X0 + 0; [ if ] (X0,X1,X2) = 2*X1 + 2*X2 + 0; ]} ]} ]} Cime worked for 0.141486 seconds (real time) Cime Exit Status: 0