page title
 MAIN   PRODUCTS   BLOG   AUTOMATED THEOREM FINDING   METAPROGRAMMING  



PRODUCTS
========

  • Instprog Default Newlisp Library
    --------------------------------


    Console after loading of library


    The collection of various useful functions and macros:

    - debuging support,
    - higher order functions,
    - conversion from macros to functions and vice versa;
      conversion from primitives to macros and functions,
    - protection against potential funcall problems,
    - gensym and related macros (genlocal, genlet, genfor ... ),
    - multiple loops like (dotimes-multi((i j k) 100) ...),
    - two macro systems,
    - the most-probable-cond and least-probable-cond,
    - support for printing of lists, lines, titles, variables...,
    - propositional logic operators and predicates,
    - factorials, double factorials, Fibonacci and Collatz's numbers,
      sum and product of digits, recursive sum and product of digits

    and many other functions and macros. For exact size of the library, look at the column on the right side of this www page. Although not all functions and macros are logically related, all are in the same file, to simplify loading. The library is in constant development and performs tests each time it is loaded. Documentation is in the source code. Free for noncommercial use.



  • 1581 propositional tautologies
    ------------------------------
    1. 1
2. (¬ 0)
3. (¬ (¬ 1))
4. (1 & 1)
5. (1 ˅ a)
6. (a ˅ 1)
7. (0 -> a)
8. (a -> 1)
9. (a -> a)
10. (a <-> a)
11. (¬ (0 & a))
12. (¬ (a & 0))
13. (¬ (0 ˅ 0))
14. (¬ (1 -> 0))
15. (¬ (1 <-> 0))
16. (¬ (0 <-> 1))
17. (a ˅ (¬ a))
18. ((¬ a) ˅ a)
19. ((¬ 1) -> a)
20. (0 <-> (¬ 1))
21. ((¬ 1) <-> 0)
22. (¬ (a & (¬ 1)))
23. (¬ (a & (¬ a)))
24. (¬ ((¬ 1) & a))
25. (¬ ((¬ a) & a))
26. (¬ (0 ˅ (¬ 1)))
27. (¬ ((¬ 1) ˅ 0))
28. (¬ (1 -> (¬ 1)))
29. (¬ (a <-> (¬ a)))
30. (¬ ((¬ a) <-> a))
31. (a ˅ (a -> b))
32. (a ˅ (0 <-> a))
33. (a ˅ (a <-> 0))
34. ((a -> b) ˅ a)
35. ((0 <-> a) ˅ a)
36. ((a <-> 0) ˅ a)
37. (a -> (¬ (¬ a)))
38. (a -> (1 & a))
39. (a -> (a & 1))
40. (a -> (a & a))
41. (a -> (a ˅ b))
42. (a -> (b ˅ a))
43. (a -> (b -> a))
44. (a -> (1 <-> a))
45. (a -> (a <-> 1))
46. ((¬ (¬ a)) -> a)
47. ((0 & a) -> b)
48. ((a & 0) -> b)
49. ((a & b) -> a)
50. ((a & b) -> b)
51. ((0 ˅ 0) -> a)
52. ((0 ˅ a) -> a)
53. ((a ˅ 0) -> a)
54. ((a ˅ a) -> a)
55. ((1 -> 0) -> a)
56. ((1 -> a) -> a)
57. ((1 <-> 0) -> a)
58. ((1 <-> a) -> a)
59. ((0 <-> 1) -> a)
60. ((a <-> 1) -> a)
61. (0 <-> (0 & a))
62. (0 <-> (a & 0))
63. (a <-> (¬ (¬ a)))
64. (a <-> (1 & a))
65. (a <-> (a & 1))
66. (a <-> (a & a))
67. (a <-> (0 ˅ a))
68. (a <-> (a ˅ 0))
69. (a <-> (a ˅ a))
70. (a <-> (1 -> a))
71. (a <-> (1 <-> a))
72. (a <-> (a <-> 1))
73. ((¬ (¬ a)) <-> a)
74. ((1 & a) <-> a)
75. ((0 & a) <-> 0)
76. ((a & 1) <-> a)
77. ((a & 0) <-> 0)
78. ((a & a) <-> a)
79. ((0 ˅ a) <-> a)
80. ((a ˅ 0) <-> a)
81. ((a ˅ a) <-> a)
82. ((1 -> a) <-> a)
83. ((1 <-> a) <-> a)
84. ((a <-> 1) <-> a)
85. (¬ (a & (0 & b)))
86. (¬ (a & (b & 0)))
87. (¬ (a & (0 ˅ 0)))
88. (¬ (a & (1 -> 0)))
89. (¬ (a & (a -> 0)))
90. (¬ (a & (1 <-> 0)))
91. (¬ (a & (0 <-> 1)))
92. (¬ (a & (0 <-> a)))
93. (¬ (a & (a <-> 0)))
94. (¬ ((0 & a) & b))
95. (¬ ((a & 0) & b))
96. (¬ ((0 ˅ 0) & a))
97. (¬ ((1 -> 0) & a))
98. (¬ ((a -> 0) & a))
99. (¬ ((1 <-> 0) & a))
100. (¬ ((0 <-> 1) & a))
101. (¬ ((0 <-> a) & a))
102. (¬ ((a <-> 0) & a))
103. (¬ (0 ˅ (0 & a)))
104. (¬ (0 ˅ (a & 0)))
105. (¬ (0 ˅ (0 ˅ 0)))
106. (¬ (0 ˅ (1 -> 0)))
107. (¬ (0 ˅ (1 <-> 0)))
108. (¬ (0 ˅ (0 <-> 1)))
109. (¬ ((¬ 1) ˅ (¬ 1)))
110. (¬ ((0 & a) ˅ 0))
111. (¬ ((a & 0) ˅ 0))
112. (¬ ((0 ˅ 0) ˅ 0))
113. (¬ ((1 -> 0) ˅ 0))
114. (¬ ((1 <-> 0) ˅ 0))
115. (¬ ((0 <-> 1) ˅ 0))
116. (¬ (1 -> (0 & a)))
117. (¬ (1 -> (a & 0)))
118. (¬ (1 -> (0 ˅ 0)))
119. (¬ (1 -> (1 -> 0)))
120. (¬ (1 -> (1 <-> 0)))
121. (¬ (1 -> (0 <-> 1)))
122. (¬ (1 <-> (0 & a)))
123. (¬ (1 <-> (a & 0)))
124. (¬ (1 <-> (0 ˅ 0)))
125. (¬ (a <-> (a -> 0)))
126. (¬ (a <-> (0 <-> a)))
127. (¬ (a <-> (a <-> 0)))
128. (¬ ((0 & a) <-> 1))
129. (¬ ((a & 0) <-> 1))
130. (¬ ((0 ˅ 0) <-> 1))
131. (¬ ((a -> 0) <-> a))
132. (¬ ((0 <-> a) <-> a))
133. (¬ ((a <-> 0) <-> a))
134. (a ˅ (¬ (¬ (¬ a))))
135. (a ˅ (¬ (a & b)))
136. (a ˅ (¬ (b & a)))
137. (a ˅ (¬ (0 ˅ a)))
138. (a ˅ (¬ (a ˅ 0)))
139. (a ˅ (¬ (a ˅ a)))
140. (a ˅ (¬ (1 -> a)))
141. (a ˅ (¬ (1 <-> a)))
142. (a ˅ (¬ (a <-> 1)))
143. (a ˅ (1 & (¬ a)))
144. (a ˅ ((¬ a) & 1))
145. (a ˅ (b ˅ (¬ a)))
146. (a ˅ ((¬ a) ˅ b))
147. (a ˅ (b -> (¬ a)))
148. (a ˅ (1 <-> (¬ a)))
149. (a ˅ (a <-> (¬ 1)))
150. (a ˅ ((¬ 1) <-> a))
151. (a ˅ ((¬ a) <-> 1))
152. ((¬ a) ˅ (1 & a))
153. ((¬ a) ˅ (a & 1))
154. ((¬ a) ˅ (a & a))
155. ((¬ a) ˅ (a ˅ b))
156. ((¬ a) ˅ (b ˅ a))
157. ((¬ a) ˅ (b -> a))
158. ((¬ a) ˅ (1 <-> a))
159. ((¬ a) ˅ (a <-> 1))
160. ((1 & a) ˅ (¬ a))
161. ((a & 1) ˅ (¬ a))
162. ((a & a) ˅ (¬ a))
163. ((a ˅ b) ˅ (¬ a))
164. ((a ˅ b) ˅ (¬ b))
165. ((a -> b) ˅ (¬ b))
166. ((1 <-> a) ˅ (¬ a))
167. ((a <-> 1) ˅ (¬ a))
168. ((¬ (¬ (¬ a))) ˅ a)
169. ((¬ (a & b)) ˅ a)
170. ((¬ (a & b)) ˅ b)
171. ((¬ (0 ˅ a)) ˅ a)
172. ((¬ (a ˅ 0)) ˅ a)
173. ((¬ (a ˅ a)) ˅ a)
174. ((¬ (1 -> a)) ˅ a)
175. ((¬ (1 <-> a)) ˅ a)
176. ((¬ (a <-> 1)) ˅ a)
177. ((1 & (¬ a)) ˅ a)
178. (((¬ a) & 1) ˅ a)
179. ((a ˅ (¬ b)) ˅ b)
180. (((¬ a) ˅ b) ˅ a)
181. ((a -> (¬ b)) ˅ b)
182. ((1 <-> (¬ a)) ˅ a)
183. ((a <-> (¬ 1)) ˅ a)
184. (((¬ 1) <-> a) ˅ a)
185. (((¬ a) <-> 1) ˅ a)
186. (a -> (¬ (a -> 0)))
187. (a -> (¬ (0 <-> a)))
188. (a -> (¬ (a <-> 0)))
189. (a -> ((¬ a) -> b))
190. (a -> (0 <-> (¬ a)))
191. (a -> ((¬ a) <-> 0))
192. ((¬ a) -> (a -> b))
193. ((¬ a) -> (0 <-> a))
194. ((¬ a) -> (a <-> 0))
195. ((a -> 0) -> (¬ a))
196. ((0 <-> a) -> (¬ a))
197. ((a <-> 0) -> (¬ a))
198. ((¬ (a -> b)) -> a)
199. ((¬ (0 <-> a)) -> a)
200. ((¬ (a <-> 0)) -> a)
201. ((a & (¬ 1)) -> b)
202. ((a & (¬ a)) -> b)
203. (((¬ 1) & a) -> b)
204. (((¬ a) & a) -> b)
205. ((0 ˅ (¬ 1)) -> a)
206. ((a ˅ (¬ 1)) -> a)
207. (((¬ 1) ˅ 0) -> a)
208. (((¬ 1) ˅ a) -> a)
209. ((1 -> (¬ 1)) -> a)
210. (((¬ a) -> 0) -> a)
211. (((¬ a) -> a) -> a)
212. ((0 <-> (¬ a)) -> a)
213. ((a <-> (¬ a)) -> b)
214. (((¬ a) <-> 0) -> a)
215. (((¬ a) <-> a) -> b)
216. (0 <-> (a & (¬ 1)))
217. (0 <-> (a & (¬ a)))
218. (0 <-> ((¬ 1) & a))
219. (0 <-> ((¬ a) & a))
220. (0 <-> (1 -> (¬ 1)))
221. (0 <-> (a <-> (¬ a)))
222. (0 <-> ((¬ a) <-> a))
223. (a <-> (¬ (a -> 0)))
224. (a <-> (¬ (0 <-> a)))
225. (a <-> (¬ (a <-> 0)))
226. (a <-> (a ˅ (¬ 1)))
227. (a <-> ((¬ 1) ˅ a))
228. (a <-> ((¬ a) -> 0))
229. (a <-> ((¬ a) -> a))
230. (a <-> (0 <-> (¬ a)))
231. (a <-> ((¬ a) <-> 0))
232. ((¬ 1) <-> (0 & a))
233. ((¬ 1) <-> (a & 0))
234. ((¬ 1) <-> (0 ˅ 0))
235. ((¬ a) <-> (a -> 0))
236. ((¬ a) <-> (0 <-> a))
237. ((¬ a) <-> (a <-> 0))
238. ((0 & a) <-> (¬ 1))
239. ((a & 0) <-> (¬ 1))
240. ((0 ˅ 0) <-> (¬ 1))
241. ((a -> 0) <-> (¬ a))
242. ((0 <-> a) <-> (¬ a))
243. ((a <-> 0) <-> (¬ a))
244. ((¬ (a -> 0)) <-> a)
245. ((¬ (0 <-> a)) <-> a)
246. ((¬ (a <-> 0)) <-> a)
247. ((a & (¬ 1)) <-> 0)
248. ((a & (¬ a)) <-> 0)
249. (((¬ 1) & a) <-> 0)
250. (((¬ a) & a) <-> 0)
251. ((a ˅ (¬ 1)) <-> a)
252. (((¬ 1) ˅ a) <-> a)
253. ((1 -> (¬ 1)) <-> 0)
254. (((¬ a) -> 0) <-> a)
255. (((¬ a) -> a) <-> a)
256. ((0 <-> (¬ a)) <-> a)
257. ((a <-> (¬ a)) <-> 0)
258. (((¬ a) <-> 0) <-> a)
259. (((¬ a) <-> a) <-> 0)
260. (¬ (a & (¬ (¬ (¬ a)))))
261. (¬ (a & (¬ (1 & a))))
262. (¬ (a & (¬ (a & 1))))
263. (¬ (a & (¬ (a & a))))
264. (¬ (a & (¬ (a ˅ b))))
265. (¬ (a & (¬ (b ˅ a))))
266. (¬ (a & (¬ (b -> a))))
267. (¬ (a & (¬ (1 <-> a))))
268. (¬ (a & (¬ (a <-> 1))))
269. (¬ (a & (b & (¬ 1))))
270. (¬ (a & (b & (¬ a))))
271. (¬ (a & (b & (¬ b))))
272. (¬ (a & ((¬ 1) & b)))
273. (¬ (a & ((¬ a) & b)))
274. (¬ (a & ((¬ b) & b)))
275. (¬ (a & (0 ˅ (¬ 1))))
276. (¬ (a & (0 ˅ (¬ a))))
277. (¬ (a & ((¬ 1) ˅ 0)))
278. (¬ (a & ((¬ a) ˅ 0)))
279. (¬ (a & (1 -> (¬ 1))))
280. (¬ (a & (1 -> (¬ a))))
281. (¬ (a & (a -> (¬ 1))))
282. (¬ (a & (a -> (¬ a))))
283. (¬ (a & (1 <-> (¬ a))))
284. (¬ (a & (a <-> (¬ 1))))
285. (¬ (a & (b <-> (¬ b))))
286. (¬ (a & ((¬ 1) <-> a)))
287. (¬ (a & ((¬ a) <-> 1)))
288. (¬ (a & ((¬ b) <-> b)))
289. (¬ ((¬ a) & (a & b)))
290. (¬ ((¬ a) & (b & a)))
291. (¬ ((¬ a) & (0 ˅ a)))
292. (¬ ((¬ a) & (a ˅ 0)))
293. (¬ ((¬ a) & (a ˅ a)))
294. (¬ ((¬ a) & (1 -> a)))
295. (¬ ((¬ a) & (1 <-> a)))
296. (¬ ((¬ a) & (a <-> 1)))
297. (¬ ((a & b) & (¬ a)))
298. (¬ ((a & b) & (¬ b)))
299. (¬ ((0 ˅ a) & (¬ a)))
300. (¬ ((a ˅ 0) & (¬ a)))
301. (¬ ((a ˅ a) & (¬ a)))
302. (¬ ((1 -> a) & (¬ a)))
303. (¬ ((1 <-> a) & (¬ a)))
304. (¬ ((a <-> 1) & (¬ a)))
305. (¬ ((¬ (¬ (¬ a))) & a))
306. (¬ ((¬ (1 & a)) & a))
307. (¬ ((¬ (a & 1)) & a))
308. (¬ ((¬ (a & a)) & a))
309. (¬ ((¬ (a ˅ b)) & a))
310. (¬ ((¬ (a ˅ b)) & b))
311. (¬ ((¬ (a -> b)) & b))
312. (¬ ((¬ (1 <-> a)) & a))
313. (¬ ((¬ (a <-> 1)) & a))
314. (¬ ((a & (¬ 1)) & b))
315. (¬ ((a & (¬ a)) & b))
316. (¬ ((a & (¬ b)) & b))
317. (¬ (((¬ 1) & a) & b))
318. (¬ (((¬ a) & a) & b))
319. (¬ (((¬ a) & b) & a))
320. (¬ ((0 ˅ (¬ 1)) & a))
321. (¬ ((0 ˅ (¬ a)) & a))
322. (¬ (((¬ 1) ˅ 0) & a))
323. (¬ (((¬ a) ˅ 0) & a))
324. (¬ ((1 -> (¬ 1)) & a))
325. (¬ ((1 -> (¬ a)) & a))
326. (¬ ((a -> (¬ 1)) & a))
327. (¬ ((a -> (¬ a)) & a))
328. (¬ ((1 <-> (¬ a)) & a))
329. (¬ ((a <-> (¬ 1)) & a))
330. (¬ ((a <-> (¬ a)) & b))
331. (¬ (((¬ 1) <-> a) & a))
332. (¬ (((¬ a) <-> 1) & a))
333. (¬ (((¬ a) <-> a) & b))
334. (¬ (0 ˅ (a & (¬ 1))))
335. (¬ (0 ˅ (a & (¬ a))))
336. (¬ (0 ˅ ((¬ 1) & a)))
337. (¬ (0 ˅ ((¬ a) & a)))
338. (¬ (0 ˅ (0 ˅ (¬ 1))))
339. (¬ (0 ˅ ((¬ 1) ˅ 0)))
340. (¬ (0 ˅ (1 -> (¬ 1))))
341. (¬ (0 ˅ (a <-> (¬ a))))
342. (¬ (0 ˅ ((¬ a) <-> a)))
343. (¬ ((¬ 1) ˅ (0 & a)))
344. (¬ ((¬ 1) ˅ (a & 0)))
345. (¬ ((¬ 1) ˅ (0 ˅ 0)))
346. (¬ ((¬ 1) ˅ (1 -> 0)))
347. (¬ ((¬ 1) ˅ (1 <-> 0)))
348. (¬ ((¬ 1) ˅ (0 <-> 1)))
349. (¬ ((0 & a) ˅ (¬ 1)))
350. (¬ ((a & 0) ˅ (¬ 1)))
351. (¬ ((0 ˅ 0) ˅ (¬ 1)))
352. (¬ ((1 -> 0) ˅ (¬ 1)))
353. (¬ ((1 <-> 0) ˅ (¬ 1)))
354. (¬ ((0 <-> 1) ˅ (¬ 1)))
355. (¬ ((a & (¬ 1)) ˅ 0))
356. (¬ ((a & (¬ a)) ˅ 0))
357. (¬ (((¬ 1) & a) ˅ 0))
358. (¬ (((¬ a) & a) ˅ 0))
359. (¬ ((0 ˅ (¬ 1)) ˅ 0))
360. (¬ (((¬ 1) ˅ 0) ˅ 0))
361. (¬ ((1 -> (¬ 1)) ˅ 0))
362. (¬ ((a <-> (¬ a)) ˅ 0))
363. (¬ (((¬ a) <-> a) ˅ 0))
364. (¬ (1 -> (a & (¬ 1))))
365. (¬ (1 -> (a & (¬ a))))
366. (¬ (1 -> ((¬ 1) & a)))
367. (¬ (1 -> ((¬ a) & a)))
368. (¬ (1 -> (0 ˅ (¬ 1))))
369. (¬ (1 -> ((¬ 1) ˅ 0)))
370. (¬ (1 -> (1 -> (¬ 1))))
371. (¬ (1 -> (a <-> (¬ a))))
372. (¬ (1 -> ((¬ a) <-> a)))
373. (¬ (1 <-> (a & (¬ 1))))
374. (¬ (1 <-> (a & (¬ a))))
375. (¬ (1 <-> ((¬ 1) & a)))
376. (¬ (1 <-> ((¬ a) & a)))
377. (¬ (1 <-> (a <-> (¬ a))))
378. (¬ (1 <-> ((¬ a) <-> a)))
379. (¬ (a <-> (¬ (¬ (¬ a)))))
380. (¬ (a <-> (¬ (1 & a))))
381. (¬ (a <-> (¬ (a & 1))))
382. (¬ (a <-> (¬ (a & a))))
383. (¬ (a <-> (¬ (0 ˅ a))))
384. (¬ (a <-> (¬ (a ˅ 0))))
385. (¬ (a <-> (¬ (a ˅ a))))
386. (¬ (a <-> (¬ (1 -> a))))
387. (¬ (a <-> (¬ (1 <-> a))))
388. (¬ (a <-> (¬ (a <-> 1))))
389. (¬ (a <-> (1 & (¬ a))))
390. (¬ (a <-> ((¬ a) & 1)))
391. (¬ (a <-> (0 ˅ (¬ a))))
392. (¬ (a <-> ((¬ a) ˅ 0)))
393. (¬ (a <-> (1 -> (¬ a))))
394. (¬ (a <-> (a -> (¬ 1))))
395. (¬ (a <-> (a -> (¬ a))))
396. (¬ (a <-> (1 <-> (¬ a))))
397. (¬ (a <-> (a <-> (¬ 1))))
398. (¬ (a <-> ((¬ 1) <-> a)))
399. (¬ (a <-> ((¬ a) <-> 1)))
400. (¬ ((¬ a) <-> (1 & a)))
401. (¬ ((¬ a) <-> (a & 1)))
402. (¬ ((¬ a) <-> (a & a)))
403. (¬ ((¬ a) <-> (0 ˅ a)))
404. (¬ ((¬ a) <-> (a ˅ 0)))
405. (¬ ((¬ a) <-> (a ˅ a)))
406. (¬ ((¬ a) <-> (1 -> a)))
407. (¬ ((¬ a) <-> (1 <-> a)))
408. (¬ ((¬ a) <-> (a <-> 1)))
409. (¬ ((1 & a) <-> (¬ a)))
410. (¬ ((a & 1) <-> (¬ a)))
411. (¬ ((a & a) <-> (¬ a)))
412. (¬ ((0 ˅ a) <-> (¬ a)))
413. (¬ ((a ˅ 0) <-> (¬ a)))
414. (¬ ((a ˅ a) <-> (¬ a)))
415. (¬ ((1 -> a) <-> (¬ a)))
416. (¬ ((1 <-> a) <-> (¬ a)))
417. (¬ ((a <-> 1) <-> (¬ a)))
418. (¬ ((¬ (¬ (¬ a))) <-> a))
419. (¬ ((¬ (1 & a)) <-> a))
420. (¬ ((¬ (a & 1)) <-> a))
421. (¬ ((¬ (a & a)) <-> a))
422. (¬ ((¬ (0 ˅ a)) <-> a))
423. (¬ ((¬ (a ˅ 0)) <-> a))
424. (¬ ((¬ (a ˅ a)) <-> a))
425. (¬ ((¬ (1 -> a)) <-> a))
426. (¬ ((¬ (1 <-> a)) <-> a))
427. (¬ ((¬ (a <-> 1)) <-> a))
428. (¬ ((1 & (¬ a)) <-> a))
429. (¬ ((a & (¬ 1)) <-> 1))
430. (¬ ((a & (¬ a)) <-> 1))
431. (¬ (((¬ 1) & a) <-> 1))
432. (¬ (((¬ a) & 1) <-> a))
433. (¬ (((¬ a) & a) <-> 1))
434. (¬ ((0 ˅ (¬ a)) <-> a))
435. (¬ (((¬ a) ˅ 0) <-> a))
436. (¬ ((1 -> (¬ a)) <-> a))
437. (¬ ((a -> (¬ 1)) <-> a))
438. (¬ ((a -> (¬ a)) <-> a))
439. (¬ ((1 <-> (¬ a)) <-> a))
440. (¬ ((a <-> (¬ 1)) <-> a))
441. (¬ ((a <-> (¬ a)) <-> 1))
442. (¬ (((¬ 1) <-> a) <-> a))
443. (¬ (((¬ a) <-> 1) <-> a))
444. (¬ (((¬ a) <-> a) <-> 1))
445. (a ˅ (¬ (¬ (a -> b))))
446. (a ˅ (¬ (¬ (0 <-> a))))
447. (a ˅ (¬ (¬ (a <-> 0))))
448. (a ˅ (¬ (a ˅ (¬ 1))))
449. (a ˅ (¬ ((¬ 1) ˅ a)))
450. (a ˅ (¬ ((¬ a) -> 0)))
451. (a ˅ (¬ ((¬ a) -> a)))
452. (a ˅ (¬ (0 <-> (¬ a))))
453. (a ˅ (¬ ((¬ a) <-> 0)))
454. (a ˅ (1 & (a -> b)))
455. (a ˅ (1 & (0 <-> a)))
456. (a ˅ (1 & (a <-> 0)))
457. (a ˅ ((¬ a) & (¬ a)))
458. (a ˅ ((a -> b) & 1))
459. (a ˅ ((0 <-> a) & 1))
460. (a ˅ ((a <-> 0) & 1))
461. (a ˅ (b ˅ (a -> c)))
462. (a ˅ (b ˅ (0 <-> a)))
463. (a ˅ (b ˅ (a <-> 0)))
464. (a ˅ (b ˅ (a <-> b)))
465. (a ˅ (b ˅ (b <-> a)))
466. (a ˅ ((a -> b) ˅ c))
467. (a ˅ ((0 <-> a) ˅ b))
468. (a ˅ ((a <-> 0) ˅ b))
469. (a ˅ ((a <-> b) ˅ b))
470. (a ˅ ((b <-> a) ˅ b))
471. (a ˅ (b -> (a -> c)))
472. (a ˅ (b -> (0 <-> a)))
473. (a ˅ (b -> (a <-> 0)))
474. (a ˅ ((¬ (¬ a)) -> b))
475. (a ˅ ((a & b) -> c))
476. (a ˅ ((b & a) -> c))
477. (a ˅ ((0 ˅ a) -> b))
478. (a ˅ ((a ˅ 0) -> b))
479. (a ˅ ((a ˅ a) -> b))
480. (a ˅ ((a ˅ b) -> b))
481. (a ˅ ((b ˅ a) -> b))
482. (a ˅ ((1 -> a) -> b))
483. (a ˅ ((1 <-> a) -> b))
484. (a ˅ ((a <-> 1) -> b))
485. (a ˅ (1 <-> (a -> b)))
486. (a ˅ (1 <-> (0 <-> a)))
487. (a ˅ (1 <-> (a <-> 0)))
488. (a ˅ (0 <-> (¬ (¬ a))))
489. (a ˅ (0 <-> (a & b)))
490. (a ˅ (0 <-> (b & a)))
491. (a ˅ (0 <-> (a ˅ a)))
492. (a ˅ (0 <-> (1 -> a)))
493. (a ˅ (0 <-> (1 <-> a)))
494. (a ˅ (0 <-> (a <-> 1)))
495. (a ˅ (a <-> (0 & b)))
496. (a ˅ (a <-> (a & b)))
497. (a ˅ (a <-> (b & 0)))
498. (a ˅ (a <-> (b & a)))
499. (a ˅ (a <-> (0 ˅ 0)))
500. (a ˅ (a <-> (1 -> 0)))
501. (a ˅ (a <-> (1 <-> 0)))
502. (a ˅ (a <-> (0 <-> 1)))
503. (a ˅ (b <-> (a ˅ b)))
504. (a ˅ (b <-> (b ˅ a)))
505. (a ˅ ((¬ (¬ a)) <-> 0))
506. (a ˅ ((0 & b) <-> a))
507. (a ˅ ((a & b) <-> 0))
508. (a ˅ ((a & b) <-> a))
509. (a ˅ ((b & 0) <-> a))
510. (a ˅ ((b & a) <-> 0))
511. (a ˅ ((b & a) <-> a))
512. (a ˅ ((0 ˅ 0) <-> a))
513. (a ˅ ((a ˅ a) <-> 0))
514. (a ˅ ((a ˅ b) <-> b))
515. (a ˅ ((b ˅ a) <-> b))
516. (a ˅ ((1 -> 0) <-> a))
517. (a ˅ ((1 -> a) <-> 0))
518. (a ˅ ((a -> b) <-> 1))
519. (a ˅ ((1 <-> 0) <-> a))
520. (a ˅ ((1 <-> a) <-> 0))
521. (a ˅ ((0 <-> 1) <-> a))
522. (a ˅ ((0 <-> a) <-> 1))
523. (a ˅ ((a <-> 1) <-> 0))
524. (a ˅ ((a <-> 0) <-> 1))
525. ((¬ a) ˅ (¬ (a -> 0)))
526. ((¬ a) ˅ (¬ (0 <-> a)))
527. ((¬ a) ˅ (¬ (a <-> 0)))
528. ((¬ (¬ a)) ˅ (a -> b))
529. ((¬ (¬ a)) ˅ (0 <-> a))
530. ((¬ (¬ a)) ˅ (a <-> 0))
531. ((1 & a) ˅ (a -> b))
532. ((1 & a) ˅ (0 <-> a))
533. ((1 & a) ˅ (a <-> 0))
534. ((a & 1) ˅ (a -> b))
535. ((a & 1) ˅ (0 <-> a))
536. ((a & 1) ˅ (a <-> 0))
537. ((a & a) ˅ (a -> b))
538. ((a & a) ˅ (0 <-> a))
539. ((a & a) ˅ (a <-> 0))
540. ((a ˅ b) ˅ (a -> c))
541. ((a ˅ b) ˅ (b -> c))
542. ((a ˅ b) ˅ (0 <-> a))
543. ((a ˅ b) ˅ (0 <-> b))
544. ((a ˅ b) ˅ (a <-> 0))
545. ((a ˅ b) ˅ (a <-> b))
546. ((a ˅ b) ˅ (b <-> 0))
547. ((a ˅ b) ˅ (b <-> a))
548. ((a -> b) ˅ (¬ (¬ a)))
549. ((a -> b) ˅ (1 & a))
550. ((a -> b) ˅ (a & 1))
551. ((a -> b) ˅ (a & a))
552. ((a -> b) ˅ (a ˅ c))
553. ((a -> b) ˅ (c ˅ a))
554. ((a -> b) ˅ (b -> c))
555. ((a -> b) ˅ (c -> a))
556. ((a -> b) ˅ (1 <-> a))
557. ((a -> b) ˅ (0 <-> b))
558. ((a -> b) ˅ (a <-> 1))
559. ((a -> b) ˅ (b <-> 0))
560. ((1 <-> a) ˅ (a -> b))
561. ((1 <-> a) ˅ (0 <-> a))
562. ((1 <-> a) ˅ (a <-> 0))
563. ((0 <-> a) ˅ (¬ (¬ a)))
564. ((0 <-> a) ˅ (1 & a))
565. ((0 <-> a) ˅ (a & 1))
566. ((0 <-> a) ˅ (a & a))
567. ((0 <-> a) ˅ (a ˅ b))
568. ((0 <-> a) ˅ (b ˅ a))
569. ((0 <-> a) ˅ (b -> a))
570. ((0 <-> a) ˅ (1 <-> a))
571. ((0 <-> a) ˅ (a <-> 1))
572. ((a <-> 1) ˅ (a -> b))
573. ((a <-> 1) ˅ (0 <-> a))
574. ((a <-> 1) ˅ (a <-> 0))
575. ((a <-> 0) ˅ (¬ (¬ a)))
576. ((a <-> 0) ˅ (1 & a))
577. ((a <-> 0) ˅ (a & 1))
578. ((a <-> 0) ˅ (a & a))
579. ((a <-> 0) ˅ (a ˅ b))
580. ((a <-> 0) ˅ (b ˅ a))
581. ((a <-> 0) ˅ (b -> a))
582. ((a <-> 0) ˅ (1 <-> a))
583. ((a <-> 0) ˅ (a <-> 1))
584. ((a <-> b) ˅ (a ˅ b))
585. ((a <-> b) ˅ (b ˅ a))
586. ((¬ (a -> 0)) ˅ (¬ a))
587. ((¬ (0 <-> a)) ˅ (¬ a))
588. ((¬ (a <-> 0)) ˅ (¬ a))
589. ((¬ (¬ (a -> b))) ˅ a)
590. ((¬ (¬ (0 <-> a))) ˅ a)
591. ((¬ (¬ (a <-> 0))) ˅ a)
592. ((¬ (a ˅ (¬ 1))) ˅ a)
593. ((¬ ((¬ 1) ˅ a)) ˅ a)
594. ((¬ ((¬ a) -> 0)) ˅ a)
595. ((¬ ((¬ a) -> a)) ˅ a)
596. ((¬ (0 <-> (¬ a))) ˅ a)
597. ((¬ ((¬ a) <-> 0)) ˅ a)
598. ((1 & (a -> b)) ˅ a)
599. ((1 & (0 <-> a)) ˅ a)
600. ((1 & (a <-> 0)) ˅ a)
    601. (((¬ a) & (¬ a)) ˅ a)
