Summary: The Counting method rewrites a logic (conceived for a backward, Prolog- like, evaluation) into another set of clauses that can be efficiently executed using a forward strategy. We assume here a forward evaluation strategy based on the saturation (of a set of clauses) operator. Under this hypothesis, the rewriting method is compared with the original logic environment by means of a stack machine, which is used as a reference environment for our comparison. By proving different correspondences between the stack history tree nodes and the atoms produced during the saturation we characterize the Counting approach as for efficiency w.r.t. shortcuts or cyclic relations and as for completeness and soundness.