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:
  
  U21#(tt, M, N) -> U22#(tt, activate(M), activate(N))
  U22#(tt, M, N) -> x#(activate(N), activate(M))
  x#(N, s(M)) -> U21#(tt, M, N)
  rules:
  
  U11(tt, M, N) -> U12(tt, activate(M), activate(N))
  U12(tt, M, N) -> s(plus(activate(N), activate(M)))
  U21(tt, M, N) -> U22(tt, activate(M), activate(N))
  U22(tt, M, N) -> plus(x(activate(N), activate(M)), activate(N))
  activate(X) -> X
  plus(N, 0) -> N
  plus(N, s(M)) -> U11(tt, M, N)
  x(N, 0) -> 0
  x(N, s(M)) -> U21(tt, M, N)
  
   the pairs 
  U21#(tt, M, N) -> U22#(tt, activate(M), activate(N))
  x#(N, s(M)) -> U21#(tt, M, N)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MS and the level mapping defined by 
  pi(U22#) = [(epsilon,0),(2,0),(3,0)]
  pi(x#) = [(epsilon,0),(1,0),(2,0)]
  pi(U21#) = [(epsilon,0),(2,1)]
  Argument Filter: 
  pi(U22#/3) = 1
  pi(tt/0) = []
  pi(x#/2) = []
  pi(activate/1) = 1
  pi(s/1) = [1]
  pi(U21#/3) = 3
  
  RPO with the following precedence
  precedence(tt[0]) = 0
  precedence(x#[2]) = 0
  precedence(s[1]) = 1
  
  precedence(_) = 0
  and the following status
  status(tt[0]) = lex
  status(x#[2]) = lex
  status(s[1]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair U22#(tt, M, N) -> x#(activate(N), activate(M)) weakly:
  [(U22#(tt, M, N),0),(M,0),(N,0)] >=mu [(x#(activate(N), activate(M)),0),(activate(N),0),(activate(M),0)] could not be ensured