MAYBE

Problem:
 eq(0(),0()) -> true()
 eq(0(),s(X)) -> false()
 eq(s(X),0()) -> false()
 eq(s(X),s(Y)) -> eq(X,Y)
 rm(N,nil()) -> nil()
 rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
 ifrm(true(),N,add(M,X)) -> rm(N,X)
 ifrm(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:
  DPs:
   eq#(s(X),s(Y)) -> eq#(X,Y)
   rm#(N,add(M,X)) -> eq#(N,M)
   rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X))
   ifrm#(true(),N,add(M,X)) -> rm#(N,X)
   ifrm#(false(),N,add(M,X)) -> rm#(N,X)
   purge#(add(N,X)) -> rm#(N,X)
   purge#(add(N,X)) -> purge#(rm(N,X))
  TRS:
   eq(0(),0()) -> true()
   eq(0(),s(X)) -> false()
   eq(s(X),0()) -> false()
   eq(s(X),s(Y)) -> eq(X,Y)
   rm(N,nil()) -> nil()
   rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
   ifrm(true(),N,add(M,X)) -> rm(N,X)
   ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
   purge(nil()) -> nil()
   purge(add(N,X)) -> add(N,purge(rm(N,X)))
  Usable Rule Processor:
   DPs:
    eq#(s(X),s(Y)) -> eq#(X,Y)
    rm#(N,add(M,X)) -> eq#(N,M)
    rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X))
    ifrm#(true(),N,add(M,X)) -> rm#(N,X)
    ifrm#(false(),N,add(M,X)) -> rm#(N,X)
    purge#(add(N,X)) -> rm#(N,X)
    purge#(add(N,X)) -> purge#(rm(N,X))
   TRS:
    f14(x,y) -> x
    f14(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)
    rm(N,nil()) -> nil()
    rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
    ifrm(true(),N,add(M,X)) -> rm(N,X)
    ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
   TDG Processor:
    DPs:
     eq#(s(X),s(Y)) -> eq#(X,Y)
     rm#(N,add(M,X)) -> eq#(N,M)
     rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X))
     ifrm#(true(),N,add(M,X)) -> rm#(N,X)
     ifrm#(false(),N,add(M,X)) -> rm#(N,X)
     purge#(add(N,X)) -> rm#(N,X)
     purge#(add(N,X)) -> purge#(rm(N,X))
    TRS:
     f14(x,y) -> x
     f14(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)
     rm(N,nil()) -> nil()
     rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
     ifrm(true(),N,add(M,X)) -> rm(N,X)
     ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
    graph:
     purge#(add(N,X)) -> purge#(rm(N,X)) ->
     purge#(add(N,X)) -> purge#(rm(N,X))
     purge#(add(N,X)) -> purge#(rm(N,X)) ->
     purge#(add(N,X)) -> rm#(N,X)
     purge#(add(N,X)) -> rm#(N,X) ->
     rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X))
     purge#(add(N,X)) -> rm#(N,X) ->
     rm#(N,add(M,X)) -> eq#(N,M)
     ifrm#(false(),N,add(M,X)) -> rm#(N,X) ->
     rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X))
     ifrm#(false(),N,add(M,X)) -> rm#(N,X) ->
     rm#(N,add(M,X)) -> eq#(N,M)
     ifrm#(true(),N,add(M,X)) -> rm#(N,X) ->
     rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X))
     ifrm#(true(),N,add(M,X)) -> rm#(N,X) ->
     rm#(N,add(M,X)) -> eq#(N,M)
     rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X)) ->
     ifrm#(false(),N,add(M,X)) -> rm#(N,X)
     rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X)) ->
     ifrm#(true(),N,add(M,X)) -> rm#(N,X)
     rm#(N,add(M,X)) -> eq#(N,M) -> eq#(s(X),s(Y)) -> eq#(X,Y)
     eq#(s(X),s(Y)) -> eq#(X,Y) -> eq#(s(X),s(Y)) -> eq#(X,Y)
    Restore Modifier:
     DPs:
      eq#(s(X),s(Y)) -> eq#(X,Y)
      rm#(N,add(M,X)) -> eq#(N,M)
      rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X))
      ifrm#(true(),N,add(M,X)) -> rm#(N,X)
      ifrm#(false(),N,add(M,X)) -> rm#(N,X)
      purge#(add(N,X)) -> rm#(N,X)
      purge#(add(N,X)) -> purge#(rm(N,X))
     TRS:
      eq(0(),0()) -> true()
      eq(0(),s(X)) -> false()
      eq(s(X),0()) -> false()
      eq(s(X),s(Y)) -> eq(X,Y)
      rm(N,nil()) -> nil()
      rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
      ifrm(true(),N,add(M,X)) -> rm(N,X)
      ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
      purge(nil()) -> nil()
      purge(add(N,X)) -> add(N,purge(rm(N,X)))
     SCC Processor:
      #sccs: 3
      #rules: 5
      #arcs: 12/49
      DPs:
       purge#(add(N,X)) -> purge#(rm(N,X))
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(X)) -> false()
       eq(s(X),0()) -> false()
       eq(s(X),s(Y)) -> eq(X,Y)
       rm(N,nil()) -> nil()
       rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
       ifrm(true(),N,add(M,X)) -> rm(N,X)
       ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
       purge(nil()) -> nil()
       purge(add(N,X)) -> add(N,purge(rm(N,X)))
      Open
      
      DPs:
       rm#(N,add(M,X)) -> ifrm#(eq(N,M),N,add(M,X))
       ifrm#(true(),N,add(M,X)) -> rm#(N,X)
       ifrm#(false(),N,add(M,X)) -> rm#(N,X)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(X)) -> false()
       eq(s(X),0()) -> false()
       eq(s(X),s(Y)) -> eq(X,Y)
       rm(N,nil()) -> nil()
       rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
       ifrm(true(),N,add(M,X)) -> rm(N,X)
       ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
       purge(nil()) -> nil()
       purge(add(N,X)) -> add(N,purge(rm(N,X)))
      Open
      
      DPs:
       eq#(s(X),s(Y)) -> eq#(X,Y)
      TRS:
       eq(0(),0()) -> true()
       eq(0(),s(X)) -> false()
       eq(s(X),0()) -> false()
       eq(s(X),s(Y)) -> eq(X,Y)
       rm(N,nil()) -> nil()
       rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
       ifrm(true(),N,add(M,X)) -> rm(N,X)
       ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
       purge(nil()) -> nil()
       purge(add(N,X)) -> add(N,purge(rm(N,X)))
      Open