;; Answers to Questions 20 to 64.
;;
;; This proof script was made by Naoki Takashima on Dec. 3, 2010.
;;

[20]

;; z1 >
(assume :a A)
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z1-2 >>
  :a
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z1-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :A))
;; z2 >
(set! A20 z)
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :A))
;; z3 >
(proves? A20 [] (A => A))
;;  => [] : <List>


[21]

;; z4 >
(assume :x (A => B))
  ;; z4-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
  ;; z4-2 >>
  (assume :y A)
    ;; z4-2-1 >>>
    :y
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z4-2-2 >>>
    (impE :x :y)
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z4-2-3 >>>
    (set! A21 z)
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z4-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
  ;; z4-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/var :B)) (Prop/=> (Prop/var :A) (Prop/var :B)))
;; z5 >
(proves? A21 [(A => B) A] B)
;;  => [] : <List>


[22]

;; z7 >
(assume :x (A => (B => C)))
  ;; z7-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/var :C)))
  ;; z7-2 >>
  (assume :b B)
    ;; z7-2-1 >>>
    :b
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z7-2-2 >>>
    (assume :a A)
      ;; z7-2-2-1 >>>>
      :a
      ;;  => -- : <Proof> of (Prop/var :A)
      ;; z7-2-2-2 >>>>
      (impE :x :a)
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :C))
      ;; z7-2-2-3 >>>>
      (impE z :b)
      ;;  => -- : <Proof> of (Prop/var :C)
      ;; z7-2-2-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :C))
    ;; z7-2-3 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/=> (Prop/var :A) (Prop/var :C)))
  ;; z7-3 >>
  (set! A22 z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/=> (Prop/var :A) (Prop/var :C)))
  ;; z7-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/var :C))) (Prop/=> (Prop/var :B) (Prop/=> (Prop/var :A) (Prop/var :C))))
;; z8 >
(proves? A22 [(A => (B => C))] (B => (A => C)))
;;  => [] : <List>


[23]

;; z9 >
(assume :x A)
  ;; z9-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z9-2 >>
  (andI :x :x)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :A))
  ;; z9-3 >>
  (set! A23 z)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :A))
  ;; z9-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/&& (Prop/var :A) (Prop/var :A)))
;; z10 >
(proves? A23 [A] (A && A))
;;  => [] : <List>


[24]

;; z11 >
(assume :x (A && A))
  ;; z11-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :A))
  ;; z11-2 >>
  (andEL :x)
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z11-3 >>
  (set! A24 z)
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z11-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :A)) (Prop/var :A))
;; z12 >
(proves? A24 [(A && A)] A)
;;  => [] : <List>


[25]

;; z13 >
(assume :x A)
  ;; z13-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z13-2 >>
  (orI (A || A) :x)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :A))
  ;; z13-3 >>
  (set! A25 z)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :A))
  ;; z13-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/|| (Prop/var :A) (Prop/var :A)))
;; z14 >
(proves? A25 [A] (A || A))
;;  => [] : <List>


[26]

;; z15 >
(assume :x (A || A))
  ;; z15-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :A))
  ;; z15-2 >>
  (assume :a A)
    ;; z15-2-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z15-2-2 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z15-2-3 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :A))
  ;; z15-3 >>
  (set! aa z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :A))
  ;; z15-4 >>
  (orE :x aa aa)
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z15-5 >>
  (set! A26 z)
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z15-6 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/var :A)) (Prop/var :A))
;; z16 >
(proves? A26 [(A || A)] A)
;;  => [] : <List>


[27]

;; z17 >
(assume :x A)
  ;; z17-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z17-2 >>
  (assume :y B)
    ;; z17-2-1 >>>
    :y
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z17-2-2 >>>
    :x
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z17-2-3 >>>
    (set! A27 z)
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z17-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :A))
  ;; z17-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/var :A)))
;; z18 >
(proves? A27 [A B] A)
;;  => [] : <List>


[28]

;; z19 >
(assume :x (A && B))
  ;; z19-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
  ;; z19-2 >>
  (andEL :x)
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z19-3 >>
  (set! a z)
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z19-4 >>
  (andER :x)
  ;;  => -- : <Proof> of (Prop/var :B)
  ;; z19-5 >>
  (set! b z)
  ;;  => -- : <Proof> of (Prop/var :B)
  ;; z19-6 >>
  (andI b a)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :B) (Prop/var :A))
  ;; z19-7 >>
  (set! A28 z)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :B) (Prop/var :A))
  ;; z19-8 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :B) (Prop/var :A)))
;; z20 >
(proves? A28 [(A && B)] (B && A))
;;  => [] : <List>


[29]

;; z21 >
(assume :x (A || B))
  ;; z21-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
  ;; z21-2 >>
  (set! ba (B || A))
  ;;  => (Prop/|| (Prop/var :B) (Prop/var :A)) : <Prop>
  ;; z21-3 >>
  (assume :a A)
    ;; z21-3-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z21-3-2 >>>
    (orI ba :a)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :A))
    ;; z21-3-3 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :A)))
  ;; z21-4 >>
  (set! aa z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :A)))
  ;; z21-5 >>
  (assume :b B)
    ;; z21-5-1 >>>
    :b
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z21-5-2 >>>
    (orI ba :b)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :A))
    ;; z21-5-3 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/|| (Prop/var :B) (Prop/var :A)))
  ;; z21-6 >>
  (set! bb z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/|| (Prop/var :B) (Prop/var :A)))
  ;; z21-7 >>
  (orE :x aa bb)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :A))
  ;; z21-8 >>
  (set! A29 z)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :A))
  ;; z21-9 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/|| (Prop/var :B) (Prop/var :A)))
