We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { active(f(x)) -> mark(f(f(x))) , f(active(x)) -> active(f(x)) , f(mark(x)) -> mark(f(x)) , f(no(x)) -> no(f(x)) , chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))) , chk(no(c())) -> active(c()) , mat(f(x), f(y())) -> f(mat(x, y())) , mat(f(x), c()) -> no(c()) , tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))), x))) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The problem is match-bounded by 2. The enriched problem is compatible with the following automaton. { active_0(3) -> 1 , active_0(5) -> 1 , active_0(7) -> 1 , active_0(8) -> 1 , active_0(9) -> 1 , active_1(12) -> 4 , active_2(26) -> 13 , f_0(3) -> 2 , f_0(5) -> 2 , f_0(7) -> 2 , f_0(8) -> 2 , f_0(9) -> 2 , f_1(3) -> 11 , f_1(5) -> 11 , f_1(7) -> 11 , f_1(8) -> 11 , f_1(9) -> 11 , f_1(16) -> 15 , f_1(17) -> 16 , f_1(18) -> 17 , f_1(19) -> 18 , f_1(20) -> 19 , f_1(21) -> 20 , f_1(22) -> 21 , f_1(23) -> 22 , f_1(24) -> 23 , f_1(25) -> 24 , mark_0(3) -> 3 , mark_0(5) -> 3 , mark_0(7) -> 3 , mark_0(8) -> 3 , mark_0(9) -> 3 , mark_1(11) -> 2 , mark_1(11) -> 11 , chk_0(3) -> 4 , chk_0(5) -> 4 , chk_0(7) -> 4 , chk_0(8) -> 4 , chk_0(9) -> 4 , chk_1(14) -> 13 , no_0(3) -> 5 , no_0(5) -> 5 , no_0(7) -> 5 , no_0(8) -> 5 , no_0(9) -> 5 , no_1(11) -> 2 , no_1(11) -> 11 , no_1(12) -> 14 , mat_0(3, 3) -> 6 , mat_0(3, 5) -> 6 , mat_0(3, 7) -> 6 , mat_0(3, 8) -> 6 , mat_0(3, 9) -> 6 , mat_0(5, 3) -> 6 , mat_0(5, 5) -> 6 , mat_0(5, 7) -> 6 , mat_0(5, 8) -> 6 , mat_0(5, 9) -> 6 , mat_0(7, 3) -> 6 , mat_0(7, 5) -> 6 , mat_0(7, 7) -> 6 , mat_0(7, 8) -> 6 , mat_0(7, 9) -> 6 , mat_0(8, 3) -> 6 , mat_0(8, 5) -> 6 , mat_0(8, 7) -> 6 , mat_0(8, 8) -> 6 , mat_0(8, 9) -> 6 , mat_0(9, 3) -> 6 , mat_0(9, 5) -> 6 , mat_0(9, 7) -> 6 , mat_0(9, 8) -> 6 , mat_0(9, 9) -> 6 , mat_1(15, 3) -> 14 , mat_1(15, 5) -> 14 , mat_1(15, 7) -> 14 , mat_1(15, 8) -> 14 , mat_1(15, 9) -> 14 , X_0() -> 7 , X_1() -> 25 , y_0() -> 8 , c_0() -> 9 , c_1() -> 12 , c_2() -> 26 , tp_0(3) -> 10 , tp_0(5) -> 10 , tp_0(7) -> 10 , tp_0(8) -> 10 , tp_0(9) -> 10 , tp_1(13) -> 10 } Hurray, we answered YES(?,O(n^1))