YES
Time: 0.144

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: 1
  interpretation:
   [s](x0) = x0 + 12,
   
   [0] = 14,
   
   [h](x0) = x0 + 1,
   
   [L](x0) = 8x0 + 14,
   
   [maxxAC](x0, x1) = x0 + x1 + 4,
   
   [maxAC](x0, x1) = x0 + x1 + 1,
   
   [NAC](x0, x1) = x0 + x1 + 4
  orientation:
   h(L(x)) = 8x + 15 >= 14 = 0()
   
   h(NAC(x,y)) = x + y + 5 >= x + y + 3 = maxAC(h(x),h(y))
   
   maxAC(0(),x) = x + 15 >= x = x
   
   maxAC(x,0()) = x + 15 >= x = x
   
   maxAC(s(x),s(y)) = x + y + 25 >= x + y + 16 = s(maxxAC(x,y))
   
   maxxAC(0(),x) = x + 18 >= x = x
   
   maxxAC(x,0()) = x + 18 >= x = x
   
   maxxAC(s(x),s(y)) = x + y + 28 >= x + y + 13 = 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