is rejecting. Note that it is impossible for a configuration to be both accepting and rejecting, however, some configurations may be neither accepting or rejecting, due to the possibility of nonterminating computations. Resource bounds When deciding if a configuration of an ATM is accepting or rejecting using the above definition, it is not always necessary to examine all configurations reachable from the current configuration. In particular, an existential configuration can be labelled as accepting if any successor configuration is found to be accepting, and a universal configuration can be labelled as rejecting if any successor configuration is found to be rejecting. An ATM decides a formal language in time if, on any input of length , examining configurations only up to steps is sufficient to label the initial configuration as accepting or rejecting. An ATM decides a language in space if examining configurations that do not modify tape cells beyond the cell from the left is sufficient. A language that is decided by some ATM in time for some constant is said to be in the class , and a language decided in space is said to be in the class . Example Perhaps the most natural problem for alternating machines to solve is the quantified Boolean formula problem, which is a generalization of the Boolean satisfiability problem in which each variable can be bound by either an existential or a universal quantifier. The alternating machine branches existentially to try all possible values of an existentially quantified variable and universally to try all possible values of a universally quantified variable, in the left-to-right order in which they are bound. After deciding a value for all quantified variables, the machine accepts if the resulting Boolean formula evaluates to true, and rejects if it evaluates to false. Thus at an existentially quantified variable the machine is accepting if a value can be substituted for the variable that renders the remaining problem satisfiable, and at a universally quantified variable the machine is accepting if any value can be substituted and the remaining problem is satisfiable. Such a machine decides quantified Boolean formulas in time and space . The Boolean satisfiability problem can be viewed as the special case where all variables are existentially quantified, allowing ordinary nondeterminism, which uses only existential branching, to solve it efficiently. Complexity classes and comparison to deterministic Turing machines The following complexity classes are useful to define for