( benchmark CELAR6_SUB0.smt
:source {Celar Radio Link Frequency Assignment. This benchmark was coded into the SMT-LIB format by Albert Oliveras.}
:status unsat
:category { industrial }
:difficulty { 1 }
:logic QF_IDL
:extrapreds ((v_13_2 ))
:extrapreds ((v_13_8 ))
:extrapreds ((v_14_2 ))
:extrapreds ((v_14_8 ))
:extrapreds ((v_15_2 ))
:extrapreds ((v_15_8 ))
:extrapreds ((v_16_2 ))
:extrapreds ((v_16_8 ))
:extrapreds ((v_321_2 ))
:extrapreds ((v_321_8 ))
:extrapreds ((v_322_2 ))
:extrapreds ((v_322_8 ))
:extrapreds ((v_323_2 ))
:extrapreds ((v_323_8 ))
:extrapreds ((v_324_2 ))
:extrapreds ((v_324_8 ))
:extrapreds ((v_519_2 ))
:extrapreds ((v_519_8 ))
:extrapreds ((v_520_2 ))
:extrapreds ((v_520_8 ))
:extrapreds ((v_557_2 ))
:extrapreds ((v_557_8 ))
:extrapreds ((v_558_2 ))
:extrapreds ((v_558_8 ))
:extrapreds ((v_593_2 ))
:extrapreds ((v_593_8 ))
:extrapreds ((v_594_2 ))
:extrapreds ((v_594_8 ))
:extrapreds ((v_597_2 ))
:extrapreds ((v_597_8 ))
:extrapreds ((v_598_2 ))
:extrapreds ((v_598_8 ))
:extrapreds ((v_599_2 ))
:extrapreds ((v_599_8 ))
:extrapreds ((v_600_2 ))
:extrapreds ((v_600_8 ))
:extrapreds ((v_613_2 ))
:extrapreds ((v_613_8 ))
:extrapreds ((v_614_2 ))
:extrapreds ((v_614_8 ))
:extrapreds ((v_629_2 ))
:extrapreds ((v_629_8 ))
:extrapreds ((v_630_2 ))
:extrapreds ((v_630_8 ))
:extrapreds ((v_631_2 ))
:extrapreds ((v_631_8 ))
:extrapreds ((v_632_2 ))
:extrapreds ((v_632_8 ))
:extrapreds ((v_665_2 ))
:extrapreds ((v_665_8 ))
:extrapreds ((v_666_2 ))
:extrapreds ((v_666_8 ))
:extrapreds ((v_765_2 ))
:extrapreds ((v_765_8 ))
:extrapreds ((v_766_2 ))
:extrapreds ((v_766_8 ))
:extrapreds ((v_767_2 ))
:extrapreds ((v_767_8 ))
:extrapreds ((v_768_2 ))
:extrapreds ((v_768_8 ))
:extrapreds ((v_785_2 ))
:extrapreds ((v_785_8 ))
:extrapreds ((v_786_2 ))
:extrapreds ((v_786_8 ))
:extrafuns ((w_13 Int ))
:extrafuns ((w_14 Int ))
:extrafuns ((w_15 Int ))
:extrafuns ((w_16 Int ))
:extrafuns ((w_321 Int ))
:extrafuns ((w_322 Int ))
:extrafuns ((w_323 Int ))
:extrafuns ((w_324 Int ))
:extrafuns ((w_519 Int ))
:extrafuns ((w_520 Int ))
:extrafuns ((w_557 Int ))
:extrafuns ((w_558 Int ))
:extrafuns ((w_593 Int ))
:extrafuns ((w_594 Int ))
:extrafuns ((w_597 Int ))
:extrafuns ((w_598 Int ))
:extrafuns ((w_599 Int ))
:extrafuns ((w_600 Int ))
:extrafuns ((w_613 Int ))
:extrafuns ((w_614 Int ))
:extrafuns ((w_629 Int ))
:extrafuns ((w_630 Int ))
:extrafuns ((w_631 Int ))
:extrafuns ((w_632 Int ))
:extrafuns ((w_665 Int ))
:extrafuns ((w_666 Int ))
:extrafuns ((w_765 Int ))
:extrafuns ((w_766 Int ))
:extrafuns ((w_767 Int ))
:extrafuns ((w_768 Int ))
:extrafuns ((w_785 Int ))
:extrafuns ((w_786 Int ))
:extrafuns ((z_0 Int ))
:formula
( and 
( or v_13_2 v_13_8 )
( or ( not v_13_2) ( not  v_13_8) )
( or v_14_2 v_14_8 )
( or ( not v_14_2) ( not  v_14_8) )
( or v_15_2 v_15_8 )
( or ( not v_15_2) ( not  v_15_8) )
( or v_16_2 v_16_8 )
( or ( not v_16_2) ( not  v_16_8) )
( or v_321_2 v_321_8 )
( or ( not v_321_2) ( not  v_321_8) )
( or v_322_2 v_322_8 )
( or ( not v_322_2) ( not  v_322_8) )
( or v_323_2 v_323_8 )
( or ( not v_323_2) ( not  v_323_8) )
( or v_324_2 v_324_8 )
( or ( not v_324_2) ( not  v_324_8) )
( or v_519_2 v_519_8 )
( or ( not v_519_2) ( not  v_519_8) )
( or v_520_2 v_520_8 )
( or ( not v_520_2) ( not  v_520_8) )
( or v_557_2 v_557_8 )
( or ( not v_557_2) ( not  v_557_8) )
( or v_558_2 v_558_8 )
( or ( not v_558_2) ( not  v_558_8) )
( or v_593_2 v_593_8 )
( or ( not v_593_2) ( not  v_593_8) )
( or v_594_2 v_594_8 )
( or ( not v_594_2) ( not  v_594_8) )
( or v_597_2 v_597_8 )
( or ( not v_597_2) ( not  v_597_8) )
( or v_598_2 v_598_8 )
( or ( not v_598_2) ( not  v_598_8) )
( or v_599_2 v_599_8 )
( or ( not v_599_2) ( not  v_599_8) )
( or v_600_2 v_600_8 )
( or ( not v_600_2) ( not  v_600_8) )
( or v_613_2 v_613_8 )
( or ( not v_613_2) ( not  v_613_8) )
( or v_614_2 v_614_8 )
( or ( not v_614_2) ( not  v_614_8) )
( or v_629_2 v_629_8 )
( or ( not v_629_2) ( not  v_629_8) )
( or v_630_2 v_630_8 )
( or ( not v_630_2) ( not  v_630_8) )
( or v_631_2 v_631_8 )
( or ( not v_631_2) ( not  v_631_8) )
( or v_632_2 v_632_8 )
( or ( not v_632_2) ( not  v_632_8) )
( or v_665_2 v_665_8 )
( or ( not v_665_2) ( not  v_665_8) )
( or v_666_2 v_666_8 )
( or ( not v_666_2) ( not  v_666_8) )
( or v_765_2 v_765_8 )
( or ( not v_765_2) ( not  v_765_8) )
( or v_766_2 v_766_8 )
( or ( not v_766_2) ( not  v_766_8) )
( or v_767_2 v_767_8 )
( or ( not v_767_2) ( not  v_767_8) )
( or v_768_2 v_768_8 )
( or ( not v_768_2) ( not  v_768_8) )
( or v_785_2 v_785_8 )
( or ( not v_785_2) ( not  v_785_8) )
( or v_786_2 v_786_8 )
( or ( not v_786_2) ( not  v_786_8) )
 ( or  ( not v_13_2) ( and  ( <= ( - w_13 z_0 ) 11) ( >= ( -  w_13 z_0 ) 1) ) ( and  ( <= ( - w_13 z_0 ) 28) ( >= ( -  w_13 z_0 ) 18) ) )
 ( or  ( not v_13_8) ( and  ( <= ( - w_13 z_0 ) 39) ( >= ( -  w_13 z_0 ) 29) ) ( and  ( <= ( - w_13 z_0 ) 56) ( >= ( -  w_13 z_0 ) 46) ) )
 ( or  ( not v_14_2) ( and  ( <= ( - w_14 z_0 ) 11) ( >= ( -  w_14 z_0 ) 1) ) ( and  ( <= ( - w_14 z_0 ) 28) ( >= ( -  w_14 z_0 ) 18) ) )
 ( or  ( not v_14_8) ( and  ( <= ( - w_14 z_0 ) 39) ( >= ( -  w_14 z_0 ) 29) ) ( and  ( <= ( - w_14 z_0 ) 56) ( >= ( -  w_14 z_0 ) 46) ) )
 ( or  ( not v_15_2) ( and  ( <= ( - w_15 z_0 ) 11) ( >= ( -  w_15 z_0 ) 1) ) ( and  ( <= ( - w_15 z_0 ) 28) ( >= ( -  w_15 z_0 ) 18) ) )
 ( or  ( not v_15_8) ( and  ( <= ( - w_15 z_0 ) 39) ( >= ( -  w_15 z_0 ) 29) ) ( and  ( <= ( - w_15 z_0 ) 56) ( >= ( -  w_15 z_0 ) 46) ) )
 ( or  ( not v_16_2) ( and  ( <= ( - w_16 z_0 ) 11) ( >= ( -  w_16 z_0 ) 1) ) ( and  ( <= ( - w_16 z_0 ) 28) ( >= ( -  w_16 z_0 ) 18) ) )
 ( or  ( not v_16_8) ( and  ( <= ( - w_16 z_0 ) 39) ( >= ( -  w_16 z_0 ) 29) ) ( and  ( <= ( - w_16 z_0 ) 56) ( >= ( -  w_16 z_0 ) 46) ) )
 ( or  ( not v_321_2) ( and  ( <= ( - w_321 z_0 ) 11) ( >= ( -  w_321 z_0 ) 1) ) ( and  ( <= ( - w_321 z_0 ) 28) ( >= ( -  w_321 z_0 ) 18) ) )
 ( or  ( not v_321_8) ( and  ( <= ( - w_321 z_0 ) 39) ( >= ( -  w_321 z_0 ) 29) ) ( and  ( <= ( - w_321 z_0 ) 56) ( >= ( -  w_321 z_0 ) 46) ) )
 ( or  ( not v_322_2) ( and  ( <= ( - w_322 z_0 ) 11) ( >= ( -  w_322 z_0 ) 1) ) ( and  ( <= ( - w_322 z_0 ) 28) ( >= ( -  w_322 z_0 ) 18) ) )
 ( or  ( not v_322_8) ( and  ( <= ( - w_322 z_0 ) 39) ( >= ( -  w_322 z_0 ) 29) ) ( and  ( <= ( - w_322 z_0 ) 56) ( >= ( -  w_322 z_0 ) 46) ) )
 ( or  ( not v_323_2) ( and  ( <= ( - w_323 z_0 ) 11) ( >= ( -  w_323 z_0 ) 1) ) ( and  ( <= ( - w_323 z_0 ) 28) ( >= ( -  w_323 z_0 ) 18) ) )
 ( or  ( not v_323_8) ( and  ( <= ( - w_323 z_0 ) 39) ( >= ( -  w_323 z_0 ) 29) ) ( and  ( <= ( - w_323 z_0 ) 56) ( >= ( -  w_323 z_0 ) 46) ) )
 ( or  ( not v_324_2) ( and  ( <= ( - w_324 z_0 ) 11) ( >= ( -  w_324 z_0 ) 1) ) ( and  ( <= ( - w_324 z_0 ) 28) ( >= ( -  w_324 z_0 ) 18) ) )
 ( or  ( not v_324_8) ( and  ( <= ( - w_324 z_0 ) 39) ( >= ( -  w_324 z_0 ) 29) ) ( and  ( <= ( - w_324 z_0 ) 56) ( >= ( -  w_324 z_0 ) 46) ) )
 ( or  ( not v_519_2) ( and  ( <= ( - w_519 z_0 ) 10) ( >= ( -  w_519 z_0 ) 2) ) ( and  ( <= ( - w_519 z_0 ) 27) ( >= ( -  w_519 z_0 ) 19) ) )
 ( or  ( not v_519_8) ( and  ( <= ( - w_519 z_0 ) 38) ( >= ( -  w_519 z_0 ) 30) ) ( and  ( <= ( - w_519 z_0 ) 55) ( >= ( -  w_519 z_0 ) 47) ) )
 ( or  ( not v_520_2) ( and  ( <= ( - w_520 z_0 ) 10) ( >= ( -  w_520 z_0 ) 2) ) ( and  ( <= ( - w_520 z_0 ) 27) ( >= ( -  w_520 z_0 ) 19) ) )
 ( or  ( not v_520_8) ( and  ( <= ( - w_520 z_0 ) 38) ( >= ( -  w_520 z_0 ) 30) ) ( and  ( <= ( - w_520 z_0 ) 55) ( >= ( -  w_520 z_0 ) 47) ) )
 ( or  ( not v_557_2) ( and  ( <= ( - w_557 z_0 ) 10) ( >= ( -  w_557 z_0 ) 2) ) ( and  ( <= ( - w_557 z_0 ) 27) ( >= ( -  w_557 z_0 ) 19) ) )
 ( or  ( not v_557_8) ( and  ( <= ( - w_557 z_0 ) 38) ( >= ( -  w_557 z_0 ) 30) ) ( and  ( <= ( - w_557 z_0 ) 55) ( >= ( -  w_557 z_0 ) 47) ) )
 ( or  ( not v_558_2) ( and  ( <= ( - w_558 z_0 ) 10) ( >= ( -  w_558 z_0 ) 2) ) ( and  ( <= ( - w_558 z_0 ) 27) ( >= ( -  w_558 z_0 ) 19) ) )
 ( or  ( not v_558_8) ( and  ( <= ( - w_558 z_0 ) 38) ( >= ( -  w_558 z_0 ) 30) ) ( and  ( <= ( - w_558 z_0 ) 55) ( >= ( -  w_558 z_0 ) 47) ) )
 ( or  ( not v_593_2) ( and  ( <= ( - w_593 z_0 ) 10) ( >= ( -  w_593 z_0 ) 2) ) ( and  ( <= ( - w_593 z_0 ) 27) ( >= ( -  w_593 z_0 ) 19) ) )
 ( or  ( not v_593_8) ( and  ( <= ( - w_593 z_0 ) 38) ( >= ( -  w_593 z_0 ) 30) ) ( and  ( <= ( - w_593 z_0 ) 55) ( >= ( -  w_593 z_0 ) 47) ) )
 ( or  ( not v_594_2) ( and  ( <= ( - w_594 z_0 ) 10) ( >= ( -  w_594 z_0 ) 2) ) ( and  ( <= ( - w_594 z_0 ) 27) ( >= ( -  w_594 z_0 ) 19) ) )
 ( or  ( not v_594_8) ( and  ( <= ( - w_594 z_0 ) 38) ( >= ( -  w_594 z_0 ) 30) ) ( and  ( <= ( - w_594 z_0 ) 55) ( >= ( -  w_594 z_0 ) 47) ) )
 ( or  ( not v_597_2) ( and  ( <= ( - w_597 z_0 ) 10) ( >= ( -  w_597 z_0 ) 2) ) ( and  ( <= ( - w_597 z_0 ) 27) ( >= ( -  w_597 z_0 ) 19) ) )
 ( or  ( not v_597_8) ( and  ( <= ( - w_597 z_0 ) 38) ( >= ( -  w_597 z_0 ) 30) ) ( and  ( <= ( - w_597 z_0 ) 55) ( >= ( -  w_597 z_0 ) 47) ) )
 ( or  ( not v_598_2) ( and  ( <= ( - w_598 z_0 ) 10) ( >= ( -  w_598 z_0 ) 2) ) ( and  ( <= ( - w_598 z_0 ) 27) ( >= ( -  w_598 z_0 ) 19) ) )
 ( or  ( not v_598_8) ( and  ( <= ( - w_598 z_0 ) 38) ( >= ( -  w_598 z_0 ) 30) ) ( and  ( <= ( - w_598 z_0 ) 55) ( >= ( -  w_598 z_0 ) 47) ) )
 ( or  ( not v_599_2) ( and  ( <= ( - w_599 z_0 ) 10) ( >= ( -  w_599 z_0 ) 2) ) ( and  ( <= ( - w_599 z_0 ) 27) ( >= ( -  w_599 z_0 ) 19) ) )
 ( or  ( not v_599_8) ( and  ( <= ( - w_599 z_0 ) 38) ( >= ( -  w_599 z_0 ) 30) ) ( and  ( <= ( - w_599 z_0 ) 55) ( >= ( -  w_599 z_0 ) 47) ) )
 ( or  ( not v_600_2) ( and  ( <= ( - w_600 z_0 ) 10) ( >= ( -  w_600 z_0 ) 2) ) ( and  ( <= ( - w_600 z_0 ) 27) ( >= ( -  w_600 z_0 ) 19) ) )
 ( or  ( not v_600_8) ( and  ( <= ( - w_600 z_0 ) 38) ( >= ( -  w_600 z_0 ) 30) ) ( and  ( <= ( - w_600 z_0 ) 55) ( >= ( -  w_600 z_0 ) 47) ) )
 ( or  ( not v_613_2) ( and  ( <= ( - w_613 z_0 ) 10) ( >= ( -  w_613 z_0 ) 2) ) ( and  ( <= ( - w_613 z_0 ) 27) ( >= ( -  w_613 z_0 ) 19) ) )
 ( or  ( not v_613_8) ( and  ( <= ( - w_613 z_0 ) 38) ( >= ( -  w_613 z_0 ) 30) ) ( and  ( <= ( - w_613 z_0 ) 55) ( >= ( -  w_613 z_0 ) 47) ) )
 ( or  ( not v_614_2) ( and  ( <= ( - w_614 z_0 ) 10) ( >= ( -  w_614 z_0 ) 2) ) ( and  ( <= ( - w_614 z_0 ) 27) ( >= ( -  w_614 z_0 ) 19) ) )
 ( or  ( not v_614_8) ( and  ( <= ( - w_614 z_0 ) 38) ( >= ( -  w_614 z_0 ) 30) ) ( and  ( <= ( - w_614 z_0 ) 55) ( >= ( -  w_614 z_0 ) 47) ) )
 ( or  ( not v_629_2) ( and  ( <= ( - w_629 z_0 ) 10) ( >= ( -  w_629 z_0 ) 2) ) ( and  ( <= ( - w_629 z_0 ) 27) ( >= ( -  w_629 z_0 ) 19) ) )
 ( or  ( not v_629_8) ( and  ( <= ( - w_629 z_0 ) 38) ( >= ( -  w_629 z_0 ) 30) ) ( and  ( <= ( - w_629 z_0 ) 55) ( >= ( -  w_629 z_0 ) 47) ) )
 ( or  ( not v_630_2) ( and  ( <= ( - w_630 z_0 ) 10) ( >= ( -  w_630 z_0 ) 2) ) ( and  ( <= ( - w_630 z_0 ) 27) ( >= ( -  w_630 z_0 ) 19) ) )
 ( or  ( not v_630_8) ( and  ( <= ( - w_630 z_0 ) 38) ( >= ( -  w_630 z_0 ) 30) ) ( and  ( <= ( - w_630 z_0 ) 55) ( >= ( -  w_630 z_0 ) 47) ) )
 ( or  ( not v_631_2) ( and  ( <= ( - w_631 z_0 ) 10) ( >= ( -  w_631 z_0 ) 2) ) ( and  ( <= ( - w_631 z_0 ) 27) ( >= ( -  w_631 z_0 ) 19) ) )
 ( or  ( not v_631_8) ( and  ( <= ( - w_631 z_0 ) 38) ( >= ( -  w_631 z_0 ) 30) ) ( and  ( <= ( - w_631 z_0 ) 55) ( >= ( -  w_631 z_0 ) 47) ) )
 ( or  ( not v_632_2) ( and  ( <= ( - w_632 z_0 ) 10) ( >= ( -  w_632 z_0 ) 2) ) ( and  ( <= ( - w_632 z_0 ) 27) ( >= ( -  w_632 z_0 ) 19) ) )
 ( or  ( not v_632_8) ( and  ( <= ( - w_632 z_0 ) 38) ( >= ( -  w_632 z_0 ) 30) ) ( and  ( <= ( - w_632 z_0 ) 55) ( >= ( -  w_632 z_0 ) 47) ) )
 ( or  ( not v_665_2) ( and  ( <= ( - w_665 z_0 ) 11) ( >= ( -  w_665 z_0 ) 1) ) ( and  ( <= ( - w_665 z_0 ) 28) ( >= ( -  w_665 z_0 ) 18) ) )
 ( or  ( not v_665_8) ( and  ( <= ( - w_665 z_0 ) 39) ( >= ( -  w_665 z_0 ) 29) ) ( and  ( <= ( - w_665 z_0 ) 56) ( >= ( -  w_665 z_0 ) 46) ) )
 ( or  ( not v_666_2) ( and  ( <= ( - w_666 z_0 ) 11) ( >= ( -  w_666 z_0 ) 1) ) ( and  ( <= ( - w_666 z_0 ) 28) ( >= ( -  w_666 z_0 ) 18) ) )
 ( or  ( not v_666_8) ( and  ( <= ( - w_666 z_0 ) 39) ( >= ( -  w_666 z_0 ) 29) ) ( and  ( <= ( - w_666 z_0 ) 56) ( >= ( -  w_666 z_0 ) 46) ) )
 ( or  ( not v_765_2) ( and  ( <= ( - w_765 z_0 ) 11) ( >= ( -  w_765 z_0 ) 1) ) ( and  ( <= ( - w_765 z_0 ) 28) ( >= ( -  w_765 z_0 ) 18) ) )
 ( or  ( not v_765_8) ( and  ( <= ( - w_765 z_0 ) 39) ( >= ( -  w_765 z_0 ) 29) ) ( and  ( <= ( - w_765 z_0 ) 56) ( >= ( -  w_765 z_0 ) 46) ) )
 ( or  ( not v_766_2) ( and  ( <= ( - w_766 z_0 ) 11) ( >= ( -  w_766 z_0 ) 1) ) ( and  ( <= ( - w_766 z_0 ) 28) ( >= ( -  w_766 z_0 ) 18) ) )
 ( or  ( not v_766_8) ( and  ( <= ( - w_766 z_0 ) 39) ( >= ( -  w_766 z_0 ) 29) ) ( and  ( <= ( - w_766 z_0 ) 56) ( >= ( -  w_766 z_0 ) 46) ) )
 ( or  ( not v_767_2) ( and  ( <= ( - w_767 z_0 ) 11) ( >= ( -  w_767 z_0 ) 1) ) ( and  ( <= ( - w_767 z_0 ) 28) ( >= ( -  w_767 z_0 ) 18) ) )
 ( or  ( not v_767_8) ( and  ( <= ( - w_767 z_0 ) 39) ( >= ( -  w_767 z_0 ) 29) ) ( and  ( <= ( - w_767 z_0 ) 56) ( >= ( -  w_767 z_0 ) 46) ) )
 ( or  ( not v_768_2) ( and  ( <= ( - w_768 z_0 ) 11) ( >= ( -  w_768 z_0 ) 1) ) ( and  ( <= ( - w_768 z_0 ) 28) ( >= ( -  w_768 z_0 ) 18) ) )
 ( or  ( not v_768_8) ( and  ( <= ( - w_768 z_0 ) 39) ( >= ( -  w_768 z_0 ) 29) ) ( and  ( <= ( - w_768 z_0 ) 56) ( >= ( -  w_768 z_0 ) 46) ) )
 ( or  ( not v_785_2) ( and  ( <= ( - w_785 z_0 ) 11) ( >= ( -  w_785 z_0 ) 1) ) ( and  ( <= ( - w_785 z_0 ) 28) ( >= ( -  w_785 z_0 ) 18) ) )
 ( or  ( not v_785_8) ( and  ( <= ( - w_785 z_0 ) 39) ( >= ( -  w_785 z_0 ) 29) ) ( and  ( <= ( - w_785 z_0 ) 56) ( >= ( -  w_785 z_0 ) 46) ) )
 ( or  ( not v_786_2) ( and  ( <= ( - w_786 z_0 ) 11) ( >= ( -  w_786 z_0 ) 1) ) ( and  ( <= ( - w_786 z_0 ) 28) ( >= ( -  w_786 z_0 ) 18) ) )
 ( or  ( not v_786_8) ( and  ( <= ( - w_786 z_0 ) 39) ( >= ( -  w_786 z_0 ) 29) ) ( and  ( <= ( - w_786 z_0 ) 56) ( >= ( -  w_786 z_0 ) 46) ) )
( or  ( not v_13_2 ) ( not v_14_2 ) ( = ( - w_13 w_14) 17) ( = ( - w_14 w_13) 17))
( or  ( not v_13_2 ) ( not v_14_8 ))
( or  ( not v_13_8 ) ( not v_14_2 ))
( or  ( not v_13_8 ) ( not v_14_8 ) ( = ( - w_13 w_14) 17) ( = ( - w_14 w_13) 17))
( or  ( not v_13_2 ) ( not v_15_2 ) ( >= ( - w_13 w_15) 5) ( <= ( - w_13 w_15) ( ~ 5)))
( or  ( not v_13_2 ) ( not v_15_8 ) ( >= ( - w_13 w_15) 5) ( <= ( - w_13 w_15) ( ~ 4)))
( or  ( not v_13_8 ) ( not v_15_2 ) ( >= ( - w_13 w_15) 4) ( <= ( - w_13 w_15) ( ~ 5)))
( or  ( not v_13_8 ) ( not v_15_8 ) ( >= ( - w_13 w_15) 5) ( <= ( - w_13 w_15) ( ~ 5)))
( or  ( not v_13_2 ) ( not v_16_2 ) ( >= ( - w_13 w_16) 14) ( <= ( - w_13 w_16) ( ~ 14)))
( or  ( not v_13_2 ) ( not v_16_8 ) ( >= ( - w_13 w_16) 14) ( <= ( - w_13 w_16) ( ~ 13)))
( or  ( not v_13_8 ) ( not v_16_2 ) ( >= ( - w_13 w_16) 13) ( <= ( - w_13 w_16) ( ~ 14)))
( or  ( not v_13_8 ) ( not v_16_8 ) ( >= ( - w_13 w_16) 14) ( <= ( - w_13 w_16) ( ~ 14)))
( or  ( not v_13_2 ) ( not v_321_2 ) ( >= ( - w_13 w_321) 1) ( <= ( - w_13 w_321) ( ~ 1)))
( or  ( not v_13_2 ) ( not v_321_8 ) ( >= ( - w_13 w_321) 2) ( <= ( - w_13 w_321) ( ~ 1)))
( or  ( not v_13_8 ) ( not v_321_2 ) ( >= ( - w_13 w_321) 1) ( <= ( - w_13 w_321) ( ~ 2)))
( or  ( not v_13_8 ) ( not v_321_8 ) ( >= ( - w_13 w_321) 1) ( <= ( - w_13 w_321) ( ~ 1)))
( or  ( not v_13_2 ) ( not v_322_2 ) ( >= ( - w_13 w_322) 14) ( <= ( - w_13 w_322) ( ~ 14)))
( or  ( not v_13_2 ) ( not v_322_8 ) ( >= ( - w_13 w_322) 14) ( <= ( - w_13 w_322) ( ~ 13)))
( or  ( not v_13_8 ) ( not v_322_2 ) ( >= ( - w_13 w_322) 13) ( <= ( - w_13 w_322) ( ~ 14)))
( or  ( not v_13_8 ) ( not v_322_8 ) ( >= ( - w_13 w_322) 14) ( <= ( - w_13 w_322) ( ~ 14)))
( or  ( not v_13_2 ) ( not v_323_2 ) ( >= ( - w_13 w_323) 12) ( <= ( - w_13 w_323) ( ~ 12)))
( or  ( not v_13_2 ) ( not v_323_8 ) ( >= ( - w_13 w_323) 13) ( <= ( - w_13 w_323) ( ~ 12)))
( or  ( not v_13_8 ) ( not v_323_2 ) ( >= ( - w_13 w_323) 12) ( <= ( - w_13 w_323) ( ~ 13)))
( or  ( not v_13_8 ) ( not v_323_8 ) ( >= ( - w_13 w_323) 12) ( <= ( - w_13 w_323) ( ~ 12)))
( or  ( not v_13_2 ) ( not v_324_2 ) ( >= ( - w_13 w_324) 4) ( <= ( - w_13 w_324) ( ~ 4)))
( or  ( not v_13_2 ) ( not v_324_8 ) ( >= ( - w_13 w_324) 5) ( <= ( - w_13 w_324) ( ~ 4)))
( or  ( not v_13_8 ) ( not v_324_2 ) ( >= ( - w_13 w_324) 4) ( <= ( - w_13 w_324) ( ~ 5)))
( or  ( not v_13_8 ) ( not v_324_8 ) ( >= ( - w_13 w_324) 4) ( <= ( - w_13 w_324) ( ~ 4)))
( or  ( not v_13_2 ) ( not v_557_2 ) ( >= ( - w_13 w_557) 7) ( <= ( - w_13 w_557) ( ~ 7)))
( or  ( not v_13_2 ) ( not v_557_8 ) ( >= ( - w_13 w_557) 7) ( <= ( - w_13 w_557) ( ~ 7)))
( or  ( not v_13_8 ) ( not v_557_2 ) ( >= ( - w_13 w_557) 7) ( <= ( - w_13 w_557) ( ~ 7)))
( or  ( not v_13_8 ) ( not v_557_8 ) ( >= ( - w_13 w_557) 7) ( <= ( - w_13 w_557) ( ~ 7)))
( or  ( not v_13_2 ) ( not v_558_2 ) ( >= ( - w_13 w_558) 19) ( <= ( - w_13 w_558) ( ~ 19)))
( or  ( not v_13_2 ) ( not v_558_8 ) ( >= ( - w_13 w_558) 20) ( <= ( - w_13 w_558) ( ~ 19)))
( or  ( not v_13_8 ) ( not v_558_2 ) ( >= ( - w_13 w_558) 19) ( <= ( - w_13 w_558) ( ~ 20)))
( or  ( not v_13_8 ) ( not v_558_8 ) ( >= ( - w_13 w_558) 19) ( <= ( - w_13 w_558) ( ~ 19)))
( or  ( not v_13_2 ) ( not v_599_2 ) ( >= ( - w_13 w_599) 2) ( <= ( - w_13 w_599) ( ~ 2)))
( or  ( not v_13_2 ) ( not v_599_8 ) ( >= ( - w_13 w_599) 3) ( <= ( - w_13 w_599) ( ~ 2)))
( or  ( not v_13_8 ) ( not v_599_2 ) ( >= ( - w_13 w_599) 2) ( <= ( - w_13 w_599) ( ~ 3)))
( or  ( not v_13_8 ) ( not v_599_8 ) ( >= ( - w_13 w_599) 2) ( <= ( - w_13 w_599) ( ~ 2)))
( or  ( not v_13_2 ) ( not v_600_2 ) ( >= ( - w_13 w_600) 15) ( <= ( - w_13 w_600) ( ~ 15)))
( or  ( not v_13_2 ) ( not v_600_8 ) ( >= ( - w_13 w_600) 15) ( <= ( - w_13 w_600) ( ~ 14)))
( or  ( not v_13_8 ) ( not v_600_2 ) ( >= ( - w_13 w_600) 14) ( <= ( - w_13 w_600) ( ~ 15)))
( or  ( not v_13_8 ) ( not v_600_8 ) ( >= ( - w_13 w_600) 15) ( <= ( - w_13 w_600) ( ~ 15)))
( or  ( not v_13_2 ) ( not v_665_2 ) ( >= ( - w_13 w_665) 13) ( <= ( - w_13 w_665) ( ~ 13)))
( or  ( not v_13_2 ) ( not v_665_8 ) ( >= ( - w_13 w_665) 14) ( <= ( - w_13 w_665) ( ~ 13)))
( or  ( not v_13_8 ) ( not v_665_2 ) ( >= ( - w_13 w_665) 13) ( <= ( - w_13 w_665) ( ~ 14)))
( or  ( not v_13_8 ) ( not v_665_8 ) ( >= ( - w_13 w_665) 13) ( <= ( - w_13 w_665) ( ~ 13)))
( or  ( not v_13_2 ) ( not v_666_2 ) ( >= ( - w_13 w_666) 1) ( <= ( - w_13 w_666) ( ~ 1)))
( or  ( not v_13_2 ) ( not v_666_8 ) ( >= ( - w_13 w_666) 1) ( <= ( - w_13 w_666) ( ~ 1)))
( or  ( not v_13_8 ) ( not v_666_2 ) ( >= ( - w_13 w_666) 1) ( <= ( - w_13 w_666) ( ~ 1)))
( or  ( not v_13_8 ) ( not v_666_8 ) ( >= ( - w_13 w_666) 1) ( <= ( - w_13 w_666) ( ~ 1)))
( or  ( not v_13_2 ) ( not v_767_2 ) ( >= ( - w_13 w_767) 5) ( <= ( - w_13 w_767) ( ~ 5)))
( or  ( not v_13_2 ) ( not v_767_8 ) ( >= ( - w_13 w_767) 5) ( <= ( - w_13 w_767) ( ~ 4)))
( or  ( not v_13_8 ) ( not v_767_2 ) ( >= ( - w_13 w_767) 4) ( <= ( - w_13 w_767) ( ~ 5)))
( or  ( not v_13_8 ) ( not v_767_8 ) ( >= ( - w_13 w_767) 5) ( <= ( - w_13 w_767) ( ~ 5)))
( or  ( not v_13_2 ) ( not v_768_2 ) ( >= ( - w_13 w_768) 17) ( <= ( - w_13 w_768) ( ~ 17)))
( or  ( not v_13_2 ) ( not v_768_8 ) ( >= ( - w_13 w_768) 18) ( <= ( - w_13 w_768) ( ~ 17)))
( or  ( not v_13_8 ) ( not v_768_2 ) ( >= ( - w_13 w_768) 17) ( <= ( - w_13 w_768) ( ~ 18)))
( or  ( not v_13_8 ) ( not v_768_8 ) ( >= ( - w_13 w_768) 17) ( <= ( - w_13 w_768) ( ~ 17)))
( or  ( not v_14_2 ) ( not v_15_2 ) ( >= ( - w_14 w_15) 14) ( <= ( - w_14 w_15) ( ~ 14)))
( or  ( not v_14_2 ) ( not v_15_8 ) ( >= ( - w_14 w_15) 14) ( <= ( - w_14 w_15) ( ~ 13)))
( or  ( not v_14_8 ) ( not v_15_2 ) ( >= ( - w_14 w_15) 13) ( <= ( - w_14 w_15) ( ~ 14)))
( or  ( not v_14_8 ) ( not v_15_8 ) ( >= ( - w_14 w_15) 14) ( <= ( - w_14 w_15) ( ~ 14)))
( or  ( not v_14_2 ) ( not v_16_2 ) ( >= ( - w_14 w_16) 5) ( <= ( - w_14 w_16) ( ~ 5)))
( or  ( not v_14_2 ) ( not v_16_8 ) ( >= ( - w_14 w_16) 5) ( <= ( - w_14 w_16) ( ~ 4)))
( or  ( not v_14_8 ) ( not v_16_2 ) ( >= ( - w_14 w_16) 4) ( <= ( - w_14 w_16) ( ~ 5)))
( or  ( not v_14_8 ) ( not v_16_8 ) ( >= ( - w_14 w_16) 5) ( <= ( - w_14 w_16) ( ~ 5)))
( or  ( not v_14_2 ) ( not v_321_2 ) ( >= ( - w_14 w_321) 12) ( <= ( - w_14 w_321) ( ~ 12)))
( or  ( not v_14_2 ) ( not v_321_8 ) ( >= ( - w_14 w_321) 13) ( <= ( - w_14 w_321) ( ~ 12)))
( or  ( not v_14_8 ) ( not v_321_2 ) ( >= ( - w_14 w_321) 12) ( <= ( - w_14 w_321) ( ~ 13)))
( or  ( not v_14_8 ) ( not v_321_8 ) ( >= ( - w_14 w_321) 12) ( <= ( - w_14 w_321) ( ~ 12)))
( or  ( not v_14_2 ) ( not v_322_2 ) ( >= ( - w_14 w_322) 1) ( <= ( - w_14 w_322) ( ~ 1)))
( or  ( not v_14_2 ) ( not v_322_8 ) ( >= ( - w_14 w_322) 2) ( <= ( - w_14 w_322) ( ~ 1)))
( or  ( not v_14_8 ) ( not v_322_2 ) ( >= ( - w_14 w_322) 1) ( <= ( - w_14 w_322) ( ~ 2)))
( or  ( not v_14_8 ) ( not v_322_8 ) ( >= ( - w_14 w_322) 1) ( <= ( - w_14 w_322) ( ~ 1)))
( or  ( not v_14_2 ) ( not v_323_2 ) ( >= ( - w_14 w_323) 4) ( <= ( - w_14 w_323) ( ~ 4)))
( or  ( not v_14_2 ) ( not v_323_8 ) ( >= ( - w_14 w_323) 5) ( <= ( - w_14 w_323) ( ~ 4)))
( or  ( not v_14_8 ) ( not v_323_2 ) ( >= ( - w_14 w_323) 4) ( <= ( - w_14 w_323) ( ~ 5)))
( or  ( not v_14_8 ) ( not v_323_8 ) ( >= ( - w_14 w_323) 4) ( <= ( - w_14 w_323) ( ~ 4)))
( or  ( not v_14_2 ) ( not v_324_2 ) ( >= ( - w_14 w_324) 11) ( <= ( - w_14 w_324) ( ~ 11)))
( or  ( not v_14_2 ) ( not v_324_8 ) ( >= ( - w_14 w_324) 12) ( <= ( - w_14 w_324) ( ~ 11)))
( or  ( not v_14_8 ) ( not v_324_2 ) ( >= ( - w_14 w_324) 11) ( <= ( - w_14 w_324) ( ~ 12)))
( or  ( not v_14_8 ) ( not v_324_8 ) ( >= ( - w_14 w_324) 11) ( <= ( - w_14 w_324) ( ~ 11)))
( or  ( not v_14_2 ) ( not v_557_2 ) ( >= ( - w_14 w_557) 19) ( <= ( - w_14 w_557) ( ~ 19)))
( or  ( not v_14_2 ) ( not v_557_8 ) ( >= ( - w_14 w_557) 20) ( <= ( - w_14 w_557) ( ~ 19)))
( or  ( not v_14_8 ) ( not v_557_2 ) ( >= ( - w_14 w_557) 19) ( <= ( - w_14 w_557) ( ~ 20)))
( or  ( not v_14_8 ) ( not v_557_8 ) ( >= ( - w_14 w_557) 19) ( <= ( - w_14 w_557) ( ~ 19)))
( or  ( not v_14_2 ) ( not v_558_2 ) ( >= ( - w_14 w_558) 30) ( <= ( - w_14 w_558) ( ~ 30)))
( or  ( not v_14_2 ) ( not v_558_8 ) ( >= ( - w_14 w_558) 30) ( <= ( - w_14 w_558) ( ~ 29)))
( or  ( not v_14_8 ) ( not v_558_2 ) ( >= ( - w_14 w_558) 29) ( <= ( - w_14 w_558) ( ~ 30)))
( or  ( not v_14_8 ) ( not v_558_8 ) ( >= ( - w_14 w_558) 30) ( <= ( - w_14 w_558) ( ~ 30)))
( or  ( not v_14_2 ) ( not v_599_2 ) ( >= ( - w_14 w_599) 15) ( <= ( - w_14 w_599) ( ~ 15)))
( or  ( not v_14_2 ) ( not v_599_8 ) ( >= ( - w_14 w_599) 15) ( <= ( - w_14 w_599) ( ~ 14)))
( or  ( not v_14_8 ) ( not v_599_2 ) ( >= ( - w_14 w_599) 14) ( <= ( - w_14 w_599) ( ~ 15)))
( or  ( not v_14_8 ) ( not v_599_8 ) ( >= ( - w_14 w_599) 15) ( <= ( - w_14 w_599) ( ~ 15)))
( or  ( not v_14_2 ) ( not v_600_2 ) ( >= ( - w_14 w_600) 25) ( <= ( - w_14 w_600) ( ~ 25)))
( or  ( not v_14_2 ) ( not v_600_8 ) ( >= ( - w_14 w_600) 25) ( <= ( - w_14 w_600) ( ~ 25)))
( or  ( not v_14_8 ) ( not v_600_2 ) ( >= ( - w_14 w_600) 25) ( <= ( - w_14 w_600) ( ~ 25)))
( or  ( not v_14_8 ) ( not v_600_8 ) ( >= ( - w_14 w_600) 25) ( <= ( - w_14 w_600) ( ~ 25)))
( or  ( not v_14_2 ) ( not v_665_2 ) ( >= ( - w_14 w_665) 1) ( <= ( - w_14 w_665) ( ~ 1)))
( or  ( not v_14_2 ) ( not v_665_8 ) ( >= ( - w_14 w_665) 1) ( <= ( - w_14 w_665) ( ~ 1)))
( or  ( not v_14_8 ) ( not v_665_2 ) ( >= ( - w_14 w_665) 1) ( <= ( - w_14 w_665) ( ~ 1)))
( or  ( not v_14_8 ) ( not v_665_8 ) ( >= ( - w_14 w_665) 1) ( <= ( - w_14 w_665) ( ~ 1)))
( or  ( not v_14_2 ) ( not v_666_2 ) ( >= ( - w_14 w_666) 13) ( <= ( - w_14 w_666) ( ~ 13)))
( or  ( not v_14_2 ) ( not v_666_8 ) ( >= ( - w_14 w_666) 14) ( <= ( - w_14 w_666) ( ~ 13)))
( or  ( not v_14_8 ) ( not v_666_2 ) ( >= ( - w_14 w_666) 13) ( <= ( - w_14 w_666) ( ~ 14)))
( or  ( not v_14_8 ) ( not v_666_8 ) ( >= ( - w_14 w_666) 13) ( <= ( - w_14 w_666) ( ~ 13)))
( or  ( not v_14_2 ) ( not v_767_2 ) ( >= ( - w_14 w_767) 9) ( <= ( - w_14 w_767) ( ~ 9)))
( or  ( not v_14_2 ) ( not v_767_8 ) ( >= ( - w_14 w_767) 10) ( <= ( - w_14 w_767) ( ~ 9)))
( or  ( not v_14_8 ) ( not v_767_2 ) ( >= ( - w_14 w_767) 9) ( <= ( - w_14 w_767) ( ~ 10)))
( or  ( not v_14_8 ) ( not v_767_8 ) ( >= ( - w_14 w_767) 9) ( <= ( - w_14 w_767) ( ~ 9)))
( or  ( not v_14_2 ) ( not v_768_2 ) ( >= ( - w_14 w_768) 5) ( <= ( - w_14 w_768) ( ~ 5)))
( or  ( not v_14_2 ) ( not v_768_8 ) ( >= ( - w_14 w_768) 5) ( <= ( - w_14 w_768) ( ~ 4)))
( or  ( not v_14_8 ) ( not v_768_2 ) ( >= ( - w_14 w_768) 4) ( <= ( - w_14 w_768) ( ~ 5)))
( or  ( not v_14_8 ) ( not v_768_8 ) ( >= ( - w_14 w_768) 5) ( <= ( - w_14 w_768) ( ~ 5)))
( or  ( not v_15_2 ) ( not v_16_2 ) ( = ( - w_15 w_16) 17) ( = ( - w_16 w_15) 17))
( or  ( not v_15_2 ) ( not v_16_8 ))
( or  ( not v_15_8 ) ( not v_16_2 ))
( or  ( not v_15_8 ) ( not v_16_8 ) ( = ( - w_15 w_16) 17) ( = ( - w_16 w_15) 17))
( or  ( not v_15_2 ) ( not v_321_2 ) ( >= ( - w_15 w_321) 1) ( <= ( - w_15 w_321) ( ~ 1)))
( or  ( not v_15_2 ) ( not v_321_8 ) ( >= ( - w_15 w_321) 2) ( <= ( - w_15 w_321) ( ~ 1)))
( or  ( not v_15_8 ) ( not v_321_2 ) ( >= ( - w_15 w_321) 1) ( <= ( - w_15 w_321) ( ~ 2)))
( or  ( not v_15_8 ) ( not v_321_8 ) ( >= ( - w_15 w_321) 1) ( <= ( - w_15 w_321) ( ~ 1)))
( or  ( not v_15_2 ) ( not v_322_2 ) ( >= ( - w_15 w_322) 14) ( <= ( - w_15 w_322) ( ~ 14)))
( or  ( not v_15_2 ) ( not v_322_8 ) ( >= ( - w_15 w_322) 14) ( <= ( - w_15 w_322) ( ~ 13)))
( or  ( not v_15_8 ) ( not v_322_2 ) ( >= ( - w_15 w_322) 13) ( <= ( - w_15 w_322) ( ~ 14)))
( or  ( not v_15_8 ) ( not v_322_8 ) ( >= ( - w_15 w_322) 14) ( <= ( - w_15 w_322) ( ~ 14)))
( or  ( not v_15_2 ) ( not v_323_2 ) ( >= ( - w_15 w_323) 12) ( <= ( - w_15 w_323) ( ~ 12)))
( or  ( not v_15_2 ) ( not v_323_8 ) ( >= ( - w_15 w_323) 13) ( <= ( - w_15 w_323) ( ~ 12)))
( or  ( not v_15_8 ) ( not v_323_2 ) ( >= ( - w_15 w_323) 12) ( <= ( - w_15 w_323) ( ~ 13)))
( or  ( not v_15_8 ) ( not v_323_8 ) ( >= ( - w_15 w_323) 12) ( <= ( - w_15 w_323) ( ~ 12)))
( or  ( not v_15_2 ) ( not v_324_2 ) ( >= ( - w_15 w_324) 4) ( <= ( - w_15 w_324) ( ~ 4)))
( or  ( not v_15_2 ) ( not v_324_8 ) ( >= ( - w_15 w_324) 5) ( <= ( - w_15 w_324) ( ~ 4)))
( or  ( not v_15_8 ) ( not v_324_2 ) ( >= ( - w_15 w_324) 4) ( <= ( - w_15 w_324) ( ~ 5)))
( or  ( not v_15_8 ) ( not v_324_8 ) ( >= ( - w_15 w_324) 4) ( <= ( - w_15 w_324) ( ~ 4)))
( or  ( not v_15_2 ) ( not v_557_2 ) ( >= ( - w_15 w_557) 7) ( <= ( - w_15 w_557) ( ~ 7)))
( or  ( not v_15_2 ) ( not v_557_8 ) ( >= ( - w_15 w_557) 7) ( <= ( - w_15 w_557) ( ~ 7)))
( or  ( not v_15_8 ) ( not v_557_2 ) ( >= ( - w_15 w_557) 7) ( <= ( - w_15 w_557) ( ~ 7)))
( or  ( not v_15_8 ) ( not v_557_8 ) ( >= ( - w_15 w_557) 7) ( <= ( - w_15 w_557) ( ~ 7)))
( or  ( not v_15_2 ) ( not v_558_2 ) ( >= ( - w_15 w_558) 19) ( <= ( - w_15 w_558) ( ~ 19)))
( or  ( not v_15_2 ) ( not v_558_8 ) ( >= ( - w_15 w_558) 20) ( <= ( - w_15 w_558) ( ~ 19)))
( or  ( not v_15_8 ) ( not v_558_2 ) ( >= ( - w_15 w_558) 19) ( <= ( - w_15 w_558) ( ~ 20)))
( or  ( not v_15_8 ) ( not v_558_8 ) ( >= ( - w_15 w_558) 19) ( <= ( - w_15 w_558) ( ~ 19)))
( or  ( not v_15_2 ) ( not v_599_2 ) ( >= ( - w_15 w_599) 2) ( <= ( - w_15 w_599) ( ~ 2)))
( or  ( not v_15_2 ) ( not v_599_8 ) ( >= ( - w_15 w_599) 3) ( <= ( - w_15 w_599) ( ~ 2)))
( or  ( not v_15_8 ) ( not v_599_2 ) ( >= ( - w_15 w_599) 2) ( <= ( - w_15 w_599) ( ~ 3)))
( or  ( not v_15_8 ) ( not v_599_8 ) ( >= ( - w_15 w_599) 2) ( <= ( - w_15 w_599) ( ~ 2)))
( or  ( not v_15_2 ) ( not v_600_2 ) ( >= ( - w_15 w_600) 15) ( <= ( - w_15 w_600) ( ~ 15)))
( or  ( not v_15_2 ) ( not v_600_8 ) ( >= ( - w_15 w_600) 15) ( <= ( - w_15 w_600) ( ~ 14)))
( or  ( not v_15_8 ) ( not v_600_2 ) ( >= ( - w_15 w_600) 14) ( <= ( - w_15 w_600) ( ~ 15)))
( or  ( not v_15_8 ) ( not v_600_8 ) ( >= ( - w_15 w_600) 15) ( <= ( - w_15 w_600) ( ~ 15)))
( or  ( not v_15_2 ) ( not v_665_2 ) ( >= ( - w_15 w_665) 13) ( <= ( - w_15 w_665) ( ~ 13)))
( or  ( not v_15_2 ) ( not v_665_8 ) ( >= ( - w_15 w_665) 14) ( <= ( - w_15 w_665) ( ~ 13)))
( or  ( not v_15_8 ) ( not v_665_2 ) ( >= ( - w_15 w_665) 13) ( <= ( - w_15 w_665) ( ~ 14)))
( or  ( not v_15_8 ) ( not v_665_8 ) ( >= ( - w_15 w_665) 13) ( <= ( - w_15 w_665) ( ~ 13)))
( or  ( not v_15_2 ) ( not v_666_2 ) ( >= ( - w_15 w_666) 1) ( <= ( - w_15 w_666) ( ~ 1)))
( or  ( not v_15_2 ) ( not v_666_8 ) ( >= ( - w_15 w_666) 1) ( <= ( - w_15 w_666) ( ~ 1)))
( or  ( not v_15_8 ) ( not v_666_2 ) ( >= ( - w_15 w_666) 1) ( <= ( - w_15 w_666) ( ~ 1)))
( or  ( not v_15_8 ) ( not v_666_8 ) ( >= ( - w_15 w_666) 1) ( <= ( - w_15 w_666) ( ~ 1)))
( or  ( not v_15_2 ) ( not v_767_2 ) ( >= ( - w_15 w_767) 5) ( <= ( - w_15 w_767) ( ~ 5)))
( or  ( not v_15_2 ) ( not v_767_8 ) ( >= ( - w_15 w_767) 5) ( <= ( - w_15 w_767) ( ~ 4)))
( or  ( not v_15_8 ) ( not v_767_2 ) ( >= ( - w_15 w_767) 4) ( <= ( - w_15 w_767) ( ~ 5)))
( or  ( not v_15_8 ) ( not v_767_8 ) ( >= ( - w_15 w_767) 5) ( <= ( - w_15 w_767) ( ~ 5)))
( or  ( not v_15_2 ) ( not v_768_2 ) ( >= ( - w_15 w_768) 17) ( <= ( - w_15 w_768) ( ~ 17)))
( or  ( not v_15_2 ) ( not v_768_8 ) ( >= ( - w_15 w_768) 18) ( <= ( - w_15 w_768) ( ~ 17)))
( or  ( not v_15_8 ) ( not v_768_2 ) ( >= ( - w_15 w_768) 17) ( <= ( - w_15 w_768) ( ~ 18)))
( or  ( not v_15_8 ) ( not v_768_8 ) ( >= ( - w_15 w_768) 17) ( <= ( - w_15 w_768) ( ~ 17)))
( or  ( not v_16_2 ) ( not v_321_2 ) ( >= ( - w_16 w_321) 12) ( <= ( - w_16 w_321) ( ~ 12)))
( or  ( not v_16_2 ) ( not v_321_8 ) ( >= ( - w_16 w_321) 13) ( <= ( - w_16 w_321) ( ~ 12)))
( or  ( not v_16_8 ) ( not v_321_2 ) ( >= ( - w_16 w_321) 12) ( <= ( - w_16 w_321) ( ~ 13)))
( or  ( not v_16_8 ) ( not v_321_8 ) ( >= ( - w_16 w_321) 12) ( <= ( - w_16 w_321) ( ~ 12)))
( or  ( not v_16_2 ) ( not v_322_2 ) ( >= ( - w_16 w_322) 1) ( <= ( - w_16 w_322) ( ~ 1)))
( or  ( not v_16_2 ) ( not v_322_8 ) ( >= ( - w_16 w_322) 2) ( <= ( - w_16 w_322) ( ~ 1)))
( or  ( not v_16_8 ) ( not v_322_2 ) ( >= ( - w_16 w_322) 1) ( <= ( - w_16 w_322) ( ~ 2)))
( or  ( not v_16_8 ) ( not v_322_8 ) ( >= ( - w_16 w_322) 1) ( <= ( - w_16 w_322) ( ~ 1)))
( or  ( not v_16_2 ) ( not v_323_2 ) ( >= ( - w_16 w_323) 4) ( <= ( - w_16 w_323) ( ~ 4)))
( or  ( not v_16_2 ) ( not v_323_8 ) ( >= ( - w_16 w_323) 5) ( <= ( - w_16 w_323) ( ~ 4)))
( or  ( not v_16_8 ) ( not v_323_2 ) ( >= ( - w_16 w_323) 4) ( <= ( - w_16 w_323) ( ~ 5)))
( or  ( not v_16_8 ) ( not v_323_8 ) ( >= ( - w_16 w_323) 4) ( <= ( - w_16 w_323) ( ~ 4)))
( or  ( not v_16_2 ) ( not v_324_2 ) ( >= ( - w_16 w_324) 11) ( <= ( - w_16 w_324) ( ~ 11)))
( or  ( not v_16_2 ) ( not v_324_8 ) ( >= ( - w_16 w_324) 12) ( <= ( - w_16 w_324) ( ~ 11)))
( or  ( not v_16_8 ) ( not v_324_2 ) ( >= ( - w_16 w_324) 11) ( <= ( - w_16 w_324) ( ~ 12)))
( or  ( not v_16_8 ) ( not v_324_8 ) ( >= ( - w_16 w_324) 11) ( <= ( - w_16 w_324) ( ~ 11)))
( or  ( not v_16_2 ) ( not v_557_2 ) ( >= ( - w_16 w_557) 19) ( <= ( - w_16 w_557) ( ~ 19)))
( or  ( not v_16_2 ) ( not v_557_8 ) ( >= ( - w_16 w_557) 20) ( <= ( - w_16 w_557) ( ~ 19)))
( or  ( not v_16_8 ) ( not v_557_2 ) ( >= ( - w_16 w_557) 19) ( <= ( - w_16 w_557) ( ~ 20)))
( or  ( not v_16_8 ) ( not v_557_8 ) ( >= ( - w_16 w_557) 19) ( <= ( - w_16 w_557) ( ~ 19)))
( or  ( not v_16_2 ) ( not v_558_2 ) ( >= ( - w_16 w_558) 30) ( <= ( - w_16 w_558) ( ~ 30)))
( or  ( not v_16_2 ) ( not v_558_8 ) ( >= ( - w_16 w_558) 30) ( <= ( - w_16 w_558) ( ~ 29)))
( or  ( not v_16_8 ) ( not v_558_2 ) ( >= ( - w_16 w_558) 29) ( <= ( - w_16 w_558) ( ~ 30)))
( or  ( not v_16_8 ) ( not v_558_8 ) ( >= ( - w_16 w_558) 30) ( <= ( - w_16 w_558) ( ~ 30)))
( or  ( not v_16_2 ) ( not v_599_2 ) ( >= ( - w_16 w_599) 15) ( <= ( - w_16 w_599) ( ~ 15)))
( or  ( not v_16_2 ) ( not v_599_8 ) ( >= ( - w_16 w_599) 15) ( <= ( - w_16 w_599) ( ~ 14)))
( or  ( not v_16_8 ) ( not v_599_2 ) ( >= ( - w_16 w_599) 14) ( <= ( - w_16 w_599) ( ~ 15)))
( or  ( not v_16_8 ) ( not v_599_8 ) ( >= ( - w_16 w_599) 15) ( <= ( - w_16 w_599) ( ~ 15)))
( or  ( not v_16_2 ) ( not v_600_2 ) ( >= ( - w_16 w_600) 25) ( <= ( - w_16 w_600) ( ~ 25)))
( or  ( not v_16_2 ) ( not v_600_8 ) ( >= ( - w_16 w_600) 25) ( <= ( - w_16 w_600) ( ~ 25)))
( or  ( not v_16_8 ) ( not v_600_2 ) ( >= ( - w_16 w_600) 25) ( <= ( - w_16 w_600) ( ~ 25)))
( or  ( not v_16_8 ) ( not v_600_8 ) ( >= ( - w_16 w_600) 25) ( <= ( - w_16 w_600) ( ~ 25)))
( or  ( not v_16_2 ) ( not v_665_2 ) ( >= ( - w_16 w_665) 1) ( <= ( - w_16 w_665) ( ~ 1)))
( or  ( not v_16_2 ) ( not v_665_8 ) ( >= ( - w_16 w_665) 1) ( <= ( - w_16 w_665) ( ~ 1)))
( or  ( not v_16_8 ) ( not v_665_2 ) ( >= ( - w_16 w_665) 1) ( <= ( - w_16 w_665) ( ~ 1)))
( or  ( not v_16_8 ) ( not v_665_8 ) ( >= ( - w_16 w_665) 1) ( <= ( - w_16 w_665) ( ~ 1)))
( or  ( not v_16_2 ) ( not v_666_2 ) ( >= ( - w_16 w_666) 13) ( <= ( - w_16 w_666) ( ~ 13)))
( or  ( not v_16_2 ) ( not v_666_8 ) ( >= ( - w_16 w_666) 14) ( <= ( - w_16 w_666) ( ~ 13)))
( or  ( not v_16_8 ) ( not v_666_2 ) ( >= ( - w_16 w_666) 13) ( <= ( - w_16 w_666) ( ~ 14)))
( or  ( not v_16_8 ) ( not v_666_8 ) ( >= ( - w_16 w_666) 13) ( <= ( - w_16 w_666) ( ~ 13)))
( or  ( not v_16_2 ) ( not v_767_2 ) ( >= ( - w_16 w_767) 9) ( <= ( - w_16 w_767) ( ~ 9)))
( or  ( not v_16_2 ) ( not v_767_8 ) ( >= ( - w_16 w_767) 10) ( <= ( - w_16 w_767) ( ~ 9)))
( or  ( not v_16_8 ) ( not v_767_2 ) ( >= ( - w_16 w_767) 9) ( <= ( - w_16 w_767) ( ~ 10)))
( or  ( not v_16_8 ) ( not v_767_8 ) ( >= ( - w_16 w_767) 9) ( <= ( - w_16 w_767) ( ~ 9)))
( or  ( not v_16_2 ) ( not v_768_2 ) ( >= ( - w_16 w_768) 5) ( <= ( - w_16 w_768) ( ~ 5)))
( or  ( not v_16_2 ) ( not v_768_8 ) ( >= ( - w_16 w_768) 5) ( <= ( - w_16 w_768) ( ~ 4)))
( or  ( not v_16_8 ) ( not v_768_2 ) ( >= ( - w_16 w_768) 4) ( <= ( - w_16 w_768) ( ~ 5)))
( or  ( not v_16_8 ) ( not v_768_8 ) ( >= ( - w_16 w_768) 5) ( <= ( - w_16 w_768) ( ~ 5)))
( or  ( not v_321_2 ) ( not v_322_2 ) ( = ( - w_321 w_322) 17) ( = ( - w_322 w_321) 17))
( or  ( not v_321_2 ) ( not v_322_8 ))
( or  ( not v_321_8 ) ( not v_322_2 ))
( or  ( not v_321_8 ) ( not v_322_8 ) ( = ( - w_321 w_322) 17) ( = ( - w_322 w_321) 17))
( or  ( not v_321_2 ) ( not v_323_2 ) ( >= ( - w_321 w_323) 13) ( <= ( - w_321 w_323) ( ~ 13)))
( or  ( not v_321_2 ) ( not v_323_8 ) ( >= ( - w_321 w_323) 14) ( <= ( - w_321 w_323) ( ~ 13)))
( or  ( not v_321_8 ) ( not v_323_2 ) ( >= ( - w_321 w_323) 13) ( <= ( - w_321 w_323) ( ~ 14)))
( or  ( not v_321_8 ) ( not v_323_8 ) ( >= ( - w_321 w_323) 13) ( <= ( - w_321 w_323) ( ~ 13)))
( or  ( not v_321_2 ) ( not v_324_2 ) ( >= ( - w_321 w_324) 6) ( <= ( - w_321 w_324) ( ~ 6)))
( or  ( not v_321_2 ) ( not v_324_8 ) ( >= ( - w_321 w_324) 7) ( <= ( - w_321 w_324) ( ~ 6)))
( or  ( not v_321_8 ) ( not v_324_2 ) ( >= ( - w_321 w_324) 6) ( <= ( - w_321 w_324) ( ~ 7)))
( or  ( not v_321_8 ) ( not v_324_8 ) ( >= ( - w_321 w_324) 6) ( <= ( - w_321 w_324) ( ~ 6)))
( or  ( not v_321_2 ) ( not v_557_2 ) ( >= ( - w_321 w_557) 8) ( <= ( - w_321 w_557) ( ~ 8)))
( or  ( not v_321_2 ) ( not v_557_8 ) ( >= ( - w_321 w_557) 8) ( <= ( - w_321 w_557) ( ~ 7)))
( or  ( not v_321_8 ) ( not v_557_2 ) ( >= ( - w_321 w_557) 7) ( <= ( - w_321 w_557) ( ~ 8)))
( or  ( not v_321_8 ) ( not v_557_8 ) ( >= ( - w_321 w_557) 8) ( <= ( - w_321 w_557) ( ~ 8)))
( or  ( not v_321_2 ) ( not v_558_2 ) ( >= ( - w_321 w_558) 20) ( <= ( - w_321 w_558) ( ~ 20)))
( or  ( not v_321_2 ) ( not v_558_8 ) ( >= ( - w_321 w_558) 20) ( <= ( - w_321 w_558) ( ~ 20)))
( or  ( not v_321_8 ) ( not v_558_2 ) ( >= ( - w_321 w_558) 20) ( <= ( - w_321 w_558) ( ~ 20)))
( or  ( not v_321_8 ) ( not v_558_8 ) ( >= ( - w_321 w_558) 20) ( <= ( - w_321 w_558) ( ~ 20)))
( or  ( not v_321_2 ) ( not v_594_2 ) ( >= ( - w_321 w_594) 16) ( <= ( - w_321 w_594) ( ~ 16)))
( or  ( not v_321_2 ) ( not v_594_8 ) ( >= ( - w_321 w_594) 16) ( <= ( - w_321 w_594) ( ~ 15)))
( or  ( not v_321_8 ) ( not v_594_2 ) ( >= ( - w_321 w_594) 15) ( <= ( - w_321 w_594) ( ~ 16)))
( or  ( not v_321_8 ) ( not v_594_8 ) ( >= ( - w_321 w_594) 16) ( <= ( - w_321 w_594) ( ~ 16)))
( or  ( not v_321_2 ) ( not v_599_2 ) ( >= ( - w_321 w_599) 3) ( <= ( - w_321 w_599) ( ~ 3)))
( or  ( not v_321_2 ) ( not v_599_8 ) ( >= ( - w_321 w_599) 3) ( <= ( - w_321 w_599) ( ~ 2)))
( or  ( not v_321_8 ) ( not v_599_2 ) ( >= ( - w_321 w_599) 2) ( <= ( - w_321 w_599) ( ~ 3)))
( or  ( not v_321_8 ) ( not v_599_8 ) ( >= ( - w_321 w_599) 3) ( <= ( - w_321 w_599) ( ~ 3)))
( or  ( not v_321_2 ) ( not v_600_2 ) ( >= ( - w_321 w_600) 15) ( <= ( - w_321 w_600) ( ~ 15)))
( or  ( not v_321_2 ) ( not v_600_8 ) ( >= ( - w_321 w_600) 16) ( <= ( - w_321 w_600) ( ~ 15)))
( or  ( not v_321_8 ) ( not v_600_2 ) ( >= ( - w_321 w_600) 15) ( <= ( - w_321 w_600) ( ~ 16)))
( or  ( not v_321_8 ) ( not v_600_8 ) ( >= ( - w_321 w_600) 15) ( <= ( - w_321 w_600) ( ~ 15)))
( or  ( not v_321_2 ) ( not v_631_2 ) ( >= ( - w_321 w_631) 14) ( <= ( - w_321 w_631) ( ~ 14)))
( or  ( not v_321_2 ) ( not v_631_8 ) ( >= ( - w_321 w_631) 15) ( <= ( - w_321 w_631) ( ~ 14)))
( or  ( not v_321_8 ) ( not v_631_2 ) ( >= ( - w_321 w_631) 14) ( <= ( - w_321 w_631) ( ~ 15)))
( or  ( not v_321_8 ) ( not v_631_8 ) ( >= ( - w_321 w_631) 14) ( <= ( - w_321 w_631) ( ~ 14)))
( or  ( not v_321_2 ) ( not v_665_2 ) ( >= ( - w_321 w_665) 12) ( <= ( - w_321 w_665) ( ~ 12)))
( or  ( not v_321_2 ) ( not v_665_8 ) ( >= ( - w_321 w_665) 13) ( <= ( - w_321 w_665) ( ~ 12)))
( or  ( not v_321_8 ) ( not v_665_2 ) ( >= ( - w_321 w_665) 12) ( <= ( - w_321 w_665) ( ~ 13)))
( or  ( not v_321_8 ) ( not v_665_8 ) ( >= ( - w_321 w_665) 12) ( <= ( - w_321 w_665) ( ~ 12)))
( or  ( not v_321_2 ) ( not v_666_2 ) ( >= ( - w_321 w_666) 1) ( <= ( - w_321 w_666) ( ~ 1)))
( or  ( not v_321_2 ) ( not v_666_8 ) ( >= ( - w_321 w_666) 2) ( <= ( - w_321 w_666) ( ~ 1)))
( or  ( not v_321_8 ) ( not v_666_2 ) ( >= ( - w_321 w_666) 1) ( <= ( - w_321 w_666) ( ~ 2)))
( or  ( not v_321_8 ) ( not v_666_8 ) ( >= ( - w_321 w_666) 1) ( <= ( - w_321 w_666) ( ~ 1)))
( or  ( not v_321_2 ) ( not v_767_2 ) ( >= ( - w_321 w_767) 5) ( <= ( - w_321 w_767) ( ~ 5)))
( or  ( not v_321_2 ) ( not v_767_8 ) ( >= ( - w_321 w_767) 5) ( <= ( - w_321 w_767) ( ~ 4)))
( or  ( not v_321_8 ) ( not v_767_2 ) ( >= ( - w_321 w_767) 4) ( <= ( - w_321 w_767) ( ~ 5)))
( or  ( not v_321_8 ) ( not v_767_8 ) ( >= ( - w_321 w_767) 5) ( <= ( - w_321 w_767) ( ~ 5)))
( or  ( not v_321_2 ) ( not v_768_2 ) ( >= ( - w_321 w_768) 16) ( <= ( - w_321 w_768) ( ~ 16)))
( or  ( not v_321_2 ) ( not v_768_8 ) ( >= ( - w_321 w_768) 17) ( <= ( - w_321 w_768) ( ~ 16)))
( or  ( not v_321_8 ) ( not v_768_2 ) ( >= ( - w_321 w_768) 16) ( <= ( - w_321 w_768) ( ~ 17)))
( or  ( not v_321_8 ) ( not v_768_8 ) ( >= ( - w_321 w_768) 16) ( <= ( - w_321 w_768) ( ~ 16)))
( or  ( not v_322_2 ) ( not v_323_2 ) ( >= ( - w_322 w_323) 6) ( <= ( - w_322 w_323) ( ~ 6)))
( or  ( not v_322_2 ) ( not v_323_8 ) ( >= ( - w_322 w_323) 7) ( <= ( - w_322 w_323) ( ~ 6)))
( or  ( not v_322_8 ) ( not v_323_2 ) ( >= ( - w_322 w_323) 6) ( <= ( - w_322 w_323) ( ~ 7)))
( or  ( not v_322_8 ) ( not v_323_8 ) ( >= ( - w_322 w_323) 6) ( <= ( - w_322 w_323) ( ~ 6)))
( or  ( not v_322_2 ) ( not v_324_2 ) ( >= ( - w_322 w_324) 13) ( <= ( - w_322 w_324) ( ~ 13)))
( or  ( not v_322_2 ) ( not v_324_8 ) ( >= ( - w_322 w_324) 14) ( <= ( - w_322 w_324) ( ~ 13)))
( or  ( not v_322_8 ) ( not v_324_2 ) ( >= ( - w_322 w_324) 13) ( <= ( - w_322 w_324) ( ~ 14)))
( or  ( not v_322_8 ) ( not v_324_8 ) ( >= ( - w_322 w_324) 13) ( <= ( - w_322 w_324) ( ~ 13)))
( or  ( not v_322_2 ) ( not v_557_2 ) ( >= ( - w_322 w_557) 20) ( <= ( - w_322 w_557) ( ~ 20)))
( or  ( not v_322_2 ) ( not v_557_8 ) ( >= ( - w_322 w_557) 20) ( <= ( - w_322 w_557) ( ~ 20)))
( or  ( not v_322_8 ) ( not v_557_2 ) ( >= ( - w_322 w_557) 20) ( <= ( - w_322 w_557) ( ~ 20)))
( or  ( not v_322_8 ) ( not v_557_8 ) ( >= ( - w_322 w_557) 20) ( <= ( - w_322 w_557) ( ~ 20)))
( or  ( not v_322_2 ) ( not v_558_2 ) ( >= ( - w_322 w_558) 30) ( <= ( - w_322 w_558) ( ~ 30)))
( or  ( not v_322_2 ) ( not v_558_8 ) ( >= ( - w_322 w_558) 31) ( <= ( - w_322 w_558) ( ~ 30)))
( or  ( not v_322_8 ) ( not v_558_2 ) ( >= ( - w_322 w_558) 30) ( <= ( - w_322 w_558) ( ~ 31)))
( or  ( not v_322_8 ) ( not v_558_8 ) ( >= ( - w_322 w_558) 30) ( <= ( - w_322 w_558) ( ~ 30)))
( or  ( not v_322_2 ) ( not v_599_2 ) ( >= ( - w_322 w_599) 15) ( <= ( - w_322 w_599) ( ~ 15)))
( or  ( not v_322_2 ) ( not v_599_8 ) ( >= ( - w_322 w_599) 16) ( <= ( - w_322 w_599) ( ~ 15)))
( or  ( not v_322_8 ) ( not v_599_2 ) ( >= ( - w_322 w_599) 15) ( <= ( - w_322 w_599) ( ~ 16)))
( or  ( not v_322_8 ) ( not v_599_8 ) ( >= ( - w_322 w_599) 15) ( <= ( - w_322 w_599) ( ~ 15)))
( or  ( not v_322_2 ) ( not v_600_2 ) ( >= ( - w_322 w_600) 26) ( <= ( - w_322 w_600) ( ~ 26)))
( or  ( not v_322_2 ) ( not v_600_8 ) ( >= ( - w_322 w_600) 26) ( <= ( - w_322 w_600) ( ~ 25)))
( or  ( not v_322_8 ) ( not v_600_2 ) ( >= ( - w_322 w_600) 25) ( <= ( - w_322 w_600) ( ~ 26)))
( or  ( not v_322_8 ) ( not v_600_8 ) ( >= ( - w_322 w_600) 26) ( <= ( - w_322 w_600) ( ~ 26)))
( or  ( not v_322_2 ) ( not v_665_2 ) ( >= ( - w_322 w_665) 1) ( <= ( - w_322 w_665) ( ~ 1)))
( or  ( not v_322_2 ) ( not v_665_8 ) ( >= ( - w_322 w_665) 2) ( <= ( - w_322 w_665) ( ~ 1)))
( or  ( not v_322_8 ) ( not v_665_2 ) ( >= ( - w_322 w_665) 1) ( <= ( - w_322 w_665) ( ~ 2)))
( or  ( not v_322_8 ) ( not v_665_8 ) ( >= ( - w_322 w_665) 1) ( <= ( - w_322 w_665) ( ~ 1)))
( or  ( not v_322_2 ) ( not v_666_2 ) ( >= ( - w_322 w_666) 14) ( <= ( - w_322 w_666) ( ~ 14)))
( or  ( not v_322_2 ) ( not v_666_8 ) ( >= ( - w_322 w_666) 14) ( <= ( - w_322 w_666) ( ~ 13)))
( or  ( not v_322_8 ) ( not v_666_2 ) ( >= ( - w_322 w_666) 13) ( <= ( - w_322 w_666) ( ~ 14)))
( or  ( not v_322_8 ) ( not v_666_8 ) ( >= ( - w_322 w_666) 14) ( <= ( - w_322 w_666) ( ~ 14)))
( or  ( not v_322_2 ) ( not v_767_2 ) ( >= ( - w_322 w_767) 10) ( <= ( - w_322 w_767) ( ~ 10)))
( or  ( not v_322_2 ) ( not v_767_8 ) ( >= ( - w_322 w_767) 10) ( <= ( - w_322 w_767) ( ~ 9)))
( or  ( not v_322_8 ) ( not v_767_2 ) ( >= ( - w_322 w_767) 9) ( <= ( - w_322 w_767) ( ~ 10)))
( or  ( not v_322_8 ) ( not v_767_8 ) ( >= ( - w_322 w_767) 10) ( <= ( - w_322 w_767) ( ~ 10)))
( or  ( not v_322_2 ) ( not v_768_2 ) ( >= ( - w_322 w_768) 4) ( <= ( - w_322 w_768) ( ~ 4)))
( or  ( not v_322_2 ) ( not v_768_8 ) ( >= ( - w_322 w_768) 5) ( <= ( - w_322 w_768) ( ~ 4)))
( or  ( not v_322_8 ) ( not v_768_2 ) ( >= ( - w_322 w_768) 4) ( <= ( - w_322 w_768) ( ~ 5)))
( or  ( not v_322_8 ) ( not v_768_8 ) ( >= ( - w_322 w_768) 4) ( <= ( - w_322 w_768) ( ~ 4)))
( or  ( not v_323_2 ) ( not v_324_2 ) ( = ( - w_323 w_324) 17) ( = ( - w_324 w_323) 17))
( or  ( not v_323_2 ) ( not v_324_8 ))
( or  ( not v_323_8 ) ( not v_324_2 ))
( or  ( not v_323_8 ) ( not v_324_8 ) ( = ( - w_323 w_324) 17) ( = ( - w_324 w_323) 17))
( or  ( not v_323_2 ) ( not v_557_2 ) ( >= ( - w_323 w_557) 19) ( <= ( - w_323 w_557) ( ~ 19)))
( or  ( not v_323_2 ) ( not v_557_8 ) ( >= ( - w_323 w_557) 19) ( <= ( - w_323 w_557) ( ~ 18)))
( or  ( not v_323_8 ) ( not v_557_2 ) ( >= ( - w_323 w_557) 18) ( <= ( - w_323 w_557) ( ~ 19)))
( or  ( not v_323_8 ) ( not v_557_8 ) ( >= ( - w_323 w_557) 19) ( <= ( - w_323 w_557) ( ~ 19)))
( or  ( not v_323_2 ) ( not v_558_2 ) ( >= ( - w_323 w_558) 31) ( <= ( - w_323 w_558) ( ~ 31)))
( or  ( not v_323_2 ) ( not v_558_8 ) ( >= ( - w_323 w_558) 32) ( <= ( - w_323 w_558) ( ~ 31)))
( or  ( not v_323_8 ) ( not v_558_2 ) ( >= ( - w_323 w_558) 31) ( <= ( - w_323 w_558) ( ~ 32)))
( or  ( not v_323_8 ) ( not v_558_8 ) ( >= ( - w_323 w_558) 31) ( <= ( - w_323 w_558) ( ~ 31)))
( or  ( not v_323_2 ) ( not v_594_2 ) ( >= ( - w_323 w_594) 5) ( <= ( - w_323 w_594) ( ~ 5)))
( or  ( not v_323_2 ) ( not v_594_8 ) ( >= ( - w_323 w_594) 5) ( <= ( - w_323 w_594) ( ~ 4)))
( or  ( not v_323_8 ) ( not v_594_2 ) ( >= ( - w_323 w_594) 4) ( <= ( - w_323 w_594) ( ~ 5)))
( or  ( not v_323_8 ) ( not v_594_8 ) ( >= ( - w_323 w_594) 5) ( <= ( - w_323 w_594) ( ~ 5)))
( or  ( not v_323_2 ) ( not v_599_2 ) ( >= ( - w_323 w_599) 14) ( <= ( - w_323 w_599) ( ~ 14)))
( or  ( not v_323_2 ) ( not v_599_8 ) ( >= ( - w_323 w_599) 15) ( <= ( - w_323 w_599) ( ~ 14)))
( or  ( not v_323_8 ) ( not v_599_2 ) ( >= ( - w_323 w_599) 14) ( <= ( - w_323 w_599) ( ~ 15)))
( or  ( not v_323_8 ) ( not v_599_8 ) ( >= ( - w_323 w_599) 14) ( <= ( - w_323 w_599) ( ~ 14)))
( or  ( not v_323_2 ) ( not v_600_2 ) ( >= ( - w_323 w_600) 27) ( <= ( - w_323 w_600) ( ~ 27)))
( or  ( not v_323_2 ) ( not v_600_8 ) ( >= ( - w_323 w_600) 27) ( <= ( - w_323 w_600) ( ~ 26)))
( or  ( not v_323_8 ) ( not v_600_2 ) ( >= ( - w_323 w_600) 26) ( <= ( - w_323 w_600) ( ~ 27)))
( or  ( not v_323_8 ) ( not v_600_8 ) ( >= ( - w_323 w_600) 27) ( <= ( - w_323 w_600) ( ~ 27)))
( or  ( not v_323_2 ) ( not v_631_2 ) ( >= ( - w_323 w_631) 26) ( <= ( - w_323 w_631) ( ~ 26)))
( or  ( not v_323_2 ) ( not v_631_8 ) ( >= ( - w_323 w_631) 26) ( <= ( - w_323 w_631) ( ~ 25)))
( or  ( not v_323_8 ) ( not v_631_2 ) ( >= ( - w_323 w_631) 25) ( <= ( - w_323 w_631) ( ~ 26)))
( or  ( not v_323_8 ) ( not v_631_8 ) ( >= ( - w_323 w_631) 26) ( <= ( - w_323 w_631) ( ~ 26)))
( or  ( not v_323_2 ) ( not v_665_2 ) ( >= ( - w_323 w_665) 4) ( <= ( - w_323 w_665) ( ~ 4)))
( or  ( not v_323_2 ) ( not v_665_8 ) ( >= ( - w_323 w_665) 5) ( <= ( - w_323 w_665) ( ~ 4)))
( or  ( not v_323_8 ) ( not v_665_2 ) ( >= ( - w_323 w_665) 4) ( <= ( - w_323 w_665) ( ~ 5)))
( or  ( not v_323_8 ) ( not v_665_8 ) ( >= ( - w_323 w_665) 4) ( <= ( - w_323 w_665) ( ~ 4)))
( or  ( not v_323_2 ) ( not v_666_2 ) ( >= ( - w_323 w_666) 13) ( <= ( - w_323 w_666) ( ~ 13)))
( or  ( not v_323_2 ) ( not v_666_8 ) ( >= ( - w_323 w_666) 13) ( <= ( - w_323 w_666) ( ~ 12)))
( or  ( not v_323_8 ) ( not v_666_2 ) ( >= ( - w_323 w_666) 12) ( <= ( - w_323 w_666) ( ~ 13)))
( or  ( not v_323_8 ) ( not v_666_8 ) ( >= ( - w_323 w_666) 13) ( <= ( - w_323 w_666) ( ~ 13)))
( or  ( not v_323_2 ) ( not v_767_2 ) ( >= ( - w_323 w_767) 9) ( <= ( - w_323 w_767) ( ~ 9)))
( or  ( not v_323_2 ) ( not v_767_8 ) ( >= ( - w_323 w_767) 10) ( <= ( - w_323 w_767) ( ~ 9)))
( or  ( not v_323_8 ) ( not v_767_2 ) ( >= ( - w_323 w_767) 9) ( <= ( - w_323 w_767) ( ~ 10)))
( or  ( not v_323_8 ) ( not v_767_8 ) ( >= ( - w_323 w_767) 9) ( <= ( - w_323 w_767) ( ~ 9)))
( or  ( not v_323_2 ) ( not v_768_2 ) ( >= ( - w_323 w_768) 5) ( <= ( - w_323 w_768) ( ~ 5)))
( or  ( not v_323_2 ) ( not v_768_8 ) ( >= ( - w_323 w_768) 6) ( <= ( - w_323 w_768) ( ~ 5)))
( or  ( not v_323_8 ) ( not v_768_2 ) ( >= ( - w_323 w_768) 5) ( <= ( - w_323 w_768) ( ~ 6)))
( or  ( not v_323_8 ) ( not v_768_8 ) ( >= ( - w_323 w_768) 5) ( <= ( - w_323 w_768) ( ~ 5)))
( or  ( not v_324_2 ) ( not v_557_2 ) ( >= ( - w_324 w_557) 9) ( <= ( - w_324 w_557) ( ~ 9)))
( or  ( not v_324_2 ) ( not v_557_8 ) ( >= ( - w_324 w_557) 9) ( <= ( - w_324 w_557) ( ~ 8)))
( or  ( not v_324_8 ) ( not v_557_2 ) ( >= ( - w_324 w_557) 8) ( <= ( - w_324 w_557) ( ~ 9)))
( or  ( not v_324_8 ) ( not v_557_8 ) ( >= ( - w_324 w_557) 9) ( <= ( - w_324 w_557) ( ~ 9)))
( or  ( not v_324_2 ) ( not v_558_2 ) ( >= ( - w_324 w_558) 19) ( <= ( - w_324 w_558) ( ~ 19)))
( or  ( not v_324_2 ) ( not v_558_8 ) ( >= ( - w_324 w_558) 19) ( <= ( - w_324 w_558) ( ~ 18)))
( or  ( not v_324_8 ) ( not v_558_2 ) ( >= ( - w_324 w_558) 18) ( <= ( - w_324 w_558) ( ~ 19)))
( or  ( not v_324_8 ) ( not v_558_8 ) ( >= ( - w_324 w_558) 19) ( <= ( - w_324 w_558) ( ~ 19)))
( or  ( not v_324_2 ) ( not v_599_2 ) ( >= ( - w_324 w_599) 4) ( <= ( - w_324 w_599) ( ~ 4)))
( or  ( not v_324_2 ) ( not v_599_8 ) ( >= ( - w_324 w_599) 5) ( <= ( - w_324 w_599) ( ~ 4)))
( or  ( not v_324_8 ) ( not v_599_2 ) ( >= ( - w_324 w_599) 4) ( <= ( - w_324 w_599) ( ~ 5)))
( or  ( not v_324_8 ) ( not v_599_8 ) ( >= ( - w_324 w_599) 4) ( <= ( - w_324 w_599) ( ~ 4)))
( or  ( not v_324_2 ) ( not v_600_2 ) ( >= ( - w_324 w_600) 14) ( <= ( - w_324 w_600) ( ~ 14)))
( or  ( not v_324_2 ) ( not v_600_8 ) ( >= ( - w_324 w_600) 15) ( <= ( - w_324 w_600) ( ~ 14)))
( or  ( not v_324_8 ) ( not v_600_2 ) ( >= ( - w_324 w_600) 14) ( <= ( - w_324 w_600) ( ~ 15)))
( or  ( not v_324_8 ) ( not v_600_8 ) ( >= ( - w_324 w_600) 14) ( <= ( - w_324 w_600) ( ~ 14)))
( or  ( not v_324_2 ) ( not v_665_2 ) ( >= ( - w_324 w_665) 11) ( <= ( - w_324 w_665) ( ~ 11)))
( or  ( not v_324_2 ) ( not v_665_8 ) ( >= ( - w_324 w_665) 12) ( <= ( - w_324 w_665) ( ~ 11)))
( or  ( not v_324_8 ) ( not v_665_2 ) ( >= ( - w_324 w_665) 11) ( <= ( - w_324 w_665) ( ~ 12)))
( or  ( not v_324_8 ) ( not v_665_8 ) ( >= ( - w_324 w_665) 11) ( <= ( - w_324 w_665) ( ~ 11)))
( or  ( not v_324_2 ) ( not v_666_2 ) ( >= ( - w_324 w_666) 4) ( <= ( - w_324 w_666) ( ~ 4)))
( or  ( not v_324_2 ) ( not v_666_8 ) ( >= ( - w_324 w_666) 5) ( <= ( - w_324 w_666) ( ~ 4)))
( or  ( not v_324_8 ) ( not v_666_2 ) ( >= ( - w_324 w_666) 4) ( <= ( - w_324 w_666) ( ~ 5)))
( or  ( not v_324_8 ) ( not v_666_8 ) ( >= ( - w_324 w_666) 4) ( <= ( - w_324 w_666) ( ~ 4)))
( or  ( not v_324_2 ) ( not v_767_2 ) ( >= ( - w_324 w_767) 5) ( <= ( - w_324 w_767) ( ~ 5)))
( or  ( not v_324_2 ) ( not v_767_8 ) ( >= ( - w_324 w_767) 6) ( <= ( - w_324 w_767) ( ~ 5)))
( or  ( not v_324_8 ) ( not v_767_2 ) ( >= ( - w_324 w_767) 5) ( <= ( - w_324 w_767) ( ~ 6)))
( or  ( not v_324_8 ) ( not v_767_8 ) ( >= ( - w_324 w_767) 5) ( <= ( - w_324 w_767) ( ~ 5)))
( or  ( not v_324_2 ) ( not v_768_2 ) ( >= ( - w_324 w_768) 16) ( <= ( - w_324 w_768) ( ~ 16)))
( or  ( not v_324_2 ) ( not v_768_8 ) ( >= ( - w_324 w_768) 16) ( <= ( - w_324 w_768) ( ~ 15)))
( or  ( not v_324_8 ) ( not v_768_2 ) ( >= ( - w_324 w_768) 15) ( <= ( - w_324 w_768) ( ~ 16)))
( or  ( not v_324_8 ) ( not v_768_8 ) ( >= ( - w_324 w_768) 16) ( <= ( - w_324 w_768) ( ~ 16)))
( or  ( not v_519_2 ) ( not v_520_2 ) ( = ( - w_519 w_520) 17) ( = ( - w_520 w_519) 17))
( or  ( not v_519_2 ) ( not v_520_8 ))
( or  ( not v_519_8 ) ( not v_520_2 ))
( or  ( not v_519_8 ) ( not v_520_8 ) ( = ( - w_519 w_520) 17) ( = ( - w_520 w_519) 17))
( or  ( not v_519_2 ) ( not v_597_2 ) ( >= ( - w_519 w_597) 21) ( <= ( - w_519 w_597) ( ~ 21)))
( or  ( not v_519_2 ) ( not v_597_8 ) ( >= ( - w_519 w_597) 22) ( <= ( - w_519 w_597) ( ~ 21)))
( or  ( not v_519_8 ) ( not v_597_2 ) ( >= ( - w_519 w_597) 21) ( <= ( - w_519 w_597) ( ~ 22)))
( or  ( not v_519_8 ) ( not v_597_8 ) ( >= ( - w_519 w_597) 21) ( <= ( - w_519 w_597) ( ~ 21)))
( or  ( not v_519_2 ) ( not v_598_2 ) ( >= ( - w_519 w_598) 31) ( <= ( - w_519 w_598) ( ~ 31)))
( or  ( not v_519_2 ) ( not v_598_8 ) ( >= ( - w_519 w_598) 32) ( <= ( - w_519 w_598) ( ~ 31)))
( or  ( not v_519_8 ) ( not v_598_2 ) ( >= ( - w_519 w_598) 31) ( <= ( - w_519 w_598) ( ~ 32)))
( or  ( not v_519_8 ) ( not v_598_8 ) ( >= ( - w_519 w_598) 31) ( <= ( - w_519 w_598) ( ~ 31)))
( or  ( not v_520_2 ) ( not v_597_2 ) ( >= ( - w_520 w_597) 9) ( <= ( - w_520 w_597) ( ~ 9)))
( or  ( not v_520_2 ) ( not v_597_8 ) ( >= ( - w_520 w_597) 9) ( <= ( - w_520 w_597) ( ~ 8)))
( or  ( not v_520_8 ) ( not v_597_2 ) ( >= ( - w_520 w_597) 8) ( <= ( - w_520 w_597) ( ~ 9)))
( or  ( not v_520_8 ) ( not v_597_8 ) ( >= ( - w_520 w_597) 9) ( <= ( - w_520 w_597) ( ~ 9)))
( or  ( not v_520_2 ) ( not v_598_2 ) ( >= ( - w_520 w_598) 21) ( <= ( - w_520 w_598) ( ~ 21)))
( or  ( not v_520_2 ) ( not v_598_8 ) ( >= ( - w_520 w_598) 22) ( <= ( - w_520 w_598) ( ~ 21)))
( or  ( not v_520_8 ) ( not v_598_2 ) ( >= ( - w_520 w_598) 21) ( <= ( - w_520 w_598) ( ~ 22)))
( or  ( not v_520_8 ) ( not v_598_8 ) ( >= ( - w_520 w_598) 21) ( <= ( - w_520 w_598) ( ~ 21)))
( or  ( not v_557_2 ) ( not v_558_2 ) ( = ( - w_557 w_558) 17) ( = ( - w_558 w_557) 17))
( or  ( not v_557_2 ) ( not v_558_8 ))
( or  ( not v_557_8 ) ( not v_558_2 ))
( or  ( not v_557_8 ) ( not v_558_8 ) ( = ( - w_557 w_558) 17) ( = ( - w_558 w_557) 17))
( or  ( not v_557_2 ) ( not v_593_2 ) ( >= ( - w_557 w_593) 11) ( <= ( - w_557 w_593) ( ~ 11)))
( or  ( not v_557_2 ) ( not v_593_8 ) ( >= ( - w_557 w_593) 12) ( <= ( - w_557 w_593) ( ~ 11)))
( or  ( not v_557_8 ) ( not v_593_2 ) ( >= ( - w_557 w_593) 11) ( <= ( - w_557 w_593) ( ~ 12)))
( or  ( not v_557_8 ) ( not v_593_8 ) ( >= ( - w_557 w_593) 11) ( <= ( - w_557 w_593) ( ~ 11)))
( or  ( not v_557_2 ) ( not v_594_2 ) ( >= ( - w_557 w_594) 24) ( <= ( - w_557 w_594) ( ~ 24)))
( or  ( not v_557_2 ) ( not v_594_8 ) ( >= ( - w_557 w_594) 24) ( <= ( - w_557 w_594) ( ~ 24)))
( or  ( not v_557_8 ) ( not v_594_2 ) ( >= ( - w_557 w_594) 24) ( <= ( - w_557 w_594) ( ~ 24)))
( or  ( not v_557_8 ) ( not v_594_8 ) ( >= ( - w_557 w_594) 24) ( <= ( - w_557 w_594) ( ~ 24)))
( or  ( not v_557_2 ) ( not v_597_2 ) ( >= ( - w_557 w_597) 4) ( <= ( - w_557 w_597) ( ~ 4)))
( or  ( not v_557_2 ) ( not v_597_8 ) ( >= ( - w_557 w_597) 4) ( <= ( - w_557 w_597) ( ~ 3)))
( or  ( not v_557_8 ) ( not v_597_2 ) ( >= ( - w_557 w_597) 3) ( <= ( - w_557 w_597) ( ~ 4)))
( or  ( not v_557_8 ) ( not v_597_8 ) ( >= ( - w_557 w_597) 4) ( <= ( - w_557 w_597) ( ~ 4)))
( or  ( not v_557_2 ) ( not v_598_2 ) ( >= ( - w_557 w_598) 10) ( <= ( - w_557 w_598) ( ~ 10)))
( or  ( not v_557_2 ) ( not v_598_8 ) ( >= ( - w_557 w_598) 10) ( <= ( - w_557 w_598) ( ~ 9)))
( or  ( not v_557_8 ) ( not v_598_2 ) ( >= ( - w_557 w_598) 9) ( <= ( - w_557 w_598) ( ~ 10)))
( or  ( not v_557_8 ) ( not v_598_8 ) ( >= ( - w_557 w_598) 10) ( <= ( - w_557 w_598) ( ~ 10)))
( or  ( not v_557_2 ) ( not v_599_2 ) ( >= ( - w_557 w_599) 5) ( <= ( - w_557 w_599) ( ~ 5)))
( or  ( not v_557_2 ) ( not v_599_8 ) ( >= ( - w_557 w_599) 6) ( <= ( - w_557 w_599) ( ~ 5)))
( or  ( not v_557_8 ) ( not v_599_2 ) ( >= ( - w_557 w_599) 5) ( <= ( - w_557 w_599) ( ~ 6)))
( or  ( not v_557_8 ) ( not v_599_8 ) ( >= ( - w_557 w_599) 5) ( <= ( - w_557 w_599) ( ~ 5)))
( or  ( not v_557_2 ) ( not v_600_2 ) ( >= ( - w_557 w_600) 8) ( <= ( - w_557 w_600) ( ~ 8)))
( or  ( not v_557_2 ) ( not v_600_8 ) ( >= ( - w_557 w_600) 9) ( <= ( - w_557 w_600) ( ~ 8)))
( or  ( not v_557_8 ) ( not v_600_2 ) ( >= ( - w_557 w_600) 8) ( <= ( - w_557 w_600) ( ~ 9)))
( or  ( not v_557_8 ) ( not v_600_8 ) ( >= ( - w_557 w_600) 8) ( <= ( - w_557 w_600) ( ~ 8)))
( or  ( not v_557_2 ) ( not v_613_2 ) ( >= ( - w_557 w_613) 4) ( <= ( - w_557 w_613) ( ~ 4)))
( or  ( not v_557_2 ) ( not v_613_8 ) ( >= ( - w_557 w_613) 4) ( <= ( - w_557 w_613) ( ~ 3)))
( or  ( not v_557_8 ) ( not v_613_2 ) ( >= ( - w_557 w_613) 3) ( <= ( - w_557 w_613) ( ~ 4)))
( or  ( not v_557_8 ) ( not v_613_8 ) ( >= ( - w_557 w_613) 4) ( <= ( - w_557 w_613) ( ~ 4)))
( or  ( not v_557_2 ) ( not v_614_2 ) ( >= ( - w_557 w_614) 10) ( <= ( - w_557 w_614) ( ~ 10)))
( or  ( not v_557_2 ) ( not v_614_8 ) ( >= ( - w_557 w_614) 10) ( <= ( - w_557 w_614) ( ~ 9)))
( or  ( not v_557_8 ) ( not v_614_2 ) ( >= ( - w_557 w_614) 9) ( <= ( - w_557 w_614) ( ~ 10)))
( or  ( not v_557_8 ) ( not v_614_8 ) ( >= ( - w_557 w_614) 10) ( <= ( - w_557 w_614) ( ~ 10)))
( or  ( not v_557_2 ) ( not v_665_2 ) ( >= ( - w_557 w_665) 20) ( <= ( - w_557 w_665) ( ~ 20)))
( or  ( not v_557_2 ) ( not v_665_8 ) ( >= ( - w_557 w_665) 20) ( <= ( - w_557 w_665) ( ~ 20)))
( or  ( not v_557_8 ) ( not v_665_2 ) ( >= ( - w_557 w_665) 20) ( <= ( - w_557 w_665) ( ~ 20)))
( or  ( not v_557_8 ) ( not v_665_8 ) ( >= ( - w_557 w_665) 20) ( <= ( - w_557 w_665) ( ~ 20)))
( or  ( not v_557_2 ) ( not v_666_2 ) ( >= ( - w_557 w_666) 8) ( <= ( - w_557 w_666) ( ~ 8)))
( or  ( not v_557_2 ) ( not v_666_8 ) ( >= ( - w_557 w_666) 8) ( <= ( - w_557 w_666) ( ~ 8)))
( or  ( not v_557_8 ) ( not v_666_2 ) ( >= ( - w_557 w_666) 8) ( <= ( - w_557 w_666) ( ~ 8)))
( or  ( not v_557_8 ) ( not v_666_8 ) ( >= ( - w_557 w_666) 8) ( <= ( - w_557 w_666) ( ~ 8)))
( or  ( not v_557_2 ) ( not v_767_2 ) ( >= ( - w_557 w_767) 11) ( <= ( - w_557 w_767) ( ~ 11)))
( or  ( not v_557_2 ) ( not v_767_8 ) ( >= ( - w_557 w_767) 12) ( <= ( - w_557 w_767) ( ~ 11)))
( or  ( not v_557_8 ) ( not v_767_2 ) ( >= ( - w_557 w_767) 11) ( <= ( - w_557 w_767) ( ~ 12)))
( or  ( not v_557_8 ) ( not v_767_8 ) ( >= ( - w_557 w_767) 11) ( <= ( - w_557 w_767) ( ~ 11)))
( or  ( not v_557_2 ) ( not v_768_2 ) ( >= ( - w_557 w_768) 23) ( <= ( - w_557 w_768) ( ~ 23)))
( or  ( not v_557_2 ) ( not v_768_8 ) ( >= ( - w_557 w_768) 24) ( <= ( - w_557 w_768) ( ~ 23)))
( or  ( not v_557_8 ) ( not v_768_2 ) ( >= ( - w_557 w_768) 23) ( <= ( - w_557 w_768) ( ~ 24)))
( or  ( not v_557_8 ) ( not v_768_8 ) ( >= ( - w_557 w_768) 23) ( <= ( - w_557 w_768) ( ~ 23)))
( or  ( not v_557_2 ) ( not v_785_2 ) ( >= ( - w_557 w_785) 4) ( <= ( - w_557 w_785) ( ~ 4)))
( or  ( not v_557_2 ) ( not v_785_8 ) ( >= ( - w_557 w_785) 4) ( <= ( - w_557 w_785) ( ~ 3)))
( or  ( not v_557_8 ) ( not v_785_2 ) ( >= ( - w_557 w_785) 3) ( <= ( - w_557 w_785) ( ~ 4)))
( or  ( not v_557_8 ) ( not v_785_8 ) ( >= ( - w_557 w_785) 4) ( <= ( - w_557 w_785) ( ~ 4)))
( or  ( not v_557_2 ) ( not v_786_2 ) ( >= ( - w_557 w_786) 9) ( <= ( - w_557 w_786) ( ~ 9)))
( or  ( not v_557_2 ) ( not v_786_8 ) ( >= ( - w_557 w_786) 10) ( <= ( - w_557 w_786) ( ~ 9)))
( or  ( not v_557_8 ) ( not v_786_2 ) ( >= ( - w_557 w_786) 9) ( <= ( - w_557 w_786) ( ~ 10)))
( or  ( not v_557_8 ) ( not v_786_8 ) ( >= ( - w_557 w_786) 9) ( <= ( - w_557 w_786) ( ~ 9)))
( or  ( not v_558_2 ) ( not v_593_2 ) ( >= ( - w_558 w_593) 24) ( <= ( - w_558 w_593) ( ~ 24)))
( or  ( not v_558_2 ) ( not v_593_8 ) ( >= ( - w_558 w_593) 24) ( <= ( - w_558 w_593) ( ~ 24)))
( or  ( not v_558_8 ) ( not v_593_2 ) ( >= ( - w_558 w_593) 24) ( <= ( - w_558 w_593) ( ~ 24)))
( or  ( not v_558_8 ) ( not v_593_8 ) ( >= ( - w_558 w_593) 24) ( <= ( - w_558 w_593) ( ~ 24)))
( or  ( not v_558_2 ) ( not v_594_2 ) ( >= ( - w_558 w_594) 34) ( <= ( - w_558 w_594) ( ~ 34)))
( or  ( not v_558_2 ) ( not v_594_8 ) ( >= ( - w_558 w_594) 35) ( <= ( - w_558 w_594) ( ~ 34)))
( or  ( not v_558_8 ) ( not v_594_2 ) ( >= ( - w_558 w_594) 34) ( <= ( - w_558 w_594) ( ~ 35)))
( or  ( not v_558_8 ) ( not v_594_8 ) ( >= ( - w_558 w_594) 34) ( <= ( - w_558 w_594) ( ~ 34)))
( or  ( not v_558_2 ) ( not v_597_2 ) ( >= ( - w_558 w_597) 16) ( <= ( - w_558 w_597) ( ~ 16)))
( or  ( not v_558_2 ) ( not v_597_8 ) ( >= ( - w_558 w_597) 17) ( <= ( - w_558 w_597) ( ~ 16)))
( or  ( not v_558_8 ) ( not v_597_2 ) ( >= ( - w_558 w_597) 16) ( <= ( - w_558 w_597) ( ~ 17)))
( or  ( not v_558_8 ) ( not v_597_8 ) ( >= ( - w_558 w_597) 16) ( <= ( - w_558 w_597) ( ~ 16)))
( or  ( not v_558_2 ) ( not v_598_2 ) ( >= ( - w_558 w_598) 4) ( <= ( - w_558 w_598) ( ~ 4)))
( or  ( not v_558_2 ) ( not v_598_8 ) ( >= ( - w_558 w_598) 4) ( <= ( - w_558 w_598) ( ~ 3)))
( or  ( not v_558_8 ) ( not v_598_2 ) ( >= ( - w_558 w_598) 3) ( <= ( - w_558 w_598) ( ~ 4)))
( or  ( not v_558_8 ) ( not v_598_8 ) ( >= ( - w_558 w_598) 4) ( <= ( - w_558 w_598) ( ~ 4)))
( or  ( not v_558_2 ) ( not v_599_2 ) ( >= ( - w_558 w_599) 18) ( <= ( - w_558 w_599) ( ~ 18)))
( or  ( not v_558_2 ) ( not v_599_8 ) ( >= ( - w_558 w_599) 18) ( <= ( - w_558 w_599) ( ~ 17)))
( or  ( not v_558_8 ) ( not v_599_2 ) ( >= ( - w_558 w_599) 17) ( <= ( - w_558 w_599) ( ~ 18)))
( or  ( not v_558_8 ) ( not v_599_8 ) ( >= ( - w_558 w_599) 18) ( <= ( - w_558 w_599) ( ~ 18)))
( or  ( not v_558_2 ) ( not v_600_2 ) ( >= ( - w_558 w_600) 5) ( <= ( - w_558 w_600) ( ~ 5)))
( or  ( not v_558_2 ) ( not v_600_8 ) ( >= ( - w_558 w_600) 6) ( <= ( - w_558 w_600) ( ~ 5)))
( or  ( not v_558_8 ) ( not v_600_2 ) ( >= ( - w_558 w_600) 5) ( <= ( - w_558 w_600) ( ~ 6)))
( or  ( not v_558_8 ) ( not v_600_8 ) ( >= ( - w_558 w_600) 5) ( <= ( - w_558 w_600) ( ~ 5)))
( or  ( not v_558_2 ) ( not v_613_2 ) ( >= ( - w_558 w_613) 16) ( <= ( - w_558 w_613) ( ~ 16)))
( or  ( not v_558_2 ) ( not v_613_8 ) ( >= ( - w_558 w_613) 17) ( <= ( - w_558 w_613) ( ~ 16)))
( or  ( not v_558_8 ) ( not v_613_2 ) ( >= ( - w_558 w_613) 16) ( <= ( - w_558 w_613) ( ~ 17)))
( or  ( not v_558_8 ) ( not v_613_8 ) ( >= ( - w_558 w_613) 16) ( <= ( - w_558 w_613) ( ~ 16)))
( or  ( not v_558_2 ) ( not v_614_2 ) ( >= ( - w_558 w_614) 4) ( <= ( - w_558 w_614) ( ~ 4)))
( or  ( not v_558_2 ) ( not v_614_8 ) ( >= ( - w_558 w_614) 4) ( <= ( - w_558 w_614) ( ~ 3)))
( or  ( not v_558_8 ) ( not v_614_2 ) ( >= ( - w_558 w_614) 3) ( <= ( - w_558 w_614) ( ~ 4)))
( or  ( not v_558_8 ) ( not v_614_8 ) ( >= ( - w_558 w_614) 4) ( <= ( - w_558 w_614) ( ~ 4)))
( or  ( not v_558_2 ) ( not v_665_2 ) ( >= ( - w_558 w_665) 31) ( <= ( - w_558 w_665) ( ~ 31)))
( or  ( not v_558_2 ) ( not v_665_8 ) ( >= ( - w_558 w_665) 31) ( <= ( - w_558 w_665) ( ~ 30)))
( or  ( not v_558_8 ) ( not v_665_2 ) ( >= ( - w_558 w_665) 30) ( <= ( - w_558 w_665) ( ~ 31)))
( or  ( not v_558_8 ) ( not v_665_8 ) ( >= ( - w_558 w_665) 31) ( <= ( - w_558 w_665) ( ~ 31)))
( or  ( not v_558_2 ) ( not v_666_2 ) ( >= ( - w_558 w_666) 20) ( <= ( - w_558 w_666) ( ~ 20)))
( or  ( not v_558_2 ) ( not v_666_8 ) ( >= ( - w_558 w_666) 20) ( <= ( - w_558 w_666) ( ~ 20)))
( or  ( not v_558_8 ) ( not v_666_2 ) ( >= ( - w_558 w_666) 20) ( <= ( - w_558 w_666) ( ~ 20)))
( or  ( not v_558_8 ) ( not v_666_8 ) ( >= ( - w_558 w_666) 20) ( <= ( - w_558 w_666) ( ~ 20)))
( or  ( not v_558_2 ) ( not v_767_2 ) ( >= ( - w_558 w_767) 23) ( <= ( - w_558 w_767) ( ~ 23)))
( or  ( not v_558_2 ) ( not v_767_8 ) ( >= ( - w_558 w_767) 24) ( <= ( - w_558 w_767) ( ~ 23)))
( or  ( not v_558_8 ) ( not v_767_2 ) ( >= ( - w_558 w_767) 23) ( <= ( - w_558 w_767) ( ~ 24)))
( or  ( not v_558_8 ) ( not v_767_8 ) ( >= ( - w_558 w_767) 23) ( <= ( - w_558 w_767) ( ~ 23)))
( or  ( not v_558_2 ) ( not v_768_2 ) ( >= ( - w_558 w_768) 34) ( <= ( - w_558 w_768) ( ~ 34)))
( or  ( not v_558_2 ) ( not v_768_8 ) ( >= ( - w_558 w_768) 34) ( <= ( - w_558 w_768) ( ~ 33)))
( or  ( not v_558_8 ) ( not v_768_2 ) ( >= ( - w_558 w_768) 33) ( <= ( - w_558 w_768) ( ~ 34)))
( or  ( not v_558_8 ) ( not v_768_8 ) ( >= ( - w_558 w_768) 34) ( <= ( - w_558 w_768) ( ~ 34)))
( or  ( not v_558_2 ) ( not v_785_2 ) ( >= ( - w_558 w_785) 16) ( <= ( - w_558 w_785) ( ~ 16)))
( or  ( not v_558_2 ) ( not v_785_8 ) ( >= ( - w_558 w_785) 17) ( <= ( - w_558 w_785) ( ~ 16)))
( or  ( not v_558_8 ) ( not v_785_2 ) ( >= ( - w_558 w_785) 16) ( <= ( - w_558 w_785) ( ~ 17)))
( or  ( not v_558_8 ) ( not v_785_8 ) ( >= ( - w_558 w_785) 16) ( <= ( - w_558 w_785) ( ~ 16)))
( or  ( not v_558_2 ) ( not v_786_2 ) ( >= ( - w_558 w_786) 4) ( <= ( - w_558 w_786) ( ~ 4)))
( or  ( not v_558_2 ) ( not v_786_8 ) ( >= ( - w_558 w_786) 4) ( <= ( - w_558 w_786) ( ~ 3)))
( or  ( not v_558_8 ) ( not v_786_2 ) ( >= ( - w_558 w_786) 3) ( <= ( - w_558 w_786) ( ~ 4)))
( or  ( not v_558_8 ) ( not v_786_8 ) ( >= ( - w_558 w_786) 4) ( <= ( - w_558 w_786) ( ~ 4)))
( or  ( not v_593_2 ) ( not v_594_2 ) ( = ( - w_593 w_594) 17) ( = ( - w_594 w_593) 17))
( or  ( not v_593_2 ) ( not v_594_8 ))
( or  ( not v_593_8 ) ( not v_594_2 ))
( or  ( not v_593_8 ) ( not v_594_8 ) ( = ( - w_593 w_594) 17) ( = ( - w_594 w_593) 17))
( or  ( not v_593_2 ) ( not v_597_2 ) ( >= ( - w_593 w_597) 8) ( <= ( - w_593 w_597) ( ~ 8)))
( or  ( not v_593_2 ) ( not v_597_8 ) ( >= ( - w_593 w_597) 9) ( <= ( - w_593 w_597) ( ~ 8)))
( or  ( not v_593_8 ) ( not v_597_2 ) ( >= ( - w_593 w_597) 8) ( <= ( - w_593 w_597) ( ~ 9)))
( or  ( not v_593_8 ) ( not v_597_8 ) ( >= ( - w_593 w_597) 8) ( <= ( - w_593 w_597) ( ~ 8)))
( or  ( not v_593_2 ) ( not v_598_2 ) ( >= ( - w_593 w_598) 21) ( <= ( - w_593 w_598) ( ~ 21)))
( or  ( not v_593_2 ) ( not v_598_8 ) ( >= ( - w_593 w_598) 21) ( <= ( - w_593 w_598) ( ~ 20)))
( or  ( not v_593_8 ) ( not v_598_2 ) ( >= ( - w_593 w_598) 20) ( <= ( - w_593 w_598) ( ~ 21)))
( or  ( not v_593_8 ) ( not v_598_8 ) ( >= ( - w_593 w_598) 21) ( <= ( - w_593 w_598) ( ~ 21)))
( or  ( not v_593_2 ) ( not v_613_2 ) ( >= ( - w_593 w_613) 8) ( <= ( - w_593 w_613) ( ~ 8)))
( or  ( not v_593_2 ) ( not v_613_8 ) ( >= ( - w_593 w_613) 9) ( <= ( - w_593 w_613) ( ~ 8)))
( or  ( not v_593_8 ) ( not v_613_2 ) ( >= ( - w_593 w_613) 8) ( <= ( - w_593 w_613) ( ~ 9)))
( or  ( not v_593_8 ) ( not v_613_8 ) ( >= ( - w_593 w_613) 8) ( <= ( - w_593 w_613) ( ~ 8)))
( or  ( not v_593_2 ) ( not v_614_2 ) ( >= ( - w_593 w_614) 21) ( <= ( - w_593 w_614) ( ~ 21)))
( or  ( not v_593_2 ) ( not v_614_8 ) ( >= ( - w_593 w_614) 21) ( <= ( - w_593 w_614) ( ~ 20)))
( or  ( not v_593_8 ) ( not v_614_2 ) ( >= ( - w_593 w_614) 20) ( <= ( - w_593 w_614) ( ~ 21)))
( or  ( not v_593_8 ) ( not v_614_8 ) ( >= ( - w_593 w_614) 21) ( <= ( - w_593 w_614) ( ~ 21)))
( or  ( not v_593_2 ) ( not v_631_2 ) ( >= ( - w_593 w_631) 19) ( <= ( - w_593 w_631) ( ~ 19)))
( or  ( not v_593_2 ) ( not v_631_8 ) ( >= ( - w_593 w_631) 20) ( <= ( - w_593 w_631) ( ~ 19)))
( or  ( not v_593_8 ) ( not v_631_2 ) ( >= ( - w_593 w_631) 19) ( <= ( - w_593 w_631) ( ~ 20)))
( or  ( not v_593_8 ) ( not v_631_8 ) ( >= ( - w_593 w_631) 19) ( <= ( - w_593 w_631) ( ~ 19)))
( or  ( not v_593_2 ) ( not v_632_2 ) ( >= ( - w_593 w_632) 7) ( <= ( - w_593 w_632) ( ~ 7)))
( or  ( not v_593_2 ) ( not v_632_8 ) ( >= ( - w_593 w_632) 7) ( <= ( - w_593 w_632) ( ~ 6)))
( or  ( not v_593_8 ) ( not v_632_2 ) ( >= ( - w_593 w_632) 6) ( <= ( - w_593 w_632) ( ~ 7)))
( or  ( not v_593_8 ) ( not v_632_8 ) ( >= ( - w_593 w_632) 7) ( <= ( - w_593 w_632) ( ~ 7)))
( or  ( not v_593_2 ) ( not v_665_2 ) ( >= ( - w_593 w_665) 8) ( <= ( - w_593 w_665) ( ~ 8)))
( or  ( not v_593_2 ) ( not v_665_8 ) ( >= ( - w_593 w_665) 9) ( <= ( - w_593 w_665) ( ~ 8)))
( or  ( not v_593_8 ) ( not v_665_2 ) ( >= ( - w_593 w_665) 8) ( <= ( - w_593 w_665) ( ~ 9)))
( or  ( not v_593_8 ) ( not v_665_8 ) ( >= ( - w_593 w_665) 8) ( <= ( - w_593 w_665) ( ~ 8)))
( or  ( not v_593_2 ) ( not v_666_2 ) ( >= ( - w_593 w_666) 5) ( <= ( - w_593 w_666) ( ~ 5)))
( or  ( not v_593_2 ) ( not v_666_8 ) ( >= ( - w_593 w_666) 6) ( <= ( - w_593 w_666) ( ~ 5)))
( or  ( not v_593_8 ) ( not v_666_2 ) ( >= ( - w_593 w_666) 5) ( <= ( - w_593 w_666) ( ~ 6)))
( or  ( not v_593_8 ) ( not v_666_8 ) ( >= ( - w_593 w_666) 5) ( <= ( - w_593 w_666) ( ~ 5)))
( or  ( not v_593_2 ) ( not v_767_2 ) ( >= ( - w_593 w_767) 1) ( <= ( - w_593 w_767) ( ~ 1)))
( or  ( not v_593_2 ) ( not v_767_8 ) ( >= ( - w_593 w_767) 2) ( <= ( - w_593 w_767) ( ~ 1)))
( or  ( not v_593_8 ) ( not v_767_2 ) ( >= ( - w_593 w_767) 1) ( <= ( - w_593 w_767) ( ~ 2)))
( or  ( not v_593_8 ) ( not v_767_8 ) ( >= ( - w_593 w_767) 1) ( <= ( - w_593 w_767) ( ~ 1)))
( or  ( not v_593_2 ) ( not v_768_2 ) ( >= ( - w_593 w_768) 11) ( <= ( - w_593 w_768) ( ~ 11)))
( or  ( not v_593_2 ) ( not v_768_8 ) ( >= ( - w_593 w_768) 12) ( <= ( - w_593 w_768) ( ~ 11)))
( or  ( not v_593_8 ) ( not v_768_2 ) ( >= ( - w_593 w_768) 11) ( <= ( - w_593 w_768) ( ~ 12)))
( or  ( not v_593_8 ) ( not v_768_8 ) ( >= ( - w_593 w_768) 11) ( <= ( - w_593 w_768) ( ~ 11)))
( or  ( not v_593_2 ) ( not v_785_2 ) ( >= ( - w_593 w_785) 8) ( <= ( - w_593 w_785) ( ~ 8)))
( or  ( not v_593_2 ) ( not v_785_8 ) ( >= ( - w_593 w_785) 9) ( <= ( - w_593 w_785) ( ~ 8)))
( or  ( not v_593_8 ) ( not v_785_2 ) ( >= ( - w_593 w_785) 8) ( <= ( - w_593 w_785) ( ~ 9)))
( or  ( not v_593_8 ) ( not v_785_8 ) ( >= ( - w_593 w_785) 8) ( <= ( - w_593 w_785) ( ~ 8)))
( or  ( not v_593_2 ) ( not v_786_2 ) ( >= ( - w_593 w_786) 20) ( <= ( - w_593 w_786) ( ~ 20)))
( or  ( not v_593_2 ) ( not v_786_8 ) ( >= ( - w_593 w_786) 21) ( <= ( - w_593 w_786) ( ~ 20)))
( or  ( not v_593_8 ) ( not v_786_2 ) ( >= ( - w_593 w_786) 20) ( <= ( - w_593 w_786) ( ~ 21)))
( or  ( not v_593_8 ) ( not v_786_8 ) ( >= ( - w_593 w_786) 20) ( <= ( - w_593 w_786) ( ~ 20)))
( or  ( not v_594_2 ) ( not v_597_2 ) ( >= ( - w_594 w_597) 21) ( <= ( - w_594 w_597) ( ~ 21)))
( or  ( not v_594_2 ) ( not v_597_8 ) ( >= ( - w_594 w_597) 21) ( <= ( - w_594 w_597) ( ~ 20)))
( or  ( not v_594_8 ) ( not v_597_2 ) ( >= ( - w_594 w_597) 20) ( <= ( - w_594 w_597) ( ~ 21)))
( or  ( not v_594_8 ) ( not v_597_8 ) ( >= ( - w_594 w_597) 21) ( <= ( - w_594 w_597) ( ~ 21)))
( or  ( not v_594_2 ) ( not v_598_2 ) ( >= ( - w_594 w_598) 31) ( <= ( - w_594 w_598) ( ~ 31)))
( or  ( not v_594_2 ) ( not v_598_8 ) ( >= ( - w_594 w_598) 31) ( <= ( - w_594 w_598) ( ~ 30)))
( or  ( not v_594_8 ) ( not v_598_2 ) ( >= ( - w_594 w_598) 30) ( <= ( - w_594 w_598) ( ~ 31)))
( or  ( not v_594_8 ) ( not v_598_8 ) ( >= ( - w_594 w_598) 31) ( <= ( - w_594 w_598) ( ~ 31)))
( or  ( not v_594_2 ) ( not v_613_2 ) ( >= ( - w_594 w_613) 21) ( <= ( - w_594 w_613) ( ~ 21)))
( or  ( not v_594_2 ) ( not v_613_8 ) ( >= ( - w_594 w_613) 21) ( <= ( - w_594 w_613) ( ~ 20)))
( or  ( not v_594_8 ) ( not v_613_2 ) ( >= ( - w_594 w_613) 20) ( <= ( - w_594 w_613) ( ~ 21)))
( or  ( not v_594_8 ) ( not v_613_8 ) ( >= ( - w_594 w_613) 21) ( <= ( - w_594 w_613) ( ~ 21)))
( or  ( not v_594_2 ) ( not v_614_2 ) ( >= ( - w_594 w_614) 31) ( <= ( - w_594 w_614) ( ~ 31)))
( or  ( not v_594_2 ) ( not v_614_8 ) ( >= ( - w_594 w_614) 31) ( <= ( - w_594 w_614) ( ~ 30)))
( or  ( not v_594_8 ) ( not v_614_2 ) ( >= ( - w_594 w_614) 30) ( <= ( - w_594 w_614) ( ~ 31)))
( or  ( not v_594_8 ) ( not v_614_8 ) ( >= ( - w_594 w_614) 31) ( <= ( - w_594 w_614) ( ~ 31)))
( or  ( not v_594_2 ) ( not v_631_2 ) ( >= ( - w_594 w_631) 29) ( <= ( - w_594 w_631) ( ~ 29)))
( or  ( not v_594_2 ) ( not v_631_8 ) ( >= ( - w_594 w_631) 30) ( <= ( - w_594 w_631) ( ~ 29)))
( or  ( not v_594_8 ) ( not v_631_2 ) ( >= ( - w_594 w_631) 29) ( <= ( - w_594 w_631) ( ~ 30)))
( or  ( not v_594_8 ) ( not v_631_8 ) ( >= ( - w_594 w_631) 29) ( <= ( - w_594 w_631) ( ~ 29)))
( or  ( not v_594_2 ) ( not v_632_2 ) ( >= ( - w_594 w_632) 19) ( <= ( - w_594 w_632) ( ~ 19)))
( or  ( not v_594_2 ) ( not v_632_8 ) ( >= ( - w_594 w_632) 20) ( <= ( - w_594 w_632) ( ~ 19)))
( or  ( not v_594_8 ) ( not v_632_2 ) ( >= ( - w_594 w_632) 19) ( <= ( - w_594 w_632) ( ~ 20)))
( or  ( not v_594_8 ) ( not v_632_8 ) ( >= ( - w_594 w_632) 19) ( <= ( - w_594 w_632) ( ~ 19)))
( or  ( not v_594_2 ) ( not v_665_2 ) ( >= ( - w_594 w_665) 5) ( <= ( - w_594 w_665) ( ~ 5)))
( or  ( not v_594_2 ) ( not v_665_8 ) ( >= ( - w_594 w_665) 6) ( <= ( - w_594 w_665) ( ~ 5)))
( or  ( not v_594_8 ) ( not v_665_2 ) ( >= ( - w_594 w_665) 5) ( <= ( - w_594 w_665) ( ~ 6)))
( or  ( not v_594_8 ) ( not v_665_8 ) ( >= ( - w_594 w_665) 5) ( <= ( - w_594 w_665) ( ~ 5)))
( or  ( not v_594_2 ) ( not v_666_2 ) ( >= ( - w_594 w_666) 18) ( <= ( - w_594 w_666) ( ~ 18)))
( or  ( not v_594_2 ) ( not v_666_8 ) ( >= ( - w_594 w_666) 18) ( <= ( - w_594 w_666) ( ~ 17)))
( or  ( not v_594_8 ) ( not v_666_2 ) ( >= ( - w_594 w_666) 17) ( <= ( - w_594 w_666) ( ~ 18)))
( or  ( not v_594_8 ) ( not v_666_8 ) ( >= ( - w_594 w_666) 18) ( <= ( - w_594 w_666) ( ~ 18)))
( or  ( not v_594_2 ) ( not v_767_2 ) ( >= ( - w_594 w_767) 13) ( <= ( - w_594 w_767) ( ~ 13)))
( or  ( not v_594_2 ) ( not v_767_8 ) ( >= ( - w_594 w_767) 13) ( <= ( - w_594 w_767) ( ~ 12)))
( or  ( not v_594_8 ) ( not v_767_2 ) ( >= ( - w_594 w_767) 12) ( <= ( - w_594 w_767) ( ~ 13)))
( or  ( not v_594_8 ) ( not v_767_8 ) ( >= ( - w_594 w_767) 13) ( <= ( - w_594 w_767) ( ~ 13)))
( or  ( not v_594_2 ) ( not v_768_2 ) ( >= ( - w_594 w_768) 1) ( <= ( - w_594 w_768) ( ~ 1)))
( or  ( not v_594_2 ) ( not v_768_8 ) ( >= ( - w_594 w_768) 2) ( <= ( - w_594 w_768) ( ~ 1)))
( or  ( not v_594_8 ) ( not v_768_2 ) ( >= ( - w_594 w_768) 1) ( <= ( - w_594 w_768) ( ~ 2)))
( or  ( not v_594_8 ) ( not v_768_8 ) ( >= ( - w_594 w_768) 1) ( <= ( - w_594 w_768) ( ~ 1)))
( or  ( not v_594_2 ) ( not v_785_2 ) ( >= ( - w_594 w_785) 21) ( <= ( - w_594 w_785) ( ~ 21)))
( or  ( not v_594_2 ) ( not v_785_8 ) ( >= ( - w_594 w_785) 21) ( <= ( - w_594 w_785) ( ~ 20)))
( or  ( not v_594_8 ) ( not v_785_2 ) ( >= ( - w_594 w_785) 20) ( <= ( - w_594 w_785) ( ~ 21)))
( or  ( not v_594_8 ) ( not v_785_8 ) ( >= ( - w_594 w_785) 21) ( <= ( - w_594 w_785) ( ~ 21)))
( or  ( not v_594_2 ) ( not v_786_2 ) ( >= ( - w_594 w_786) 31) ( <= ( - w_594 w_786) ( ~ 31)))
( or  ( not v_594_2 ) ( not v_786_8 ) ( >= ( - w_594 w_786) 31) ( <= ( - w_594 w_786) ( ~ 30)))
( or  ( not v_594_8 ) ( not v_786_2 ) ( >= ( - w_594 w_786) 30) ( <= ( - w_594 w_786) ( ~ 31)))
( or  ( not v_594_8 ) ( not v_786_8 ) ( >= ( - w_594 w_786) 31) ( <= ( - w_594 w_786) ( ~ 31)))
( or  ( not v_597_2 ) ( not v_598_2 ) ( = ( - w_597 w_598) 17) ( = ( - w_598 w_597) 17))
( or  ( not v_597_2 ) ( not v_598_8 ))
( or  ( not v_597_8 ) ( not v_598_2 ))
( or  ( not v_597_8 ) ( not v_598_8 ) ( = ( - w_597 w_598) 17) ( = ( - w_598 w_597) 17))
( or  ( not v_597_2 ) ( not v_613_2 ) ( >= ( - w_597 w_613) 1) ( <= ( - w_597 w_613) ( ~ 1)))
( or  ( not v_597_2 ) ( not v_613_8 ) ( >= ( - w_597 w_613) 1) ( <= ( - w_597 w_613) 0))
( or  ( not v_597_8 ) ( not v_613_2 ) ( >= ( - w_597 w_613) 0) ( <= ( - w_597 w_613) ( ~ 1)))
( or  ( not v_597_8 ) ( not v_613_8 ) ( >= ( - w_597 w_613) 1) ( <= ( - w_597 w_613) ( ~ 1)))
( or  ( not v_597_2 ) ( not v_614_2 ) ( >= ( - w_597 w_614) 13) ( <= ( - w_597 w_614) ( ~ 13)))
( or  ( not v_597_2 ) ( not v_614_8 ) ( >= ( - w_597 w_614) 14) ( <= ( - w_597 w_614) ( ~ 13)))
( or  ( not v_597_8 ) ( not v_614_2 ) ( >= ( - w_597 w_614) 13) ( <= ( - w_597 w_614) ( ~ 14)))
( or  ( not v_597_8 ) ( not v_614_8 ) ( >= ( - w_597 w_614) 13) ( <= ( - w_597 w_614) ( ~ 13)))
( or  ( not v_597_2 ) ( not v_665_2 ) ( >= ( - w_597 w_665) 16) ( <= ( - w_597 w_665) ( ~ 16)))
( or  ( not v_597_2 ) ( not v_665_8 ) ( >= ( - w_597 w_665) 16) ( <= ( - w_597 w_665) ( ~ 16)))
( or  ( not v_597_8 ) ( not v_665_2 ) ( >= ( - w_597 w_665) 16) ( <= ( - w_597 w_665) ( ~ 16)))
( or  ( not v_597_8 ) ( not v_665_8 ) ( >= ( - w_597 w_665) 16) ( <= ( - w_597 w_665) ( ~ 16)))
( or  ( not v_597_2 ) ( not v_666_2 ) ( >= ( - w_597 w_666) 4) ( <= ( - w_597 w_666) ( ~ 4)))
( or  ( not v_597_2 ) ( not v_666_8 ) ( >= ( - w_597 w_666) 4) ( <= ( - w_597 w_666) ( ~ 3)))
( or  ( not v_597_8 ) ( not v_666_2 ) ( >= ( - w_597 w_666) 3) ( <= ( - w_597 w_666) ( ~ 4)))
( or  ( not v_597_8 ) ( not v_666_8 ) ( >= ( - w_597 w_666) 4) ( <= ( - w_597 w_666) ( ~ 4)))
( or  ( not v_597_2 ) ( not v_767_2 ) ( >= ( - w_597 w_767) 8) ( <= ( - w_597 w_767) ( ~ 8)))
( or  ( not v_597_2 ) ( not v_767_8 ) ( >= ( - w_597 w_767) 8) ( <= ( - w_597 w_767) ( ~ 7)))
( or  ( not v_597_8 ) ( not v_767_2 ) ( >= ( - w_597 w_767) 7) ( <= ( - w_597 w_767) ( ~ 8)))
( or  ( not v_597_8 ) ( not v_767_8 ) ( >= ( - w_597 w_767) 8) ( <= ( - w_597 w_767) ( ~ 8)))
( or  ( not v_597_2 ) ( not v_768_2 ) ( >= ( - w_597 w_768) 19) ( <= ( - w_597 w_768) ( ~ 19)))
( or  ( not v_597_2 ) ( not v_768_8 ) ( >= ( - w_597 w_768) 19) ( <= ( - w_597 w_768) ( ~ 19)))
( or  ( not v_597_8 ) ( not v_768_2 ) ( >= ( - w_597 w_768) 19) ( <= ( - w_597 w_768) ( ~ 19)))
( or  ( not v_597_8 ) ( not v_768_8 ) ( >= ( - w_597 w_768) 19) ( <= ( - w_597 w_768) ( ~ 19)))
( or  ( not v_597_2 ) ( not v_785_2 ) ( >= ( - w_597 w_785) 1) ( <= ( - w_597 w_785) ( ~ 1)))
( or  ( not v_597_2 ) ( not v_785_8 ) ( >= ( - w_597 w_785) 1) ( <= ( - w_597 w_785) 0))
( or  ( not v_597_8 ) ( not v_785_2 ) ( >= ( - w_597 w_785) 0) ( <= ( - w_597 w_785) ( ~ 1)))
( or  ( not v_597_8 ) ( not v_785_8 ) ( >= ( - w_597 w_785) 1) ( <= ( - w_597 w_785) ( ~ 1)))
( or  ( not v_597_2 ) ( not v_786_2 ) ( >= ( - w_597 w_786) 13) ( <= ( - w_597 w_786) ( ~ 13)))
( or  ( not v_597_2 ) ( not v_786_8 ) ( >= ( - w_597 w_786) 13) ( <= ( - w_597 w_786) ( ~ 12)))
( or  ( not v_597_8 ) ( not v_786_2 ) ( >= ( - w_597 w_786) 12) ( <= ( - w_597 w_786) ( ~ 13)))
( or  ( not v_597_8 ) ( not v_786_8 ) ( >= ( - w_597 w_786) 13) ( <= ( - w_597 w_786) ( ~ 13)))
( or  ( not v_598_2 ) ( not v_613_2 ) ( >= ( - w_598 w_613) 13) ( <= ( - w_598 w_613) ( ~ 13)))
( or  ( not v_598_2 ) ( not v_613_8 ) ( >= ( - w_598 w_613) 14) ( <= ( - w_598 w_613) ( ~ 13)))
( or  ( not v_598_8 ) ( not v_613_2 ) ( >= ( - w_598 w_613) 13) ( <= ( - w_598 w_613) ( ~ 14)))
( or  ( not v_598_8 ) ( not v_613_8 ) ( >= ( - w_598 w_613) 13) ( <= ( - w_598 w_613) ( ~ 13)))
( or  ( not v_598_2 ) ( not v_614_2 ) ( >= ( - w_598 w_614) 1) ( <= ( - w_598 w_614) ( ~ 1)))
( or  ( not v_598_2 ) ( not v_614_8 ) ( >= ( - w_598 w_614) 1) ( <= ( - w_598 w_614) 0))
( or  ( not v_598_8 ) ( not v_614_2 ) ( >= ( - w_598 w_614) 0) ( <= ( - w_598 w_614) ( ~ 1)))
( or  ( not v_598_8 ) ( not v_614_8 ) ( >= ( - w_598 w_614) 1) ( <= ( - w_598 w_614) ( ~ 1)))
( or  ( not v_598_2 ) ( not v_665_2 ) ( >= ( - w_598 w_665) 26) ( <= ( - w_598 w_665) ( ~ 26)))
( or  ( not v_598_2 ) ( not v_665_8 ) ( >= ( - w_598 w_665) 27) ( <= ( - w_598 w_665) ( ~ 26)))
( or  ( not v_598_8 ) ( not v_665_2 ) ( >= ( - w_598 w_665) 26) ( <= ( - w_598 w_665) ( ~ 27)))
( or  ( not v_598_8 ) ( not v_665_8 ) ( >= ( - w_598 w_665) 26) ( <= ( - w_598 w_665) ( ~ 26)))
( or  ( not v_598_2 ) ( not v_666_2 ) ( >= ( - w_598 w_666) 16) ( <= ( - w_598 w_666) ( ~ 16)))
( or  ( not v_598_2 ) ( not v_666_8 ) ( >= ( - w_598 w_666) 16) ( <= ( - w_598 w_666) ( ~ 16)))
( or  ( not v_598_8 ) ( not v_666_2 ) ( >= ( - w_598 w_666) 16) ( <= ( - w_598 w_666) ( ~ 16)))
( or  ( not v_598_8 ) ( not v_666_8 ) ( >= ( - w_598 w_666) 16) ( <= ( - w_598 w_666) ( ~ 16)))
( or  ( not v_598_2 ) ( not v_768_2 ) ( >= ( - w_598 w_768) 30) ( <= ( - w_598 w_768) ( ~ 30)))
( or  ( not v_598_2 ) ( not v_768_8 ) ( >= ( - w_598 w_768) 31) ( <= ( - w_598 w_768) ( ~ 30)))
( or  ( not v_598_8 ) ( not v_768_2 ) ( >= ( - w_598 w_768) 30) ( <= ( - w_598 w_768) ( ~ 31)))
( or  ( not v_598_8 ) ( not v_768_8 ) ( >= ( - w_598 w_768) 30) ( <= ( - w_598 w_768) ( ~ 30)))
( or  ( not v_598_2 ) ( not v_785_2 ) ( >= ( - w_598 w_785) 13) ( <= ( - w_598 w_785) ( ~ 13)))
( or  ( not v_598_2 ) ( not v_785_8 ) ( >= ( - w_598 w_785) 14) ( <= ( - w_598 w_785) ( ~ 13)))
( or  ( not v_598_8 ) ( not v_785_2 ) ( >= ( - w_598 w_785) 13) ( <= ( - w_598 w_785) ( ~ 14)))
( or  ( not v_598_8 ) ( not v_785_8 ) ( >= ( - w_598 w_785) 13) ( <= ( - w_598 w_785) ( ~ 13)))
( or  ( not v_598_2 ) ( not v_786_2 ) ( >= ( - w_598 w_786) 1) ( <= ( - w_598 w_786) ( ~ 1)))
( or  ( not v_598_2 ) ( not v_786_8 ) ( >= ( - w_598 w_786) 1) ( <= ( - w_598 w_786) 0))
( or  ( not v_598_8 ) ( not v_786_2 ) ( >= ( - w_598 w_786) 0) ( <= ( - w_598 w_786) ( ~ 1)))
( or  ( not v_598_8 ) ( not v_786_8 ) ( >= ( - w_598 w_786) 1) ( <= ( - w_598 w_786) ( ~ 1)))
( or  ( not v_599_2 ) ( not v_600_2 ) ( = ( - w_599 w_600) 17) ( = ( - w_600 w_599) 17))
( or  ( not v_599_2 ) ( not v_600_8 ))
( or  ( not v_599_8 ) ( not v_600_2 ))
( or  ( not v_599_8 ) ( not v_600_8 ) ( = ( - w_599 w_600) 17) ( = ( - w_600 w_599) 17))
( or  ( not v_599_2 ) ( not v_665_2 ) ( >= ( - w_599 w_665) 15) ( <= ( - w_599 w_665) ( ~ 15)))
( or  ( not v_599_2 ) ( not v_665_8 ) ( >= ( - w_599 w_665) 15) ( <= ( - w_599 w_665) ( ~ 14)))
( or  ( not v_599_8 ) ( not v_665_2 ) ( >= ( - w_599 w_665) 14) ( <= ( - w_599 w_665) ( ~ 15)))
( or  ( not v_599_8 ) ( not v_665_8 ) ( >= ( - w_599 w_665) 15) ( <= ( - w_599 w_665) ( ~ 15)))
( or  ( not v_599_2 ) ( not v_666_2 ) ( >= ( - w_599 w_666) 2) ( <= ( - w_599 w_666) ( ~ 2)))
( or  ( not v_599_2 ) ( not v_666_8 ) ( >= ( - w_599 w_666) 3) ( <= ( - w_599 w_666) ( ~ 2)))
( or  ( not v_599_8 ) ( not v_666_2 ) ( >= ( - w_599 w_666) 2) ( <= ( - w_599 w_666) ( ~ 3)))
( or  ( not v_599_8 ) ( not v_666_8 ) ( >= ( - w_599 w_666) 2) ( <= ( - w_599 w_666) ( ~ 2)))
( or  ( not v_599_2 ) ( not v_767_2 ) ( >= ( - w_599 w_767) 7) ( <= ( - w_599 w_767) ( ~ 7)))
( or  ( not v_599_2 ) ( not v_767_8 ) ( >= ( - w_599 w_767) 7) ( <= ( - w_599 w_767) ( ~ 6)))
( or  ( not v_599_8 ) ( not v_767_2 ) ( >= ( - w_599 w_767) 6) ( <= ( - w_599 w_767) ( ~ 7)))
( or  ( not v_599_8 ) ( not v_767_8 ) ( >= ( - w_599 w_767) 7) ( <= ( - w_599 w_767) ( ~ 7)))
( or  ( not v_599_2 ) ( not v_768_2 ) ( >= ( - w_599 w_768) 19) ( <= ( - w_599 w_768) ( ~ 19)))
( or  ( not v_599_2 ) ( not v_768_8 ) ( >= ( - w_599 w_768) 19) ( <= ( - w_599 w_768) ( ~ 18)))
( or  ( not v_599_8 ) ( not v_768_2 ) ( >= ( - w_599 w_768) 18) ( <= ( - w_599 w_768) ( ~ 19)))
( or  ( not v_599_8 ) ( not v_768_8 ) ( >= ( - w_599 w_768) 19) ( <= ( - w_599 w_768) ( ~ 19)))
( or  ( not v_600_2 ) ( not v_665_2 ) ( >= ( - w_600 w_665) 25) ( <= ( - w_600 w_665) ( ~ 25)))
( or  ( not v_600_2 ) ( not v_665_8 ) ( >= ( - w_600 w_665) 25) ( <= ( - w_600 w_665) ( ~ 25)))
( or  ( not v_600_8 ) ( not v_665_2 ) ( >= ( - w_600 w_665) 25) ( <= ( - w_600 w_665) ( ~ 25)))
( or  ( not v_600_8 ) ( not v_665_8 ) ( >= ( - w_600 w_665) 25) ( <= ( - w_600 w_665) ( ~ 25)))
( or  ( not v_600_2 ) ( not v_666_2 ) ( >= ( - w_600 w_666) 15) ( <= ( - w_600 w_666) ( ~ 15)))
( or  ( not v_600_2 ) ( not v_666_8 ) ( >= ( - w_600 w_666) 15) ( <= ( - w_600 w_666) ( ~ 14)))
( or  ( not v_600_8 ) ( not v_666_2 ) ( >= ( - w_600 w_666) 14) ( <= ( - w_600 w_666) ( ~ 15)))
( or  ( not v_600_8 ) ( not v_666_8 ) ( >= ( - w_600 w_666) 15) ( <= ( - w_600 w_666) ( ~ 15)))
( or  ( not v_600_2 ) ( not v_767_2 ) ( >= ( - w_600 w_767) 19) ( <= ( - w_600 w_767) ( ~ 19)))
( or  ( not v_600_2 ) ( not v_767_8 ) ( >= ( - w_600 w_767) 19) ( <= ( - w_600 w_767) ( ~ 18)))
( or  ( not v_600_8 ) ( not v_767_2 ) ( >= ( - w_600 w_767) 18) ( <= ( - w_600 w_767) ( ~ 19)))
( or  ( not v_600_8 ) ( not v_767_8 ) ( >= ( - w_600 w_767) 19) ( <= ( - w_600 w_767) ( ~ 19)))
( or  ( not v_600_2 ) ( not v_768_2 ) ( >= ( - w_600 w_768) 29) ( <= ( - w_600 w_768) ( ~ 29)))
( or  ( not v_600_2 ) ( not v_768_8 ) ( >= ( - w_600 w_768) 30) ( <= ( - w_600 w_768) ( ~ 29)))
( or  ( not v_600_8 ) ( not v_768_2 ) ( >= ( - w_600 w_768) 29) ( <= ( - w_600 w_768) ( ~ 30)))
( or  ( not v_600_8 ) ( not v_768_8 ) ( >= ( - w_600 w_768) 29) ( <= ( - w_600 w_768) ( ~ 29)))
( or  ( not v_613_2 ) ( not v_614_2 ) ( = ( - w_613 w_614) 17) ( = ( - w_614 w_613) 17))
( or  ( not v_613_2 ) ( not v_614_8 ))
( or  ( not v_613_8 ) ( not v_614_2 ))
( or  ( not v_613_8 ) ( not v_614_8 ) ( = ( - w_613 w_614) 17) ( = ( - w_614 w_613) 17))
( or  ( not v_613_2 ) ( not v_665_2 ) ( >= ( - w_613 w_665) 16) ( <= ( - w_613 w_665) ( ~ 16)))
( or  ( not v_613_2 ) ( not v_665_8 ) ( >= ( - w_613 w_665) 16) ( <= ( - w_613 w_665) ( ~ 16)))
( or  ( not v_613_8 ) ( not v_665_2 ) ( >= ( - w_613 w_665) 16) ( <= ( - w_613 w_665) ( ~ 16)))
( or  ( not v_613_8 ) ( not v_665_8 ) ( >= ( - w_613 w_665) 16) ( <= ( - w_613 w_665) ( ~ 16)))
( or  ( not v_613_2 ) ( not v_666_2 ) ( >= ( - w_613 w_666) 3) ( <= ( - w_613 w_666) ( ~ 3)))
( or  ( not v_613_2 ) ( not v_666_8 ) ( >= ( - w_613 w_666) 4) ( <= ( - w_613 w_666) ( ~ 3)))
( or  ( not v_613_8 ) ( not v_666_2 ) ( >= ( - w_613 w_666) 3) ( <= ( - w_613 w_666) ( ~ 4)))
( or  ( not v_613_8 ) ( not v_666_8 ) ( >= ( - w_613 w_666) 3) ( <= ( - w_613 w_666) ( ~ 3)))
( or  ( not v_613_2 ) ( not v_765_2 ) ( >= ( - w_613 w_765) 4) ( <= ( - w_613 w_765) ( ~ 4)))
( or  ( not v_613_2 ) ( not v_765_8 ) ( >= ( - w_613 w_765) 4) ( <= ( - w_613 w_765) ( ~ 3)))
( or  ( not v_613_8 ) ( not v_765_2 ) ( >= ( - w_613 w_765) 3) ( <= ( - w_613 w_765) ( ~ 4)))
( or  ( not v_613_8 ) ( not v_765_8 ) ( >= ( - w_613 w_765) 4) ( <= ( - w_613 w_765) ( ~ 4)))
( or  ( not v_613_2 ) ( not v_766_2 ) ( >= ( - w_613 w_766) 16) ( <= ( - w_613 w_766) ( ~ 16)))
( or  ( not v_613_2 ) ( not v_766_8 ) ( >= ( - w_613 w_766) 17) ( <= ( - w_613 w_766) ( ~ 16)))
( or  ( not v_613_8 ) ( not v_766_2 ) ( >= ( - w_613 w_766) 16) ( <= ( - w_613 w_766) ( ~ 17)))
( or  ( not v_613_8 ) ( not v_766_8 ) ( >= ( - w_613 w_766) 16) ( <= ( - w_613 w_766) ( ~ 16)))
( or  ( not v_613_2 ) ( not v_768_2 ) ( >= ( - w_613 w_768) 19) ( <= ( - w_613 w_768) ( ~ 19)))
( or  ( not v_613_2 ) ( not v_768_8 ) ( >= ( - w_613 w_768) 19) ( <= ( - w_613 w_768) ( ~ 18)))
( or  ( not v_613_8 ) ( not v_768_2 ) ( >= ( - w_613 w_768) 18) ( <= ( - w_613 w_768) ( ~ 19)))
( or  ( not v_613_8 ) ( not v_768_8 ) ( >= ( - w_613 w_768) 19) ( <= ( - w_613 w_768) ( ~ 19)))
( or  ( not v_613_2 ) ( not v_785_2 ) ( >= ( - w_613 w_785) 2) ( <= ( - w_613 w_785) ( ~ 2)))
( or  ( not v_613_2 ) ( not v_785_8 ) ( >= ( - w_613 w_785) 3) ( <= ( - w_613 w_785) ( ~ 2)))
( or  ( not v_613_8 ) ( not v_785_2 ) ( >= ( - w_613 w_785) 2) ( <= ( - w_613 w_785) ( ~ 3)))
( or  ( not v_613_8 ) ( not v_785_8 ) ( >= ( - w_613 w_785) 2) ( <= ( - w_613 w_785) ( ~ 2)))
( or  ( not v_613_2 ) ( not v_786_2 ) ( >= ( - w_613 w_786) 13) ( <= ( - w_613 w_786) ( ~ 13)))
( or  ( not v_613_2 ) ( not v_786_8 ) ( >= ( - w_613 w_786) 13) ( <= ( - w_613 w_786) ( ~ 12)))
( or  ( not v_613_8 ) ( not v_786_2 ) ( >= ( - w_613 w_786) 12) ( <= ( - w_613 w_786) ( ~ 13)))
( or  ( not v_613_8 ) ( not v_786_8 ) ( >= ( - w_613 w_786) 13) ( <= ( - w_613 w_786) ( ~ 13)))
( or  ( not v_614_2 ) ( not v_665_2 ) ( >= ( - w_614 w_665) 26) ( <= ( - w_614 w_665) ( ~ 26)))
( or  ( not v_614_2 ) ( not v_665_8 ) ( >= ( - w_614 w_665) 27) ( <= ( - w_614 w_665) ( ~ 26)))
( or  ( not v_614_8 ) ( not v_665_2 ) ( >= ( - w_614 w_665) 26) ( <= ( - w_614 w_665) ( ~ 27)))
( or  ( not v_614_8 ) ( not v_665_8 ) ( >= ( - w_614 w_665) 26) ( <= ( - w_614 w_665) ( ~ 26)))
( or  ( not v_614_2 ) ( not v_666_2 ) ( >= ( - w_614 w_666) 16) ( <= ( - w_614 w_666) ( ~ 16)))
( or  ( not v_614_2 ) ( not v_666_8 ) ( >= ( - w_614 w_666) 16) ( <= ( - w_614 w_666) ( ~ 16)))
( or  ( not v_614_8 ) ( not v_666_2 ) ( >= ( - w_614 w_666) 16) ( <= ( - w_614 w_666) ( ~ 16)))
( or  ( not v_614_8 ) ( not v_666_8 ) ( >= ( - w_614 w_666) 16) ( <= ( - w_614 w_666) ( ~ 16)))
( or  ( not v_614_2 ) ( not v_765_2 ) ( >= ( - w_614 w_765) 9) ( <= ( - w_614 w_765) ( ~ 9)))
( or  ( not v_614_2 ) ( not v_765_8 ) ( >= ( - w_614 w_765) 10) ( <= ( - w_614 w_765) ( ~ 9)))
( or  ( not v_614_8 ) ( not v_765_2 ) ( >= ( - w_614 w_765) 9) ( <= ( - w_614 w_765) ( ~ 10)))
( or  ( not v_614_8 ) ( not v_765_8 ) ( >= ( - w_614 w_765) 9) ( <= ( - w_614 w_765) ( ~ 9)))
( or  ( not v_614_2 ) ( not v_766_2 ) ( >= ( - w_614 w_766) 4) ( <= ( - w_614 w_766) ( ~ 4)))
( or  ( not v_614_2 ) ( not v_766_8 ) ( >= ( - w_614 w_766) 4) ( <= ( - w_614 w_766) ( ~ 3)))
( or  ( not v_614_8 ) ( not v_766_2 ) ( >= ( - w_614 w_766) 3) ( <= ( - w_614 w_766) ( ~ 4)))
( or  ( not v_614_8 ) ( not v_766_8 ) ( >= ( - w_614 w_766) 4) ( <= ( - w_614 w_766) ( ~ 4)))
( or  ( not v_614_2 ) ( not v_767_2 ) ( >= ( - w_614 w_767) 19) ( <= ( - w_614 w_767) ( ~ 19)))
( or  ( not v_614_2 ) ( not v_767_8 ) ( >= ( - w_614 w_767) 19) ( <= ( - w_614 w_767) ( ~ 18)))
( or  ( not v_614_8 ) ( not v_767_2 ) ( >= ( - w_614 w_767) 18) ( <= ( - w_614 w_767) ( ~ 19)))
( or  ( not v_614_8 ) ( not v_767_8 ) ( >= ( - w_614 w_767) 19) ( <= ( - w_614 w_767) ( ~ 19)))
( or  ( not v_614_2 ) ( not v_768_2 ) ( >= ( - w_614 w_768) 30) ( <= ( - w_614 w_768) ( ~ 30)))
( or  ( not v_614_2 ) ( not v_768_8 ) ( >= ( - w_614 w_768) 31) ( <= ( - w_614 w_768) ( ~ 30)))
( or  ( not v_614_8 ) ( not v_768_2 ) ( >= ( - w_614 w_768) 30) ( <= ( - w_614 w_768) ( ~ 31)))
( or  ( not v_614_8 ) ( not v_768_8 ) ( >= ( - w_614 w_768) 30) ( <= ( - w_614 w_768) ( ~ 30)))
( or  ( not v_614_2 ) ( not v_785_2 ) ( >= ( - w_614 w_785) 13) ( <= ( - w_614 w_785) ( ~ 13)))
( or  ( not v_614_2 ) ( not v_785_8 ) ( >= ( - w_614 w_785) 14) ( <= ( - w_614 w_785) ( ~ 13)))
( or  ( not v_614_8 ) ( not v_785_2 ) ( >= ( - w_614 w_785) 13) ( <= ( - w_614 w_785) ( ~ 14)))
( or  ( not v_614_8 ) ( not v_785_8 ) ( >= ( - w_614 w_785) 13) ( <= ( - w_614 w_785) ( ~ 13)))
( or  ( not v_614_2 ) ( not v_786_2 ) ( >= ( - w_614 w_786) 2) ( <= ( - w_614 w_786) ( ~ 2)))
( or  ( not v_614_2 ) ( not v_786_8 ) ( >= ( - w_614 w_786) 3) ( <= ( - w_614 w_786) ( ~ 2)))
( or  ( not v_614_8 ) ( not v_786_2 ) ( >= ( - w_614 w_786) 2) ( <= ( - w_614 w_786) ( ~ 3)))
( or  ( not v_614_8 ) ( not v_786_8 ) ( >= ( - w_614 w_786) 2) ( <= ( - w_614 w_786) ( ~ 2)))
( or  ( not v_629_2 ) ( not v_630_2 ) ( = ( - w_629 w_630) 17) ( = ( - w_630 w_629) 17))
( or  ( not v_629_2 ) ( not v_630_8 ))
( or  ( not v_629_8 ) ( not v_630_2 ))
( or  ( not v_629_8 ) ( not v_630_8 ) ( = ( - w_629 w_630) 17) ( = ( - w_630 w_629) 17))
( or  ( not v_629_2 ) ( not v_631_2 ) ( >= ( - w_629 w_631) 19) ( <= ( - w_629 w_631) ( ~ 19)))
( or  ( not v_629_2 ) ( not v_631_8 ) ( >= ( - w_629 w_631) 20) ( <= ( - w_629 w_631) ( ~ 19)))
( or  ( not v_629_8 ) ( not v_631_2 ) ( >= ( - w_629 w_631) 19) ( <= ( - w_629 w_631) ( ~ 20)))
( or  ( not v_629_8 ) ( not v_631_8 ) ( >= ( - w_629 w_631) 19) ( <= ( - w_629 w_631) ( ~ 19)))
( or  ( not v_629_2 ) ( not v_632_2 ) ( >= ( - w_629 w_632) 9) ( <= ( - w_629 w_632) ( ~ 9)))
( or  ( not v_629_2 ) ( not v_632_8 ) ( >= ( - w_629 w_632) 10) ( <= ( - w_629 w_632) ( ~ 9)))
( or  ( not v_629_8 ) ( not v_632_2 ) ( >= ( - w_629 w_632) 9) ( <= ( - w_629 w_632) ( ~ 10)))
( or  ( not v_629_8 ) ( not v_632_8 ) ( >= ( - w_629 w_632) 9) ( <= ( - w_629 w_632) ( ~ 9)))
( or  ( not v_629_2 ) ( not v_768_2 ) ( >= ( - w_629 w_768) 10) ( <= ( - w_629 w_768) ( ~ 10)))
( or  ( not v_629_2 ) ( not v_768_8 ) ( >= ( - w_629 w_768) 10) ( <= ( - w_629 w_768) ( ~ 10)))
( or  ( not v_629_8 ) ( not v_768_2 ) ( >= ( - w_629 w_768) 10) ( <= ( - w_629 w_768) ( ~ 10)))
( or  ( not v_629_8 ) ( not v_768_8 ) ( >= ( - w_629 w_768) 10) ( <= ( - w_629 w_768) ( ~ 10)))
( or  ( not v_630_2 ) ( not v_631_2 ) ( >= ( - w_630 w_631) 32) ( <= ( - w_630 w_631) ( ~ 32)))
( or  ( not v_630_2 ) ( not v_631_8 ) ( >= ( - w_630 w_631) 32) ( <= ( - w_630 w_631) ( ~ 32)))
( or  ( not v_630_8 ) ( not v_631_2 ) ( >= ( - w_630 w_631) 32) ( <= ( - w_630 w_631) ( ~ 32)))
( or  ( not v_630_8 ) ( not v_631_8 ) ( >= ( - w_630 w_631) 32) ( <= ( - w_630 w_631) ( ~ 32)))
( or  ( not v_630_2 ) ( not v_632_2 ) ( >= ( - w_630 w_632) 19) ( <= ( - w_630 w_632) ( ~ 19)))
( or  ( not v_630_2 ) ( not v_632_8 ) ( >= ( - w_630 w_632) 20) ( <= ( - w_630 w_632) ( ~ 19)))
( or  ( not v_630_8 ) ( not v_632_2 ) ( >= ( - w_630 w_632) 19) ( <= ( - w_630 w_632) ( ~ 20)))
( or  ( not v_630_8 ) ( not v_632_8 ) ( >= ( - w_630 w_632) 19) ( <= ( - w_630 w_632) ( ~ 19)))
( or  ( not v_630_2 ) ( not v_768_2 ) ( >= ( - w_630 w_768) 3) ( <= ( - w_630 w_768) ( ~ 3)))
( or  ( not v_630_2 ) ( not v_768_8 ) ( >= ( - w_630 w_768) 3) ( <= ( - w_630 w_768) ( ~ 2)))
( or  ( not v_630_8 ) ( not v_768_2 ) ( >= ( - w_630 w_768) 2) ( <= ( - w_630 w_768) ( ~ 3)))
( or  ( not v_630_8 ) ( not v_768_8 ) ( >= ( - w_630 w_768) 3) ( <= ( - w_630 w_768) ( ~ 3)))
( or  ( not v_631_2 ) ( not v_632_2 ) ( = ( - w_631 w_632) 17) ( = ( - w_632 w_631) 17))
( or  ( not v_631_2 ) ( not v_632_8 ))
( or  ( not v_631_8 ) ( not v_632_2 ))
( or  ( not v_631_8 ) ( not v_632_8 ) ( = ( - w_631 w_632) 17) ( = ( - w_632 w_631) 17))
( or  ( not v_631_2 ) ( not v_767_2 ) ( >= ( - w_631 w_767) 18) ( <= ( - w_631 w_767) ( ~ 18)))
( or  ( not v_631_2 ) ( not v_767_8 ) ( >= ( - w_631 w_767) 18) ( <= ( - w_631 w_767) ( ~ 17)))
( or  ( not v_631_8 ) ( not v_767_2 ) ( >= ( - w_631 w_767) 17) ( <= ( - w_631 w_767) ( ~ 18)))
( or  ( not v_631_8 ) ( not v_767_8 ) ( >= ( - w_631 w_767) 18) ( <= ( - w_631 w_767) ( ~ 18)))
( or  ( not v_631_2 ) ( not v_768_2 ) ( >= ( - w_631 w_768) 29) ( <= ( - w_631 w_768) ( ~ 29)))
( or  ( not v_631_2 ) ( not v_768_8 ) ( >= ( - w_631 w_768) 29) ( <= ( - w_631 w_768) ( ~ 29)))
( or  ( not v_631_8 ) ( not v_768_2 ) ( >= ( - w_631 w_768) 29) ( <= ( - w_631 w_768) ( ~ 29)))
( or  ( not v_631_8 ) ( not v_768_8 ) ( >= ( - w_631 w_768) 29) ( <= ( - w_631 w_768) ( ~ 29)))
( or  ( not v_632_2 ) ( not v_767_2 ) ( >= ( - w_632 w_767) 6) ( <= ( - w_632 w_767) ( ~ 6)))
( or  ( not v_632_2 ) ( not v_767_8 ) ( >= ( - w_632 w_767) 7) ( <= ( - w_632 w_767) ( ~ 6)))
( or  ( not v_632_8 ) ( not v_767_2 ) ( >= ( - w_632 w_767) 6) ( <= ( - w_632 w_767) ( ~ 7)))
( or  ( not v_632_8 ) ( not v_767_8 ) ( >= ( - w_632 w_767) 6) ( <= ( - w_632 w_767) ( ~ 6)))
( or  ( not v_665_2 ) ( not v_666_2 ) ( = ( - w_665 w_666) 17) ( = ( - w_666 w_665) 17))
( or  ( not v_665_2 ) ( not v_666_8 ))
( or  ( not v_665_8 ) ( not v_666_2 ))
( or  ( not v_665_8 ) ( not v_666_8 ) ( = ( - w_665 w_666) 17) ( = ( - w_666 w_665) 17))
( or  ( not v_665_2 ) ( not v_767_2 ) ( >= ( - w_665 w_767) 9) ( <= ( - w_665 w_767) ( ~ 9)))
( or  ( not v_665_2 ) ( not v_767_8 ) ( >= ( - w_665 w_767) 10) ( <= ( - w_665 w_767) ( ~ 9)))
( or  ( not v_665_8 ) ( not v_767_2 ) ( >= ( - w_665 w_767) 9) ( <= ( - w_665 w_767) ( ~ 10)))
( or  ( not v_665_8 ) ( not v_767_8 ) ( >= ( - w_665 w_767) 9) ( <= ( - w_665 w_767) ( ~ 9)))
( or  ( not v_665_2 ) ( not v_768_2 ) ( >= ( - w_665 w_768) 5) ( <= ( - w_665 w_768) ( ~ 5)))
( or  ( not v_665_2 ) ( not v_768_8 ) ( >= ( - w_665 w_768) 5) ( <= ( - w_665 w_768) ( ~ 4)))
( or  ( not v_665_8 ) ( not v_768_2 ) ( >= ( - w_665 w_768) 4) ( <= ( - w_665 w_768) ( ~ 5)))
( or  ( not v_665_8 ) ( not v_768_8 ) ( >= ( - w_665 w_768) 5) ( <= ( - w_665 w_768) ( ~ 5)))
( or  ( not v_665_2 ) ( not v_785_2 ) ( >= ( - w_665 w_785) 16) ( <= ( - w_665 w_785) ( ~ 16)))
( or  ( not v_665_2 ) ( not v_785_8 ) ( >= ( - w_665 w_785) 16) ( <= ( - w_665 w_785) ( ~ 16)))
( or  ( not v_665_8 ) ( not v_785_2 ) ( >= ( - w_665 w_785) 16) ( <= ( - w_665 w_785) ( ~ 16)))
( or  ( not v_665_8 ) ( not v_785_8 ) ( >= ( - w_665 w_785) 16) ( <= ( - w_665 w_785) ( ~ 16)))
( or  ( not v_665_2 ) ( not v_786_2 ) ( >= ( - w_665 w_786) 26) ( <= ( - w_665 w_786) ( ~ 26)))
( or  ( not v_665_2 ) ( not v_786_8 ) ( >= ( - w_665 w_786) 27) ( <= ( - w_665 w_786) ( ~ 26)))
( or  ( not v_665_8 ) ( not v_786_2 ) ( >= ( - w_665 w_786) 26) ( <= ( - w_665 w_786) ( ~ 27)))
( or  ( not v_665_8 ) ( not v_786_8 ) ( >= ( - w_665 w_786) 26) ( <= ( - w_665 w_786) ( ~ 26)))
( or  ( not v_666_2 ) ( not v_767_2 ) ( >= ( - w_666 w_767) 5) ( <= ( - w_666 w_767) ( ~ 5)))
( or  ( not v_666_2 ) ( not v_767_8 ) ( >= ( - w_666 w_767) 5) ( <= ( - w_666 w_767) ( ~ 4)))
( or  ( not v_666_8 ) ( not v_767_2 ) ( >= ( - w_666 w_767) 4) ( <= ( - w_666 w_767) ( ~ 5)))
( or  ( not v_666_8 ) ( not v_767_8 ) ( >= ( - w_666 w_767) 5) ( <= ( - w_666 w_767) ( ~ 5)))
( or  ( not v_666_2 ) ( not v_768_2 ) ( >= ( - w_666 w_768) 17) ( <= ( - w_666 w_768) ( ~ 17)))
( or  ( not v_666_2 ) ( not v_768_8 ) ( >= ( - w_666 w_768) 18) ( <= ( - w_666 w_768) ( ~ 17)))
( or  ( not v_666_8 ) ( not v_768_2 ) ( >= ( - w_666 w_768) 17) ( <= ( - w_666 w_768) ( ~ 18)))
( or  ( not v_666_8 ) ( not v_768_8 ) ( >= ( - w_666 w_768) 17) ( <= ( - w_666 w_768) ( ~ 17)))
( or  ( not v_666_2 ) ( not v_785_2 ) ( >= ( - w_666 w_785) 4) ( <= ( - w_666 w_785) ( ~ 4)))
( or  ( not v_666_2 ) ( not v_785_8 ) ( >= ( - w_666 w_785) 4) ( <= ( - w_666 w_785) ( ~ 3)))
( or  ( not v_666_8 ) ( not v_785_2 ) ( >= ( - w_666 w_785) 3) ( <= ( - w_666 w_785) ( ~ 4)))
( or  ( not v_666_8 ) ( not v_785_8 ) ( >= ( - w_666 w_785) 4) ( <= ( - w_666 w_785) ( ~ 4)))
( or  ( not v_666_2 ) ( not v_786_2 ) ( >= ( - w_666 w_786) 16) ( <= ( - w_666 w_786) ( ~ 16)))
( or  ( not v_666_2 ) ( not v_786_8 ) ( >= ( - w_666 w_786) 16) ( <= ( - w_666 w_786) ( ~ 15)))
( or  ( not v_666_8 ) ( not v_786_2 ) ( >= ( - w_666 w_786) 15) ( <= ( - w_666 w_786) ( ~ 16)))
( or  ( not v_666_8 ) ( not v_786_8 ) ( >= ( - w_666 w_786) 16) ( <= ( - w_666 w_786) ( ~ 16)))
( or  ( not v_765_2 ) ( not v_766_2 ) ( = ( - w_765 w_766) 17) ( = ( - w_766 w_765) 17))
( or  ( not v_765_2 ) ( not v_766_8 ))
( or  ( not v_765_8 ) ( not v_766_2 ))
( or  ( not v_765_8 ) ( not v_766_8 ) ( = ( - w_765 w_766) 17) ( = ( - w_766 w_765) 17))
( or  ( not v_765_2 ) ( not v_767_2 ) ( >= ( - w_765 w_767) 11) ( <= ( - w_765 w_767) ( ~ 11)))
( or  ( not v_765_2 ) ( not v_767_8 ) ( >= ( - w_765 w_767) 11) ( <= ( - w_765 w_767) ( ~ 10)))
( or  ( not v_765_8 ) ( not v_767_2 ) ( >= ( - w_765 w_767) 10) ( <= ( - w_765 w_767) ( ~ 11)))
( or  ( not v_765_8 ) ( not v_767_8 ) ( >= ( - w_765 w_767) 11) ( <= ( - w_765 w_767) ( ~ 11)))
( or  ( not v_767_2 ) ( not v_768_2 ) ( = ( - w_767 w_768) 17) ( = ( - w_768 w_767) 17))
( or  ( not v_767_2 ) ( not v_768_8 ))
( or  ( not v_767_8 ) ( not v_768_2 ))
( or  ( not v_767_8 ) ( not v_768_8 ) ( = ( - w_767 w_768) 17) ( = ( - w_768 w_767) 17))
( or  ( not v_767_2 ) ( not v_785_2 ) ( >= ( - w_767 w_785) 8) ( <= ( - w_767 w_785) ( ~ 8)))
( or  ( not v_767_2 ) ( not v_785_8 ) ( >= ( - w_767 w_785) 8) ( <= ( - w_767 w_785) ( ~ 7)))
( or  ( not v_767_8 ) ( not v_785_2 ) ( >= ( - w_767 w_785) 7) ( <= ( - w_767 w_785) ( ~ 8)))
( or  ( not v_767_8 ) ( not v_785_8 ) ( >= ( - w_767 w_785) 8) ( <= ( - w_767 w_785) ( ~ 8)))
( or  ( not v_767_2 ) ( not v_786_2 ) ( >= ( - w_767 w_786) 19) ( <= ( - w_767 w_786) ( ~ 19)))
( or  ( not v_767_2 ) ( not v_786_8 ) ( >= ( - w_767 w_786) 19) ( <= ( - w_767 w_786) ( ~ 19)))
( or  ( not v_767_8 ) ( not v_786_2 ) ( >= ( - w_767 w_786) 19) ( <= ( - w_767 w_786) ( ~ 19)))
( or  ( not v_767_8 ) ( not v_786_8 ) ( >= ( - w_767 w_786) 19) ( <= ( - w_767 w_786) ( ~ 19)))
( or  ( not v_768_2 ) ( not v_785_2 ) ( >= ( - w_768 w_785) 19) ( <= ( - w_768 w_785) ( ~ 19)))
( or  ( not v_768_2 ) ( not v_785_8 ) ( >= ( - w_768 w_785) 19) ( <= ( - w_768 w_785) ( ~ 19)))
( or  ( not v_768_8 ) ( not v_785_2 ) ( >= ( - w_768 w_785) 19) ( <= ( - w_768 w_785) ( ~ 19)))
( or  ( not v_768_8 ) ( not v_785_8 ) ( >= ( - w_768 w_785) 19) ( <= ( - w_768 w_785) ( ~ 19)))
( or  ( not v_785_2 ) ( not v_786_2 ) ( = ( - w_785 w_786) 17) ( = ( - w_786 w_785) 17))
( or  ( not v_785_2 ) ( not v_786_8 ))
( or  ( not v_785_8 ) ( not v_786_2 ))
( or  ( not v_785_8 ) ( not v_786_8 ) ( = ( - w_785 w_786) 17) ( = ( - w_786 w_785) 17))
)
)