for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂ being set holds
not ( ( $ b₁ implies $ AND2 (NOT1 b₁₀),(NOT1 b₉) ) & ( $ AND2 (NOT1 b₁₀),(NOT1 b₉) implies $ b₁ ) & ( $ b₂ implies $ AND2 (NOT1 b₁₀),b₉ ) & ( $ AND2 (NOT1 b₁₀),b₉ implies $ b₂ ) & ( $ b₃ implies $ AND2 b₁₀,(NOT1 b₉) ) & ( $ AND2 b₁₀,(NOT1 b₉) implies $ b₃ ) & ( $ b₄ implies $ AND2 b₁₀,b₉ ) & ( $ AND2 b₁₀,b₉ implies $ b₄ ) & ( $ b₅ implies $ AND2 (NOT1 b₁₂),(NOT1 b₁₁) ) & ( $ AND2 (NOT1 b₁₂),(NOT1 b₁₁) implies $ b₅ ) & ( $ b₆ implies $ AND2 (NOT1 b₁₂),b₁₁ ) & ( $ AND2 (NOT1 b₁₂),b₁₁ implies $ b₆ ) & ( $ b₇ implies $ AND2 b₁₂,(NOT1 b₁₁) ) & ( $ AND2 b₁₂,(NOT1 b₁₁) implies $ b₇ ) & ( $ b₈ implies $ AND2 b₁₂,b₁₁ ) & ( $ AND2 b₁₂,b₁₁ implies $ b₈ ) & ( $ b₁₁ implies $ NOT1 b₁₀ ) & ( $ NOT1 b₁₀ implies $ b₁₁ ) & ( $ b₁₂ implies $ b₉ ) & ( $ b₉ implies $ b₁₂ ) & not ( ( $ b₆ implies $ b₁ ) & ( $ b₁ implies $ b₆ ) & ( $ b₈ implies $ b₂ ) & ( $ b₂ implies $ b₈ ) & ( $ b₇ implies $ b₄ ) & ( $ b₄ implies $ b₇ ) & ( $ b₅ implies $ b₃ ) & ( $ b₃ implies $ b₅ ) ) )

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃ being set holds
not ( ( $ b₁ implies $ AND2 (NOT1 b₁₀),(NOT1 b₉) ) & ( $ AND2 (NOT1 b₁₀),(NOT1 b₉) implies $ b₁ ) & ( $ b₂ implies $ AND2 (NOT1 b₁₀),b₉ ) & ( $ AND2 (NOT1 b₁₀),b₉ implies $ b₂ ) & ( $ b₃ implies $ AND2 b₁₀,(NOT1 b₉) ) & ( $ AND2 b₁₀,(NOT1 b₉) implies $ b₃ ) & ( $ b₄ implies $ AND2 b₁₀,b₉ ) & ( $ AND2 b₁₀,b₉ implies $ b₄ ) & ( $ b₅ implies $ AND2 (NOT1 b₁₂),(NOT1 b₁₁) ) & ( $ AND2 (NOT1 b₁₂),(NOT1 b₁₁) implies $ b₅ ) & ( $ b₆ implies $ AND2 (NOT1 b₁₂),b₁₁ ) & ( $ AND2 (NOT1 b₁₂),b₁₁ implies $ b₆ ) & ( $ b₇ implies $ AND2 b₁₂,(NOT1 b₁₁) ) & ( $ AND2 b₁₂,(NOT1 b₁₁) implies $ b₇ ) & ( $ b₈ implies $ AND2 b₁₂,b₁₁ ) & ( $ AND2 b₁₂,b₁₁ implies $ b₈ ) & ( $ b₁₁ implies $ AND2 (NOT1 b₁₀),b₁₃ ) & ( $ AND2 (NOT1 b₁₀),b₁₃ implies $ b₁₁ ) & ( $ b₁₂ implies $ AND2 b₉,b₁₃ ) & ( $ AND2 b₉,b₁₃ implies $ b₁₂ ) & not ( ( $ b₆ implies $ AND2 b₁,b₁₃ ) & ( $ AND2 b₁,b₁₃ implies $ b₆ ) & ( $ b₈ implies $ AND2 b₂,b₁₃ ) & ( $ AND2 b₂,b₁₃ implies $ b₈ ) & ( $ b₇ implies $ AND2 b₄,b₁₃ ) & ( $ AND2 b₄,b₁₃ implies $ b₇ ) & ( $ b₅ implies $ OR2 (AND2 b₃,b₁₃),(NOT1 b₁₃) ) & ( $ OR2 (AND2 b₃,b₁₃),(NOT1 b₁₃) implies $ b₅ ) ) )

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅, b₁₆, b₁₇, b₁₈, b₁₉, b₂₀, b₂₁, b₂₂ being set holds
not ( ( $ b₁ implies $ AND3 (NOT1 b₁₉),(NOT1 b₁₈),(NOT1 b₁₇) ) & ( $ AND3 (NOT1 b₁₉),(NOT1 b₁₈),(NOT1 b₁₇) implies $ b₁ ) & ( $ b₂ implies $ AND3 (NOT1 b₁₉),(NOT1 b₁₈),b₁₇ ) & ( $ AND3 (NOT1 b₁₉),(NOT1 b₁₈),b₁₇ implies $ b₂ ) & ( $ b₃ implies $ AND3 (NOT1 b₁₉),b₁₈,(NOT1 b₁₇) ) & ( $ AND3 (NOT1 b₁₉),b₁₈,(NOT1 b₁₇) implies $ b₃ ) & ( $ b₄ implies $ AND3 (NOT1 b₁₉),b₁₈,b₁₇ ) & ( $ AND3 (NOT1 b₁₉),b₁₈,b₁₇ implies $ b₄ ) & ( $ b₅ implies $ AND3 b₁₉,(NOT1 b₁₈),(NOT1 b₁₇) ) & ( $ AND3 b₁₉,(NOT1 b₁₈),(NOT1 b₁₇) implies $ b₅ ) & ( $ b₆ implies $ AND3 b₁₉,(NOT1 b₁₈),b₁₇ ) & ( $ AND3 b₁₉,(NOT1 b₁₈),b₁₇ implies $ b₆ ) & ( $ b₇ implies $ AND3 b₁₉,b₁₈,(NOT1 b₁₇) ) & ( $ AND3 b₁₉,b₁₈,(NOT1 b₁₇) implies $ b₇ ) & ( $ b₈ implies $ AND3 b₁₉,b₁₈,b₁₇ ) & ( $ AND3 b₁₉,b₁₈,b₁₇ implies $ b₈ ) & ( $ b₉ implies $ AND3 (NOT1 b₂₂),(NOT1 b₂₁),(NOT1 b₂₀) ) & ( $ AND3 (NOT1 b₂₂),(NOT1 b₂₁),(NOT1 b₂₀) implies $ b₉ ) & ( $ b₁₀ implies $ AND3 (NOT1 b₂₂),(NOT1 b₂₁),b₂₀ ) & ( $ AND3 (NOT1 b₂₂),(NOT1 b₂₁),b₂₀ implies $ b₁₀ ) & ( $ b₁₁ implies $ AND3 (NOT1 b₂₂),b₂₁,(NOT1 b₂₀) ) & ( $ AND3 (NOT1 b₂₂),b₂₁,(NOT1 b₂₀) implies $ b₁₁ ) & ( $ b₁₂ implies $ AND3 (NOT1 b₂₂),b₂₁,b₂₀ ) & ( $ AND3 (NOT1 b₂₂),b₂₁,b₂₀ implies $ b₁₂ ) & ( $ b₁₃ implies $ AND3 b₂₂,(NOT1 b₂₁),(NOT1 b₂₀) ) & ( $ AND3 b₂₂,(NOT1 b₂₁),(NOT1 b₂₀) implies $ b₁₃ ) & ( $ b₁₄ implies $ AND3 b₂₂,(NOT1 b₂₁),b₂₀ ) & ( $ AND3 b₂₂,(NOT1 b₂₁),b₂₀ implies $ b₁₄ ) & ( $ b₁₅ implies $ AND3 b₂₂,b₂₁,(NOT1 b₂₀) ) & ( $ AND3 b₂₂,b₂₁,(NOT1 b₂₀) implies $ b₁₅ ) & ( $ b₁₆ implies $ AND3 b₂₂,b₂₁,b₂₀ ) & ( $ AND3 b₂₂,b₂₁,b₂₀ implies $ b₁₆ ) & ( $ b₂₀ implies $ NOT1 b₁₉ ) & ( $ NOT1 b₁₉ implies $ b₂₀ ) & ( $ b₂₁ implies $ b₁₇ ) & ( $ b₁₇ implies $ b₂₁ ) & ( $ b₂₂ implies $ b₁₈ ) & ( $ b₁₈ implies $ b₂₂ ) & not ( ( $ b₁₀ implies $ b₁ ) & ( $ b₁ implies $ b₁₀ ) & ( $ b₁₂ implies $ b₂ ) & ( $ b₂ implies $ b₁₂ ) & ( $ b₁₆ implies $ b₄ ) & ( $ b₄ implies $ b₁₆ ) & ( $ b₁₅ implies $ b₈ ) & ( $ b₈ implies $ b₁₅ ) & ( $ b₁₃ implies $ b₇ ) & ( $ b₇ implies $ b₁₃ ) & ( $ b₉ implies $ b₅ ) & ( $ b₅ implies $ b₉ ) & ( $ b₁₁ implies $ b₆ ) & ( $ b₆ implies $ b₁₁ ) & ( $ b₁₄ implies $ b₃ ) & ( $ b₃ implies $ b₁₄ ) ) )

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅, b₁₆, b₁₇, b₁₈, b₁₉, b₂₀, b₂₁, b₂₂, b₂₃ being set holds
not ( ( $ b₁ implies $ AND3 (NOT1 b₁₉),(NOT1 b₁₈),(NOT1 b₁₇) ) & ( $ AND3 (NOT1 b₁₉),(NOT1 b₁₈),(NOT1 b₁₇) implies $ b₁ ) & ( $ b₂ implies $ AND3 (NOT1 b₁₉),(NOT1 b₁₈),b₁₇ ) & ( $ AND3 (NOT1 b₁₉),(NOT1 b₁₈),b₁₇ implies $ b₂ ) & ( $ b₃ implies $ AND3 (NOT1 b₁₉),b₁₈,(NOT1 b₁₇) ) & ( $ AND3 (NOT1 b₁₉),b₁₈,(NOT1 b₁₇) implies $ b₃ ) & ( $ b₄ implies $ AND3 (NOT1 b₁₉),b₁₈,b₁₇ ) & ( $ AND3 (NOT1 b₁₉),b₁₈,b₁₇ implies $ b₄ ) & ( $ b₅ implies $ AND3 b₁₉,(NOT1 b₁₈),(NOT1 b₁₇) ) & ( $ AND3 b₁₉,(NOT1 b₁₈),(NOT1 b₁₇) implies $ b₅ ) & ( $ b₆ implies $ AND3 b₁₉,(NOT1 b₁₈),b₁₇ ) & ( $ AND3 b₁₉,(NOT1 b₁₈),b₁₇ implies $ b₆ ) & ( $ b₇ implies $ AND3 b₁₉,b₁₈,(NOT1 b₁₇) ) & ( $ AND3 b₁₉,b₁₈,(NOT1 b₁₇) implies $ b₇ ) & ( $ b₈ implies $ AND3 b₁₉,b₁₈,b₁₇ ) & ( $ AND3 b₁₉,b₁₈,b₁₇ implies $ b₈ ) & ( $ b₉ implies $ AND3 (NOT1 b₂₂),(NOT1 b₂₁),(NOT1 b₂₀) ) & ( $ AND3 (NOT1 b₂₂),(NOT1 b₂₁),(NOT1 b₂₀) implies $ b₉ ) & ( $ b₁₀ implies $ AND3 (NOT1 b₂₂),(NOT1 b₂₁),b₂₀ ) & ( $ AND3 (NOT1 b₂₂),(NOT1 b₂₁),b₂₀ implies $ b₁₀ ) & ( $ b₁₁ implies $ AND3 (NOT1 b₂₂),b₂₁,(NOT1 b₂₀) ) & ( $ AND3 (NOT1 b₂₂),b₂₁,(NOT1 b₂₀) implies $ b₁₁ ) & ( $ b₁₂ implies $ AND3 (NOT1 b₂₂),b₂₁,b₂₀ ) & ( $ AND3 (NOT1 b₂₂),b₂₁,b₂₀ implies $ b₁₂ ) & ( $ b₁₃ implies $ AND3 b₂₂,(NOT1 b₂₁),(NOT1 b₂₀) ) & ( $ AND3 b₂₂,(NOT1 b₂₁),(NOT1 b₂₀) implies $ b₁₃ ) & ( $ b₁₄ implies $ AND3 b₂₂,(NOT1 b₂₁),b₂₀ ) & ( $ AND3 b₂₂,(NOT1 b₂₁),b₂₀ implies $ b₁₄ ) & ( $ b₁₅ implies $ AND3 b₂₂,b₂₁,(NOT1 b₂₀) ) & ( $ AND3 b₂₂,b₂₁,(NOT1 b₂₀) implies $ b₁₅ ) & ( $ b₁₆ implies $ AND3 b₂₂,b₂₁,b₂₀ ) & ( $ AND3 b₂₂,b₂₁,b₂₀ implies $ b₁₆ ) & ( $ b₂₀ implies $ AND2 (NOT1 b₁₉),b₂₃ ) & ( $ AND2 (NOT1 b₁₉),b₂₃ implies $ b₂₀ ) & ( $ b₂₁ implies $ AND2 b₁₇,b₂₃ ) & ( $ AND2 b₁₇,b₂₃ implies $ b₂₁ ) & ( $ b₂₂ implies $ AND2 b₁₈,b₂₃ ) & ( $ AND2 b₁₈,b₂₃ implies $ b₂₂ ) & not ( ( $ b₁₀ implies $ AND2 b₁,b₂₃ ) & ( $ AND2 b₁,b₂₃ implies $ b₁₀ ) & ( $ b₁₂ implies $ AND2 b₂,b₂₃ ) & ( $ AND2 b₂,b₂₃ implies $ b₁₂ ) & ( $ b₁₆ implies $ AND2 b₄,b₂₃ ) & ( $ AND2 b₄,b₂₃ implies $ b₁₆ ) & ( $ b₁₅ implies $ AND2 b₈,b₂₃ ) & ( $ AND2 b₈,b₂₃ implies $ b₁₅ ) & ( $ b₁₃ implies $ AND2 b₇,b₂₃ ) & ( $ AND2 b₇,b₂₃ implies $ b₁₃ ) & ( $ b₉ implies $ OR2 (AND2 b₅,b₂₃),(NOT1 b₂₃) ) & ( $ OR2 (AND2 b₅,b₂₃),(NOT1 b₂₃) implies $ b₉ ) & ( $ b₁₁ implies $ AND2 b₆,b₂₃ ) & ( $ AND2 b₆,b₂₃ implies $ b₁₁ ) & ( $ b₁₄ implies $ AND2 b₃,b₂₃ ) & ( $ AND2 b₃,b₂₃ implies $ b₁₄ ) ) )

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅, b₁₆, b₁₇, b₁₈, b₁₉, b₂₀, b₂₁, b₂₂, b₂₃, b₂₄, b₂₅, b₂₆, b₂₇, b₂₈, b₂₉, b₃₀, b₃₁, b₃₂, b₃₃, b₃₄, b₃₅, b₃₆, b₃₇, b₃₈, b₃₉, b₄₀ being set holds
not ( ( $ b₁ implies $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),(NOT1 b₃₄),(NOT1 b₃₃) ) & ( $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),(NOT1 b₃₄),(NOT1 b₃₃) implies $ b₁ ) & ( $ b₂ implies $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),(NOT1 b₃₄),b₃₃ ) & ( $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),(NOT1 b₃₄),b₃₃ implies $ b₂ ) & ( $ b₃ implies $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),b₃₄,(NOT1 b₃₃) ) & ( $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),b₃₄,(NOT1 b₃₃) implies $ b₃ ) & ( $ b₄ implies $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),b₃₄,b₃₃ ) & ( $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),b₃₄,b₃₃ implies $ b₄ ) & ( $ b₅ implies $ AND4 (NOT1 b₃₆),b₃₅,(NOT1 b₃₄),(NOT1 b₃₃) ) & ( $ AND4 (NOT1 b₃₆),b₃₅,(NOT1 b₃₄),(NOT1 b₃₃) implies $ b₅ ) & ( $ b₆ implies $ AND4 (NOT1 b₃₆),b₃₅,(NOT1 b₃₄),b₃₃ ) & ( $ AND4 (NOT1 b₃₆),b₃₅,(NOT1 b₃₄),b₃₃ implies $ b₆ ) & ( $ b₇ implies $ AND4 (NOT1 b₃₆),b₃₅,b₃₄,(NOT1 b₃₃) ) & ( $ AND4 (NOT1 b₃₆),b₃₅,b₃₄,(NOT1 b₃₃) implies $ b₇ ) & ( $ b₈ implies $ AND4 (NOT1 b₃₆),b₃₅,b₃₄,b₃₃ ) & ( $ AND4 (NOT1 b₃₆),b₃₅,b₃₄,b₃₃ implies $ b₈ ) & ( $ b₉ implies $ AND4 b₃₆,(NOT1 b₃₅),(NOT1 b₃₄),(NOT1 b₃₃) ) & ( $ AND4 b₃₆,(NOT1 b₃₅),(NOT1 b₃₄),(NOT1 b₃₃) implies $ b₉ ) & ( $ b₁₀ implies $ AND4 b₃₆,(NOT1 b₃₅),(NOT1 b₃₄),b₃₃ ) & ( $ AND4 b₃₆,(NOT1 b₃₅),(NOT1 b₃₄),b₃₃ implies $ b₁₀ ) & ( $ b₁₁ implies $ AND4 b₃₆,(NOT1 b₃₅),b₃₄,(NOT1 b₃₃) ) & ( $ AND4 b₃₆,(NOT1 b₃₅),b₃₄,(NOT1 b₃₃) implies $ b₁₁ ) & ( $ b₁₂ implies $ AND4 b₃₆,(NOT1 b₃₅),b₃₄,b₃₃ ) & ( $ AND4 b₃₆,(NOT1 b₃₅),b₃₄,b₃₃ implies $ b₁₂ ) & ( $ b₁₃ implies $ AND4 b₃₆,b₃₅,(NOT1 b₃₄),(NOT1 b₃₃) ) & ( $ AND4 b₃₆,b₃₅,(NOT1 b₃₄),(NOT1 b₃₃) implies $ b₁₃ ) & ( $ b₁₄ implies $ AND4 b₃₆,b₃₅,(NOT1 b₃₄),b₃₃ ) & ( $ AND4 b₃₆,b₃₅,(NOT1 b₃₄),b₃₃ implies $ b₁₄ ) & ( $ b₁₅ implies $ AND4 b₃₆,b₃₅,b₃₄,(NOT1 b₃₃) ) & ( $ AND4 b₃₆,b₃₅,b₃₄,(NOT1 b₃₃) implies $ b₁₅ ) & ( $ b₁₆ implies $ AND4 b₃₆,b₃₅,b₃₄,b₃₃ ) & ( $ AND4 b₃₆,b₃₅,b₃₄,b₃₃ implies $ b₁₆ ) & ( $ b₁₇ implies $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),(NOT1 b₃₈),(NOT1 b₃₇) ) & ( $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),(NOT1 b₃₈),(NOT1 b₃₇) implies $ b₁₇ ) & ( $ b₁₈ implies $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),(NOT1 b₃₈),b₃₇ ) & ( $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),(NOT1 b₃₈),b₃₇ implies $ b₁₈ ) & ( $ b₁₉ implies $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),b₃₈,(NOT1 b₃₇) ) & ( $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),b₃₈,(NOT1 b₃₇) implies $ b₁₉ ) & ( $ b₂₀ implies $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),b₃₈,b₃₇ ) & ( $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),b₃₈,b₃₇ implies $ b₂₀ ) & ( $ b₂₁ implies $ AND4 (NOT1 b₄₀),b₃₉,(NOT1 b₃₈),(NOT1 b₃₇) ) & ( $ AND4 (NOT1 b₄₀),b₃₉,(NOT1 b₃₈),(NOT1 b₃₇) implies $ b₂₁ ) & ( $ b₂₂ implies $ AND4 (NOT1 b₄₀),b₃₉,(NOT1 b₃₈),b₃₇ ) & ( $ AND4 (NOT1 b₄₀),b₃₉,(NOT1 b₃₈),b₃₇ implies $ b₂₂ ) & ( $ b₂₃ implies $ AND4 (NOT1 b₄₀),b₃₉,b₃₈,(NOT1 b₃₇) ) & ( $ AND4 (NOT1 b₄₀),b₃₉,b₃₈,(NOT1 b₃₇) implies $ b₂₃ ) & ( $ b₂₄ implies $ AND4 (NOT1 b₄₀),b₃₉,b₃₈,b₃₇ ) & ( $ AND4 (NOT1 b₄₀),b₃₉,b₃₈,b₃₇ implies $ b₂₄ ) & ( $ b₂₅ implies $ AND4 b₄₀,(NOT1 b₃₉),(NOT1 b₃₈),(NOT1 b₃₇) ) & ( $ AND4 b₄₀,(NOT1 b₃₉),(NOT1 b₃₈),(NOT1 b₃₇) implies $ b₂₅ ) & ( $ b₂₆ implies $ AND4 b₄₀,(NOT1 b₃₉),(NOT1 b₃₈),b₃₇ ) & ( $ AND4 b₄₀,(NOT1 b₃₉),(NOT1 b₃₈),b₃₇ implies $ b₂₆ ) & ( $ b₂₇ implies $ AND4 b₄₀,(NOT1 b₃₉),b₃₈,(NOT1 b₃₇) ) & ( $ AND4 b₄₀,(NOT1 b₃₉),b₃₈,(NOT1 b₃₇) implies $ b₂₇ ) & ( $ b₂₈ implies $ AND4 b₄₀,(NOT1 b₃₉),b₃₈,b₃₇ ) & ( $ AND4 b₄₀,(NOT1 b₃₉),b₃₈,b₃₇ implies $ b₂₈ ) & ( $ b₂₉ implies $ AND4 b₄₀,b₃₉,(NOT1 b₃₈),(NOT1 b₃₇) ) & ( $ AND4 b₄₀,b₃₉,(NOT1 b₃₈),(NOT1 b₃₇) implies $ b₂₉ ) & ( $ b₃₀ implies $ AND4 b₄₀,b₃₉,(NOT1 b₃₈),b₃₇ ) & ( $ AND4 b₄₀,b₃₉,(NOT1 b₃₈),b₃₇ implies $ b₃₀ ) & ( $ b₃₁ implies $ AND4 b₄₀,b₃₉,b₃₈,(NOT1 b₃₇) ) & ( $ AND4 b₄₀,b₃₉,b₃₈,(NOT1 b₃₇) implies $ b₃₁ ) & ( $ b₃₂ implies $ AND4 b₄₀,b₃₉,b₃₈,b₃₇ ) & ( $ AND4 b₄₀,b₃₉,b₃₈,b₃₇ implies $ b₃₂ ) & ( $ b₃₇ implies $ NOT1 b₃₆ ) & ( $ NOT1 b₃₆ implies $ b₃₇ ) & ( $ b₃₈ implies $ b₃₃ ) & ( $ b₃₃ implies $ b₃₈ ) & ( $ b₃₉ implies $ b₃₄ ) & ( $ b₃₄ implies $ b₃₉ ) & ( $ b₄₀ implies $ b₃₅ ) & ( $ b₃₅ implies $ b₄₀ ) & not ( ( $ b₁₈ implies $ b₁ ) & ( $ b₁ implies $ b₁₈ ) & ( $ b₂₀ implies $ b₂ ) & ( $ b₂ implies $ b₂₀ ) & ( $ b₂₄ implies $ b₄ ) & ( $ b₄ implies $ b₂₄ ) & ( $ b₃₂ implies $ b₈ ) & ( $ b₈ implies $ b₃₂ ) & ( $ b₃₁ implies $ b₁₆ ) & ( $ b₁₆ implies $ b₃₁ ) & ( $ b₂₉ implies $ b₁₅ ) & ( $ b₁₅ implies $ b₂₉ ) & ( $ b₂₅ implies $ b₁₃ ) & ( $ b₁₃ implies $ b₂₅ ) & ( $ b₁₇ implies $ b₉ ) & ( $ b₉ implies $ b₁₇ ) & ( $ b₂₂ implies $ b₃ ) & ( $ b₃ implies $ b₂₂ ) & ( $ b₂₈ implies $ b₆ ) & ( $ b₆ implies $ b₂₈ ) & ( $ b₂₃ implies $ b₁₂ ) & ( $ b₁₂ implies $ b₂₃ ) & ( $ b₃₀ implies $ b₇ ) & ( $ b₇ implies $ b₃₀ ) & ( $ b₂₇ implies $ b₁₄ ) & ( $ b₁₄ implies $ b₂₇ ) & ( $ b₂₁ implies $ b₁₁ ) & ( $ b₁₁ implies $ b₂₁ ) & ( $ b₂₆ implies $ b₅ ) & ( $ b₅ implies $ b₂₆ ) & ( $ b₁₉ implies $ b₁₀ ) & ( $ b₁₀ implies $ b₁₉ ) ) )

