YES
Time: 0.019

Problem:
 Equations:
  
 TRS:
  unAC(empty(),x) -> x
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  eq(0(),0()) -> true()
  eq(0(),s(x)) -> false()
  eq(s(x),0()) -> false()
  eq(s(x),s(y)) -> eq(x,y)
  interAC(x,empty()) -> empty()
  interAC(x,unAC(y,z)) -> unAC(interAC(x,y),interAC(x,z))
  interAC(single(x),single(y)) -> if(eq(x,y),single(x),empty())

Proof:
 AC-RPO Processor:
  precedence:
   s > single > 0 > false > empty > interAC > eq > if > true > unAC
  status:
   eq:mul  if:mul  
  problem:
   Equations:
    
   TRS:
    
  Qed