MAYBE
Time: 0.169

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:
  +AC(g(x),g(y)) -> g(+AC(g(a()),+AC(x,y)))

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:
   +{AC,#}(g(x),g(y)) -> +{AC,#}(x,y)
   +{AC,#}(g(x),g(y)) -> +{AC,#}(g(a()),+AC(x,y))
   +{AC,#}(x5,+AC(g(x),g(y))) -> +{AC,#}(x,y)
   +{AC,#}(x5,+AC(g(x),g(y))) -> +{AC,#}(g(a()),+AC(x,y))
   +{AC,#}(x5,+AC(g(x),g(y))) -> +{AC,#}(x5,g(+AC(g(a()),+AC(x,y))))
  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:
   +AC(g(x),g(y)) -> g(+AC(g(a()),+AC(x,y)))
  S:
   +{AC,#}(+AC(x6,x7),x8) -> +{AC,#}(x6,x7)
   +{AC,#}(x6,+AC(x7,x8)) -> +{AC,#}(x7,x8)
  Open