write a Prolog program that transforms a given propositional formula into conjunc- tive normal form. In this, follow the example program given in Section 2.9 of Fittings book, which shows a program to transform a propositional formula into disjunctive normal form.

In your program, you need to define the unary operator neg and the binary operators and, or, imp, revimp, uparrow, downarrow, notimp, and notrevimp, which denote the eight aforemen- tioned primary connectives (see Table 2.1 in the book). Also reuse the predicates conjunctive/1, disjunctive/1 that recognise - and -formulas, and the predicates components/3 and component/2 that split formulas into their components (see Table 2.2 in the book). The interface of this part of the program should be a predicate clauseform(X,Y), where Y is the conjunctive normal form of the formula X. For example, for the query ?- clauseform(a imp b, Y)., the result should be Y=[[neg a, b]], and for the query ?- clauseform(neg(a uparrow b), Y), the result should be Y=[[a],[b]].

Then augment your program so that it can also handle the secondary binary operators equiv and notequiv (see Table 2.1 in the book). Finally, test your program on larger formulas containing all of the operators mentioned before.

As a second step, implement the atomic resolution rule using predicates resolutionstep/2 and resolution/2 (analogous to singlestep/2 and expand/2, respectively), and a check for a closed resolution expansion (explained in Section 3.3 of the book), and put these together, following the implementation described in Section 3.2, and the remarks at the end of Section 3.3. The outermost interface of your program should be a predicate test/1, which takes a propositional formula as input, and prints YES if it has a proposition proof, and NO otherwise.

You may also want to think about ways of making your program more efficient, by eliminating duplicate variables and clauses early on in the process.