------------------------------------------------

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: 0 0 1 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

True: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #3. Negation: 0 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not 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)

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)

Not true: (A->B)->((~A->B)->B)

Not 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 #4. Negation: 0 1 0 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

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 #5. Negation: 0 1 1 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

True: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #6. Negation: 0 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

True: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #7. Negation: 0 2 0 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

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 #8. Negation: 0 2 1 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

True: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #9. Negation: 0 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #10. 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))



 Variant #11. Negation: 1 0 1 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

True: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #12. Negation: 1 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

True: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #13. Negation: 1 1 0 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not 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 #14. Negation: 1 1 1 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #15. Negation: 1 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #16. Negation: 1 2 0 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not 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 #17. Negation: 1 2 1 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #18. Negation: 1 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #19. Negation: 2 0 0 L9 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

True: (A->B)->((~A->B)->B)

Not 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 #20. Negation: 2 0 1 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #21. Negation: 2 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #22. Negation: 2 1 0 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

True: (A->B)->((~A->B)->B)

Not 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 #23. Negation: 2 1 1 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #24. Negation: 2 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #25. Negation: 2 2 0 L9 not true. L10 not true. L11 true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not 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)

Not true: ((~~A)->(~~B))->(A->B)

True: (A->B)->((~A)vB)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

True: (A->B)->((~A->B)->B)

Not 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 #26. Negation: 2 2 1 L9 true. L10 not true. L11 true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

True: (A->B)->((~A)vB)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #27. Negation: 2 2 2 L9 true. L10 not true. L11 true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

True: (A->B)->((~A)vB)

Not true: ((A->B)->B)->(AvB)

Not true: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not true: (A->B)->((~A->B)->B)

Not 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 #28. 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 #29. 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 #30. Negation: 0 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #31. 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 #32. 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 #33. Negation: 0 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #34. 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 #35. 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 #36. Negation: 0 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #37. 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 #38. 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 #39. Negation: 1 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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: 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 #41. 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 #42. Negation: 1 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #43. 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 #44. 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 #45. Negation: 1 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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: 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 #47. 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 #48. Negation: 2 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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))



 Variant #51. Negation: 2 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #52. Negation: 2 2 0 L9 true. L10 true. L11 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

True: ((~B)->(~A))->(A->B)

True: ((~A)->B)->((~B)->A)

True: ((~~A)->(~~B))->(A->B)

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)

True: (A->B)->(((~A)->(~B))->(B->A))



 Variant #53. Negation: 2 2 1 L9 true. L10 true. L11 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

True: ((~B)->(~A))->(A->B)

True: ((~A)->B)->((~B)->A)

True: ((~~A)->(~~B))->(A->B)

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)

True: (A->B)->(((~A)->(~B))->(B->A))



 Variant #54. Negation: 2 2 2 L9 true. L10 not true. L11 true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

True: (A->B)->((~A)vB)

True: ((A->B)->B)->(AvB)

True: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not 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 #55. 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 #56. 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 #57. Negation: 0 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #58. 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 #59. 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 #60. Negation: 0 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #61. 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 #62. 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 #63. Negation: 0 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #64. 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 #65. 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 #66. Negation: 1 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #67. 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 #68. 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 #69. Negation: 1 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #70. 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 #71. 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 #72. Negation: 1 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #73. 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 #74. 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 #75. Negation: 2 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #76. 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 #77. 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))



 Variant #78. Negation: 2 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #79. Negation: 2 2 0 L9 true. L10 true. L11 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

True: ((~B)->(~A))->(A->B)

True: ((~A)->B)->((~B)->A)

True: ((~~A)->(~~B))->(A->B)

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)

True: (A->B)->(((~A)->(~B))->(B->A))



 Variant #80. Negation: 2 2 1 L9 true. L10 true. L11 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

True: ((~B)->(~A))->(A->B)

True: ((~A)->B)->((~B)->A)

True: ((~~A)->(~~B))->(A->B)

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)

True: (A->B)->(((~A)->(~B))->(B->A))



 Variant #81. Negation: 2 2 2 L9 true. L10 not true. L11 true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

True: (A->B)->((~A)vB)

True: ((A->B)->B)->(AvB)

True: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not 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 #4:

 2 2 2 2 2 2 1 0 2 L1-L8 true. 

 Variant #82. 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 #83. 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 #84. Negation: 0 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #85. 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 #86. 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 #87. Negation: 0 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #88. 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 #89. 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 #90. Negation: 0 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #91. 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 #92. 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 #93. Negation: 1 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #94. 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 #95. 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 #96. Negation: 1 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #97. 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 #98. 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 #99. Negation: 1 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #100. 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 #101. 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 #102. Negation: 2 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #103. 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 #104. 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))



 Variant #105. Negation: 2 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #106. Negation: 2 2 0 L9 true. L10 true. L11 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

True: ((~B)->(~A))->(A->B)

True: ((~A)->B)->((~B)->A)

True: ((~~A)->(~~B))->(A->B)

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)

True: (A->B)->(((~A)->(~B))->(B->A))



 Variant #107. Negation: 2 2 1 L9 true. L10 true. L11 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

True: ((~B)->(~A))->(A->B)

True: ((~A)->B)->((~B)->A)

True: ((~~A)->(~~B))->(A->B)

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)

True: (A->B)->(((~A)->(~B))->(B->A))



 Variant #108. Negation: 2 2 2 L9 true. L10 not true. L11 true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

True: (A->B)->((~A)vB)

True: ((A->B)->B)->(AvB)

True: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not 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 #109. 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 #110. 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 #111. Negation: 0 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #112. 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 #113. 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 #114. Negation: 0 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #115. 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 #116. 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 #117. Negation: 0 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #118. 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 #119. 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 #120. Negation: 1 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #121. 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 #122. 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 #123. Negation: 1 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not 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)

Not 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 #124. 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 #125. 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 #126. Negation: 1 2 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #127. 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 #128. 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 #129. Negation: 2 0 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #130. 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 #131. 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))



 Variant #132. Negation: 2 1 2 L9 not true. L10 not true. L11 not true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

Not true: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

Not 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 #133. Negation: 2 2 0 L9 true. L10 true. L11 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

True: ((~B)->(~A))->(A->B)

True: ((~A)->B)->((~B)->A)

True: ((~~A)->(~~B))->(A->B)

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)

True: (A->B)->(((~A)->(~B))->(B->A))



 Variant #134. Negation: 2 2 1 L9 true. L10 true. L11 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

True: ((~B)->(~A))->(A->B)

True: ((~A)->B)->((~B)->A)

True: ((~~A)->(~~B))->(A->B)

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)

True: (A->B)->(((~A)->(~B))->(B->A))



 Variant #135. Negation: 2 2 2 L9 true. L10 not true. L11 true.

 Constructively provable formulas

Not true: (AvB)->((~A)->B)

Not true: ((~A)vB)->(A->B)

True: ((~~A)->(~~B))->(~~(A->B))

Not true: (~~A)->((~A)->A)

Not 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)

True: (A->B)->((~A)vB)

True: ((A->B)->B)->(AvB)

True: ((A->B)->A)->A

Not true: (~(A&(~B)))->(A->B)

Not 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))



----------------------The End.---------------------