A     [A -> not B] 1
   ----------------------
         not B                B
       --------------------------
              bottom
         ---------------- [1]
          not(A -> not B)