MAYBE
Time: 0.053

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:
 DP Processor:
  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)
  DPs:
   d#(+AC(s(x),y)) -> p#(s(x))
   d#(+AC(s(x),y)) -> d#(+AC(p(s(x)),y))
   p#(s(s(x))) -> p#(s(x))
  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)))
  S:
   +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6)
   +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7)
  AC-EDG Processor:
   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)
   DPs:
    d#(+AC(s(x),y)) -> p#(s(x))
    d#(+AC(s(x),y)) -> d#(+AC(p(s(x)),y))
    p#(s(s(x))) -> p#(s(x))
   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)))
   S:
    +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,x6)
    +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(x6,x7)
   Open