Understood the problem from commit c6c66a8a (it's an ESL bug).

In commit c6c66a8a, I had written:

    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.

That's a `bug' of ESL. SSAs alone cannot trigger unit resolution,
obviously, because they are no clauses (usually). The example (from the
kitchen domain) worked only if we split dynamic literals because then
the literal [z.n]SF(n) was split as well. But that's hardly intuitive
and only works for sensing.

ESL does NOT satisfy the following property in general:
Suppose action n does not occur in the SSAs of p and q. Then:
  |= [z] B_k(p v q) -> [z.n] B_k(p v q)