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 to remove from the DP problem
  pairs:
  
  g#(x, c(y)) -> g#(x, g(s(c(y)), y))
  g#(x, c(y)) -> g#(s(c(y)), y)
  rules:
  
  f(0) -> true
  f(1) -> false
  f(s(x)) -> f(x)
  g(s(x), s(y)) -> if(f(x), s(x), s(y))
  g(x, c(y)) -> g(x, g(s(c(y)), y))
  if(true, x, y) -> x
  if(false, x, y) -> y
  
   the pairs 
  g#(x, c(y)) -> g#(s(c(y)), y)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MAX and the level mapping defined by 
  pi(g#) = [(epsilon,0),(2,0)]
  Argument Filter: 
  pi(g#/2) = [1]
  pi(c/1) = [1]
  pi(s/1) = []
  pi(g/2) = [2]
  pi(if/3) = [1,2,3]
  pi(f/1) = []
  pi(0/0) = []
  pi(true/0) = []
  pi(1/0) = []
  pi(false/0) = []
  
  RPO with the following precedence
  precedence(g#[2]) = 0
  precedence(c[1]) = 1
  precedence(s[1]) = 0
  precedence(g[2]) = 1
  precedence(if[3]) = 0
  precedence(f[1]) = 1
  precedence(0[0]) = 1
  precedence(true[0]) = 1
  precedence(1[0]) = 2
  precedence(false[0]) = 1
  
  precedence(_) = 0
  and the following status
  status(g#[2]) = mul
  status(c[1]) = mul
  status(s[1]) = mul
  status(g[2]) = mul
  status(if[3]) = mul
  status(f[1]) = mul
  status(0[0]) = mul
  status(true[0]) = mul
  status(1[0]) = mul
  status(false[0]) = mul
  
  status(_) = lex
  
  problem when orienting (usable) rules
  could not orient g(x, c(y)) >= g(x, g(s(c(y)), y))
  pi( g(x, c(y)) ) = g(c(y))
  pi( g(x, g(s(c(y)), y)) ) = g(g(y))
  could not orient g(c(y)) >=RPO g(g(y))