MAYBE
* Step 1: DependencyPairs MAYBE
    + Considered Problem:
        - Strict TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),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,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)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            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_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            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),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2} / {Case/3,Cons_sum/3,Cons_usual/3,Id/0,Left/0,Right/0
            ,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2,Term_var/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat,Frozen,Sum_sub,Term_sub} and constructors {Case
            ,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u))
          Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t))
          Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t))
          Concat#(Id(),s) -> c_4()
          Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s))
          Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s))
          Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s))
          Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8()
          Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s))
          Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s))
          Sum_sub#(xi,Id()) -> c_11()
          Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s))
          Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s))
          Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s))
          Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s))
          Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s))
          Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t))
          Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s))
          Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19()
          Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s))
          Term_sub#(Term_var(x),Id()) -> c_21()
        Weak DPs
          
        
        and mark the set of starting terms.
* Step 2: PredecessorEstimation MAYBE
    + Considered Problem:
        - Strict DPs:
            Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u))
            Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t))
            Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t))
            Concat#(Id(),s) -> c_4()
            Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s))
            Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s))
            Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s))
            Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8()
            Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s))
            Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s))
            Sum_sub#(xi,Id()) -> c_11()
            Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s))
            Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s))
            Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s))
            Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s))
            Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s))
            Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t))
            Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s))
            Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19()
            Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s))
            Term_sub#(Term_var(x),Id()) -> c_21()
        - Weak TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),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,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)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            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_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            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),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3
            ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2
            ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1
            ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub#
            ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app
            ,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {4,8,11,19,21}
        by application of
          Pre({4,8,11,19,21}) = {1,2,3,5,6,7,9,10,12,13,14,15,16,17,18,20}.
        Here rules are labelled as follows:
          1: Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u))
          2: Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t))
          3: Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t))
          4: Concat#(Id(),s) -> c_4()
          5: Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s))
          6: Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s))
          7: Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s))
          8: Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8()
          9: Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s))
          10: Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s))
          11: Sum_sub#(xi,Id()) -> c_11()
          12: Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s))
          13: Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s))
          14: Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s))
          15: Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s))
          16: Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s))
          17: Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t))
          18: Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s))
          19: Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19()
          20: Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s))
          21: Term_sub#(Term_var(x),Id()) -> c_21()
* Step 3: RemoveWeakSuffixes MAYBE
    + Considered Problem:
        - Strict DPs:
            Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u))
            Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t))
            Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t))
            Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s))
            Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s))
            Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s))
            Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s))
            Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s))
            Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s))
            Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s))
            Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s))
            Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s))
            Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s))
            Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t))
            Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s))
            Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s))
        - Weak DPs:
            Concat#(Id(),s) -> c_4()
            Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8()
            Sum_sub#(xi,Id()) -> c_11()
            Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19()
            Term_sub#(Term_var(x),Id()) -> c_21()
        - Weak TRS:
            Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
            Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
            Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),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,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)
            Sum_sub(xi,Id()) -> Sum_term_var(xi)
            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_inl(m),s) -> Term_inl(Term_sub(m,s))
            Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
            Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
            Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
            Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
            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),Id()) -> Term_var(x)
        - Signature:
            {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3
            ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2
            ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1
            ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub#
            ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app
            ,Term_inl,Term_inr,Term_pair,Term_var}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u))
             -->_2 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3
             -->_1 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3
             -->_2 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2
             -->_1 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2
             -->_2 Concat#(Id(),s) -> c_4():17
             -->_1 Concat#(Id(),s) -> c_4():17
             -->_2 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1
             -->_1 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1
          
          2:S:Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t))
             -->_1 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3
             -->_1 Concat#(Id(),s) -> c_4():17
             -->_1 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2
             -->_1 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1
          
          3:S:Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t))
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_2 Concat#(Id(),s) -> c_4():17
             -->_2 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3
             -->_2 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2
             -->_2 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1
          
          4:S:Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s))
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
          
          5:S:Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s))
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
          
          6:S:Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s))
             -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_2 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_2 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_2 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_2 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_2 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_2 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_2 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
             -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
             -->_2 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
          
          7:S:Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s))
             -->_1 Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)):8
             -->_1 Sum_sub#(xi,Id()) -> c_11():19
             -->_1 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8():18
             -->_1 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)):7
          
          8:S:Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s))
             -->_1 Sum_sub#(xi,Id()) -> c_11():19
             -->_1 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8():18
             -->_1 Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)):8
             -->_1 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)):7
          
          9:S:Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s))
             -->_2 Sum_sub#(xi,Id()) -> c_11():19
             -->_2 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8():18
             -->_2 Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s)):8
             -->_2 Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s)):7
             -->_1 Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s)):6
             -->_1 Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s)):5
             -->_1 Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s)):4
          
          10:S:Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s))
             -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_2 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_2 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_2 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_2 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_2 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_2 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_2 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_2 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
             -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
          
          11:S:Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s))
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
          
          12:S:Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s))
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
          
          13:S:Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s))
             -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_2 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_2 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_2 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_2 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_2 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_2 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_2 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_2 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_2 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
             -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
          
          14:S:Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t))
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_2 Concat#(Id(),s) -> c_4():17
             -->_1 Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t)):14
             -->_1 Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s)):13
             -->_1 Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s)):12
             -->_1 Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s)):11
             -->_1 Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s)):10
             -->_1 Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s)):9
             -->_2 Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t)):3
             -->_2 Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t)):2
             -->_2 Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u)):1
          
          15:S:Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s))
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
          
          16:S:Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s))
             -->_1 Term_sub#(Term_var(x),Id()) -> c_21():21
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19():20
             -->_1 Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s)):16
             -->_1 Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s)):15
          
          17:W:Concat#(Id(),s) -> c_4()
             
          
          18:W:Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8()
             
          
          19:W:Sum_sub#(xi,Id()) -> c_11()
             
          
          20:W:Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19()
             
          
          21:W:Term_sub#(Term_var(x),Id()) -> c_21()
             
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          18: Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_8()
          19: Sum_sub#(xi,Id()) -> c_11()
          17: Concat#(Id(),s) -> c_4()
          20: Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_19()
          21: Term_sub#(Term_var(x),Id()) -> c_21()
