Yikes! O.o What I call "resolvents" above are not. Resolvents are the clauses that result from the elimination of complementary literals found by DFS. Haha. Goo

Yikes! O.o What I call "resolvents" above are not. Resolvents are the clauses that result from the elimination of complementary literals found by DFS. Haha. Good thing I sometimes go back and re-read my old comments...