MAYBE
Time: 1.315

Problem:
 Equations:
  plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
  plusAC(x2,x3) -> plusAC(x3,x2)
  plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
  plusAC(x3,x2) -> plusAC(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()))))

Proof:
 DP Processor:
  Equations#:
   plus{AC,#}(plusAC(x2,x3),x4) -> plus{AC,#}(x2,plusAC(x3,x4))
   plus{AC,#}(x2,x3) -> plus{AC,#}(x3,x2)
   plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4)
   plus{AC,#}(x3,x2) -> plus{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())))
   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())))))
  Equations:
   plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
   plusAC(x2,x3) -> plusAC(x3,x2)
   plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
   plusAC(x3,x2) -> plusAC(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()))))
  S:
   plus{AC,#}(plusAC(x12,x13),x14) -> plus{AC,#}(x12,x13)
   plus{AC,#}(x12,plusAC(x13,x14)) -> plus{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)
    plus{AC,#}(x2,plusAC(x3,x4)) -> plus{AC,#}(plusAC(x2,x3),x4)
    plus{AC,#}(x3,x2) -> plus{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())))
    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())))))
   Equations:
    plusAC(plusAC(x2,x3),x4) -> plusAC(x2,plusAC(x3,x4))
    plusAC(x2,x3) -> plusAC(x3,x2)
    plusAC(x2,plusAC(x3,x4)) -> plusAC(plusAC(x2,x3),x4)
    plusAC(x3,x2) -> plusAC(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()))))
   S:
    plus{AC,#}(plusAC(x12,x13),x14) -> plus{AC,#}(x12,x13)
    plus{AC,#}(x12,plusAC(x13,x14)) -> plus{AC,#}(x13,x14)
   Open