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:
  
  qsort#(add(N, X)) -> f_3#(split(N, X), N, X)
  f_3#(pair(Y, Z), N, X) -> qsort#(Y)
  f_3#(pair(Y, Z), N, X) -> qsort#(Z)
  rules:
  
  append(nil, Y) -> Y
  append(add(N, X), Y) -> add(N, append(X, Y))
  f_1(pair(X, Z), N, M, Y) -> f_2(lt(N, M), N, M, Y, X, Z)
  f_2(true, N, M, Y, X, Z) -> pair(X, add(M, Z))
  f_2(false, N, M, Y, X, Z) -> pair(add(M, X), Z)
  f_3(pair(Y, Z), N, X) -> append(qsort(Y), add(X, qsort(Z)))
  lt(0, s(X)) -> true
  lt(s(X), 0) -> false
  lt(s(X), s(Y)) -> lt(X, Y)
  qsort(nil) -> nil
  qsort(add(N, X)) -> f_3(split(N, X), N, X)
  split(N, nil) -> pair(nil, nil)
  split(N, add(M, Y)) -> f_1(split(N, Y), N, M, Y)
  
   the pairs 
  f_3#(pair(Y, Z), N, X) -> qsort#(Y)
  f_3#(pair(Y, Z), N, X) -> qsort#(Z)
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MAX and the level mapping defined by 
  pi(qsort#) = [(epsilon,0),(1,2)]
  pi(f_3#) = [(1,2),(3,5)]
  Argument Filter: 
  pi(qsort#/1) = 1
  pi(add/2) = [2]
  pi(f_3#/3) = [1,2]
  pi(split/2) = [2]
  pi(pair/2) = [1,2]
  pi(nil/0) = []
  pi(f_1/4) = [1]
  pi(f_2/6) = [1,5,6]
  pi(lt/2) = []
  pi(0/0) = []
  pi(s/1) = 1
  pi(true/0) = []
  pi(false/0) = []
  
  RPO with the following precedence
  precedence(add[2]) = 4
  precedence(f_3#[3]) = 0
  precedence(split[2]) = 4
  precedence(pair[2]) = 2
  precedence(nil[0]) = 3
  precedence(f_1[4]) = 4
  precedence(f_2[6]) = 4
  precedence(lt[2]) = 2
  precedence(0[0]) = 5
  precedence(true[0]) = 1
  precedence(false[0]) = 2
  
  precedence(_) = 0
  and the following status
  status(add[2]) = mul
  status(f_3#[3]) = mul
  status(split[2]) = mul
  status(pair[2]) = mul
  status(nil[0]) = mul
  status(f_1[4]) = mul
  status(f_2[6]) = mul
  status(lt[2]) = mul
  status(0[0]) = mul
  status(true[0]) = mul
  status(false[0]) = mul
  
  status(_) = lex
  
  problem when orienting (usable) rules
  could not orient split(N, add(M, Y)) >= f_1(split(N, Y), N, M, Y)
  pi( split(N, add(M, Y)) ) = split(add(Y))
  pi( f_1(split(N, Y), N, M, Y) ) = f_1(split(Y))
  could not orient split(add(Y)) >=RPO f_1(split(Y))