602. (((a -> b) & 1) ˅ a)
603. (((0 <-> a) & 1) ˅ a)
604. (((a <-> 0) & 1) ˅ a)
605. ((a ˅ (b -> c)) ˅ b)
606. ((a ˅ (0 <-> b)) ˅ b)
607. ((a ˅ (a <-> b)) ˅ b)
608. ((a ˅ (b <-> 0)) ˅ b)
609. ((a ˅ (b <-> a)) ˅ b)
610. (((a -> b) ˅ c) ˅ a)
611. (((0 <-> a) ˅ b) ˅ a)
612. (((a <-> 0) ˅ b) ˅ a)
613. (((a <-> b) ˅ a) ˅ b)
614. (((a <-> b) ˅ b) ˅ a)
615. ((a -> (b -> c)) ˅ b)
616. ((a -> (0 <-> b)) ˅ b)
617. ((a -> (b <-> 0)) ˅ b)
618. (((¬ (¬ a)) -> b) ˅ a)
619. (((a & b) -> c) ˅ a)
620. (((a & b) -> c) ˅ b)
621. (((0 ˅ a) -> b) ˅ a)
622. (((a ˅ 0) -> b) ˅ a)
623. (((a ˅ a) -> b) ˅ a)
624. (((a ˅ b) -> a) ˅ b)
625. (((a ˅ b) -> b) ˅ a)
626. (((1 -> a) -> b) ˅ a)
627. (((1 <-> a) -> b) ˅ a)
628. (((a <-> 1) -> b) ˅ a)
629. ((1 <-> (a -> b)) ˅ a)
630. ((1 <-> (0 <-> a)) ˅ a)
631. ((1 <-> (a <-> 0)) ˅ a)
632. ((0 <-> (¬ (¬ a))) ˅ a)
633. ((0 <-> (a & b)) ˅ a)
634. ((0 <-> (a & b)) ˅ b)
635. ((0 <-> (a ˅ a)) ˅ a)
636. ((0 <-> (1 -> a)) ˅ a)
637. ((0 <-> (1 <-> a)) ˅ a)
638. ((0 <-> (a <-> 1)) ˅ a)
639. ((a <-> (0 & b)) ˅ a)
640. ((a <-> (a & b)) ˅ a)
641. ((a <-> (b & 0)) ˅ a)
642. ((a <-> (b & a)) ˅ a)
643. ((a <-> (0 ˅ 0)) ˅ a)
644. ((a <-> (a ˅ b)) ˅ b)
645. ((a <-> (b ˅ a)) ˅ b)
646. ((a <-> (1 -> 0)) ˅ a)
647. ((a <-> (1 <-> 0)) ˅ a)
648. ((a <-> (0 <-> 1)) ˅ a)
649. (((¬ (¬ a)) <-> 0) ˅ a)
650. (((0 & a) <-> b) ˅ b)
651. (((a & 0) <-> b) ˅ b)
652. (((a & b) <-> 0) ˅ a)
653. (((a & b) <-> 0) ˅ b)
654. (((a & b) <-> a) ˅ a)
655. (((a & b) <-> b) ˅ b)
656. (((0 ˅ 0) <-> a) ˅ a)
657. (((a ˅ a) <-> 0) ˅ a)
658. (((a ˅ b) <-> a) ˅ b)
659. (((a ˅ b) <-> b) ˅ a)
660. (((1 -> 0) <-> a) ˅ a)
661. (((1 -> a) <-> 0) ˅ a)
662. (((a -> b) <-> 1) ˅ a)
663. (((1 <-> 0) <-> a) ˅ a)
664. (((1 <-> a) <-> 0) ˅ a)
665. (((0 <-> 1) <-> a) ˅ a)
666. (((0 <-> a) <-> 1) ˅ a)
667. (((a <-> 1) <-> 0) ˅ a)
668. (((a <-> 0) <-> 1) ˅ a)
669. (a -> (¬ (¬ (¬ (¬ a)))))
670. (a -> (¬ (¬ (1 & a))))
671. (a -> (¬ (¬ (a & 1))))
672. (a -> (¬ (¬ (a & a))))
673. (a -> (¬ (¬ (a ˅ b))))
674. (a -> (¬ (¬ (b ˅ a))))
675. (a -> (¬ (¬ (b -> a))))
676. (a -> (¬ (¬ (1 <-> a))))
677. (a -> (¬ (¬ (a <-> 1))))
678. (a -> (¬ (b & (¬ a))))
679. (a -> (¬ ((¬ a) & b)))
680. (a -> (¬ (0 ˅ (¬ a))))
681. (a -> (¬ ((¬ a) ˅ 0)))
682. (a -> (¬ (1 -> (¬ a))))
683. (a -> (¬ (a -> (¬ 1))))
684. (a -> (¬ (a -> (¬ a))))
685. (a -> (¬ (1 <-> (¬ a))))
686. (a -> (¬ (a <-> (¬ 1))))
687. (a -> (¬ ((¬ 1) <-> a)))
688. (a -> (¬ ((¬ a) <-> 1)))
689. (a -> (1 & (¬ (¬ a))))
690. (a -> (1 & (1 & a)))
691. (a -> (1 & (a & 1)))
692. (a -> (1 & (a & a)))
693. (a -> (1 & (a ˅ b)))
694. (a -> (1 & (b ˅ a)))
695. (a -> (1 & (b -> a)))
696. (a -> (1 & (1 <-> a)))
697. (a -> (1 & (a <-> 1)))
698. (a -> (a & (¬ (¬ a))))
699. (a -> (a & (1 & a)))
700. (a -> (a & (a & 1)))
701. (a -> (a & (a & a)))
702. (a -> (a & (a ˅ b)))
703. (a -> (a & (b ˅ a)))
704. (a -> (a & (b -> a)))
705. (a -> (a & (1 <-> a)))
706. (a -> (a & (a <-> 1)))
707. (a -> ((¬ (¬ a)) & 1))
708. (a -> ((¬ (¬ a)) & a))
709. (a -> ((1 & a) & 1))
710. (a -> ((1 & a) & a))
711. (a -> ((a & 1) & 1))
712. (a -> ((a & 1) & a))
713. (a -> ((a & a) & 1))
714. (a -> ((a & a) & a))
715. (a -> ((a ˅ b) & 1))
716. (a -> ((a ˅ b) & a))
717. (a -> ((b ˅ a) & 1))
718. (a -> ((b ˅ a) & a))
719. (a -> ((b -> a) & 1))
720. (a -> ((b -> a) & a))
721. (a -> ((1 <-> a) & 1))
722. (a -> ((1 <-> a) & a))
723. (a -> ((a <-> 1) & 1))
724. (a -> ((a <-> 1) & a))
725. (a -> (b ˅ (¬ (¬ a))))
726. (a -> (b ˅ (1 & a)))
727. (a -> (b ˅ (a & 1)))
728. (a -> (b ˅ (a & a)))
729. (a -> (b ˅ (a ˅ c)))
730. (a -> (b ˅ (c ˅ a)))
731. (a -> (b ˅ (c -> a)))
732. (a -> (b ˅ (1 <-> a)))
733. (a -> (b ˅ (a <-> 1)))
734. (a -> ((¬ (¬ a)) ˅ b))
735. (a -> ((1 & a) ˅ b))
736. (a -> ((a & 1) ˅ b))
737. (a -> ((a & a) ˅ b))
738. (a -> ((a ˅ b) ˅ c))
739. (a -> ((b ˅ a) ˅ c))
740. (a -> ((b -> a) ˅ c))
741. (a -> ((1 <-> a) ˅ b))
742. (a -> ((a <-> 1) ˅ b))
743. (a -> (b -> (¬ (¬ a))))
744. (a -> (b -> (1 & a)))
745. (a -> (b -> (a & 1)))
746. (a -> (b -> (a & a)))
747. (a -> (b -> (a & b)))
748. (a -> (b -> (b & a)))
749. (a -> (b -> (a ˅ c)))
750. (a -> (b -> (c ˅ a)))
751. (a -> (b -> (c -> a)))
752. (a -> (b -> (1 <-> a)))
753. (a -> (b -> (a <-> 1)))
754. (a -> (b -> (a <-> b)))
755. (a -> (b -> (b <-> a)))
756. (a -> ((a -> 0) -> b))
757. (a -> ((a -> b) -> b))
758. (a -> ((0 <-> a) -> b))
759. (a -> ((a <-> 0) -> b))
760. (a -> ((a <-> b) -> b))
761. (a -> ((b <-> a) -> b))
762. (a -> (1 <-> (¬ (¬ a))))
763. (a -> (1 <-> (a & a)))
764. (a -> (1 <-> (a ˅ b)))
765. (a -> (1 <-> (b ˅ a)))
766. (a -> (1 <-> (b -> a)))
767. (a -> (a <-> (a ˅ b)))
768. (a -> (a <-> (b ˅ a)))
769. (a -> (a <-> (b -> a)))
770. (a -> (b <-> (a & b)))
771. (a -> (b <-> (b & a)))
772. (a -> (b <-> (a -> b)))
773. (a -> (b <-> (a <-> b)))
774. (a -> (b <-> (b <-> a)))
775. (a -> ((¬ 1) <-> (¬ a)))
776. (a -> ((¬ a) <-> (¬ 1)))
777. (a -> ((¬ (¬ a)) <-> 1))
778. (a -> ((a & a) <-> 1))
779. (a -> ((a & b) <-> b))
780. (a -> ((b & a) <-> b))
781. (a -> ((a ˅ b) <-> 1))
782. (a -> ((a ˅ b) <-> a))
783. (a -> ((b ˅ a) <-> 1))
784. (a -> ((b ˅ a) <-> a))
785. (a -> ((a -> b) <-> b))
786. (a -> ((b -> a) <-> 1))
787. (a -> ((b -> a) <-> a))
788. (a -> ((a <-> b) <-> b))
789. (a -> ((b <-> a) <-> b))
790. ((¬ a) -> (¬ (a & b)))
791. ((¬ a) -> (¬ (b & a)))
792. ((¬ a) -> (¬ (0 ˅ a)))
793. ((¬ a) -> (¬ (a ˅ 0)))
794. ((¬ a) -> (¬ (a ˅ a)))
795. ((¬ a) -> (¬ (1 -> a)))
796. ((¬ a) -> (¬ (1 <-> a)))
797. ((¬ a) -> (¬ (a <-> 1)))
798. ((¬ a) -> (a <-> (¬ 1)))
799. ((¬ a) -> ((¬ 1) <-> a))
800. ((¬ (¬ a)) -> (1 & a))
801. ((¬ (¬ a)) -> (a & 1))
802. ((¬ (¬ a)) -> (a & a))
803. ((¬ (¬ a)) -> (a ˅ b))
804. ((¬ (¬ a)) -> (b ˅ a))
805. ((¬ (¬ a)) -> (b -> a))
806. ((¬ (¬ a)) -> (1 <-> a))
807. ((¬ (¬ a)) -> (a <-> 1))
808. ((a & b) -> (¬ (¬ a)))
809. ((a & b) -> (¬ (¬ b)))
810. ((a & b) -> (1 & a))
811. ((a & b) -> (1 & b))
812. ((a & b) -> (a & 1))
813. ((a & b) -> (a & a))
814. ((a & b) -> (b & 1))
815. ((a & b) -> (b & a))
816. ((a & b) -> (b & b))
817. ((a & b) -> (a ˅ c))
818. ((a & b) -> (b ˅ c))
819. ((a & b) -> (c ˅ a))
820. ((a & b) -> (c ˅ b))
821. ((a & b) -> (c -> a))
822. ((a & b) -> (c -> b))
823. ((a & b) -> (1 <-> a))
824. ((a & b) -> (1 <-> b))
825. ((a & b) -> (a <-> 1))
826. ((a & b) -> (a <-> b))
827. ((a & b) -> (b <-> 1))
828. ((a & b) -> (b <-> a))
829. ((0 ˅ a) -> (¬ (¬ a)))
830. ((0 ˅ a) -> (1 & a))
831. ((0 ˅ a) -> (a & 1))
832. ((0 ˅ a) -> (a & a))
833. ((0 ˅ a) -> (a ˅ b))
834. ((0 ˅ a) -> (b ˅ a))
835. ((0 ˅ a) -> (b -> a))
836. ((0 ˅ a) -> (1 <-> a))
837. ((0 ˅ a) -> (a <-> 1))
838. ((a ˅ 0) -> (¬ (¬ a)))
839. ((a ˅ 0) -> (1 & a))
840. ((a ˅ 0) -> (a & 1))
841. ((a ˅ 0) -> (a & a))
842. ((a ˅ 0) -> (a ˅ b))
843. ((a ˅ 0) -> (b ˅ a))
844. ((a ˅ 0) -> (b -> a))
845. ((a ˅ 0) -> (1 <-> a))
846. ((a ˅ 0) -> (a <-> 1))
847. ((a ˅ a) -> (¬ (¬ a)))
848. ((a ˅ a) -> (1 & a))
849. ((a ˅ a) -> (a & 1))
850. ((a ˅ a) -> (a & a))
851. ((a ˅ a) -> (a ˅ b))
852. ((a ˅ a) -> (b ˅ a))
853. ((a ˅ a) -> (b -> a))
854. ((a ˅ a) -> (1 <-> a))
855. ((a ˅ a) -> (a <-> 1))
856. ((a ˅ b) -> (b ˅ a))
857. ((1 -> a) -> (¬ (¬ a)))
858. ((1 -> a) -> (1 & a))
859. ((1 -> a) -> (a & 1))
860. ((1 -> a) -> (a & a))
861. ((1 -> a) -> (a ˅ b))
862. ((1 -> a) -> (b ˅ a))
863. ((1 -> a) -> (b -> a))
864. ((1 -> a) -> (1 <-> a))
865. ((1 -> a) -> (a <-> 1))
866. ((a -> 0) -> (a -> b))
867. ((a -> 0) -> (0 <-> a))
868. ((a -> 0) -> (a <-> 0))
869. ((1 <-> a) -> (¬ (¬ a)))
870. ((1 <-> a) -> (1 & a))
871. ((1 <-> a) -> (a & 1))
872. ((1 <-> a) -> (a & a))
873. ((1 <-> a) -> (a ˅ b))
874. ((1 <-> a) -> (b ˅ a))
875. ((1 <-> a) -> (b -> a))
876. ((0 <-> a) -> (a -> b))
877. ((a <-> 1) -> (¬ (¬ a)))
878. ((a <-> 1) -> (1 & a))
879. ((a <-> 1) -> (a & 1))
880. ((a <-> 1) -> (a & a))
881. ((a <-> 1) -> (a ˅ b))
882. ((a <-> 1) -> (b ˅ a))
883. ((a <-> 1) -> (b -> a))
884. ((a <-> 0) -> (a -> b))
885. ((a <-> b) -> (a -> b))
886. ((a <-> b) -> (b -> a))
887. ((a <-> b) -> (b <-> a))
888. ((¬ (1 & a)) -> (¬ a))
889. ((¬ (a & 1)) -> (¬ a))
890. ((¬ (a & a)) -> (¬ a))
891. ((¬ (a ˅ b)) -> (¬ a))
892. ((¬ (a ˅ b)) -> (¬ b))
893. ((¬ (a -> b)) -> (¬ b))
894. ((¬ (1 <-> a)) -> (¬ a))
895. ((¬ (a <-> 1)) -> (¬ a))
896. ((a -> (¬ 1)) -> (¬ a))
897. ((a -> (¬ a)) -> (¬ a))
898. ((a <-> (¬ 1)) -> (¬ a))
899. (((¬ 1) <-> a) -> (¬ a))
900. ((¬ (¬ (¬ (¬ a)))) -> a)
901. ((¬ (¬ (a & b))) -> a)
902. ((¬ (¬ (a & b))) -> b)
903. ((¬ (¬ (0 ˅ a))) -> a)
904. ((¬ (¬ (a ˅ 0))) -> a)
905. ((¬ (¬ (a ˅ a))) -> a)
906. ((¬ (¬ (1 -> a))) -> a)
907. ((¬ (¬ (1 <-> a))) -> a)
908. ((¬ (¬ (a <-> 1))) -> a)
909. ((¬ (1 & (¬ a))) -> a)
910. ((¬ ((¬ a) & 1)) -> a)
911. ((¬ (a ˅ (¬ b))) -> b)
912. ((¬ ((¬ a) ˅ b)) -> a)
913. ((¬ (a -> (¬ b))) -> b)
914. ((¬ (1 <-> (¬ a))) -> a)
915. ((¬ (a <-> (¬ 1))) -> a)
916. ((¬ ((¬ 1) <-> a)) -> a)
917. ((¬ ((¬ a) <-> 1)) -> a)
918. ((a & (¬ (¬ b))) -> b)
919. ((a & (0 & b)) -> c)
920. ((a & (b & 0)) -> c)
921. ((a & (b & c)) -> b)
922. ((a & (b & c)) -> c)
923. ((a & (0 ˅ 0)) -> b)
924. ((a & (0 ˅ b)) -> b)
925. ((a & (b ˅ 0)) -> b)
926. ((a & (b ˅ b)) -> b)
927. ((a & (1 -> 0)) -> b)
928. ((a & (1 -> b)) -> b)
929. ((a & (a -> 0)) -> b)
930. ((a & (a -> b)) -> b)
931. ((a & (1 <-> 0)) -> b)
932. ((a & (1 <-> b)) -> b)
933. ((a & (0 <-> 1)) -> b)
934. ((a & (0 <-> a)) -> b)
935. ((a & (a <-> 0)) -> b)
936. ((a & (a <-> b)) -> b)
937. ((a & (b <-> 1)) -> b)
938. ((a & (b <-> a)) -> b)
939. (((¬ (¬ a)) & b) -> a)
940. (((0 & a) & b) -> c)
941. (((a & 0) & b) -> c)
942. (((a & b) & c) -> a)
943. (((a & b) & c) -> b)
944. (((0 ˅ 0) & a) -> b)
945. (((0 ˅ a) & b) -> a)
946. (((a ˅ 0) & b) -> a)
947. (((a ˅ a) & b) -> a)
948. (((1 -> 0) & a) -> b)
949. (((1 -> a) & b) -> a)
950. (((a -> 0) & a) -> b)
951. (((a -> b) & a) -> b)
952. (((1 <-> 0) & a) -> b)
953. (((1 <-> a) & b) -> a)
954. (((0 <-> 1) & a) -> b)
955. (((0 <-> a) & a) -> b)
956. (((a <-> 1) & b) -> a)
957. (((a <-> 0) & a) -> b)
958. (((a <-> b) & a) -> b)
959. (((a <-> b) & b) -> a)
960. ((0 ˅ (¬ (¬ a))) -> a)
961. ((0 ˅ (0 & a)) -> b)
962. ((0 ˅ (a & 0)) -> b)
963. ((0 ˅ (a & b)) -> a)
964. ((0 ˅ (a & b)) -> b)
965. ((0 ˅ (0 ˅ 0)) -> a)
966. ((0 ˅ (0 ˅ a)) -> a)
967. ((0 ˅ (a ˅ 0)) -> a)
968. ((0 ˅ (a ˅ a)) -> a)
969. ((0 ˅ (1 -> 0)) -> a)
970. ((0 ˅ (1 -> a)) -> a)
971. ((0 ˅ (1 <-> 0)) -> a)
972. ((0 ˅ (1 <-> a)) -> a)
973. ((0 ˅ (0 <-> 1)) -> a)
974. ((0 ˅ (a <-> 1)) -> a)
975. ((a ˅ (¬ (¬ a))) -> a)
976. ((a ˅ (0 & b)) -> a)
977. ((a ˅ (a & b)) -> a)
978. ((a ˅ (b & 0)) -> a)
979. ((a ˅ (b & a)) -> a)
980. ((a ˅ (0 ˅ 0)) -> a)
981. ((a ˅ (0 ˅ a)) -> a)
982. ((a ˅ (a ˅ 0)) -> a)
983. ((a ˅ (a ˅ a)) -> a)
984. ((a ˅ (1 -> 0)) -> a)
985. ((a ˅ (1 -> a)) -> a)
986. ((a ˅ (1 <-> 0)) -> a)
987. ((a ˅ (1 <-> a)) -> a)
988. ((a ˅ (0 <-> 1)) -> a)
989. ((a ˅ (a <-> 1)) -> a)
990. (((¬ 1) ˅ (¬ 1)) -> a)
991. (((¬ (¬ a)) ˅ 0) -> a)
992. (((¬ (¬ a)) ˅ a) -> a)
993. (((0 & a) ˅ 0) -> b)
994. (((0 & a) ˅ b) -> b)
995. (((a & 0) ˅ 0) -> b)
996. (((a & 0) ˅ b) -> b)
997. (((a & b) ˅ 0) -> a)
998. (((a & b) ˅ 0) -> b)
999. (((a & b) ˅ a) -> a)
1000. (((a & b) ˅ b) -> b)
1001. (((0 ˅ 0) ˅ 0) -> a)
1002. (((0 ˅ 0) ˅ a) -> a)
1003. (((0 ˅ a) ˅ 0) -> a)
1004. (((0 ˅ a) ˅ a) -> a)
1005. (((a ˅ 0) ˅ 0) -> a)
1006. (((a ˅ 0) ˅ a) -> a)
1007. (((a ˅ a) ˅ 0) -> a)
1008. (((a ˅ a) ˅ a) -> a)
1009. (((1 -> 0) ˅ 0) -> a)
1010. (((1 -> 0) ˅ a) -> a)
1011. (((1 -> a) ˅ 0) -> a)
1012. (((1 -> a) ˅ a) -> a)
1013. (((1 <-> 0) ˅ 0) -> a)
1014. (((1 <-> 0) ˅ a) -> a)
1015. (((1 <-> a) ˅ 0) -> a)
1016. (((1 <-> a) ˅ a) -> a)
1017. (((0 <-> 1) ˅ 0) -> a)
1018. (((0 <-> 1) ˅ a) -> a)
1019. (((a <-> 1) ˅ 0) -> a)
1020. (((a <-> 1) ˅ a) -> a)
1021. ((1 -> (¬ (¬ a))) -> a)
1022. ((1 -> (0 & a)) -> b)
1023. ((1 -> (a & 0)) -> b)
1024. ((1 -> (a & b)) -> a)
1025. ((1 -> (a & b)) -> b)
1026. ((1 -> (0 ˅ 0)) -> a)
1027. ((1 -> (0 ˅ a)) -> a)
1028. ((1 -> (a ˅ 0)) -> a)
1029. ((1 -> (a ˅ a)) -> a)
1030. ((1 -> (1 -> 0)) -> a)
1031. ((1 -> (1 -> a)) -> a)
1032. ((1 -> (1 <-> 0)) -> a)
1033. ((1 -> (1 <-> a)) -> a)
1034. ((1 -> (0 <-> 1)) -> a)
1035. ((1 -> (a <-> 1)) -> a)
1036. (((¬ a) -> (¬ 1)) -> a)
1037. (((a -> b) -> 0) -> a)
1038. (((a -> b) -> a) -> a)
1039. (((0 <-> a) -> 0) -> a)
1040. (((0 <-> a) -> a) -> a)
1041. (((a <-> 0) -> 0) -> a)
1042. (((a <-> 0) -> a) -> a)
1043. ((1 <-> (¬ (¬ a))) -> a)
1044. ((1 <-> (0 & a)) -> b)
1045. ((1 <-> (a & 0)) -> b)
1046. ((1 <-> (a & b)) -> a)
1047. ((1 <-> (a & b)) -> b)
1048. ((1 <-> (0 ˅ 0)) -> a)
1049. ((1 <-> (0 ˅ a)) -> a)
1050. ((1 <-> (a ˅ 0)) -> a)
1051. ((1 <-> (a ˅ a)) -> a)
1052. ((0 <-> (a -> b)) -> a)
1053. ((a <-> (a -> 0)) -> b)
1054. ((a <-> (a -> b)) -> a)
1055. ((a <-> (a -> b)) -> b)
1056. ((a <-> (0 <-> a)) -> b)
1057. ((a <-> (a <-> 0)) -> b)
1058. ((a <-> (a <-> b)) -> b)
1059. ((a <-> (b <-> a)) -> b)
1060. (((¬ 1) <-> (¬ a)) -> a)
1061. (((¬ a) <-> (¬ 1)) -> a)
1062. (((¬ (¬ a)) <-> 1) -> a)
1063. (((0 & a) <-> 1) -> b)
1064. (((a & 0) <-> 1) -> b)
1065. (((a & b) <-> 1) -> a)
1066. (((a & b) <-> 1) -> b)
1067. (((0 ˅ 0) <-> 1) -> a)
1068. (((0 ˅ a) <-> 1) -> a)
1069. (((a ˅ 0) <-> 1) -> a)
1070. (((a ˅ a) <-> 1) -> a)
1071. (((a -> 0) <-> a) -> b)
1072. (((a -> b) <-> 0) -> a)
1073. (((a -> b) <-> a) -> a)
1074. (((a -> b) <-> a) -> b)
1075. (((0 <-> a) <-> a) -> b)
1076. (((a <-> 0) <-> a) -> b)
1077. (((a <-> b) <-> a) -> b)
1078. (((a <-> b) <-> b) -> a)
1079. (0 <-> (a & (0 & b)))
1080. (0 <-> (a & (b & 0)))
1081. (0 <-> (a & (0 ˅ 0)))
1082. (0 <-> (a & (1 -> 0)))
1083. (0 <-> (a & (a -> 0)))
1084. (0 <-> (a & (1 <-> 0)))
1085. (0 <-> (a & (0 <-> 1)))
1086. (0 <-> (a & (0 <-> a)))
1087. (0 <-> (a & (a <-> 0)))
1088. (0 <-> ((0 & a) & b))
1089. (0 <-> ((a & 0) & b))
1090. (0 <-> ((0 ˅ 0) & a))
1091. (0 <-> ((1 -> 0) & a))
1092. (0 <-> ((a -> 0) & a))
1093. (0 <-> ((1 <-> 0) & a))
1094. (0 <-> ((0 <-> 1) & a))
1095. (0 <-> ((0 <-> a) & a))
1096. (0 <-> ((a <-> 0) & a))
1097. (0 <-> ((¬ 1) ˅ (¬ 1)))
1098. (0 <-> (1 -> (0 & a)))
1099. (0 <-> (1 -> (a & 0)))
1100. (0 <-> (1 <-> (0 & a)))
1101. (0 <-> (1 <-> (a & 0)))
1102. (0 <-> (a <-> (a -> 0)))
1103. (0 <-> ((0 & a) <-> 1))
1104. (0 <-> ((a & 0) <-> 1))
1105. (0 <-> ((a -> 0) <-> a))
1106. (a <-> (¬ (¬ (¬ (¬ a)))))
1107. (a <-> (¬ (¬ (1 & a))))
1108. (a <-> (¬ (¬ (a & 1))))
1109. (a <-> (¬ (¬ (a & a))))
1110. (a <-> (¬ (¬ (0 ˅ a))))
1111. (a <-> (¬ (¬ (a ˅ 0))))
1112. (a <-> (¬ (¬ (a ˅ a))))
1113. (a <-> (¬ (¬ (1 -> a))))
1114. (a <-> (¬ (¬ (1 <-> a))))
1115. (a <-> (¬ (¬ (a <-> 1))))
1116. (a <-> (¬ (1 & (¬ a))))
1117. (a <-> (¬ ((¬ a) & 1)))
1118. (a <-> (¬ (0 ˅ (¬ a))))
1119. (a <-> (¬ ((¬ a) ˅ 0)))
1120. (a <-> (¬ (1 -> (¬ a))))
1121. (a <-> (¬ (a -> (¬ 1))))
1122. (a <-> (¬ (a -> (¬ a))))
1123. (a <-> (¬ (1 <-> (¬ a))))
1124. (a <-> (¬ (a <-> (¬ 1))))
1125. (a <-> (¬ ((¬ 1) <-> a)))
1126. (a <-> (¬ ((¬ a) <-> 1)))
1127. (a <-> (1 & (¬ (¬ a))))
1128. (a <-> (1 & (1 & a)))
1129. (a <-> (1 & (a & 1)))
1130. (a <-> (1 & (a & a)))
1131. (a <-> (1 & (0 ˅ a)))
1132. (a <-> (1 & (a ˅ 0)))
1133. (a <-> (1 & (a ˅ a)))
1134. (a <-> (1 & (1 -> a)))
1135. (a <-> (1 & (1 <-> a)))
1136. (a <-> (1 & (a <-> 1)))
1137. (a <-> (a & (¬ (¬ a))))
1138. (a <-> (a & (1 & a)))
1139. (a <-> (a & (a & 1)))
1140. (a <-> (a & (a & a)))
1141. (a <-> (a & (a ˅ b)))
1142. (a <-> (a & (b ˅ a)))
1143. (a <-> (a & (b -> a)))
1144. (a <-> (a & (1 <-> a)))
1145. (a <-> (a & (a <-> 1)))
1146. (a <-> ((¬ (¬ a)) & 1))
1147. (a <-> ((¬ (¬ a)) & a))
1148. (a <-> ((1 & a) & 1))
1149. (a <-> ((1 & a) & a))
1150. (a <-> ((a & 1) & 1))
1151. (a <-> ((a & 1) & a))
1152. (a <-> ((a & a) & 1))
1153. (a <-> ((a & a) & a))
1154. (a <-> ((0 ˅ a) & 1))
1155. (a <-> ((a ˅ 0) & 1))
1156. (a <-> ((a ˅ a) & 1))
1157. (a <-> ((a ˅ b) & a))
1158. (a <-> ((b ˅ a) & a))
1159. (a <-> ((1 -> a) & 1))
1160. (a <-> ((b -> a) & a))
1161. (a <-> ((1 <-> a) & 1))
1162. (a <-> ((1 <-> a) & a))
1163. (a <-> ((a <-> 1) & 1))
1164. (a <-> ((a <-> 1) & a))
1165. (a <-> (0 ˅ (¬ (¬ a))))
1166. (a <-> (0 ˅ (1 & a)))
1167. (a <-> (0 ˅ (a & 1)))
1168. (a <-> (0 ˅ (a & a)))
1169. (a <-> (0 ˅ (0 ˅ a)))
1170. (a <-> (0 ˅ (a ˅ 0)))
1171. (a <-> (0 ˅ (a ˅ a)))
1172. (a <-> (0 ˅ (1 -> a)))
1173. (a <-> (0 ˅ (1 <-> a)))
1174. (a <-> (0 ˅ (a <-> 1)))
1175. (a <-> (a ˅ (¬ (¬ a))))
1176. (a <-> (a ˅ (0 & b)))
1177. (a <-> (a ˅ (a & b)))
1178. (a <-> (a ˅ (b & 0)))
1179. (a <-> (a ˅ (b & a)))
1180. (a <-> (a ˅ (0 ˅ 0)))
1181. (a <-> (a ˅ (0 ˅ a)))
1182. (a <-> (a ˅ (a ˅ 0)))
1183. (a <-> (a ˅ (a ˅ a)))
1184. (a <-> (a ˅ (1 -> 0)))
1185. (a <-> (a ˅ (1 -> a)))
1186. (a <-> (a ˅ (1 <-> 0)))
1187. (a <-> (a ˅ (1 <-> a)))
1188. (a <-> (a ˅ (0 <-> 1)))
1189. (a <-> (a ˅ (a <-> 1)))
1190. (a <-> ((¬ (¬ a)) ˅ 0))
1191. (a <-> ((¬ (¬ a)) ˅ a))
1192. (a <-> ((1 & a) ˅ 0))
1193. (a <-> ((0 & b) ˅ a))
1194. (a <-> ((a & 1) ˅ 0))
1195. (a <-> ((a & a) ˅ 0))
1196. (a <-> ((a & b) ˅ a))
1197. (a <-> ((b & 0) ˅ a))
1198. (a <-> ((b & a) ˅ a))
1199. (a <-> ((0 ˅ 0) ˅ a))
1200. (a <-> ((0 ˅ a) ˅ 0))
    1201. (a <-> ((0 ˅ a) ˅ a))
