Here's another example of the use of Refutation + Resolution +
Unification to show the validity of a first-order inference:

Show that the following inference is valid:

	Ax[Px v Qx], Ex[-Px] |- Ex[Qx]

1.  Convert all premises to Clause Form:

	Ax[Px v Qx] -> Px v Qx -> {PxQx}, where "->" means "rewrites as"

	Ex[-Px] -> {-Pc}, where c is a Skolem constant

2.  Convert the negation of the conclusion (for Refutation) to Clause Form:

	-Ex[Qx] -> Ax[-Qx] -> {-Qx}

3.  Union the above, renaming variables:

	{PxQx, -Pc, -Qy}

4.  Apply Resolution to derive {}.  Where Unification is needed in
    order to do this, show the MGU.

	PxQx	-Pc	Qy
          \      /      /
           \    /      /
      {c/x} \  /      /
             \/      /
             Qc     /
              \    /
         {c/y} \  /
                \/
                {}       

    Alternatively:

	PxQx    -Qy	-Pc
          \     /        /
     {x/y} \   /        /
            \ /        /
             Px       / {c/x}
              \      /
               \    /
                \  /
                 \/
                 {}