for s0, s1, s2, s3, ns0, ns1, ns2, ns3, q1, q2, nq1, nq2 being ( ( ) ( ) set ) holds
not ( ( not s0 : ( ( ) ( ) set ) is empty implies not AND2 ((NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 ((NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s0 : ( ( ) ( ) set ) is empty ) & ( not s1 : ( ( ) ( ) set ) is empty implies not AND2 ((NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 ((NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s1 : ( ( ) ( ) set ) is empty ) & ( not s2 : ( ( ) ( ) set ) is empty implies not AND2 (q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s2 : ( ( ) ( ) set ) is empty ) & ( not s3 : ( ( ) ( ) set ) is empty implies not AND2 (q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s3 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not AND2 ((NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 ((NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns0 : ( ( ) ( ) set ) is empty ) & ( not ns1 : ( ( ) ( ) set ) is empty implies not AND2 ((NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 ((NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns1 : ( ( ) ( ) set ) is empty ) & ( not ns2 : ( ( ) ( ) set ) is empty implies not AND2 (nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns2 : ( ( ) ( ) set ) is empty ) & ( not ns3 : ( ( ) ( ) set ) is empty implies not AND2 (nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not nq1 : ( ( ) ( ) set ) is empty implies not NOT1 q2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) is empty ) & ( not NOT1 q2 : ( ( ) ( ) set ) : ( ( ) ( ) set ) is empty implies not nq1 : ( ( ) ( ) set ) is empty ) & ( not nq2 : ( ( ) ( ) set ) is empty implies not q1 : ( ( ) ( ) set ) is empty ) & ( not q1 : ( ( ) ( ) set ) is empty implies not nq2 : ( ( ) ( ) 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 ns3 : ( ( ) ( ) set ) is empty implies not s1 : ( ( ) ( ) set ) is empty ) & ( not s1 : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not ns2 : ( ( ) ( ) set ) is empty implies not s3 : ( ( ) ( ) set ) is empty ) & ( not s3 : ( ( ) ( ) set ) is empty implies not ns2 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not s2 : ( ( ) ( ) set ) is empty ) & ( not s2 : ( ( ) ( ) set ) is empty implies not ns0 : ( ( ) ( ) set ) is empty ) ) ) ;

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

for s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, ns8, ns9, ns10, ns11, ns12, ns13, ns14, ns15, q1, q2, q3, q4, nq1, nq2, nq3, nq4 being ( ( ) ( ) set ) holds
not ( ( not s0 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s3 : ( ( ) ( ) set ) is empty ) & ( not s4 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,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 AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s5 : ( ( ) ( ) set ) is empty ) & ( not s6 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s6 : ( ( ) ( ) set ) is empty ) & ( not s7 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s7 : ( ( ) ( ) set ) is empty ) & ( not s8 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s8 : ( ( ) ( ) set ) is empty ) & ( not s9 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s9 : ( ( ) ( ) set ) is empty ) & ( not s10 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s10 : ( ( ) ( ) set ) is empty ) & ( not s11 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s11 : ( ( ) ( ) set ) is empty ) & ( not s12 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s12 : ( ( ) ( ) set ) is empty ) & ( not s13 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s13 : ( ( ) ( ) set ) is empty ) & ( not s14 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s14 : ( ( ) ( ) set ) is empty ) & ( not s15 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s15 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not ns4 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,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 AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns5 : ( ( ) ( ) set ) is empty ) & ( not ns6 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns6 : ( ( ) ( ) set ) is empty ) & ( not ns7 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns7 : ( ( ) ( ) set ) is empty ) & ( not ns8 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns8 : ( ( ) ( ) set ) is empty ) & ( not ns9 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns9 : ( ( ) ( ) set ) is empty ) & ( not ns10 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns10 : ( ( ) ( ) set ) is empty ) & ( not ns11 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns11 : ( ( ) ( ) set ) is empty ) & ( not ns12 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns12 : ( ( ) ( ) set ) is empty ) & ( not ns13 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns13 : ( ( ) ( ) set ) is empty ) & ( not ns14 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns14 : ( ( ) ( ) set ) is empty ) & ( not ns15 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns15 : ( ( ) ( ) set ) is empty ) & ( not nq1 : ( ( ) ( ) set ) is empty implies not NOT1 q4 : ( ( ) ( ) set ) : ( ( ) ( ) set ) is empty ) & ( not NOT1 q4 : ( ( ) ( ) set ) : ( ( ) ( ) set ) is empty implies not nq1 : ( ( ) ( ) set ) is empty ) & ( not nq2 : ( ( ) ( ) set ) is empty implies not q1 : ( ( ) ( ) set ) is empty ) & ( not q1 : ( ( ) ( ) set ) is empty implies not nq2 : ( ( ) ( ) set ) is empty ) & ( not nq3 : ( ( ) ( ) set ) is empty implies not q2 : ( ( ) ( ) set ) is empty ) & ( not q2 : ( ( ) ( ) set ) is empty implies not nq3 : ( ( ) ( ) set ) is empty ) & ( not nq4 : ( ( ) ( ) set ) is empty implies not q3 : ( ( ) ( ) set ) is empty ) & ( not q3 : ( ( ) ( ) set ) is empty implies not nq4 : ( ( ) ( ) 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 ns3 : ( ( ) ( ) set ) is empty implies not s1 : ( ( ) ( ) set ) is empty ) & ( not s1 : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not ns7 : ( ( ) ( ) set ) is empty implies not s3 : ( ( ) ( ) set ) is empty ) & ( not s3 : ( ( ) ( ) set ) is empty implies not ns7 : ( ( ) ( ) set ) is empty ) & ( not ns15 : ( ( ) ( ) set ) is empty implies not s7 : ( ( ) ( ) set ) is empty ) & ( not s7 : ( ( ) ( ) set ) is empty implies not ns15 : ( ( ) ( ) set ) is empty ) & ( not ns14 : ( ( ) ( ) set ) is empty implies not s15 : ( ( ) ( ) set ) is empty ) & ( not s15 : ( ( ) ( ) set ) is empty implies not ns14 : ( ( ) ( ) set ) is empty ) & ( not ns12 : ( ( ) ( ) set ) is empty implies not s14 : ( ( ) ( ) set ) is empty ) & ( not s14 : ( ( ) ( ) set ) is empty implies not ns12 : ( ( ) ( ) set ) is empty ) & ( not ns8 : ( ( ) ( ) set ) is empty implies not s12 : ( ( ) ( ) set ) is empty ) & ( not s12 : ( ( ) ( ) set ) is empty implies not ns8 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not s8 : ( ( ) ( ) set ) is empty ) & ( not s8 : ( ( ) ( ) set ) is empty implies not ns0 : ( ( ) ( ) set ) is empty ) & ( not ns5 : ( ( ) ( ) set ) is empty implies not s2 : ( ( ) ( ) set ) is empty ) & ( not s2 : ( ( ) ( ) set ) is empty implies not ns5 : ( ( ) ( ) set ) is empty ) & ( not ns11 : ( ( ) ( ) set ) is empty implies not s5 : ( ( ) ( ) set ) is empty ) & ( not s5 : ( ( ) ( ) set ) is empty implies not ns11 : ( ( ) ( ) set ) is empty ) & ( not ns6 : ( ( ) ( ) set ) is empty implies not s11 : ( ( ) ( ) set ) is empty ) & ( not s11 : ( ( ) ( ) set ) is empty implies not ns6 : ( ( ) ( ) set ) is empty ) & ( not ns13 : ( ( ) ( ) set ) is empty implies not s6 : ( ( ) ( ) set ) is empty ) & ( not s6 : ( ( ) ( ) set ) is empty implies not ns13 : ( ( ) ( ) set ) is empty ) & ( not ns10 : ( ( ) ( ) set ) is empty implies not s13 : ( ( ) ( ) set ) is empty ) & ( not s13 : ( ( ) ( ) set ) is empty implies not ns10 : ( ( ) ( ) set ) is empty ) & ( not ns4 : ( ( ) ( ) set ) is empty implies not s10 : ( ( ) ( ) set ) is empty ) & ( not s10 : ( ( ) ( ) set ) is empty implies not ns4 : ( ( ) ( ) set ) is empty ) & ( not ns9 : ( ( ) ( ) set ) is empty implies not s4 : ( ( ) ( ) set ) is empty ) & ( not s4 : ( ( ) ( ) set ) is empty implies not ns9 : ( ( ) ( ) set ) is empty ) & ( not ns2 : ( ( ) ( ) set ) is empty implies not s9 : ( ( ) ( ) set ) is empty ) & ( not s9 : ( ( ) ( ) set ) is empty implies not ns2 : ( ( ) ( ) set ) is empty ) ) ) ;

for s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, ns0, ns1, ns2, ns3, ns4, ns5, ns6, ns7, ns8, ns9, ns10, ns11, ns12, ns13, ns14, ns15, q1, q2, q3, q4, nq1, nq2, nq3, nq4, R being ( ( ) ( ) set ) holds
not ( ( not s0 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s3 : ( ( ) ( ) set ) is empty ) & ( not s4 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,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 AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s5 : ( ( ) ( ) set ) is empty ) & ( not s6 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s6 : ( ( ) ( ) set ) is empty ) & ( not s7 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s7 : ( ( ) ( ) set ) is empty ) & ( not s8 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s8 : ( ( ) ( ) set ) is empty ) & ( not s9 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s9 : ( ( ) ( ) set ) is empty ) & ( not s10 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s10 : ( ( ) ( ) set ) is empty ) & ( not s11 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,(NOT1 q3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s11 : ( ( ) ( ) set ) is empty ) & ( not s12 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s12 : ( ( ) ( ) set ) is empty ) & ( not s13 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,(NOT1 q2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s13 : ( ( ) ( ) set ) is empty ) & ( not s14 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,(NOT1 q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s14 : ( ( ) ( ) set ) is empty ) & ( not s15 : ( ( ) ( ) set ) is empty implies not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (q4 : ( ( ) ( ) set ) ,q3 : ( ( ) ( ) set ) ,q2 : ( ( ) ( ) set ) ,q1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not s15 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(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 AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not ns4 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,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 AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns5 : ( ( ) ( ) set ) is empty ) & ( not ns6 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns6 : ( ( ) ( ) set ) is empty ) & ( not ns7 : ( ( ) ( ) set ) is empty implies not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 ((NOT1 nq4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns7 : ( ( ) ( ) set ) is empty ) & ( not ns8 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns8 : ( ( ) ( ) set ) is empty ) & ( not ns9 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns9 : ( ( ) ( ) set ) is empty ) & ( not ns10 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns10 : ( ( ) ( ) set ) is empty ) & ( not ns11 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,(NOT1 nq3 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns11 : ( ( ) ( ) set ) is empty ) & ( not ns12 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns12 : ( ( ) ( ) set ) is empty ) & ( not ns13 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,(NOT1 nq2 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns13 : ( ( ) ( ) set ) is empty ) & ( not ns14 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,(NOT1 nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns14 : ( ( ) ( ) set ) is empty ) & ( not ns15 : ( ( ) ( ) set ) is empty implies not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND4 (nq4 : ( ( ) ( ) set ) ,nq3 : ( ( ) ( ) set ) ,nq2 : ( ( ) ( ) set ) ,nq1 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns15 : ( ( ) ( ) set ) is empty ) & ( not nq1 : ( ( ) ( ) set ) is empty implies not AND2 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 ((NOT1 q4 : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not nq1 : ( ( ) ( ) set ) is empty ) & ( not nq2 : ( ( ) ( ) set ) is empty implies not AND2 (q1 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (q1 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not nq2 : ( ( ) ( ) set ) is empty ) & ( not nq3 : ( ( ) ( ) set ) is empty implies not AND2 (q2 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (q2 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not nq3 : ( ( ) ( ) set ) is empty ) & ( not nq4 : ( ( ) ( ) set ) is empty implies not AND2 (q3 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (q3 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not nq4 : ( ( ) ( ) 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 ns3 : ( ( ) ( ) set ) is empty implies not AND2 (s1 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s1 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns3 : ( ( ) ( ) set ) is empty ) & ( not ns7 : ( ( ) ( ) set ) is empty implies not AND2 (s3 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s3 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns7 : ( ( ) ( ) set ) is empty ) & ( not ns15 : ( ( ) ( ) set ) is empty implies not AND2 (s7 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s7 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns15 : ( ( ) ( ) set ) is empty ) & ( not ns14 : ( ( ) ( ) set ) is empty implies not AND2 (s15 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s15 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns14 : ( ( ) ( ) set ) is empty ) & ( not ns12 : ( ( ) ( ) set ) is empty implies not AND2 (s14 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s14 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns12 : ( ( ) ( ) set ) is empty ) & ( not ns8 : ( ( ) ( ) set ) is empty implies not AND2 (s12 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s12 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns8 : ( ( ) ( ) set ) is empty ) & ( not ns0 : ( ( ) ( ) set ) is empty implies not OR2 ((AND2 (s8 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(NOT1 R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not OR2 ((AND2 (s8 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) )) : ( ( ) ( ) set ) ,(NOT1 R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns0 : ( ( ) ( ) set ) is empty ) & ( not ns5 : ( ( ) ( ) set ) is empty implies not AND2 (s2 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s2 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns5 : ( ( ) ( ) set ) is empty ) & ( not ns11 : ( ( ) ( ) set ) is empty implies not AND2 (s5 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s5 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns11 : ( ( ) ( ) set ) is empty ) & ( not ns6 : ( ( ) ( ) set ) is empty implies not AND2 (s11 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s11 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns6 : ( ( ) ( ) set ) is empty ) & ( not ns13 : ( ( ) ( ) set ) is empty implies not AND2 (s6 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s6 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns13 : ( ( ) ( ) set ) is empty ) & ( not ns10 : ( ( ) ( ) set ) is empty implies not AND2 (s13 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s13 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns10 : ( ( ) ( ) set ) is empty ) & ( not ns4 : ( ( ) ( ) set ) is empty implies not AND2 (s10 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s10 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns4 : ( ( ) ( ) set ) is empty ) & ( not ns9 : ( ( ) ( ) set ) is empty implies not AND2 (s4 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s4 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns9 : ( ( ) ( ) set ) is empty ) & ( not ns2 : ( ( ) ( ) set ) is empty implies not AND2 (s9 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty ) & ( not AND2 (s9 : ( ( ) ( ) set ) ,R : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) is empty implies not ns2 : ( ( ) ( ) set ) is empty ) ) ) ;