;; z22 >
(proves? A29 [(A || B)] (B || A))


[30]

;; z23 >
(assume :x ((A && B) && C))
  ;; z23-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/&& (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/var :C))
  ;; z23-2 >>
  (set! ab (andEL :x))
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
  ;; z23-3 >>
  (set! a (andEL ab))
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z23-4 >>
  (set! b (andER ab))
  ;;  => -- : <Proof> of (Prop/var :B)
  ;; z23-5 >>
  (set! c (andER :x))
  ;;  => -- : <Proof> of (Prop/var :C)
  ;; z23-6 >>
  (andI b c)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :B) (Prop/var :C))
  ;; z23-7 >>
  (andI a z)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/&& (Prop/var :B) (Prop/var :C)))
  ;; z23-8 >>
  (set! A30 z)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/&& (Prop/var :B) (Prop/var :C)))
  ;; z23-9 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/var :C)) (Prop/&& (Prop/var :A) (Prop/&& (Prop/var :B) (Prop/var :C))))
;; z24 >
(proves? A30 [((A && B) && C)] (A && (B && C)))
;;  => [] : <List>


[31]

;; z1 >
(assume :x ((A || B) || C))
  ;; z1-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/|| (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/var :C))
  ;; z1-2 >>
  (set! r (A || (B || C)))
  ;;  => (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))) : <Prop>
  ;; z1-3 >>
  (assume :ab (A || B))
    ;; z1-3-1 >>>
    :ab
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
    ;; z1-3-2 >>>
    (assume :a A)
      ;; z1-3-2-1 >>>>
      :a
      ;;  => -- : <Proof> of (Prop/var :A)
      ;; z1-3-2-2 >>>>
      (orI r :a)
      ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
      ;; z1-3-2-3 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
    ;; z1-3-3 >>>
    (set! aTr z)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
    ;; z1-3-4 >>>
    (assume :b B)
      ;; z1-3-4-1 >>>>
      :b
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z1-3-4-2 >>>>
      (orI (B || C) :b)
      ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :C))
      ;; z1-3-4-3 >>>>
      (orI r z)
      ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
      ;; z1-3-4-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
    ;; z1-3-5 >>>
    (set! bTr z)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
    ;; z1-3-6 >>>
    (orE :ab aTr bTr)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
    ;; z1-3-7 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
  ;; z1-4 >>
  (set! abTr z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
  ;; z1-5 >>
  (assume :c C)
    ;; z1-5-1 >>>
    :c
    ;;  => -- : <Proof> of (Prop/var :C)
    ;; z1-5-2 >>>
    (orI (B || C) :c)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :C))
    ;; z1-5-3 >>>
    (orI r z)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
    ;; z1-5-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :C) (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
  ;; z1-6 >>
  (set! cTr z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :C) (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
  ;; z1-7 >>
  (orE :x abTr cTr)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
  ;; z1-8 >>
  (set! A31 z)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
  ;; z1-9 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/var :C)) (Prop/|| (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
;; z2 >
(proves? A31 [((A || B) || C)] (A || (B || C)))
;;  => [] : <List>


[32]

;; z3 >
(assume :x (A && (B || C)))
  ;; z3-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
  ;; z3-2 >>
  (set! a (andEL :x))
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z3-3 >>
  (set! borc (andER :x))
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :C))
  ;; z3-4 >>
  (assume :b B)
    ;; z3-4-1 >>>
    :b
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z3-4-2 >>>
    (andI a :b)
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
    ;; z3-4-3 >>>
    (orI ((A && B) || (A && C)) z)
    ;;  => -- : <Proof> of (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C)))
    ;; z3-4-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C))))
  ;; z3-5 >>
  (set! bTr z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C))))
  ;; z3-6 >>
  (assume :c C)
    ;; z3-6-1 >>>
    :c
    ;;  => -- : <Proof> of (Prop/var :C)
    ;; z3-6-2 >>>
    (andI a :c)
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :C))
    ;; z3-6-3 >>>
    (orI ((A && B) || (A && C)) z)
    ;;  => -- : <Proof> of (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C)))
    ;; z3-6-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :C) (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C))))
  ;; z3-7 >>
  (set! cTr z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :C) (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C))))
  ;; z3-8 >>
  (orE borc bTr cTr)
  ;;  => -- : <Proof> of (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C)))
  ;; z3-9 >>
  (set! A32 z)
  ;;  => -- : <Proof> of (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C)))
  ;; z3-10 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))) (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C))))
;; z4 >
(proves? A32 [(A && (B || C))] ((A && B) || (A && C)))
;;  => [] : <List>


[33]

;; z5 >
(assume :x ((A && B) || (A && C)))
  ;; z5-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C)))
  ;; z5-2 >>
  (set! r (A && (B || C)))
  ;;  => (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))) : <Prop>
  ;; z5-3 >>
  (assume :ab (A && B))
    ;; z5-3-1 >>>
    :ab
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
    ;; z5-3-2 >>>
    (set! a (andEL :ab))
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z5-3-3 >>>
    (set! b (andER :ab))
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z5-3-4 >>>
    (orI (B || C) b)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :C))
    ;; z5-3-5 >>>
    (andI a z)
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
    ;; z5-3-6 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
  ;; z5-4 >>
  (set! abTr z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
  ;; z5-5 >>
  (assume :ac (A && C))
    ;; z5-5-1 >>>
    :ac
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :C))
    ;; z5-5-2 >>>
    (set! a (andEL :ac))
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z5-5-3 >>>
    (set! c (andER :ac))
    ;;  => -- : <Proof> of (Prop/var :C)
    ;; z5-5-4 >>>
    (orI (B || C) c)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :C))
    ;; z5-5-5 >>>
    (andI a z)
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
    ;; z5-5-6 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :C)) (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
  ;; z5-6 >>
  (set! acTr z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :C)) (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
  ;; z5-7 >>
  (orE :x abTr acTr)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
  ;; z5-8 >>
  (set! A33 z)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C)))
  ;; z5-9 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/&& (Prop/var :A) (Prop/var :C))) (Prop/&& (Prop/var :A) (Prop/|| (Prop/var :B) (Prop/var :C))))
