YES
Time: 0.301

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-KBO Processor:
       argument filtering:
        pi(eqC) = []
        pi(0) = []
        pi(true) = []
        pi(s) = []
        pi(false) = []
        pi(nil) = []
        pi(rm) = 1
        pi(add) = [1]
        pi(if_rm) = 2
        pi(purge#) = 0
       precedence:
        eqC > purge# ~ if_rm ~ add ~ rm ~ nil ~ false ~ s ~ true ~ 0
        weight function:
         w0 = 1
         w(s) = 7
         w(if_rm) = w(add) = w(0) = 4
         w(purge#) = w(nil) = w(false) = w(true) = w(eqC) = 1
         w(rm) = 0
         usable rules:
          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)
         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-KBO Processor:
        argument filtering:
         pi(eqC) = []
         pi(0) = []
         pi(true) = []
         pi(s) = 0
         pi(false) = []
         pi(add) = [0,1]
         pi(rm#) = [1]
         pi(if_rm#) = 2
        precedence:
         if_rm# ~ rm# ~ false ~ s ~ true ~ 0 ~ eqC > add
         weight function:
          w0 = 1
          w(s) = 6
          w(false) = w(true) = w(0) = 4
          w(add) = 3
          w(if_rm#) = w(eqC) = 1
          w(rm#) = 0
          usable rules:
           
          problem:
           Equations#:
            
           DPs:
            
           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:
            
          Qed
      
      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-KBO Processor:
         argument filtering:
          pi(s) = [0]
          pi(eq{C,#}) = [0,1]
         precedence:
          eq{C,#} ~ s
          weight function:
           w0 = 2
           w(eq{C,#}) = 2
           w(s) = 0
           usable rules:
            
           problem:
            Equations#:
             
            DPs:
             
            Equations:
             
            TRS:
             
            S:
             
           Qed