Input TRS:
    1: Term_sub(Case(m,xi,n),s) -> Frozen(m,Sum_sub(xi,s),n,s)
    2: Frozen(m,Sum_constant(Left()),n,s) -> Term_sub(m,s)
    3: Frozen(m,Sum_constant(Right()),n,s) -> Term_sub(n,s)
    4: Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(n,s))
    5: Term_sub(Term_app(m,n),s) -> Term_app(Term_sub(m,s),Term_sub(n,s))
    6: Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
    7: Term_sub(Term_inl(m),s) -> Term_inl(Term_sub(m,s))
    8: Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
    9: Term_sub(Term_var(x),Id()) -> Term_var(x)
    10: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> m
    11: Term_sub(Term_var(x),Cons_usual(y,m,s)) -> Term_sub(Term_var(x),s)
    12: Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
    13: Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
    14: Sum_sub(xi,Id()) -> Sum_term_var(xi)
    15: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k)
    16: Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s)
    17: Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s)
    18: Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
    19: Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),Concat(s,t))
    20: Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
    21: Concat(Id(),s) -> s
Number of strict rules: 21
Direct Order(PosReal,>,Poly) ... failed.
Freezing ... failed.
Dependency Pairs:
   #1: #Frozen(m,Sum_constant(Left()),n,s) -> #Term_sub(m,s)
   #2: #Term_sub(Term_pair(m,n),s) -> #Term_sub(m,s)
   #3: #Term_sub(Term_pair(m,n),s) -> #Term_sub(n,s)
   #4: #Term_sub(Term_sub(m,s),t) -> #Term_sub(m,Concat(s,t))
   #5: #Term_sub(Term_sub(m,s),t) -> #Concat(s,t)
   #6: #Term_sub(Term_var(x),Cons_usual(y,m,s)) -> #Term_sub(Term_var(x),s)
   #7: #Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> #Term_sub(Term_var(x),s)
   #8: #Concat(Cons_sum(xi,k,s),t) -> #Concat(s,t)
   #9: #Term_sub(Term_inl(m),s) -> #Term_sub(m,s)
   #10: #Term_sub(Term_app(m,n),s) -> #Term_sub(m,s)
   #11: #Term_sub(Term_app(m,n),s) -> #Term_sub(n,s)
   #12: #Sum_sub(xi,Cons_usual(y,m,s)) -> #Sum_sub(xi,s)
   #13: #Concat(Cons_usual(x,m,s),t) -> #Term_sub(m,t)
   #14: #Concat(Cons_usual(x,m,s),t) -> #Concat(s,t)
   #15: #Sum_sub(xi,Cons_sum(psi,k,s)) -> #Sum_sub(xi,s)
   #16: #Frozen(m,Sum_constant(Right()),n,s) -> #Term_sub(n,s)
   #17: #Term_sub(Case(m,xi,n),s) -> #Frozen(m,Sum_sub(xi,s),n,s)
   #18: #Term_sub(Case(m,xi,n),s) -> #Sum_sub(xi,s)
   #19: #Term_sub(Term_inr(m),s) -> #Term_sub(m,s)
   #20: #Frozen(m,Sum_term_var(xi),n,s) -> #Term_sub(m,s)
   #21: #Frozen(m,Sum_term_var(xi),n,s) -> #Term_sub(n,s)
   #22: #Concat(Concat(s,t),u) -> #Concat(s,Concat(t,u))
   #23: #Concat(Concat(s,t),u) -> #Concat(t,u)
