Do exercise 20.1 on page 446, but with the following
modification: reverse the order of the arguments in each call to
resolution listed in the exercise. To make sure that your MGUs
really are MGUs, remember that the MGU of two
terms should unify those terms when applied to them in a single pass;
it shouldn't be necessary to do substitutions and then further
substitions in the result.
Do exercise 20.2 on page 446.
Do exercise 20.3 on page 446.
Do exercise 20.5 on page 447.