YES
Time: 0.154

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:
  sum(L(x)) -> x
  sum(NAC(L(0()),L(y))) -> y
  sum(NAC(L(s(x)),L(y))) -> s(sum(NAC(L(x),L(y))))
  sum(NAC(L(x),NAC(y,z))) -> sum(NAC(L(x),L(sum(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:
   sum#(NAC(L(s(x)),L(y))) -> sum#(NAC(L(x),L(y)))
   sum#(NAC(L(x),NAC(y,z))) -> sum#(NAC(y,z))
   sum#(NAC(L(x),NAC(y,z))) -> sum#(NAC(L(x),L(sum(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:
   sum(L(x)) -> x
   sum(NAC(L(0()),L(y))) -> y
   sum(NAC(L(s(x)),L(y))) -> s(sum(NAC(L(x),L(y))))
   sum(NAC(L(x),NAC(y,z))) -> sum(NAC(L(x),L(sum(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:
    sum#(NAC(L(s(x)),L(y))) -> sum#(NAC(L(x),L(y)))
    sum#(NAC(L(x),NAC(y,z))) -> sum#(NAC(y,z))
    sum#(NAC(L(x),NAC(y,z))) -> sum#(NAC(L(x),L(sum(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:
    sum(L(x)) -> x
    sum(NAC(L(0()),L(y))) -> y
    sum(NAC(L(s(x)),L(y))) -> s(sum(NAC(L(x),L(y))))
    sum(NAC(L(x),NAC(y,z))) -> sum(NAC(L(x),L(sum(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:
     sum#(NAC(L(x),NAC(y,z))) -> sum#(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:
     sum(L(x)) -> x
     sum(NAC(L(0()),L(y))) -> y
     sum(NAC(L(s(x)),L(y))) -> s(sum(NAC(L(x),L(y))))
     sum(NAC(L(x),NAC(y,z))) -> sum(NAC(L(x),L(sum(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:
      sum#(NAC(L(x),NAC(y,z))) -> sum#(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:
      sum(L(x)) -> x
      sum(NAC(L(0()),L(y))) -> y
      sum(NAC(L(s(x)),L(y))) -> s(sum(NAC(L(x),L(y))))
      sum(NAC(L(x),NAC(y,z))) -> sum(NAC(L(x),L(sum(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:
       sum#(NAC(L(x),NAC(y,z))) -> sum#(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(sum#) = 0
       precedence:
        sum# > L ~ NAC
        weight function:
         [sum#](x0) = x0,
         
         [L](x0) = 1,
         
         [NAC](x0, x1) = x0 + x1
         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:
      sum#(NAC(L(s(x)),L(y))) -> sum#(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:
      sum(L(x)) -> x
      sum(NAC(L(0()),L(y))) -> y
      sum(NAC(L(s(x)),L(y))) -> s(sum(NAC(L(x),L(y))))
      sum(NAC(L(x),NAC(y,z))) -> sum(NAC(L(x),L(sum(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:
       sum#(NAC(L(s(x)),L(y))) -> sum#(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:
       sum(L(x)) -> x
       sum(NAC(L(0()),L(y))) -> y
       sum(NAC(L(s(x)),L(y))) -> s(sum(NAC(L(x),L(y))))
       sum(NAC(L(x),NAC(y,z))) -> sum(NAC(L(x),L(sum(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:
        sum#(NAC(L(s(x)),L(y))) -> sum#(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(sum#) = [0]
        precedence:
         sum# > s ~ L ~ NAC
         weight function:
          [sum#](x0) = 4x0,
          
          [s](x0) = 2x0 + 1,
          
          [L](x0) = 2x0 + 4,
          
          [NAC](x0, x1) = x0 + x1 + 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