YES
Time: 1.168

Problem:
 Equations:
  NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
  NAC(x3,x4) -> NAC(x4,x3)
  maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5))
  maxAC(x3,x4) -> maxAC(x4,x3)
  maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5))
  maxxAC(x3,x4) -> maxxAC(x4,x3)
  NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
  NAC(x4,x3) -> NAC(x3,x4)
  maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5)
  maxAC(x4,x3) -> maxAC(x3,x4)
  maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5)
  maxxAC(x4,x3) -> maxxAC(x3,x4)
 TRS:
  h(L(x)) -> 0()
  h(NAC(x,y)) -> maxAC(h(x),h(y))
  maxAC(0(),x) -> x
  maxAC(x,0()) -> x
  maxAC(s(x),s(y)) -> s(maxxAC(x,y))
  maxxAC(0(),x) -> x
  maxxAC(x,0()) -> x
  maxxAC(s(x),s(y)) -> s(maxAC(x,y))

Proof:
 Matrix Interpretation Processor:
  dimension: 2
  interpretation:
                  [1]
   [s](x0) = x0 + [0],
   
         [2]
   [0] = [5],
   
             [1  13]     [1]
   [h](x0) = [1  12]x0 + [3],
   
             [1 0]     [2]
   [L](x0) = [0 0]x0 + [0],
   
                                [4]
   [maxxAC](x0, x1) = x0 + x1 + [0],
   
                               [4]
   [maxAC](x0, x1) = x0 + x1 + [0],
   
                             [4]
   [NAC](x0, x1) = x0 + x1 + [2]
  orientation:
             [1 0]    [3]    [2]      
   h(L(x)) = [1 0]x + [5] >= [5] = 0()
   
                 [1  13]    [1  13]    [31]    [1  13]    [1  13]    [6]                   
   h(NAC(x,y)) = [1  12]x + [1  12]y + [31] >= [1  12]x + [1  12]y + [6] = maxAC(h(x),h(y))
   
                      [6]         
   maxAC(0(),x) = x + [5] >= x = x
   
                      [6]         
   maxAC(x,0()) = x + [5] >= x = x
   
                              [6]            [5]                 
   maxAC(s(x),s(y)) = x + y + [0] >= x + y + [0] = s(maxxAC(x,y))
   
                       [6]         
   maxxAC(0(),x) = x + [5] >= x = x
   
                       [6]         
   maxxAC(x,0()) = x + [5] >= x = x
   
                               [6]            [5]                
   maxxAC(s(x),s(y)) = x + y + [0] >= x + y + [0] = s(maxAC(x,y))
  problem:
   Equations:
    NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
    NAC(x3,x4) -> NAC(x4,x3)
    maxAC(maxAC(x3,x4),x5) -> maxAC(x3,maxAC(x4,x5))
    maxAC(x3,x4) -> maxAC(x4,x3)
    maxxAC(maxxAC(x3,x4),x5) -> maxxAC(x3,maxxAC(x4,x5))
    maxxAC(x3,x4) -> maxxAC(x4,x3)
    NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
    NAC(x4,x3) -> NAC(x3,x4)
    maxAC(x3,maxAC(x4,x5)) -> maxAC(maxAC(x3,x4),x5)
    maxAC(x4,x3) -> maxAC(x3,x4)
    maxxAC(x3,maxxAC(x4,x5)) -> maxxAC(maxxAC(x3,x4),x5)
    maxxAC(x4,x3) -> maxxAC(x3,x4)
   TRS:
    
  Qed