MAYBE
Time: 0.010

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