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:
  
  quicksort#(cons(N, L)) -> quicksort#(low(N, L))
  quicksort#(cons(N, L)) -> quicksort#(high(N, L))
  rules:
  
  app(nil, Y) -> Y
  app(cons(N, L), Y) -> cons(N, app(L, Y))
  high(N, nil) -> nil
  high(N, cons(M, L)) -> ifhigh(le(M, N), N, cons(M, L))
  ifhigh(true, N, cons(M, L)) -> high(N, L)
  ifhigh(false, N, cons(M, L)) -> cons(M, high(N, L))
  iflow(true, N, cons(M, L)) -> cons(M, low(N, L))
  iflow(false, N, cons(M, L)) -> low(N, L)
  le(0, Y) -> true
  le(s(X), 0) -> false
  le(s(X), s(Y)) -> le(X, Y)
  low(N, nil) -> nil
  low(N, cons(M, L)) -> iflow(le(M, N), N, cons(M, L))
  quicksort(nil) -> nil
  quicksort(cons(N, L)) -> app(quicksort(low(N, L)), cons(N, quicksort(high(N, L))))
  
   the pairs 
  quicksort#(cons(N, L)) -> quicksort#(low(N, L))
  
  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(cons/2) = [2]
  pi(high/2) = [2]
  pi(low/2) = 2
  pi(nil/0) = []
  pi(ifhigh/3) = [3]
  pi(le/2) = [1,2]
  pi(true/0) = []
  pi(iflow/3) = 3
  pi(false/0) = []
  pi(0/0) = []
  pi(s/1) = []
  
  RPO with the following precedence
  precedence(cons[2]) = 1
  precedence(high[2]) = 1
  precedence(nil[0]) = 1
  precedence(ifhigh[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(cons[2]) = mul
  status(high[2]) = mul
  status(nil[0]) = mul
  status(ifhigh[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 ifhigh(false, N, cons(M, L)) >= cons(M, high(N, L))
  pi( ifhigh(false, N, cons(M, L)) ) = ifhigh(cons(L))
  pi( cons(M, high(N, L)) ) = cons(high(L))
  could not orient ifhigh(cons(L)) >=RPO cons(high(L))