MAYBE
Time: 0.014

Problem:
 Equations:
  
 TRS:
  zero(0()) -> 0()
  plusAC(x,0()) -> x
  plusAC(zero(x),zero(y)) -> zero(plusAC(x,y))
  plusAC(zero(x),un(y)) -> un(plusAC(x,y))
  plusAC(zero(x),j(y)) -> j(plusAC(x,y))
  plusAC(un(x),j(y)) -> zero(plusAC(x,y))
  plusAC(un(x),un(y)) -> j(plusAC(x,plusAC(y,un(0()))))
  plusAC(j(x),j(y)) -> un(plusAC(x,plusAC(y,j(0()))))
  minus(x,y) -> plusAC(x,neg(y))
  neg(0()) -> 0()
  neg(zero(x)) -> zero(neg(x))
  neg(un(x)) -> j(neg(x))
  neg(j(x)) -> un(neg(x))
  timesAC(x,0()) -> 0()
  timesAC(x,timesAC(0(),z)) -> timesAC(0(),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)
  timesAC(x,j(y)) -> plusAC(zero(timesAC(x,y)),neg(x))
  timesAC(x,timesAC(j(y),z)) -> timesAC(plusAC(zero(timesAC(x,y)),neg(x)),z)

Proof:
 Open