Kazimir Majorinc's Blog (currently not in use): October 2009

One Hundred Propositional Tautologies (5)

The same like last post, but this time 1500 tautologies, and
these are in the infix form. It is very easy to change prefix
into infix in Newlisp. And vice versa - same function can be
used for changing infix to prefix. But, tautologies are great.

(set 'infix<->prefix 
  (lambda(L)
    (cond ((symbol? L) L)
          ((= (length L) 2) (map infix<->prefix L))
          ((= (length L) 3) (let((L1 (map infix<->prefix L)))
                                (list (nth 1 L1) (nth 0 L1) (nth 2 L1)))))))

Generated 1005725 formulas.
Filtered to 187105 tautologies in T1.
Filtered to 2730 tautologies in T2.
Filtered to 1581 tautologies in T3 and 1149 tautologies in M3.

*** T3 ***

1. true
2. (not false)
3. (not (not true))
4. (true and true)
5. (true or a)
6. (a or true)
7. (false -> a)
8. (a -> true)
9. (a -> a)
10. (a <-> a)
11. (not (false and a))
12. (not (a and false))
13. (not (false or false))
14. (not (true -> false))
15. (not (true <-> false))
16. (not (false <-> true))
17. (a or (not a))
18. ((not a) or a)
19. ((not true) -> a)
20. (false <-> (not true))
21. ((not true) <-> false)
22. (not (a and (not true)))
23. (not (a and (not a)))
24. (not ((not true) and a))
25. (not ((not a) and a))
26. (not (false or (not true)))
27. (not ((not true) or false))
28. (not (true -> (not true)))
29. (not (a <-> (not a)))
30. (not ((not a) <-> a))
31. (a or (a -> b))
32. (a or (false <-> a))
33. (a or (a <-> false))
34. ((a -> b) or a)
35. ((false <-> a) or a)
36. ((a <-> false) or a)
37. (a -> (not (not a)))
38. (a -> (true and a))
39. (a -> (a and true))
40. (a -> (a and a))
41. (a -> (a or b))
42. (a -> (b or a))
43. (a -> (b -> a))
44. (a -> (true <-> a))
45. (a -> (a <-> true))
46. ((not (not a)) -> a)
47. ((false and a) -> b)
48. ((a and false) -> b)
49. ((a and b) -> a)
50. ((a and b) -> b)
51. ((false or false) -> a)
52. ((false or a) -> a)
53. ((a or false) -> a)
54. ((a or a) -> a)
55. ((true -> false) -> a)
56. ((true -> a) -> a)
57. ((true <-> false) -> a)
58. ((true <-> a) -> a)
59. ((false <-> true) -> a)
60. ((a <-> true) -> a)
61. (false <-> (false and a))
62. (false <-> (a and false))
63. (a <-> (not (not a)))
64. (a <-> (true and a))
65. (a <-> (a and true))
66. (a <-> (a and a))
67. (a <-> (false or a))
68. (a <-> (a or false))
69. (a <-> (a or a))
70. (a <-> (true -> a))
71. (a <-> (true <-> a))
72. (a <-> (a <-> true))
73. ((not (not a)) <-> a)
74. ((true and a) <-> a)
75. ((false and a) <-> false)
76. ((a and true) <-> a)
77. ((a and false) <-> false)
78. ((a and a) <-> a)
79. ((false or a) <-> a)
80. ((a or false) <-> a)
81. ((a or a) <-> a)
82. ((true -> a) <-> a)
83. ((true <-> a) <-> a)
84. ((a <-> true) <-> a)
85. (not (a and (false and b)))
86. (not (a and (b and false)))
87. (not (a and (false or false)))
88. (not (a and (true -> false)))
89. (not (a and (a -> false)))
90. (not (a and (true <-> false)))
91. (not (a and (false <-> true)))
92. (not (a and (false <-> a)))
93. (not (a and (a <-> false)))
94. (not ((false and a) and b))
95. (not ((a and false) and b))
96. (not ((false or false) and a))
97. (not ((true -> false) and a))
98. (not ((a -> false) and a))
99. (not ((true <-> false) and a))
100. (not ((false <-> true) and a))
101. (not ((false <-> a) and a))
102. (not ((a <-> false) and a))
103. (not (false or (false and a)))
104. (not (false or (a and false)))
105. (not (false or (false or false)))
106. (not (false or (true -> false)))
107. (not (false or (true <-> false)))
108. (not (false or (false <-> true)))
109. (not ((not true) or (not true)))
110. (not ((false and a) or false))
111. (not ((a and false) or false))
112. (not ((false or false) or false))
113. (not ((true -> false) or false))
114. (not ((true <-> false) or false))
115. (not ((false <-> true) or false))
116. (not (true -> (false and a)))
117. (not (true -> (a and false)))
118. (not (true -> (false or false)))
119. (not (true -> (true -> false)))
120. (not (true -> (true <-> false)))
121. (not (true -> (false <-> true)))
122. (not (true <-> (false and a)))
123. (not (true <-> (a and false)))
124. (not (true <-> (false or false)))
125. (not (a <-> (a -> false)))
126. (not (a <-> (false <-> a)))
127. (not (a <-> (a <-> false)))
128. (not ((false and a) <-> true))
129. (not ((a and false) <-> true))
130. (not ((false or false) <-> true))
131. (not ((a -> false) <-> a))
132. (not ((false <-> a) <-> a))
133. (not ((a <-> false) <-> a))
134. (a or (not (not (not a))))
135. (a or (not (a and b)))
136. (a or (not (b and a)))
137. (a or (not (false or a)))
138. (a or (not (a or false)))
139. (a or (not (a or a)))
140. (a or (not (true -> a)))
141. (a or (not (true <-> a)))
142. (a or (not (a <-> true)))
143. (a or (true and (not a)))
144. (a or ((not a) and true))
145. (a or (b or (not a)))
146. (a or ((not a) or b))
147. (a or (b -> (not a)))
148. (a or (true <-> (not a)))
149. (a or (a <-> (not true)))
150. (a or ((not true) <-> a))
151. (a or ((not a) <-> true))
152. ((not a) or (true and a))
153. ((not a) or (a and true))
154. ((not a) or (a and a))
155. ((not a) or (a or b))
156. ((not a) or (b or a))
157. ((not a) or (b -> a))
158. ((not a) or (true <-> a))
159. ((not a) or (a <-> true))
160. ((true and a) or (not a))
161. ((a and true) or (not a))
162. ((a and a) or (not a))
163. ((a or b) or (not a))
164. ((a or b) or (not b))
165. ((a -> b) or (not b))
166. ((true <-> a) or (not a))
167. ((a <-> true) or (not a))
168. ((not (not (not a))) or a)
169. ((not (a and b)) or a)
170. ((not (a and b)) or b)
171. ((not (false or a)) or a)
172. ((not (a or false)) or a)
173. ((not (a or a)) or a)
174. ((not (true -> a)) or a)
175. ((not (true <-> a)) or a)
176. ((not (a <-> true)) or a)
177. ((true and (not a)) or a)
178. (((not a) and true) or a)
179. ((a or (not b)) or b)
180. (((not a) or b) or a)
181. ((a -> (not b)) or b)
182. ((true <-> (not a)) or a)
183. ((a <-> (not true)) or a)
184. (((not true) <-> a) or a)
185. (((not a) <-> true) or a)
186. (a -> (not (a -> false)))
187. (a -> (not (false <-> a)))
188. (a -> (not (a <-> false)))
189. (a -> ((not a) -> b))
190. (a -> (false <-> (not a)))
191. (a -> ((not a) <-> false))
192. ((not a) -> (a -> b))
193. ((not a) -> (false <-> a))
194. ((not a) -> (a <-> false))
195. ((a -> false) -> (not a))
196. ((false <-> a) -> (not a))
197. ((a <-> false) -> (not a))
198. ((not (a -> b)) -> a)
199. ((not (false <-> a)) -> a)
200. ((not (a <-> false)) -> a)
201. ((a and (not true)) -> b)
202. ((a and (not a)) -> b)
203. (((not true) and a) -> b)
204. (((not a) and a) -> b)
205. ((false or (not true)) -> a)
206. ((a or (not true)) -> a)
207. (((not true) or false) -> a)
208. (((not true) or a) -> a)
209. ((true -> (not true)) -> a)
210. (((not a) -> false) -> a)
211. (((not a) -> a) -> a)
212. ((false <-> (not a)) -> a)
213. ((a <-> (not a)) -> b)
214. (((not a) <-> false) -> a)
215. (((not a) <-> a) -> b)
216. (false <-> (a and (not true)))
217. (false <-> (a and (not a)))
218. (false <-> ((not true) and a))
219. (false <-> ((not a) and a))
220. (false <-> (true -> (not true)))
221. (false <-> (a <-> (not a)))
222. (false <-> ((not a) <-> a))
223. (a <-> (not (a -> false)))
224. (a <-> (not (false <-> a)))
225. (a <-> (not (a <-> false)))
226. (a <-> (a or (not true)))
227. (a <-> ((not true) or a))
228. (a <-> ((not a) -> false))
229. (a <-> ((not a) -> a))
230. (a <-> (false <-> (not a)))
231. (a <-> ((not a) <-> false))
232. ((not true) <-> (false and a))
233. ((not true) <-> (a and false))
234. ((not true) <-> (false or false))
235. ((not a) <-> (a -> false))
236. ((not a) <-> (false <-> a))
237. ((not a) <-> (a <-> false))
238. ((false and a) <-> (not true))
239. ((a and false) <-> (not true))
240. ((false or false) <-> (not true))
241. ((a -> false) <-> (not a))
242. ((false <-> a) <-> (not a))
243. ((a <-> false) <-> (not a))
244. ((not (a -> false)) <-> a)
245. ((not (false <-> a)) <-> a)
246. ((not (a <-> false)) <-> a)
247. ((a and (not true)) <-> false)
248. ((a and (not a)) <-> false)
249. (((not true) and a) <-> false)
250. (((not a) and a) <-> false)
251. ((a or (not true)) <-> a)
252. (((not true) or a) <-> a)
253. ((true -> (not true)) <-> false)
254. (((not a) -> false) <-> a)
255. (((not a) -> a) <-> a)
256. ((false <-> (not a)) <-> a)
257. ((a <-> (not a)) <-> false)
258. (((not a) <-> false) <-> a)
259. (((not a) <-> a) <-> false)
260. (not (a and (not (not (not a)))))
261. (not (a and (not (true and a))))
262. (not (a and (not (a and true))))
263. (not (a and (not (a and a))))
264. (not (a and (not (a or b))))
265. (not (a and (not (b or a))))
266. (not (a and (not (b -> a))))
267. (not (a and (not (true <-> a))))
268. (not (a and (not (a <-> true))))
269. (not (a and (b and (not true))))
270. (not (a and (b and (not a))))
271. (not (a and (b and (not b))))
272. (not (a and ((not true) and b)))
273. (not (a and ((not a) and b)))
274. (not (a and ((not b) and b)))
275. (not (a and (false or (not true))))
276. (not (a and (false or (not a))))
277. (not (a and ((not true) or false)))
278. (not (a and ((not a) or false)))
279. (not (a and (true -> (not true))))
280. (not (a and (true -> (not a))))
281. (not (a and (a -> (not true))))
282. (not (a and (a -> (not a))))
283. (not (a and (true <-> (not a))))
284. (not (a and (a <-> (not true))))
285. (not (a and (b <-> (not b))))
286. (not (a and ((not true) <-> a)))
287. (not (a and ((not a) <-> true)))
288. (not (a and ((not b) <-> b)))
289. (not ((not a) and (a and b)))
290. (not ((not a) and (b and a)))
291. (not ((not a) and (false or a)))
292. (not ((not a) and (a or false)))
293. (not ((not a) and (a or a)))
294. (not ((not a) and (true -> a)))
295. (not ((not a) and (true <-> a)))
296. (not ((not a) and (a <-> true)))
297. (not ((a and b) and (not a)))
298. (not ((a and b) and (not b)))
299. (not ((false or a) and (not a)))
300. (not ((a or false) and (not a)))
301. (not ((a or a) and (not a)))
302. (not ((true -> a) and (not a)))
303. (not ((true <-> a) and (not a)))
304. (not ((a <-> true) and (not a)))
305. (not ((not (not (not a))) and a))
306. (not ((not (true and a)) and a))
307. (not ((not (a and true)) and a))
308. (not ((not (a and a)) and a))
309. (not ((not (a or b)) and a))
310. (not ((not (a or b)) and b))
311. (not ((not (a -> b)) and b))
312. (not ((not (true <-> a)) and a))
313. (not ((not (a <-> true)) and a))
314. (not ((a and (not true)) and b))
315. (not ((a and (not a)) and b))
316. (not ((a and (not b)) and b))
317. (not (((not true) and a) and b))
318. (not (((not a) and a) and b))
319. (not (((not a) and b) and a))
320. (not ((false or (not true)) and a))
321. (not ((false or (not a)) and a))
322. (not (((not true) or false) and a))
323. (not (((not a) or false) and a))
324. (not ((true -> (not true)) and a))
325. (not ((true -> (not a)) and a))
326. (not ((a -> (not true)) and a))
327. (not ((a -> (not a)) and a))
328. (not ((true <-> (not a)) and a))
329. (not ((a <-> (not true)) and a))
330. (not ((a <-> (not a)) and b))
331. (not (((not true) <-> a) and a))
332. (not (((not a) <-> true) and a))
333. (not (((not a) <-> a) and b))
334. (not (false or (a and (not true))))
335. (not (false or (a and (not a))))
336. (not (false or ((not true) and a)))
337. (not (false or ((not a) and a)))
338. (not (false or (false or (not true))))
339. (not (false or ((not true) or false)))
340. (not (false or (true -> (not true))))
341. (not (false or (a <-> (not a))))
342. (not (false or ((not a) <-> a)))
343. (not ((not true) or (false and a)))
344. (not ((not true) or (a and false)))
345. (not ((not true) or (false or false)))
346. (not ((not true) or (true -> false)))
347. (not ((not true) or (true <-> false)))
348. (not ((not true) or (false <-> true)))
349. (not ((false and a) or (not true)))
350. (not ((a and false) or (not true)))
351. (not ((false or false) or (not true)))
352. (not ((true -> false) or (not true)))
353. (not ((true <-> false) or (not true)))
354. (not ((false <-> true) or (not true)))
355. (not ((a and (not true)) or false))
356. (not ((a and (not a)) or false))
357. (not (((not true) and a) or false))
358. (not (((not a) and a) or false))
359. (not ((false or (not true)) or false))
360. (not (((not true) or false) or false))
361. (not ((true -> (not true)) or false))
362. (not ((a <-> (not a)) or false))
363. (not (((not a) <-> a) or false))
364. (not (true -> (a and (not true))))
365. (not (true -> (a and (not a))))
366. (not (true -> ((not true) and a)))
367. (not (true -> ((not a) and a)))
368. (not (true -> (false or (not true))))
369. (not (true -> ((not true) or false)))
370. (not (true -> (true -> (not true))))
371. (not (true -> (a <-> (not a))))
372. (not (true -> ((not a) <-> a)))
373. (not (true <-> (a and (not true))))
374. (not (true <-> (a and (not a))))
375. (not (true <-> ((not true) and a)))
376. (not (true <-> ((not a) and a)))
377. (not (true <-> (a <-> (not a))))
378. (not (true <-> ((not a) <-> a)))
379. (not (a <-> (not (not (not a)))))
380. (not (a <-> (not (true and a))))
381. (not (a <-> (not (a and true))))
382. (not (a <-> (not (a and a))))
383. (not (a <-> (not (false or a))))
384. (not (a <-> (not (a or false))))
385. (not (a <-> (not (a or a))))
386. (not (a <-> (not (true -> a))))
387. (not (a <-> (not (true <-> a))))
388. (not (a <-> (not (a <-> true))))
389. (not (a <-> (true and (not a))))
390. (not (a <-> ((not a) and true)))
391. (not (a <-> (false or (not a))))
392. (not (a <-> ((not a) or false)))
393. (not (a <-> (true -> (not a))))
394. (not (a <-> (a -> (not true))))
395. (not (a <-> (a -> (not a))))
396. (not (a <-> (true <-> (not a))))
397. (not (a <-> (a <-> (not true))))
398. (not (a <-> ((not true) <-> a)))
399. (not (a <-> ((not a) <-> true)))
400. (not ((not a) <-> (true and a)))

