MAYBE
Time: 0.154

Problem:
 Equations:
  plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
  plusAC(x4,x5) -> plusAC(x5,x4)
  plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
  plusAC(x5,x4) -> plusAC(x4,x5)
 TRS:
  plusAC(x,0()) -> x
  plusAC(x,s(y)) -> s(plusAC(x,y))
  sum(nil(),nil()) -> 0()
  sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil()))
  sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs))
  sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys))

Proof:
 DP Processor:
  Equations#:
   plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
   plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
   plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
   plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
  DPs:
   plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y)
   sum#(cons(x,xs),nil()) -> sum#(xs,nil())
   sum#(cons(x,xs),nil()) -> plus{AC,#}(x,sum(xs,nil()))
   sum#(nil(),cons(x,xs)) -> sum#(nil(),xs)
   sum#(nil(),cons(x,xs)) -> plus{AC,#}(x,sum(nil(),xs))
   sum#(cons(x,xs),cons(y,ys)) -> sum#(xs,ys)
   sum#(cons(x,xs),cons(y,ys)) -> plus{AC,#}(x,y)
   sum#(cons(x,xs),cons(y,ys)) -> plus{AC,#}(plusAC(x,y),sum(xs,ys))
   plus{AC,#}(x7,plusAC(x,0())) -> plus{AC,#}(x7,x)
   plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x,y)
   plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x8,s(plusAC(x,y)))
  Equations:
   plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
   plusAC(x4,x5) -> plusAC(x5,x4)
   plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
   plusAC(x5,x4) -> plusAC(x4,x5)
  TRS:
   plusAC(x,0()) -> x
   plusAC(x,s(y)) -> s(plusAC(x,y))
   sum(nil(),nil()) -> 0()
   sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil()))
   sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs))
   sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys))
  S:
   plus{AC,#}(plusAC(x9,x10),x11) -> plus{AC,#}(x9,x10)
   plus{AC,#}(x9,plusAC(x10,x11)) -> plus{AC,#}(x10,x11)
  AC-EDG Processor:
   Equations#:
    plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
    plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
    plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
    plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
   DPs:
    plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y)
    sum#(cons(x,xs),nil()) -> sum#(xs,nil())
    sum#(cons(x,xs),nil()) -> plus{AC,#}(x,sum(xs,nil()))
    sum#(nil(),cons(x,xs)) -> sum#(nil(),xs)
    sum#(nil(),cons(x,xs)) -> plus{AC,#}(x,sum(nil(),xs))
    sum#(cons(x,xs),cons(y,ys)) -> sum#(xs,ys)
    sum#(cons(x,xs),cons(y,ys)) -> plus{AC,#}(x,y)
    sum#(cons(x,xs),cons(y,ys)) -> plus{AC,#}(plusAC(x,y),sum(xs,ys))
    plus{AC,#}(x7,plusAC(x,0())) -> plus{AC,#}(x7,x)
    plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x,y)
    plus{AC,#}(x8,plusAC(x,s(y))) -> plus{AC,#}(x8,s(plusAC(x,y)))
   Equations:
    plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
    plusAC(x4,x5) -> plusAC(x5,x4)
    plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
    plusAC(x5,x4) -> plusAC(x4,x5)
   TRS:
    plusAC(x,0()) -> x
    plusAC(x,s(y)) -> s(plusAC(x,y))
    sum(nil(),nil()) -> 0()
    sum(cons(x,xs),nil()) -> plusAC(x,sum(xs,nil()))
    sum(nil(),cons(x,xs)) -> plusAC(x,sum(nil(),xs))
    sum(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sum(xs,ys))
   S:
    plus{AC,#}(plusAC(x9,x10),x11) -> plus{AC,#}(x9,x10)
    plus{AC,#}(x9,plusAC(x10,x11)) -> plus{AC,#}(x10,x11)
   Open