- : unit = () h : heuristic = - : unit = () APPLY CRITERIA (Marked dependency pairs) TRS termination of: [1] D(t) -> 1 [2] D(constant) -> 0 [3] D(+(x,y)) -> +(D(x),D(y)) [4] D( *(x,y)) -> +( *(y,D(x)), *(x,D(y))) [5] D(-(x,y)) -> -(D(x),D(y)) 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: { D(t) >= 1 ; D(constant) >= 0 ; D(+(x,y)) >= +(D(x),D(y)) ; D( *(x,y)) >= +( *(y,D(x)), *(x,D(y))) ; D(-(x,y)) >= -(D(x),D(y)) ; Marked_D(+(x,y)) >= Marked_D(x) ; Marked_D(+(x,y)) >= Marked_D(y) ; Marked_D( *(x,y)) >= Marked_D(x) ; Marked_D( *(x,y)) >= Marked_D(y) ; Marked_D(-(x,y)) >= Marked_D(x) ; Marked_D(-(x,y)) >= Marked_D(y) ; } + Disjunctions:{ { Marked_D(+(x,y)) > Marked_D(x) ; } { Marked_D(+(x,y)) > Marked_D(y) ; } { Marked_D( *(x,y)) > Marked_D(x) ; } { Marked_D( *(x,y)) > Marked_D(y) ; } { Marked_D(-(x,y)) > Marked_D(x) ; } { Marked_D(-(x,y)) > Marked_D(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 === STOPING TIMER real === === STOPING TIMER virtual === No solution found for these parameters. Entering rpo_solver === TIMER virtual : 25.000000 === Search parameters: AFS type: 2 ; time limit: 25.. === STOPING TIMER virtual === === STOPING TIMER virtual === constraint: D(t) >= 1 constraint: D(constant) >= 0 constraint: D(+(x,y)) >= +(D(x),D(y)) constraint: D( *(x,y)) >= +( *(y,D(x)), *(x,D(y))) constraint: D(-(x,y)) >= -(D(x),D(y)) constraint: Marked_D(+(x,y)) >= Marked_D(x) constraint: Marked_D(+(x,y)) >= Marked_D(y) constraint: Marked_D( *(x,y)) >= Marked_D(x) constraint: Marked_D( *(x,y)) >= Marked_D(y) constraint: Marked_D(-(x,y)) >= Marked_D(x) constraint: Marked_D(-(x,y)) >= Marked_D(y) APPLY CRITERIA (Graph splitting) Found 0 components: SOLVED { TRS termination of: [1] D(t) -> 1 [2] D(constant) -> 0 [3] D(+(x,y)) -> +(D(x),D(y)) [4] D( *(x,y)) -> +( *(y,D(x)), *(x,D(y))) [5] D(-(x,y)) -> -(D(x),D(y)) , CRITERION: MDP [ { DP termination of: , CRITERION: SG [ { DP termination of: , CRITERION: ORD [ Solution found: RPO with AFS = AFS: and precedence: prec (All symbols are Lex.): { 1 < D ; D > 1 ; D > 0 ; D > + ; D > * ; D > - ; 0 < D ; + < D ; * < D ; - < D ; } ]} ]} ]} Cime worked for 0.051151 seconds (real time) Cime Exit Status: 0