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.

(a) The minimal explanations of get_gun are { hunting } and { robbing } .

(b) The minimal explanations of get_gun ∧ goto_bank are { hunting, banking } and { robbing }

© Observing puton_goodShoes would remove the first explanation as it is inconsistent.

  However, you would still need to be able to explain it. This could be done by making //puton_goodShoes// assumable.

(d) { banking } and { robbing } .

(e) { hunting, banking }