;; z6 >
(proves? A33 [((A && B) || (A && C))] (A && (B || C)))
;;  => [] : <List>


[34]

;; z1 >
(assume :x ((A && B) => C))
  ;; z1-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/var :C))
  ;; z1-2 >>
  (assume :a A)
    ;; z1-2-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z1-2-2 >>>
    (assume :b B)
      ;; z1-2-2-1 >>>>
      :b
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z1-2-2-2 >>>>
      (andI :a :b)
      ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
      ;; z1-2-2-3 >>>>
      (impE :x z)
      ;;  => -- : <Proof> of (Prop/var :C)
      ;; z1-2-2-4 >>>>
      (set! c z)
      ;;  => -- : <Proof> of (Prop/var :C)
      ;; z1-2-2-5 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :C))
    ;; z1-2-3 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/var :C)))
  ;; z1-3 >>
  (set! A34 z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/var :C)))
  ;; z1-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/var :C)) (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/var :C))))
;; z2 >
(proves? A34 [((A && B) => C)] (A => (B => C)))
;;  => [] : <List>


[35]

;; z3 >
(assume :x (A => (B => C)))
  ;; z3-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/var :C)))
  ;; z3-2 >>
  (assume :ab (A && B))
    ;; z3-2-1 >>>
    :ab
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
    ;; z3-2-2 >>>
    (set! a (andEL :ab))
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z3-2-3 >>>
    (set! b (andER :ab))
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z3-2-4 >>>
    (impE :x a)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :C))
    ;; z3-2-5 >>>
    (impE z b)
    ;;  => -- : <Proof> of (Prop/var :C)
    ;; z3-2-6 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/var :C))
  ;; z3-3 >>
  (set! A35 z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/var :C))
  ;; z3-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/var :C))) (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/var :C)))
;; z4 >
(proves? A35 [(A => (B => C))] ((A && B) => C))
;;  => [] : <List>


[36]

;; z7 >
(assume :x B)
  ;; z7-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/var :B)
  ;; z7-2 >>
  (assume :a A)
    ;; z7-2-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z7-2-2 >>>
    :x
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z7-2-3 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
  ;; z7-3 >>
  (set! A36 z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
  ;; z7-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/=> (Prop/var :A) (Prop/var :B)))
;; z8 >
(proves? A36 [B] (A => B))
;;  => [] : <List>


[37]

;; z9 >
(assume :x A)
  ;; z9-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z9-2 >>
  (assume :y (~~ B))
    ;; z9-2-1 >>>
    :y
    ;;  => -- : <Proof> of (Prop/~~ (Prop/var :B))
    ;; z9-2-2 >>>
    (assume :ab (A => B))
      ;; z9-2-2-1 >>>>
      :ab
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
      ;; z9-2-2-2 >>>>
      (impE :ab :x)
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z9-2-2-3 >>>>
      (notE :y z)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z9-2-2-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/var :B)) (Prop/false))
    ;; z9-2-3 >>>
    (notI z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/=> (Prop/var :A) (Prop/var :B)))
    ;; z9-2-4 >>>
    (set! A37 z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/=> (Prop/var :A) (Prop/var :B)))
    ;; z9-2-5 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/~~ (Prop/=> (Prop/var :A) (Prop/var :B))))
  ;; z9-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/~~ (Prop/=> (Prop/var :A) (Prop/var :B)))))
;; z10 >
(proves? A37 [A (~~ B)] (~~ (A => B)))
;;  => [] : <List>


[38]

;; z11 >
(assume :x (~~ A))
  ;; z11-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z11-2 >>
  (assume :y (~~ B))
    ;; z11-2-1 >>>
    :y
    ;;  => -- : <Proof> of (Prop/~~ (Prop/var :B))
    ;; z11-2-2 >>>
    (assume :a A)
      ;; z11-2-2-1 >>>>
      :a
      ;;  => -- : <Proof> of (Prop/var :A)
      ;; z11-2-2-2 >>>>
      (notE :x :a)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z11-2-2-3 >>>>
      (falseE B z)
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z11-2-2-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
    ;; z11-2-3 >>>
    (set! A38 z)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
    ;; z11-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/=> (Prop/var :A) (Prop/var :B)))
  ;; z11-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/=> (Prop/var :A) (Prop/var :B))))
;; z12 >
(proves? A38 [(~~ A) (~~ B)] (A => B))
;;  => [] : <List>


[39]

;; z13 >
(assume :x A)
  ;; z13-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z13-2 >>
  (assume :na (~~ A))
    ;; z13-2-1 >>>
    :na
    ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
    ;; z13-2-2 >>>
    (notE :na :x)
    ;;  => -- : <Proof> of (Prop/false)
    ;; z13-2-3 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/false))
  ;; z13-3 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/~~ (Prop/var :A)))
  ;; z13-4 >>
  (set! A39 z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/~~ (Prop/var :A)))
  ;; z13-5 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/~~ (Prop/~~ (Prop/var :A))))
;; z14 >
(proves? A39 [A] (~~ (~~ A)))
;;  => [] : <List>