Number of SCCs: 3, DPs: 22, edges: 145
	SCC { #12 #15 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
Cons_sum(x1,x2,x3)	weight: (/ 1 2) + x3
  Left()	weight: 0
Sum_term_var(x1)	weight: 0
#Concat(x1,x2)	weight: 0
  Case(x1,x2,x3)	weight: 0
Term_inr(x1)	weight: 0
#Sum_sub(x1,x2)	weight: x2
Sum_constant(x1)	weight: 0
Sum_sub(x1,x2)	weight: 0
 Right()	weight: 0
Cons_usual(x1,x2,x3)	weight: (/ 1 2) + x3
Term_var(x1)	weight: 0
    Id()	weight: 0
Term_sub(x1,x2)	weight: 0
Frozen(x1,x2,x3,x4)	weight: 0
#Frozen(x1,x2,x3,x4)	weight: 0
Term_app(x1,x2)	weight: 0
Term_inl(x1)	weight: 0
Term_pair(x1,x2)	weight: 0
#Term_sub(x1,x2)	weight: 0
Concat(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #12 #15
Number of SCCs: 2, DPs: 20, edges: 141
	SCC { #6 #7 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
Cons_sum(x1,x2,x3)	weight: (/ 1 2) + x3
  Left()	weight: 0
Sum_term_var(x1)	weight: 0
#Concat(x1,x2)	weight: 0
  Case(x1,x2,x3)	weight: 0
Term_inr(x1)	weight: 0
#Sum_sub(x1,x2)	weight: 0
Sum_constant(x1)	weight: 0
Sum_sub(x1,x2)	weight: 0
 Right()	weight: 0
Cons_usual(x1,x2,x3)	weight: (/ 1 2) + x3
Term_var(x1)	weight: x1
    Id()	weight: 0
Term_sub(x1,x2)	weight: 0
Frozen(x1,x2,x3,x4)	weight: 0
#Frozen(x1,x2,x3,x4)	weight: 0
Term_app(x1,x2)	weight: 0
Term_inl(x1)	weight: 0
Term_pair(x1,x2)	weight: 0
#Term_sub(x1,x2)	weight: x1 + x2
Concat(x1,x2)	weight: 0
    Usable rules: { }
    Removed DPs: #6 #7
Number of SCCs: 1, DPs: 18, edges: 137
	SCC { #1..5 #8..11 #13 #14 #16 #17 #19..23 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
Cons_sum(x1,x2,x3)	weight: x1 + x2 + x3
  Left()	weight: 0
Sum_term_var(x1)	weight: (/ 1 2) + x1
#Concat(x1,x2)	weight: x1
  Case(x1,x2,x3)	weight: (/ 1 2) + x1 + x2 + x3
Term_inr(x1)	weight: (/ 1 4) + x1
#Sum_sub(x1,x2)	weight: 0
Sum_constant(x1)	weight: (/ 1 2)
Sum_sub(x1,x2)	weight: (/ 1 4) + x2
 Right()	weight: 0
Cons_usual(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
Term_var(x1)	weight: (/ 1 4)
    Id()	weight: 0
Term_sub(x1,x2)	weight: x1 + x2
Frozen(x1,x2,x3,x4)	weight: (/ 1 4)
#Frozen(x1,x2,x3,x4)	weight: (/ 1 2) + x1 + x3
Term_app(x1,x2)	weight: (/ 1 4) + x1 + x2
Term_inl(x1)	weight: (/ 1 4) + x1
Term_pair(x1,x2)	weight: (/ 1 4) + x1 + x2
#Term_sub(x1,x2)	weight: (/ 1 4) + x1
Concat(x1,x2)	weight: (/ 1 4) + x1 + x2
    Usable rules: { }
    Removed DPs: #1..3 #5 #9..11 #14 #16 #17 #19..23
Number of SCCs: 2, DPs: 2, edges: 2
	SCC { #8 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
Cons_sum(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
  Left()	weight: 0
Sum_term_var(x1)	weight: (/ 1 2) + x1
#Concat(x1,x2)	weight: x1
  Case(x1,x2,x3)	weight: (/ 1 2) + x1 + x2 + x3
Term_inr(x1)	weight: (/ 1 4) + x1
#Sum_sub(x1,x2)	weight: 0
Sum_constant(x1)	weight: (/ 1 2)
Sum_sub(x1,x2)	weight: (/ 1 4)
 Right()	weight: 0
Cons_usual(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
Term_var(x1)	weight: (/ 1 4)
    Id()	weight: 0
Term_sub(x1,x2)	weight: x1 + x2
Frozen(x1,x2,x3,x4)	weight: (/ 1 4)
#Frozen(x1,x2,x3,x4)	weight: (/ 1 2)
Term_app(x1,x2)	weight: (/ 1 4) + x1 + x2
Term_inl(x1)	weight: (/ 1 4) + x1
Term_pair(x1,x2)	weight: (/ 1 4) + x1 + x2
#Term_sub(x1,x2)	weight: (/ 1 4)
Concat(x1,x2)	weight: (/ 1 4) + x1 + x2
    Usable rules: { }
    Removed DPs: #8
Number of SCCs: 1, DPs: 1, edges: 1
	SCC { #4 }
Removing DPs: Order(PosReal,>,Sum)... succeeded.
Cons_sum(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
  Left()	weight: 0
Sum_term_var(x1)	weight: (/ 1 2) + x1
#Concat(x1,x2)	weight: 0
  Case(x1,x2,x3)	weight: (/ 1 2) + x2
Term_inr(x1)	weight: (/ 1 4) + x1
#Sum_sub(x1,x2)	weight: 0
Sum_constant(x1)	weight: (/ 1 2)
Sum_sub(x1,x2)	weight: (/ 1 4)
 Right()	weight: 0
Cons_usual(x1,x2,x3)	weight: (/ 1 4) + x1 + x2 + x3
Term_var(x1)	weight: (/ 1 4)
    Id()	weight: 0
Term_sub(x1,x2)	weight: (/ 1 4) + x1 + x2
Frozen(x1,x2,x3,x4)	weight: (/ 1 4)
#Frozen(x1,x2,x3,x4)	weight: (/ 1 2)
Term_app(x1,x2)	weight: (/ 1 4) + x1 + x2
Term_inl(x1)	weight: (/ 1 4)
Term_pair(x1,x2)	weight: (/ 1 4) + x1
#Term_sub(x1,x2)	weight: (/ 1 4) + x1
Concat(x1,x2)	weight: (/ 1 2) + x1 + x2
    Usable rules: { }
    Removed DPs: #4
Number of SCCs: 0, DPs: 0, edges: 0
YES