:: XBOOLEAN  semantic presentation begin  definitionfunc  :::"FALSE":::  ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 1 (Set   ($#k6_numbers :::"0"::: )  ); func  :::"TRUE":::  ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 2 (Num 1); end; 








:: deftheorem    defines :::"FALSE"::: XBOOLEAN:def 1 :  (Bool (Set   ($#k1_xboolean :::"FALSE"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  )); 
 
:: deftheorem    defines :::"TRUE"::: XBOOLEAN:def 2 :  (Bool (Set   ($#k2_xboolean :::"TRUE"::: )  )  ($#r1_hidden :::"="::: )  (Num 1)); 
 definitionlet "p" be    ($#m1_hidden :::"set"::: )  ; attr "p" is  :::"boolean":::  means :: XBOOLEAN:def 3 (Bool  "("  (Bool "p"  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  )) "or" (Bool "p"  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))  ")" ); end; 




:: deftheorem    defines :::"boolean"::: XBOOLEAN:def 3 :  (Bool  "for" (Set (Var "p")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "p")) "is"   ($#v1_xboolean :::"boolean"::: )  ) "iff" (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  )) "or" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))  ")" )  ")" )); 
 registration
cluster (Set   ($#k1_xboolean :::"FALSE"::: )  ) ->   ($#v1_xboolean :::"boolean"::: )   ; 

cluster (Set   ($#k2_xboolean :::"TRUE"::: )  ) ->   ($#v1_xboolean :::"boolean"::: )   ; 

cluster   ($#v1_xboolean :::"boolean"::: )    for    ($#m1_hidden :::"set"::: )  ; 

cluster   ($#v1_xboolean :::"boolean"::: )    ->   ($#v7_ordinal1 :::"natural"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 





definitionlet "p" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; func  :::"'not'"::: "p" ->   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   equals :: XBOOLEAN:def 4 (Set (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  "p"); involutiveness  
(Bool  "for" (Set (Var "b1")) "," (Set (Var "b2")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "b1")))))
 ; let "q" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; func "p" :::"'&'"::: "q" ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 5 (Set "p"  ($#k3_xcmplx_0 :::"*"::: )  "q"); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "q"))))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p"))))))
 ; idempotence  
(Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")))))
 ; end; 











:: deftheorem    defines :::"'not'"::: XBOOLEAN:def 4 :  (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Num 1)  ($#k6_xcmplx_0 :::"-"::: )  (Set (Var "p"))))); 
 
:: deftheorem    defines :::"'&'"::: XBOOLEAN:def 5 :  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "q"))))); 
 registrationlet "p", "q" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "p"  ($#k4_xboolean :::"'&'"::: )  "q") ->   ($#v1_xboolean :::"boolean"::: )   ; 
end; definitionlet "p", "q" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; func "p" :::"'or'"::: "q" ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 6 (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  "p" ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  "q" ")" ) ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" ) ")" )))))
 ; idempotence  
(Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" ) ")" ))))
 ; end; 






:: deftheorem    defines :::"'or'"::: XBOOLEAN:def 6 :  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )))); 
 definitionlet "p", "q" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; func "p" :::"=>"::: "q" ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 7 (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  "p" ")" )  ($#k5_xboolean :::"'or'"::: )  "q"); end; 






:: deftheorem    defines :::"=>"::: XBOOLEAN:def 7 :  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q"))))); 
 registrationlet "p", "q" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "p"  ($#k5_xboolean :::"'or'"::: )  "q") ->   ($#v1_xboolean :::"boolean"::: )   ; 

cluster (Set "p"  ($#k6_xboolean :::"=>"::: )  "q") ->   ($#v1_xboolean :::"boolean"::: )   ; 
end; definitionlet "p", "q" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; func "p" :::"<=>"::: "q" ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 8 (Set (Set  "(" "p"  ($#k6_xboolean :::"=>"::: )  "q" ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" "q"  ($#k6_xboolean :::"=>"::: )  "p" ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )))))
 ; end; 






:: deftheorem    defines :::"<=>"::: XBOOLEAN:def 8 :  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" )))); 
 registrationlet "p", "q" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "p"  ($#k7_xboolean :::"<=>"::: )  "q") ->   ($#v1_xboolean :::"boolean"::: )   ; 
end; definitionlet "p", "q" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; func "p" :::"'nand'"::: "q" ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 9 (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" "p"  ($#k4_xboolean :::"'&'"::: )  "q" ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "q"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "p")) ")" )))))
 ; func "p" :::"'nor'"::: "q" ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 10 (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" "p"  ($#k5_xboolean :::"'or'"::: )  "q" ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "q"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "p")) ")" )))))
 ; func "p" :::"'xor'"::: "q" ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 11 (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" "p"  ($#k7_xboolean :::"<=>"::: )  "q" ")" )); commutativity  
(Bool  "for" (Set (Var "b1")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" )))) "holds"  (Bool (Set (Var "b1"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "p")) ")" )))))
 ; func "p" :::"'\'"::: "q" ->    ($#m1_hidden :::"set"::: )   equals :: XBOOLEAN:def 12 (Set "p"  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  "q" ")" )); end; 
























:: deftheorem    defines :::"'nand'"::: XBOOLEAN:def 9 :  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )))); 
 
:: deftheorem    defines :::"'nor'"::: XBOOLEAN:def 10 :  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )))); 
 
:: deftheorem    defines :::"'xor'"::: XBOOLEAN:def 11 :  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" )))); 
 
:: deftheorem    defines :::"'\'"::: XBOOLEAN:def 12 :  (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))); 
 registrationlet "p", "q" be   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "p"  ($#k8_xboolean :::"'nand'"::: )  "q") ->   ($#v1_xboolean :::"boolean"::: )   ; 

cluster (Set "p"  ($#k9_xboolean :::"'nor'"::: )  "q") ->   ($#v1_xboolean :::"boolean"::: )   ; 

cluster (Set "p"  ($#k10_xboolean :::"'xor'"::: )  "q") ->   ($#v1_xboolean :::"boolean"::: )   ; 

cluster (Set "p"  ($#k11_xboolean :::"'\'"::: )  "q") ->   ($#v1_xboolean :::"boolean"::: )   ; 
end; begin  
theorem :: XBOOLEAN:1 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: XBOOLEAN:2 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:3 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: XBOOLEAN:4 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:5 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: XBOOLEAN:6 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "p")))) ; 
 
theorem :: XBOOLEAN:7 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:8 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:9 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "q"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:10 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "q"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" ) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "r"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "r"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "p")) ")" )))) ; 
 
theorem :: XBOOLEAN:11 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:12 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:13 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:14 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:15 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:16 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:17 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:18 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:19 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" )  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:20 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:21 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:22 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:23 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" ) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:24 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:25 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:26 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:27 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:28 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:29 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:30 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:31 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:32 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:33 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:34 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:35 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:36 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:37 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:38 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "q"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:39 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "q"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:40 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "q"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:41 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:42 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:43 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:44 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:45 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "q"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "r"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" )))) ; 
 
theorem :: XBOOLEAN:46 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:47 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:48 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:49 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" ) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:50 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:51 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:52 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:53 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:54 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "q"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:55 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "q"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:56 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:57 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:58 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "q"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:59 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:60 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:61 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:62 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:63 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:64 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:65 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:66 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "r")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:67 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "q"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r"))))) ; 
 
theorem :: XBOOLEAN:68 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "q")) ")" )  ($#k11_xboolean :::"'\'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:69 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:70 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:71 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:72 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) ; 
 
theorem :: XBOOLEAN:73 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" )  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "q"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:74 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:75 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "q"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:76 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:77 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:78 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:79 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:80 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:81 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:82 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:83 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "q"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "q"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" ) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "q"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" ) ")" ) ")" )))) ; 
 
