MAYBE
Time: 3.137

Problem:
 Equations:
  +AC(+AC(x2,x3),x4) -> +AC(x2,+AC(x3,x4))
  +AC(x2,x3) -> +AC(x3,x2)
  *AC(*AC(x2,x3),x4) -> *AC(x2,*AC(x3,x4))
  *AC(x2,x3) -> *AC(x3,x2)
  +AC(x2,+AC(x3,x4)) -> +AC(+AC(x2,x3),x4)
  +AC(x3,x2) -> +AC(x2,x3)
  *AC(x2,*AC(x3,x4)) -> *AC(*AC(x2,x3),x4)
  *AC(x3,x2) -> *AC(x2,x3)
 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