By Lemma 12, the clause C = Cn is conflicting on M with respect to [F,Π], that is, consistent(M) |= ¬C and F,Πo|= C. By the construction, C = l
′ ∨C
′, where l
′is the only literal whose complement belongs to the decision level dec and the complements of all literals in C
′ belong to lower decision levels.

Case 1. dec = 0. Since for every literal l ∈ C
′, the decision level of l is strictly lower than dec, C
′ = ⊥. Since M||Γ is a backjump state, M contains a decision literal. Then M can be written as Pl∆Q, where P contains no decision literals (in other words P consists of all literals in *consistent*(M) of decision level dec = 0) and l
′ ∈ P. Clearly, P |= ¬C
′(as C
′ = ⊥). Since F,Πo|= C(= l
′ ∨C
′), C is a reason for l
′to be in Pl′.

Case 2. dec ≥ 1. Let l be the decision literal in M that starts the decision level dec. Then, M
can be written as Pl∆Q. By the construction of the clause C, the complement of every literal in C
′ belongs to a decision level smaller than dec, that is, to P. It follows that P |= ¬C
′.

Thus, as before, we conclude that C is a reason for l
′to be in Pl′.

## Proposition 9 For Any Sm(Asp) Theory [F,Π],

(a) every path in SML(ASP)F,Π *contains only finitely many edges justified by basic transition rules,*
(b) for any semi-terminal state M||Γ of SML(ASP)F,Π reachable from /0||/0*, M is a model* of [F,Π],
(c) FailState is reachable from /0||/0 in SML(ASP)F,Π if and only if [F,Π] has no models.

## Proof

Part (a) is proved as in the proof of Proposition 13↑(Lierler 2010)(we preserve the notation used in that work).

(b) Let M||G be a semi-terminal state reachable from /0||/0 (that is, none of the basic rules are applicable.) Since *Decide* is not applicable, M assigns all literals. Next, M is consistent. Indeed, if M were inconsistent then, since *Fail* is not applicable, M would contain a decision literal. Consequently, M||Γ would be a backjump state. By Lemma 13, the transition rule *Backjump* would be applicable in M||Γ, contradicting our assumption that M||Γ is semi-terminal. We now proceed as in the proof of Proposition 7 (b) to show M is a model of F and M+ is an input answer set of Π.

(c) If *FailState* is reachable from /0||/0 in SML(ASP)F,Π, then there is a state M||Γ reachable from /0||/0 in SML(ASP)F,Π such that there is an edge between M||Γ and *FailState*. By the definition of SML(ASP)F,Π, this edge is due to the transition rule *Fail*. Thus, M is inconsistent and contains no decision literals. By Lemma 9, every model N of [F,Π] satisfies M.

Since M is inconsistent, [F,Π] has no models.

Conversely, if [F,Π] has no models, let us consider a maximal path in SML(ASP)F,Π
starting in /0||/0 and consisting of basic transition rules. By (a), it follows that such a path is finite and ends in a semi-terminal state. By (b), this semi-terminal must be *FailState*,
because [F,Π] has no models.