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

Strict Trs:
  { a__f(X) -> f(X)
  , a__f(0()) -> cons(0(), f(s(0())))
  , a__f(s(0())) -> a__f(a__p(s(0())))
  , a__p(X) -> p(X)
  , a__p(s(0())) -> 0()
  , mark(0()) -> 0()
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(f(X)) -> a__f(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(p(X)) -> a__p(mark(X)) }
Obligation:
  runtime complexity
Answer:
  YES(?,O(n^1))

The input is overlay and right-linear. Switching to innermost
rewriting.

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

Strict Trs:
  { a__f(X) -> f(X)
  , a__f(0()) -> cons(0(), f(s(0())))
  , a__f(s(0())) -> a__f(a__p(s(0())))
  , a__p(X) -> p(X)
  , a__p(s(0())) -> 0()
  , mark(0()) -> 0()
  , mark(cons(X1, X2)) -> cons(mark(X1), X2)
  , mark(f(X)) -> a__f(mark(X))
  , mark(s(X)) -> s(mark(X))
  , mark(p(X)) -> a__p(mark(X)) }
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.
{ a__f_0(2) -> 1
, a__f_0(3) -> 1
, a__f_0(4) -> 1
, a__f_0(5) -> 1
, a__f_0(8) -> 1
, a__f_1(13) -> 1
, a__f_1(14) -> 7
, a__f_1(14) -> 14
, a__f_2(17) -> 7
, a__f_2(17) -> 14
, 0_0() -> 2
, 0_1() -> 6
, 0_1() -> 7
, 0_1() -> 9
, 0_1() -> 12
, 0_1() -> 14
, 0_2() -> 7
, 0_2() -> 13
, 0_2() -> 14
, 0_3() -> 17
, cons_0(2, 2) -> 3
, cons_0(2, 3) -> 3
, cons_0(2, 4) -> 3
, cons_0(2, 5) -> 3
, cons_0(2, 8) -> 3
, cons_0(3, 2) -> 3
, cons_0(3, 3) -> 3
, cons_0(3, 4) -> 3
, cons_0(3, 5) -> 3
, cons_0(3, 8) -> 3
, cons_0(4, 2) -> 3
, cons_0(4, 3) -> 3
, cons_0(4, 4) -> 3
, cons_0(4, 5) -> 3
, cons_0(4, 8) -> 3
, cons_0(5, 2) -> 3
, cons_0(5, 3) -> 3
, cons_0(5, 4) -> 3
, cons_0(5, 5) -> 3
, cons_0(5, 8) -> 3
, cons_0(8, 2) -> 3
, cons_0(8, 3) -> 3
, cons_0(8, 4) -> 3
, cons_0(8, 5) -> 3
, cons_0(8, 8) -> 3
, cons_1(9, 10) -> 1
, cons_1(14, 2) -> 7
, cons_1(14, 2) -> 14
, cons_1(14, 3) -> 7
, cons_1(14, 3) -> 14
, cons_1(14, 4) -> 7
, cons_1(14, 4) -> 14
, cons_1(14, 5) -> 7
, cons_1(14, 5) -> 14
, cons_1(14, 8) -> 7
, cons_1(14, 8) -> 14
, cons_2(13, 15) -> 1
, cons_2(13, 15) -> 7
, cons_2(13, 15) -> 14
, cons_3(17, 18) -> 7
, cons_3(17, 18) -> 14
, f_0(2) -> 4
, f_0(3) -> 4
, f_0(4) -> 4
, f_0(5) -> 4
, f_0(8) -> 4
, f_1(2) -> 1
, f_1(3) -> 1
, f_1(4) -> 1
, f_1(5) -> 1
, f_1(8) -> 1
, f_1(11) -> 10
, f_2(13) -> 1
, f_2(14) -> 7
, f_2(14) -> 14
, f_2(16) -> 15
, f_3(17) -> 7
, f_3(17) -> 14
, f_3(19) -> 18
, s_0(2) -> 5
, s_0(3) -> 5
, s_0(4) -> 5
, s_0(5) -> 5
, s_0(8) -> 5
, s_1(12) -> 11
, s_1(14) -> 7
, s_1(14) -> 14
, s_2(13) -> 16
, s_3(17) -> 19
, a__p_0(2) -> 6
, a__p_0(3) -> 6
, a__p_0(4) -> 6
, a__p_0(5) -> 6
, a__p_0(8) -> 6
, a__p_1(11) -> 13
, a__p_1(14) -> 7
, a__p_1(14) -> 14
, a__p_2(16) -> 17
, mark_0(2) -> 7
, mark_0(3) -> 7
, mark_0(4) -> 7
, mark_0(5) -> 7
, mark_0(8) -> 7
, mark_1(2) -> 14
, mark_1(3) -> 14
, mark_1(4) -> 14
, mark_1(5) -> 14
, mark_1(8) -> 14
, p_0(2) -> 8
, p_0(3) -> 8
, p_0(4) -> 8
, p_0(5) -> 8
, p_0(8) -> 8
, p_1(2) -> 6
, p_1(3) -> 6
, p_1(4) -> 6
, p_1(5) -> 6
, p_1(8) -> 6
, p_2(11) -> 13
, p_2(14) -> 7
, p_2(14) -> 14
, p_3(16) -> 17 }

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