401. (not ((not a) <-> (a and true)))
402. (not ((not a) <-> (a and a)))
403. (not ((not a) <-> (false or a)))
404. (not ((not a) <-> (a or false)))
405. (not ((not a) <-> (a or a)))
406. (not ((not a) <-> (true -> a)))
407. (not ((not a) <-> (true <-> a)))
408. (not ((not a) <-> (a <-> true)))
409. (not ((true and a) <-> (not a)))
410. (not ((a and true) <-> (not a)))
411. (not ((a and a) <-> (not a)))
412. (not ((false or a) <-> (not a)))
413. (not ((a or false) <-> (not a)))
414. (not ((a or a) <-> (not a)))
415. (not ((true -> a) <-> (not a)))
416. (not ((true <-> a) <-> (not a)))
417. (not ((a <-> true) <-> (not a)))
418. (not ((not (not (not a))) <-> a))
419. (not ((not (true and a)) <-> a))
420. (not ((not (a and true)) <-> a))
421. (not ((not (a and a)) <-> a))
422. (not ((not (false or a)) <-> a))
423. (not ((not (a or false)) <-> a))
424. (not ((not (a or a)) <-> a))
425. (not ((not (true -> a)) <-> a))
426. (not ((not (true <-> a)) <-> a))
427. (not ((not (a <-> true)) <-> a))
428. (not ((true and (not a)) <-> a))
429. (not ((a and (not true)) <-> true))
430. (not ((a and (not a)) <-> true))
431. (not (((not true) and a) <-> true))
432. (not (((not a) and true) <-> a))
433. (not (((not a) and a) <-> true))
434. (not ((false or (not a)) <-> a))
435. (not (((not a) or false) <-> a))
436. (not ((true -> (not a)) <-> a))
437. (not ((a -> (not true)) <-> a))
438. (not ((a -> (not a)) <-> a))
439. (not ((true <-> (not a)) <-> a))
440. (not ((a <-> (not true)) <-> a))
441. (not ((a <-> (not a)) <-> true))
442. (not (((not true) <-> a) <-> a))
443. (not (((not a) <-> true) <-> a))
444. (not (((not a) <-> a) <-> true))
445. (a or (not (not (a -> b))))
446. (a or (not (not (false <-> a))))
447. (a or (not (not (a <-> false))))
448. (a or (not (a or (not true))))
449. (a or (not ((not true) or a)))
450. (a or (not ((not a) -> false)))
451. (a or (not ((not a) -> a)))
452. (a or (not (false <-> (not a))))
453. (a or (not ((not a) <-> false)))
454. (a or (true and (a -> b)))
455. (a or (true and (false <-> a)))
456. (a or (true and (a <-> false)))
457. (a or ((not a) and (not a)))
458. (a or ((a -> b) and true))
459. (a or ((false <-> a) and true))
460. (a or ((a <-> false) and true))
461. (a or (b or (a -> c)))
462. (a or (b or (false <-> a)))
463. (a or (b or (a <-> false)))
464. (a or (b or (a <-> b)))
465. (a or (b or (b <-> a)))
466. (a or ((a -> b) or c))
467. (a or ((false <-> a) or b))
468. (a or ((a <-> false) or b))
469. (a or ((a <-> b) or b))
470. (a or ((b <-> a) or b))
471. (a or (b -> (a -> c)))
472. (a or (b -> (false <-> a)))
473. (a or (b -> (a <-> false)))
474. (a or ((not (not a)) -> b))
475. (a or ((a and b) -> c))
476. (a or ((b and a) -> c))
477. (a or ((false or a) -> b))
478. (a or ((a or false) -> b))
479. (a or ((a or a) -> b))
480. (a or ((a or b) -> b))
481. (a or ((b or a) -> b))
482. (a or ((true -> a) -> b))
483. (a or ((true <-> a) -> b))
484. (a or ((a <-> true) -> b))
485. (a or (true <-> (a -> b)))
486. (a or (true <-> (false <-> a)))
487. (a or (true <-> (a <-> false)))
488. (a or (false <-> (not (not a))))
489. (a or (false <-> (a and b)))
490. (a or (false <-> (b and a)))
491. (a or (false <-> (a or a)))
492. (a or (false <-> (true -> a)))
493. (a or (false <-> (true <-> a)))
494. (a or (false <-> (a <-> true)))
495. (a or (a <-> (false and b)))
496. (a or (a <-> (a and b)))
497. (a or (a <-> (b and false)))
498. (a or (a <-> (b and a)))
499. (a or (a <-> (false or false)))
500. (a or (a <-> (true -> false)))
501. (a or (a <-> (true <-> false)))
502. (a or (a <-> (false <-> true)))
503. (a or (b <-> (a or b)))
504. (a or (b <-> (b or a)))
505. (a or ((not (not a)) <-> false))
506. (a or ((false and b) <-> a))
507. (a or ((a and b) <-> false))
508. (a or ((a and b) <-> a))
509. (a or ((b and false) <-> a))
510. (a or ((b and a) <-> false))
511. (a or ((b and a) <-> a))
512. (a or ((false or false) <-> a))
513. (a or ((a or a) <-> false))
514. (a or ((a or b) <-> b))
515. (a or ((b or a) <-> b))
516. (a or ((true -> false) <-> a))
517. (a or ((true -> a) <-> false))
518. (a or ((a -> b) <-> true))
519. (a or ((true <-> false) <-> a))
520. (a or ((true <-> a) <-> false))
521. (a or ((false <-> true) <-> a))
522. (a or ((false <-> a) <-> true))
523. (a or ((a <-> true) <-> false))
524. (a or ((a <-> false) <-> true))
525. ((not a) or (not (a -> false)))
526. ((not a) or (not (false <-> a)))
527. ((not a) or (not (a <-> false)))
528. ((not (not a)) or (a -> b))
529. ((not (not a)) or (false <-> a))
530. ((not (not a)) or (a <-> false))
531. ((true and a) or (a -> b))
532. ((true and a) or (false <-> a))
533. ((true and a) or (a <-> false))
534. ((a and true) or (a -> b))
535. ((a and true) or (false <-> a))
536. ((a and true) or (a <-> false))
537. ((a and a) or (a -> b))
538. ((a and a) or (false <-> a))
539. ((a and a) or (a <-> false))
540. ((a or b) or (a -> c))
541. ((a or b) or (b -> c))
542. ((a or b) or (false <-> a))
543. ((a or b) or (false <-> b))
544. ((a or b) or (a <-> false))
545. ((a or b) or (a <-> b))
546. ((a or b) or (b <-> false))
547. ((a or b) or (b <-> a))
548. ((a -> b) or (not (not a)))
549. ((a -> b) or (true and a))
550. ((a -> b) or (a and true))
551. ((a -> b) or (a and a))
552. ((a -> b) or (a or c))
553. ((a -> b) or (c or a))
554. ((a -> b) or (b -> c))
555. ((a -> b) or (c -> a))
556. ((a -> b) or (true <-> a))
557. ((a -> b) or (false <-> b))
558. ((a -> b) or (a <-> true))
559. ((a -> b) or (b <-> false))
560. ((true <-> a) or (a -> b))
561. ((true <-> a) or (false <-> a))
562. ((true <-> a) or (a <-> false))
563. ((false <-> a) or (not (not a)))
564. ((false <-> a) or (true and a))
565. ((false <-> a) or (a and true))
566. ((false <-> a) or (a and a))
567. ((false <-> a) or (a or b))
568. ((false <-> a) or (b or a))
569. ((false <-> a) or (b -> a))
570. ((false <-> a) or (true <-> a))
571. ((false <-> a) or (a <-> true))
572. ((a <-> true) or (a -> b))
573. ((a <-> true) or (false <-> a))
574. ((a <-> true) or (a <-> false))
575. ((a <-> false) or (not (not a)))
576. ((a <-> false) or (true and a))
577. ((a <-> false) or (a and true))
578. ((a <-> false) or (a and a))
579. ((a <-> false) or (a or b))
580. ((a <-> false) or (b or a))
581. ((a <-> false) or (b -> a))
582. ((a <-> false) or (true <-> a))
583. ((a <-> false) or (a <-> true))
584. ((a <-> b) or (a or b))
585. ((a <-> b) or (b or a))
586. ((not (a -> false)) or (not a))
587. ((not (false <-> a)) or (not a))
588. ((not (a <-> false)) or (not a))
589. ((not (not (a -> b))) or a)
590. ((not (not (false <-> a))) or a)
591. ((not (not (a <-> false))) or a)
592. ((not (a or (not true))) or a)
593. ((not ((not true) or a)) or a)
594. ((not ((not a) -> false)) or a)
595. ((not ((not a) -> a)) or a)
596. ((not (false <-> (not a))) or a)
597. ((not ((not a) <-> false)) or a)
598. ((true and (a -> b)) or a)
599. ((true and (false <-> a)) or a)
600. ((true and (a <-> false)) or a)
601. (((not a) and (not a)) or a)
602. (((a -> b) and true) or a)
603. (((false <-> a) and true) or a)
604. (((a <-> false) and true) or a)
605. ((a or (b -> c)) or b)
606. ((a or (false <-> b)) or b)
607. ((a or (a <-> b)) or b)
608. ((a or (b <-> false)) or b)
609. ((a or (b <-> a)) or b)
610. (((a -> b) or c) or a)
611. (((false <-> a) or b) or a)
612. (((a <-> false) or b) or a)
613. (((a <-> b) or a) or b)
614. (((a <-> b) or b) or a)
615. ((a -> (b -> c)) or b)
616. ((a -> (false <-> b)) or b)
617. ((a -> (b <-> false)) or b)
618. (((not (not a)) -> b) or a)
619. (((a and b) -> c) or a)
620. (((a and b) -> c) or b)
621. (((false or a) -> b) or a)
622. (((a or false) -> b) or a)
623. (((a or a) -> b) or a)
624. (((a or b) -> a) or b)
625. (((a or b) -> b) or a)
626. (((true -> a) -> b) or a)
627. (((true <-> a) -> b) or a)
628. (((a <-> true) -> b) or a)
629. ((true <-> (a -> b)) or a)
630. ((true <-> (false <-> a)) or a)
631. ((true <-> (a <-> false)) or a)
632. ((false <-> (not (not a))) or a)
633. ((false <-> (a and b)) or a)
634. ((false <-> (a and b)) or b)
635. ((false <-> (a or a)) or a)
636. ((false <-> (true -> a)) or a)
637. ((false <-> (true <-> a)) or a)
638. ((false <-> (a <-> true)) or a)
639. ((a <-> (false and b)) or a)
640. ((a <-> (a and b)) or a)
641. ((a <-> (b and false)) or a)
642. ((a <-> (b and a)) or a)
643. ((a <-> (false or false)) or a)
644. ((a <-> (a or b)) or b)
645. ((a <-> (b or a)) or b)
646. ((a <-> (true -> false)) or a)
647. ((a <-> (true <-> false)) or a)
648. ((a <-> (false <-> true)) or a)
649. (((not (not a)) <-> false) or a)
650. (((false and a) <-> b) or b)
651. (((a and false) <-> b) or b)
652. (((a and b) <-> false) or a)
653. (((a and b) <-> false) or b)
654. (((a and b) <-> a) or a)
655. (((a and b) <-> b) or b)
656. (((false or false) <-> a) or a)
657. (((a or a) <-> false) or a)
658. (((a or b) <-> a) or b)
659. (((a or b) <-> b) or a)
660. (((true -> false) <-> a) or a)
661. (((true -> a) <-> false) or a)
662. (((a -> b) <-> true) or a)
663. (((true <-> false) <-> a) or a)
664. (((true <-> a) <-> false) or a)
665. (((false <-> true) <-> a) or a)
666. (((false <-> a) <-> true) or a)
667. (((a <-> true) <-> false) or a)
668. (((a <-> false) <-> true) or a)
669. (a -> (not (not (not (not a)))))
670. (a -> (not (not (true and a))))
671. (a -> (not (not (a and true))))
672. (a -> (not (not (a and a))))
673. (a -> (not (not (a or b))))
674. (a -> (not (not (b or a))))
675. (a -> (not (not (b -> a))))
676. (a -> (not (not (true <-> a))))
677. (a -> (not (not (a <-> true))))
678. (a -> (not (b and (not a))))
679. (a -> (not ((not a) and b)))
680. (a -> (not (false or (not a))))
681. (a -> (not ((not a) or false)))
682. (a -> (not (true -> (not a))))
683. (a -> (not (a -> (not true))))
684. (a -> (not (a -> (not a))))
685. (a -> (not (true <-> (not a))))
686. (a -> (not (a <-> (not true))))
687. (a -> (not ((not true) <-> a)))
688. (a -> (not ((not a) <-> true)))
689. (a -> (true and (not (not a))))
690. (a -> (true and (true and a)))
691. (a -> (true and (a and true)))
692. (a -> (true and (a and a)))
693. (a -> (true and (a or b)))
694. (a -> (true and (b or a)))
695. (a -> (true and (b -> a)))
696. (a -> (true and (true <-> a)))
697. (a -> (true and (a <-> true)))
698. (a -> (a and (not (not a))))
699. (a -> (a and (true and a)))
700. (a -> (a and (a and true)))
701. (a -> (a and (a and a)))
702. (a -> (a and (a or b)))
703. (a -> (a and (b or a)))
704. (a -> (a and (b -> a)))
705. (a -> (a and (true <-> a)))
706. (a -> (a and (a <-> true)))
707. (a -> ((not (not a)) and true))
708. (a -> ((not (not a)) and a))
709. (a -> ((true and a) and true))
710. (a -> ((true and a) and a))
711. (a -> ((a and true) and true))
712. (a -> ((a and true) and a))
713. (a -> ((a and a) and true))
714. (a -> ((a and a) and a))
715. (a -> ((a or b) and true))
716. (a -> ((a or b) and a))
717. (a -> ((b or a) and true))
718. (a -> ((b or a) and a))
719. (a -> ((b -> a) and true))
720. (a -> ((b -> a) and a))
721. (a -> ((true <-> a) and true))
722. (a -> ((true <-> a) and a))
723. (a -> ((a <-> true) and true))
724. (a -> ((a <-> true) and a))
725. (a -> (b or (not (not a))))
726. (a -> (b or (true and a)))
727. (a -> (b or (a and true)))
728. (a -> (b or (a and a)))
729. (a -> (b or (a or c)))
730. (a -> (b or (c or a)))
731. (a -> (b or (c -> a)))
732. (a -> (b or (true <-> a)))
733. (a -> (b or (a <-> true)))
734. (a -> ((not (not a)) or b))
735. (a -> ((true and a) or b))
736. (a -> ((a and true) or b))
737. (a -> ((a and a) or b))
738. (a -> ((a or b) or c))
739. (a -> ((b or a) or c))
740. (a -> ((b -> a) or c))
741. (a -> ((true <-> a) or b))
742. (a -> ((a <-> true) or b))
743. (a -> (b -> (not (not a))))
744. (a -> (b -> (true and a)))
745. (a -> (b -> (a and true)))
746. (a -> (b -> (a and a)))
747. (a -> (b -> (a and b)))
748. (a -> (b -> (b and a)))
749. (a -> (b -> (a or c)))
750. (a -> (b -> (c or a)))
751. (a -> (b -> (c -> a)))
752. (a -> (b -> (true <-> a)))
753. (a -> (b -> (a <-> true)))
754. (a -> (b -> (a <-> b)))
755. (a -> (b -> (b <-> a)))
756. (a -> ((a -> false) -> b))
757. (a -> ((a -> b) -> b))
758. (a -> ((false <-> a) -> b))
759. (a -> ((a <-> false) -> b))
760. (a -> ((a <-> b) -> b))
761. (a -> ((b <-> a) -> b))
762. (a -> (true <-> (not (not a))))
763. (a -> (true <-> (a and a)))
764. (a -> (true <-> (a or b)))
765. (a -> (true <-> (b or a)))
766. (a -> (true <-> (b -> a)))
767. (a -> (a <-> (a or b)))
768. (a -> (a <-> (b or a)))
769. (a -> (a <-> (b -> a)))
770. (a -> (b <-> (a and b)))
771. (a -> (b <-> (b and a)))
772. (a -> (b <-> (a -> b)))
773. (a -> (b <-> (a <-> b)))
774. (a -> (b <-> (b <-> a)))
775. (a -> ((not true) <-> (not a)))
776. (a -> ((not a) <-> (not true)))
777. (a -> ((not (not a)) <-> true))
778. (a -> ((a and a) <-> true))
779. (a -> ((a and b) <-> b))
780. (a -> ((b and a) <-> b))
781. (a -> ((a or b) <-> true))
782. (a -> ((a or b) <-> a))
783. (a -> ((b or a) <-> true))
784. (a -> ((b or a) <-> a))
785. (a -> ((a -> b) <-> b))
786. (a -> ((b -> a) <-> true))
787. (a -> ((b -> a) <-> a))
788. (a -> ((a <-> b) <-> b))
789. (a -> ((b <-> a) <-> b))
790. ((not a) -> (not (a and b)))
791. ((not a) -> (not (b and a)))
792. ((not a) -> (not (false or a)))
793. ((not a) -> (not (a or false)))
794. ((not a) -> (not (a or a)))
795. ((not a) -> (not (true -> a)))
796. ((not a) -> (not (true <-> a)))
797. ((not a) -> (not (a <-> true)))
798. ((not a) -> (a <-> (not true)))
799. ((not a) -> ((not true) <-> a))
800. ((not (not a)) -> (true and a))

