MAYBE
Time: 0.024

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)
  sign(x) -> if_sign(x,S())
  if_sign(S(),x) -> x
  if_sign(0(x),y) -> if_sign(x,y)
  if_sign(1(x),y) -> if_sign(x,1(S()))
  if_sign(j(x),y) -> if_sign(x,j(S()))
  abs(x) -> if_abs(x,x,S())
  if_abs(0(x),y,z) -> if_abs(x,y,z)
  if_abs(1(x),y,z) -> if_abs(x,y,1(S()))
  if_abs(j(x),y,z) -> if_abs(x,y,j(S()))
  if_abs(S(),x,S()) -> S()
  if_abs(S(),x,1(S())) -> x
  if_abs(S(),x,j(S())) -> opp(x)
  min(x,y) -> if_min(minus(abs(y),abs(x)),x,y,S())
  min'(x,y) -> if_min(minus(abs(1(y)),abs(1(x))),x,y,S())
  min''(x,y) -> if_min(minus(abs(j(y)),abs(j(x))),x,y,S())
  if_min(0(x),y,z,u) -> if_min(x,y,z,u)
  if_min(1(x),y,z,u) -> if_min(x,y,z,1(S()))
  if_min(j(x),y,z,u) -> if_min(x,y,z,j(S()))
  if_min(S(),x,y,S()) -> x
  if_min(S(),x,y,1(S())) -> x
  if_min(S(),x,y,j(S())) -> y

Proof:
 Open