[40]

;; z15 >
(assume :x (~~ A))
  ;; z15-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z15-2 >>
  (set! A40 z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z15-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/~~ (Prop/var :A)))
;; z16 >
(proves? A40 [(~~ A)] (~~ A))
;;  => [] : <List>


[41]

;; z17 >
(assume :x A)
  ;; z17-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z17-2 >>
  (assume :y B)
    ;; z17-2-1 >>>
    :y
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z17-2-2 >>>
    (andI :x :y)
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
    ;; z17-2-3 >>>
    (set! A41 z)
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
    ;; z17-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/&& (Prop/var :A) (Prop/var :B)))
  ;; z17-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/&& (Prop/var :A) (Prop/var :B))))
;; z18 >
(proves? A41 [A B] (A && B))
;;  => [] : <List>


[42]

;; z20 >
(assume :x (~~ B))
  ;; z20-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :B))
  ;; z20-2 >>
  (assume :ab (A && B))
    ;; z20-2-1 >>>
    :ab
    ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
    ;; z20-2-2 >>>
    (andER :ab)
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z20-2-3 >>>
    (notE :x z)
    ;;  => -- : <Proof> of (Prop/false)
    ;; z20-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/false))
  ;; z20-3 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B)))
  ;; z20-4 >>
  (set! A42 z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B)))
  ;; z20-5 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B))))
;; z21 >
(proves? A42 [(~~ B)] (~~ (A && B)))
;;  => [] : <List>


[43]

;; z22 >
(assume :x (~~ A))
  ;; z22-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z22-2 >>
  (assume :y B)
    ;; z22-2-1 >>>
    :y
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z22-2-2 >>>
    (assume :ab (A && B))
      ;; z22-2-2-1 >>>>
      :ab
      ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
      ;; z22-2-2-2 >>>>
      (andEL :ab)
      ;;  => -- : <Proof> of (Prop/var :A)
      ;; z22-2-2-3 >>>>
      (notE :x z)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z22-2-2-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/false))
    ;; z22-2-3 >>>
    (notI z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B)))
    ;; z22-2-4 >>>
    (set! A43 z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B)))
    ;; z22-2-5 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B))))
  ;; z22-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/=> (Prop/var :B) (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B)))))
;; z23 >
(proves? A43 [(~~ A) B] (~~ (A && B)))
;;  => [] : <List>


[44]

;; z24 >
(assume :x A)
  ;; z24-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z24-2 >>
  (orI (A || B) :x)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
  ;; z24-3 >>
  (set! A44 z)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
  ;; z24-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/|| (Prop/var :A) (Prop/var :B)))
;; z25 >
(proves? A44 [A] (A || B))
;;  => [] : <List>


[45]

;; z26 >
(assume :x B)
  ;; z26-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/var :B)
  ;; z26-2 >>
  (orI (A || B) :x)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
  ;; z26-3 >>
  (set! A45 z)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
  ;; z26-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/|| (Prop/var :A) (Prop/var :B)))
;; z27 >
(proves? A45 [B] (A || B))
;;  => [] : <List>


[46]

;; z28 >
(assume :x (~~ A))
  ;; z28-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z28-2 >>
  (assume :y (~~ B))
    ;; z28-2-1 >>>
    :y
    ;;  => -- : <Proof> of (Prop/~~ (Prop/var :B))
    ;; z28-2-2 >>>
    (assume :ab (A || B))
      ;; z28-2-2-1 >>>>
      :ab
      ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
      ;; z28-2-2-2 >>>>
      (assume :a A)
        ;; z28-2-2-2-1 >>>>>
        :a
        ;;  => -- : <Proof> of (Prop/var :A)
        ;; z28-2-2-2-2 >>>>>
        (notE :x :a)
        ;;  => -- : <Proof> of (Prop/false)
        ;; z28-2-2-2-3 >>>>>
        pop
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/false))
      ;; z28-2-2-3 >>>>
      (set! af z)
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/false))
      ;; z28-2-2-4 >>>>
      (assume :b B)
        ;; z28-2-2-4-1 >>>>>
        :b
        ;;  => -- : <Proof> of (Prop/var :B)
        ;; z28-2-2-4-2 >>>>>
        (notE :y :b)
        ;;  => -- : <Proof> of (Prop/false)
        ;; z28-2-2-4-3 >>>>>
        pop
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/false))
      ;; z28-2-2-5 >>>>
      (set! bf z)
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/false))
      ;; z28-2-2-6 >>>>
      (orE :ab af bf)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z28-2-2-7 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/false))
    ;; z28-2-3 >>>
    (notI z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/|| (Prop/var :A) (Prop/var :B)))
    ;; z28-2-4 >>>
    (set! A46 z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/|| (Prop/var :A) (Prop/var :B)))
    ;; z28-2-5 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/~~ (Prop/|| (Prop/var :A) (Prop/var :B))))
  ;; z28-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/~~ (Prop/|| (Prop/var :A) (Prop/var :B)))))
;; z29 >
(proves? A46 [(~~ A) (~~ B)] (~~ (A || B)))
;;  => [] : <List>


[47]

