MAYBE
Time: 0.011

Problem:
 Equations:
  
 TRS:
  dx(X()) -> 1()
  dx(0()) -> 0()
  dx(1()) -> 0()
  dx(a()) -> 0()
  dx(+AC(f,g)) -> +AC(dx(f),dx(g))
  dx(*AC(f,g)) -> +AC(*AC(dx(f),g),*AC(dx(g),f))
  dx(-(f,g)) -> -(dx(f),dx(g))
  dx(neg(f)) -> neg(dx(f))
  dx(/(f,g)) -> -(/(dx(f),g),/(*AC(dx(g),f),exp(g,2())))
  dx(ln(f)) -> /(dx(f),f)
  dx(exp(f,g)) -> +AC(*AC(dx(f),*AC(exp(f,-(g,1())),g)),*AC(dx(g),*AC(exp(f,g),ln(f))))

Proof:
 Open