:: GATE_4  semantic presentation begin  
theorem :: GATE_4:1 (Bool  "for" (Set (Var "g0")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g5")) "," (Set (Var "g6")) "," (Set (Var "g7")) "," (Set (Var "g8")) "," (Set (Var "g9")) "," (Set (Var "g10")) "," (Set (Var "g11")) "," (Set (Var "g12")) "," (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "a6")) "," (Set (Var "a7")) "," (Set (Var "a8")) "," (Set (Var "a9")) "," (Set (Var "a10")) "," (Set (Var "a11")) "," (Set (Var "b0")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "," (Set (Var "b6")) "," (Set (Var "b7")) "," (Set (Var "b8")) "," (Set (Var "b9")) "," (Set (Var "b10")) "," (Set (Var "b11")) "," (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "not" (Bool  "("  (Bool (Bool  "not" (Set (Var "g12")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) &  "("  (Bool (Bool (Bool  "not" (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  & (Bool  "not" (Bool  "("   "("  (Bool (Bool (Bool  "not" (Set (Var "a11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "a11")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "a11")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "p")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a11")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "p")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"   ")" ))  ")" ))) ; 
 
theorem :: GATE_4:2 (Bool  "for" (Set (Var "g0")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g5")) "," (Set (Var "g6")) "," (Set (Var "g7")) "," (Set (Var "g8")) "," (Set (Var "g9")) "," (Set (Var "g10")) "," (Set (Var "g11")) "," (Set (Var "g12")) "," (Set (Var "g13")) "," (Set (Var "g14")) "," (Set (Var "g15")) "," (Set (Var "g16")) "," (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "a6")) "," (Set (Var "a7")) "," (Set (Var "a8")) "," (Set (Var "a9")) "," (Set (Var "a10")) "," (Set (Var "a11")) "," (Set (Var "a12")) "," (Set (Var "a13")) "," (Set (Var "a14")) "," (Set (Var "a15")) "," (Set (Var "b0")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "," (Set (Var "b6")) "," (Set (Var "b7")) "," (Set (Var "b8")) "," (Set (Var "b9")) "," (Set (Var "b10")) "," (Set (Var "b11")) "," (Set (Var "b12")) "," (Set (Var "b13")) "," (Set (Var "b14")) "," (Set (Var "b15")) "," (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    "holds"  (Bool  "not" (Bool  "("  (Bool (Bool  "not" (Set (Var "g16")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) &  "("  (Bool (Bool (Bool  "not" (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "p")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b12")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b12")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b13")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a12")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a12")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b13")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b14")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a13")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a13")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b14")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b15")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a14")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a14")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b15")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  & (Bool  "not" (Bool  "("   "("  (Bool (Bool (Bool  "not" (Set (Var "a15")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g16")) "," (Set (Var "a15")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g16")) "," (Set (Var "a15")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a15")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a14")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b15")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b15")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a14")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a13")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b14")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b14")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a13")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a12")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b13")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b13")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a12")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b12")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b12")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "a0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "a0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "p")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "b0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a15")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "p")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"   ")" ))  ")" ))) ; 
 begin  
