MAYBE
Time: 1.928

Problem:
 Equations:
  plusAC(plusAC(x3,x4),x5) -> plusAC(x3,plusAC(x4,x5))
  plusAC(x3,x4) -> plusAC(x4,x3)
  timesAC(timesAC(x3,x4),x5) -> timesAC(x3,timesAC(x4,x5))
  timesAC(x3,x4) -> timesAC(x4,x3)
  plusAC(x3,plusAC(x4,x5)) -> plusAC(plusAC(x3,x4),x5)
  plusAC(x4,x3) -> plusAC(x3,x4)
  timesAC(x3,timesAC(x4,x5)) -> timesAC(timesAC(x3,x4),x5)
  timesAC(x4,x3) -> timesAC(x3,x4)
 TRS:
  zero(S()) -> S()
  plusAC(x,S()) -> x
  plusAC(zero(x),zero(y)) -> zero(plusAC(x,y))
  plusAC(zero(x),un(y)) -> un(plusAC(x,y))
  plusAC(un(x),un(y)) -> zero(plusAC(x,plusAC(y,un(S()))))
  timesAC(x,S()) -> S()
  timesAC(x,timesAC(S(),z)) -> timesAC(S(),z)
  timesAC(x,zero(y)) -> zero(timesAC(x,y))
  timesAC(x,timesAC(zero(y),z)) -> timesAC(zero(timesAC(x,y)),z)
  timesAC(x,un(y)) -> plusAC(x,zero(timesAC(x,y)))
  timesAC(x,timesAC(un(y),z)) -> timesAC(plusAC(x,zero(timesAC(x,y))),z)

Proof:
 Open