YES Trs: {a b -> a c b} Comment: We consider a non-duplicating trs. BOUND: Automaton: {b_1(q3) -> q4, b_0(q2) -> q2, c_1(q4) -> q5, c_0(q2) -> q2, a_1(q5) -> q6, a_0(q2) -> q2, q6 -> q2, q2 -> q3} Strict: {} Qed