theorem :: XBOOLEAN:84 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:85 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:86 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:87 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ) ")" ) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:88 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:89 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) ; 
 
theorem :: XBOOLEAN:90 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )))) ; 
 
theorem :: XBOOLEAN:91 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:92 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:93 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:94 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:95 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:96 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "q"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" )  ($#k7_xboolean :::"<=>"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" )))) ; 
 
theorem :: XBOOLEAN:97 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:98 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "q"))))) ; 
 
theorem :: XBOOLEAN:99 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "p"))))) ; 
 
theorem :: XBOOLEAN:100 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "q"))  ($#k11_xboolean :::"'\'"::: )  (Set (Var "p"))))) ; 
 begin  
theorem :: XBOOLEAN:101 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool  "("  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))  ")" )) ; 
 
theorem :: XBOOLEAN:102 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:103 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:104 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:105 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:106 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:107 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "r"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "r"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:108 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:109 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:110 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:111 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:112 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  ($#k2_xboolean :::"TRUE"::: ) )  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:113 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:114 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:115 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:116 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set (Var "q")))) ; 
 
theorem :: XBOOLEAN:117 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:118 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:119 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:120 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:121 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "q"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" ) ")" )  ($#k6_xboolean :::"=>"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:122 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:123 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:124 (Bool  "for" (Set (Var "q")) "," (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "q")) ")" )  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" )  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:125 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:126 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set  "(" (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")) ")" )  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" )  ($#k7_xboolean :::"<=>"::: )  (Set (Var "p")) ")" )  ($#k7_xboolean :::"<=>"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:127 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:128 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Set (Var "r"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "r")) ")" )  ($#k7_xboolean :::"<=>"::: )  (Set  "(" (Set (Var "q"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:129 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:130 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Set (Var "r"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "r")) ")" )  ($#k7_xboolean :::"<=>"::: )  (Set  "(" (Set (Var "q"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:131 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Set (Var "r"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "r")) ")" )  ($#k7_xboolean :::"<=>"::: )  (Set  "(" (Set (Var "q"))  ($#k5_xboolean :::"'or'"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:132 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"   (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) "iff" (Bool  "("  (Bool (Set (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))  ")" )  ")" )) ; 
 
theorem :: XBOOLEAN:133 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "," (Set (Var "r")) "," (Set (Var "s")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  )) & (Bool (Set (Set (Var "r"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "r")) ")" )  ($#k7_xboolean :::"<=>"::: )  (Set  "(" (Set (Var "q"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "s")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:134 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:135 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:136 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k5_xboolean :::"'or'"::: )  (Set  "(" (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:137 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_xboolean :::"TRUE"::: )  ))) ; 
 
theorem :: XBOOLEAN:138 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) ; 
 
theorem :: XBOOLEAN:139 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) "holds"  (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) ; 
 