;; z31 >
(assume :x ((~~ A) || (~~ B)))
  ;; z31-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/~~ (Prop/var :B)))
  ;; z31-2 >>
  (assume :na (~~ A))
    ;; z31-2-1 >>>
    :na
    ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
    ;; z31-2-2 >>>
    (assume :ab (A && B))
      ;; z31-2-2-1 >>>>
      :ab
      ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
      ;; z31-2-2-2 >>>>
      (andEL z)
      ;;  => -- : <Proof> of (Prop/var :A)
      ;; z31-2-2-3 >>>>
      (notE :na z)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z31-2-2-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/false))
    ;; z31-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/false)))
  ;; z31-3 >>
  (set! nab1r z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/false)))
  ;; z31-4 >>
  (assume :nb (~~ B))
    ;; z31-4-1 >>>
    :nb
    ;;  => -- : <Proof> of (Prop/~~ (Prop/var :B))
    ;; z31-4-2 >>>
    (assume :ab (A && B))
      ;; z31-4-2-1 >>>>
      :ab
      ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/var :B))
      ;; z31-4-2-2 >>>>
      (andER :ab)
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z31-4-2-3 >>>>
      (notE :nb z)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z31-4-2-4 >>>>
      (set! nab2 z)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z31-4-2-5 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/false))
    ;; z31-4-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/false)))
  ;; z31-5 >>
  (set! nab2r z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/false)))
  ;; z31-6 >>
  (orE :x nab1r nab2r)
  ;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/var :B)) (Prop/false))
  ;; z31-7 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B)))
  ;; z31-8 >>
  (set! A47 z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B)))
  ;; z31-9 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/~~ (Prop/var :B))) (Prop/~~ (Prop/&& (Prop/var :A) (Prop/var :B))))
;; z32 >
(proves? A47 [((~~ A) || (~~ B))] (~~ (A && B)))
;;  => [] : <List>


[48]

;; z34 >
(assume :x ((~~ A) && (~~ B)))
  ;; z34-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/&& (Prop/~~ (Prop/var :A)) (Prop/~~ (Prop/var :B)))
  ;; z34-2 >>
  (set! na (andEL :x))
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z34-3 >>
  (set! nb (andER :x))
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :B))
  ;; z34-4 >>
  (assume :ab (A || B))
    ;; z34-4-1 >>>
    :ab
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
    ;; z34-4-2 >>>
    (assume :a A)
      ;; z34-4-2-1 >>>>
      :a
      ;;  => -- : <Proof> of (Prop/var :A)
      ;; z34-4-2-2 >>>>
      (notE na :a)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z34-4-2-3 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/false))
    ;; z34-4-3 >>>
    (set! af z)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/false))
    ;; z34-4-4 >>>
    (assume :b B)
      ;; z34-4-4-1 >>>>
      :b
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z34-4-4-2 >>>>
      (notE nb :b)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z34-4-4-3 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/false))
    ;; z34-4-5 >>>
    (set! bf z)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/false))
    ;; z34-4-6 >>>
    (orE :ab af bf)
    ;;  => -- : <Proof> of (Prop/false)
    ;; z34-4-7 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/false))
  ;; z34-5 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/|| (Prop/var :A) (Prop/var :B)))
  ;; z34-6 >>
  (set! A48 z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/|| (Prop/var :A) (Prop/var :B)))
  ;; z34-7 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/~~ (Prop/var :A)) (Prop/~~ (Prop/var :B))) (Prop/~~ (Prop/|| (Prop/var :A) (Prop/var :B))))
;; z35 >
(proves? A48 [((~~ A) && (~~ B))] (~~ (A || B)))
;;  => [] : <List>


[49]

;; z37 >
(assume :x (~~ (A || B)))
  ;; z37-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/~~ (Prop/|| (Prop/var :A) (Prop/var :B)))
  ;; z37-2 >>
  (assume :a A)
    ;; z37-2-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z37-2-2 >>>
    (orI (A || B) :a)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
    ;; z37-2-3 >>>
    (notE :x z)
    ;;  => -- : <Proof> of (Prop/false)
    ;; z37-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/false))
  ;; z37-3 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z37-4 >>
  (set! na z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z37-5 >>
  (assume :b B)
    ;; z37-5-1 >>>
    :b
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z37-5-2 >>>
    (orI (A || B) :b)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
    ;; z37-5-3 >>>
    (notE :x z)
    ;;  => -- : <Proof> of (Prop/false)
    ;; z37-5-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/false))
  ;; z37-6 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :B))
  ;; z37-7 >>
  (set! nb z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :B))
  ;; z37-8 >>
  (andI na nb)
  ;;  => -- : <Proof> of (Prop/&& (Prop/~~ (Prop/var :A)) (Prop/~~ (Prop/var :B)))
  ;; z37-9 >>
  (set! A49 z)
  ;;  => -- : <Proof> of (Prop/&& (Prop/~~ (Prop/var :A)) (Prop/~~ (Prop/var :B)))
  ;; z37-10 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/|| (Prop/var :A) (Prop/var :B))) (Prop/&& (Prop/~~ (Prop/var :A)) (Prop/~~ (Prop/var :B))))
;; z38 >
(proves? A49 [(~~ (A || B))] ((~~ A) && (~~ B)))
;;  => [] : <List>


[50]

;; z39 >
(assume :x (A => B))
  ;; z39-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
  ;; z39-2 >>
  (assume :nb (~~ B))
    ;; z39-2-1 >>>
    :nb
    ;;  => -- : <Proof> of (Prop/~~ (Prop/var :B))
    ;; z39-2-2 >>>
    (assume :a A)
      ;; z39-2-2-1 >>>>
      :a
      ;;  => -- : <Proof> of (Prop/var :A)
      ;; z39-2-2-2 >>>>
      (impE :x :a)
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z39-2-2-3 >>>>
      (notE :nb z)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z39-2-2-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/false))
    ;; z39-2-3 >>>
    (notI z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
    ;; z39-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/~~ (Prop/var :A)))
  ;; z39-3 >>
  (set! A50 z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/~~ (Prop/var :A)))
  ;; z39-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/var :B)) (Prop/=> (Prop/~~ (Prop/var :B)) (Prop/~~ (Prop/var :A))))
