MAYBE
Time: 0.619

Problem:
 Equations:
  
 TRS:
  0(S()) -> S()
  plusAC(S(),x) -> x
  plusAC(0(x),0(y)) -> 0(plusAC(x,y))
  plusAC(0(x),1(y)) -> 1(plusAC(x,y))
  plusAC(0(x),j(y)) -> j(plusAC(x,y))
  plusAC(1(x),1(y)) -> j(plusAC(1(S()),plusAC(x,y)))
  plusAC(j(x),j(y)) -> 1(plusAC(j(S()),plusAC(x,y)))
  plusAC(1(x),j(y)) -> 0(plusAC(x,y))
  opp(S()) -> S()
  opp(0(x)) -> 0(opp(x))
  opp(1(x)) -> j(opp(x))
  opp(j(x)) -> 1(opp(x))
  minus(x,y) -> plusAC(opp(y),x)
  timesAC(S(),x) -> S()
  timesAC(0(x),y) -> 0(timesAC(x,y))
  timesAC(1(x),y) -> plusAC(0(timesAC(x,y)),y)
  timesAC(j(x),y) -> minus(0(timesAC(x,y)),y)

Proof:
 Open