* Step 4: Failure MAYBE
  + Considered Problem:
      - Strict DPs:
          Concat#(Concat(s,t),u) -> c_1(Concat#(s,Concat(t,u)),Concat#(t,u))
          Concat#(Cons_sum(xi,k,s),t) -> c_2(Concat#(s,t))
          Concat#(Cons_usual(x,m,s),t) -> c_3(Term_sub#(m,t),Concat#(s,t))
          Frozen#(m,Sum_constant(Left()),n,s) -> c_5(Term_sub#(m,s))
          Frozen#(m,Sum_constant(Right()),n,s) -> c_6(Term_sub#(n,s))
          Frozen#(m,Sum_term_var(xi),n,s) -> c_7(Term_sub#(m,s),Term_sub#(n,s))
          Sum_sub#(xi,Cons_sum(psi,k,s)) -> c_9(Sum_sub#(xi,s))
          Sum_sub#(xi,Cons_usual(y,m,s)) -> c_10(Sum_sub#(xi,s))
          Term_sub#(Case(m,xi,n),s) -> c_12(Frozen#(m,Sum_sub(xi,s),n,s),Sum_sub#(xi,s))
          Term_sub#(Term_app(m,n),s) -> c_13(Term_sub#(m,s),Term_sub#(n,s))
          Term_sub#(Term_inl(m),s) -> c_14(Term_sub#(m,s))
          Term_sub#(Term_inr(m),s) -> c_15(Term_sub#(m,s))
          Term_sub#(Term_pair(m,n),s) -> c_16(Term_sub#(m,s),Term_sub#(n,s))
          Term_sub#(Term_sub(m,s),t) -> c_17(Term_sub#(m,Concat(s,t)),Concat#(s,t))
          Term_sub#(Term_var(x),Cons_sum(xi,k,s)) -> c_18(Term_sub#(Term_var(x),s))
          Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> c_20(Term_sub#(Term_var(x),s))
      - Weak TRS:
          Concat(Concat(s,t),u) -> Concat(s,Concat(t,u))
          Concat(Cons_sum(xi,k,s),t) -> Cons_sum(xi,k,Concat(s,t))
          Concat(Cons_usual(x,m,s),t) -> Cons_usual(x,Term_sub(m,t),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,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)
          Sum_sub(xi,Id()) -> Sum_term_var(xi)
          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_inl(m),s) -> Term_inl(Term_sub(m,s))
          Term_sub(Term_inr(m),s) -> Term_inr(Term_sub(m,s))
          Term_sub(Term_pair(m,n),s) -> Term_pair(Term_sub(m,s),Term_sub(n,s))
          Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t))
          Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub(Term_var(x),s)
          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),Id()) -> Term_var(x)
      - Signature:
          {Concat/2,Frozen/4,Sum_sub/2,Term_sub/2,Concat#/2,Frozen#/4,Sum_sub#/2,Term_sub#/2} / {Case/3,Cons_sum/3
          ,Cons_usual/3,Id/0,Left/0,Right/0,Sum_constant/1,Sum_term_var/1,Term_app/2,Term_inl/1,Term_inr/1,Term_pair/2
          ,Term_var/1,c_1/2,c_2/1,c_3/2,c_4/0,c_5/1,c_6/1,c_7/2,c_8/0,c_9/1,c_10/1,c_11/0,c_12/2,c_13/2,c_14/1,c_15/1
          ,c_16/2,c_17/2,c_18/1,c_19/0,c_20/1,c_21/0}
      - Obligation:
          innermost runtime complexity wrt. defined symbols {Concat#,Frozen#,Sum_sub#
          ,Term_sub#} and constructors {Case,Cons_sum,Cons_usual,Id,Left,Right,Sum_constant,Sum_term_var,Term_app
          ,Term_inl,Term_inr,Term_pair,Term_var}
  + Applied Processor:
      EmptyProcessor
  + Details:
      The problem is still open.
MAYBE