MAYBE
Time: 1.342

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(x,NAC(y,z))) -> max(NAC(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(x,NAC(y,z))) -> max#(NAC(y,z))
   max#(NAC(x,NAC(y,z))) -> max#(NAC(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(x,NAC(y,z))) -> max(NAC(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(x,NAC(y,z))) -> max#(NAC(y,z))
    max#(NAC(x,NAC(y,z))) -> max#(NAC(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(x,NAC(y,z))) -> max(NAC(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)
   Open