The semantics of constraint logic programming languages with coroutining facilities (freeze, suspension, residuation, etc.) cannot be fully declarative; thus, an operational semantics has to be taken as the defining one. We give a formal operational semantics for a Prolog-like language with cut and entailment-based conditional. The difficulty here is to present the semantics in a form that abstracts away inessential details and highlights the interaction between language constructs. Our approach is derived from those used for concurrent calculi. We use abstract syntax trees, congruence laws and rewrite rules to define the semantics. A computation step is modeled as the application of a rewrite rule to an abstract syntax tree modulo structural congruence. This semantics serves as a defining tool for the language designer and as the interface between the language designer and implementor; it allows the programmer to check his intuition with a formal execution model and it gives him a performance measure for the execution of programs. We have used the semantics to make precise, for the first time, the critical interaction between sequential execution (including backtracking and cut pruning) and coroutining. In particular we exhibit cases where this interaction can lead to indeterministic results (i.e., to non-predictable program execution).