<p>The calculus <b>C</b> was introduced by H. Wansing as a constructive logic with strong negation. In addition, <b>C</b> validates the theses of connexive logic that are attributed to Aristotle and Boethius. A further remarkable property of <b>C</b> is that it is a non-trivial but negation inconsistent system: it has a formula and its negation as theorems. From a bilateralist-minded perspective, such a contradiction can be seen as the existence of both a verification and a falsification of one and the same formula. Relatedly, it has been noted by Wansing that there seems to be a kind of correspondence between these two types of derivations when it comes to a proof of contradiction. Following this observation, we attempt in this paper to introduce a precise notion for such a correspondence. We thence establish that this correspondence obtains in propositional and first-order versions of <b>C</b>, via formulations of suitable sequent and tableau calculi.</p>