Translating Free-Variable Tableaux
A free-variable tableau with root
x(Fx &
y~Fy)
closes after 4 nodes and 1 application of Closure. A standard tableau, on the other hand, will have at least 6 nodes because the root formula must be used twice. So translating free-variable tableaux into standard tableaux is not as easy as I once thought. I wonder if it would suffice to add a rule to the free-variable construction that forbids Closure to unify a variable with a constant that first appears after the variable on the branch.