;; z40 >
(proves? A50 [(A => B)] ((~~ B) => (~~ A)))
;;  => [] : <List>


[51]

;; z41 >
(assume :a A)
  ;; z41-1 >>
  :a
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z41-2 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :A))
;; z42 >
(set! A51 z)
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :A))
;; z43 >
(proves? A51 [] (A => A))
;;  => [] : <List>


[52]

;; z1 >
(assume :f :false)
  ;; z1-1 >>
  :f
  ;;  => -- : <Proof> of (Prop/false)
  ;; z1-2 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/false) (Prop/false))
;; z2 >
(notI z)
;;  => -- : <Proof> of (Prop/~~ (Prop/false))
;; z3 >
(set! A52 z)
;;  => -- : <Proof> of (Prop/~~ (Prop/false))
;; z4 >
(proves? A52 [] (~~ :false))
;;  => [] : <List>


[53]

;; z48 >
(assume :aab (A => (A => B)))
  ;; z48-1 >>
  :aab
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :A) (Prop/var :B)))
  ;; z48-2 >>
  (assume :a A)
    ;; z48-2-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z48-2-2 >>>
    (impE :aab :a)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
    ;; z48-2-3 >>>
    (impE z :a)
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z48-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
  ;; z48-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :A) (Prop/var :B))) (Prop/=> (Prop/var :A) (Prop/var :B)))
;; z49 >
(set! A53 z)
;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :A) (Prop/var :B))) (Prop/=> (Prop/var :A) (Prop/var :B)))
;; z50 >
(proves? A53 [] ((A => (A => B)) => (A => B)))
;;  => [] : <List>


[54]

;; z7 >
(assume :af (A && :false))
  ;; z7-1 >>
  :af
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/false))
  ;; z7-2 >>
  (andER :af)
  ;;  => -- : <Proof> of (Prop/false)
  ;; z7-3 >>
  (falseE (B && A) z)
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :B) (Prop/var :A))
  ;; z7-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/false)) (Prop/&& (Prop/var :B) (Prop/var :A)))
;; z8 >
(set! A54 z)
;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/false)) (Prop/&& (Prop/var :B) (Prop/var :A)))
;; z9 >
(proves? A54 [] ((A && :false) => (B && A)))
;;  => [] : <List>


[55]

;; z55 >
(assume :na (~~ A))
  ;; z55-1 >>
  :na
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z55-2 >>
  (assume :ba (B || A))
    ;; z55-2-1 >>>
    :ba
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :B) (Prop/var :A))
    ;; z55-2-2 >>>
    (assume :b B)
      ;; z55-2-2-1 >>>>
      :b
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z55-2-2-2 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :B))
    ;; z55-2-3 >>>
    (set! br z)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :B))
    ;; z55-2-4 >>>
    (assume :a A)
      ;; z55-2-4-1 >>>>
      :a
      ;;  => -- : <Proof> of (Prop/var :A)
      ;; z55-2-4-2 >>>>
      (notE :na :a)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z55-2-4-3 >>>>
      (falseE B z)
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z55-2-4-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
    ;; z55-2-5 >>>
    (set! ar z)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
    ;; z55-2-6 >>>
    (orE :ba br ar)
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z55-2-7 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :B) (Prop/var :A)) (Prop/var :B))
  ;; z55-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/=> (Prop/|| (Prop/var :B) (Prop/var :A)) (Prop/var :B)))
;; z56 >
(set! A55 z)
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/=> (Prop/|| (Prop/var :B) (Prop/var :A)) (Prop/var :B)))
;; z57 >
(proves? A55 [] ((~~ A) => ((B || A) => B)))
;;  => [] : <List>


[56]

;; z10 >
(assume :af (A || :false))
  ;; z10-1 >>
  :af
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/false))
  ;; z10-2 >>
  (assume :a A)
    ;; z10-2-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z10-2-2 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :A))
  ;; z10-3 >>
  (set! ar z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :A))
  ;; z10-4 >>
  (assume :f :false)
    ;; z10-4-1 >>>
    :f
    ;;  => -- : <Proof> of (Prop/false)
    ;; z10-4-2 >>>
    (falseE A :f)
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z10-4-3 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/false) (Prop/var :A))
  ;; z10-5 >>
  (set! fr z)
  ;;  => -- : <Proof> of (Prop/=> (Prop/false) (Prop/var :A))
  ;; z10-6 >>
  (orE :af ar fr)
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z10-7 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/false)) (Prop/var :A))
;; z11 >
(set! A56 z)
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/false)) (Prop/var :A))
;; z12 >
(proves? A56 [] ((A || :false) => A))
;;  => [] : <List>


[57]

;; z60 >
(assume :nana (A && (~~ A)))
  ;; z60-1 >>
  :nana
  ;;  => -- : <Proof> of (Prop/&& (Prop/var :A) (Prop/~~ (Prop/var :A)))
  ;; z60-2 >>
  (set! a (andEL :nana))
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z60-3 >>
  (set! na (andER :nana))
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z60-4 >>
  (notE na a)
  ;;  => -- : <Proof> of (Prop/false)
  ;; z60-5 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/&& (Prop/var :A) (Prop/~~ (Prop/var :A))) (Prop/false))
;; z61 >
(notI z)
;;  => -- : <Proof> of (Prop/~~ (Prop/&& (Prop/var :A) (Prop/~~ (Prop/var :A))))
;; z62 >
(set! A57 z)
;;  => -- : <Proof> of (Prop/~~ (Prop/&& (Prop/var :A) (Prop/~~ (Prop/var :A))))
;; z63 >
(proves? A57 [] (~~ (A && (~~ A))))
;;  => [] : <List>


