YES Trs: {f(f(x, a()), a()) -> f(f(f(a(), a()), f(x, a())), a())} Comment: We consider a non-duplicating trs. BOUND: Automaton: { a_2() -> q11, a_1() -> q3, a_0() -> q2, f_2(q14, q11) -> q5, f_2(q12, q13) -> q14, f_2(q11, q11) -> q12, f_2(q6, q11) -> q13, f_1(q6, q3) -> q5 | q2, f_1(q4, q5) -> q6, f_1(q3, q3) -> q4, f_1(q2, q3) -> q5, f_0(q2, q2) -> q2} Strict: {} Qed