How to submit the 3rd home assignment

• For the first part, you should derive the clausal form step by step and give a resolution proof. You should also indicate the most general unifiers and the renaming of variables in each step of the proof. This part is to be done by hand.
• For the second part, submit the input file for OTTER together with explanations for sentences therein. In addtition to this, attach some proofs (including queries) that you can find using OTTER. Give also a query for which OTTER does not find a proof (in this case, OTTER loops for ever or announces that "sos is empty" and stops). This is to ensure the consistency of your sentences.
• It is strongly recommended that your submission does not exceed 10 pages.
• The deadline is the 7th of December, 1998.

OTTER is available in the machines named as "alpha", "beta", "gamma" and so on. The command "use otter" updates the path variables of your shell so that otter becomes available.