MAYBE
Time: 0.009

Problem:
 Equations:
  
 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