801. ((not (not a)) -> (a and true))
802. ((not (not a)) -> (a and a))
803. ((not (not a)) -> (a or b))
804. ((not (not a)) -> (b or a))
805. ((not (not a)) -> (b -> a))
806. ((not (not a)) -> (true <-> a))
807. ((not (not a)) -> (a <-> true))
808. ((a and b) -> (not (not a)))
809. ((a and b) -> (not (not b)))
810. ((a and b) -> (true and a))
811. ((a and b) -> (true and b))
812. ((a and b) -> (a and true))
813. ((a and b) -> (a and a))
814. ((a and b) -> (b and true))
815. ((a and b) -> (b and a))
816. ((a and b) -> (b and b))
817. ((a and b) -> (a or c))
818. ((a and b) -> (b or c))
819. ((a and b) -> (c or a))
820. ((a and b) -> (c or b))
821. ((a and b) -> (c -> a))
822. ((a and b) -> (c -> b))
823. ((a and b) -> (true <-> a))
824. ((a and b) -> (true <-> b))
825. ((a and b) -> (a <-> true))
826. ((a and b) -> (a <-> b))
827. ((a and b) -> (b <-> true))
828. ((a and b) -> (b <-> a))
829. ((false or a) -> (not (not a)))
830. ((false or a) -> (true and a))
831. ((false or a) -> (a and true))
832. ((false or a) -> (a and a))
833. ((false or a) -> (a or b))
834. ((false or a) -> (b or a))
835. ((false or a) -> (b -> a))
836. ((false or a) -> (true <-> a))
837. ((false or a) -> (a <-> true))
838. ((a or false) -> (not (not a)))
839. ((a or false) -> (true and a))
840. ((a or false) -> (a and true))
841. ((a or false) -> (a and a))
842. ((a or false) -> (a or b))
843. ((a or false) -> (b or a))
844. ((a or false) -> (b -> a))
845. ((a or false) -> (true <-> a))
846. ((a or false) -> (a <-> true))
847. ((a or a) -> (not (not a)))
848. ((a or a) -> (true and a))
849. ((a or a) -> (a and true))
850. ((a or a) -> (a and a))
851. ((a or a) -> (a or b))
852. ((a or a) -> (b or a))
853. ((a or a) -> (b -> a))
854. ((a or a) -> (true <-> a))
855. ((a or a) -> (a <-> true))
856. ((a or b) -> (b or a))
857. ((true -> a) -> (not (not a)))
858. ((true -> a) -> (true and a))
859. ((true -> a) -> (a and true))
860. ((true -> a) -> (a and a))
861. ((true -> a) -> (a or b))
862. ((true -> a) -> (b or a))
863. ((true -> a) -> (b -> a))
864. ((true -> a) -> (true <-> a))
865. ((true -> a) -> (a <-> true))
866. ((a -> false) -> (a -> b))
867. ((a -> false) -> (false <-> a))
868. ((a -> false) -> (a <-> false))
869. ((true <-> a) -> (not (not a)))
870. ((true <-> a) -> (true and a))
871. ((true <-> a) -> (a and true))
872. ((true <-> a) -> (a and a))
873. ((true <-> a) -> (a or b))
874. ((true <-> a) -> (b or a))
875. ((true <-> a) -> (b -> a))
876. ((false <-> a) -> (a -> b))
877. ((a <-> true) -> (not (not a)))
878. ((a <-> true) -> (true and a))
879. ((a <-> true) -> (a and true))
880. ((a <-> true) -> (a and a))
881. ((a <-> true) -> (a or b))
882. ((a <-> true) -> (b or a))
883. ((a <-> true) -> (b -> a))
884. ((a <-> false) -> (a -> b))
885. ((a <-> b) -> (a -> b))
886. ((a <-> b) -> (b -> a))
887. ((a <-> b) -> (b <-> a))
888. ((not (true and a)) -> (not a))
889. ((not (a and true)) -> (not a))
890. ((not (a and a)) -> (not a))
891. ((not (a or b)) -> (not a))
892. ((not (a or b)) -> (not b))
893. ((not (a -> b)) -> (not b))
894. ((not (true <-> a)) -> (not a))
895. ((not (a <-> true)) -> (not a))
896. ((a -> (not true)) -> (not a))
897. ((a -> (not a)) -> (not a))
898. ((a <-> (not true)) -> (not a))
899. (((not true) <-> a) -> (not a))
900. ((not (not (not (not a)))) -> a)
901. ((not (not (a and b))) -> a)
902. ((not (not (a and b))) -> b)
903. ((not (not (false or a))) -> a)
904. ((not (not (a or false))) -> a)
905. ((not (not (a or a))) -> a)
906. ((not (not (true -> a))) -> a)
907. ((not (not (true <-> a))) -> a)
908. ((not (not (a <-> true))) -> a)
909. ((not (true and (not a))) -> a)
910. ((not ((not a) and true)) -> a)
911. ((not (a or (not b))) -> b)
912. ((not ((not a) or b)) -> a)
913. ((not (a -> (not b))) -> b)
914. ((not (true <-> (not a))) -> a)
915. ((not (a <-> (not true))) -> a)
916. ((not ((not true) <-> a)) -> a)
917. ((not ((not a) <-> true)) -> a)
918. ((a and (not (not b))) -> b)
919. ((a and (false and b)) -> c)
920. ((a and (b and false)) -> c)
921. ((a and (b and c)) -> b)
922. ((a and (b and c)) -> c)
923. ((a and (false or false)) -> b)
924. ((a and (false or b)) -> b)
925. ((a and (b or false)) -> b)
926. ((a and (b or b)) -> b)
927. ((a and (true -> false)) -> b)
928. ((a and (true -> b)) -> b)
929. ((a and (a -> false)) -> b)
930. ((a and (a -> b)) -> b)
931. ((a and (true <-> false)) -> b)
932. ((a and (true <-> b)) -> b)
933. ((a and (false <-> true)) -> b)
934. ((a and (false <-> a)) -> b)
935. ((a and (a <-> false)) -> b)
936. ((a and (a <-> b)) -> b)
937. ((a and (b <-> true)) -> b)
938. ((a and (b <-> a)) -> b)
939. (((not (not a)) and b) -> a)
940. (((false and a) and b) -> c)
941. (((a and false) and b) -> c)
942. (((a and b) and c) -> a)
943. (((a and b) and c) -> b)
944. (((false or false) and a) -> b)
945. (((false or a) and b) -> a)
946. (((a or false) and b) -> a)
947. (((a or a) and b) -> a)
948. (((true -> false) and a) -> b)
949. (((true -> a) and b) -> a)
950. (((a -> false) and a) -> b)
951. (((a -> b) and a) -> b)
952. (((true <-> false) and a) -> b)
953. (((true <-> a) and b) -> a)
954. (((false <-> true) and a) -> b)
955. (((false <-> a) and a) -> b)
956. (((a <-> true) and b) -> a)
957. (((a <-> false) and a) -> b)
958. (((a <-> b) and a) -> b)
959. (((a <-> b) and b) -> a)
960. ((false or (not (not a))) -> a)
961. ((false or (false and a)) -> b)
962. ((false or (a and false)) -> b)
963. ((false or (a and b)) -> a)
964. ((false or (a and b)) -> b)
965. ((false or (false or false)) -> a)
966. ((false or (false or a)) -> a)
967. ((false or (a or false)) -> a)
968. ((false or (a or a)) -> a)
969. ((false or (true -> false)) -> a)
970. ((false or (true -> a)) -> a)
971. ((false or (true <-> false)) -> a)
972. ((false or (true <-> a)) -> a)
973. ((false or (false <-> true)) -> a)
974. ((false or (a <-> true)) -> a)
975. ((a or (not (not a))) -> a)
976. ((a or (false and b)) -> a)
977. ((a or (a and b)) -> a)
978. ((a or (b and false)) -> a)
979. ((a or (b and a)) -> a)
980. ((a or (false or false)) -> a)
981. ((a or (false or a)) -> a)
982. ((a or (a or false)) -> a)
983. ((a or (a or a)) -> a)
984. ((a or (true -> false)) -> a)
985. ((a or (true -> a)) -> a)
986. ((a or (true <-> false)) -> a)
987. ((a or (true <-> a)) -> a)
988. ((a or (false <-> true)) -> a)
989. ((a or (a <-> true)) -> a)
990. (((not true) or (not true)) -> a)
991. (((not (not a)) or false) -> a)
992. (((not (not a)) or a) -> a)
993. (((false and a) or false) -> b)
994. (((false and a) or b) -> b)
995. (((a and false) or false) -> b)
996. (((a and false) or b) -> b)
997. (((a and b) or false) -> a)
998. (((a and b) or false) -> b)
999. (((a and b) or a) -> a)
1000. (((a and b) or b) -> b)
1001. (((false or false) or false) -> a)
1002. (((false or false) or a) -> a)
1003. (((false or a) or false) -> a)
1004. (((false or a) or a) -> a)
1005. (((a or false) or false) -> a)
1006. (((a or false) or a) -> a)
1007. (((a or a) or false) -> a)
1008. (((a or a) or a) -> a)
1009. (((true -> false) or false) -> a)
1010. (((true -> false) or a) -> a)
1011. (((true -> a) or false) -> a)
1012. (((true -> a) or a) -> a)
1013. (((true <-> false) or false) -> a)
1014. (((true <-> false) or a) -> a)
1015. (((true <-> a) or false) -> a)
1016. (((true <-> a) or a) -> a)
1017. (((false <-> true) or false) -> a)
1018. (((false <-> true) or a) -> a)
1019. (((a <-> true) or false) -> a)
1020. (((a <-> true) or a) -> a)
1021. ((true -> (not (not a))) -> a)
1022. ((true -> (false and a)) -> b)
1023. ((true -> (a and false)) -> b)
1024. ((true -> (a and b)) -> a)
1025. ((true -> (a and b)) -> b)
1026. ((true -> (false or false)) -> a)
1027. ((true -> (false or a)) -> a)
1028. ((true -> (a or false)) -> a)
1029. ((true -> (a or a)) -> a)
1030. ((true -> (true -> false)) -> a)
1031. ((true -> (true -> a)) -> a)
1032. ((true -> (true <-> false)) -> a)
1033. ((true -> (true <-> a)) -> a)
1034. ((true -> (false <-> true)) -> a)
1035. ((true -> (a <-> true)) -> a)
1036. (((not a) -> (not true)) -> a)
1037. (((a -> b) -> false) -> a)
1038. (((a -> b) -> a) -> a)
1039. (((false <-> a) -> false) -> a)
1040. (((false <-> a) -> a) -> a)
1041. (((a <-> false) -> false) -> a)
1042. (((a <-> false) -> a) -> a)
1043. ((true <-> (not (not a))) -> a)
1044. ((true <-> (false and a)) -> b)
1045. ((true <-> (a and false)) -> b)
1046. ((true <-> (a and b)) -> a)
1047. ((true <-> (a and b)) -> b)
1048. ((true <-> (false or false)) -> a)
1049. ((true <-> (false or a)) -> a)
1050. ((true <-> (a or false)) -> a)
1051. ((true <-> (a or a)) -> a)
1052. ((false <-> (a -> b)) -> a)
1053. ((a <-> (a -> false)) -> b)
1054. ((a <-> (a -> b)) -> a)
1055. ((a <-> (a -> b)) -> b)
1056. ((a <-> (false <-> a)) -> b)
1057. ((a <-> (a <-> false)) -> b)
1058. ((a <-> (a <-> b)) -> b)
1059. ((a <-> (b <-> a)) -> b)
1060. (((not true) <-> (not a)) -> a)
1061. (((not a) <-> (not true)) -> a)
1062. (((not (not a)) <-> true) -> a)
1063. (((false and a) <-> true) -> b)
1064. (((a and false) <-> true) -> b)
1065. (((a and b) <-> true) -> a)
1066. (((a and b) <-> true) -> b)
1067. (((false or false) <-> true) -> a)
1068. (((false or a) <-> true) -> a)
1069. (((a or false) <-> true) -> a)
1070. (((a or a) <-> true) -> a)
1071. (((a -> false) <-> a) -> b)
1072. (((a -> b) <-> false) -> a)
1073. (((a -> b) <-> a) -> a)
1074. (((a -> b) <-> a) -> b)
1075. (((false <-> a) <-> a) -> b)
1076. (((a <-> false) <-> a) -> b)
1077. (((a <-> b) <-> a) -> b)
1078. (((a <-> b) <-> b) -> a)
1079. (false <-> (a and (false and b)))
1080. (false <-> (a and (b and false)))
1081. (false <-> (a and (false or false)))
1082. (false <-> (a and (true -> false)))
1083. (false <-> (a and (a -> false)))
1084. (false <-> (a and (true <-> false)))
1085. (false <-> (a and (false <-> true)))
1086. (false <-> (a and (false <-> a)))
1087. (false <-> (a and (a <-> false)))
1088. (false <-> ((false and a) and b))
1089. (false <-> ((a and false) and b))
1090. (false <-> ((false or false) and a))
1091. (false <-> ((true -> false) and a))
1092. (false <-> ((a -> false) and a))
1093. (false <-> ((true <-> false) and a))
1094. (false <-> ((false <-> true) and a))
1095. (false <-> ((false <-> a) and a))
1096. (false <-> ((a <-> false) and a))
1097. (false <-> ((not true) or (not true)))
1098. (false <-> (true -> (false and a)))
1099. (false <-> (true -> (a and false)))
1100. (false <-> (true <-> (false and a)))
1101. (false <-> (true <-> (a and false)))
1102. (false <-> (a <-> (a -> false)))
1103. (false <-> ((false and a) <-> true))
1104. (false <-> ((a and false) <-> true))
1105. (false <-> ((a -> false) <-> a))
1106. (a <-> (not (not (not (not a)))))
1107. (a <-> (not (not (true and a))))
1108. (a <-> (not (not (a and true))))
1109. (a <-> (not (not (a and a))))
1110. (a <-> (not (not (false or a))))
1111. (a <-> (not (not (a or false))))
1112. (a <-> (not (not (a or a))))
1113. (a <-> (not (not (true -> a))))
1114. (a <-> (not (not (true <-> a))))
1115. (a <-> (not (not (a <-> true))))
1116. (a <-> (not (true and (not a))))
1117. (a <-> (not ((not a) and true)))
1118. (a <-> (not (false or (not a))))
1119. (a <-> (not ((not a) or false)))
1120. (a <-> (not (true -> (not a))))
1121. (a <-> (not (a -> (not true))))
1122. (a <-> (not (a -> (not a))))
1123. (a <-> (not (true <-> (not a))))
1124. (a <-> (not (a <-> (not true))))
1125. (a <-> (not ((not true) <-> a)))
1126. (a <-> (not ((not a) <-> true)))
1127. (a <-> (true and (not (not a))))
1128. (a <-> (true and (true and a)))
1129. (a <-> (true and (a and true)))
1130. (a <-> (true and (a and a)))
1131. (a <-> (true and (false or a)))
1132. (a <-> (true and (a or false)))
1133. (a <-> (true and (a or a)))
1134. (a <-> (true and (true -> a)))
1135. (a <-> (true and (true <-> a)))
1136. (a <-> (true and (a <-> true)))
1137. (a <-> (a and (not (not a))))
1138. (a <-> (a and (true and a)))
1139. (a <-> (a and (a and true)))
1140. (a <-> (a and (a and a)))
1141. (a <-> (a and (a or b)))
1142. (a <-> (a and (b or a)))
1143. (a <-> (a and (b -> a)))
1144. (a <-> (a and (true <-> a)))
1145. (a <-> (a and (a <-> true)))
1146. (a <-> ((not (not a)) and true))
1147. (a <-> ((not (not a)) and a))
1148. (a <-> ((true and a) and true))
1149. (a <-> ((true and a) and a))
1150. (a <-> ((a and true) and true))
1151. (a <-> ((a and true) and a))
1152. (a <-> ((a and a) and true))
1153. (a <-> ((a and a) and a))
1154. (a <-> ((false or a) and true))
1155. (a <-> ((a or false) and true))
1156. (a <-> ((a or a) and true))
1157. (a <-> ((a or b) and a))
1158. (a <-> ((b or a) and a))
1159. (a <-> ((true -> a) and true))
1160. (a <-> ((b -> a) and a))
1161. (a <-> ((true <-> a) and true))
1162. (a <-> ((true <-> a) and a))
1163. (a <-> ((a <-> true) and true))
1164. (a <-> ((a <-> true) and a))
1165. (a <-> (false or (not (not a))))
1166. (a <-> (false or (true and a)))
1167. (a <-> (false or (a and true)))
1168. (a <-> (false or (a and a)))
1169. (a <-> (false or (false or a)))
1170. (a <-> (false or (a or false)))
1171. (a <-> (false or (a or a)))
1172. (a <-> (false or (true -> a)))
1173. (a <-> (false or (true <-> a)))
1174. (a <-> (false or (a <-> true)))
1175. (a <-> (a or (not (not a))))
1176. (a <-> (a or (false and b)))
1177. (a <-> (a or (a and b)))
1178. (a <-> (a or (b and false)))
1179. (a <-> (a or (b and a)))
1180. (a <-> (a or (false or false)))
1181. (a <-> (a or (false or a)))
1182. (a <-> (a or (a or false)))
1183. (a <-> (a or (a or a)))
1184. (a <-> (a or (true -> false)))
1185. (a <-> (a or (true -> a)))
1186. (a <-> (a or (true <-> false)))
1187. (a <-> (a or (true <-> a)))
1188. (a <-> (a or (false <-> true)))
1189. (a <-> (a or (a <-> true)))
1190. (a <-> ((not (not a)) or false))
1191. (a <-> ((not (not a)) or a))
1192. (a <-> ((true and a) or false))
1193. (a <-> ((false and b) or a))
1194. (a <-> ((a and true) or false))
1195. (a <-> ((a and a) or false))
1196. (a <-> ((a and b) or a))
1197. (a <-> ((b and false) or a))
1198. (a <-> ((b and a) or a))
1199. (a <-> ((false or false) or a))
1200. (a <-> ((false or a) or false))