for b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, b₉, b₁₀, b₁₁, b₁₂, b₁₃, b₁₄, b₁₅, b₁₆, b₁₇, b₁₈, b₁₉, b₂₀, b₂₁, b₂₂, b₂₃, b₂₄, b₂₅, b₂₆, b₂₇, b₂₈, b₂₉, b₃₀, b₃₁, b₃₂, b₃₃, b₃₄, b₃₅, b₃₆, b₃₇, b₃₈, b₃₉, b₄₀, b₄₁ being set holds
not ( ( $ b₁ implies $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),(NOT1 b₃₄),(NOT1 b₃₃) ) & ( $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),(NOT1 b₃₄),(NOT1 b₃₃) implies $ b₁ ) & ( $ b₂ implies $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),(NOT1 b₃₄),b₃₃ ) & ( $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),(NOT1 b₃₄),b₃₃ implies $ b₂ ) & ( $ b₃ implies $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),b₃₄,(NOT1 b₃₃) ) & ( $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),b₃₄,(NOT1 b₃₃) implies $ b₃ ) & ( $ b₄ implies $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),b₃₄,b₃₃ ) & ( $ AND4 (NOT1 b₃₆),(NOT1 b₃₅),b₃₄,b₃₃ implies $ b₄ ) & ( $ b₅ implies $ AND4 (NOT1 b₃₆),b₃₅,(NOT1 b₃₄),(NOT1 b₃₃) ) & ( $ AND4 (NOT1 b₃₆),b₃₅,(NOT1 b₃₄),(NOT1 b₃₃) implies $ b₅ ) & ( $ b₆ implies $ AND4 (NOT1 b₃₆),b₃₅,(NOT1 b₃₄),b₃₃ ) & ( $ AND4 (NOT1 b₃₆),b₃₅,(NOT1 b₃₄),b₃₃ implies $ b₆ ) & ( $ b₇ implies $ AND4 (NOT1 b₃₆),b₃₅,b₃₄,(NOT1 b₃₃) ) & ( $ AND4 (NOT1 b₃₆),b₃₅,b₃₄,(NOT1 b₃₃) implies $ b₇ ) & ( $ b₈ implies $ AND4 (NOT1 b₃₆),b₃₅,b₃₄,b₃₃ ) & ( $ AND4 (NOT1 b₃₆),b₃₅,b₃₄,b₃₃ implies $ b₈ ) & ( $ b₉ implies $ AND4 b₃₆,(NOT1 b₃₅),(NOT1 b₃₄),(NOT1 b₃₃) ) & ( $ AND4 b₃₆,(NOT1 b₃₅),(NOT1 b₃₄),(NOT1 b₃₃) implies $ b₉ ) & ( $ b₁₀ implies $ AND4 b₃₆,(NOT1 b₃₅),(NOT1 b₃₄),b₃₃ ) & ( $ AND4 b₃₆,(NOT1 b₃₅),(NOT1 b₃₄),b₃₃ implies $ b₁₀ ) & ( $ b₁₁ implies $ AND4 b₃₆,(NOT1 b₃₅),b₃₄,(NOT1 b₃₃) ) & ( $ AND4 b₃₆,(NOT1 b₃₅),b₃₄,(NOT1 b₃₃) implies $ b₁₁ ) & ( $ b₁₂ implies $ AND4 b₃₆,(NOT1 b₃₅),b₃₄,b₃₃ ) & ( $ AND4 b₃₆,(NOT1 b₃₅),b₃₄,b₃₃ implies $ b₁₂ ) & ( $ b₁₃ implies $ AND4 b₃₆,b₃₅,(NOT1 b₃₄),(NOT1 b₃₃) ) & ( $ AND4 b₃₆,b₃₅,(NOT1 b₃₄),(NOT1 b₃₃) implies $ b₁₃ ) & ( $ b₁₄ implies $ AND4 b₃₆,b₃₅,(NOT1 b₃₄),b₃₃ ) & ( $ AND4 b₃₆,b₃₅,(NOT1 b₃₄),b₃₃ implies $ b₁₄ ) & ( $ b₁₅ implies $ AND4 b₃₆,b₃₅,b₃₄,(NOT1 b₃₃) ) & ( $ AND4 b₃₆,b₃₅,b₃₄,(NOT1 b₃₃) implies $ b₁₅ ) & ( $ b₁₆ implies $ AND4 b₃₆,b₃₅,b₃₄,b₃₃ ) & ( $ AND4 b₃₆,b₃₅,b₃₄,b₃₃ implies $ b₁₆ ) & ( $ b₁₇ implies $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),(NOT1 b₃₈),(NOT1 b₃₇) ) & ( $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),(NOT1 b₃₈),(NOT1 b₃₇) implies $ b₁₇ ) & ( $ b₁₈ implies $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),(NOT1 b₃₈),b₃₇ ) & ( $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),(NOT1 b₃₈),b₃₇ implies $ b₁₈ ) & ( $ b₁₉ implies $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),b₃₈,(NOT1 b₃₇) ) & ( $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),b₃₈,(NOT1 b₃₇) implies $ b₁₉ ) & ( $ b₂₀ implies $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),b₃₈,b₃₇ ) & ( $ AND4 (NOT1 b₄₀),(NOT1 b₃₉),b₃₈,b₃₇ implies $ b₂₀ ) & ( $ b₂₁ implies $ AND4 (NOT1 b₄₀),b₃₉,(NOT1 b₃₈),(NOT1 b₃₇) ) & ( $ AND4 (NOT1 b₄₀),b₃₉,(NOT1 b₃₈),(NOT1 b₃₇) implies $ b₂₁ ) & ( $ b₂₂ implies $ AND4 (NOT1 b₄₀),b₃₉,(NOT1 b₃₈),b₃₇ ) & ( $ AND4 (NOT1 b₄₀),b₃₉,(NOT1 b₃₈),b₃₇ implies $ b₂₂ ) & ( $ b₂₃ implies $ AND4 (NOT1 b₄₀),b₃₉,b₃₈,(NOT1 b₃₇) ) & ( $ AND4 (NOT1 b₄₀),b₃₉,b₃₈,(NOT1 b₃₇) implies $ b₂₃ ) & ( $ b₂₄ implies $ AND4 (NOT1 b₄₀),b₃₉,b₃₈,b₃₇ ) & ( $ AND4 (NOT1 b₄₀),b₃₉,b₃₈,b₃₇ implies $ b₂₄ ) & ( $ b₂₅ implies $ AND4 b₄₀,(NOT1 b₃₉),(NOT1 b₃₈),(NOT1 b₃₇) ) & ( $ AND4 b₄₀,(NOT1 b₃₉),(NOT1 b₃₈),(NOT1 b₃₇) implies $ b₂₅ ) & ( $ b₂₆ implies $ AND4 b₄₀,(NOT1 b₃₉),(NOT1 b₃₈),b₃₇ ) & ( $ AND4 b₄₀,(NOT1 b₃₉),(NOT1 b₃₈),b₃₇ implies $ b₂₆ ) & ( $ b₂₇ implies $ AND4 b₄₀,(NOT1 b₃₉),b₃₈,(NOT1 b₃₇) ) & ( $ AND4 b₄₀,(NOT1 b₃₉),b₃₈,(NOT1 b₃₇) implies $ b₂₇ ) & ( $ b₂₈ implies $ AND4 b₄₀,(NOT1 b₃₉),b₃₈,b₃₇ ) & ( $ AND4 b₄₀,(NOT1 b₃₉),b₃₈,b₃₇ implies $ b₂₈ ) & ( $ b₂₉ implies $ AND4 b₄₀,b₃₉,(NOT1 b₃₈),(NOT1 b₃₇) ) & ( $ AND4 b₄₀,b₃₉,(NOT1 b₃₈),(NOT1 b₃₇) implies $ b₂₉ ) & ( $ b₃₀ implies $ AND4 b₄₀,b₃₉,(NOT1 b₃₈),b₃₇ ) & ( $ AND4 b₄₀,b₃₉,(NOT1 b₃₈),b₃₇ implies $ b₃₀ ) & ( $ b₃₁ implies $ AND4 b₄₀,b₃₉,b₃₈,(NOT1 b₃₇) ) & ( $ AND4 b₄₀,b₃₉,b₃₈,(NOT1 b₃₇) implies $ b₃₁ ) & ( $ b₃₂ implies $ AND4 b₄₀,b₃₉,b₃₈,b₃₇ ) & ( $ AND4 b₄₀,b₃₉,b₃₈,b₃₇ implies $ b₃₂ ) & ( $ b₃₇ implies $ AND2 (NOT1 b₃₆),b₄₁ ) & ( $ AND2 (NOT1 b₃₆),b₄₁ implies $ b₃₇ ) & ( $ b₃₈ implies $ AND2 b₃₃,b₄₁ ) & ( $ AND2 b₃₃,b₄₁ implies $ b₃₈ ) & ( $ b₃₉ implies $ AND2 b₃₄,b₄₁ ) & ( $ AND2 b₃₄,b₄₁ implies $ b₃₉ ) & ( $ b₄₀ implies $ AND2 b₃₅,b₄₁ ) & ( $ AND2 b₃₅,b₄₁ implies $ b₄₀ ) & not ( ( $ b₁₈ implies $ AND2 b₁,b₄₁ ) & ( $ AND2 b₁,b₄₁ implies $ b₁₈ ) & ( $ b₂₀ implies $ AND2 b₂,b₄₁ ) & ( $ AND2 b₂,b₄₁ implies $ b₂₀ ) & ( $ b₂₄ implies $ AND2 b₄,b₄₁ ) & ( $ AND2 b₄,b₄₁ implies $ b₂₄ ) & ( $ b₃₂ implies $ AND2 b₈,b₄₁ ) & ( $ AND2 b₈,b₄₁ implies $ b₃₂ ) & ( $ b₃₁ implies $ AND2 b₁₆,b₄₁ ) & ( $ AND2 b₁₆,b₄₁ implies $ b₃₁ ) & ( $ b₂₉ implies $ AND2 b₁₅,b₄₁ ) & ( $ AND2 b₁₅,b₄₁ implies $ b₂₉ ) & ( $ b₂₅ implies $ AND2 b₁₃,b₄₁ ) & ( $ AND2 b₁₃,b₄₁ implies $ b₂₅ ) & ( $ b₁₇ implies $ OR2 (AND2 b₉,b₄₁),(NOT1 b₄₁) ) & ( $ OR2 (AND2 b₉,b₄₁),(NOT1 b₄₁) implies $ b₁₇ ) & ( $ b₂₂ implies $ AND2 b₃,b₄₁ ) & ( $ AND2 b₃,b₄₁ implies $ b₂₂ ) & ( $ b₂₈ implies $ AND2 b₆,b₄₁ ) & ( $ AND2 b₆,b₄₁ implies $ b₂₈ ) & ( $ b₂₃ implies $ AND2 b₁₂,b₄₁ ) & ( $ AND2 b₁₂,b₄₁ implies $ b₂₃ ) & ( $ b₃₀ implies $ AND2 b₇,b₄₁ ) & ( $ AND2 b₇,b₄₁ implies $ b₃₀ ) & ( $ b₂₇ implies $ AND2 b₁₄,b₄₁ ) & ( $ AND2 b₁₄,b₄₁ implies $ b₂₇ ) & ( $ b₂₁ implies $ AND2 b₁₁,b₄₁ ) & ( $ AND2 b₁₁,b₄₁ implies $ b₂₁ ) & ( $ b₂₆ implies $ AND2 b₅,b₄₁ ) & ( $ AND2 b₅,b₄₁ implies $ b₂₆ ) & ( $ b₁₉ implies $ AND2 b₁₀,b₄₁ ) & ( $ AND2 b₁₀,b₄₁ implies $ b₁₉ ) ) )