Exercise 7.30 [dpll-fc-exercise]

Trace the behavior of {DPLL} on the knowledge base in Figure pl-horn-example-figure when trying to prove $Q$, and compare this behavior with that of the forward-chaining algorithm.