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 $ XOR2 b₁₇,b₁₈ ) & ( $ XOR2 b₁₇,b₁₈ implies $ b₂₁ ) & ( $ b₂₂ implies $ OR2 (AND2 b₁₉,(NOT1 b₁₇)),(AND2 b₁₇,(XOR2 b₁₈,b₁₉)) ) & ( $ OR2 (AND2 b₁₉,(NOT1 b₁₇)),(AND2 b₁₇,(XOR2 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₄ being set holds
( $ AND3 (AND2 b₁,b₂),(AND2 b₃,b₂),(AND2 b₄,b₂) iff $ AND2 (AND3 b₁,b₃,b₄),b₂ )

for b₁, b₂, b₃, b₄ being set holds
( ( not $ AND2 b₁,b₂ implies $ OR2 (NOT1 b₁),(NOT1 b₂) ) & ( $ OR2 (NOT1 b₁),(NOT1 b₂) implies not $ AND2 b₁,b₂ ) & ( $ OR2 b₁,b₂ & $ OR2 b₃,b₂ implies $ OR2 (AND2 b₁,b₃),b₂ ) & ( $ OR2 (AND2 b₁,b₃),b₂ implies ( $ OR2 b₁,b₂ & $ OR2 b₃,b₂ ) ) & ( $ OR2 b₁,b₂ & $ OR2 b₃,b₂ & $ OR2 b₄,b₂ implies $ OR2 (AND3 b₁,b₃,b₄),b₂ ) & ( $ OR2 (AND3 b₁,b₃,b₄),b₂ implies ( $ OR2 b₁,b₂ & $ OR2 b₃,b₂ & $ OR2 b₄,b₂ ) ) & not ( $ OR2 b₁,b₂ & ( $ b₁ implies $ b₃ ) & ( $ b₃ implies $ b₁ ) & not $ OR2 b₃,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 (XOR2 b₁₇,b₁₈),b₂₃ ) & ( $ AND2 (XOR2 b₁₇,b₁₈),b₂₃ implies $ b₂₁ ) & ( $ b₂₂ implies $ AND2 (OR2 (AND2 b₁₉,(NOT1 b₁₇)),(AND2 b₁₇,(XOR2 b₁₈,b₁₉))),b₂₃ ) & ( $ AND2 (OR2 (AND2 b₁₉,(NOT1 b₁₇)),(AND2 b₁₇,(XOR2 b₁₈,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 b₈,(NOT1 b₂₃) ) & ( $ OR2 b₈,(NOT1 b₂₃) implies $ b₉ ) ) )