We are left with following problem, upon which TcT provides the certificate YES(?,O(n^1)). Strict Trs: { f(x, x, y) -> x , f(x, y, y) -> y , f(x, y, g(y)) -> x , f(f(x, y, z), u, f(x, y, v)) -> f(x, y, f(z, u, v)) , f(g(x), x, y) -> y } Obligation: runtime complexity Answer: YES(?,O(n^1)) The problem is match-bounded by 0. The enriched problem is compatible with the following automaton. { f_0(2, 2, 2) -> 1 , g_0(2) -> 1 , g_0(2) -> 2 } Hurray, we answered YES(?,O(n^1))