MAYBE
Time: 1.982

Problem:
 Equations:
  plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
  plusAC(x2,x3) -> plusAC(x3,x2)
  multAC(multAC(x2,x3),x4) -> multAC(x2,multAC(x3,x4))
  multAC(x2,x3) -> multAC(x3,x2)
  plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
  plusAC(x3,x2) -> plusAC(x2,x3)
  multAC(x2,multAC(x3,x4)) -> multAC(multAC(x2,x3),x4)
  multAC(x3,x2) -> multAC(x2,x3)
 TRS:
  zero(sharp()) -> sharp()
  plusAC(x,sharp()) -> x
  plusAC(zero(x),zero(y)) -> zero(plusAC(x,y))
  plusAC(zero(x),one(y)) -> one(plusAC(x,y))
  plusAC(one(x),one(y)) -> j(plusAC(x,plusAC(y,one(sharp()))))
  plusAC(zero(x),j(y)) -> j(plusAC(x,y))
  plusAC(j(x),one(y)) -> zero(plusAC(x,y))
  plusAC(j(x),j(y)) -> one(plusAC(x,plusAC(y,j(sharp()))))
  minus(x,y) -> plusAC(x,opp(y))
  opp(sharp()) -> sharp()
  opp(zero(x)) -> zero(opp(x))
  opp(one(x)) -> j(opp(x))
  opp(j(x)) -> one(opp(x))
  multAC(x,sharp()) -> sharp()
  multAC(zero(x),y) -> zero(multAC(x,y))
  multAC(one(x),y) -> plusAC(zero(multAC(x,y)),y)

