MAYBE
Time: 0.010

Problem:
 Equations:
  
 TRS:
  s(p(x)) -> x
  p(s(x)) -> x
  plusAC(0(),y) -> y
  plusAC(s(x),y) -> s(plusAC(x,y))
  plusAC(p(x),y) -> p(plusAC(x,y))
  plusAC(i(x),x) -> 0()
  plusAC(x,plusAC(i(x),y)) -> y
  i(0()) -> 0()
  i(s(x)) -> p(i(x))
  i(p(x)) -> s(i(x))
  i(i(x)) -> x
  i(plusAC(x,y)) -> plusAC(i(y),i(x))
  timesAC(0(),y) -> 0()
  timesAC(s(x),y) -> plusAC(timesAC(x,y),y)
  timesAC(p(x),y) -> plusAC(timesAC(x,y),i(y))

Proof:
 Open