An inference machine on a CNF knowledge base using resolution.

Basic usage is (print-knowledge (make-inferences (read-kbdb "filename"))). Knowledge base must have one clause per line, see example knowledge-base.