Part of the axiom meta-issue issue924.

Updated the title of the issue: we now commit to restricting derived variables to binary (true/false) domains. This needs to be enforced at the code level and documented, and we should point out somewhere (in the code is perhaps enough) that this differs from the AIJ translator paper.

To simplify things, I think we should then also make clear which of the two domain values stands for "false" and which one stands for "true". (This matters for negation-by-failure semantics.)

See issue458.

The AIJ translator paper associates layers with axiom *rules*, not with axiom
*variables*. This is more general because it allows for non-binary derived
variables. (In our implementation's version, non-binary derived variables would
either be trivial, i.e. certain values could never be achieved, or they'd
violate the layering property in the AIJ translator paper.)

For people who directly generate FDR tasks rather than go through our
translator, we should either support the more general case, or at least properly
document the restriction of derived variables to the binary case.