MAYBE
Time: 7.032

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