1201. (a <-> ((false or a) or a))
1202. (a <-> ((a or false) or false))
1203. (a <-> ((a or false) or a))
1204. (a <-> ((a or a) or false))
1205. (a <-> ((a or a) or a))
1206. (a <-> ((true -> false) or a))
1207. (a <-> ((true -> a) or false))
1208. (a <-> ((true -> a) or a))
1209. (a <-> ((true <-> false) or a))
1210. (a <-> ((true <-> a) or false))
1211. (a <-> ((true <-> a) or a))
1212. (a <-> ((false <-> true) or a))
1213. (a <-> ((a <-> true) or false))
1214. (a <-> ((a <-> true) or a))
1215. (a <-> (true -> (not (not a))))
1216. (a <-> (true -> (true and a)))
1217. (a <-> (true -> (a and true)))
1218. (a <-> (true -> (a and a)))
1219. (a <-> (true -> (false or a)))
1220. (a <-> (true -> (a or false)))
1221. (a <-> (true -> (a or a)))
1222. (a <-> (true -> (true -> a)))
1223. (a <-> (true -> (true <-> a)))
1224. (a <-> (true -> (a <-> true)))
1225. (a <-> ((not a) -> (not true)))
1226. (a <-> ((a -> false) -> false))
1227. (a <-> ((a -> b) -> a))
1228. (a <-> ((false <-> a) -> false))
1229. (a <-> ((false <-> a) -> a))
1230. (a <-> ((a <-> false) -> false))
1231. (a <-> ((a <-> false) -> a))
1232. (a <-> (true <-> (not (not a))))
1233. (a <-> (true <-> (true and a)))
1234. (a <-> (true <-> (a and true)))
1235. (a <-> (true <-> (a and a)))
1236. (a <-> (true <-> (false or a)))
1237. (a <-> (true <-> (a or false)))
1238. (a <-> (true <-> (a or a)))
1239. (a <-> (true <-> (true -> a)))
1240. (a <-> (false <-> (a -> false)))
1241. (a <-> (b <-> (a <-> b)))
1242. (a <-> (b <-> (b <-> a)))
1243. (a <-> ((not true) <-> (not a)))
1244. (a <-> ((not a) <-> (not true)))
1245. (a <-> ((not (not a)) <-> true))
1246. (a <-> ((true and a) <-> true))
1247. (a <-> ((a and true) <-> true))
1248. (a <-> ((a and a) <-> true))
1249. (a <-> ((false or a) <-> true))
1250. (a <-> ((a or false) <-> true))
1251. (a <-> ((a or a) <-> true))
1252. (a <-> ((true -> a) <-> true))
1253. (a <-> ((a -> false) <-> false))
1254. (a <-> ((a <-> b) <-> b))
1255. (a <-> ((b <-> a) <-> b))
1256. ((not true) <-> (a and (not true)))
1257. ((not true) <-> (a and (not a)))
1258. ((not true) <-> ((not true) and a))
1259. ((not true) <-> ((not a) and a))
1260. ((not true) <-> (a <-> (not a)))
1261. ((not true) <-> ((not a) <-> a))
1262. ((not a) <-> (not (true and a)))
1263. ((not a) <-> (not (a and true)))
1264. ((not a) <-> (not (a and a)))
1265. ((not a) <-> (not (false or a)))
1266. ((not a) <-> (not (a or false)))
1267. ((not a) <-> (not (a or a)))
1268. ((not a) <-> (not (true -> a)))
1269. ((not a) <-> (not (true <-> a)))
1270. ((not a) <-> (not (a <-> true)))
1271. ((not a) <-> (a -> (not true)))
1272. ((not a) <-> (a -> (not a)))
1273. ((not a) <-> (a <-> (not true)))
1274. ((not a) <-> ((not true) <-> a))
1275. ((not (not a)) <-> (true and a))
1276. ((not (not a)) <-> (a and true))
1277. ((not (not a)) <-> (a and a))
1278. ((not (not a)) <-> (false or a))
1279. ((not (not a)) <-> (a or false))
1280. ((not (not a)) <-> (a or a))
1281. ((not (not a)) <-> (true -> a))
1282. ((not (not a)) <-> (true <-> a))
1283. ((not (not a)) <-> (a <-> true))
1284. ((true and a) <-> (not (not a)))
1285. ((true and a) <-> (a and a))
1286. ((true and a) <-> (false or a))
1287. ((true and a) <-> (a or false))
1288. ((true and a) <-> (a or a))
1289. ((true and a) <-> (true -> a))
1290. ((true and a) <-> (true <-> a))
1291. ((true and a) <-> (a <-> true))
1292. ((false and a) <-> (false and b))
1293. ((false and a) <-> (b and false))
1294. ((false and a) <-> (false or false))
1295. ((false and a) <-> (true -> false))
1296. ((false and a) <-> (true <-> false))
1297. ((false and a) <-> (false <-> true))
1298. ((a and true) <-> (not (not a)))
1299. ((a and true) <-> (a and a))
1300. ((a and true) <-> (false or a))
1301. ((a and true) <-> (a or false))
1302. ((a and true) <-> (a or a))
1303. ((a and true) <-> (true -> a))
1304. ((a and true) <-> (true <-> a))
1305. ((a and true) <-> (a <-> true))
1306. ((a and false) <-> (false and b))
1307. ((a and false) <-> (b and false))
1308. ((a and false) <-> (false or false))
1309. ((a and false) <-> (true -> false))
1310. ((a and false) <-> (true <-> false))
1311. ((a and false) <-> (false <-> true))
1312. ((a and a) <-> (not (not a)))
1313. ((a and a) <-> (true and a))
1314. ((a and a) <-> (a and true))
1315. ((a and a) <-> (false or a))
1316. ((a and a) <-> (a or false))
1317. ((a and a) <-> (a or a))
1318. ((a and a) <-> (true -> a))
1319. ((a and a) <-> (true <-> a))
1320. ((a and a) <-> (a <-> true))
1321. ((a and b) <-> (b and a))
1322. ((false or false) <-> (false and a))
1323. ((false or false) <-> (a and false))
1324. ((false or a) <-> (not (not a)))
1325. ((false or a) <-> (true and a))
1326. ((false or a) <-> (a and true))
1327. ((false or a) <-> (a and a))
1328. ((false or a) <-> (a or a))
1329. ((false or a) <-> (true -> a))
1330. ((false or a) <-> (true <-> a))
1331. ((false or a) <-> (a <-> true))
1332. ((a or false) <-> (not (not a)))
1333. ((a or false) <-> (true and a))
1334. ((a or false) <-> (a and true))
1335. ((a or false) <-> (a and a))
1336. ((a or false) <-> (a or a))
1337. ((a or false) <-> (true -> a))
1338. ((a or false) <-> (true <-> a))
1339. ((a or false) <-> (a <-> true))
1340. ((a or a) <-> (not (not a)))
1341. ((a or a) <-> (true and a))
1342. ((a or a) <-> (a and true))
1343. ((a or a) <-> (a and a))
1344. ((a or a) <-> (false or a))
1345. ((a or a) <-> (a or false))
1346. ((a or a) <-> (true -> a))
1347. ((a or a) <-> (true <-> a))
1348. ((a or a) <-> (a <-> true))
1349. ((a or b) <-> (b or a))
1350. ((true -> false) <-> (false and a))
1351. ((true -> false) <-> (a and false))
1352. ((true -> a) <-> (not (not a)))
1353. ((true -> a) <-> (true and a))
1354. ((true -> a) <-> (a and true))
1355. ((true -> a) <-> (a and a))
1356. ((true -> a) <-> (false or a))
1357. ((true -> a) <-> (a or false))
1358. ((true -> a) <-> (a or a))
1359. ((true -> a) <-> (true <-> a))
1360. ((true -> a) <-> (a <-> true))
1361. ((a -> false) <-> (false <-> a))
1362. ((a -> false) <-> (a <-> false))
1363. ((true <-> false) <-> (false and a))
1364. ((true <-> false) <-> (a and false))
1365. ((true <-> a) <-> (not (not a)))
1366. ((true <-> a) <-> (true and a))
1367. ((true <-> a) <-> (a and true))
1368. ((true <-> a) <-> (a and a))
1369. ((true <-> a) <-> (false or a))
1370. ((true <-> a) <-> (a or false))
1371. ((true <-> a) <-> (a or a))
1372. ((true <-> a) <-> (true -> a))
1373. ((false <-> true) <-> (false and a))
1374. ((false <-> true) <-> (a and false))
1375. ((false <-> a) <-> (a -> false))
1376. ((a <-> true) <-> (not (not a)))
1377. ((a <-> true) <-> (true and a))
1378. ((a <-> true) <-> (a and true))
1379. ((a <-> true) <-> (a and a))
1380. ((a <-> true) <-> (false or a))
1381. ((a <-> true) <-> (a or false))
1382. ((a <-> true) <-> (a or a))
1383. ((a <-> true) <-> (true -> a))
1384. ((a <-> false) <-> (a -> false))
1385. ((a <-> b) <-> (b <-> a))
1386. ((not (true and a)) <-> (not a))
1387. ((not (a and true)) <-> (not a))
1388. ((not (a and a)) <-> (not a))
1389. ((not (false or a)) <-> (not a))
1390. ((not (a or false)) <-> (not a))
1391. ((not (a or a)) <-> (not a))
1392. ((not (true -> a)) <-> (not a))
1393. ((not (true <-> a)) <-> (not a))
1394. ((not (a <-> true)) <-> (not a))
1395. ((a and (not true)) <-> (not true))
1396. ((a and (not a)) <-> (not true))
1397. (((not true) and a) <-> (not true))
1398. (((not a) and a) <-> (not true))
1399. ((a -> (not true)) <-> (not a))
1400. ((a -> (not a)) <-> (not a))
1401. ((a <-> (not true)) <-> (not a))
1402. ((a <-> (not a)) <-> (not true))
1403. (((not true) <-> a) <-> (not a))
1404. (((not a) <-> a) <-> (not true))
1405. ((not (not (not (not a)))) <-> a)
1406. ((not (not (true and a))) <-> a)
1407. ((not (not (a and true))) <-> a)
1408. ((not (not (a and a))) <-> a)
1409. ((not (not (false or a))) <-> a)
1410. ((not (not (a or false))) <-> a)
1411. ((not (not (a or a))) <-> a)
1412. ((not (not (true -> a))) <-> a)
1413. ((not (not (true <-> a))) <-> a)
1414. ((not (not (a <-> true))) <-> a)
1415. ((not (true and (not a))) <-> a)
1416. ((not ((not a) and true)) <-> a)
1417. ((not (false or (not a))) <-> a)
1418. ((not ((not a) or false)) <-> a)
1419. ((not (true -> (not a))) <-> a)
1420. ((not (a -> (not true))) <-> a)
1421. ((not (a -> (not a))) <-> a)
1422. ((not (true <-> (not a))) <-> a)
1423. ((not (a <-> (not true))) <-> a)
1424. ((not ((not true) <-> a)) <-> a)
1425. ((not ((not a) <-> true)) <-> a)
1426. ((true and (not (not a))) <-> a)
1427. ((true and (true and a)) <-> a)
1428. ((true and (a and true)) <-> a)
1429. ((true and (a and a)) <-> a)
1430. ((true and (false or a)) <-> a)
1431. ((true and (a or false)) <-> a)
1432. ((true and (a or a)) <-> a)
1433. ((true and (true -> a)) <-> a)
1434. ((true and (true <-> a)) <-> a)
1435. ((true and (a <-> true)) <-> a)
1436. ((a and (not (not a))) <-> a)
1437. ((a and (true and a)) <-> a)
1438. ((a and (false and b)) <-> false)
1439. ((a and (a and true)) <-> a)
1440. ((a and (a and a)) <-> a)
1441. ((a and (b and false)) <-> false)
1442. ((a and (false or false)) <-> false)
1443. ((a and (a or b)) <-> a)
1444. ((a and (b or a)) <-> a)
1445. ((a and (true -> false)) <-> false)
1446. ((a and (a -> false)) <-> false)
1447. ((a and (b -> a)) <-> a)
1448. ((a and (true <-> false)) <-> false)
1449. ((a and (true <-> a)) <-> a)
1450. ((a and (false <-> true)) <-> false)
1451. ((a and (false <-> a)) <-> false)
1452. ((a and (a <-> true)) <-> a)
1453. ((a and (a <-> false)) <-> false)
1454. (((not (not a)) and true) <-> a)
1455. (((not (not a)) and a) <-> a)
1456. (((true and a) and true) <-> a)
1457. (((true and a) and a) <-> a)
1458. (((false and a) and b) <-> false)
1459. (((a and true) and true) <-> a)
1460. (((a and true) and a) <-> a)
1461. (((a and false) and b) <-> false)
1462. (((a and a) and true) <-> a)
1463. (((a and a) and a) <-> a)
1464. (((false or false) and a) <-> false)
1465. (((false or a) and true) <-> a)
1466. (((a or false) and true) <-> a)
1467. (((a or a) and true) <-> a)
1468. (((a or b) and a) <-> a)
1469. (((a or b) and b) <-> b)
1470. (((true -> false) and a) <-> false)
1471. (((true -> a) and true) <-> a)
1472. (((a -> false) and a) <-> false)
1473. (((a -> b) and b) <-> b)
1474. (((true <-> false) and a) <-> false)
1475. (((true <-> a) and true) <-> a)
1476. (((true <-> a) and a) <-> a)
1477. (((false <-> true) and a) <-> false)
1478. (((false <-> a) and a) <-> false)
1479. (((a <-> true) and true) <-> a)
1480. (((a <-> true) and a) <-> a)
1481. (((a <-> false) and a) <-> false)
1482. ((false or (not (not a))) <-> a)
1483. ((false or (true and a)) <-> a)
1484. ((false or (a and true)) <-> a)
1485. ((false or (a and a)) <-> a)
1486. ((false or (false or a)) <-> a)
1487. ((false or (a or false)) <-> a)
1488. ((false or (a or a)) <-> a)
1489. ((false or (true -> a)) <-> a)
1490. ((false or (true <-> a)) <-> a)
1491. ((false or (a <-> true)) <-> a)
1492. ((a or (not (not a))) <-> a)
1493. ((a or (false and b)) <-> a)
1494. ((a or (a and b)) <-> a)
1495. ((a or (b and false)) <-> a)
1496. ((a or (b and a)) <-> a)
1497. ((a or (false or false)) <-> a)
1498. ((a or (false or a)) <-> a)
1499. ((a or (a or false)) <-> a)
1500. ((a or (a or a)) <-> a)
1501. ((a or (true -> false)) <-> a)
1502. ((a or (true -> a)) <-> a)
1503. ((a or (true <-> false)) <-> a)
1504. ((a or (true <-> a)) <-> a)
1505. ((a or (false <-> true)) <-> a)
1506. ((a or (a <-> true)) <-> a)
1507. (((not true) or (not true)) <-> false)
1508. (((not (not a)) or false) <-> a)
1509. (((not (not a)) or a) <-> a)
1510. (((true and a) or false) <-> a)
1511. (((false and a) or b) <-> b)
1512. (((a and true) or false) <-> a)
1513. (((a and false) or b) <-> b)
1514. (((a and a) or false) <-> a)
1515. (((a and b) or a) <-> a)
1516. (((a and b) or b) <-> b)
1517. (((false or false) or a) <-> a)
1518. (((false or a) or false) <-> a)
1519. (((false or a) or a) <-> a)
1520. (((a or false) or false) <-> a)
1521. (((a or false) or a) <-> a)
1522. (((a or a) or false) <-> a)
1523. (((a or a) or a) <-> a)
1524. (((true -> false) or a) <-> a)
1525. (((true -> a) or false) <-> a)
1526. (((true -> a) or a) <-> a)
1527. (((true <-> false) or a) <-> a)
1528. (((true <-> a) or false) <-> a)
1529. (((true <-> a) or a) <-> a)
1530. (((false <-> true) or a) <-> a)
1531. (((a <-> true) or false) <-> a)
1532. (((a <-> true) or a) <-> a)
1533. ((true -> (not (not a))) <-> a)
1534. ((true -> (true and a)) <-> a)
1535. ((true -> (false and a)) <-> false)
1536. ((true -> (a and true)) <-> a)
1537. ((true -> (a and false)) <-> false)
1538. ((true -> (a and a)) <-> a)
1539. ((true -> (false or a)) <-> a)
1540. ((true -> (a or false)) <-> a)
1541. ((true -> (a or a)) <-> a)
1542. ((true -> (true -> a)) <-> a)
1543. ((true -> (true <-> a)) <-> a)
1544. ((true -> (a <-> true)) <-> a)
1545. (((not a) -> (not true)) <-> a)
1546. (((a -> false) -> false) <-> a)
1547. (((a -> b) -> a) <-> a)
1548. (((false <-> a) -> false) <-> a)
1549. (((false <-> a) -> a) <-> a)
1550. (((a <-> false) -> false) <-> a)
1551. (((a <-> false) -> a) <-> a)
1552. ((true <-> (not (not a))) <-> a)
1553. ((true <-> (true and a)) <-> a)
1554. ((true <-> (false and a)) <-> false)
1555. ((true <-> (a and true)) <-> a)
1556. ((true <-> (a and false)) <-> false)
1557. ((true <-> (a and a)) <-> a)
1558. ((true <-> (false or a)) <-> a)
1559. ((true <-> (a or false)) <-> a)
1560. ((true <-> (a or a)) <-> a)
1561. ((true <-> (true -> a)) <-> a)
1562. ((false <-> (a -> false)) <-> a)
1563. ((a <-> (a -> false)) <-> false)
1564. ((a <-> (a <-> b)) <-> b)
1565. ((a <-> (b <-> a)) <-> b)
1566. (((not true) <-> (not a)) <-> a)
1567. (((not a) <-> (not true)) <-> a)
1568. (((not (not a)) <-> true) <-> a)
1569. (((true and a) <-> true) <-> a)
1570. (((false and a) <-> true) <-> false)
1571. (((a and true) <-> true) <-> a)
1572. (((a and false) <-> true) <-> false)
1573. (((a and a) <-> true) <-> a)
1574. (((false or a) <-> true) <-> a)
1575. (((a or false) <-> true) <-> a)
1576. (((a or a) <-> true) <-> a)
1577. (((true -> a) <-> true) <-> a)
1578. (((a -> false) <-> false) <-> a)
1579. (((a -> false) <-> a) <-> false)
1580. (((a <-> b) <-> a) <-> b)
1581. (((a <-> b) <-> b) <-> a)

