MAYBE
Time: 0.518

Problem:
 Equations:
  plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
  plusAC(x4,x5) -> plusAC(x5,x4)
  sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6))
  sumAC(x4,x5) -> sumAC(x5,x4)
  plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
  plusAC(x5,x4) -> plusAC(x4,x5)
  sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6)
  sumAC(x5,x4) -> sumAC(x4,x5)
 TRS:
  plusAC(x,0()) -> x
  plusAC(x,s(y)) -> s(plusAC(x,y))
  sumAC(nil(),nil()) -> 0()
  sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil()))
  sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs))
  sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(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)
   sum{AC,#}(sumAC(x4,x5),x6) -> sum{AC,#}(x4,sumAC(x5,x6))
   sum{AC,#}(x4,x5) -> sum{AC,#}(x5,x4)
   plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
   plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
   sum{AC,#}(x4,sumAC(x5,x6)) -> sum{AC,#}(sumAC(x4,x5),x6)
   sum{AC,#}(x5,x4) -> sum{AC,#}(x4,x5)
  DPs:
   plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y)
   sum{AC,#}(cons(x,xs),nil()) -> sum{AC,#}(xs,nil())
   sum{AC,#}(cons(x,xs),nil()) -> plus{AC,#}(x,sumAC(xs,nil()))
   sum{AC,#}(nil(),cons(x,xs)) -> sum{AC,#}(nil(),xs)
   sum{AC,#}(nil(),cons(x,xs)) -> plus{AC,#}(x,sumAC(nil(),xs))
   sum{AC,#}(cons(x,xs),cons(y,ys)) -> sum{AC,#}(xs,ys)
   sum{AC,#}(cons(x,xs),cons(y,ys)) -> plus{AC,#}(x,y)
   sum{AC,#}(cons(x,xs),cons(y,ys)) -> plus{AC,#}(plusAC(x,y),sumAC(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)))
   sum{AC,#}(x9,sumAC(nil(),nil())) -> sum{AC,#}(x9,0())
   sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(xs,nil())
   sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> plus{AC,#}(x,sumAC(xs,nil()))
   sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(x10,plusAC(x,sumAC(xs,nil())))
   sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(nil(),xs)
   sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> plus{AC,#}(x,sumAC(nil(),xs))
   sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(x11,plusAC(x,sumAC(nil(),xs)))
   sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(xs,ys)
   sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> plus{AC,#}(x,y)
   sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> plus{AC,#}(plusAC(x,y),sumAC(xs,ys))
   sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(x12,plusAC(plusAC(x,y),sumAC(xs,ys)))
  Equations:
   plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
   plusAC(x4,x5) -> plusAC(x5,x4)
   sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6))
   sumAC(x4,x5) -> sumAC(x5,x4)
   plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
   plusAC(x5,x4) -> plusAC(x4,x5)
   sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6)
   sumAC(x5,x4) -> sumAC(x4,x5)
  TRS:
   plusAC(x,0()) -> x
   plusAC(x,s(y)) -> s(plusAC(x,y))
   sumAC(nil(),nil()) -> 0()
   sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil()))
   sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs))
   sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys))
  S:
   plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14)
   plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15)
   sum{AC,#}(sumAC(x13,x14),x15) -> sum{AC,#}(x13,x14)
   sum{AC,#}(x13,sumAC(x14,x15)) -> sum{AC,#}(x14,x15)
  AC-EDG Processor:
   Equations#:
    plus{AC,#}(plusAC(x4,x5),x6) -> plus{AC,#}(x4,plusAC(x5,x6))
    plus{AC,#}(x4,x5) -> plus{AC,#}(x5,x4)
    sum{AC,#}(sumAC(x4,x5),x6) -> sum{AC,#}(x4,sumAC(x5,x6))
    sum{AC,#}(x4,x5) -> sum{AC,#}(x5,x4)
    plus{AC,#}(x4,plusAC(x5,x6)) -> plus{AC,#}(plusAC(x4,x5),x6)
    plus{AC,#}(x5,x4) -> plus{AC,#}(x4,x5)
    sum{AC,#}(x4,sumAC(x5,x6)) -> sum{AC,#}(sumAC(x4,x5),x6)
    sum{AC,#}(x5,x4) -> sum{AC,#}(x4,x5)
   DPs:
    plus{AC,#}(x,s(y)) -> plus{AC,#}(x,y)
    sum{AC,#}(cons(x,xs),nil()) -> sum{AC,#}(xs,nil())
    sum{AC,#}(cons(x,xs),nil()) -> plus{AC,#}(x,sumAC(xs,nil()))
    sum{AC,#}(nil(),cons(x,xs)) -> sum{AC,#}(nil(),xs)
    sum{AC,#}(nil(),cons(x,xs)) -> plus{AC,#}(x,sumAC(nil(),xs))
    sum{AC,#}(cons(x,xs),cons(y,ys)) -> sum{AC,#}(xs,ys)
    sum{AC,#}(cons(x,xs),cons(y,ys)) -> plus{AC,#}(x,y)
    sum{AC,#}(cons(x,xs),cons(y,ys)) -> plus{AC,#}(plusAC(x,y),sumAC(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)))
    sum{AC,#}(x9,sumAC(nil(),nil())) -> sum{AC,#}(x9,0())
    sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(xs,nil())
    sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> plus{AC,#}(x,sumAC(xs,nil()))
    sum{AC,#}(x10,sumAC(cons(x,xs),nil())) -> sum{AC,#}(x10,plusAC(x,sumAC(xs,nil())))
    sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(nil(),xs)
    sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> plus{AC,#}(x,sumAC(nil(),xs))
    sum{AC,#}(x11,sumAC(nil(),cons(x,xs))) -> sum{AC,#}(x11,plusAC(x,sumAC(nil(),xs)))
    sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(xs,ys)
    sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> plus{AC,#}(x,y)
    sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> plus{AC,#}(plusAC(x,y),sumAC(xs,ys))
    sum{AC,#}(x12,sumAC(cons(x,xs),cons(y,ys))) -> sum{AC,#}(x12,plusAC(plusAC(x,y),sumAC(xs,ys)))
   Equations:
    plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
    plusAC(x4,x5) -> plusAC(x5,x4)
    sumAC(sumAC(x4,x5),x6) -> sumAC(x4,sumAC(x5,x6))
    sumAC(x4,x5) -> sumAC(x5,x4)
    plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
    plusAC(x5,x4) -> plusAC(x4,x5)
    sumAC(x4,sumAC(x5,x6)) -> sumAC(sumAC(x4,x5),x6)
    sumAC(x5,x4) -> sumAC(x4,x5)
   TRS:
    plusAC(x,0()) -> x
    plusAC(x,s(y)) -> s(plusAC(x,y))
    sumAC(nil(),nil()) -> 0()
    sumAC(cons(x,xs),nil()) -> plusAC(x,sumAC(xs,nil()))
    sumAC(nil(),cons(x,xs)) -> plusAC(x,sumAC(nil(),xs))
    sumAC(cons(x,xs),cons(y,ys)) -> plusAC(plusAC(x,y),sumAC(xs,ys))
   S:
    plus{AC,#}(plusAC(x13,x14),x15) -> plus{AC,#}(x13,x14)
    plus{AC,#}(x13,plusAC(x14,x15)) -> plus{AC,#}(x14,x15)
    sum{AC,#}(sumAC(x13,x14),x15) -> sum{AC,#}(x13,x14)
    sum{AC,#}(x13,sumAC(x14,x15)) -> sum{AC,#}(x14,x15)
   Open