Added a test for eventual completeness.

Eventual completeness is not given for non-fluent formulas due to
special treatment of SF in splitting, but for fluent formulas it should
hold.