Fixed: splitting only initial literals is not sufficient.

The PEL optimization is too much. When we sense [z]SF(n) and have
[z](SF(n) <-> p v q), we want to know (p v q) for k = 0.
That must be checked out.