according to proof by contradiction, it is : KB AND ¬Alpha ( we show is unsatisfiable to prove KB entails Alpha)

but in the example, it is Alpha = ¬P12

So then ¬ Alpha is: ¬(¬P12), will become just P12 and so it is reflected in Figure 7.13

Right?!