ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.2: error when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  h2#(x, j(y, h1(z, u)), h1(z, u)) -> h2#(s(x), y, h1(s(z), u))
  rules:
  
  f(j(x, y), y) -> g(f(x, k(y)))
  f(x, h1(y, z)) -> h2(0, x, h1(y, z))
  g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
  h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
  i(f(x, h(y))) -> y
  i(h2(s(x), y, h1(x, z))) -> z
  k(h(x)) -> h1(0, x)
  k(h1(x, y)) -> h1(s(x), y)
  
   the pairs 
  h2#(x, j(y, h1(z, u)), h1(z, u)) -> h2#(s(x), y, h1(s(z), u))
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MS and the level mapping defined by 
  pi(h2#) = [(2,0),(3,1)]
  Argument Filter: 
  pi(h2#/3) = [1,2,3]
  pi(j/2) = [1]
  pi(h1/2) = 2
  pi(s/1) = [1]
  
  RPO with the following precedence
  precedence(j[2]) = 0
  precedence(s[1]) = 1
  precedence(h2#[3]) = 2
  
  precedence(_) = 0
  and the following status
  status(j[2]) = lex
  status(s[1]) = lex
  status(h2#[3]) = lex
  
  status(_) = lex
  
  problem when orienting DPs
  cannot orient pair h2#(x, j(y, h1(z, u)), h1(z, u)) -> h2#(s(x), y, h1(s(z), u)) strictly:
  [(j(y, h1(z, u)),0),(h1(z, u),1)] >mu [(y,0),(h1(s(z), u),1)] could not be ensured