1202. (a <-> ((a ˅ 0) ˅ 0))
1203. (a <-> ((a ˅ 0) ˅ a))
1204. (a <-> ((a ˅ a) ˅ 0))
1205. (a <-> ((a ˅ a) ˅ a))
1206. (a <-> ((1 -> 0) ˅ a))
1207. (a <-> ((1 -> a) ˅ 0))
1208. (a <-> ((1 -> a) ˅ a))
1209. (a <-> ((1 <-> 0) ˅ a))
1210. (a <-> ((1 <-> a) ˅ 0))
1211. (a <-> ((1 <-> a) ˅ a))
1212. (a <-> ((0 <-> 1) ˅ a))
1213. (a <-> ((a <-> 1) ˅ 0))
1214. (a <-> ((a <-> 1) ˅ a))
1215. (a <-> (1 -> (¬ (¬ a))))
1216. (a <-> (1 -> (1 & a)))
1217. (a <-> (1 -> (a & 1)))
1218. (a <-> (1 -> (a & a)))
1219. (a <-> (1 -> (0 ˅ a)))
1220. (a <-> (1 -> (a ˅ 0)))
1221. (a <-> (1 -> (a ˅ a)))
1222. (a <-> (1 -> (1 -> a)))
1223. (a <-> (1 -> (1 <-> a)))
1224. (a <-> (1 -> (a <-> 1)))
1225. (a <-> ((¬ a) -> (¬ 1)))
1226. (a <-> ((a -> 0) -> 0))
1227. (a <-> ((a -> b) -> a))
1228. (a <-> ((0 <-> a) -> 0))
1229. (a <-> ((0 <-> a) -> a))
1230. (a <-> ((a <-> 0) -> 0))
1231. (a <-> ((a <-> 0) -> a))
1232. (a <-> (1 <-> (¬ (¬ a))))
1233. (a <-> (1 <-> (1 & a)))
1234. (a <-> (1 <-> (a & 1)))
1235. (a <-> (1 <-> (a & a)))
1236. (a <-> (1 <-> (0 ˅ a)))
1237. (a <-> (1 <-> (a ˅ 0)))
1238. (a <-> (1 <-> (a ˅ a)))
1239. (a <-> (1 <-> (1 -> a)))
1240. (a <-> (0 <-> (a -> 0)))
1241. (a <-> (b <-> (a <-> b)))
1242. (a <-> (b <-> (b <-> a)))
1243. (a <-> ((¬ 1) <-> (¬ a)))
1244. (a <-> ((¬ a) <-> (¬ 1)))
1245. (a <-> ((¬ (¬ a)) <-> 1))
1246. (a <-> ((1 & a) <-> 1))
1247. (a <-> ((a & 1) <-> 1))
1248. (a <-> ((a & a) <-> 1))
1249. (a <-> ((0 ˅ a) <-> 1))
1250. (a <-> ((a ˅ 0) <-> 1))
1251. (a <-> ((a ˅ a) <-> 1))
1252. (a <-> ((1 -> a) <-> 1))
1253. (a <-> ((a -> 0) <-> 0))
1254. (a <-> ((a <-> b) <-> b))
1255. (a <-> ((b <-> a) <-> b))
1256. ((¬ 1) <-> (a & (¬ 1)))
1257. ((¬ 1) <-> (a & (¬ a)))
1258. ((¬ 1) <-> ((¬ 1) & a))
1259. ((¬ 1) <-> ((¬ a) & a))
1260. ((¬ 1) <-> (a <-> (¬ a)))
1261. ((¬ 1) <-> ((¬ a) <-> a))
1262. ((¬ a) <-> (¬ (1 & a)))
1263. ((¬ a) <-> (¬ (a & 1)))
1264. ((¬ a) <-> (¬ (a & a)))
1265. ((¬ a) <-> (¬ (0 ˅ a)))
1266. ((¬ a) <-> (¬ (a ˅ 0)))
1267. ((¬ a) <-> (¬ (a ˅ a)))
1268. ((¬ a) <-> (¬ (1 -> a)))
1269. ((¬ a) <-> (¬ (1 <-> a)))
1270. ((¬ a) <-> (¬ (a <-> 1)))
1271. ((¬ a) <-> (a -> (¬ 1)))
1272. ((¬ a) <-> (a -> (¬ a)))
1273. ((¬ a) <-> (a <-> (¬ 1)))
1274. ((¬ a) <-> ((¬ 1) <-> a))
1275. ((¬ (¬ a)) <-> (1 & a))
1276. ((¬ (¬ a)) <-> (a & 1))
1277. ((¬ (¬ a)) <-> (a & a))
1278. ((¬ (¬ a)) <-> (0 ˅ a))
1279. ((¬ (¬ a)) <-> (a ˅ 0))
1280. ((¬ (¬ a)) <-> (a ˅ a))
1281. ((¬ (¬ a)) <-> (1 -> a))
1282. ((¬ (¬ a)) <-> (1 <-> a))
1283. ((¬ (¬ a)) <-> (a <-> 1))
1284. ((1 & a) <-> (¬ (¬ a)))
1285. ((1 & a) <-> (a & a))
1286. ((1 & a) <-> (0 ˅ a))
1287. ((1 & a) <-> (a ˅ 0))
1288. ((1 & a) <-> (a ˅ a))
1289. ((1 & a) <-> (1 -> a))
1290. ((1 & a) <-> (1 <-> a))
1291. ((1 & a) <-> (a <-> 1))
1292. ((0 & a) <-> (0 & b))
1293. ((0 & a) <-> (b & 0))
1294. ((0 & a) <-> (0 ˅ 0))
1295. ((0 & a) <-> (1 -> 0))
1296. ((0 & a) <-> (1 <-> 0))
1297. ((0 & a) <-> (0 <-> 1))
1298. ((a & 1) <-> (¬ (¬ a)))
1299. ((a & 1) <-> (a & a))
1300. ((a & 1) <-> (0 ˅ a))
1301. ((a & 1) <-> (a ˅ 0))
1302. ((a & 1) <-> (a ˅ a))
1303. ((a & 1) <-> (1 -> a))
1304. ((a & 1) <-> (1 <-> a))
1305. ((a & 1) <-> (a <-> 1))
1306. ((a & 0) <-> (0 & b))
1307. ((a & 0) <-> (b & 0))
1308. ((a & 0) <-> (0 ˅ 0))
1309. ((a & 0) <-> (1 -> 0))
1310. ((a & 0) <-> (1 <-> 0))
1311. ((a & 0) <-> (0 <-> 1))
1312. ((a & a) <-> (¬ (¬ a)))
1313. ((a & a) <-> (1 & a))
1314. ((a & a) <-> (a & 1))
1315. ((a & a) <-> (0 ˅ a))
1316. ((a & a) <-> (a ˅ 0))
1317. ((a & a) <-> (a ˅ a))
1318. ((a & a) <-> (1 -> a))
1319. ((a & a) <-> (1 <-> a))
1320. ((a & a) <-> (a <-> 1))
1321. ((a & b) <-> (b & a))
1322. ((0 ˅ 0) <-> (0 & a))
1323. ((0 ˅ 0) <-> (a & 0))
1324. ((0 ˅ a) <-> (¬ (¬ a)))
1325. ((0 ˅ a) <-> (1 & a))
1326. ((0 ˅ a) <-> (a & 1))
1327. ((0 ˅ a) <-> (a & a))
1328. ((0 ˅ a) <-> (a ˅ a))
1329. ((0 ˅ a) <-> (1 -> a))
1330. ((0 ˅ a) <-> (1 <-> a))
1331. ((0 ˅ a) <-> (a <-> 1))
1332. ((a ˅ 0) <-> (¬ (¬ a)))
1333. ((a ˅ 0) <-> (1 & a))
1334. ((a ˅ 0) <-> (a & 1))
1335. ((a ˅ 0) <-> (a & a))
1336. ((a ˅ 0) <-> (a ˅ a))
1337. ((a ˅ 0) <-> (1 -> a))
1338. ((a ˅ 0) <-> (1 <-> a))
1339. ((a ˅ 0) <-> (a <-> 1))
1340. ((a ˅ a) <-> (¬ (¬ a)))
1341. ((a ˅ a) <-> (1 & a))
1342. ((a ˅ a) <-> (a & 1))
1343. ((a ˅ a) <-> (a & a))
1344. ((a ˅ a) <-> (0 ˅ a))
1345. ((a ˅ a) <-> (a ˅ 0))
1346. ((a ˅ a) <-> (1 -> a))
1347. ((a ˅ a) <-> (1 <-> a))
1348. ((a ˅ a) <-> (a <-> 1))
1349. ((a ˅ b) <-> (b ˅ a))
1350. ((1 -> 0) <-> (0 & a))
1351. ((1 -> 0) <-> (a & 0))
1352. ((1 -> a) <-> (¬ (¬ a)))
1353. ((1 -> a) <-> (1 & a))
1354. ((1 -> a) <-> (a & 1))
1355. ((1 -> a) <-> (a & a))
1356. ((1 -> a) <-> (0 ˅ a))
1357. ((1 -> a) <-> (a ˅ 0))
1358. ((1 -> a) <-> (a ˅ a))
1359. ((1 -> a) <-> (1 <-> a))
1360. ((1 -> a) <-> (a <-> 1))
1361. ((a -> 0) <-> (0 <-> a))
1362. ((a -> 0) <-> (a <-> 0))
1363. ((1 <-> 0) <-> (0 & a))
1364. ((1 <-> 0) <-> (a & 0))
1365. ((1 <-> a) <-> (¬ (¬ a)))
1366. ((1 <-> a) <-> (1 & a))
1367. ((1 <-> a) <-> (a & 1))
1368. ((1 <-> a) <-> (a & a))
1369. ((1 <-> a) <-> (0 ˅ a))
1370. ((1 <-> a) <-> (a ˅ 0))
1371. ((1 <-> a) <-> (a ˅ a))
1372. ((1 <-> a) <-> (1 -> a))
1373. ((0 <-> 1) <-> (0 & a))
1374. ((0 <-> 1) <-> (a & 0))
1375. ((0 <-> a) <-> (a -> 0))
1376. ((a <-> 1) <-> (¬ (¬ a)))
1377. ((a <-> 1) <-> (1 & a))
1378. ((a <-> 1) <-> (a & 1))
1379. ((a <-> 1) <-> (a & a))
1380. ((a <-> 1) <-> (0 ˅ a))
1381. ((a <-> 1) <-> (a ˅ 0))
1382. ((a <-> 1) <-> (a ˅ a))
1383. ((a <-> 1) <-> (1 -> a))
1384. ((a <-> 0) <-> (a -> 0))
1385. ((a <-> b) <-> (b <-> a))
1386. ((¬ (1 & a)) <-> (¬ a))
1387. ((¬ (a & 1)) <-> (¬ a))
1388. ((¬ (a & a)) <-> (¬ a))
1389. ((¬ (0 ˅ a)) <-> (¬ a))
1390. ((¬ (a ˅ 0)) <-> (¬ a))
1391. ((¬ (a ˅ a)) <-> (¬ a))
1392. ((¬ (1 -> a)) <-> (¬ a))
1393. ((¬ (1 <-> a)) <-> (¬ a))
1394. ((¬ (a <-> 1)) <-> (¬ a))
1395. ((a & (¬ 1)) <-> (¬ 1))
1396. ((a & (¬ a)) <-> (¬ 1))
1397. (((¬ 1) & a) <-> (¬ 1))
1398. (((¬ a) & a) <-> (¬ 1))
1399. ((a -> (¬ 1)) <-> (¬ a))
1400. ((a -> (¬ a)) <-> (¬ a))
1401. ((a <-> (¬ 1)) <-> (¬ a))
1402. ((a <-> (¬ a)) <-> (¬ 1))
1403. (((¬ 1) <-> a) <-> (¬ a))
1404. (((¬ a) <-> a) <-> (¬ 1))
1405. ((¬ (¬ (¬ (¬ a)))) <-> a)
1406. ((¬ (¬ (1 & a))) <-> a)
1407. ((¬ (¬ (a & 1))) <-> a)
1408. ((¬ (¬ (a & a))) <-> a)
1409. ((¬ (¬ (0 ˅ a))) <-> a)
1410. ((¬ (¬ (a ˅ 0))) <-> a)
1411. ((¬ (¬ (a ˅ a))) <-> a)
1412. ((¬ (¬ (1 -> a))) <-> a)
1413. ((¬ (¬ (1 <-> a))) <-> a)
1414. ((¬ (¬ (a <-> 1))) <-> a)
1415. ((¬ (1 & (¬ a))) <-> a)
1416. ((¬ ((¬ a) & 1)) <-> a)
1417. ((¬ (0 ˅ (¬ a))) <-> a)
1418. ((¬ ((¬ a) ˅ 0)) <-> a)
1419. ((¬ (1 -> (¬ a))) <-> a)
1420. ((¬ (a -> (¬ 1))) <-> a)
1421. ((¬ (a -> (¬ a))) <-> a)
1422. ((¬ (1 <-> (¬ a))) <-> a)
1423. ((¬ (a <-> (¬ 1))) <-> a)
1424. ((¬ ((¬ 1) <-> a)) <-> a)
1425. ((¬ ((¬ a) <-> 1)) <-> a)
1426. ((1 & (¬ (¬ a))) <-> a)
1427. ((1 & (1 & a)) <-> a)
1428. ((1 & (a & 1)) <-> a)
1429. ((1 & (a & a)) <-> a)
1430. ((1 & (0 ˅ a)) <-> a)
1431. ((1 & (a ˅ 0)) <-> a)
1432. ((1 & (a ˅ a)) <-> a)
1433. ((1 & (1 -> a)) <-> a)
1434. ((1 & (1 <-> a)) <-> a)
1435. ((1 & (a <-> 1)) <-> a)
1436. ((a & (¬ (¬ a))) <-> a)
1437. ((a & (1 & a)) <-> a)
1438. ((a & (0 & b)) <-> 0)
1439. ((a & (a & 1)) <-> a)
1440. ((a & (a & a)) <-> a)
1441. ((a & (b & 0)) <-> 0)
1442. ((a & (0 ˅ 0)) <-> 0)
1443. ((a & (a ˅ b)) <-> a)
1444. ((a & (b ˅ a)) <-> a)
1445. ((a & (1 -> 0)) <-> 0)
1446. ((a & (a -> 0)) <-> 0)
1447. ((a & (b -> a)) <-> a)
1448. ((a & (1 <-> 0)) <-> 0)
1449. ((a & (1 <-> a)) <-> a)
1450. ((a & (0 <-> 1)) <-> 0)
1451. ((a & (0 <-> a)) <-> 0)
1452. ((a & (a <-> 1)) <-> a)
1453. ((a & (a <-> 0)) <-> 0)
1454. (((¬ (¬ a)) & 1) <-> a)
1455. (((¬ (¬ a)) & a) <-> a)
1456. (((1 & a) & 1) <-> a)
1457. (((1 & a) & a) <-> a)
1458. (((0 & a) & b) <-> 0)
1459. (((a & 1) & 1) <-> a)
1460. (((a & 1) & a) <-> a)
1461. (((a & 0) & b) <-> 0)
1462. (((a & a) & 1) <-> a)
1463. (((a & a) & a) <-> a)
1464. (((0 ˅ 0) & a) <-> 0)
1465. (((0 ˅ a) & 1) <-> a)
1466. (((a ˅ 0) & 1) <-> a)
1467. (((a ˅ a) & 1) <-> a)
1468. (((a ˅ b) & a) <-> a)
1469. (((a ˅ b) & b) <-> b)
1470. (((1 -> 0) & a) <-> 0)
1471. (((1 -> a) & 1) <-> a)
1472. (((a -> 0) & a) <-> 0)
1473. (((a -> b) & b) <-> b)
1474. (((1 <-> 0) & a) <-> 0)
1475. (((1 <-> a) & 1) <-> a)
1476. (((1 <-> a) & a) <-> a)
1477. (((0 <-> 1) & a) <-> 0)
1478. (((0 <-> a) & a) <-> 0)
1479. (((a <-> 1) & 1) <-> a)
1480. (((a <-> 1) & a) <-> a)
1481. (((a <-> 0) & a) <-> 0)
1482. ((0 ˅ (¬ (¬ a))) <-> a)
1483. ((0 ˅ (1 & a)) <-> a)
1484. ((0 ˅ (a & 1)) <-> a)
1485. ((0 ˅ (a & a)) <-> a)
1486. ((0 ˅ (0 ˅ a)) <-> a)
1487. ((0 ˅ (a ˅ 0)) <-> a)
1488. ((0 ˅ (a ˅ a)) <-> a)
1489. ((0 ˅ (1 -> a)) <-> a)
1490. ((0 ˅ (1 <-> a)) <-> a)
1491. ((0 ˅ (a <-> 1)) <-> a)
1492. ((a ˅ (¬ (¬ a))) <-> a)
1493. ((a ˅ (0 & b)) <-> a)
1494. ((a ˅ (a & b)) <-> a)
1495. ((a ˅ (b & 0)) <-> a)
1496. ((a ˅ (b & a)) <-> a)
1497. ((a ˅ (0 ˅ 0)) <-> a)
1498. ((a ˅ (0 ˅ a)) <-> a)
1499. ((a ˅ (a ˅ 0)) <-> a)
1500. ((a ˅ (a ˅ a)) <-> a)
1501. ((a ˅ (1 -> 0)) <-> a)
1502. ((a ˅ (1 -> a)) <-> a)
1503. ((a ˅ (1 <-> 0)) <-> a)
1504. ((a ˅ (1 <-> a)) <-> a)
1505. ((a ˅ (0 <-> 1)) <-> a)
1506. ((a ˅ (a <-> 1)) <-> a)
1507. (((¬ 1) ˅ (¬ 1)) <-> 0)
1508. (((¬ (¬ a)) ˅ 0) <-> a)
1509. (((¬ (¬ a)) ˅ a) <-> a)
1510. (((1 & a) ˅ 0) <-> a)
1511. (((0 & a) ˅ b) <-> b)
1512. (((a & 1) ˅ 0) <-> a)
1513. (((a & 0) ˅ b) <-> b)
1514. (((a & a) ˅ 0) <-> a)
1515. (((a & b) ˅ a) <-> a)
1516. (((a & b) ˅ b) <-> b)
1517. (((0 ˅ 0) ˅ a) <-> a)
1518. (((0 ˅ a) ˅ 0) <-> a)
1519. (((0 ˅ a) ˅ a) <-> a)
1520. (((a ˅ 0) ˅ 0) <-> a)
1521. (((a ˅ 0) ˅ a) <-> a)
1522. (((a ˅ a) ˅ 0) <-> a)
1523. (((a ˅ a) ˅ a) <-> a)
1524. (((1 -> 0) ˅ a) <-> a)
1525. (((1 -> a) ˅ 0) <-> a)
1526. (((1 -> a) ˅ a) <-> a)
1527. (((1 <-> 0) ˅ a) <-> a)
1528. (((1 <-> a) ˅ 0) <-> a)
1529. (((1 <-> a) ˅ a) <-> a)
1530. (((0 <-> 1) ˅ a) <-> a)
1531. (((a <-> 1) ˅ 0) <-> a)
1532. (((a <-> 1) ˅ a) <-> a)
1533. ((1 -> (¬ (¬ a))) <-> a)
1534. ((1 -> (1 & a)) <-> a)
1535. ((1 -> (0 & a)) <-> 0)
1536. ((1 -> (a & 1)) <-> a)
1537. ((1 -> (a & 0)) <-> 0)
1538. ((1 -> (a & a)) <-> a)
1539. ((1 -> (0 ˅ a)) <-> a)
1540. ((1 -> (a ˅ 0)) <-> a)
1541. ((1 -> (a ˅ a)) <-> a)
1542. ((1 -> (1 -> a)) <-> a)
1543. ((1 -> (1 <-> a)) <-> a)
1544. ((1 -> (a <-> 1)) <-> a)
1545. (((¬ a) -> (¬ 1)) <-> a)
1546. (((a -> 0) -> 0) <-> a)
1547. (((a -> b) -> a) <-> a)
1548. (((0 <-> a) -> 0) <-> a)
1549. (((0 <-> a) -> a) <-> a)
1550. (((a <-> 0) -> 0) <-> a)
1551. (((a <-> 0) -> a) <-> a)
1552. ((1 <-> (¬ (¬ a))) <-> a)
1553. ((1 <-> (1 & a)) <-> a)
1554. ((1 <-> (0 & a)) <-> 0)
1555. ((1 <-> (a & 1)) <-> a)
1556. ((1 <-> (a & 0)) <-> 0)
1557. ((1 <-> (a & a)) <-> a)
1558. ((1 <-> (0 ˅ a)) <-> a)
1559. ((1 <-> (a ˅ 0)) <-> a)
1560. ((1 <-> (a ˅ a)) <-> a)
1561. ((1 <-> (1 -> a)) <-> a)
1562. ((0 <-> (a -> 0)) <-> a)
1563. ((a <-> (a -> 0)) <-> 0)
1564. ((a <-> (a <-> b)) <-> b)
1565. ((a <-> (b <-> a)) <-> b)
1566. (((¬ 1) <-> (¬ a)) <-> a)
1567. (((¬ a) <-> (¬ 1)) <-> a)
1568. (((¬ (¬ a)) <-> 1) <-> a)
1569. (((1 & a) <-> 1) <-> a)
1570. (((0 & a) <-> 1) <-> 0)
1571. (((a & 1) <-> 1) <-> a)
1572. (((a & 0) <-> 1) <-> 0)
1573. (((a & a) <-> 1) <-> a)
1574. (((0 ˅ a) <-> 1) <-> a)
1575. (((a ˅ 0) <-> 1) <-> a)
1576. (((a ˅ a) <-> 1) <-> a)
1577. (((1 -> a) <-> 1) <-> a)
1578. (((a -> 0) <-> 0) <-> a)
1579. (((a -> 0) <-> a) <-> 0)
1580. (((a <-> b) <-> a) <-> b)
1581. (((a <-> b) <-> b) <-> a)

|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|