[58]

;; z64 >
(assume :nnna (~~ (~~ (~~ A))))
  ;; z64-1 >>
  :nnna
  ;;  => -- : <Proof> of (Prop/~~ (Prop/~~ (Prop/~~ (Prop/var :A))))
  ;; z64-2 >>
  (assume :a A)
    ;; z64-2-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z64-2-2 >>>
    (assume :na (~~ A))
      ;; z64-2-2-1 >>>>
      :na
      ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
      ;; z64-2-2-2 >>>>
      (notE :na :a)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z64-2-2-3 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/false))
    ;; z64-2-3 >>>
    (notI z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/~~ (Prop/var :A)))
    ;; z64-2-4 >>>
    (notE :nnna z)
    ;;  => -- : <Proof> of (Prop/false)
    ;; z64-2-5 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/false))
  ;; z64-3 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z64-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/~~ (Prop/~~ (Prop/var :A)))) (Prop/~~ (Prop/var :A)))
;; z65 >
(set! A58 z)
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/~~ (Prop/~~ (Prop/var :A)))) (Prop/~~ (Prop/var :A)))
;; z66 >
(proves? A58 [] ((~~ (~~ (~~ A))) => (~~ A)))
;;  => [] : <List>


[59]

;; z67 >
(assume :nab ((~~ A) || B))
  ;; z67-1 >>
  :nab
  ;;  => -- : <Proof> of (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))
  ;; z67-2 >>
  (assume :a A)
    ;; z67-2-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z67-2-2 >>>
    (assume :na (~~ A))
      ;; z67-2-2-1 >>>>
      :na
      ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
      ;; z67-2-2-2 >>>>
      (notE :na :a)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z67-2-2-3 >>>>
      (falseE B z)
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z67-2-2-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/var :B))
    ;; z67-2-3 >>>
    (set! nar z)
    ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/var :B))
    ;; z67-2-4 >>>
    (assume :b B)
      ;; z67-2-4-1 >>>>
      :b
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z67-2-4-2 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :B))
    ;; z67-2-5 >>>
    (set! br z)
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :B))
    ;; z67-2-6 >>>
    (orE :nab nar br)
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z67-2-7 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
  ;; z67-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B)) (Prop/=> (Prop/var :A) (Prop/var :B)))
;; z68 >
(set! A59 z)
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B)) (Prop/=> (Prop/var :A) (Prop/var :B)))
;; z69 >
(proves? A59 [] (((~~ A) || B) => (A => B)))
;;  => [] : <List>


[60]

;; z1 >
(assume :a A)
  ;; z1-1 >>
  :a
  ;;  => -- : <Proof> of (Prop/var :A)
  ;; z1-2 >>
  (assume :b B)
    ;; z1-2-1 >>>
    :b
    ;;  => -- : <Proof> of (Prop/var :B)
    ;; z1-2-2 >>>
    (assume :nna (~~ ((~~ A) || B)))
      ;; z1-2-2-1 >>>>
      :nna
      ;;  => -- : <Proof> of (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B)))
      ;; z1-2-2-2 >>>>
      (orI ((~~ A) || B) :b)
      ;;  => -- : <Proof> of (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))
      ;; z1-2-2-3 >>>>
      (notE :nna z)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z1-2-2-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))) (Prop/false))
    ;; z1-2-3 >>>
    (notI z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))))
    ;; z1-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/~~ (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B)))))
  ;; z1-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/~~ (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))))))
;; z2 >
(set! A60 z)
;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/=> (Prop/var :B) (Prop/~~ (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))))))
;; z3 >
(proves? A60 [] (A => (B => (~~ (~~ ((~~ A) || B))))))
;;  => [] : <List>


[61]

;; z2 >
(assume :ab (A || B))
  ;; z2-1 >>
  :ab
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
  ;; z2-2 >>
  (assume :nna (~~ ((~~ A) => B)))
    ;; z2-2-1 >>>
    :nna
    ;;  => -- : <Proof> of (Prop/~~ (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/var :B)))
    ;; z2-2-2 >>>
    (assume :na (~~ A))
      ;; z2-2-2-1 >>>>
      :na
      ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
      ;; z2-2-2-2 >>>>
      (assume :a A)
        ;; z2-2-2-2-1 >>>>>
        :a
        ;;  => -- : <Proof> of (Prop/var :A)
        ;; z2-2-2-2-2 >>>>>
        (notE :na :a)
        ;;  => -- : <Proof> of (Prop/false)
        ;; z2-2-2-2-3 >>>>>
        (falseE B z)
        ;;  => -- : <Proof> of (Prop/var :B)
        ;; z2-2-2-2-4 >>>>>
        pop
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
      ;; z2-2-2-3 >>>>
      (set! ar z)
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
      ;; z2-2-2-4 >>>>
      (assume :b B)
        ;; z2-2-2-4-1 >>>>>
        :b
        ;;  => -- : <Proof> of (Prop/var :B)
        ;; z2-2-2-4-2 >>>>>
        pop
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :B))
      ;; z2-2-2-5 >>>>
      (set! br z)
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :B))
      ;; z2-2-2-6 >>>>
      (orE :ab ar br)
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z2-2-2-7 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/var :B))
    ;; z2-2-3 >>>
    (notE :nna z)
    ;;  => -- : <Proof> of (Prop/false)
    ;; z2-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/var :B))) (Prop/false))
  ;; z2-3 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/~~ (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/var :B))))
  ;; z2-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/~~ (Prop/~~ (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/var :B)))))
