YES
Time: 0.128

Problem:
 Equations:
  plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
  plusAC(x2,x3) -> plusAC(x3,x2)
  plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
  plusAC(x3,x2) -> plusAC(x2,x3)
 TRS:
  zero(sharp()) -> sharp()
  plusAC(x,sharp()) -> x
  plusAC(zero(x),zero(y)) -> zero(plusAC(x,y))
  plusAC(zero(x),one(y)) -> one(plusAC(x,y))
  plusAC(one(x),one(y)) -> zero(plusAC(x,plusAC(y,one(sharp()))))

Proof:
 Matrix Interpretation Processor:
  dimension: 1
  interpretation:
   [one](x0) = x0 + 11,
   
   [zero](x0) = x0 + 1,
   
   [sharp] = 4,
   
   [plusAC](x0, x1) = x0 + x1 + 4
  orientation:
   zero(sharp()) = 5 >= 4 = sharp()
   
   plusAC(x,sharp()) = x + 8 >= x = x
   
   plusAC(zero(x),zero(y)) = x + y + 6 >= x + y + 5 = zero(plusAC(x,y))
   
   plusAC(zero(x),one(y)) = x + y + 16 >= x + y + 15 = one(plusAC(x,y))
   
   plusAC(one(x),one(y)) = x + y + 26 >= x + y + 24 = zero(plusAC(x,plusAC(y,one(sharp()))))
  problem:
   Equations:
    plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
    plusAC(x2,x3) -> plusAC(x3,x2)
    plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
    plusAC(x3,x2) -> plusAC(x2,x3)
   TRS:
    
  Qed