MAYBE
Time: 9.360

Problem:
 Equations:
  +AC(+AC(x5,x6),x7) -> +AC(x5,+AC(x6,x7))
  +AC(x5,x6) -> +AC(x6,x5)
  *AC(*AC(x5,x6),x7) -> *AC(x5,*AC(x6,x7))
  *AC(x5,x6) -> *AC(x6,x5)
  +AC(x5,+AC(x6,x7)) -> +AC(+AC(x5,x6),x7)
  +AC(x6,x5) -> +AC(x5,x6)
  *AC(x5,*AC(x6,x7)) -> *AC(*AC(x5,x6),x7)
  *AC(x6,x5) -> *AC(x5,x6)
 TRS:
  0(#()) -> #()
  +AC(#(),x) -> x
  +AC(0(x),0(y)) -> 0(+AC(x,y))
  +AC(0(x),1(y)) -> 1(+AC(x,y))
  +AC(0(x),j(y)) -> j(+AC(x,y))
  +AC(1(x),1(y)) -> j(+AC(1(#()),+AC(x,y)))
  +AC(j(x),j(y)) -> 1(+AC(j(#()),+AC(x,y)))
  +AC(1(x),j(y)) -> 0(+AC(x,y))
  opp(#()) -> #()
  opp(0(x)) -> 0(opp(x))
  opp(1(x)) -> j(opp(x))
  opp(j(x)) -> 1(opp(x))
  -(x,y) -> +AC(opp(y),x)
  *AC(#(),x) -> #()
  *AC(0(x),y) -> 0(*AC(x,y))
  *AC(1(x),y) -> +AC(0(*AC(x,y)),y)
  *AC(j(x),y) -> -(0(*AC(x,y)),y)
  abs(x) -> test_abs_pos(x,x)
  test_abs_pos(#(),x) -> x
  test_abs_pos(0(x),y) -> test_abs_pos(x,y)
  test_abs_pos(1(x),y) -> test_abs_pos(x,y)
  test_abs_pos(j(x),y) -> test_abs_neg(x,y)
  test_abs_neg(#(),x) -> opp(x)
  test_abs_neg(0(x),y) -> test_abs_neg(x,y)
  test_abs_neg(1(x),y) -> test_abs_pos(x,y)
  test_abs_neg(j(x),y) -> test_abs_neg(x,y)
  signe(#()) -> #()
  signe(0(x)) -> signe(x)
  signe(1(x)) -> test_signe_pos(x)
  signe(j(x)) -> test_signe_neg(x)
  test_signe_pos(#()) -> 1(#())
  test_signe_pos(0(x)) -> test_signe_pos(x)
  test_signe_pos(1(x)) -> test_signe_pos(x)
  test_signe_pos(j(x)) -> test_signe_neg(x)
  test_signe_neg(#()) -> j(#())
  test_signe_neg(0(x)) -> test_signe_neg(x)
  test_signe_neg(1(x)) -> test_signe_pos(x)
  test_signe_neg(j(x)) -> test_signe_neg(x)
  min(x,y) -> test_min_pos(-(abs(y),abs(x)),x,y)
  min'(x,y) -> test_min_pos(-(abs(1(y)),abs(1(x))),x,y)
  min''(x,y) -> test_min_pos(-(abs(j(y)),abs(j(x))),x,y)
  test_min_pos(#(),x,y) -> x
  test_min_pos(0(x),y,z) -> test_min_pos(x,y,z)
  test_min_pos(1(x),y,z) -> test_min_pos(x,y,z)
  test_min_pos(j(x),y,z) -> test_min_neg(x,y,z)
  test_min_neg(#(),x,y) -> y
  test_min_neg(0(x),y,z) -> test_min_neg(x,y,z)
  test_min_neg(1(x),y,z) -> test_min_pos(x,y,z)
  test_min_neg(j(x),y,z) -> test_min_neg(x,y,z)
  f(#(),x) -> #()
  f(x,#()) -> signe(x)
  f(0(x),0(y)) -> f(x,y)
  f(0(x),1(y)) -> 0(f(x,1(y)))
  f(0(x),j(y)) -> 0(f(x,j(y)))
  f(1(x),0(y)) -> f(1(x),y)
  f(1(x),1(y)) -> +AC(0(f(-(x,min'(x,y)),1(y))),f(min(1(x),1(y)),-(x,y)))
  f(1(x),j(y)) -> +AC(0(f(+AC(min''(opp(x),y),x),j(y))),f(min(1(x),1(opp(y))),+AC(x,y)))
  f(j(x),0(y)) -> f(j(x),y)
  f(j(x),1(y)) -> +AC(0(f(+AC(min'(opp(x),y),x),1(y))),f(min(j(x),j(opp(y))),+AC(x,y)))
  f(j(x),j(y)) -> +AC(0(f(-(x,min''(x,y)),j(y))),f(min(j(x),j(y)),-(x,y)))
  rat(x,y) -> irred(*AC(signe(y),f(x,y)),*AC(signe(y),f(y,x)))
  +_QC(irred(x,y),irred(u,v)) -> irred(+AC(*AC(x,v),*AC(y,u)),*AC(y,v))
  *_QC(irred(x,y),irred(u,v)) -> rat(*AC(x,u),*AC(y,v))

Proof:
 DP Processor:
  Equations#:
   +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,+AC(x6,x7))
   +{AC,#}(x5,x6) -> +{AC,#}(x6,x5)
   *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,*AC(x6,x7))
   *{AC,#}(x5,x6) -> *{AC,#}(x6,x5)
   +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(+AC(x5,x6),x7)
   +{AC,#}(x6,x5) -> +{AC,#}(x5,x6)
   *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(*AC(x5,x6),x7)
   *{AC,#}(x6,x5) -> *{AC,#}(x5,x6)
  DPs:
   +{AC,#}(0(x),0(y)) -> +{AC,#}(x,y)
   +{AC,#}(0(x),0(y)) -> 0#(+AC(x,y))
   +{AC,#}(0(x),1(y)) -> +{AC,#}(x,y)
   +{AC,#}(0(x),j(y)) -> +{AC,#}(x,y)
   +{AC,#}(1(x),1(y)) -> +{AC,#}(x,y)
   +{AC,#}(1(x),1(y)) -> +{AC,#}(1(#()),+AC(x,y))
   +{AC,#}(j(x),j(y)) -> +{AC,#}(x,y)
   +{AC,#}(j(x),j(y)) -> +{AC,#}(j(#()),+AC(x,y))
   +{AC,#}(1(x),j(y)) -> +{AC,#}(x,y)
   +{AC,#}(1(x),j(y)) -> 0#(+AC(x,y))
   opp#(0(x)) -> opp#(x)
   opp#(0(x)) -> 0#(opp(x))
   opp#(1(x)) -> opp#(x)
   opp#(j(x)) -> opp#(x)
   -#(x,y) -> opp#(y)
   -#(x,y) -> +{AC,#}(opp(y),x)
   *{AC,#}(0(x),y) -> *{AC,#}(x,y)
   *{AC,#}(0(x),y) -> 0#(*AC(x,y))
   *{AC,#}(1(x),y) -> *{AC,#}(x,y)
   *{AC,#}(1(x),y) -> 0#(*AC(x,y))
   *{AC,#}(1(x),y) -> +{AC,#}(0(*AC(x,y)),y)
   *{AC,#}(j(x),y) -> *{AC,#}(x,y)
   *{AC,#}(j(x),y) -> 0#(*AC(x,y))
   *{AC,#}(j(x),y) -> -#(0(*AC(x,y)),y)
   abs#(x) -> test_abs_pos#(x,x)
   test_abs_pos#(0(x),y) -> test_abs_pos#(x,y)
   test_abs_pos#(1(x),y) -> test_abs_pos#(x,y)
   test_abs_pos#(j(x),y) -> test_abs_neg#(x,y)
   test_abs_neg#(#(),x) -> opp#(x)
   test_abs_neg#(0(x),y) -> test_abs_neg#(x,y)
   test_abs_neg#(1(x),y) -> test_abs_pos#(x,y)
   test_abs_neg#(j(x),y) -> test_abs_neg#(x,y)
   signe#(0(x)) -> signe#(x)
   signe#(1(x)) -> test_signe_pos#(x)
   signe#(j(x)) -> test_signe_neg#(x)
   test_signe_pos#(0(x)) -> test_signe_pos#(x)
   test_signe_pos#(1(x)) -> test_signe_pos#(x)
   test_signe_pos#(j(x)) -> test_signe_neg#(x)
   test_signe_neg#(0(x)) -> test_signe_neg#(x)
   test_signe_neg#(1(x)) -> test_signe_pos#(x)
   test_signe_neg#(j(x)) -> test_signe_neg#(x)
   min#(x,y) -> abs#(x)
   min#(x,y) -> abs#(y)
   min#(x,y) -> -#(abs(y),abs(x))
   min#(x,y) -> test_min_pos#(-(abs(y),abs(x)),x,y)
   min'#(x,y) -> abs#(1(x))
   min'#(x,y) -> abs#(1(y))
   min'#(x,y) -> -#(abs(1(y)),abs(1(x)))
   min'#(x,y) -> test_min_pos#(-(abs(1(y)),abs(1(x))),x,y)
   min''#(x,y) -> abs#(j(x))
   min''#(x,y) -> abs#(j(y))
   min''#(x,y) -> -#(abs(j(y)),abs(j(x)))
   min''#(x,y) -> test_min_pos#(-(abs(j(y)),abs(j(x))),x,y)
   test_min_pos#(0(x),y,z) -> test_min_pos#(x,y,z)
   test_min_pos#(1(x),y,z) -> test_min_pos#(x,y,z)
   test_min_pos#(j(x),y,z) -> test_min_neg#(x,y,z)
   test_min_neg#(0(x),y,z) -> test_min_neg#(x,y,z)
   test_min_neg#(1(x),y,z) -> test_min_pos#(x,y,z)
   test_min_neg#(j(x),y,z) -> test_min_neg#(x,y,z)
   f#(x,#()) -> signe#(x)
   f#(0(x),0(y)) -> f#(x,y)
   f#(0(x),1(y)) -> f#(x,1(y))
   f#(0(x),1(y)) -> 0#(f(x,1(y)))
   f#(0(x),j(y)) -> f#(x,j(y))
   f#(0(x),j(y)) -> 0#(f(x,j(y)))
   f#(1(x),0(y)) -> f#(1(x),y)
   f#(1(x),1(y)) -> -#(x,y)
   f#(1(x),1(y)) -> min#(1(x),1(y))
   f#(1(x),1(y)) -> f#(min(1(x),1(y)),-(x,y))
   f#(1(x),1(y)) -> min'#(x,y)
   f#(1(x),1(y)) -> -#(x,min'(x,y))
   f#(1(x),1(y)) -> f#(-(x,min'(x,y)),1(y))
   f#(1(x),1(y)) -> 0#(f(-(x,min'(x,y)),1(y)))
   f#(1(x),1(y)) -> +{AC,#}(0(f(-(x,min'(x,y)),1(y))),f(min(1(x),1(y)),-(x,y)))
   f#(1(x),j(y)) -> +{AC,#}(x,y)
   f#(1(x),j(y)) -> opp#(y)
   f#(1(x),j(y)) -> min#(1(x),1(opp(y)))
   f#(1(x),j(y)) -> f#(min(1(x),1(opp(y))),+AC(x,y))
   f#(1(x),j(y)) -> opp#(x)
   f#(1(x),j(y)) -> min''#(opp(x),y)
   f#(1(x),j(y)) -> +{AC,#}(min''(opp(x),y),x)
   f#(1(x),j(y)) -> f#(+AC(min''(opp(x),y),x),j(y))
   f#(1(x),j(y)) -> 0#(f(+AC(min''(opp(x),y),x),j(y)))
   f#(1(x),j(y)) -> +{AC,#}(0(f(+AC(min''(opp(x),y),x),j(y))),f(min(1(x),1(opp(y))),+AC(x,y)))
   f#(j(x),0(y)) -> f#(j(x),y)
   f#(j(x),1(y)) -> +{AC,#}(x,y)
   f#(j(x),1(y)) -> opp#(y)
   f#(j(x),1(y)) -> min#(j(x),j(opp(y)))
   f#(j(x),1(y)) -> f#(min(j(x),j(opp(y))),+AC(x,y))
   f#(j(x),1(y)) -> opp#(x)
   f#(j(x),1(y)) -> min'#(opp(x),y)
   f#(j(x),1(y)) -> +{AC,#}(min'(opp(x),y),x)
   f#(j(x),1(y)) -> f#(+AC(min'(opp(x),y),x),1(y))
   f#(j(x),1(y)) -> 0#(f(+AC(min'(opp(x),y),x),1(y)))
   f#(j(x),1(y)) -> +{AC,#}(0(f(+AC(min'(opp(x),y),x),1(y))),f(min(j(x),j(opp(y))),+AC(x,y)))
   f#(j(x),j(y)) -> -#(x,y)
   f#(j(x),j(y)) -> min#(j(x),j(y))
   f#(j(x),j(y)) -> f#(min(j(x),j(y)),-(x,y))
   f#(j(x),j(y)) -> min''#(x,y)
   f#(j(x),j(y)) -> -#(x,min''(x,y))
   f#(j(x),j(y)) -> f#(-(x,min''(x,y)),j(y))
   f#(j(x),j(y)) -> 0#(f(-(x,min''(x,y)),j(y)))
   f#(j(x),j(y)) -> +{AC,#}(0(f(-(x,min''(x,y)),j(y))),f(min(j(x),j(y)),-(x,y)))
   rat#(x,y) -> f#(y,x)
   rat#(x,y) -> *{AC,#}(signe(y),f(y,x))
   rat#(x,y) -> f#(x,y)
   rat#(x,y) -> signe#(y)
   rat#(x,y) -> *{AC,#}(signe(y),f(x,y))
   +_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(y,v)
   +_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(y,u)
   +_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(x,v)
   +_Q{C,#}(irred(x,y),irred(u,v)) -> +{AC,#}(*AC(x,v),*AC(y,u))
   *_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(y,v)
   *_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(x,u)
   *_Q{C,#}(irred(x,y),irred(u,v)) -> rat#(*AC(x,u),*AC(y,v))
   +{AC,#}(x8,+AC(#(),x)) -> +{AC,#}(x8,x)
   +{AC,#}(x9,+AC(0(x),0(y))) -> +{AC,#}(x,y)
   +{AC,#}(x9,+AC(0(x),0(y))) -> 0#(+AC(x,y))
   +{AC,#}(x9,+AC(0(x),0(y))) -> +{AC,#}(x9,0(+AC(x,y)))
   +{AC,#}(x10,+AC(0(x),1(y))) -> +{AC,#}(x,y)
   +{AC,#}(x10,+AC(0(x),1(y))) -> +{AC,#}(x10,1(+AC(x,y)))
   +{AC,#}(x11,+AC(0(x),j(y))) -> +{AC,#}(x,y)
   +{AC,#}(x11,+AC(0(x),j(y))) -> +{AC,#}(x11,j(+AC(x,y)))
   +{AC,#}(x12,+AC(1(x),1(y))) -> +{AC,#}(x,y)
   +{AC,#}(x12,+AC(1(x),1(y))) -> +{AC,#}(1(#()),+AC(x,y))
   +{AC,#}(x12,+AC(1(x),1(y))) -> +{AC,#}(x12,j(+AC(1(#()),+AC(x,y))))
   +{AC,#}(x13,+AC(j(x),j(y))) -> +{AC,#}(x,y)
   +{AC,#}(x13,+AC(j(x),j(y))) -> +{AC,#}(j(#()),+AC(x,y))
   +{AC,#}(x13,+AC(j(x),j(y))) -> +{AC,#}(x13,1(+AC(j(#()),+AC(x,y))))
   +{AC,#}(x14,+AC(1(x),j(y))) -> +{AC,#}(x,y)
   +{AC,#}(x14,+AC(1(x),j(y))) -> 0#(+AC(x,y))
   +{AC,#}(x14,+AC(1(x),j(y))) -> +{AC,#}(x14,0(+AC(x,y)))
   *{AC,#}(x15,*AC(#(),x)) -> *{AC,#}(x15,#())
   *{AC,#}(x16,*AC(0(x),y)) -> *{AC,#}(x,y)
   *{AC,#}(x16,*AC(0(x),y)) -> 0#(*AC(x,y))
   *{AC,#}(x16,*AC(0(x),y)) -> *{AC,#}(x16,0(*AC(x,y)))
   *{AC,#}(x17,*AC(1(x),y)) -> *{AC,#}(x,y)
   *{AC,#}(x17,*AC(1(x),y)) -> 0#(*AC(x,y))
   *{AC,#}(x17,*AC(1(x),y)) -> +{AC,#}(0(*AC(x,y)),y)
   *{AC,#}(x17,*AC(1(x),y)) -> *{AC,#}(x17,+AC(0(*AC(x,y)),y))
   *{AC,#}(x18,*AC(j(x),y)) -> *{AC,#}(x,y)
   *{AC,#}(x18,*AC(j(x),y)) -> 0#(*AC(x,y))
   *{AC,#}(x18,*AC(j(x),y)) -> -#(0(*AC(x,y)),y)
   *{AC,#}(x18,*AC(j(x),y)) -> *{AC,#}(x18,-(0(*AC(x,y)),y))
  Equations:
   +AC(+AC(x5,x6),x7) -> +AC(x5,+AC(x6,x7))
   +AC(x5,x6) -> +AC(x6,x5)
   *AC(*AC(x5,x6),x7) -> *AC(x5,*AC(x6,x7))
   *AC(x5,x6) -> *AC(x6,x5)
   +AC(x5,+AC(x6,x7)) -> +AC(+AC(x5,x6),x7)
   +AC(x6,x5) -> +AC(x5,x6)
   *AC(x5,*AC(x6,x7)) -> *AC(*AC(x5,x6),x7)
   *AC(x6,x5) -> *AC(x5,x6)
  TRS:
   0(#()) -> #()
   +AC(#(),x) -> x
   +AC(0(x),0(y)) -> 0(+AC(x,y))
   +AC(0(x),1(y)) -> 1(+AC(x,y))
   +AC(0(x),j(y)) -> j(+AC(x,y))
   +AC(1(x),1(y)) -> j(+AC(1(#()),+AC(x,y)))
   +AC(j(x),j(y)) -> 1(+AC(j(#()),+AC(x,y)))
   +AC(1(x),j(y)) -> 0(+AC(x,y))
   opp(#()) -> #()
   opp(0(x)) -> 0(opp(x))
   opp(1(x)) -> j(opp(x))
   opp(j(x)) -> 1(opp(x))
   -(x,y) -> +AC(opp(y),x)
   *AC(#(),x) -> #()
   *AC(0(x),y) -> 0(*AC(x,y))
   *AC(1(x),y) -> +AC(0(*AC(x,y)),y)
   *AC(j(x),y) -> -(0(*AC(x,y)),y)
   abs(x) -> test_abs_pos(x,x)
   test_abs_pos(#(),x) -> x
   test_abs_pos(0(x),y) -> test_abs_pos(x,y)
   test_abs_pos(1(x),y) -> test_abs_pos(x,y)
   test_abs_pos(j(x),y) -> test_abs_neg(x,y)
   test_abs_neg(#(),x) -> opp(x)
   test_abs_neg(0(x),y) -> test_abs_neg(x,y)
   test_abs_neg(1(x),y) -> test_abs_pos(x,y)
   test_abs_neg(j(x),y) -> test_abs_neg(x,y)
   signe(#()) -> #()
   signe(0(x)) -> signe(x)
   signe(1(x)) -> test_signe_pos(x)
   signe(j(x)) -> test_signe_neg(x)
   test_signe_pos(#()) -> 1(#())
   test_signe_pos(0(x)) -> test_signe_pos(x)
   test_signe_pos(1(x)) -> test_signe_pos(x)
   test_signe_pos(j(x)) -> test_signe_neg(x)
   test_signe_neg(#()) -> j(#())
   test_signe_neg(0(x)) -> test_signe_neg(x)
   test_signe_neg(1(x)) -> test_signe_pos(x)
   test_signe_neg(j(x)) -> test_signe_neg(x)
   min(x,y) -> test_min_pos(-(abs(y),abs(x)),x,y)
   min'(x,y) -> test_min_pos(-(abs(1(y)),abs(1(x))),x,y)
   min''(x,y) -> test_min_pos(-(abs(j(y)),abs(j(x))),x,y)
   test_min_pos(#(),x,y) -> x
   test_min_pos(0(x),y,z) -> test_min_pos(x,y,z)
   test_min_pos(1(x),y,z) -> test_min_pos(x,y,z)
   test_min_pos(j(x),y,z) -> test_min_neg(x,y,z)
   test_min_neg(#(),x,y) -> y
   test_min_neg(0(x),y,z) -> test_min_neg(x,y,z)
   test_min_neg(1(x),y,z) -> test_min_pos(x,y,z)
   test_min_neg(j(x),y,z) -> test_min_neg(x,y,z)
   f(#(),x) -> #()
   f(x,#()) -> signe(x)
   f(0(x),0(y)) -> f(x,y)
   f(0(x),1(y)) -> 0(f(x,1(y)))
   f(0(x),j(y)) -> 0(f(x,j(y)))
   f(1(x),0(y)) -> f(1(x),y)
   f(1(x),1(y)) -> +AC(0(f(-(x,min'(x,y)),1(y))),f(min(1(x),1(y)),-(x,y)))
   f(1(x),j(y)) -> +AC(0(f(+AC(min''(opp(x),y),x),j(y))),f(min(1(x),1(opp(y))),+AC(x,y)))
   f(j(x),0(y)) -> f(j(x),y)
   f(j(x),1(y)) -> +AC(0(f(+AC(min'(opp(x),y),x),1(y))),f(min(j(x),j(opp(y))),+AC(x,y)))
   f(j(x),j(y)) -> +AC(0(f(-(x,min''(x,y)),j(y))),f(min(j(x),j(y)),-(x,y)))
   rat(x,y) -> irred(*AC(signe(y),f(x,y)),*AC(signe(y),f(y,x)))
   +_QC(irred(x,y),irred(u,v)) -> irred(+AC(*AC(x,v),*AC(y,u)),*AC(y,v))
   *_QC(irred(x,y),irred(u,v)) -> rat(*AC(x,u),*AC(y,v))
  S:
   +{AC,#}(+AC(x19,x20),x21) -> +{AC,#}(x19,x20)
   +{AC,#}(x19,+AC(x20,x21)) -> +{AC,#}(x20,x21)
   *{AC,#}(*AC(x19,x20),x21) -> *{AC,#}(x19,x20)
   *{AC,#}(x19,*AC(x20,x21)) -> *{AC,#}(x20,x21)
  AC-EDG Processor:
   Equations#:
    +{AC,#}(+AC(x5,x6),x7) -> +{AC,#}(x5,+AC(x6,x7))
    +{AC,#}(x5,x6) -> +{AC,#}(x6,x5)
    *{AC,#}(*AC(x5,x6),x7) -> *{AC,#}(x5,*AC(x6,x7))
    *{AC,#}(x5,x6) -> *{AC,#}(x6,x5)
    +{AC,#}(x5,+AC(x6,x7)) -> +{AC,#}(+AC(x5,x6),x7)
    +{AC,#}(x6,x5) -> +{AC,#}(x5,x6)
    *{AC,#}(x5,*AC(x6,x7)) -> *{AC,#}(*AC(x5,x6),x7)
    *{AC,#}(x6,x5) -> *{AC,#}(x5,x6)
   DPs:
    +{AC,#}(0(x),0(y)) -> +{AC,#}(x,y)
    +{AC,#}(0(x),0(y)) -> 0#(+AC(x,y))
    +{AC,#}(0(x),1(y)) -> +{AC,#}(x,y)
    +{AC,#}(0(x),j(y)) -> +{AC,#}(x,y)
    +{AC,#}(1(x),1(y)) -> +{AC,#}(x,y)
    +{AC,#}(1(x),1(y)) -> +{AC,#}(1(#()),+AC(x,y))
    +{AC,#}(j(x),j(y)) -> +{AC,#}(x,y)
    +{AC,#}(j(x),j(y)) -> +{AC,#}(j(#()),+AC(x,y))
    +{AC,#}(1(x),j(y)) -> +{AC,#}(x,y)
    +{AC,#}(1(x),j(y)) -> 0#(+AC(x,y))
    opp#(0(x)) -> opp#(x)
    opp#(0(x)) -> 0#(opp(x))
    opp#(1(x)) -> opp#(x)
    opp#(j(x)) -> opp#(x)
    -#(x,y) -> opp#(y)
    -#(x,y) -> +{AC,#}(opp(y),x)
    *{AC,#}(0(x),y) -> *{AC,#}(x,y)
    *{AC,#}(0(x),y) -> 0#(*AC(x,y))
    *{AC,#}(1(x),y) -> *{AC,#}(x,y)
    *{AC,#}(1(x),y) -> 0#(*AC(x,y))
    *{AC,#}(1(x),y) -> +{AC,#}(0(*AC(x,y)),y)
    *{AC,#}(j(x),y) -> *{AC,#}(x,y)
    *{AC,#}(j(x),y) -> 0#(*AC(x,y))
    *{AC,#}(j(x),y) -> -#(0(*AC(x,y)),y)
    abs#(x) -> test_abs_pos#(x,x)
    test_abs_pos#(0(x),y) -> test_abs_pos#(x,y)
    test_abs_pos#(1(x),y) -> test_abs_pos#(x,y)
    test_abs_pos#(j(x),y) -> test_abs_neg#(x,y)
    test_abs_neg#(#(),x) -> opp#(x)
    test_abs_neg#(0(x),y) -> test_abs_neg#(x,y)
    test_abs_neg#(1(x),y) -> test_abs_pos#(x,y)
    test_abs_neg#(j(x),y) -> test_abs_neg#(x,y)
    signe#(0(x)) -> signe#(x)
    signe#(1(x)) -> test_signe_pos#(x)
    signe#(j(x)) -> test_signe_neg#(x)
    test_signe_pos#(0(x)) -> test_signe_pos#(x)
    test_signe_pos#(1(x)) -> test_signe_pos#(x)
    test_signe_pos#(j(x)) -> test_signe_neg#(x)
    test_signe_neg#(0(x)) -> test_signe_neg#(x)
    test_signe_neg#(1(x)) -> test_signe_pos#(x)
    test_signe_neg#(j(x)) -> test_signe_neg#(x)
    min#(x,y) -> abs#(x)
    min#(x,y) -> abs#(y)
    min#(x,y) -> -#(abs(y),abs(x))
    min#(x,y) -> test_min_pos#(-(abs(y),abs(x)),x,y)
    min'#(x,y) -> abs#(1(x))
    min'#(x,y) -> abs#(1(y))
    min'#(x,y) -> -#(abs(1(y)),abs(1(x)))
    min'#(x,y) -> test_min_pos#(-(abs(1(y)),abs(1(x))),x,y)
    min''#(x,y) -> abs#(j(x))
    min''#(x,y) -> abs#(j(y))
    min''#(x,y) -> -#(abs(j(y)),abs(j(x)))
    min''#(x,y) -> test_min_pos#(-(abs(j(y)),abs(j(x))),x,y)
    test_min_pos#(0(x),y,z) -> test_min_pos#(x,y,z)
    test_min_pos#(1(x),y,z) -> test_min_pos#(x,y,z)
    test_min_pos#(j(x),y,z) -> test_min_neg#(x,y,z)
    test_min_neg#(0(x),y,z) -> test_min_neg#(x,y,z)
    test_min_neg#(1(x),y,z) -> test_min_pos#(x,y,z)
    test_min_neg#(j(x),y,z) -> test_min_neg#(x,y,z)
    f#(x,#()) -> signe#(x)
    f#(0(x),0(y)) -> f#(x,y)
    f#(0(x),1(y)) -> f#(x,1(y))
    f#(0(x),1(y)) -> 0#(f(x,1(y)))
    f#(0(x),j(y)) -> f#(x,j(y))
    f#(0(x),j(y)) -> 0#(f(x,j(y)))
    f#(1(x),0(y)) -> f#(1(x),y)
    f#(1(x),1(y)) -> -#(x,y)
    f#(1(x),1(y)) -> min#(1(x),1(y))
    f#(1(x),1(y)) -> f#(min(1(x),1(y)),-(x,y))
    f#(1(x),1(y)) -> min'#(x,y)
    f#(1(x),1(y)) -> -#(x,min'(x,y))
    f#(1(x),1(y)) -> f#(-(x,min'(x,y)),1(y))
    f#(1(x),1(y)) -> 0#(f(-(x,min'(x,y)),1(y)))
    f#(1(x),1(y)) -> +{AC,#}(0(f(-(x,min'(x,y)),1(y))),f(min(1(x),1(y)),-(x,y)))
    f#(1(x),j(y)) -> +{AC,#}(x,y)
    f#(1(x),j(y)) -> opp#(y)
    f#(1(x),j(y)) -> min#(1(x),1(opp(y)))
    f#(1(x),j(y)) -> f#(min(1(x),1(opp(y))),+AC(x,y))
    f#(1(x),j(y)) -> opp#(x)
    f#(1(x),j(y)) -> min''#(opp(x),y)
    f#(1(x),j(y)) -> +{AC,#}(min''(opp(x),y),x)
    f#(1(x),j(y)) -> f#(+AC(min''(opp(x),y),x),j(y))
    f#(1(x),j(y)) -> 0#(f(+AC(min''(opp(x),y),x),j(y)))
    f#(1(x),j(y)) -> +{AC,#}(0(f(+AC(min''(opp(x),y),x),j(y))),f(min(1(x),1(opp(y))),+AC(x,y)))
    f#(j(x),0(y)) -> f#(j(x),y)
    f#(j(x),1(y)) -> +{AC,#}(x,y)
    f#(j(x),1(y)) -> opp#(y)
    f#(j(x),1(y)) -> min#(j(x),j(opp(y)))
    f#(j(x),1(y)) -> f#(min(j(x),j(opp(y))),+AC(x,y))
    f#(j(x),1(y)) -> opp#(x)
    f#(j(x),1(y)) -> min'#(opp(x),y)
    f#(j(x),1(y)) -> +{AC,#}(min'(opp(x),y),x)
    f#(j(x),1(y)) -> f#(+AC(min'(opp(x),y),x),1(y))
    f#(j(x),1(y)) -> 0#(f(+AC(min'(opp(x),y),x),1(y)))
    f#(j(x),1(y)) -> +{AC,#}(0(f(+AC(min'(opp(x),y),x),1(y))),f(min(j(x),j(opp(y))),+AC(x,y)))
    f#(j(x),j(y)) -> -#(x,y)
    f#(j(x),j(y)) -> min#(j(x),j(y))
    f#(j(x),j(y)) -> f#(min(j(x),j(y)),-(x,y))
    f#(j(x),j(y)) -> min''#(x,y)
    f#(j(x),j(y)) -> -#(x,min''(x,y))
    f#(j(x),j(y)) -> f#(-(x,min''(x,y)),j(y))
    f#(j(x),j(y)) -> 0#(f(-(x,min''(x,y)),j(y)))
    f#(j(x),j(y)) -> +{AC,#}(0(f(-(x,min''(x,y)),j(y))),f(min(j(x),j(y)),-(x,y)))
    rat#(x,y) -> f#(y,x)
    rat#(x,y) -> *{AC,#}(signe(y),f(y,x))
    rat#(x,y) -> f#(x,y)
    rat#(x,y) -> signe#(y)
    rat#(x,y) -> *{AC,#}(signe(y),f(x,y))
    +_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(y,v)
    +_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(y,u)
    +_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(x,v)
    +_Q{C,#}(irred(x,y),irred(u,v)) -> +{AC,#}(*AC(x,v),*AC(y,u))
    *_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(y,v)
    *_Q{C,#}(irred(x,y),irred(u,v)) -> *{AC,#}(x,u)
    *_Q{C,#}(irred(x,y),irred(u,v)) -> rat#(*AC(x,u),*AC(y,v))
    +{AC,#}(x8,+AC(#(),x)) -> +{AC,#}(x8,x)
    +{AC,#}(x9,+AC(0(x),0(y))) -> +{AC,#}(x,y)
    +{AC,#}(x9,+AC(0(x),0(y))) -> 0#(+AC(x,y))
    +{AC,#}(x9,+AC(0(x),0(y))) -> +{AC,#}(x9,0(+AC(x,y)))
    +{AC,#}(x10,+AC(0(x),1(y))) -> +{AC,#}(x,y)
    +{AC,#}(x10,+AC(0(x),1(y))) -> +{AC,#}(x10,1(+AC(x,y)))
    +{AC,#}(x11,+AC(0(x),j(y))) -> +{AC,#}(x,y)
    +{AC,#}(x11,+AC(0(x),j(y))) -> +{AC,#}(x11,j(+AC(x,y)))
    +{AC,#}(x12,+AC(1(x),1(y))) -> +{AC,#}(x,y)
    +{AC,#}(x12,+AC(1(x),1(y))) -> +{AC,#}(1(#()),+AC(x,y))
    +{AC,#}(x12,+AC(1(x),1(y))) -> +{AC,#}(x12,j(+AC(1(#()),+AC(x,y))))
    +{AC,#}(x13,+AC(j(x),j(y))) -> +{AC,#}(x,y)
    +{AC,#}(x13,+AC(j(x),j(y))) -> +{AC,#}(j(#()),+AC(x,y))
    +{AC,#}(x13,+AC(j(x),j(y))) -> +{AC,#}(x13,1(+AC(j(#()),+AC(x,y))))
    +{AC,#}(x14,+AC(1(x),j(y))) -> +{AC,#}(x,y)
    +{AC,#}(x14,+AC(1(x),j(y))) -> 0#(+AC(x,y))
    +{AC,#}(x14,+AC(1(x),j(y))) -> +{AC,#}(x14,0(+AC(x,y)))
    *{AC,#}(x15,*AC(#(),x)) -> *{AC,#}(x15,#())
    *{AC,#}(x16,*AC(0(x),y)) -> *{AC,#}(x,y)
    *{AC,#}(x16,*AC(0(x),y)) -> 0#(*AC(x,y))
    *{AC,#}(x16,*AC(0(x),y)) -> *{AC,#}(x16,0(*AC(x,y)))
    *{AC,#}(x17,*AC(1(x),y)) -> *{AC,#}(x,y)
    *{AC,#}(x17,*AC(1(x),y)) -> 0#(*AC(x,y))
    *{AC,#}(x17,*AC(1(x),y)) -> +{AC,#}(0(*AC(x,y)),y)
    *{AC,#}(x17,*AC(1(x),y)) -> *{AC,#}(x17,+AC(0(*AC(x,y)),y))
    *{AC,#}(x18,*AC(j(x),y)) -> *{AC,#}(x,y)
    *{AC,#}(x18,*AC(j(x),y)) -> 0#(*AC(x,y))
    *{AC,#}(x18,*AC(j(x),y)) -> -#(0(*AC(x,y)),y)
    *{AC,#}(x18,*AC(j(x),y)) -> *{AC,#}(x18,-(0(*AC(x,y)),y))
   Equations:
    +AC(+AC(x5,x6),x7) -> +AC(x5,+AC(x6,x7))
    +AC(x5,x6) -> +AC(x6,x5)
    *AC(*AC(x5,x6),x7) -> *AC(x5,*AC(x6,x7))
    *AC(x5,x6) -> *AC(x6,x5)
    +AC(x5,+AC(x6,x7)) -> +AC(+AC(x5,x6),x7)
    +AC(x6,x5) -> +AC(x5,x6)
    *AC(x5,*AC(x6,x7)) -> *AC(*AC(x5,x6),x7)
    *AC(x6,x5) -> *AC(x5,x6)
   TRS:
    0(#()) -> #()
    +AC(#(),x) -> x
    +AC(0(x),0(y)) -> 0(+AC(x,y))
    +AC(0(x),1(y)) -> 1(+AC(x,y))
    +AC(0(x),j(y)) -> j(+AC(x,y))
    +AC(1(x),1(y)) -> j(+AC(1(#()),+AC(x,y)))
    +AC(j(x),j(y)) -> 1(+AC(j(#()),+AC(x,y)))
    +AC(1(x),j(y)) -> 0(+AC(x,y))
    opp(#()) -> #()
    opp(0(x)) -> 0(opp(x))
    opp(1(x)) -> j(opp(x))
    opp(j(x)) -> 1(opp(x))
    -(x,y) -> +AC(opp(y),x)
    *AC(#(),x) -> #()
    *AC(0(x),y) -> 0(*AC(x,y))
    *AC(1(x),y) -> +AC(0(*AC(x,y)),y)
    *AC(j(x),y) -> -(0(*AC(x,y)),y)
    abs(x) -> test_abs_pos(x,x)
    test_abs_pos(#(),x) -> x
    test_abs_pos(0(x),y) -> test_abs_pos(x,y)
    test_abs_pos(1(x),y) -> test_abs_pos(x,y)
    test_abs_pos(j(x),y) -> test_abs_neg(x,y)
    test_abs_neg(#(),x) -> opp(x)
    test_abs_neg(0(x),y) -> test_abs_neg(x,y)
    test_abs_neg(1(x),y) -> test_abs_pos(x,y)
    test_abs_neg(j(x),y) -> test_abs_neg(x,y)
    signe(#()) -> #()
    signe(0(x)) -> signe(x)
    signe(1(x)) -> test_signe_pos(x)
    signe(j(x)) -> test_signe_neg(x)
    test_signe_pos(#()) -> 1(#())
    test_signe_pos(0(x)) -> test_signe_pos(x)
    test_signe_pos(1(x)) -> test_signe_pos(x)
    test_signe_pos(j(x)) -> test_signe_neg(x)
    test_signe_neg(#()) -> j(#())
    test_signe_neg(0(x)) -> test_signe_neg(x)
    test_signe_neg(1(x)) -> test_signe_pos(x)
    test_signe_neg(j(x)) -> test_signe_neg(x)
    min(x,y) -> test_min_pos(-(abs(y),abs(x)),x,y)
    min'(x,y) -> test_min_pos(-(abs(1(y)),abs(1(x))),x,y)
    min''(x,y) -> test_min_pos(-(abs(j(y)),abs(j(x))),x,y)
    test_min_pos(#(),x,y) -> x
    test_min_pos(0(x),y,z) -> test_min_pos(x,y,z)
    test_min_pos(1(x),y,z) -> test_min_pos(x,y,z)
    test_min_pos(j(x),y,z) -> test_min_neg(x,y,z)
    test_min_neg(#(),x,y) -> y
    test_min_neg(0(x),y,z) -> test_min_neg(x,y,z)
    test_min_neg(1(x),y,z) -> test_min_pos(x,y,z)
    test_min_neg(j(x),y,z) -> test_min_neg(x,y,z)
    f(#(),x) -> #()
    f(x,#()) -> signe(x)
    f(0(x),0(y)) -> f(x,y)
    f(0(x),1(y)) -> 0(f(x,1(y)))
    f(0(x),j(y)) -> 0(f(x,j(y)))
    f(1(x),0(y)) -> f(1(x),y)
    f(1(x),1(y)) -> +AC(0(f(-(x,min'(x,y)),1(y))),f(min(1(x),1(y)),-(x,y)))
    f(1(x),j(y)) -> +AC(0(f(+AC(min''(opp(x),y),x),j(y))),f(min(1(x),1(opp(y))),+AC(x,y)))
    f(j(x),0(y)) -> f(j(x),y)
    f(j(x),1(y)) -> +AC(0(f(+AC(min'(opp(x),y),x),1(y))),f(min(j(x),j(opp(y))),+AC(x,y)))
    f(j(x),j(y)) -> +AC(0(f(-(x,min''(x,y)),j(y))),f(min(j(x),j(y)),-(x,y)))
    rat(x,y) -> irred(*AC(signe(y),f(x,y)),*AC(signe(y),f(y,x)))
    +_QC(irred(x,y),irred(u,v)) -> irred(+AC(*AC(x,v),*AC(y,u)),*AC(y,v))
    *_QC(irred(x,y),irred(u,v)) -> rat(*AC(x,u),*AC(y,v))
   S:
    +{AC,#}(+AC(x19,x20),x21) -> +{AC,#}(x19,x20)
    +{AC,#}(x19,+AC(x20,x21)) -> +{AC,#}(x20,x21)
    *{AC,#}(*AC(x19,x20),x21) -> *{AC,#}(x19,x20)
    *{AC,#}(x19,*AC(x20,x21)) -> *{AC,#}(x20,x21)
   Open