The use of term-rewriting systems (TRSs) is at the core of automated theorem proving (ATP). There are a number of methods whereby we can build terminating TRSs with full deduction power, with respect to some theory. Yet, there exist theories these techniques cannot handle, giving rise to a trade-off between deduction power and termination. One such theory is the theory of observation congruence [Milner, 1989b] in CCS [Milner, 1989a]. The standard approach to overcome this situation is to use meta-level information; it, however, introduces the problem of finding and capturing such meta-level control. This paper advocates the use of annotated TRSs (ATRSs) for approaching these problems; the annotation are used to capture meta-level information that helps direct proof search, while giving an intuitive account about why and how rewriting is expected to work. We introduce an ATRS, called Observant. Observant is goal-oriented, and, hence domain-specific: it can be used to build a decision procedure for observation congruence in CCS [Milner, 1989a]; furthermore, it can be used to attempt to solve or prove CCS equations, involving either finite-state systems, or infinite-state systems. We prove Observant terminating, sound, and complete - over the normalisation of finite processes. We argue that Observant surpasses rival term-rewriting strategies.