MAYBE
Time: 1.216

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)) -> zero(plusAC(x,plusAC(y,one(sharp()))))
  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,#}(one(x),one(y)) -> zero#(plusAC(x,plusAC(y,one(sharp()))))
   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))) -> zero#(plusAC(x,plusAC(y,one(sharp()))))
   plus{AC,#}(x8,plusAC(one(x),one(y))) -> plus{AC,#}(x8,zero(plusAC(x,plusAC(y,one(sharp())))))
   mult{AC,#}(x9,multAC(x,sharp())) -> mult{AC,#}(x9,sharp())
   mult{AC,#}(x10,multAC(zero(x),y)) -> mult{AC,#}(x,y)
   mult{AC,#}(x10,multAC(zero(x),y)) -> zero#(multAC(x,y))
   mult{AC,#}(x10,multAC(zero(x),y)) -> mult{AC,#}(x10,zero(multAC(x,y)))
   mult{AC,#}(x11,multAC(one(x),y)) -> mult{AC,#}(x,y)
   mult{AC,#}(x11,multAC(one(x),y)) -> zero#(multAC(x,y))
   mult{AC,#}(x11,multAC(one(x),y)) -> plus{AC,#}(zero(multAC(x,y)),y)
   mult{AC,#}(x11,multAC(one(x),y)) -> mult{AC,#}(x11,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)) -> zero(plusAC(x,plusAC(y,one(sharp()))))
   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(x12,x13),x14) -> plus{AC,#}(x12,x13)
   plus{AC,#}(x12,plusAC(x13,x14)) -> plus{AC,#}(x13,x14)
   mult{AC,#}(multAC(x12,x13),x14) -> mult{AC,#}(x12,x13)
   mult{AC,#}(x12,multAC(x13,x14)) -> mult{AC,#}(x13,x14)
  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,#}(one(x),one(y)) -> zero#(plusAC(x,plusAC(y,one(sharp()))))
    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))) -> zero#(plusAC(x,plusAC(y,one(sharp()))))
    plus{AC,#}(x8,plusAC(one(x),one(y))) -> plus{AC,#}(x8,zero(plusAC(x,plusAC(y,one(sharp())))))
    mult{AC,#}(x9,multAC(x,sharp())) -> mult{AC,#}(x9,sharp())
    mult{AC,#}(x10,multAC(zero(x),y)) -> mult{AC,#}(x,y)
    mult{AC,#}(x10,multAC(zero(x),y)) -> zero#(multAC(x,y))
    mult{AC,#}(x10,multAC(zero(x),y)) -> mult{AC,#}(x10,zero(multAC(x,y)))
    mult{AC,#}(x11,multAC(one(x),y)) -> mult{AC,#}(x,y)
    mult{AC,#}(x11,multAC(one(x),y)) -> zero#(multAC(x,y))
    mult{AC,#}(x11,multAC(one(x),y)) -> plus{AC,#}(zero(multAC(x,y)),y)
    mult{AC,#}(x11,multAC(one(x),y)) -> mult{AC,#}(x11,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)) -> zero(plusAC(x,plusAC(y,one(sharp()))))
    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(x12,x13),x14) -> plus{AC,#}(x12,x13)
    plus{AC,#}(x12,plusAC(x13,x14)) -> plus{AC,#}(x13,x14)
    mult{AC,#}(multAC(x12,x13),x14) -> mult{AC,#}(x12,x13)
    mult{AC,#}(x12,multAC(x13,x14)) -> mult{AC,#}(x13,x14)
   Open