YES
Time: 0.017

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:
 AC-RPO Processor:
  precedence:
   sum > nil > plusAC > cons > s > 0
  status:
   cons:mul  sum:mul  
  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:
    
  Qed