theorem :: GATE_4:3 (Bool  "for" (Set (Var "g0")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g5")) "," (Set (Var "g6")) "," (Set (Var "g7")) "," (Set (Var "g8")) "," (Set (Var "g9")) "," (Set (Var "g10")) "," (Set (Var "g11")) "," (Set (Var "g12")) "," (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "a6")) "," (Set (Var "a7")) "," (Set (Var "a8")) "," (Set (Var "a9")) "," (Set (Var "a10")) "," (Set (Var "a11")) "," (Set (Var "b0")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "," (Set (Var "b6")) "," (Set (Var "b7")) "," (Set (Var "b8")) "," (Set (Var "b9")) "," (Set (Var "b10")) "," (Set (Var "b11")) "," (Set (Var "z")) "," (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "g0")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "z")) "is"   ($#v1_xboole_0 :::"empty"::: )  ) &  "("  (Bool (Bool (Bool  "not" (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "p")) "," (Set (Var "a11")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "p")) "," (Set (Var "a11")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" ) "holds"  (Bool  "("   "("  (Bool (Bool (Bool  "not" (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a11")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"   ")" )) ; 
 
theorem :: GATE_4:4 (Bool  "for" (Set (Var "g0")) "," (Set (Var "g1")) "," (Set (Var "g2")) "," (Set (Var "g3")) "," (Set (Var "g4")) "," (Set (Var "g5")) "," (Set (Var "g6")) "," (Set (Var "g7")) "," (Set (Var "g8")) "," (Set (Var "g9")) "," (Set (Var "g10")) "," (Set (Var "g11")) "," (Set (Var "g12")) "," (Set (Var "g13")) "," (Set (Var "g14")) "," (Set (Var "g15")) "," (Set (Var "g16")) "," (Set (Var "a0")) "," (Set (Var "a1")) "," (Set (Var "a2")) "," (Set (Var "a3")) "," (Set (Var "a4")) "," (Set (Var "a5")) "," (Set (Var "a6")) "," (Set (Var "a7")) "," (Set (Var "a8")) "," (Set (Var "a9")) "," (Set (Var "a10")) "," (Set (Var "a11")) "," (Set (Var "a12")) "," (Set (Var "a13")) "," (Set (Var "a14")) "," (Set (Var "a15")) "," (Set (Var "b0")) "," (Set (Var "b1")) "," (Set (Var "b2")) "," (Set (Var "b3")) "," (Set (Var "b4")) "," (Set (Var "b5")) "," (Set (Var "b6")) "," (Set (Var "b7")) "," (Set (Var "b8")) "," (Set (Var "b9")) "," (Set (Var "b10")) "," (Set (Var "b11")) "," (Set (Var "b12")) "," (Set (Var "b13")) "," (Set (Var "b14")) "," (Set (Var "b15")) "," (Set (Var "z")) "," (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Bool  "not" (Set (Var "g0")) "is"   ($#v1_xboole_0 :::"empty"::: )  )) & (Bool (Set (Var "z")) "is"   ($#v1_xboole_0 :::"empty"::: )  ) &  "("  (Bool (Bool (Bool  "not" (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "p")) "," (Set (Var "a15")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "p")) "," (Set (Var "a15")) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b12")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b12")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b13")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a12")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a12")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b13")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b14")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a13")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a13")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b14")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b15")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a14")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a14")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "b0")) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b15")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")" ) "holds"  (Bool  "("   "("  (Bool (Bool (Bool  "not" (Set (Var "b15")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a14")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a14")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g15")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b15")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b14")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a13")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a13")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g14")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b14")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b13")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a12")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a12")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g13")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b13")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b12")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a11")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g12")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b12")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a10")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g11")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b11")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a9")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g10")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b10")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a8")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g9")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b9")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a7")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g8")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b8")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a6")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g7")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b7")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a5")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g6")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b6")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a4")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g5")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b5")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a3")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g4")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b4")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a2")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g3")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b3")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a1")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g2")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b2")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "a0")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g1")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b1")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set   ($#k4_gate_1 :::"XOR2"::: )   "(" (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "a15")) ")"  ")" ) ")"  ")" ) "," (Set  "("  ($#k4_gate_1 :::"XOR2"::: )   "(" (Set (Var "z")) "," (Set  "("  ($#k2_gate_1 :::"AND2"::: )   "(" (Set (Var "g0")) "," (Set (Var "p")) ")"  ")" ) ")"  ")" ) ")" ) "is"   ($#v1_xboole_0 :::"empty"::: )  ))) "implies" (Bool  "not" (Bool (Set (Var "b0")) "is"   ($#v1_xboole_0 :::"empty"::: )  ))  ")"   ")" )) ;