Here is my start command for the example we are working on Wednesday the 25th.
This is not assigned; it is an extra credit opportunity.

s "((Ax1.P1(x1))->(Ax2.(Ex3.x2 R2 x3))) & (Ax1.(Ax2.(Ax3.x1 R2 x2 & x2 R2 x3 -> x1 R3 x3))) & (Ax1.P1(x1)v~P4(x1)) & (Ax1.(Ax2.(P4(x1)&~P4(x2)->x1R3x2))) & ((~(Ex1.P4(x1))->(Ex2.x2 R3 x2))) -> (Ex1.(Ex2.x1 R3 x2))";