Enhance error output if exploration counterexample is invalid

In the case the counterexample provided by the expert does
invalidated some already confirmed implications, these implications
are printed as error output.  Please note that this (again) only works
for reasonably small explorations — for larger ones, you may need to
use another handler.

This feature was suggested by Johannes Wollbold

Signed-off-by: Daniel Borchmann <daniel.borchmann@mailbox.tu-dresden.de>