Apply the DPLL algorithm to prove if the following 3-CNF formula is satisfaiable. In particular, show the sequence of formula manipulating operation and at the same time show how the formula it is modified.

^ = and ~ = not

(~a V ~b V ~c ) ^ ( a V ~b V ~c ) ^ ( ~a V b V ~c) ^ (~a V ~b V c) ^ ( ~a V b V c ) ^ ( a V ~b V c) ^ (a V b V ~c) ^ (a V b V c)