YES
Time: 0.171

Problem:
 Equations:
  pAC(pAC(x2,x3),x4) -> pAC(x2,pAC(x3,x4))
  pAC(x2,x3) -> pAC(x3,x2)
  pAC(x2,pAC(x3,x4)) -> pAC(pAC(x2,x3),x4)
  pAC(x3,x2) -> pAC(x2,x3)
 TRS:
  pAC(x,one()) -> x
  pAC(x,x) -> x
  pAC(T(x),x) -> T(x)
  T(pAC(x,T(y))) -> pAC(T(pAC(x,y)),T(y))
  L(pAC(x,T(y))) -> pAC(L(pAC(x,y)),L(y))

Proof:
 Matrix Interpretation Processor:
  dimension: 1
  interpretation:
   [L](x0) = 3x0 + 3,
   
   [T](x0) = 4x0 + 3,
   
   [one] = 0,
   
   [pAC](x0, x1) = x0 + x1 + 2
  orientation:
   pAC(x,one()) = x + 2 >= x = x
   
   pAC(x,x) = 2x + 2 >= x = x
   
   pAC(T(x),x) = 5x + 5 >= 4x + 3 = T(x)
   
   T(pAC(x,T(y))) = 4x + 16y + 23 >= 4x + 8y + 16 = pAC(T(pAC(x,y)),T(y))
   
   L(pAC(x,T(y))) = 3x + 12y + 18 >= 3x + 6y + 14 = pAC(L(pAC(x,y)),L(y))
  problem:
   Equations:
    pAC(pAC(x2,x3),x4) -> pAC(x2,pAC(x3,x4))
    pAC(x2,x3) -> pAC(x3,x2)
    pAC(x2,pAC(x3,x4)) -> pAC(pAC(x2,x3),x4)
    pAC(x3,x2) -> pAC(x2,x3)
   TRS:
    
  Qed