------------------------------------------------ Implication variant #1: 2 2 2 0 2 2 0 1 2 L1-L8 true. Variant #1. Negation: 0 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) Not true: ((A->B)->B)->(AvB) Not true: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) Not true: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #2. Negation: 1 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) Not true: ((A->B)->B)->(AvB) Not true: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) Not true: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) ------------------------------------------------ Implication variant #2: 2 2 2 2 2 2 0 0 2 L1-L8 true. Variant #3. Negation: 0 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #4. Negation: 0 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #5. Negation: 0 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #6. Negation: 0 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #7. Negation: 0 2 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #8. Negation: 0 2 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) True: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #9. Negation: 1 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #10. Negation: 1 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #11. Negation: 1 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #12. Negation: 1 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #13. Negation: 1 2 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #14. Negation: 1 2 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #15. Negation: 2 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #16. Negation: 2 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #17. Negation: 2 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) True: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #18. Negation: 2 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) ------------------------------------------------ Implication variant #3: 2 2 2 2 2 2 0 1 2 L1-L8 true. Variant #19. Negation: 0 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #20. Negation: 0 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #21. Negation: 0 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #22. Negation: 0 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #23. Negation: 0 2 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #24. Negation: 0 2 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) True: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #25. Negation: 1 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #26. Negation: 1 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #27. Negation: 1 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #28. Negation: 1 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #29. Negation: 1 2 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #30. Negation: 1 2 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #31. Negation: 2 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #32. Negation: 2 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #33. Negation: 2 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) True: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #34. Negation: 2 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) ------------------------------------------------ Implication variant #4: 2 2 2 2 2 2 1 0 2 L1-L8 true. Variant #35. Negation: 0 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #36. Negation: 0 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #37. Negation: 0 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #38. Negation: 0 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #39. Negation: 0 2 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #40. Negation: 0 2 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) True: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #41. Negation: 1 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #42. Negation: 1 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #43. Negation: 1 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #44. Negation: 1 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #45. Negation: 1 2 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #46. Negation: 1 2 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #47. Negation: 2 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #48. Negation: 2 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #49. Negation: 2 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) True: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #50. Negation: 2 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) ------------------------------------------------ Implication variant #5: 2 2 2 2 2 2 1 1 2 L1-L8 true. Variant #51. Negation: 0 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #52. Negation: 0 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #53. Negation: 0 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #54. Negation: 0 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #55. Negation: 0 2 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #56. Negation: 0 2 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) True: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #57. Negation: 1 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #58. Negation: 1 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #59. Negation: 1 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #60. Negation: 1 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) True: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #61. Negation: 1 2 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #62. Negation: 1 2 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) Not true: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #63. Negation: 2 0 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #64. Negation: 2 0 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) Not true: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A Not true: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #65. Negation: 2 1 0 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) True: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) True: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) True: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) Variant #66. Negation: 2 1 1 L9 not true. L10 true. L11 not true. Constructively provable formulas True: (AvB)->((~A)->B) True: ((~A)vB)->(A->B) Not true: ((~~A)->(~~B))->(~~(A->B)) True: (~~A)->((~A)->A) True: (Av(~A))->((~~A)->A) Not true: ~~((~~A)->A) Classically provable formulas True: (~~(AvB))->((~~A)v(~~B)) True: (~(A&B))->((~A)v(~B)) True: (~~A)->A Not true: ((~B)->(~A))->(A->B) Not true: ((~A)->B)->((~B)->A) Not true: ((~~A)->(~~B))->(A->B) Not true: (A->B)->((~A)vB) True: ((A->B)->B)->(AvB) True: ((A->B)->A)->A True: (~(A&(~B)))->(A->B) True: (A->B)->((~A->B)->B) True: (~(A->B))->(A&(~B)) True: Av(A->B) True: (A->B)v(B->A) Not true: (A->B)->(((~A)->(~B))->(B->A)) ----------------------The End.---------------------