Once negated, consider the conjunctive normal form (CNF) of the goal if it is
not printable as is. This prevents failures on formula which are OK besides
their form. Indeed, CNF is logically equivalent to the original formula.

- Update to new stdlib organization.
- All properties in a single file, with formulation closer to the original.