 Like Nelson’s four-valued constructive logic N4, C is a paraconsistent logic (cf. the entry  logic: paraconsistent).  Note that C contains contradictions, for example: ⊢C ((p ∧ ~p) → (~ p ∨ p)) and ⊢C ~((p ∧ ~p) → (~ p ∨ p)). It is obvious from the above presentation that C differs from N4 only with respect to the falsification (or support of falsity) conditions of implications. As in N4, provable strong equivalence is a congruence relation, i.e., the set {A : ⊢C A} is closed under the rule A ↔ B, ~ A ↔ ~ B / C(A) ↔ C(B). Wansing (2005) also introduces a first-order extension QC of C. Kamide and Wansing (2011) present a sound and complete sequent calculus for C and show the cut-rule to be admissible, which means that it can be dispensed with.