YES(?,O(n^1)) We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { a(c(d(x))) -> c(x) , u(b(d(d(x)))) -> b(x) , v(a(a(x))) -> u(v(x)) , v(a(c(x))) -> u(b(d(x))) , v(c(x)) -> b(x) , w(a(a(x))) -> u(w(x)) , w(a(c(x))) -> u(b(d(x))) , w(c(x)) -> b(x) } Obligation: innermost runtime complexity Answer: YES(?,O(n^1)) The input was oriented with the instance of 'Small Polynomial Path Order (PS,1-bounded)' as induced by the safe mapping safe(a) = {1}, safe(c) = {1}, safe(d) = {1}, safe(u) = {1}, safe(b) = {1}, safe(v) = {}, safe(w) = {} and precedence v > u, w > u, v ~ w . Following symbols are considered recursive: {v, w} The recursion depth is 1. For your convenience, here are the satisfied ordering constraints: a(; c(; d(; x))) > c(; x) u(; b(; d(; d(; x)))) > b(; x) v(a(; a(; x));) > u(; v(x;)) v(a(; c(; x));) > u(; b(; d(; x))) v(c(; x);) > b(; x) w(a(; a(; x));) > u(; w(x;)) w(a(; c(; x));) > u(; b(; d(; x))) w(c(; x);) > b(; x) Hurray, we answered YES(?,O(n^1))