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₃₈ being set st $ b₁ & $ b₁₃ & ( $ b₂₆ implies $ XOR2 b₃₈,(AND2 b₁,b₂₅) ) & ( $ XOR2 b₃₈,(AND2 b₁,b₂₅) implies $ b₂₆ ) & ( $ b₂₇ implies $ XOR2 b₁₄,(AND2 b₂,b₂₅) ) & ( $ XOR2 b₁₄,(AND2 b₂,b₂₅) implies $ b₂₇ ) & ( $ b₂₈ implies $ XOR2 b₁₅,(AND2 b₃,b₂₅) ) & ( $ XOR2 b₁₅,(AND2 b₃,b₂₅) implies $ b₂₈ ) & ( $ b₂₉ implies $ XOR2 b₁₆,(AND2 b₄,b₂₅) ) & ( $ XOR2 b₁₆,(AND2 b₄,b₂₅) implies $ b₂₉ ) & ( $ b₃₀ implies $ XOR2 b₁₇,(AND2 b₅,b₂₅) ) & ( $ XOR2 b₁₇,(AND2 b₅,b₂₅) implies $ b₃₀ ) & ( $ b₃₁ implies $ XOR2 b₁₈,(AND2 b₆,b₂₅) ) & ( $ XOR2 b₁₈,(AND2 b₆,b₂₅) implies $ b₃₁ ) & ( $ b₃₂ implies $ XOR2 b₁₉,(AND2 b₇,b₂₅) ) & ( $ XOR2 b₁₉,(AND2 b₇,b₂₅) implies $ b₃₂ ) & ( $ b₃₃ implies $ XOR2 b₂₀,(AND2 b₈,b₂₅) ) & ( $ XOR2 b₂₀,(AND2 b₈,b₂₅) implies $ b₃₃ ) & ( $ b₃₄ implies $ XOR2 b₂₁,(AND2 b₉,b₂₅) ) & ( $ XOR2 b₂₁,(AND2 b₉,b₂₅) implies $ b₃₄ ) & ( $ b₃₅ implies $ XOR2 b₂₂,(AND2 b₁₀,b₂₅) ) & ( $ XOR2 b₂₂,(AND2 b₁₀,b₂₅) implies $ b₃₅ ) & ( $ b₃₆ implies $ XOR2 b₂₃,(AND2 b₁₁,b₂₅) ) & ( $ XOR2 b₂₃,(AND2 b₁₁,b₂₅) implies $ b₃₆ ) & ( $ b₃₇ implies $ XOR2 b₂₄,(AND2 b₁₂,b₂₅) ) & ( $ XOR2 b₂₄,(AND2 b₁₂,b₂₅) implies $ b₃₇ ) holds
( ( $ b₂₅ implies $ AND2 b₁₃,b₂₅ ) & ( $ AND2 b₁₃,b₂₅ implies $ b₂₅ ) & ( $ b₂₄ implies $ XOR2 b₃₇,(AND2 b₁₂,b₂₅) ) & ( $ XOR2 b₃₇,(AND2 b₁₂,b₂₅) implies $ b₂₄ ) & ( $ b₂₃ implies $ XOR2 b₃₆,(AND2 b₁₁,b₂₅) ) & ( $ XOR2 b₃₆,(AND2 b₁₁,b₂₅) implies $ b₂₃ ) & ( $ b₂₂ implies $ XOR2 b₃₅,(AND2 b₁₀,b₂₅) ) & ( $ XOR2 b₃₅,(AND2 b₁₀,b₂₅) implies $ b₂₂ ) & ( $ b₂₁ implies $ XOR2 b₃₄,(AND2 b₉,b₂₅) ) & ( $ XOR2 b₃₄,(AND2 b₉,b₂₅) implies $ b₂₁ ) & ( $ b₂₀ implies $ XOR2 b₃₃,(AND2 b₈,b₂₅) ) & ( $ XOR2 b₃₃,(AND2 b₈,b₂₅) implies $ b₂₀ ) & ( $ b₁₉ implies $ XOR2 b₃₂,(AND2 b₇,b₂₅) ) & ( $ XOR2 b₃₂,(AND2 b₇,b₂₅) implies $ b₁₉ ) & ( $ b₁₈ implies $ XOR2 b₃₁,(AND2 b₆,b₂₅) ) & ( $ XOR2 b₃₁,(AND2 b₆,b₂₅) implies $ b₁₈ ) & ( $ b₁₇ implies $ XOR2 b₃₀,(AND2 b₅,b₂₅) ) & ( $ XOR2 b₃₀,(AND2 b₅,b₂₅) implies $ b₁₇ ) & ( $ b₁₆ implies $ XOR2 b₂₉,(AND2 b₄,b₂₅) ) & ( $ XOR2 b₂₉,(AND2 b₄,b₂₅) implies $ b₁₆ ) & ( $ b₁₅ implies $ XOR2 b₂₈,(AND2 b₃,b₂₅) ) & ( $ XOR2 b₂₈,(AND2 b₃,b₂₅) implies $ b₁₅ ) & ( $ b₁₄ implies $ XOR2 b₂₇,(AND2 b₂,b₂₅) ) & ( $ XOR2 b₂₇,(AND2 b₂,b₂₅) implies $ b₁₄ ) & ( $ b₃₈ implies $ XOR2 b₂₆,(AND2 b₁,b₂₅) ) & ( $ XOR2 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₄₀, b₄₁, b₄₂, b₄₃, b₄₄, b₄₅, b₄₆, b₄₇, b₄₈, b₄₉, b₅₀ being set st $ b₁ & $ b₁₇ & ( $ b₃₄ implies $ XOR2 b₅₀,(AND2 b₁,b₃₃) ) & ( $ XOR2 b₅₀,(AND2 b₁,b₃₃) implies $ b₃₄ ) & ( $ b₃₅ implies $ XOR2 b₁₈,(AND2 b₂,b₃₃) ) & ( $ XOR2 b₁₈,(AND2 b₂,b₃₃) implies $ b₃₅ ) & ( $ b₃₆ implies $ XOR2 b₁₉,(AND2 b₃,b₃₃) ) & ( $ XOR2 b₁₉,(AND2 b₃,b₃₃) implies $ b₃₆ ) & ( $ b₃₇ implies $ XOR2 b₂₀,(AND2 b₄,b₃₃) ) & ( $ XOR2 b₂₀,(AND2 b₄,b₃₃) implies $ b₃₇ ) & ( $ b₃₈ implies $ XOR2 b₂₁,(AND2 b₅,b₃₃) ) & ( $ XOR2 b₂₁,(AND2 b₅,b₃₃) implies $ b₃₈ ) & ( $ b₃₉ implies $ XOR2 b₂₂,(AND2 b₆,b₃₃) ) & ( $ XOR2 b₂₂,(AND2 b₆,b₃₃) implies $ b₃₉ ) & ( $ b₄₀ implies $ XOR2 b₂₃,(AND2 b₇,b₃₃) ) & ( $ XOR2 b₂₃,(AND2 b₇,b₃₃) implies $ b₄₀ ) & ( $ b₄₁ implies $ XOR2 b₂₄,(AND2 b₈,b₃₃) ) & ( $ XOR2 b₂₄,(AND2 b₈,b₃₃) implies $ b₄₁ ) & ( $ b₄₂ implies $ XOR2 b₂₅,(AND2 b₉,b₃₃) ) & ( $ XOR2 b₂₅,(AND2 b₉,b₃₃) implies $ b₄₂ ) & ( $ b₄₃ implies $ XOR2 b₂₆,(AND2 b₁₀,b₃₃) ) & ( $ XOR2 b₂₆,(AND2 b₁₀,b₃₃) implies $ b₄₃ ) & ( $ b₄₄ implies $ XOR2 b₂₇,(AND2 b₁₁,b₃₃) ) & ( $ XOR2 b₂₇,(AND2 b₁₁,b₃₃) implies $ b₄₄ ) & ( $ b₄₅ implies $ XOR2 b₂₈,(AND2 b₁₂,b₃₃) ) & ( $ XOR2 b₂₈,(AND2 b₁₂,b₃₃) implies $ b₄₅ ) & ( $ b₄₆ implies $ XOR2 b₂₉,(AND2 b₁₃,b₃₃) ) & ( $ XOR2 b₂₉,(AND2 b₁₃,b₃₃) implies $ b₄₆ ) & ( $ b₄₇ implies $ XOR2 b₃₀,(AND2 b₁₄,b₃₃) ) & ( $ XOR2 b₃₀,(AND2 b₁₄,b₃₃) implies $ b₄₇ ) & ( $ b₄₈ implies $ XOR2 b₃₁,(AND2 b₁₅,b₃₃) ) & ( $ XOR2 b₃₁,(AND2 b₁₅,b₃₃) implies $ b₄₈ ) & ( $ b₄₉ implies $ XOR2 b₃₂,(AND2 b₁₆,b₃₃) ) & ( $ XOR2 b₃₂,(AND2 b₁₆,b₃₃) implies $ b₄₉ ) holds
( ( $ b₃₃ implies $ AND2 b₁₇,b₃₃ ) & ( $ AND2 b₁₇,b₃₃ implies $ b₃₃ ) & ( $ b₃₂ implies $ XOR2 b₄₉,(AND2 b₁₆,b₃₃) ) & ( $ XOR2 b₄₉,(AND2 b₁₆,b₃₃) implies $ b₃₂ ) & ( $ b₃₁ implies $ XOR2 b₄₈,(AND2 b₁₅,b₃₃) ) & ( $ XOR2 b₄₈,(AND2 b₁₅,b₃₃) implies $ b₃₁ ) & ( $ b₃₀ implies $ XOR2 b₄₇,(AND2 b₁₄,b₃₃) ) & ( $ XOR2 b₄₇,(AND2 b₁₄,b₃₃) implies $ b₃₀ ) & ( $ b₂₉ implies $ XOR2 b₄₆,(AND2 b₁₃,b₃₃) ) & ( $ XOR2 b₄₆,(AND2 b₁₃,b₃₃) implies $ b₂₉ ) & ( $ b₂₈ implies $ XOR2 b₄₅,(AND2 b₁₂,b₃₃) ) & ( $ XOR2 b₄₅,(AND2 b₁₂,b₃₃) implies $ b₂₈ ) & ( $ b₂₇ implies $ XOR2 b₄₄,(AND2 b₁₁,b₃₃) ) & ( $ XOR2 b₄₄,(AND2 b₁₁,b₃₃) implies $ b₂₇ ) & ( $ b₂₆ implies $ XOR2 b₄₃,(AND2 b₁₀,b₃₃) ) & ( $ XOR2 b₄₃,(AND2 b₁₀,b₃₃) implies $ b₂₆ ) & ( $ b₂₅ implies $ XOR2 b₄₂,(AND2 b₉,b₃₃) ) & ( $ XOR2 b₄₂,(AND2 b₉,b₃₃) implies $ b₂₅ ) & ( $ b₂₄ implies $ XOR2 b₄₁,(AND2 b₈,b₃₃) ) & ( $ XOR2 b₄₁,(AND2 b₈,b₃₃) implies $ b₂₄ ) & ( $ b₂₃ implies $ XOR2 b₄₀,(AND2 b₇,b₃₃) ) & ( $ XOR2 b₄₀,(AND2 b₇,b₃₃) implies $ b₂₃ ) & ( $ b₂₂ implies $ XOR2 b₃₉,(AND2 b₆,b₃₃) ) & ( $ XOR2 b₃₉,(AND2 b₆,b₃₃) implies $ b₂₂ ) & ( $ b₂₁ implies $ XOR2 b₃₈,(AND2 b₅,b₃₃) ) & ( $ XOR2 b₃₈,(AND2 b₅,b₃₃) implies $ b₂₁ ) & ( $ b₂₀ implies $ XOR2 b₃₇,(AND2 b₄,b₃₃) ) & ( $ XOR2 b₃₇,(AND2 b₄,b₃₃) implies $ b₂₀ ) & ( $ b₁₉ implies $ XOR2 b₃₆,(AND2 b₃,b₃₃) ) & ( $ XOR2 b₃₆,(AND2 b₃,b₃₃) implies $ b₁₉ ) & ( $ b₁₈ implies $ XOR2 b₃₅,(AND2 b₂,b₃₃) ) & ( $ XOR2 b₃₅,(AND2 b₂,b₃₃) implies $ b₁₈ ) & ( $ b₅₀ implies $ XOR2 b₃₄,(AND2 b₁,b₃₃) ) & ( $ XOR2 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₃₉ being set st $ b₁ & $ b₁₃ & not $ b₃₈ & ( $ b₂₆ implies $ XOR2 b₃₉,b₂₅ ) & ( $ XOR2 b₃₉,b₂₅ implies $ b₂₆ ) & ( $ b₂₇ implies $ XOR2 b₁₄,(AND2 b₂,b₂₆) ) & ( $ XOR2 b₁₄,(AND2 b₂,b₂₆) implies $ b₂₇ ) & ( $ b₂₈ implies $ XOR2 b₁₅,(AND2 b₃,b₂₆) ) & ( $ XOR2 b₁₅,(AND2 b₃,b₂₆) implies $ b₂₈ ) & ( $ b₂₉ implies $ XOR2 b₁₆,(AND2 b₄,b₂₆) ) & ( $ XOR2 b₁₆,(AND2 b₄,b₂₆) implies $ b₂₉ ) & ( $ b₃₀ implies $ XOR2 b₁₇,(AND2 b₅,b₂₆) ) & ( $ XOR2 b₁₇,(AND2 b₅,b₂₆) implies $ b₃₀ ) & ( $ b₃₁ implies $ XOR2 b₁₈,(AND2 b₆,b₂₆) ) & ( $ XOR2 b₁₈,(AND2 b₆,b₂₆) implies $ b₃₁ ) & ( $ b₃₂ implies $ XOR2 b₁₉,(AND2 b₇,b₂₆) ) & ( $ XOR2 b₁₉,(AND2 b₇,b₂₆) implies $ b₃₂ ) & ( $ b₃₃ implies $ XOR2 b₂₀,(AND2 b₈,b₂₆) ) & ( $ XOR2 b₂₀,(AND2 b₈,b₂₆) implies $ b₃₃ ) & ( $ b₃₄ implies $ XOR2 b₂₁,(AND2 b₉,b₂₆) ) & ( $ XOR2 b₂₁,(AND2 b₉,b₂₆) implies $ b₃₄ ) & ( $ b₃₅ implies $ XOR2 b₂₂,(AND2 b₁₀,b₂₆) ) & ( $ XOR2 b₂₂,(AND2 b₁₀,b₂₆) implies $ b₃₅ ) & ( $ b₃₆ implies $ XOR2 b₂₃,(AND2 b₁₁,b₂₆) ) & ( $ XOR2 b₂₃,(AND2 b₁₁,b₂₆) implies $ b₃₆ ) & ( $ b₃₇ implies $ XOR2 b₂₄,(AND2 b₁₂,b₂₆) ) & ( $ XOR2 b₂₄,(AND2 b₁₂,b₂₆) implies $ b₃₇ ) holds
( ( $ b₃₇ implies $ XOR2 (XOR2 b₂₄,(AND2 b₁₂,b₂₅)),(XOR2 b₃₈,(AND2 b₁₂,b₃₉)) ) & ( $ XOR2 (XOR2 b₂₄,(AND2 b₁₂,b₂₅)),(XOR2 b₃₈,(AND2 b₁₂,b₃₉)) implies $ b₃₇ ) & ( $ b₃₆ implies $ XOR2 (XOR2 b₂₃,(AND2 b₁₁,b₂₅)),(XOR2 b₃₈,(AND2 b₁₁,b₃₉)) ) & ( $ XOR2 (XOR2 b₂₃,(AND2 b₁₁,b₂₅)),(XOR2 b₃₈,(AND2 b₁₁,b₃₉)) implies $ b₃₆ ) & ( $ b₃₅ implies $ XOR2 (XOR2 b₂₂,(AND2 b₁₀,b₂₅)),(XOR2 b₃₈,(AND2 b₁₀,b₃₉)) ) & ( $ XOR2 (XOR2 b₂₂,(AND2 b₁₀,b₂₅)),(XOR2 b₃₈,(AND2 b₁₀,b₃₉)) implies $ b₃₅ ) & ( $ b₃₄ implies $ XOR2 (XOR2 b₂₁,(AND2 b₉,b₂₅)),(XOR2 b₃₈,(AND2 b₉,b₃₉)) ) & ( $ XOR2 (XOR2 b₂₁,(AND2 b₉,b₂₅)),(XOR2 b₃₈,(AND2 b₉,b₃₉)) implies $ b₃₄ ) & ( $ b₃₃ implies $ XOR2 (XOR2 b₂₀,(AND2 b₈,b₂₅)),(XOR2 b₃₈,(AND2 b₈,b₃₉)) ) & ( $ XOR2 (XOR2 b₂₀,(AND2 b₈,b₂₅)),(XOR2 b₃₈,(AND2 b₈,b₃₉)) implies $ b₃₃ ) & ( $ b₃₂ implies $ XOR2 (XOR2 b₁₉,(AND2 b₇,b₂₅)),(XOR2 b₃₈,(AND2 b₇,b₃₉)) ) & ( $ XOR2 (XOR2 b₁₉,(AND2 b₇,b₂₅)),(XOR2 b₃₈,(AND2 b₇,b₃₉)) implies $ b₃₂ ) & ( $ b₃₁ implies $ XOR2 (XOR2 b₁₈,(AND2 b₆,b₂₅)),(XOR2 b₃₈,(AND2 b₆,b₃₉)) ) & ( $ XOR2 (XOR2 b₁₈,(AND2 b₆,b₂₅)),(XOR2 b₃₈,(AND2 b₆,b₃₉)) implies $ b₃₁ ) & ( $ b₃₀ implies $ XOR2 (XOR2 b₁₇,(AND2 b₅,b₂₅)),(XOR2 b₃₈,(AND2 b₅,b₃₉)) ) & ( $ XOR2 (XOR2 b₁₇,(AND2 b₅,b₂₅)),(XOR2 b₃₈,(AND2 b₅,b₃₉)) implies $ b₃₀ ) & ( $ b₂₉ implies $ XOR2 (XOR2 b₁₆,(AND2 b₄,b₂₅)),(XOR2 b₃₈,(AND2 b₄,b₃₉)) ) & ( $ XOR2 (XOR2 b₁₆,(AND2 b₄,b₂₅)),(XOR2 b₃₈,(AND2 b₄,b₃₉)) implies $ b₂₉ ) & ( $ b₂₈ implies $ XOR2 (XOR2 b₁₅,(AND2 b₃,b₂₅)),(XOR2 b₃₈,(AND2 b₃,b₃₉)) ) & ( $ XOR2 (XOR2 b₁₅,(AND2 b₃,b₂₅)),(XOR2 b₃₈,(AND2 b₃,b₃₉)) implies $ b₂₈ ) & ( $ b₂₇ implies $ XOR2 (XOR2 b₁₄,(AND2 b₂,b₂₅)),(XOR2 b₃₈,(AND2 b₂,b₃₉)) ) & ( $ XOR2 (XOR2 b₁₄,(AND2 b₂,b₂₅)),(XOR2 b₃₈,(AND2 b₂,b₃₉)) implies $ b₂₇ ) & ( $ b₂₆ implies $ XOR2 (XOR2 b₃₈,(AND2 b₁,b₂₅)),(XOR2 b₃₈,(AND2 b₁,b₃₉)) ) & ( $ XOR2 (XOR2 b₃₈,(AND2 b₁,b₂₅)),(XOR2 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₄₀, b₄₁, b₄₂, b₄₃, b₄₄, b₄₅, b₄₆, b₄₇, b₄₈, b₄₉, b₅₀, b₅₁ being set st $ b₁ & $ b₁₇ & not $ b₅₀ & ( $ b₃₄ implies $ XOR2 b₅₁,b₃₃ ) & ( $ XOR2 b₅₁,b₃₃ implies $ b₃₄ ) & ( $ b₃₅ implies $ XOR2 b₁₈,(AND2 b₂,b₃₄) ) & ( $ XOR2 b₁₈,(AND2 b₂,b₃₄) implies $ b₃₅ ) & ( $ b₃₆ implies $ XOR2 b₁₉,(AND2 b₃,b₃₄) ) & ( $ XOR2 b₁₉,(AND2 b₃,b₃₄) implies $ b₃₆ ) & ( $ b₃₇ implies $ XOR2 b₂₀,(AND2 b₄,b₃₄) ) & ( $ XOR2 b₂₀,(AND2 b₄,b₃₄) implies $ b₃₇ ) & ( $ b₃₈ implies $ XOR2 b₂₁,(AND2 b₅,b₃₄) ) & ( $ XOR2 b₂₁,(AND2 b₅,b₃₄) implies $ b₃₈ ) & ( $ b₃₉ implies $ XOR2 b₂₂,(AND2 b₆,b₃₄) ) & ( $ XOR2 b₂₂,(AND2 b₆,b₃₄) implies $ b₃₉ ) & ( $ b₄₀ implies $ XOR2 b₂₃,(AND2 b₇,b₃₄) ) & ( $ XOR2 b₂₃,(AND2 b₇,b₃₄) implies $ b₄₀ ) & ( $ b₄₁ implies $ XOR2 b₂₄,(AND2 b₈,b₃₄) ) & ( $ XOR2 b₂₄,(AND2 b₈,b₃₄) implies $ b₄₁ ) & ( $ b₄₂ implies $ XOR2 b₂₅,(AND2 b₉,b₃₄) ) & ( $ XOR2 b₂₅,(AND2 b₉,b₃₄) implies $ b₄₂ ) & ( $ b₄₃ implies $ XOR2 b₂₆,(AND2 b₁₀,b₃₄) ) & ( $ XOR2 b₂₆,(AND2 b₁₀,b₃₄) implies $ b₄₃ ) & ( $ b₄₄ implies $ XOR2 b₂₇,(AND2 b₁₁,b₃₄) ) & ( $ XOR2 b₂₇,(AND2 b₁₁,b₃₄) implies $ b₄₄ ) & ( $ b₄₅ implies $ XOR2 b₂₈,(AND2 b₁₂,b₃₄) ) & ( $ XOR2 b₂₈,(AND2 b₁₂,b₃₄) implies $ b₄₅ ) & ( $ b₄₆ implies $ XOR2 b₂₉,(AND2 b₁₃,b₃₄) ) & ( $ XOR2 b₂₉,(AND2 b₁₃,b₃₄) implies $ b₄₆ ) & ( $ b₄₇ implies $ XOR2 b₃₀,(AND2 b₁₄,b₃₄) ) & ( $ XOR2 b₃₀,(AND2 b₁₄,b₃₄) implies $ b₄₇ ) & ( $ b₄₈ implies $ XOR2 b₃₁,(AND2 b₁₅,b₃₄) ) & ( $ XOR2 b₃₁,(AND2 b₁₅,b₃₄) implies $ b₄₈ ) & ( $ b₄₉ implies $ XOR2 b₃₂,(AND2 b₁₆,b₃₄) ) & ( $ XOR2 b₃₂,(AND2 b₁₆,b₃₄) implies $ b₄₉ ) holds
( ( $ b₄₉ implies $ XOR2 (XOR2 b₃₂,(AND2 b₁₆,b₃₃)),(XOR2 b₅₀,(AND2 b₁₆,b₅₁)) ) & ( $ XOR2 (XOR2 b₃₂,(AND2 b₁₆,b₃₃)),(XOR2 b₅₀,(AND2 b₁₆,b₅₁)) implies $ b₄₉ ) & ( $ b₄₈ implies $ XOR2 (XOR2 b₃₁,(AND2 b₁₅,b₃₃)),(XOR2 b₅₀,(AND2 b₁₅,b₅₁)) ) & ( $ XOR2 (XOR2 b₃₁,(AND2 b₁₅,b₃₃)),(XOR2 b₅₀,(AND2 b₁₅,b₅₁)) implies $ b₄₈ ) & ( $ b₄₇ implies $ XOR2 (XOR2 b₃₀,(AND2 b₁₄,b₃₃)),(XOR2 b₅₀,(AND2 b₁₄,b₅₁)) ) & ( $ XOR2 (XOR2 b₃₀,(AND2 b₁₄,b₃₃)),(XOR2 b₅₀,(AND2 b₁₄,b₅₁)) implies $ b₄₇ ) & ( $ b₄₆ implies $ XOR2 (XOR2 b₂₉,(AND2 b₁₃,b₃₃)),(XOR2 b₅₀,(AND2 b₁₃,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₉,(AND2 b₁₃,b₃₃)),(XOR2 b₅₀,(AND2 b₁₃,b₅₁)) implies $ b₄₆ ) & ( $ b₄₅ implies $ XOR2 (XOR2 b₂₈,(AND2 b₁₂,b₃₃)),(XOR2 b₅₀,(AND2 b₁₂,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₈,(AND2 b₁₂,b₃₃)),(XOR2 b₅₀,(AND2 b₁₂,b₅₁)) implies $ b₄₅ ) & ( $ b₄₄ implies $ XOR2 (XOR2 b₂₇,(AND2 b₁₁,b₃₃)),(XOR2 b₅₀,(AND2 b₁₁,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₇,(AND2 b₁₁,b₃₃)),(XOR2 b₅₀,(AND2 b₁₁,b₅₁)) implies $ b₄₄ ) & ( $ b₄₃ implies $ XOR2 (XOR2 b₂₆,(AND2 b₁₀,b₃₃)),(XOR2 b₅₀,(AND2 b₁₀,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₆,(AND2 b₁₀,b₃₃)),(XOR2 b₅₀,(AND2 b₁₀,b₅₁)) implies $ b₄₃ ) & ( $ b₄₂ implies $ XOR2 (XOR2 b₂₅,(AND2 b₉,b₃₃)),(XOR2 b₅₀,(AND2 b₉,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₅,(AND2 b₉,b₃₃)),(XOR2 b₅₀,(AND2 b₉,b₅₁)) implies $ b₄₂ ) & ( $ b₄₁ implies $ XOR2 (XOR2 b₂₄,(AND2 b₈,b₃₃)),(XOR2 b₅₀,(AND2 b₈,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₄,(AND2 b₈,b₃₃)),(XOR2 b₅₀,(AND2 b₈,b₅₁)) implies $ b₄₁ ) & ( $ b₄₀ implies $ XOR2 (XOR2 b₂₃,(AND2 b₇,b₃₃)),(XOR2 b₅₀,(AND2 b₇,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₃,(AND2 b₇,b₃₃)),(XOR2 b₅₀,(AND2 b₇,b₅₁)) implies $ b₄₀ ) & ( $ b₃₉ implies $ XOR2 (XOR2 b₂₂,(AND2 b₆,b₃₃)),(XOR2 b₅₀,(AND2 b₆,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₂,(AND2 b₆,b₃₃)),(XOR2 b₅₀,(AND2 b₆,b₅₁)) implies $ b₃₉ ) & ( $ b₃₈ implies $ XOR2 (XOR2 b₂₁,(AND2 b₅,b₃₃)),(XOR2 b₅₀,(AND2 b₅,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₁,(AND2 b₅,b₃₃)),(XOR2 b₅₀,(AND2 b₅,b₅₁)) implies $ b₃₈ ) & ( $ b₃₇ implies $ XOR2 (XOR2 b₂₀,(AND2 b₄,b₃₃)),(XOR2 b₅₀,(AND2 b₄,b₅₁)) ) & ( $ XOR2 (XOR2 b₂₀,(AND2 b₄,b₃₃)),(XOR2 b₅₀,(AND2 b₄,b₅₁)) implies $ b₃₇ ) & ( $ b₃₆ implies $ XOR2 (XOR2 b₁₉,(AND2 b₃,b₃₃)),(XOR2 b₅₀,(AND2 b₃,b₅₁)) ) & ( $ XOR2 (XOR2 b₁₉,(AND2 b₃,b₃₃)),(XOR2 b₅₀,(AND2 b₃,b₅₁)) implies $ b₃₆ ) & ( $ b₃₅ implies $ XOR2 (XOR2 b₁₈,(AND2 b₂,b₃₃)),(XOR2 b₅₀,(AND2 b₂,b₅₁)) ) & ( $ XOR2 (XOR2 b₁₈,(AND2 b₂,b₃₃)),(XOR2 b₅₀,(AND2 b₂,b₅₁)) implies $ b₃₅ ) & ( $ b₃₄ implies $ XOR2 (XOR2 b₅₀,(AND2 b₁,b₃₃)),(XOR2 b₅₀,(AND2 b₁,b₅₁)) ) & ( $ XOR2 (XOR2 b₅₀,(AND2 b₁,b₃₃)),(XOR2 b₅₀,(AND2 b₁,b₅₁)) implies $ b₃₄ ) )