- : 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)) [6] D(minus(x)) -> minus(D(x)) [7] D(div(x,y)) -> -(div(D(x),y),div( *(x,D(y)),pow(y,2))) [8] D(ln(x)) -> div(D(x),x) [9] D(pow(x,y)) -> +( *( *(y,pow(x,-(y,1))),D(x)), *( *(pow(x,y),ln(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)) ; D(minus(x)) >= minus(D(x)) ; D(div(x,y)) >= -(div(D(x),y),div( *(x,D(y)),pow(y,2))) ; D(pow(x,y)) >= +( *( *(y,pow(x,-(y,1))),D(x)), *( *(pow(x,y),ln(x)),D(y))) ; D(ln(x)) >= div(D(x),x) ; 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) ; Marked_D(minus(x)) >= Marked_D(x) ; Marked_D(div(x,y)) >= Marked_D(x) ; Marked_D(div(x,y)) >= Marked_D(y) ; Marked_D(pow(x,y)) >= Marked_D(x) ; Marked_D(pow(x,y)) >= Marked_D(y) ; Marked_D(ln(x)) >= Marked_D(x) ; } + 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) ; } { Marked_D(minus(x)) > Marked_D(x) ; } { Marked_D(div(x,y)) > Marked_D(x) ; } { Marked_D(div(x,y)) > Marked_D(y) ; } { Marked_D(pow(x,y)) > Marked_D(x) ; } { Marked_D(pow(x,y)) > Marked_D(y) ; } { Marked_D(ln(x)) > Marked_D(x) ; } } === 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: D(minus(x)) >= minus(D(x)) constraint: D(div(x,y)) >= -(div(D(x),y),div( *(x,D(y)),pow(y,2))) constraint: D(pow(x,y)) >= +( *( *(y,pow(x,-(y,1))),D(x)), *( *(pow(x,y),ln(x)),D(y))) constraint: D(ln(x)) >= div(D(x),x) 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) constraint: Marked_D(minus(x)) >= Marked_D(x) constraint: Marked_D(div(x,y)) >= Marked_D(x) constraint: Marked_D(div(x,y)) >= Marked_D(y) constraint: Marked_D(pow(x,y)) >= Marked_D(x) constraint: Marked_D(pow(x,y)) >= Marked_D(y) constraint: Marked_D(ln(x)) >= Marked_D(x) 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)) [6] D(minus(x)) -> minus(D(x)) [7] D(div(x,y)) -> -(div(D(x),y),div( *(x,D(y)),pow(y,2))) [8] D(ln(x)) -> div(D(x),x) [9] D(pow(x,y)) -> +( *( *(y,pow(x,-(y,1))),D(x)), *( *(pow(x,y),ln(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 > - ; D > minus ; D > div ; D > pow ; D > 2 ; D > ln ; 0 < D ; + < D ; * < D ; - < D ; minus < D ; div < D ; pow < D ; 2 < D ; ln < D ; } ]} ]} ]} Cime worked for 0.199747 seconds (real time) Cime Exit Status: 0