YES
Time: 1.648

Problem:
 Equations:
  pAC(pAC(x4,x5),x6) -> pAC(x4,pAC(x5,x6))
  pAC(x4,x5) -> pAC(x5,x4)
  pAC(x4,pAC(x5,x6)) -> pAC(pAC(x4,x5),x6)
  pAC(x5,x4) -> pAC(x4,x5)
 TRS:
  pAC(zero(),x) -> x
  pAC(i(x),x) -> zero()
  phi(zero(),y1) -> y1
  phi(y1,phi(y2,x)) -> phi(pAC(y1,y2),x)
  phi(g1(x),g2(y1)) -> phi(g2(y1),g1(x))
  g1(zero()) -> zero()
  g2(zero()) -> zero()
  g1(pAC(x,y)) -> pAC(g1(x),g1(y))
  g2(pAC(x,y)) -> pAC(g2(x),g2(y))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
              [2 0]     [1]
   [g2](x0) = [7 1]x0 + [1],
   
              [3 0]     [3]
   [g1](x0) = [1 0]x0 + [1],
   
                   [8 2]     [1 4]     [0]
   [phi](x0, x1) = [4 0]x0 + [0 4]x1 + [6],
   
             [4 0]     [1]
   [i](x0) = [0 0]x0 + [0],
   
            [1]
   [zero] = [0],
   
                             [2]
   [pAC](x0, x1) = x0 + x1 + [0]
  orientation:
                       [3]         
   pAC(zero(),x) = x + [0] >= x = x
   
                 [5 0]    [3]    [1]         
   pAC(i(x),x) = [0 1]x + [0] >= [0] = zero()
   
                    [1 4]     [8 ]           
   phi(zero(),y1) = [0 4]y1 + [10] >= y1 = y1
   
                       [1  20]    [8 2]     [24 2 ]     [24]    [1 4]    [8 2]     [8 2]     [16]                    
   phi(y1,phi(y2,x)) = [0  16]x + [4 0]y1 + [16 0 ]y2 + [30] >= [0 4]x + [4 0]y1 + [4 0]y2 + [14] = phi(pAC(y1,y2),x)
   
                       [26 0 ]    [30 4 ]     [31]    [7 0]    [30 2 ]     [17]                    
   phi(g1(x),g2(y1)) = [12 0 ]x + [28 4 ]y1 + [22] >= [4 0]x + [8  0 ]y1 + [14] = phi(g2(y1),g1(x))
   
                [6]    [1]         
   g1(zero()) = [2] >= [0] = zero()
   
                [3]    [1]         
   g2(zero()) = [8] >= [0] = zero()
   
                  [3 0]    [3 0]    [9]    [3 0]    [3 0]    [8]                   
   g1(pAC(x,y)) = [1 0]x + [1 0]y + [3] >= [1 0]x + [1 0]y + [2] = pAC(g1(x),g1(y))
   
                  [2 0]    [2 0]    [5 ]    [2 0]    [2 0]    [4]                   
   g2(pAC(x,y)) = [7 1]x + [7 1]y + [15] >= [7 1]x + [7 1]y + [2] = pAC(g2(x),g2(y))
  problem:
   Equations:
    pAC(pAC(x4,x5),x6) -> pAC(x4,pAC(x5,x6))
    pAC(x4,x5) -> pAC(x5,x4)
    pAC(x4,pAC(x5,x6)) -> pAC(pAC(x4,x5),x6)
    pAC(x5,x4) -> pAC(x4,x5)
   TRS:
    
  Qed