Preliminary version of the demo kitchen BAT.

The performance in the C implementation was very bad. The reason was:

<QUOTE about C-implementation>

The resulting setups are huge and grow linearly in the number of
actions, and query evaluation seems to grow quadratically in the size
of the setup.

The split optimizations in setup are still worth their cost (replacing
setup_clause_small_pel() with setup_full_pel() costs about 20% and
removing the expensive part of setup_relevant_split() costs 1000%).

</QUOTE about C-implementation>
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.
Fixed: missing assignment in Formula::Cnf::C::Substitute().

Since this bug is fixed, the fol_incompleteness test fails.
The test asserts that (x. P(x)) v (Ex. ~P(x)) cannot be proven. But
since in both branches there is just one variable, it just tries one
standard name. Probably that should be more. Needs to be investigated.
Added kitchen scenario from the demo.

* BATs are a single library now.