MAYBE
Time: 0.009

Problem:
 Equations:
  +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)
 TRS:
  d(+AC(s(x),y)) -> s(d(+AC(p(s(x)),y)))
  p(s(s(x))) -> s(p(s(x)))

Proof:
 Open