We consider the following Problem: Strict Trs: {f(f(a(), x), y) -> f(a(), f(f(x, h(y)), a()))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: {f(f(a(), x), y) -> f(a(), f(f(x, h(y)), a()))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: We consider the following Problem: Strict Trs: {f(f(a(), x), y) -> f(a(), f(f(x, h(y)), a()))} StartTerms: basic terms Strategy: innermost Certificate: YES(?,O(n^1)) Proof: The problem is match-bounded by 0. The enriched problem is compatible with the following automaton: { f_0(2, 2) -> 1 , a_0() -> 2 , h_0(2) -> 2} Hurray, we answered YES(?,O(n^1))