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