ceta_equiv: 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:
  
  din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)
  din#(der(plus(X, Y))) -> din#(der(X))
  u21#(dout(DX), X, Y) -> din#(der(Y))
  din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)
  din#(der(times(X, Y))) -> din#(der(X))
  u31#(dout(DX), X, Y) -> din#(der(Y))
  din#(der(der(X))) -> u41#(din(der(X)), X)
  din#(der(der(X))) -> din#(der(X))
  u41#(dout(DX), X) -> din#(der(DX))
  rules:
  
  din(der(plus(X, Y))) -> u21(din(der(X)), X, Y)
  din(der(times(X, Y))) -> u31(din(der(X)), X, Y)
  din(der(der(X))) -> u41(din(der(X)), X)
  u21(dout(DX), X, Y) -> u22(din(der(Y)), X, Y, DX)
  u22(dout(DY), X, Y, DX) -> dout(plus(DX, DY))
  u31(dout(DX), X, Y) -> u32(din(der(Y)), X, Y, DX)
  u32(dout(DY), X, Y, DX) -> dout(plus(times(X, DY), times(Y, DX)))
  u41(dout(DX), X) -> u42(din(der(DX)), X, DX)
  u42(dout(DDX), X, DX) -> dout(DDX)
  
   the pairs 
  din#(der(plus(X, Y))) -> u21#(din(der(X)), X, Y)
  u21#(dout(DX), X, Y) -> din#(der(Y))
  din#(der(times(X, Y))) -> u31#(din(der(X)), X, Y)
  u41#(dout(DX), X) -> din#(der(DX))
  
  could not apply the generic root reduction pair processor with the following
  SCNP-version with mu = MAX and the level mapping defined by 
  pi(u21#) = [(1,12)]
  pi(din#) = [(epsilon,0),(1,1)]
  pi(u31#) = [(1,0)]
  pi(u41#) = [(epsilon,0),(1,9)]
  Argument Filter: 
  pi(u21#/3) = [1,2,3]
  pi(dout/1) = [1]
  pi(din#/1) = [1]
  pi(der/1) = []
  pi(plus/2) = 1
  pi(din/1) = 1
  pi(times/2) = 2
  pi(u31#/3) = [1,2,3]
  pi(u41#/2) = [1]
  pi(u21/3) = 1
  pi(u31/3) = 1
  pi(u41/2) = 1
  pi(u32/4) = [1]
  pi(u22/4) = [4]
  pi(u42/3) = 1
  
  RPO with the following precedence
  precedence(u21#[3]) = 1
  precedence(dout[1]) = 0
  precedence(din#[1]) = 0
  precedence(der[1]) = 0
  precedence(u31#[3]) = 0
  precedence(u41#[2]) = 0
  precedence(u32[4]) = 0
  precedence(u22[4]) = 0
  
  precedence(_) = 0
  and the following status
  status(u21#[3]) = mul
  status(dout[1]) = mul
  status(din#[1]) = mul
  status(der[1]) = mul
  status(u31#[3]) = mul
  status(u41#[2]) = mul
  status(u32[4]) = mul
  status(u22[4]) = mul
  
  status(_) = lex
  
  problem when orienting (usable) rules
  could not orient u31(dout(DX), X, Y) >= u32(din(der(Y)), X, Y, DX)
  pi( u31(dout(DX), X, Y) ) = dout(DX)
  pi( u32(din(der(Y)), X, Y, DX) ) = u32(der)
  could not orient dout(DX) >=RPO u32(der)