It only needs to ask an askable atom when there is a clause where the head has not already been proved, all of the non-askable atoms in the body have been proved, and the askable atoms in the body that have been asked have been answered by “yes”.

Here is a trace of AILog

ailog: load ’elect_bug2.ail’.
AILog theory elect_bug2.ail loaded. 

ailog: ask lit_l1.
Answer: lit_l1.
  Runtime since last report: 0.0 secs. 
    [ok,more,how,help]: how.
     lit_l1 <-
       1: light_l1 
       2: live_l1 
       3: ok_l1
     How? [Number,up,retry,ok,prompt,help]: how 2. 
     live_l1 <-
       1: live_w0 
     How? [Number,up,retry,ok,prompt,help]: how 1. 
     live_w0 <-
       1: live_w1 
       2: up_s2 
     How? [Number,up,retry,ok,prompt,help]: how 1. 
     live_w1 <-
       1: live_w3 
       2: up_s1 
     How? [Number,up,retry,ok,prompt,help]: how 2. 
up_s1 is a fact

The buggy clause is

up_s1.

The minimal conflicts are: { d } , { e, g } and { h }.

The general idea is to make the reliability of the source assumable.

(a)

a <- h & reliable_s_1.
d <- c & reliable_s_1.

e <- d & reliable_s_2.
f <- k & reliable_s_2.
z <- g & reliable_s_2.
j <- reliable_s_2.

h <- d & reliable_s_3.

a <- b & e & reliable_s_4.
b <- c & reliable_s_4.

g <- f & j & reliable_s_5.

false <- a & z.
c.
k.

assumable reliable_s_1.
assumable reliable_s_2.
assumable reliable_s_3.
assumable reliable_s_4.
assumable reliable_s_5.

% Try:
% ask false.

(b) There are two minimal conflicts:
[ reliable(s₁), reliable(s₃), reliable(s₂), reliable(s₅) ]
and
[ reliable(s₄), reliable(s₁), reliable(s₂), reliable(s₅) ].

(c) Those elements that are in all conflicts can account for the contradiction. This means that s₁, s₂ and s₅ can account for the contradiction.

(d) The only pair of sources that could account for the contradiction are those obtained by pairing the elements of the two conflicts that are not in the intersection of the conflicts. This means that there is one such pair { s₃, s₄ } .