YES
Time: 1.188

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: 2
  interpretation:
             [1 4]     [8]
   [L](x0) = [0 1]x0 + [0],
   
             [1 4]     [0]
   [T](x0) = [1 4]x0 + [4],
   
           [3]
   [one] = [4],
   
                             [1]
   [pAC](x0, x1) = x0 + x1 + [0]
  orientation:
                      [4]         
   pAC(x,one()) = x + [4] >= x = x
   
              [2 0]    [1]         
   pAC(x,x) = [0 2]x + [0] >= x = x
   
                 [2 4]    [1]    [1 4]    [0]       
   pAC(T(x),x) = [1 5]x + [4] >= [1 4]x + [4] = T(x)
   
                    [1 4]    [5  20]    [17]    [1 4]    [2 8]    [2]                        
   T(pAC(x,T(y))) = [1 4]x + [5  20]y + [21] >= [1 4]x + [2 8]y + [9] = pAC(T(pAC(x,y)),T(y))
   
                    [1 4]    [5  20]    [25]    [1 4]    [2 8]    [18]                        
   L(pAC(x,T(y))) = [0 1]x + [1  4 ]y + [4 ] >= [0 1]x + [0 2]y + [0 ] = 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