ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  purge#(add(N, X)) -> purge#(rm(N, X))
  rules:
  
  eq(0, 0) -> true
  eq(0, s(X)) -> false
  eq(s(X), 0) -> false
  eq(s(X), s(Y)) -> eq(X, Y)
  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)))
  rm(N, nil) -> nil
  rm(N, add(M, X)) -> ifrm(eq(N, M), N, add(M, X))
  
   the pairs 
  purge#(add(N, X)) -> purge#(rm(N, X))
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MS and the level mapping defined by 
  pi(purge#) = [(epsilon,0),(1,1)]
  Argument Filter: 
  pi(purge#/1) = []
  pi(add/2) = [2,1]
  pi(rm/2) = 2
  pi(nil/0) = []
  pi(ifrm/3) = 3
  pi(eq/2) = 1
  pi(true/0) = []
  pi(false/0) = []
  pi(0/0) = []
  pi(s/1) = []
  
  RPO with the following precedence
  precedence(purge#[1]) = 1
  precedence(add[2]) = 0
  precedence(nil[0]) = 2
  precedence(true[0]) = 3
  precedence(false[0]) = 4
  precedence(0[0]) = 3
  precedence(s[1]) = 5
  
  precedence(_) = 0
  and the following status
  status(purge#[1]) = lex
  status(add[2]) = lex
  status(nil[0]) = lex
  status(true[0]) = lex
  status(false[0]) = lex
  status(0[0]) = lex
  status(s[1]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair purge#(add(N, X)) -> purge#(rm(N, X)) strictly:
  [(purge#(add(N, X)),0),(add(N, X),1)] >mu [(purge#(rm(N, X)),0),(rm(N, X),1)] could not be ensured