Implemented consistency checks.

Each setup caches consistency results for different k.
Whether or not the setup is consistent is updated in
setup_add_sensing_result() by checking if the negation of the SF literal
is entailed. That should be much faster than checking if the empty
clause is entailed because the relevant PEL for the SF literal is
sufficient.