YES
Time: 0.876

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: 2
  interpretation:
               [1 0]     [14]
   [one](x0) = [0 2]x0 + [2 ],
   
                [1 0]     [12]
   [zero](x0) = [0 2]x0 + [0 ],
   
             [1]
   [sharp] = [0],
   
                             
   [plusAC](x0, x1) = x0 + x1
  orientation:
                   [13]    [1]          
   zero(sharp()) = [0 ] >= [0] = sharp()
   
                           [1]         
   plusAC(x,sharp()) = x + [0] >= x = x
   
                             [1 0]    [1 0]    [24]    [1 0]    [1 0]    [12]                    
   plusAC(zero(x),zero(y)) = [0 2]x + [0 2]y + [0 ] >= [0 2]x + [0 2]y + [0 ] = zero(plusAC(x,y))
   
                            [1 0]    [1 0]    [26]    [1 0]    [1 0]    [14]                   
   plusAC(zero(x),one(y)) = [0 2]x + [0 2]y + [2 ] >= [0 2]x + [0 2]y + [2 ] = one(plusAC(x,y))
   
                           [1 0]    [1 0]    [28]    [1 0]    [1 0]    [27]                                         
   plusAC(one(x),one(y)) = [0 2]x + [0 2]y + [4 ] >= [0 2]x + [0 2]y + [4 ] = 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