Can't prove NOT (a IFF NOT a)

[Quelklef]

... because doing so first requires establishing LEM, which the bot doesn't know how to do.