Confluence check: improve debug output in case of a single (controllable) event in the specification

For a single controllable event, there are no pairs. There are thus also no proven pairs, but also no pairs that can't be proven. We then get the following messages as debug output:

• No proven pairs.
• All pairs proven. Confluence holds.

This is confusing, as it seems it couldn't prove it, but it also proved it. I think we should detect this as special case, and instead of these two lines, print No pairs. Confluence holds..

Addresses #892