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 below the reduction pair processor
  1.1.2.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
   pairs:
   
   min#(min(X, Y), Z) -> min#(X, plus(Y, Z))
   rules:
   
   min(X, 0) -> X
   min(s(X), s(Y)) -> min(X, Y)
   min(min(X, Y), Z) -> min(X, plus(Y, Z))
   plus(0, Y) -> Y
   plus(s(X), Y) -> s(plus(X, Y))
   quot(0, s(Y)) -> 0
   quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
   
    the pairs 
   min#(min(X, Y), Z) -> min#(X, plus(Y, Z))
   
   could not apply the generic root reduction pair processor with the following
   SCNP-version with mu = MS and the level mapping defined by 
   pi(min#) = [(epsilon,0),(2,1)]
   Argument Filter: 
   pi(min#/2) = [1]
   pi(min/2) = [1,2]
   pi(Z/0) = []
   pi(plus/2) = 2
   pi(0/0) = []
   pi(s/1) = 1
   
   RPO with the following precedence
   precedence(min#[2]) = 0
   precedence(min[2]) = 1
   precedence(Z[0]) = 2
   precedence(0[0]) = 3
   
   precedence(_) = 0
   and the following status
   status(min#[2]) = mul
   status(min[2]) = mul
   status(Z[0]) = mul
   status(0[0]) = mul
   
   status(_) = lex
   
   problem when orienting DPs
   cannot orient pair min#(min(X, Y), Z) -> min#(X, plus(Y, Z)) strictly:
   [(min#(min(X, Y), Z),0),(Z,1)] >mu [(min#(X, plus(Y, Z)),0),(plus(Y, Z),1)] could not be ensured