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 below the reduction pair processor
  1.1.1.1: error below the reduction pair processor
   1.1.1.1.1: error below the dependency graph processor
    1.1.1.1.1.1: error below the reduction pair processor
     1.1.1.1.1.1.1: error when applying the reduction pair processor with usable rules to remove from the DP problem
      pairs:
      
      Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)
      Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)
      Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)
      Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)
      Term_sub#(Term_inl(m), s) -> Term_sub#(m, s)
      Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))
      rules:
      
      Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))
      Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t))
      Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t))
      Concat(Id, s) -> s
      Frozen(m, Sum_constant(Left), n, s) -> Term_sub(m, s)
      Frozen(m, Sum_constant(Right), n, s) -> Term_sub(n, s)
      Frozen(m, Sum_term_var(xi), n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s))
      Sum_sub(xi, Id) -> Sum_term_var(xi)
      Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant(k)
      Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s)
      Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s)
      Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s)
      Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s))
      Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s))
      Term_sub(Term_inl(m), s) -> Term_inl(Term_sub(m, s))
      Term_sub(Term_inr(m), s) -> Term_inr(Term_sub(m, s))
      Term_sub(Term_var(x), Id) -> Term_var(x)
      Term_sub(Term_var(x), Cons_usual(y, m, s)) -> m
      Term_sub(Term_var(x), Cons_usual(y, m, s)) -> Term_sub(Term_var(x), s)
      Term_sub(Term_var(x), Cons_sum(xi, k, s)) -> Term_sub(Term_var(x), s)
      Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t))
      
       the pairs 
      Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))
      
      could not apply the generic root reduction pair processor with the following
      SCNP-version with mu = MS and the level mapping defined by 
      pi(Term_sub#) = [(1,3),(2,0)]
      polynomial interpretration over naturals with negative constants
      Pol(Term_sub#(x_1, x_2)) = 1
      Pol(Term_app(x_1, x_2)) = x_2 + x_1
      Pol(Term_pair(x_1, x_2)) = x_2 + x_1
      Pol(Term_inl(x_1)) = x_1
      Pol(Term_sub(x_1, x_2)) = 1 + x_2 + x_1
      Pol(Concat(x_1, x_2)) = x_2
      Pol(Cons_usual(x_1, x_2, x_3)) = 0
      Pol(Cons_sum(x_1, x_2, x_3)) = x_3
      Pol(Id) = 0
      Pol(Term_inr(x_1)) = 1 + x_1
      Pol(Frozen(x_1, x_2, x_3, x_4)) = x_4
      Pol(Sum_constant(x_1)) = 0
      Pol(Left) = 0
      Pol(Case(x_1, x_2, x_3)) = x_3 + x_2 + x_1
      Pol(Sum_sub(x_1, x_2)) = 1
      Pol(Right) = 0
      Pol(Sum_term_var(x_1)) = 1 + x_1
      Pol(Term_var(x_1)) = 1
      problem when orienting DPs
      cannot orient pair Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s) weakly:
      [(Term_app(m, n),3),(s,0)] >=mu [(m,3),(s,0)] could not be ensured