[d03a044ec35d4d9a3f6d0f5118bc4f8a02a08e61fe7815b2002d007f]
(1) C0C1.0              -    CpCqp            -    0\imply(1\imply0)
(2) CC0C1.2CC0.1C0.2    -    CCpCqrCCpqCpr    -    (0\imply(1\imply2))\imply((0\imply1)\imply(0\imply2))
(3) CCN0N1C1.0          -    CCNpNqCqp        -    (\not0\imply\not1)\imply(1\imply0)
(4) CL0.0               -    CLpp             -    \nece0\imply0
(5) CLC0.1CL0L1         -    CLCpqCLpLq       -    \nece(0\imply1)\imply(\nece0\imply\nece1)
(6) CNLN0LNLN0          -    CNLNpLNLNp       -    \not\nece\not0\imply\nece\not\nece\not0
Supports necessitation steps.
#removals;1:0,2:0,3:0,4:1,5:6,6:6,7:19,8:29,9:83,10:102,11:279,12:422,13:1014,14:1596,15:3648,16:6016,17:13307,18:22703,19:48921,20:86809,21:183513,22:334530,23:699371,24:1304710