YES
Time: 0.412

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) = 0
        pi(false) = []
        pi(nil) = []
        pi(rm) = [1]
        pi(add) = [1]
        pi(if_rm) = [2]
        pi(purge#) = [0]
       precedence:
        purge# > rm > if_rm ~ add ~ nil ~ false ~ s ~ true ~ 0 ~ eqC
        weight function:
         [purge#](x0) = 4x0,
         
         [if_rm](x0, x1, x2) = 2x2 + 2,
         
         [add](x0, x1) = 2x1 + 4,
         
         [rm](x0, x1) = 2x1 + 2,
         
         [nil] = 3,
         
         [false] = 4,
         
         [s](x0) = x0,
         
         [true] = 1,
         
         [0] = 4,
         
         [eqC](x0, x1) = 2
         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))
         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#) = [0,2]
        precedence:
         s > eqC > rm# > if_rm# ~ add ~ false ~ true ~ 0
         weight function:
          [if_rm#](x0, x1, x2) = 5x0 + x2 + 1,
          
          [rm#](x0, x1) = 5x1 + 2,
          
          [add](x0, x1) = 5x0 + 5x1 + 4,
          
          [false] = 1,
          
          [s](x0) = 4x0 + 4,
          
          [true] = 2,
          
          [0] = 4,
          
          [eqC](x0, x1) = 2
          usable rules:
           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:
            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:
          s > eq{C,#}
          weight function:
           [eq{C,#}](x0, x1) = 2x0 + 2x1 + 1,
           
           [s](x0) = x0
           usable rules:
            
           problem:
            Equations#:
             
            DPs:
             
            Equations:
             
            TRS:
             
            S:
             
           Qed