MAYBE
* Step 1: Failure 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:
      Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3}
  + Details:
      The input can not be schown compatible.
MAYBE