One Hundred Propositional Tautologies (4)

; In list of the propositional tautologies from the last article
; in this series, I have found another redundancy. For example,
; both (or true nil) and (or true A) are still in the 100 formulas,
; although (or true nil) is special case of (or true A).

; How it happened? (or true A) is discovered after
; (or true nil). So, tests confirmed that (or true A) is not the instance
; of any tautology, but (or true nil) suddenly became the instance.
; of later developed theorem. And what now?

; (or true nil) becomes some kind of a formula for museum. In time it
; was discovered, it was interesting enough, but now - it cannot
; be effectively used any more in future development. So, what to
; do with that? I'll build special list, and call it museum. OK,
; I could use the word "archive", but this word is somehow overloaded,
; so I'll use museum.
;
; Then, I'll change the program on this way: first,
;
;    (1) it generates all propositional formulas of a given length,
;        making a list PF.
;
;    (2) it filters out tautologies - and makes the list T1
;
;    (3) one by one, it passes through tautologies in T1 and tests
;        whether some of them are instances of other, previously
;        developed tautologies in T1. More than that, it tests
;        whether some of the subformulas of tautologies is an
;        instance of the previously developed tautologies. Only
;        those tautologies, proved not to be an instances are
;        inserted in new list T2.
;
;    (4) Some of the formulas from T2 are "obsolete", because
;        some of the tautologies generated later are more general
;        - more general in a sense - older formula is and instance
;        - of new formula, or some subformula of the older formula
;        is an instance of a newer formula. These formulas are
;        moved to "museum", I'll name it M2.

