[20]
; ...
(proves? A20 [] (A => A))

[21]
(assume :x (A => B))
(assume :y A)
; ...
(proves? A21 [(A => B) A] B)

[22]
(assume :x (A => (B => C)))
; ...
(proves? A22 [(A => (B => C))] (B => (A => C)))

[23]
(assume :x A)
; ...
(proves? A23 [A] (A && A))

[24]
(assume :x (A && A))
; ...
(proves? A24 [(A && A)] A)

[25]
(assume :x A)
; ...
(proves? A25 [A] (A || A))

[26]
(assume :x (A || A))
; ...
(proves? A26 [(A || A)] A)

[27]
(assume :x A)
(assume :y B)
; ...
(proves? A27 [A B] A)

[28]
(assume :x (A && B))
; ...
(proves? A28 [(A && B)] (B && A))

[29]
(assume :x (A || B))
; ...
(proves? A29 [(A || B)] (B || A))

[30]
(assume :x ((A && B) && C))
; ...
(proves? A30 [((A && B) && C)] (A && (B && C)))

[31]
(assume :x ((A || B) || C))
; ...
(proves? A31 [((A || B) || C)] (A || (B || C)))

[32]
(assume :x (A && (B || C)))
; ...
(proves? A32 [(A && (B || C))] ((A && B) || (A && C)))

[33]
(assume :x ((A && B) || (A && C)))
; ...
(proves? A33 [((A && B) || (A && C))] (A && (B || C)))

[34]
(assume :x ((A && B) => C))
; ...
(proves? A34 [((A && B) => C)] (A => (B => C)))

[35]
(assume :x (A => (B => C)))
; ...
(proves? A35 [(A => (B => C))] ((A && B) => C))

[36]
(assume :x B)
; ...
(proves? A36 [B] (A => B))

[37]
(assume :x A)
(assume :y (~~ B))
; ...
(proves? A37 [A (~~ B)] (~~ (A => B)))

[38]
(assume :x (~~ A))
(assume :y (~~ B))
; ...
(proves? A38 [(~~ A) (~~ B)] (A => B))

[39]
(assume :x A)
; ...
(proves? A39 [A] (~~ (~~ A)))

[40]
(assume :x (~~ A))
; ...
(proves? A40 [(~~ A)] (~~ A))

[41]
(assume :x A)
(assume :y B)
; ...
(proves? A41 [A B] (A && B))

[42]
(assume :x (~~ B))
; ...
(proves? A42 [(~~ B)] (~~ (A && B)))

[43]
(assume :x (~~ A))
(assume :y B)
; ...
(proves? A43 [(~~ A) B] (~~ (A && B)))

[44]
(assume :x A)
; ...
(proves? A44 [A] (A || B))

[45]
(assume :x B)
; ...
(proves? A45 [B] (A || B))

[46]
(assume :x (~~ A))
(assume :y (~~ B))
; ...
(proves? A46 [(~~ A) (~~ B)] (~~ (A || B)))

[47]
(assume :x ((~~ A) || (~~ B)))
; ...
(proves? A47 [((~~ A) || (~~ B))] (~~ (A && B)))

[48]
(assume :x ((~~ A) && (~~ B)))
; ...
(proves? A48 [((~~ A) && (~~ B))] (~~ (A || B)))

[49]
(assume :x (~~ (A || B)))
; ...
(proves? A49 [(~~ (A || B))] ((~~ A) && (~~ B)))

[50]
(assume :x (A => B))
; ...
(proves? A50 [(A => B)] ((~~ B) => (~~ A)))

[51]
; ...
(proves? A51 [] (A => A))

[52]
; ...
(proves? A52 [] (~~ :false))

[53]
; ...
(proves? A53 [] ((A => (A => B)) => (A => B)))

[54]
; ...
(proves? A54 [] ((A && :false) => (B && A)))

[55]
; ...
(proves? A55 [] ((~~ A) => ((B || A) => B)))

[56]
; ...
(proves? A56 [] ((A || :false) => A))

[57]
; ...
(proves? A57 [] (~~ (A && (~~ A))))

[58]
; ...
(proves? A58 [] ((~~ (~~ (~~ A))) => (~~ A)))

[59]
; ...
(proves? A59 [] (((~~ A) || B) => (A => B)))

[60]
; ...
(proves? A60 [] (A => (B => (~~ (~~ ((~~ A) || B))))))

[61]
; ...
(proves? A61 [] ((A || B) => (~~ (~~ ((~~ A) => B)))))

[62]
; ...
(proves? A62 [] (~~ (~~ (A || (~~ A)))))

[63]
; ...
(proves? A63 [] ((A => B) => (~~ (~~ ((~~ A) || B)))))

[64]
(assume :x (A || B))
(assume :y (A => C))
(assume :z (B => C))
; ...
(proves? A64 [(A || B) (A => C) (B => C)] C)