YES
Time: 0.020

Problem:
 Equations:
  plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
  plusAC(x4,x5) -> plusAC(x5,x4)
  appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
  appAC(x4,x5) -> appAC(x5,x4)
  plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
  plusAC(x5,x4) -> plusAC(x4,x5)
  appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
  appAC(x5,x4) -> appAC(x4,x5)
 TRS:
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  eq(0(),0()) -> true()
  eq(0(),s(x)) -> false()
  eq(s(x),s(y)) -> eq(x,y)
  plusAC(empty(),x) -> x
  appAC(x,empty()) -> empty()
  appAC(x,appAC(empty(),z)) -> appAC(empty(),z)
  appAC(x,plusAC(y,z)) -> plusAC(appAC(x,y),appAC(x,z))
  appAC(x,appAC(plusAC(y,z),t)) -> appAC(plusAC(appAC(x,y),appAC(x,z)),t)
  appAC(singl(x),singl(y)) -> if(eq(x,y),singl(x),empty())

Proof:
 AC-RPO Processor:
  precedence:
   s > 0 > appAC > if > eq > plusAC > false > true > singl > empty
  status:
   eq:mul  if:mul  
  problem:
   Equations:
    plusAC(plusAC(x4,x5),x6) -> plusAC(x4,plusAC(x5,x6))
    plusAC(x4,x5) -> plusAC(x5,x4)
    appAC(appAC(x4,x5),x6) -> appAC(x4,appAC(x5,x6))
    appAC(x4,x5) -> appAC(x5,x4)
    plusAC(x4,plusAC(x5,x6)) -> plusAC(plusAC(x4,x5),x6)
    plusAC(x5,x4) -> plusAC(x4,x5)
    appAC(x4,appAC(x5,x6)) -> appAC(appAC(x4,x5),x6)
    appAC(x5,x4) -> appAC(x4,x5)
   TRS:
    
  Qed