for s0, s1, s2, s3, s4, s5, s6, s7, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, q1, q2, q3, nq1, nq2, nq3 being ( ( ) ( ) set ) holds
not ( ( not s0 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s0 : ( ( ) ( ) set ) is empty ) & ( not s1 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s1 : ( ( ) ( ) set ) is empty ) & ( not s2 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s2 : ( ( ) ( ) set ) is empty ) & ( not s3 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s3 : ( ( ) ( ) set ) is empty ) & ( not s4 : ( ( ) ( ) set ) is empty implies not AND3 (q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s4 : ( ( ) ( ) set ) is empty ) & ( not s5 : ( ( ) ( ) set ) is empty implies not AND3 (q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s5 : ( ( ) ( ) set ) is empty ) & ( not s6 : ( ( ) ( ) set ) is empty implies not AND3 (q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s6 : ( ( ) ( ) set ) is empty ) & ( not s7 : ( ( ) ( ) set ) is empty implies not AND3 (q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s7 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns0 : ( ( ) ( ) set ) is empty ) & ( not ns1 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns1 : ( ( ) ( ) set ) is empty ) & ( not ns2 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns2 : ( ( ) ( ) set ) is empty ) & ( not ns3 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not ns4 : ( ( ) ( ) set ) is empty implies not AND3 (nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns4 : ( ( ) ( ) set ) is empty ) & ( not ns5 : ( ( ) ( ) set ) is empty implies not AND3 (nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns5 : ( ( ) ( ) set ) is empty ) & ( not ns6 : ( ( ) ( ) set ) is empty implies not AND3 (nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns6 : ( ( ) ( ) set ) is empty ) & ( not ns7 : ( ( ) ( ) set ) is empty implies not AND3 (nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns7 : ( ( ) ( ) set ) is empty ) & ( not nq1 : ( ( ) ( ) set ) is empty implies not NOT1 q1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) is empty ) & ( not NOT1 q1 : ( ( ) ( ) set ) : ( ( ) ( ) set ) is empty implies not nq1 : ( ( ) ( ) set ) is empty ) & ( not nq2 : ( ( ) ( ) set ) is empty implies not XOR2 (q1 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not XOR2 (q1 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not nq2 : ( ( ) ( ) set ) is empty ) & ( not nq3 : ( ( ) ( ) set ) is empty implies not OR2 ((AND2 (q3 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (q1 : ( ( ) ( ) set ) ,(XOR2 (q2 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not OR2 ((AND2 (q3 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (q1 : ( ( ) ( ) set ) ,(XOR2 (q2 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not nq3 : ( ( ) ( ) set ) is empty ) & not ( ( not ns1 : ( ( ) ( ) set ) is empty implies not s0 : ( ( ) ( ) set ) is empty ) & ( not s0 : ( ( ) ( ) set ) is empty implies not ns1 : ( ( ) ( ) set ) is empty ) & ( not ns2 : ( ( ) ( ) set ) is empty implies not s1 : ( ( ) ( ) set ) is empty ) & ( not s1 : ( ( ) ( ) set ) is empty implies not ns2 : ( ( ) ( ) set ) is empty ) & ( not ns3 : ( ( ) ( ) set ) is empty implies not s2 : ( ( ) ( ) set ) is empty ) & ( not s2 : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not ns4 : ( ( ) ( ) set ) is empty implies not s3 : ( ( ) ( ) set ) is empty ) & ( not s3 : ( ( ) ( ) set ) is empty implies not ns4 : ( ( ) ( ) set ) is empty ) & ( not ns5 : ( ( ) ( ) set ) is empty implies not s4 : ( ( ) ( ) set ) is empty ) & ( not s4 : ( ( ) ( ) set ) is empty implies not ns5 : ( ( ) ( ) set ) is empty ) & ( not ns6 : ( ( ) ( ) set ) is empty implies not s5 : ( ( ) ( ) set ) is empty ) & ( not s5 : ( ( ) ( ) set ) is empty implies not ns6 : ( ( ) ( ) set ) is empty ) & ( not ns7 : ( ( ) ( ) set ) is empty implies not s6 : ( ( ) ( ) set ) is empty ) & ( not s6 : ( ( ) ( ) set ) is empty implies not ns7 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not s7 : ( ( ) ( ) set ) is empty ) & ( not s7 : ( ( ) ( ) set ) is empty implies not ns0 : ( ( ) ( ) set ) is empty ) ) ) ;

for a, d, b, c being ( ( ) ( ) set ) holds
( not AND3 ((AND2 (a : ( ( ) ( ) set ) ,d : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (b : ( ( ) ( ) set ) ,d : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (c : ( ( ) ( ) set ) ,d : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty iff not AND2 ((AND3 (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,d : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) ;

for a, b, c, d being ( ( ) ( ) set ) holds
( ( AND2 (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not OR2 ((NOT1 a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not OR2 ((NOT1 a : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies AND2 (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not OR2 (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty & not OR2 (c : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not OR2 ((AND2 (a : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not OR2 ((AND2 (a : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies ( not OR2 (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty & not OR2 (c : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) ) & ( not OR2 (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty & not OR2 (c : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty & not OR2 (d : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not OR2 ((AND3 (a : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) ,d : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not OR2 ((AND3 (a : ( ( ) ( ) set ) ,c : ( ( ) ( ) set ) ,d : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies ( not OR2 (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty & not OR2 (c : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty & not OR2 (d : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) ) & not ( not OR2 (a : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty & ( not a : ( ( ) ( ) set ) is empty implies not c : ( ( ) ( ) set ) is empty ) & ( not c : ( ( ) ( ) set ) is empty implies not a : ( ( ) ( ) set ) is empty ) & OR2 (c : ( ( ) ( ) set ) ,b : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) ) ;

for s0, s1, s2, s3, s4, s5, s6, s7, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, q1, q2, q3, nq1, nq2, nq3, R being ( ( ) ( ) set ) holds
not ( ( not s0 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s0 : ( ( ) ( ) set ) is empty ) & ( not s1 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s1 : ( ( ) ( ) set ) is empty ) & ( not s2 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s2 : ( ( ) ( ) set ) is empty ) & ( not s3 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s3 : ( ( ) ( ) set ) is empty ) & ( not s4 : ( ( ) ( ) set ) is empty implies not AND3 (q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s4 : ( ( ) ( ) set ) is empty ) & ( not s5 : ( ( ) ( ) set ) is empty implies not AND3 (q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s5 : ( ( ) ( ) set ) is empty ) & ( not s6 : ( ( ) ( ) set ) is empty implies not AND3 (q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s6 : ( ( ) ( ) set ) is empty ) & ( not s7 : ( ( ) ( ) set ) is empty implies not AND3 (q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s7 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns0 : ( ( ) ( ) set ) is empty ) & ( not ns1 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns1 : ( ( ) ( ) set ) is empty ) & ( not ns2 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns2 : ( ( ) ( ) set ) is empty ) & ( not ns3 : ( ( ) ( ) set ) is empty implies not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 ((NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not ns4 : ( ( ) ( ) set ) is empty implies not AND3 (nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns4 : ( ( ) ( ) set ) is empty ) & ( not ns5 : ( ( ) ( ) set ) is empty implies not AND3 (nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns5 : ( ( ) ( ) set ) is empty ) & ( not ns6 : ( ( ) ( ) set ) is empty implies not AND3 (nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns6 : ( ( ) ( ) set ) is empty ) & ( not ns7 : ( ( ) ( ) set ) is empty implies not AND3 (nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND3 (nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns7 : ( ( ) ( ) set ) is empty ) & ( not nq1 : ( ( ) ( ) set ) is empty implies not AND2 ((NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 ((NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not nq1 : ( ( ) ( ) set ) is empty ) & ( not nq2 : ( ( ) ( ) set ) is empty implies not AND2 ((XOR2 (q1 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 ((XOR2 (q1 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not nq2 : ( ( ) ( ) set ) is empty ) & ( not nq3 : ( ( ) ( ) set ) is empty implies not AND2 ((OR2 ((AND2 (q3 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (q1 : ( ( ) ( ) set ) ,(XOR2 (q2 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 ((OR2 ((AND2 (q3 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(AND2 (q1 : ( ( ) ( ) set ) ,(XOR2 (q2 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not nq3 : ( ( ) ( ) set ) is empty ) & not ( ( not ns1 : ( ( ) ( ) set ) is empty implies not AND2 (s0 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s0 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns1 : ( ( ) ( ) set ) is empty ) & ( not ns2 : ( ( ) ( ) set ) is empty implies not AND2 (s1 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s1 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns2 : ( ( ) ( ) set ) is empty ) & ( not ns3 : ( ( ) ( ) set ) is empty implies not AND2 (s2 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s2 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not ns4 : ( ( ) ( ) set ) is empty implies not AND2 (s3 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s3 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns4 : ( ( ) ( ) set ) is empty ) & ( not ns5 : ( ( ) ( ) set ) is empty implies not AND2 (s4 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s4 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns5 : ( ( ) ( ) set ) is empty ) & ( not ns6 : ( ( ) ( ) set ) is empty implies not AND2 (s5 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s5 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns6 : ( ( ) ( ) set ) is empty ) & ( not ns7 : ( ( ) ( ) set ) is empty implies not AND2 (s6 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s6 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns7 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not OR2 (s7 : ( ( ) ( ) set ) ,(NOT1 R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not OR2 (s7 : ( ( ) ( ) set ) ,(NOT1 R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns0 : ( ( ) ( ) set ) is empty ) ) ) ;