theorem :: XBOOLEAN:140 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )    "holds"  (Bool  "("   "not" (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set (Var "q")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  )) "or" (Bool (Set (Var "p"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  )) "or" (Bool (Set (Var "q"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))  ")" )) ; 
 
theorem :: XBOOLEAN:141 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) ; 
 
theorem :: XBOOLEAN:142 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set  "("  ($#k3_xboolean :::"'not'"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) ; 
 
theorem :: XBOOLEAN:143 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k3_xboolean :::"'not'"::: )  (Set  "(" (Set (Var "p"))  ($#k7_xboolean :::"<=>"::: )  (Set (Var "p")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) ; 
 
theorem :: XBOOLEAN:144 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k4_xboolean :::"'&'"::: )  (Set  "(" (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) ; 
 
theorem :: XBOOLEAN:145 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k6_xboolean :::"=>"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) ; 
 
theorem :: XBOOLEAN:146 (Bool  "for" (Set (Var "p")) "," (Set (Var "q")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k9_xboolean :::"'nor'"::: )  (Set  "(" (Set (Var "p"))  ($#k8_xboolean :::"'nand'"::: )  (Set (Var "q")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) ; 
 
theorem :: XBOOLEAN:147 (Bool  "for" (Set (Var "p")) "being"   ($#v1_xboolean :::"boolean"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "p"))  ($#k10_xboolean :::"'xor'"::: )  (Set (Var "p")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboolean :::"FALSE"::: )  ))) ;