YES
Time: 0.113

Problem:
 Equations:
  NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
  NAC(x3,x4) -> NAC(x4,x3)
  NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
  NAC(x4,x3) -> NAC(x3,x4)
 TRS:
  max(L(x)) -> x
  max(NAC(L(0()),L(y))) -> y
  max(NAC(L(s(x)),L(s(y)))) -> s(max(NAC(L(x),L(y))))
  max(NAC(L(x),NAC(y,z))) -> max(NAC(L(x),L(max(NAC(y,z)))))

Proof:
 DP Processor:
  Equations#:
   N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5))
   N{AC,#}(x3,x4) -> N{AC,#}(x4,x3)
   N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5)
   N{AC,#}(x4,x3) -> N{AC,#}(x3,x4)
  DPs:
   max#(NAC(L(s(x)),L(s(y)))) -> max#(NAC(L(x),L(y)))
   max#(NAC(L(x),NAC(y,z))) -> max#(NAC(y,z))
   max#(NAC(L(x),NAC(y,z))) -> max#(NAC(L(x),L(max(NAC(y,z)))))
  Equations:
   NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
   NAC(x3,x4) -> NAC(x4,x3)
   NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
   NAC(x4,x3) -> NAC(x3,x4)
  TRS:
   max(L(x)) -> x
   max(NAC(L(0()),L(y))) -> y
   max(NAC(L(s(x)),L(s(y)))) -> s(max(NAC(L(x),L(y))))
   max(NAC(L(x),NAC(y,z))) -> max(NAC(L(x),L(max(NAC(y,z)))))
  S:
   N{AC,#}(NAC(x6,x7),x8) -> N{AC,#}(x6,x7)
   N{AC,#}(x6,NAC(x7,x8)) -> N{AC,#}(x7,x8)
  AC-EDG Processor:
   Equations#:
    N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5))
    N{AC,#}(x3,x4) -> N{AC,#}(x4,x3)
    N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5)
    N{AC,#}(x4,x3) -> N{AC,#}(x3,x4)
   DPs:
    max#(NAC(L(s(x)),L(s(y)))) -> max#(NAC(L(x),L(y)))
    max#(NAC(L(x),NAC(y,z))) -> max#(NAC(y,z))
    max#(NAC(L(x),NAC(y,z))) -> max#(NAC(L(x),L(max(NAC(y,z)))))
   Equations:
    NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
    NAC(x3,x4) -> NAC(x4,x3)
    NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
    NAC(x4,x3) -> NAC(x3,x4)
   TRS:
    max(L(x)) -> x
    max(NAC(L(0()),L(y))) -> y
    max(NAC(L(s(x)),L(s(y)))) -> s(max(NAC(L(x),L(y))))
    max(NAC(L(x),NAC(y,z))) -> max(NAC(L(x),L(max(NAC(y,z)))))
   S:
    N{AC,#}(NAC(x6,x7),x8) -> N{AC,#}(x6,x7)
    N{AC,#}(x6,NAC(x7,x8)) -> N{AC,#}(x7,x8)
   SCC Processor:
    #sccs: 2
    #rules: 2
    #arcs: 5/9
    Equations#:
     N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5))
     N{AC,#}(x3,x4) -> N{AC,#}(x4,x3)
     N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5)
     N{AC,#}(x4,x3) -> N{AC,#}(x3,x4)
    DPs:
     max#(NAC(L(x),NAC(y,z))) -> max#(NAC(y,z))
    Equations:
     NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
     NAC(x3,x4) -> NAC(x4,x3)
     NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
     NAC(x4,x3) -> NAC(x3,x4)
    TRS:
     max(L(x)) -> x
     max(NAC(L(0()),L(y))) -> y
     max(NAC(L(s(x)),L(s(y)))) -> s(max(NAC(L(x),L(y))))
     max(NAC(L(x),NAC(y,z))) -> max(NAC(L(x),L(max(NAC(y,z)))))
    S:
     N{AC,#}(NAC(x6,x7),x8) -> N{AC,#}(x6,x7)
     N{AC,#}(x6,NAC(x7,x8)) -> N{AC,#}(x7,x8)
    AC-DP unlabeling:
     Equations#:
      NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
      NAC(x3,x4) -> NAC(x4,x3)
      NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
      NAC(x4,x3) -> NAC(x3,x4)
     DPs:
      max#(NAC(L(x),NAC(y,z))) -> max#(NAC(y,z))
     Equations:
      NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
      NAC(x3,x4) -> NAC(x4,x3)
      NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
      NAC(x4,x3) -> NAC(x3,x4)
     TRS:
      max(L(x)) -> x
      max(NAC(L(0()),L(y))) -> y
      max(NAC(L(s(x)),L(s(y)))) -> s(max(NAC(L(x),L(y))))
      max(NAC(L(x),NAC(y,z))) -> max(NAC(L(x),L(max(NAC(y,z)))))
     S:
      NAC(NAC(x6,x7),x8) -> NAC(x6,x7)
      NAC(x6,NAC(x7,x8)) -> NAC(x7,x8)
     Usable Rule Processor:
      Equations#:
       NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
       NAC(x3,x4) -> NAC(x4,x3)
       NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
       NAC(x4,x3) -> NAC(x3,x4)
      DPs:
       max#(NAC(L(x),NAC(y,z))) -> max#(NAC(y,z))
      Equations:
       NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
       NAC(x3,x4) -> NAC(x4,x3)
       NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
       NAC(x4,x3) -> NAC(x3,x4)
      TRS:
       
      S:
       NAC(NAC(x6,x7),x8) -> NAC(x6,x7)
       NAC(x6,NAC(x7,x8)) -> NAC(x7,x8)
      AC-KBO Processor:
       argument filtering:
        pi(NAC) = [0,1]
        pi(L) = []
        pi(max#) = 0
       precedence:
        max# ~ L ~ NAC
        weight function:
         w0 = 2
         w(L) = 6
         w(NAC) = 5
         w(max#) = 1
         usable rules:
          
         problem:
          Equations#:
           NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
           NAC(x3,x4) -> NAC(x4,x3)
           NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
           NAC(x4,x3) -> NAC(x3,x4)
          DPs:
           
          Equations:
           NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
           NAC(x3,x4) -> NAC(x4,x3)
           NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
           NAC(x4,x3) -> NAC(x3,x4)
          TRS:
           
          S:
           NAC(NAC(x6,x7),x8) -> NAC(x6,x7)
           NAC(x6,NAC(x7,x8)) -> NAC(x7,x8)
         Qed
     
     Equations#:
      N{AC,#}(NAC(x3,x4),x5) -> N{AC,#}(x3,NAC(x4,x5))
      N{AC,#}(x3,x4) -> N{AC,#}(x4,x3)
      N{AC,#}(x3,NAC(x4,x5)) -> N{AC,#}(NAC(x3,x4),x5)
      N{AC,#}(x4,x3) -> N{AC,#}(x3,x4)
     DPs:
      max#(NAC(L(s(x)),L(s(y)))) -> max#(NAC(L(x),L(y)))
     Equations:
      NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
      NAC(x3,x4) -> NAC(x4,x3)
      NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
      NAC(x4,x3) -> NAC(x3,x4)
     TRS:
      max(L(x)) -> x
      max(NAC(L(0()),L(y))) -> y
      max(NAC(L(s(x)),L(s(y)))) -> s(max(NAC(L(x),L(y))))
      max(NAC(L(x),NAC(y,z))) -> max(NAC(L(x),L(max(NAC(y,z)))))
     S:
      N{AC,#}(NAC(x6,x7),x8) -> N{AC,#}(x6,x7)
      N{AC,#}(x6,NAC(x7,x8)) -> N{AC,#}(x7,x8)
     AC-DP unlabeling:
      Equations#:
       NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
       NAC(x3,x4) -> NAC(x4,x3)
       NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
       NAC(x4,x3) -> NAC(x3,x4)
      DPs:
       max#(NAC(L(s(x)),L(s(y)))) -> max#(NAC(L(x),L(y)))
      Equations:
       NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
       NAC(x3,x4) -> NAC(x4,x3)
       NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
       NAC(x4,x3) -> NAC(x3,x4)
      TRS:
       max(L(x)) -> x
       max(NAC(L(0()),L(y))) -> y
       max(NAC(L(s(x)),L(s(y)))) -> s(max(NAC(L(x),L(y))))
       max(NAC(L(x),NAC(y,z))) -> max(NAC(L(x),L(max(NAC(y,z)))))
      S:
       NAC(NAC(x6,x7),x8) -> NAC(x6,x7)
       NAC(x6,NAC(x7,x8)) -> NAC(x7,x8)
      Usable Rule Processor:
       Equations#:
        NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
        NAC(x3,x4) -> NAC(x4,x3)
        NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
        NAC(x4,x3) -> NAC(x3,x4)
       DPs:
        max#(NAC(L(s(x)),L(s(y)))) -> max#(NAC(L(x),L(y)))
       Equations:
        NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
        NAC(x3,x4) -> NAC(x4,x3)
        NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
        NAC(x4,x3) -> NAC(x3,x4)
       TRS:
        
       S:
        NAC(NAC(x6,x7),x8) -> NAC(x6,x7)
        NAC(x6,NAC(x7,x8)) -> NAC(x7,x8)
       AC-KBO Processor:
        argument filtering:
         pi(NAC) = [0,1]
         pi(L) = 0
         pi(s) = [0]
         pi(max#) = 0
        precedence:
         L > max# ~ s ~ NAC
         weight function:
          w0 = 2
          w(NAC) = 6
          w(s) = 3
          w(max#) = w(L) = 2
          usable rules:
           
          problem:
           Equations#:
            NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
            NAC(x3,x4) -> NAC(x4,x3)
            NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
            NAC(x4,x3) -> NAC(x3,x4)
           DPs:
            
           Equations:
            NAC(NAC(x3,x4),x5) -> NAC(x3,NAC(x4,x5))
            NAC(x3,x4) -> NAC(x4,x3)
            NAC(x3,NAC(x4,x5)) -> NAC(NAC(x3,x4),x5)
            NAC(x4,x3) -> NAC(x3,x4)
           TRS:
            
           S:
            NAC(NAC(x6,x7),x8) -> NAC(x6,x7)
            NAC(x6,NAC(x7,x8)) -> NAC(x7,x8)
          Qed