for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, p being ( ( ) ( ) set ) holds
not ( not g12 : ( ( ) ( ) set ) is empty & ( not b0 : ( ( ) ( ) set ) is empty implies not XOR2 (p : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (p : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b0 : ( ( ) ( ) set ) is empty ) & ( not b1 : ( ( ) ( ) set ) is empty implies not XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b1 : ( ( ) ( ) set ) is empty ) & ( not b2 : ( ( ) ( ) set ) is empty implies not XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b2 : ( ( ) ( ) set ) is empty ) & ( not b3 : ( ( ) ( ) set ) is empty implies not XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b3 : ( ( ) ( ) set ) is empty ) & ( not b4 : ( ( ) ( ) set ) is empty implies not XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b4 : ( ( ) ( ) set ) is empty ) & ( not b5 : ( ( ) ( ) set ) is empty implies not XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b5 : ( ( ) ( ) set ) is empty ) & ( not b6 : ( ( ) ( ) set ) is empty implies not XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b6 : ( ( ) ( ) set ) is empty ) & ( not b7 : ( ( ) ( ) set ) is empty implies not XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b7 : ( ( ) ( ) set ) is empty ) & ( not b8 : ( ( ) ( ) set ) is empty implies not XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b8 : ( ( ) ( ) set ) is empty ) & ( not b9 : ( ( ) ( ) set ) is empty implies not XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b9 : ( ( ) ( ) set ) is empty ) & ( not b10 : ( ( ) ( ) set ) is empty implies not XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b10 : ( ( ) ( ) set ) is empty ) & ( not b11 : ( ( ) ( ) set ) is empty implies not XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b11 : ( ( ) ( ) set ) is empty ) & not ( ( not a11 : ( ( ) ( ) set ) is empty implies not AND2 (g12 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (g12 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a11 : ( ( ) ( ) set ) is empty ) & ( not a10 : ( ( ) ( ) set ) is empty implies not XOR2 (b11 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b11 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a10 : ( ( ) ( ) set ) is empty ) & ( not a9 : ( ( ) ( ) set ) is empty implies not XOR2 (b10 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b10 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a9 : ( ( ) ( ) set ) is empty ) & ( not a8 : ( ( ) ( ) set ) is empty implies not XOR2 (b9 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b9 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a8 : ( ( ) ( ) set ) is empty ) & ( not a7 : ( ( ) ( ) set ) is empty implies not XOR2 (b8 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b8 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a7 : ( ( ) ( ) set ) is empty ) & ( not a6 : ( ( ) ( ) set ) is empty implies not XOR2 (b7 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b7 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a6 : ( ( ) ( ) set ) is empty ) & ( not a5 : ( ( ) ( ) set ) is empty implies not XOR2 (b6 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b6 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a5 : ( ( ) ( ) set ) is empty ) & ( not a4 : ( ( ) ( ) set ) is empty implies not XOR2 (b5 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b5 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a4 : ( ( ) ( ) set ) is empty ) & ( not a3 : ( ( ) ( ) set ) is empty implies not XOR2 (b4 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b4 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a3 : ( ( ) ( ) set ) is empty ) & ( not a2 : ( ( ) ( ) set ) is empty implies not XOR2 (b3 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b3 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a2 : ( ( ) ( ) set ) is empty ) & ( not a1 : ( ( ) ( ) set ) is empty implies not XOR2 (b2 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b2 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a1 : ( ( ) ( ) set ) is empty ) & ( not a0 : ( ( ) ( ) set ) is empty implies not XOR2 (b1 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b1 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a0 : ( ( ) ( ) set ) is empty ) & ( not p : ( ( ) ( ) set ) is empty implies not XOR2 (b0 : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b0 : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not p : ( ( ) ( ) set ) is empty ) ) ) ;

for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, p being ( ( ) ( ) set ) holds
not ( not g16 : ( ( ) ( ) set ) is empty & ( not b0 : ( ( ) ( ) set ) is empty implies not XOR2 (p : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (p : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b0 : ( ( ) ( ) set ) is empty ) & ( not b1 : ( ( ) ( ) set ) is empty implies not XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b1 : ( ( ) ( ) set ) is empty ) & ( not b2 : ( ( ) ( ) set ) is empty implies not XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b2 : ( ( ) ( ) set ) is empty ) & ( not b3 : ( ( ) ( ) set ) is empty implies not XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b3 : ( ( ) ( ) set ) is empty ) & ( not b4 : ( ( ) ( ) set ) is empty implies not XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b4 : ( ( ) ( ) set ) is empty ) & ( not b5 : ( ( ) ( ) set ) is empty implies not XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b5 : ( ( ) ( ) set ) is empty ) & ( not b6 : ( ( ) ( ) set ) is empty implies not XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b6 : ( ( ) ( ) set ) is empty ) & ( not b7 : ( ( ) ( ) set ) is empty implies not XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b7 : ( ( ) ( ) set ) is empty ) & ( not b8 : ( ( ) ( ) set ) is empty implies not XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b8 : ( ( ) ( ) set ) is empty ) & ( not b9 : ( ( ) ( ) set ) is empty implies not XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b9 : ( ( ) ( ) set ) is empty ) & ( not b10 : ( ( ) ( ) set ) is empty implies not XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b10 : ( ( ) ( ) set ) is empty ) & ( not b11 : ( ( ) ( ) set ) is empty implies not XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b11 : ( ( ) ( ) set ) is empty ) & ( not b12 : ( ( ) ( ) set ) is empty implies not XOR2 (a11 : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a11 : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b12 : ( ( ) ( ) set ) is empty ) & ( not b13 : ( ( ) ( ) set ) is empty implies not XOR2 (a12 : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a12 : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b13 : ( ( ) ( ) set ) is empty ) & ( not b14 : ( ( ) ( ) set ) is empty implies not XOR2 (a13 : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a13 : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b14 : ( ( ) ( ) set ) is empty ) & ( not b15 : ( ( ) ( ) set ) is empty implies not XOR2 (a14 : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a14 : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b15 : ( ( ) ( ) set ) is empty ) & not ( ( not a15 : ( ( ) ( ) set ) is empty implies not AND2 (g16 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (g16 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a15 : ( ( ) ( ) set ) is empty ) & ( not a14 : ( ( ) ( ) set ) is empty implies not XOR2 (b15 : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b15 : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a14 : ( ( ) ( ) set ) is empty ) & ( not a13 : ( ( ) ( ) set ) is empty implies not XOR2 (b14 : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b14 : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a13 : ( ( ) ( ) set ) is empty ) & ( not a12 : ( ( ) ( ) set ) is empty implies not XOR2 (b13 : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b13 : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a12 : ( ( ) ( ) set ) is empty ) & ( not a11 : ( ( ) ( ) set ) is empty implies not XOR2 (b12 : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b12 : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a11 : ( ( ) ( ) set ) is empty ) & ( not a10 : ( ( ) ( ) set ) is empty implies not XOR2 (b11 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b11 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a10 : ( ( ) ( ) set ) is empty ) & ( not a9 : ( ( ) ( ) set ) is empty implies not XOR2 (b10 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b10 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a9 : ( ( ) ( ) set ) is empty ) & ( not a8 : ( ( ) ( ) set ) is empty implies not XOR2 (b9 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b9 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a8 : ( ( ) ( ) set ) is empty ) & ( not a7 : ( ( ) ( ) set ) is empty implies not XOR2 (b8 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b8 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a7 : ( ( ) ( ) set ) is empty ) & ( not a6 : ( ( ) ( ) set ) is empty implies not XOR2 (b7 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b7 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a6 : ( ( ) ( ) set ) is empty ) & ( not a5 : ( ( ) ( ) set ) is empty implies not XOR2 (b6 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b6 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a5 : ( ( ) ( ) set ) is empty ) & ( not a4 : ( ( ) ( ) set ) is empty implies not XOR2 (b5 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b5 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a4 : ( ( ) ( ) set ) is empty ) & ( not a3 : ( ( ) ( ) set ) is empty implies not XOR2 (b4 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b4 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a3 : ( ( ) ( ) set ) is empty ) & ( not a2 : ( ( ) ( ) set ) is empty implies not XOR2 (b3 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b3 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a2 : ( ( ) ( ) set ) is empty ) & ( not a1 : ( ( ) ( ) set ) is empty implies not XOR2 (b2 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b2 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a1 : ( ( ) ( ) set ) is empty ) & ( not a0 : ( ( ) ( ) set ) is empty implies not XOR2 (b1 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b1 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not a0 : ( ( ) ( ) set ) is empty ) & ( not p : ( ( ) ( ) set ) is empty implies not XOR2 (b0 : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (b0 : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not p : ( ( ) ( ) set ) is empty ) ) ) ;

for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, z, p being ( ( ) ( ) set ) st not g0 : ( ( ) ( ) set ) is empty & z : ( ( ) ( ) set ) is empty & ( not b0 : ( ( ) ( ) set ) is empty implies not XOR2 (p : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (p : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b0 : ( ( ) ( ) set ) is empty ) & ( not b1 : ( ( ) ( ) set ) is empty implies not XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b1 : ( ( ) ( ) set ) is empty ) & ( not b2 : ( ( ) ( ) set ) is empty implies not XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b2 : ( ( ) ( ) set ) is empty ) & ( not b3 : ( ( ) ( ) set ) is empty implies not XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b3 : ( ( ) ( ) set ) is empty ) & ( not b4 : ( ( ) ( ) set ) is empty implies not XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b4 : ( ( ) ( ) set ) is empty ) & ( not b5 : ( ( ) ( ) set ) is empty implies not XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b5 : ( ( ) ( ) set ) is empty ) & ( not b6 : ( ( ) ( ) set ) is empty implies not XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b6 : ( ( ) ( ) set ) is empty ) & ( not b7 : ( ( ) ( ) set ) is empty implies not XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b7 : ( ( ) ( ) set ) is empty ) & ( not b8 : ( ( ) ( ) set ) is empty implies not XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b8 : ( ( ) ( ) set ) is empty ) & ( not b9 : ( ( ) ( ) set ) is empty implies not XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b9 : ( ( ) ( ) set ) is empty ) & ( not b10 : ( ( ) ( ) set ) is empty implies not XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b10 : ( ( ) ( ) set ) is empty ) & ( not b11 : ( ( ) ( ) set ) is empty implies not XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b11 : ( ( ) ( ) set ) is empty ) holds
( ( not b11 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b11 : ( ( ) ( ) set ) is empty ) & ( not b10 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b10 : ( ( ) ( ) set ) is empty ) & ( not b9 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b9 : ( ( ) ( ) set ) is empty ) & ( not b8 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b8 : ( ( ) ( ) set ) is empty ) & ( not b7 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b7 : ( ( ) ( ) set ) is empty ) & ( not b6 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b6 : ( ( ) ( ) set ) is empty ) & ( not b5 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b5 : ( ( ) ( ) set ) is empty ) & ( not b4 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b4 : ( ( ) ( ) set ) is empty ) & ( not b3 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b3 : ( ( ) ( ) set ) is empty ) & ( not b2 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b2 : ( ( ) ( ) set ) is empty ) & ( not b1 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b1 : ( ( ) ( ) set ) is empty ) & ( not b0 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a11 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b0 : ( ( ) ( ) set ) is empty ) ) ;

for g0, g1, g2, g3, g4, g5, g6, g7, g8, g9, g10, g11, g12, g13, g14, g15, g16, a0, a1, a2, a3, a4, a5, a6, a7, a8, a9, a10, a11, a12, a13, a14, a15, b0, b1, b2, b3, b4, b5, b6, b7, b8, b9, b10, b11, b12, b13, b14, b15, z, p being ( ( ) ( ) set ) st not g0 : ( ( ) ( ) set ) is empty & z : ( ( ) ( ) set ) is empty & ( not b0 : ( ( ) ( ) set ) is empty implies not XOR2 (p : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (p : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b0 : ( ( ) ( ) set ) is empty ) & ( not b1 : ( ( ) ( ) set ) is empty implies not XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b1 : ( ( ) ( ) set ) is empty ) & ( not b2 : ( ( ) ( ) set ) is empty implies not XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b2 : ( ( ) ( ) set ) is empty ) & ( not b3 : ( ( ) ( ) set ) is empty implies not XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b3 : ( ( ) ( ) set ) is empty ) & ( not b4 : ( ( ) ( ) set ) is empty implies not XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b4 : ( ( ) ( ) set ) is empty ) & ( not b5 : ( ( ) ( ) set ) is empty implies not XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b5 : ( ( ) ( ) set ) is empty ) & ( not b6 : ( ( ) ( ) set ) is empty implies not XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b6 : ( ( ) ( ) set ) is empty ) & ( not b7 : ( ( ) ( ) set ) is empty implies not XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b7 : ( ( ) ( ) set ) is empty ) & ( not b8 : ( ( ) ( ) set ) is empty implies not XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b8 : ( ( ) ( ) set ) is empty ) & ( not b9 : ( ( ) ( ) set ) is empty implies not XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b9 : ( ( ) ( ) set ) is empty ) & ( not b10 : ( ( ) ( ) set ) is empty implies not XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b10 : ( ( ) ( ) set ) is empty ) & ( not b11 : ( ( ) ( ) set ) is empty implies not XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b11 : ( ( ) ( ) set ) is empty ) & ( not b12 : ( ( ) ( ) set ) is empty implies not XOR2 (a11 : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a11 : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b12 : ( ( ) ( ) set ) is empty ) & ( not b13 : ( ( ) ( ) set ) is empty implies not XOR2 (a12 : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a12 : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b13 : ( ( ) ( ) set ) is empty ) & ( not b14 : ( ( ) ( ) set ) is empty implies not XOR2 (a13 : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a13 : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b14 : ( ( ) ( ) set ) is empty ) & ( not b15 : ( ( ) ( ) set ) is empty implies not XOR2 (a14 : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (a14 : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,b0 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b15 : ( ( ) ( ) set ) is empty ) holds
( ( not b15 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a14 : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a14 : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g15 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b15 : ( ( ) ( ) set ) is empty ) & ( not b14 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a13 : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a13 : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g14 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b14 : ( ( ) ( ) set ) is empty ) & ( not b13 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a12 : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a12 : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g13 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b13 : ( ( ) ( ) set ) is empty ) & ( not b12 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a11 : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a11 : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g12 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b12 : ( ( ) ( ) set ) is empty ) & ( not b11 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a10 : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g11 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b11 : ( ( ) ( ) set ) is empty ) & ( not b10 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a9 : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g10 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b10 : ( ( ) ( ) set ) is empty ) & ( not b9 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a8 : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g9 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b9 : ( ( ) ( ) set ) is empty ) & ( not b8 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a7 : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g8 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b8 : ( ( ) ( ) set ) is empty ) & ( not b7 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a6 : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g7 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b7 : ( ( ) ( ) set ) is empty ) & ( not b6 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a5 : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g6 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b6 : ( ( ) ( ) set ) is empty ) & ( not b5 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a4 : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g5 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b5 : ( ( ) ( ) set ) is empty ) & ( not b4 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a3 : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g4 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b4 : ( ( ) ( ) set ) is empty ) & ( not b3 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a2 : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g3 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b3 : ( ( ) ( ) set ) is empty ) & ( not b2 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a1 : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g2 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b2 : ( ( ) ( ) set ) is empty ) & ( not b1 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (a0 : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g1 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b1 : ( ( ) ( ) set ) is empty ) & ( not b0 : ( ( ) ( ) set ) is empty implies not XOR2 ((XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 ((XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,a15 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(XOR2 (z : ( ( ) ( ) set ) ,(AND2 (g0 : ( ( ) ( ) set ) ,p : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not b0 : ( ( ) ( ) set ) is empty ) ) ;