YES(?,O(n^1))

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_1(7) -> 1
, a__f_1(8) -> 1
, a__f_1(8) -> 8
, a__f_2(11) -> 1
, a__f_2(11) -> 8
, 0_0() -> 2
, 0_1() -> 1
, 0_1() -> 3
, 0_1() -> 6
, 0_1() -> 8
, 0_2() -> 1
, 0_2() -> 7
, 0_2() -> 8
, 0_3() -> 11
, cons_0(2, 2) -> 2
, cons_1(3, 4) -> 1
, cons_1(8, 2) -> 1
, cons_1(8, 2) -> 8
, cons_2(7, 9) -> 1
, cons_2(7, 9) -> 8
, cons_3(11, 12) -> 1
, cons_3(11, 12) -> 8
, f_0(2) -> 2
, f_1(2) -> 1
, f_1(5) -> 4
, f_2(7) -> 1
, f_2(8) -> 1
, f_2(8) -> 8
, f_2(10) -> 9
, f_3(11) -> 1
, f_3(11) -> 8
, f_3(13) -> 12
, s_0(2) -> 2
, s_1(6) -> 5
, s_1(8) -> 1
, s_1(8) -> 8
, s_2(7) -> 10
, s_3(11) -> 13
, a__p_0(2) -> 1
, a__p_1(5) -> 7
, a__p_1(8) -> 1
, a__p_1(8) -> 8
, a__p_2(10) -> 11
, mark_0(2) -> 1
, mark_1(2) -> 8
, p_0(2) -> 2
, p_1(2) -> 1
, p_2(5) -> 7
, p_2(8) -> 1
, p_2(8) -> 8
, p_3(10) -> 11 }

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