YES
Time: 0.016

Problem:
 Equations:
  plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
  plusAC(x2,x3) -> plusAC(x3,x2)
  timesAC(timesAC(x2,x3),x4) -> timesAC(x2,timesAC(x3,x4))
  timesAC(x2,x3) -> timesAC(x3,x2)
  plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
  plusAC(x3,x2) -> plusAC(x2,x3)
  timesAC(x2,timesAC(x3,x4)) -> timesAC(timesAC(x2,x3),x4)
  timesAC(x3,x2) -> timesAC(x2,x3)
 TRS:
  s(p(x)) -> x
  p(s(x)) -> x
  plusAC(0(),y) -> y
  plusAC(s(x),y) -> s(plusAC(x,y))
  plusAC(p(x),y) -> p(plusAC(x,y))
  plusAC(i(x),x) -> 0()
  plusAC(x,plusAC(i(x),y)) -> y
  i(0()) -> 0()
  i(s(x)) -> p(i(x))
  i(p(x)) -> s(i(x))
  i(i(x)) -> x
  i(plusAC(x,y)) -> plusAC(i(y),i(x))
  timesAC(0(),y) -> 0()
  timesAC(s(x),y) -> plusAC(timesAC(x,y),y)
  timesAC(p(x),y) -> plusAC(timesAC(x,y),i(y))

Proof:
 AC-RPO Processor:
  precedence:
   timesAC > i > plusAC > 0 > p > s
  status:
   
  problem:
   Equations:
    plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
    plusAC(x2,x3) -> plusAC(x3,x2)
    timesAC(timesAC(x2,x3),x4) -> timesAC(x2,timesAC(x3,x4))
    timesAC(x2,x3) -> timesAC(x3,x2)
    plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
    plusAC(x3,x2) -> plusAC(x2,x3)
    timesAC(x2,timesAC(x3,x4)) -> timesAC(timesAC(x2,x3),x4)
    timesAC(x3,x2) -> timesAC(x2,x3)
   TRS:
    
  Qed