Write a Propositional-logic-theorem-prover to determine if a well formed formula is a tautology. Performs proofs by contradiction by first negating the wff and converting it into cnf. Then, each conjunct of the result is turned into a clause. Resolution is applied to both these original clauses and new clauses produced during the proof until either nil is produced or all pairs of clauses have been tried.
(Note: The prover has to be written in common lisp, actually i found code that worked in github that you can use, but you gotta change some of the code so that it wont cause problem, you know to pass the code check or something... which means it can become a code partially rewrite thing depends on how you think)