(load "http://www.instprog.com/Instprog.default-library.lsp")

(set 'PF (apply append (map (lambda(x)(all-pf x '(true nil a b c d e)
                                                '(not)
                                                '(and or -> <->)))
                            (sequence 1 5))))

(println "Generated " (length PF) " formulas.")

(set 'T1 (filter tautology? PF))

(println "Filtered to " (length T1) " tautologies in T1.")

(set 'T2 (list))
(dolist(f1 T1)
   (set 'is-instance nil)
   (dolist(f2 T2 is-instance)
      (let((uf2 (upper-case-formula f2)))
          (dolist (sf1 (difference (branches f1) booleans) is-instance)
            (set 'u (unify sf1 uf2))
            (when (or u (= u '()))
                  (set 'is-instance true)))))
    (unless is-instance
            (push f1 T2 -1)))

(println "Filtered to " (length T2) " tautologies in T2.")

(set 'T2 (reverse T2))
(set 'T3 (list))
(set 'M3 (list))

(dolist(f1 T2)
   (set 'f1counter $idx)
   (set 'is-instance nil)
   (dolist(f2 T2)
     (when (> f1counter $idx)
        (let((uf2 (upper-case-formula f2)))
          (dolist (sf1 (difference (branches f1) booleans) is-instance)
            (set 'u (unify sf1 uf2))
            (when (or u (= u '()))
                  ;(println "--- " f1counter " ---")
                  ;(println= "\nInstance discovered: \n" f1 "\n" sf1 "\n" uf2)
                  (set 'is-instance true))))))
   (if is-instance (push f1 M3)
                   (push f1 T3)))

(println "Filtered to " (length T3) " tautologies in T3 and "
                        (length M3) " tautologies in M3.")

(println "\n\n\n*** T3 ***\n")
(map (lambda(x)(println (+ $idx 1) ". " x)) T3)

(println "\n\n\n*** M3 ***\n")
(map (lambda(x)(println (+ $idx 1) ". " x)) M3)

(exit)

;---------------------------------------------------------------
; OUTPUT

Generated 12971 formulas.
Filtered to 2467 tautologies in T1.
Filtered to 137 tautologies in T2.
Filtered to 84 tautologies in T3 and 53 tautologies in M3.

*** T3 ***

1. true
2. (not nil)
3. (not (not true))
4. (and true true)
5. (or true a)
6. (or a true)
7. (-> nil a)
8. (-> a true)
9. (-> a a)
10. (<-> a a)
11. (not (and nil a))
12. (not (and a nil))
13. (not (or nil nil))
14. (not (-> true nil))
15. (not (<-> true nil))
16. (not (<-> nil true))
17. (or a (not a))
18. (or (not a) a)
19. (-> (not true) a)
20. (<-> nil (not true))
21. (<-> (not true) nil)
22. (not (and a (not true)))
23. (not (and a (not a)))
24. (not (and (not true) a))
25. (not (and (not a) a))
26. (not (or nil (not true)))
27. (not (or (not true) nil))
28. (not (-> true (not true)))
29. (not (<-> a (not a)))
30. (not (<-> (not a) a))
31. (or a (-> a b))
32. (or a (<-> nil a))
33. (or a (<-> a nil))
34. (or (-> a b) a)
35. (or (<-> nil a) a)
36. (or (<-> a nil) a)
37. (-> a (not (not a)))
38. (-> a (and true a))
39. (-> a (and a true))
40. (-> a (and a a))
41. (-> a (or a b))
42. (-> a (or b a))
43. (-> a (-> b a))
44. (-> a (<-> true a))
45. (-> a (<-> a true))
46. (-> (not (not a)) a)
47. (-> (and nil a) b)
48. (-> (and a nil) b)
49. (-> (and a b) a)
50. (-> (and a b) b)
51. (-> (or nil nil) a)
52. (-> (or nil a) a)
53. (-> (or a nil) a)
54. (-> (or a a) a)
55. (-> (-> true nil) a)
56. (-> (-> true a) a)
57. (-> (<-> true nil) a)
58. (-> (<-> true a) a)
59. (-> (<-> nil true) a)
60. (-> (<-> a true) a)
61. (<-> nil (and nil a))
62. (<-> nil (and a nil))
63. (<-> a (not (not a)))
64. (<-> a (and true a))
65. (<-> a (and a true))
66. (<-> a (and a a))
67. (<-> a (or nil a))
68. (<-> a (or a nil))
69. (<-> a (or a a))
70. (<-> a (-> true a))
71. (<-> a (<-> true a))
72. (<-> a (<-> a true))
73. (<-> (not (not a)) a)
74. (<-> (and true a) a)
75. (<-> (and nil a) nil)
76. (<-> (and a true) a)
77. (<-> (and a nil) nil)
78. (<-> (and a a) a)
79. (<-> (or nil a) a)
80. (<-> (or a nil) a)
81. (<-> (or a a) a)
82. (<-> (-> true a) a)
83. (<-> (<-> true a) a)
84. (<-> (<-> a true) a)

*** M3 ***

1. (or true true)
2. (or true nil)
3. (or nil true)
4. (-> true true)
5. (-> nil true)
6. (-> nil nil)
7. (<-> true true)
8. (<-> nil nil)
9. (not (and true nil))
10. (not (and nil true))
11. (not (and nil nil))
12. (-> (not true) nil)
13. (not (and true (not true)))
14. (not (and (not true) true))
15. (not (<-> true (not true)))
16. (not (<-> (not true) true))
17. (or a (-> a nil))
18. (or (-> a nil) a)
19. (-> a (or nil a))
20. (-> a (or a nil))
21. (-> a (or a a))
22. (-> a (-> true a))
23. (-> (and true nil) nil)
24. (-> (and true nil) a)
25. (-> (and true a) a)
26. (-> (and nil true) nil)
27. (-> (and nil true) a)
28. (-> (and nil nil) nil)
29. (-> (and nil nil) a)
30. (-> (and nil a) nil)
31. (-> (and nil a) a)
32. (-> (and a true) a)
33. (-> (and a nil) nil)
34. (-> (and a nil) a)
35. (-> (and a a) a)
36. (-> (or nil nil) nil)
37. (-> (-> true nil) nil)
38. (-> (<-> true nil) nil)
39. (-> (<-> nil true) nil)
40. (<-> nil (and true nil))
41. (<-> nil (and nil true))
42. (<-> nil (and nil nil))
43. (<-> nil (or nil nil))
44. (<-> nil (-> true nil))
45. (<-> nil (<-> true nil))
46. (<-> nil (<-> nil true))
47. (<-> (and true nil) nil)
48. (<-> (and nil true) nil)
49. (<-> (and nil nil) nil)
50. (<-> (or nil nil) nil)
51. (<-> (-> true nil) nil)
52. (<-> (<-> true nil) nil)
53. (<-> (<-> nil true) nil)

---

Kazimir Majorinc's Blog (currently not in use)

One Hundred Propositional Tautologies (5)

One Hundred Propositional Tautologies (4)

Newlisp Related Blogs

Newlisp Related Sites.