YES(?,O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^1)).

Strict Trs:
  { bind_1[4](bind'_0(x5), x4, x3, x2, S(x1)) ->
    bind'_0[6](x5, x3, bot[2](), x4, x2, S(x1))
  , bind_1[4](bind'_0(x5), x4, x3, x2, S(x1)) ->
    bind'_0[6](x5, x3, bot[4](), x4, x2, S(x1))
  , bind_1[4](bind'_0(x5), x4, x3, x2, S(x1)) ->
    bind'_0[6](x5, x3, bot[6](), x4, x2, S(x1))
  , bind'_0[6](eos(), x31, x27, x76, Cons(x60, x44), S(x28)) ->
    ParseFail(S(x28))
  , bind'_0[6](eos(), x63, x55, runParser_0(), Nil(), S(x12)) ->
    ParseSuccess(Nil())
  , bind'_0[6](eos(), x3, x2, bind_1(), Nil(), S(x1)) ->
    bind_1[4](bind'_0(eos()), runParser_0(), Unit(), Nil(), S(x1))
  , bind'_0[6](bind_p_f(bind_p_f(any(), filter_0()),
                        bind'_0(return_x())),
               x4,
               x3,
               x2,
               Nil(),
               S(x1))
    -> ParseFail(S(x1))
  , bind'_0[6](bind_p_f(bind_p_f(any(), filter_0()),
                        bind'_0(return_x())),
               x5,
               x4,
               x3,
               Cons(A(), x2),
               S(x1))
    -> ParseFail(S(S(x1)))
  , bind'_0[6](bind_p_f(bind_p_f(any(), filter_0()),
                        bind'_0(return_x())),
               x5,
               x4,
               x3,
               Cons(B(), x2),
               S(x1))
    -> bind_1[4](bind'_0(return_x()), x3, B(), x2, S(S(x1)))
  , bind'_0[6](bind_p_f(bind_p_f(any(), filter_0()),
                        bind'_0(return_x())),
               x5,
               x4,
               x3,
               Cons(C(), x2),
               S(x1))
    -> ParseFail(S(S(x1)))
  , bind'_0[6](return_x(), x11, x9, runParser_0(), x4, S(x2)) ->
    ParseSuccess(x4)
  , bind'_0[6](return_x(), x11, x9, bind_1(), x4, S(x2)) ->
    bind_1[4](bind'_0(eos()), runParser_0(), Unit(), x4, S(x2))
  , rec[string_0][6](x23, Nil()) -> ParseFail(0())
  , rec[string_0][6](x23, Cons(A(), x2)) ->
    bind_1[4](bind'_0(bind_p_f(bind_p_f(any(), filter_0()),
                               bind'_0(return_x()))),
              bind_1(),
              A(),
              x2,
              S(0()))
  , rec[string_0][6](x23, Cons(B(), x2)) -> ParseFail(S(0()))
  , rec[string_0][6](x23, Cons(C(), x2)) -> ParseFail(S(0()))
  , main(x3) -> rec[string_0][6](bot[1](), x3)
  , main(x3) -> rec[string_0][6](bot[3](), x3)
  , main(x3) -> rec[string_0][6](bot[5](), x3) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^1))

The problem is match-bounded by 3. The enriched problem is
compatible with the following automaton.
{ bind'_0_0(2) -> 2
, bind'_0_1(9) -> 6
, bind'_0_1(12) -> 10
, bind'_0_2(26) -> 23
, S_0(2) -> 2
, S_1(2) -> 4
, S_1(4) -> 4
, S_2(2) -> 21
, S_2(4) -> 21
, S_3(2) -> 28
, S_3(4) -> 28
, bind_1[4]_0(2, 2, 2, 2, 2) -> 1
, bind_1[4]_1(6, 7, 8, 2, 4) -> 1
, bind_1[4]_1(6, 7, 8, 5, 4) -> 1
, bind_1[4]_1(10, 2, 11, 2, 4) -> 1
, bind_1[4]_2(23, 24, 25, 2, 21) -> 1
, bot[2]_0() -> 2
, bot[2]_1() -> 3
, bot[2]_2() -> 20
, bot[2]_3() -> 27
, bind'_0[6]_0(2, 2, 2, 2, 2, 2) -> 1
, bind'_0[6]_1(2, 2, 3, 2, 2, 4) -> 1
, bind'_0[6]_2(9, 8, 20, 7, 2, 21) -> 1
, bind'_0[6]_2(9, 8, 20, 7, 5, 21) -> 1
, bind'_0[6]_2(12, 11, 20, 2, 2, 21) -> 1
, bind'_0[6]_3(26, 25, 27, 24, 2, 28) -> 1
, bot[4]_0() -> 2
, bot[4]_1() -> 3
, bot[4]_2() -> 20
, bot[4]_3() -> 27
, eos_0() -> 2
, eos_1() -> 9
, eos_2() -> 26
, runParser_0_0() -> 2
, runParser_0_1() -> 7
, runParser_0_2() -> 24
, Nil_0() -> 2
, Nil_1() -> 5
, Nil_2() -> 22
, ParseSuccess_0(2) -> 2
, ParseSuccess_1(2) -> 1
, ParseSuccess_1(5) -> 1
, ParseSuccess_2(22) -> 1
, bind_1_0() -> 2
, bind_1_1() -> 2
, Unit_0() -> 2
, Unit_1() -> 8
, Unit_2() -> 25
, Cons_0(2, 2) -> 2
, ParseFail_0(2) -> 2
, ParseFail_1(4) -> 1
, any_0() -> 2
, any_1() -> 17
, filter_0_0() -> 2
, filter_0_1() -> 18
, bind_p_f_0(2, 2) -> 2
, bind_p_f_1(16, 10) -> 12
, bind_p_f_1(17, 18) -> 16
, return_x_0() -> 2
, return_x_1() -> 12
, A_0() -> 2
, A_1() -> 11
, B_0() -> 2
, B_1() -> 11
, C_0() -> 2
, bot[6]_0() -> 2
, bot[6]_1() -> 3
, bot[6]_2() -> 20
, bot[6]_3() -> 27
, rec[string_0][6]_0(2, 2) -> 1
, rec[string_0][6]_1(19, 2) -> 1
, 0_0() -> 2
, 0_1() -> 4
, main_0(2) -> 1
, bot[1]_0() -> 2
, bot[1]_1() -> 19
, bot[3]_0() -> 2
, bot[3]_1() -> 19
, bot[5]_0() -> 2
, bot[5]_1() -> 19 }

Hurray, we answered YES(?,O(n^1))