MAYBE
Time: 0.004844
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))}
 DP:
  DP:
   {               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))}
  UR:
   {               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)),
                        a(x, y) -> x,
                        a(x, y) -> y}
   EDG:
    {(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))
     (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))
     (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))
     (ifrm#(false(), N, add(M, 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)))
     (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> rm#(N, X))
     (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> purge# rm(N, X))}
    EDG:
     {(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))
      (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))
      (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))
      (ifrm#(false(), N, add(M, 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)))
      (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> rm#(N, X))
      (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> purge# rm(N, X))}
     EDG:
      {(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))
       (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))
       (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))
       (ifrm#(false(), N, add(M, 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)))
       (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> rm#(N, X))
       (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> purge# rm(N, X))}
      EDG:
       {(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))
        (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))
        (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))
        (ifrm#(false(), N, add(M, 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)))
        (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> rm#(N, X))
        (purge# add(N, X) -> purge# rm(N, X), purge# add(N, X) -> purge# rm(N, X))}
       STATUS:
        arrows: 0.755102
        SCCS (3):
         Scc:
          {purge# add(N, X) -> purge# rm(N, X)}
         Scc:
          {           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)}
         Scc:
          {eq#(s X, s Y) -> eq#(X, Y)}
         
         SCC (1):
          Strict:
           {purge# add(N, X) -> purge# rm(N, X)}
          Weak:
          {               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
         
         SCC (3):
          Strict:
           {           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)}
          Weak:
          {               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
         
         SCC (1):
          Strict:
           {eq#(s X, s Y) -> eq#(X, Y)}
          Weak:
          {               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