MAYBE
Time: 0.016

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:
 Open