Homework one:

Question 1: Input two propositional clauses and output the result of resolving
them together, or output "Resolution Failed".

The clauses are in the form A | -B | ... | Z. Each literal is a single letter,
possibly preceded by a negation sign "-".

Code to input, store and output clauses is supplied in:

/afs/cs/class/cs222/homework/one/resolve.c




Question 2: Input two terms and output their most general unifier, if one
exists or "Unification Failed".

Terms are of the form f(g(X,a)). Where small letters are used for constant and
function names, and capitals for variables.

Code to input, store and output terms is supplied in:

/afs/cs/class/cs222/homework/one/unify.c