;; z3 >
(set! A61 z)
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/~~ (Prop/~~ (Prop/=> (Prop/~~ (Prop/var :A)) (Prop/var :B)))))
;; z4 >
(proves? A61 [] ((A || B) => (~~ (~~ ((~~ A) => B)))))
;;  => [] : <List>


[62]

;; z1 >
(assume :nna (~~ (A || (~~ A))))
  ;; z1-1 >>
  :nna
  ;;  => -- : <Proof> of (Prop/~~ (Prop/|| (Prop/var :A) (Prop/~~ (Prop/var :A))))
  ;; z1-2 >>
  (assume :a A)
    ;; z1-2-1 >>>
    :a
    ;;  => -- : <Proof> of (Prop/var :A)
    ;; z1-2-2 >>>
    (orI (A || (~~ A)) z)
    ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/~~ (Prop/var :A)))
    ;; z1-2-3 >>>
    (notE :nna z)
    ;;  => -- : <Proof> of (Prop/false)
    ;; z1-2-4 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/false))
  ;; z1-3 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
  ;; z1-4 >>
  (orI (A || (~~ A)) z)
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/~~ (Prop/var :A)))
  ;; z1-5 >>
  (notE :nna z)
  ;;  => -- : <Proof> of (Prop/false)
  ;; z1-6 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/|| (Prop/var :A) (Prop/~~ (Prop/var :A)))) (Prop/false))
;; z2 >
(notI z)
;;  => -- : <Proof> of (Prop/~~ (Prop/~~ (Prop/|| (Prop/var :A) (Prop/~~ (Prop/var :A)))))
;; z3 >
(set! A62 z)
;;  => -- : <Proof> of (Prop/~~ (Prop/~~ (Prop/|| (Prop/var :A) (Prop/~~ (Prop/var :A)))))
;; z4 >
(proves? A62 [] (~~ (~~ (A || (~~ A)))))
;;  => [] : <List>


[63]

;; z1 >
(assume :ab (A => B))
  ;; z1-1 >>
  :ab
  ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :B))
  ;; z1-2 >>
  (assume :nna (~~ ((~~ A) || B)))
    ;; z1-2-1 >>>
    :nna
    ;;  => -- : <Proof> of (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B)))
    ;; z1-2-2 >>>
    (assume :a A)
      ;; z1-2-2-1 >>>>
      :a
      ;;  => -- : <Proof> of (Prop/var :A)
      ;; z1-2-2-2 >>>>
      (impE :ab :a)
      ;;  => -- : <Proof> of (Prop/var :B)
      ;; z1-2-2-3 >>>>
      (orI ((~~ A) || B) z)
      ;;  => -- : <Proof> of (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))
      ;; z1-2-2-4 >>>>
      (notE :nna z)
      ;;  => -- : <Proof> of (Prop/false)
      ;; z1-2-2-5 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/false))
    ;; z1-2-3 >>>
    (notI z)
    ;;  => -- : <Proof> of (Prop/~~ (Prop/var :A))
    ;; z1-2-4 >>>
    (orI ((~~ A) || B) z)
    ;;  => -- : <Proof> of (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))
    ;; z1-2-5 >>>
    (notE :nna z)
    ;;  => -- : <Proof> of (Prop/false)
    ;; z1-2-6 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))) (Prop/false))
  ;; z1-3 >>
  (notI z)
  ;;  => -- : <Proof> of (Prop/~~ (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B))))
  ;; z1-4 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/var :B)) (Prop/~~ (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B)))))
;; z2 >
(set! A63 z)
;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/var :B)) (Prop/~~ (Prop/~~ (Prop/|| (Prop/~~ (Prop/var :A)) (Prop/var :B)))))
;; z3 >
(proves? A63 [] ((A => B) => (~~ (~~ ((~~ A) || B)))))
;;  => [] : <List>


[64]

;; z1 >
(assume :x (A || B))
  ;; z1-1 >>
  :x
  ;;  => -- : <Proof> of (Prop/|| (Prop/var :A) (Prop/var :B))
  ;; z1-2 >>
  (assume :y (A => C))
    ;; z1-2-1 >>>
    :y
    ;;  => -- : <Proof> of (Prop/=> (Prop/var :A) (Prop/var :C))
    ;; z1-2-2 >>>
    (assume :z (B => C))
      ;; z1-2-2-1 >>>>
      :z
      ;;  => -- : <Proof> of (Prop/=> (Prop/var :B) (Prop/var :C))
      ;; z1-2-2-2 >>>>
      (orE :x :y :z)
      ;;  => -- : <Proof> of (Prop/var :C)
      ;; z1-2-2-3 >>>>
      (set! A64 z)
      ;;  => -- : <Proof> of (Prop/var :C)
      ;; z1-2-2-4 >>>>
      pop
    ;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :B) (Prop/var :C)) (Prop/var :C))
    ;; z1-2-3 >>>
    pop
  ;;  => -- : <Proof> of (Prop/=> (Prop/=> (Prop/var :A) (Prop/var :C)) (Prop/=> (Prop/=> (Prop/var :B) (Prop/var :C)) (Prop/var :C)))
  ;; z1-3 >>
  pop
;;  => -- : <Proof> of (Prop/=> (Prop/|| (Prop/var :A) (Prop/var :B)) (Prop/=> (Prop/=> (Prop/var :A) (Prop/var :C)) (Prop/=> (Prop/=> (Prop/var :B) (Prop/var :C)) (Prop/var :C))))
;; z2 >
(proves? A64 [(A || B) (A => C) (B => C)] C)
;;  => [] : <List>