YES
Time: 0.015

Problem:
 Equations:
  
 TRS:
  if(true(),x,y) -> x
  if(false(),x,y) -> y
  eqC(0(),0()) -> true()
  eqC(0(),s(x)) -> false()
  eqC(s(x),s(y)) -> eqC(x,y)
  unionAC(empty(),x) -> x
  interAC(empty(),x) -> empty()
  interAC(unionAC(y,z),x) -> unionAC(interAC(x,y),interAC(x,z))
  interAC(singl(x),singl(y)) -> if(eqC(x,y),singl(x),empty())

Proof:
 AC-RPO Processor:
  precedence:
   singl > empty > s > 0 > false > true > interAC > eqC > if > unionAC
  status:
   if:mul  eqC:mul  
  problem:
   Equations:
    
   TRS:
    
  Qed