Artificial intelligence

6 points) Consider the following first-order predicate calculus statements, which have already been written in Skolemized clause form. Write all pairs of clauses below that can resolve (there are 6 of them). If a pair resolves, give the resulting substitution given by unification along with the resolution. Note: I am not asking you to give a complete proof, just the result of one resolution at a time. a. inst(sk(?a), human) v mortal(sk0(?a)) b. inst(Socrates, human) c. ~mortal(?b) d. ~inst(?c,?d) e. inst(Socrates, 2e) f. -inst(?f, human) v-married(spouse-of(?f) v single(?0) g. married(spouse-of(Socrates)