Proof:
 DP Processor:
  Equations#:
   plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4))
   plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2)
   mult{AC,#}(multAC(x2,x3),x4) -> mult{AC,#}(x2,multAC(x3,x4))
   mult{AC,#}(x2,x3) -> mult{AC,#}(x3,x2)
   plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4)
   plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3)
   mult{AC,#}(x2,multAC(x3,x4)) -> mult{AC,#}(multAC(x2,x3),x4)
   mult{AC,#}(x3,x2) -> mult{AC,#}(x2,x3)
  DPs:
   plus{AC,#}(zero(x),zero(y)) -> plus{AC,#}(x,y)
   plus{AC,#}(zero(x),zero(y)) -> zero#(plusAC(x,y))
   plus{AC,#}(zero(x),one(y)) -> plus{AC,#}(x,y)
   plus{AC,#}(one(x),one(y)) -> plus{AC,#}(y,one(sharp()))
   plus{AC,#}(one(x),one(y)) -> plus{AC,#}(x,plusAC(y,one(sharp())))
   plus{AC,#}(zero(x),j(y)) -> plus{AC,#}(x,y)
   plus{AC,#}(j(x),one(y)) -> plus{AC,#}(x,y)
   plus{AC,#}(j(x),one(y)) -> zero#(plusAC(x,y))
   plus{AC,#}(j(x),j(y)) -> plus{AC,#}(y,j(sharp()))
   plus{AC,#}(j(x),j(y)) -> plus{AC,#}(x,plusAC(y,j(sharp())))
   minus#(x,y) -> opp#(y)
   minus#(x,y) -> plus{AC,#}(x,opp(y))
   opp#(zero(x)) -> opp#(x)
   opp#(zero(x)) -> zero#(opp(x))
   opp#(one(x)) -> opp#(x)
   opp#(j(x)) -> opp#(x)
   mult{AC,#}(zero(x),y) -> mult{AC,#}(x,y)
   mult{AC,#}(zero(x),y) -> zero#(multAC(x,y))
   mult{AC,#}(one(x),y) -> mult{AC,#}(x,y)
   mult{AC,#}(one(x),y) -> zero#(multAC(x,y))
   mult{AC,#}(one(x),y) -> plus{AC,#}(zero(multAC(x,y)),y)
   plus{AC,#}(x5,plusAC(x,sharp())) -> plus{AC,#}(x5,x)
   plus{AC,#}(x6,plusAC(zero(x),zero(y))) -> plus{AC,#}(x,y)
   plus{AC,#}(x6,plusAC(zero(x),zero(y))) -> zero#(plusAC(x,y))
   plus{AC,#}(x6,plusAC(zero(x),zero(y))) -> plus{AC,#}(x6,zero(plusAC(x,y)))
   plus{AC,#}(x7,plusAC(zero(x),one(y))) -> plus{AC,#}(x,y)
   plus{AC,#}(x7,plusAC(zero(x),one(y))) -> plus{AC,#}(x7,one(plusAC(x,y)))
   plus{AC,#}(x8,plusAC(one(x),one(y))) -> plus{AC,#}(y,one(sharp()))
   plus{AC,#}(x8,plusAC(one(x),one(y))) -> plus{AC,#}(x,plusAC(y,one(sharp())))
   plus{AC,#}(x8,plusAC(one(x),one(y))) -> plus{AC,#}(x8,j(plusAC(x,plusAC(y,one(sharp())))))
   plus{AC,#}(x9,plusAC(zero(x),j(y))) -> plus{AC,#}(x,y)
   plus{AC,#}(x9,plusAC(zero(x),j(y))) -> plus{AC,#}(x9,j(plusAC(x,y)))
   plus{AC,#}(x10,plusAC(j(x),one(y))) -> plus{AC,#}(x,y)
   plus{AC,#}(x10,plusAC(j(x),one(y))) -> zero#(plusAC(x,y))
   plus{AC,#}(x10,plusAC(j(x),one(y))) -> plus{AC,#}(x10,zero(plusAC(x,y)))
   plus{AC,#}(x11,plusAC(j(x),j(y))) -> plus{AC,#}(y,j(sharp()))
   plus{AC,#}(x11,plusAC(j(x),j(y))) -> plus{AC,#}(x,plusAC(y,j(sharp())))
   plus{AC,#}(x11,plusAC(j(x),j(y))) -> plus{AC,#}(x11,one(plusAC(x,plusAC(y,j(sharp())))))
   mult{AC,#}(x12,multAC(x,sharp())) -> mult{AC,#}(x12,sharp())
   mult{AC,#}(x13,multAC(zero(x),y)) -> mult{AC,#}(x,y)
   mult{AC,#}(x13,multAC(zero(x),y)) -> zero#(multAC(x,y))
   mult{AC,#}(x13,multAC(zero(x),y)) -> mult{AC,#}(x13,zero(multAC(x,y)))
   mult{AC,#}(x14,multAC(one(x),y)) -> mult{AC,#}(x,y)
   mult{AC,#}(x14,multAC(one(x),y)) -> zero#(multAC(x,y))
   mult{AC,#}(x14,multAC(one(x),y)) -> plus{AC,#}(zero(multAC(x,y)),y)
   mult{AC,#}(x14,multAC(one(x),y)) -> mult{AC,#}(x14,plusAC(zero(multAC(x,y)),y))
  Equations:
   plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
   plusAC(x2,x3) -> plusAC(x3,x2)
   multAC(multAC(x2,x3),x4) -> multAC(x2,multAC(x3,x4))
   multAC(x2,x3) -> multAC(x3,x2)
   plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
   plusAC(x3,x2) -> plusAC(x2,x3)
   multAC(x2,multAC(x3,x4)) -> multAC(multAC(x2,x3),x4)
   multAC(x3,x2) -> multAC(x2,x3)
  TRS:
   zero(sharp()) -> sharp()
   plusAC(x,sharp()) -> x
   plusAC(zero(x),zero(y)) -> zero(plusAC(x,y))
   plusAC(zero(x),one(y)) -> one(plusAC(x,y))
   plusAC(one(x),one(y)) -> j(plusAC(x,plusAC(y,one(sharp()))))
   plusAC(zero(x),j(y)) -> j(plusAC(x,y))
   plusAC(j(x),one(y)) -> zero(plusAC(x,y))
   plusAC(j(x),j(y)) -> one(plusAC(x,plusAC(y,j(sharp()))))
   minus(x,y) -> plusAC(x,opp(y))
   opp(sharp()) -> sharp()
   opp(zero(x)) -> zero(opp(x))
   opp(one(x)) -> j(opp(x))
   opp(j(x)) -> one(opp(x))
   multAC(x,sharp()) -> sharp()
   multAC(zero(x),y) -> zero(multAC(x,y))
   multAC(one(x),y) -> plusAC(zero(multAC(x,y)),y)
  S:
   plus{AC,#}(plusAC(x15,x16),x17) -> plus{AC,#}(x15,x16)
   plus{AC,#}(x15,plusAC(x16,x17)) -> plus{AC,#}(x16,x17)
   mult{AC,#}(multAC(x15,x16),x17) -> mult{AC,#}(x15,x16)
   mult{AC,#}(x15,multAC(x16,x17)) -> mult{AC,#}(x16,x17)
  AC-EDG Processor:
   Equations#:
    plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4))
    plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2)
    mult{AC,#}(multAC(x2,x3),x4) -> mult{AC,#}(x2,multAC(x3,x4))
    mult{AC,#}(x2,x3) -> mult{AC,#}(x3,x2)
    plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4)
    plus{AC,#}(x3,x2) -> plus{AC,#}(x2,x3)
    mult{AC,#}(x2,multAC(x3,x4)) -> mult{AC,#}(multAC(x2,x3),x4)
    mult{AC,#}(x3,x2) -> mult{AC,#}(x2,x3)
   DPs:
    plus{AC,#}(zero(x),zero(y)) -> plus{AC,#}(x,y)
    plus{AC,#}(zero(x),zero(y)) -> zero#(plusAC(x,y))
    plus{AC,#}(zero(x),one(y)) -> plus{AC,#}(x,y)
    plus{AC,#}(one(x),one(y)) -> plus{AC,#}(y,one(sharp()))
    plus{AC,#}(one(x),one(y)) -> plus{AC,#}(x,plusAC(y,one(sharp())))
    plus{AC,#}(zero(x),j(y)) -> plus{AC,#}(x,y)
    plus{AC,#}(j(x),one(y)) -> plus{AC,#}(x,y)
    plus{AC,#}(j(x),one(y)) -> zero#(plusAC(x,y))
    plus{AC,#}(j(x),j(y)) -> plus{AC,#}(y,j(sharp()))
    plus{AC,#}(j(x),j(y)) -> plus{AC,#}(x,plusAC(y,j(sharp())))
    minus#(x,y) -> opp#(y)
    minus#(x,y) -> plus{AC,#}(x,opp(y))
    opp#(zero(x)) -> opp#(x)
    opp#(zero(x)) -> zero#(opp(x))
    opp#(one(x)) -> opp#(x)
    opp#(j(x)) -> opp#(x)
    mult{AC,#}(zero(x),y) -> mult{AC,#}(x,y)
    mult{AC,#}(zero(x),y) -> zero#(multAC(x,y))
    mult{AC,#}(one(x),y) -> mult{AC,#}(x,y)
    mult{AC,#}(one(x),y) -> zero#(multAC(x,y))
    mult{AC,#}(one(x),y) -> plus{AC,#}(zero(multAC(x,y)),y)
    plus{AC,#}(x5,plusAC(x,sharp())) -> plus{AC,#}(x5,x)
    plus{AC,#}(x6,plusAC(zero(x),zero(y))) -> plus{AC,#}(x,y)
    plus{AC,#}(x6,plusAC(zero(x),zero(y))) -> zero#(plusAC(x,y))
    plus{AC,#}(x6,plusAC(zero(x),zero(y))) -> plus{AC,#}(x6,zero(plusAC(x,y)))
    plus{AC,#}(x7,plusAC(zero(x),one(y))) -> plus{AC,#}(x,y)
    plus{AC,#}(x7,plusAC(zero(x),one(y))) -> plus{AC,#}(x7,one(plusAC(x,y)))
    plus{AC,#}(x8,plusAC(one(x),one(y))) -> plus{AC,#}(y,one(sharp()))
    plus{AC,#}(x8,plusAC(one(x),one(y))) -> plus{AC,#}(x,plusAC(y,one(sharp())))
    plus{AC,#}(x8,plusAC(one(x),one(y))) -> plus{AC,#}(x8,j(plusAC(x,plusAC(y,one(sharp())))))
    plus{AC,#}(x9,plusAC(zero(x),j(y))) -> plus{AC,#}(x,y)
    plus{AC,#}(x9,plusAC(zero(x),j(y))) -> plus{AC,#}(x9,j(plusAC(x,y)))
    plus{AC,#}(x10,plusAC(j(x),one(y))) -> plus{AC,#}(x,y)
    plus{AC,#}(x10,plusAC(j(x),one(y))) -> zero#(plusAC(x,y))
    plus{AC,#}(x10,plusAC(j(x),one(y))) -> plus{AC,#}(x10,zero(plusAC(x,y)))
    plus{AC,#}(x11,plusAC(j(x),j(y))) -> plus{AC,#}(y,j(sharp()))
    plus{AC,#}(x11,plusAC(j(x),j(y))) -> plus{AC,#}(x,plusAC(y,j(sharp())))
    plus{AC,#}(x11,plusAC(j(x),j(y))) -> plus{AC,#}(x11,one(plusAC(x,plusAC(y,j(sharp())))))
    mult{AC,#}(x12,multAC(x,sharp())) -> mult{AC,#}(x12,sharp())
    mult{AC,#}(x13,multAC(zero(x),y)) -> mult{AC,#}(x,y)
    mult{AC,#}(x13,multAC(zero(x),y)) -> zero#(multAC(x,y))
    mult{AC,#}(x13,multAC(zero(x),y)) -> mult{AC,#}(x13,zero(multAC(x,y)))
    mult{AC,#}(x14,multAC(one(x),y)) -> mult{AC,#}(x,y)
    mult{AC,#}(x14,multAC(one(x),y)) -> zero#(multAC(x,y))
    mult{AC,#}(x14,multAC(one(x),y)) -> plus{AC,#}(zero(multAC(x,y)),y)
    mult{AC,#}(x14,multAC(one(x),y)) -> mult{AC,#}(x14,plusAC(zero(multAC(x,y)),y))
   Equations:
    plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
    plusAC(x2,x3) -> plusAC(x3,x2)
    multAC(multAC(x2,x3),x4) -> multAC(x2,multAC(x3,x4))
    multAC(x2,x3) -> multAC(x3,x2)
    plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
    plusAC(x3,x2) -> plusAC(x2,x3)
    multAC(x2,multAC(x3,x4)) -> multAC(multAC(x2,x3),x4)
    multAC(x3,x2) -> multAC(x2,x3)
   TRS:
    zero(sharp()) -> sharp()
    plusAC(x,sharp()) -> x
    plusAC(zero(x),zero(y)) -> zero(plusAC(x,y))
    plusAC(zero(x),one(y)) -> one(plusAC(x,y))
    plusAC(one(x),one(y)) -> j(plusAC(x,plusAC(y,one(sharp()))))
    plusAC(zero(x),j(y)) -> j(plusAC(x,y))
    plusAC(j(x),one(y)) -> zero(plusAC(x,y))
    plusAC(j(x),j(y)) -> one(plusAC(x,plusAC(y,j(sharp()))))
    minus(x,y) -> plusAC(x,opp(y))
    opp(sharp()) -> sharp()
    opp(zero(x)) -> zero(opp(x))
    opp(one(x)) -> j(opp(x))
    opp(j(x)) -> one(opp(x))
    multAC(x,sharp()) -> sharp()
    multAC(zero(x),y) -> zero(multAC(x,y))
    multAC(one(x),y) -> plusAC(zero(multAC(x,y)),y)
   S:
    plus{AC,#}(plusAC(x15,x16),x17) -> plus{AC,#}(x15,x16)
    plus{AC,#}(x15,plusAC(x16,x17)) -> plus{AC,#}(x16,x17)
    mult{AC,#}(multAC(x15,x16),x17) -> mult{AC,#}(x15,x16)
    mult{AC,#}(x15,multAC(x16,x17)) -> mult{AC,#}(x16,x17)
   Open