ceta_eq: termination proof not accepted
1: error below switch to dependency pairs
1.1: error below the dependency graph processor
 1.1.3: error when applying the reduction pair processor with usable rules to remove from the DP problem
  pairs:
  
  quicksort#(add(n, x)) -> quicksort#(low(n, x))
  quicksort#(add(n, x)) -> quicksort#(high(n, x))
  rules:
  
  app(nil, y) -> y
  app(add(n, x), y) -> add(n, app(x, y))
  high(n, nil) -> nil
  high(n, add(m, x)) -> if_high(le(m, n), n, add(m, x))
  if_high(true, n, add(m, x)) -> high(n, x)
  if_high(false, n, add(m, x)) -> add(m, high(n, x))
  if_low(true, n, add(m, x)) -> add(m, low(n, x))
  if_low(false, n, add(m, x)) -> low(n, x)
  le(0, y) -> true
  le(s(x), 0) -> false
  le(s(x), s(y)) -> le(x, y)
  low(n, nil) -> nil
  low(n, add(m, x)) -> if_low(le(m, n), n, add(m, x))
  minus(x, 0) -> x
  minus(s(x), s(y)) -> minus(x, y)
  quicksort(nil) -> nil
  quicksort(add(n, x)) -> app(quicksort(low(n, x)), add(n, quicksort(high(n, x))))
  quot(0, s(y)) -> 0
  quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
  
   the pairs 
  quicksort#(add(n, x)) -> quicksort#(low(n, x))
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MAX and the level mapping defined by 
  pi(quicksort#) = [(epsilon,0),(1,1)]
  Argument Filter: 
  pi(quicksort#/1) = 1
  pi(add/2) = [2]
  pi(high/2) = [2]
  pi(low/2) = 2
  pi(nil/0) = []
  pi(if_high/3) = [3]
  pi(le/2) = [1,2]
  pi(true/0) = []
  pi(if_low/3) = 3
  pi(false/0) = []
  pi(0/0) = []
  pi(s/1) = []
  
  RPO with the following precedence
  precedence(add[2]) = 1
  precedence(high[2]) = 1
  precedence(nil[0]) = 1
  precedence(if_high[3]) = 1
  precedence(le[2]) = 0
  precedence(true[0]) = 2
  precedence(false[0]) = 0
  precedence(0[0]) = 0
  precedence(s[1]) = 0
  
  precedence(_) = 0
  and the following status
  status(add[2]) = mul
  status(high[2]) = mul
  status(nil[0]) = mul
  status(if_high[3]) = mul
  status(le[2]) = mul
  status(true[0]) = mul
  status(false[0]) = mul
  status(0[0]) = mul
  status(s[1]) = mul
  
  status(_) = lex
  
  problem when orienting (usable) rules
  could not orient if_high(false, n, add(m, x)) >= add(m, high(n, x))
  pi( if_high(false, n, add(m, x)) ) = if_high(add(x))
  pi( add(m, high(n, x)) ) = add(high(x))
  could not orient if_high(add(x)) >=RPO add(high(x))