`checkImplicationWorker` presents misleading state when a proof is stuck

[jberthold]

When inspecting a unit test:

This state is returned and printed to the user, but it is not the proof state which is stuck. It is an artefact from the checking algorithm. In case of NotImplied, the check routine returns the original claimPattern, whereas here (NotImpliedStuck) it returns part of its negation.

This will confuse users.

Related: #3218 , possibly #3116

Scope

Investigate whether more useful output can be presented to the user in stuck states.
If this is not possible, print additional information for the user to understand the output.