- : unit = ()
- : unit = ()
h : heuristic = <heuristic>
- : unit = ()
APPLY CRITERIA (Marked dependency pairs)

TRS termination of:
[1] dx(X) -> one
[2] dx(a) -> zero
[3] dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
[4] dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
[5] dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
[6] dx(neg(ALPHA)) -> neg(dx(ALPHA))
[7] dx(div(ALPHA,BETA)) ->
 minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two))))
[8] dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
[9] dx(exp(ALPHA,BETA)) ->
 plus(times(BETA,times(exp(ALPHA,minus(BETA,one)),dx(ALPHA))),
  times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))


Sub problem: 
guided: 

DP termination of:
<Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
<Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
<Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
 
END GUIDED
APPLY CRITERIA (Graph splitting)
Found 1 components:

{  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
      --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
  <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)> 
     --> <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
}
APPLY CRITERIA (Subterm criterion)

ST: Marked_dx -> 1

APPLY CRITERIA (Graph splitting)
Found 0 components:
SOLVED
{
 
TRS termination of:
[1] dx(X) -> one
[2] dx(a) -> zero
[3] dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
[4] dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
[5] dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
[6] dx(neg(ALPHA)) -> neg(dx(ALPHA))
[7] dx(div(ALPHA,BETA)) ->
 minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two))))
[8] dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
[9] dx(exp(ALPHA,BETA)) ->
 plus(times(BETA,times(exp(ALPHA,minus(BETA,one)),dx(ALPHA))),
  times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
 ,
 CRITERION: MDP
 [ {
      
     DP termination of:
     <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
<Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
<Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
 ,
 CRITERION: SG
 [ {
      
     DP termination of:
     <Marked_dx(plus(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(plus(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(times(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(times(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(minus(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(minus(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(neg(ALPHA)) , Marked_dx(ALPHA)>
<Marked_dx(div(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(div(ALPHA,BETA)) , Marked_dx(BETA)>
<Marked_dx(ln(ALPHA)) , Marked_dx(ALPHA)>
<Marked_dx(exp(ALPHA,BETA)) , Marked_dx(ALPHA)>
<Marked_dx(exp(ALPHA,BETA)) , Marked_dx(BETA)>
 ,
 CRITERION: ST
 [ {
      
     DP termination of:
      ,
      CRITERION: SG
      [  ]} 
      ]} 
 ]} 
 ]} 

Cime worked for 0.015247 seconds (real time)
Cime Exit Status: 0