I have become knowledgeable about using Prover 9 to do resolutions.

I am now working on my second homework assignment in knowledge representation. To do both problems I need to use Otter or its modern implementation Prover 9. I have written all the formulas now for one problem into Prover 9 input files. Now I need to consult my course notes and the lecturer's slides to see how and what to set my goals to in Prover 9. I may move on now to the second problem and write that up into input files. I have about 12 hours to do this work. I must also do a write up and then make a pdf of that and burn all the files to CD.