MAYBE
Time: 1.440

Problem:
 Equations:
  plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
  plusAC(x3,x4) -> plusAC(x4,x3)
  plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
  plusAC(x4,x3) -> plusAC(x3,x4)
 TRS:
  sum(x,y) -> S(int(x,y))
  S(nil()) -> 0()
  S(cons(x,xs)) -> plusAC(x,S(xs))
  plusAC(x,0()) -> x
  plusAC(x,s(y)) -> s(plusAC(x,y))
  int(0(),0()) -> cons(0(),nil())
  int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
  int(s(x),0()) -> nil()
  int(s(x),s(y)) -> intlist(int(x,y))
  intlist(nil()) -> nil()
  intlist(cons(x,y)) -> cons(s(x),intlist(y))

Proof:
 Open