Add a few negative examples

[septract]

Creates a subdirectory negative-examples containing examples should always fail.

(In the other subdirectories of example-archive, proofs that fail represent true properties that cannot be established by CN for whatever reason).

[dc-mak]

Lgtm, though maybe naming it "should-fail" or "expected-fail" would be clearer? We need to think about the types of error we have and how to name and signal them...