lisp program need to be done

Resolution theorem proover Write a program which takes as a input Statement1 Statement2 Conclusion Statement1 and Statement2 are the facts. We have to proove the Conclusion using resolution. The above three are infix expressions of first order predicate logic. Expression may have symbols,variables, existential quantifiers, universal quantifiers. Part 1: Convert all three expressions to CNF(Conjective Normal Form) form. a)While converting to CNF, If clauses have variables, Standardize variables 1. For sentences like (?x P(x)) ? (?x Q(x)) which use the same variable name twice, change the name of one of the variables. This avoids confusion later when we drop the quantifiers. 2. From ?x [?y Animal(y) ? ¬Loves(x, y)] ? [?y Loves(y, x)]. we obtain: ?x [?y Animal(y) ? ¬Loves(x, y)] ? [?z Loves(z,x)]. b)Removing quantifiers Existential Quantifiers are converted to skolem functions. Universal Quantifiers are dropped after variables are standardized. Part 2: Add individual clauses generated by converting to conjuctive normal form to a database using lisp alists. Add the negation of the conclusion to the database. Part 3: Resolution Try to find a contradiction by combining two clauses from the database. If we find a contradiction we exit, thus Conclusion is proven. If not we continue our search. If the clauses have variables use unification algorithm to equate the two clause. Sample formats (or p q) (implies p q) (not r) (forall ?x (forall ?y (exists ?z (implies (P ?x ?y) (Q ?x ?y ?z))))) this is equivalent to ?x [?y [?z [ P(x,y) -> Q(x,y,z) ]]] Note: A '?' before symbol indicates variable.