YES
Time: 0.065

Problem:
 Equations:
  
 TRS:
  eqC(0(),0()) -> true()
  eqC(0(),s(x)) -> false()
  eqC(s(x),0()) -> false()
  eqC(s(x),s(y)) -> eqC(x,y)
  rm(n,nil()) -> nil()
  rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
  if_rm(true(),n,add(m,x)) -> rm(n,x)
  if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
  purge(nil()) -> nil()
  purge(add(n,x)) -> add(n,purge(rm(n,x)))

Proof:
 DP Processor:
  Equations#:
   
  DPs:
   eq{C,#}(s(x),s(y)) -> eq{C,#}(x,y)
   rm#(n,add(m,x)) -> eq{C,#}(n,m)
   rm#(n,add(m,x)) -> if_rm#(eqC(n,m),n,add(m,x))
   if_rm#(true(),n,add(m,x)) -> rm#(n,x)
   if_rm#(false(),n,add(m,x)) -> rm#(n,x)
   purge#(add(n,x)) -> rm#(n,x)
   purge#(add(n,x)) -> purge#(rm(n,x))
  Equations:
   
  TRS:
   eqC(0(),0()) -> true()
   eqC(0(),s(x)) -> false()
   eqC(s(x),0()) -> false()
   eqC(s(x),s(y)) -> eqC(x,y)
   rm(n,nil()) -> nil()
   rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
   if_rm(true(),n,add(m,x)) -> rm(n,x)
   if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
   purge(nil()) -> nil()
   purge(add(n,x)) -> add(n,purge(rm(n,x)))
  S:
   
  AC-EDG Processor:
   Equations#:
    
   DPs:
    eq{C,#}(s(x),s(y)) -> eq{C,#}(x,y)
    rm#(n,add(m,x)) -> eq{C,#}(n,m)
    rm#(n,add(m,x)) -> if_rm#(eqC(n,m),n,add(m,x))
    if_rm#(true(),n,add(m,x)) -> rm#(n,x)
    if_rm#(false(),n,add(m,x)) -> rm#(n,x)
    purge#(add(n,x)) -> rm#(n,x)
    purge#(add(n,x)) -> purge#(rm(n,x))
   Equations:
    
   TRS:
    eqC(0(),0()) -> true()
    eqC(0(),s(x)) -> false()
    eqC(s(x),0()) -> false()
    eqC(s(x),s(y)) -> eqC(x,y)
    rm(n,nil()) -> nil()
    rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
    if_rm(true(),n,add(m,x)) -> rm(n,x)
    if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
    purge(nil()) -> nil()
    purge(add(n,x)) -> add(n,purge(rm(n,x)))
   S:
    
   SCC Processor:
    #sccs: 3
    #rules: 5
    #arcs: 12/49
    Equations#:
     
    DPs:
     purge#(add(n,x)) -> purge#(rm(n,x))
    Equations:
     
    TRS:
     eqC(0(),0()) -> true()
     eqC(0(),s(x)) -> false()
     eqC(s(x),0()) -> false()
     eqC(s(x),s(y)) -> eqC(x,y)
     rm(n,nil()) -> nil()
     rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
     if_rm(true(),n,add(m,x)) -> rm(n,x)
     if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
     purge(nil()) -> nil()
     purge(add(n,x)) -> add(n,purge(rm(n,x)))
    S:
     
    AC-DP unlabeling:
     Equations#:
      
     DPs:
      purge#(add(n,x)) -> purge#(rm(n,x))
     Equations:
      
     TRS:
      eqC(0(),0()) -> true()
      eqC(0(),s(x)) -> false()
      eqC(s(x),0()) -> false()
      eqC(s(x),s(y)) -> eqC(x,y)
      rm(n,nil()) -> nil()
      rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
      if_rm(true(),n,add(m,x)) -> rm(n,x)
      if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
      purge(nil()) -> nil()
      purge(add(n,x)) -> add(n,purge(rm(n,x)))
     S:
      
     Usable Rule Processor:
      Equations#:
       
      DPs:
       purge#(add(n,x)) -> purge#(rm(n,x))
      Equations:
       
      TRS:
       rm(n,nil()) -> nil()
       rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
       if_rm(true(),n,add(m,x)) -> rm(n,x)
       if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
       eqC(0(),0()) -> true()
       eqC(0(),s(x)) -> false()
       eqC(s(x),0()) -> false()
       eqC(s(x),s(y)) -> eqC(x,y)
      S:
       
      AC-RPO Processor:
       argument filtering:
        pi(eqC) = [0,1]
        pi(0) = []
        pi(true) = []
        pi(s) = 0
        pi(false) = []
        pi(nil) = []
        pi(rm) = 1
        pi(add) = [1]
        pi(if_rm) = 2
        pi(purge#) = [0]
       precedence:
        add > purge# > if_rm > nil > rm > false > s > true > 0 > eqC
       status:
        if_rm:mul  add:mul  rm:mul  
       problem:
        Equations#:
         
        DPs:
         
        Equations:
         
        TRS:
         rm(n,nil()) -> nil()
         rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
         if_rm(true(),n,add(m,x)) -> rm(n,x)
         if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
         eqC(0(),0()) -> true()
         eqC(0(),s(x)) -> false()
         eqC(s(x),0()) -> false()
         eqC(s(x),s(y)) -> eqC(x,y)
        S:
         
       Qed
    
    Equations#:
     
    DPs:
     rm#(n,add(m,x)) -> if_rm#(eqC(n,m),n,add(m,x))
     if_rm#(false(),n,add(m,x)) -> rm#(n,x)
     if_rm#(true(),n,add(m,x)) -> rm#(n,x)
    Equations:
     
    TRS:
     eqC(0(),0()) -> true()
     eqC(0(),s(x)) -> false()
     eqC(s(x),0()) -> false()
     eqC(s(x),s(y)) -> eqC(x,y)
     rm(n,nil()) -> nil()
     rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
     if_rm(true(),n,add(m,x)) -> rm(n,x)
     if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
     purge(nil()) -> nil()
     purge(add(n,x)) -> add(n,purge(rm(n,x)))
    S:
     
    AC-DP unlabeling:
     Equations#:
      
     DPs:
      rm#(n,add(m,x)) -> if_rm#(eqC(n,m),n,add(m,x))
      if_rm#(false(),n,add(m,x)) -> rm#(n,x)
      if_rm#(true(),n,add(m,x)) -> rm#(n,x)
     Equations:
      
     TRS:
      eqC(0(),0()) -> true()
      eqC(0(),s(x)) -> false()
      eqC(s(x),0()) -> false()
      eqC(s(x),s(y)) -> eqC(x,y)
      rm(n,nil()) -> nil()
      rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
      if_rm(true(),n,add(m,x)) -> rm(n,x)
      if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
      purge(nil()) -> nil()
      purge(add(n,x)) -> add(n,purge(rm(n,x)))
     S:
      
     Usable Rule Processor:
      Equations#:
       
      DPs:
       rm#(n,add(m,x)) -> if_rm#(eqC(n,m),n,add(m,x))
       if_rm#(false(),n,add(m,x)) -> rm#(n,x)
       if_rm#(true(),n,add(m,x)) -> rm#(n,x)
      Equations:
       
      TRS:
       eqC(0(),0()) -> true()
       eqC(0(),s(x)) -> false()
       eqC(s(x),0()) -> false()
       eqC(s(x),s(y)) -> eqC(x,y)
      S:
       
      AC-RPO Processor:
       argument filtering:
        pi(eqC) = [0,1]
        pi(0) = []
        pi(true) = []
        pi(s) = [0]
        pi(false) = []
        pi(add) = [1]
        pi(rm#) = 1
        pi(if_rm#) = 2
       precedence:
        eqC > add > s > 0 > false > true > if_rm# > rm#
       status:
        if_rm#:mul  rm#:mul  add:mul  
       problem:
        Equations#:
         
        DPs:
         rm#(n,add(m,x)) -> if_rm#(eqC(n,m),n,add(m,x))
        Equations:
         
        TRS:
         eqC(0(),0()) -> true()
         eqC(0(),s(x)) -> false()
         eqC(s(x),0()) -> false()
         eqC(s(x),s(y)) -> eqC(x,y)
        S:
         
       Restore Modifier:
        Equations#:
         
        DPs:
         rm#(n,add(m,x)) -> if_rm#(eqC(n,m),n,add(m,x))
        Equations:
         
        TRS:
         eqC(0(),0()) -> true()
         eqC(0(),s(x)) -> false()
         eqC(s(x),0()) -> false()
         eqC(s(x),s(y)) -> eqC(x,y)
        S:
         
        SCC Processor:
         #sccs: 0
         #rules: 0
         #arcs: 4/1
         
    
    Equations#:
     
    DPs:
     eq{C,#}(s(x),s(y)) -> eq{C,#}(x,y)
    Equations:
     
    TRS:
     eqC(0(),0()) -> true()
     eqC(0(),s(x)) -> false()
     eqC(s(x),0()) -> false()
     eqC(s(x),s(y)) -> eqC(x,y)
     rm(n,nil()) -> nil()
     rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
     if_rm(true(),n,add(m,x)) -> rm(n,x)
     if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
     purge(nil()) -> nil()
     purge(add(n,x)) -> add(n,purge(rm(n,x)))
    S:
     
    AC-DP unlabeling:
     Equations#:
      
     DPs:
      eq{C,#}(s(x),s(y)) -> eq{C,#}(x,y)
     Equations:
      
     TRS:
      eqC(0(),0()) -> true()
      eqC(0(),s(x)) -> false()
      eqC(s(x),0()) -> false()
      eqC(s(x),s(y)) -> eqC(x,y)
      rm(n,nil()) -> nil()
      rm(n,add(m,x)) -> if_rm(eqC(n,m),n,add(m,x))
      if_rm(true(),n,add(m,x)) -> rm(n,x)
      if_rm(false(),n,add(m,x)) -> add(m,rm(n,x))
      purge(nil()) -> nil()
      purge(add(n,x)) -> add(n,purge(rm(n,x)))
     S:
      
     Usable Rule Processor:
      Equations#:
       
      DPs:
       eq{C,#}(s(x),s(y)) -> eq{C,#}(x,y)
      Equations:
       
      TRS:
       
      S:
       
      AC-RPO Processor:
       argument filtering:
        pi(s) = [0]
        pi(eq{C,#}) = []
       precedence:
        eq{C,#} > s
       status:
        
       problem:
        Equations#:
         
        DPs:
         
        Equations:
         
        TRS:
         
        S:
         
       Qed