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

Implication variant #1:

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

 Variant #1. 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))



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

Implication variant #2:

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

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

Implication variant #3:

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

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

Implication variant #4:

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

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

Implication variant #5:

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

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