[12] | 1 | ( benchmark CELAR6_SUB0.smt |
---|
| 2 | :source {Celar Radio Link Frequency Assignment. This benchmark was coded into the SMT-LIB format by Albert Oliveras.} |
---|
| 3 | :status unsat |
---|
| 4 | :category { industrial } |
---|
| 5 | :difficulty { 1 } |
---|
| 6 | :logic QF_IDL |
---|
| 7 | :extrapreds ((v_13_2 )) |
---|
| 8 | :extrapreds ((v_13_8 )) |
---|
| 9 | :extrapreds ((v_14_2 )) |
---|
| 10 | :extrapreds ((v_14_8 )) |
---|
| 11 | :extrapreds ((v_15_2 )) |
---|
| 12 | :extrapreds ((v_15_8 )) |
---|
| 13 | :extrapreds ((v_16_2 )) |
---|
| 14 | :extrapreds ((v_16_8 )) |
---|
| 15 | :extrapreds ((v_321_2 )) |
---|
| 16 | :extrapreds ((v_321_8 )) |
---|
| 17 | :extrapreds ((v_322_2 )) |
---|
| 18 | :extrapreds ((v_322_8 )) |
---|
| 19 | :extrapreds ((v_323_2 )) |
---|
| 20 | :extrapreds ((v_323_8 )) |
---|
| 21 | :extrapreds ((v_324_2 )) |
---|
| 22 | :extrapreds ((v_324_8 )) |
---|
| 23 | :extrapreds ((v_519_2 )) |
---|
| 24 | :extrapreds ((v_519_8 )) |
---|
| 25 | :extrapreds ((v_520_2 )) |
---|
| 26 | :extrapreds ((v_520_8 )) |
---|
| 27 | :extrapreds ((v_557_2 )) |
---|
| 28 | :extrapreds ((v_557_8 )) |
---|
| 29 | :extrapreds ((v_558_2 )) |
---|
| 30 | :extrapreds ((v_558_8 )) |
---|
| 31 | :extrapreds ((v_593_2 )) |
---|
| 32 | :extrapreds ((v_593_8 )) |
---|
| 33 | :extrapreds ((v_594_2 )) |
---|
| 34 | :extrapreds ((v_594_8 )) |
---|
| 35 | :extrapreds ((v_597_2 )) |
---|
| 36 | :extrapreds ((v_597_8 )) |
---|
| 37 | :extrapreds ((v_598_2 )) |
---|
| 38 | :extrapreds ((v_598_8 )) |
---|
| 39 | :extrapreds ((v_599_2 )) |
---|
| 40 | :extrapreds ((v_599_8 )) |
---|
| 41 | :extrapreds ((v_600_2 )) |
---|
| 42 | :extrapreds ((v_600_8 )) |
---|
| 43 | :extrapreds ((v_613_2 )) |
---|
| 44 | :extrapreds ((v_613_8 )) |
---|
| 45 | :extrapreds ((v_614_2 )) |
---|
| 46 | :extrapreds ((v_614_8 )) |
---|
| 47 | :extrapreds ((v_629_2 )) |
---|
| 48 | :extrapreds ((v_629_8 )) |
---|
| 49 | :extrapreds ((v_630_2 )) |
---|
| 50 | :extrapreds ((v_630_8 )) |
---|
| 51 | :extrapreds ((v_631_2 )) |
---|
| 52 | :extrapreds ((v_631_8 )) |
---|
| 53 | :extrapreds ((v_632_2 )) |
---|
| 54 | :extrapreds ((v_632_8 )) |
---|
| 55 | :extrapreds ((v_665_2 )) |
---|
| 56 | :extrapreds ((v_665_8 )) |
---|
| 57 | :extrapreds ((v_666_2 )) |
---|
| 58 | :extrapreds ((v_666_8 )) |
---|
| 59 | :extrapreds ((v_765_2 )) |
---|
| 60 | :extrapreds ((v_765_8 )) |
---|
| 61 | :extrapreds ((v_766_2 )) |
---|
| 62 | :extrapreds ((v_766_8 )) |
---|
| 63 | :extrapreds ((v_767_2 )) |
---|
| 64 | :extrapreds ((v_767_8 )) |
---|
| 65 | :extrapreds ((v_768_2 )) |
---|
| 66 | :extrapreds ((v_768_8 )) |
---|
| 67 | :extrapreds ((v_785_2 )) |
---|
| 68 | :extrapreds ((v_785_8 )) |
---|
| 69 | :extrapreds ((v_786_2 )) |
---|
| 70 | :extrapreds ((v_786_8 )) |
---|
| 71 | :extrafuns ((w_13 Int )) |
---|
| 72 | :extrafuns ((w_14 Int )) |
---|
| 73 | :extrafuns ((w_15 Int )) |
---|
| 74 | :extrafuns ((w_16 Int )) |
---|
| 75 | :extrafuns ((w_321 Int )) |
---|
| 76 | :extrafuns ((w_322 Int )) |
---|
| 77 | :extrafuns ((w_323 Int )) |
---|
| 78 | :extrafuns ((w_324 Int )) |
---|
| 79 | :extrafuns ((w_519 Int )) |
---|
| 80 | :extrafuns ((w_520 Int )) |
---|
| 81 | :extrafuns ((w_557 Int )) |
---|
| 82 | :extrafuns ((w_558 Int )) |
---|
| 83 | :extrafuns ((w_593 Int )) |
---|
| 84 | :extrafuns ((w_594 Int )) |
---|
| 85 | :extrafuns ((w_597 Int )) |
---|
| 86 | :extrafuns ((w_598 Int )) |
---|
| 87 | :extrafuns ((w_599 Int )) |
---|
| 88 | :extrafuns ((w_600 Int )) |
---|
| 89 | :extrafuns ((w_613 Int )) |
---|
| 90 | :extrafuns ((w_614 Int )) |
---|
| 91 | :extrafuns ((w_629 Int )) |
---|
| 92 | :extrafuns ((w_630 Int )) |
---|
| 93 | :extrafuns ((w_631 Int )) |
---|
| 94 | :extrafuns ((w_632 Int )) |
---|
| 95 | :extrafuns ((w_665 Int )) |
---|
| 96 | :extrafuns ((w_666 Int )) |
---|
| 97 | :extrafuns ((w_765 Int )) |
---|
| 98 | :extrafuns ((w_766 Int )) |
---|
| 99 | :extrafuns ((w_767 Int )) |
---|
| 100 | :extrafuns ((w_768 Int )) |
---|
| 101 | :extrafuns ((w_785 Int )) |
---|
| 102 | :extrafuns ((w_786 Int )) |
---|
| 103 | :extrafuns ((z_0 Int )) |
---|
| 104 | :formula |
---|
| 105 | ( and |
---|
| 106 | ( or v_13_2 v_13_8 ) |
---|
| 107 | ( or ( not v_13_2) ( not v_13_8) ) |
---|
| 108 | ( or v_14_2 v_14_8 ) |
---|
| 109 | ( or ( not v_14_2) ( not v_14_8) ) |
---|
| 110 | ( or v_15_2 v_15_8 ) |
---|
| 111 | ( or ( not v_15_2) ( not v_15_8) ) |
---|
| 112 | ( or v_16_2 v_16_8 ) |
---|
| 113 | ( or ( not v_16_2) ( not v_16_8) ) |
---|
| 114 | ( or v_321_2 v_321_8 ) |
---|
| 115 | ( or ( not v_321_2) ( not v_321_8) ) |
---|
| 116 | ( or v_322_2 v_322_8 ) |
---|
| 117 | ( or ( not v_322_2) ( not v_322_8) ) |
---|
| 118 | ( or v_323_2 v_323_8 ) |
---|
| 119 | ( or ( not v_323_2) ( not v_323_8) ) |
---|
| 120 | ( or v_324_2 v_324_8 ) |
---|
| 121 | ( or ( not v_324_2) ( not v_324_8) ) |
---|
| 122 | ( or v_519_2 v_519_8 ) |
---|
| 123 | ( or ( not v_519_2) ( not v_519_8) ) |
---|
| 124 | ( or v_520_2 v_520_8 ) |
---|
| 125 | ( or ( not v_520_2) ( not v_520_8) ) |
---|
| 126 | ( or v_557_2 v_557_8 ) |
---|
| 127 | ( or ( not v_557_2) ( not v_557_8) ) |
---|
| 128 | ( or v_558_2 v_558_8 ) |
---|
| 129 | ( or ( not v_558_2) ( not v_558_8) ) |
---|
| 130 | ( or v_593_2 v_593_8 ) |
---|
| 131 | ( or ( not v_593_2) ( not v_593_8) ) |
---|
| 132 | ( or v_594_2 v_594_8 ) |
---|
| 133 | ( or ( not v_594_2) ( not v_594_8) ) |
---|
| 134 | ( or v_597_2 v_597_8 ) |
---|
| 135 | ( or ( not v_597_2) ( not v_597_8) ) |
---|
| 136 | ( or v_598_2 v_598_8 ) |
---|
| 137 | ( or ( not v_598_2) ( not v_598_8) ) |
---|
| 138 | ( or v_599_2 v_599_8 ) |
---|
| 139 | ( or ( not v_599_2) ( not v_599_8) ) |
---|
| 140 | ( or v_600_2 v_600_8 ) |
---|
| 141 | ( or ( not v_600_2) ( not v_600_8) ) |
---|
| 142 | ( or v_613_2 v_613_8 ) |
---|
| 143 | ( or ( not v_613_2) ( not v_613_8) ) |
---|
| 144 | ( or v_614_2 v_614_8 ) |
---|
| 145 | ( or ( not v_614_2) ( not v_614_8) ) |
---|
| 146 | ( or v_629_2 v_629_8 ) |
---|
| 147 | ( or ( not v_629_2) ( not v_629_8) ) |
---|
| 148 | ( or v_630_2 v_630_8 ) |
---|
| 149 | ( or ( not v_630_2) ( not v_630_8) ) |
---|
| 150 | ( or v_631_2 v_631_8 ) |
---|
| 151 | ( or ( not v_631_2) ( not v_631_8) ) |
---|
| 152 | ( or v_632_2 v_632_8 ) |
---|
| 153 | ( or ( not v_632_2) ( not v_632_8) ) |
---|
| 154 | ( or v_665_2 v_665_8 ) |
---|
| 155 | ( or ( not v_665_2) ( not v_665_8) ) |
---|
| 156 | ( or v_666_2 v_666_8 ) |
---|
| 157 | ( or ( not v_666_2) ( not v_666_8) ) |
---|
| 158 | ( or v_765_2 v_765_8 ) |
---|
| 159 | ( or ( not v_765_2) ( not v_765_8) ) |
---|
| 160 | ( or v_766_2 v_766_8 ) |
---|
| 161 | ( or ( not v_766_2) ( not v_766_8) ) |
---|
| 162 | ( or v_767_2 v_767_8 ) |
---|
| 163 | ( or ( not v_767_2) ( not v_767_8) ) |
---|
| 164 | ( or v_768_2 v_768_8 ) |
---|
| 165 | ( or ( not v_768_2) ( not v_768_8) ) |
---|
| 166 | ( or v_785_2 v_785_8 ) |
---|
| 167 | ( or ( not v_785_2) ( not v_785_8) ) |
---|
| 168 | ( or v_786_2 v_786_8 ) |
---|
| 169 | ( or ( not v_786_2) ( not v_786_8) ) |
---|
| 170 | ( 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) ) ) |
---|
| 171 | ( 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) ) ) |
---|
| 172 | ( 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) ) ) |
---|
| 173 | ( 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) ) ) |
---|
| 174 | ( 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) ) ) |
---|
| 175 | ( 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) ) ) |
---|
| 176 | ( 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) ) ) |
---|
| 177 | ( 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) ) ) |
---|
| 178 | ( 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) ) ) |
---|
| 179 | ( 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) ) ) |
---|
| 180 | ( 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) ) ) |
---|
| 181 | ( 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) ) ) |
---|
| 182 | ( 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) ) ) |
---|
| 183 | ( 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) ) ) |
---|
| 184 | ( 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) ) ) |
---|
| 185 | ( 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) ) ) |
---|
| 186 | ( 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) ) ) |
---|
| 187 | ( 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) ) ) |
---|
| 188 | ( 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) ) ) |
---|
| 189 | ( 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) ) ) |
---|
| 190 | ( 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) ) ) |
---|
| 191 | ( 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) ) ) |
---|
| 192 | ( 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) ) ) |
---|
| 193 | ( 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) ) ) |
---|
| 194 | ( 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) ) ) |
---|
| 195 | ( 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) ) ) |
---|
| 196 | ( 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) ) ) |
---|
| 197 | ( 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) ) ) |
---|
| 198 | ( 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) ) ) |
---|
| 199 | ( 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) ) ) |
---|
| 200 | ( 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) ) ) |
---|
| 201 | ( 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) ) ) |
---|
| 202 | ( 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) ) ) |
---|
| 203 | ( 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) ) ) |
---|
| 204 | ( 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) ) ) |
---|
| 205 | ( 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) ) ) |
---|
| 206 | ( 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) ) ) |
---|
| 207 | ( 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) ) ) |
---|
| 208 | ( 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) ) ) |
---|
| 209 | ( 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) ) ) |
---|
| 210 | ( 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) ) ) |
---|
| 211 | ( 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) ) ) |
---|
| 212 | ( 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) ) ) |
---|
| 213 | ( 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) ) ) |
---|
| 214 | ( 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) ) ) |
---|
| 215 | ( 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) ) ) |
---|
| 216 | ( 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) ) ) |
---|
| 217 | ( 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) ) ) |
---|
| 218 | ( 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) ) ) |
---|
| 219 | ( 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) ) ) |
---|
| 220 | ( 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) ) ) |
---|
| 221 | ( 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) ) ) |
---|
| 222 | ( 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) ) ) |
---|
| 223 | ( 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) ) ) |
---|
| 224 | ( 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) ) ) |
---|
| 225 | ( 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) ) ) |
---|
| 226 | ( 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) ) ) |
---|
| 227 | ( 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) ) ) |
---|
| 228 | ( 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) ) ) |
---|
| 229 | ( 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) ) ) |
---|
| 230 | ( 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) ) ) |
---|
| 231 | ( 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) ) ) |
---|
| 232 | ( 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) ) ) |
---|
| 233 | ( 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) ) ) |
---|
| 234 | ( or ( not v_13_2 ) ( not v_14_2 ) ( = ( - w_13 w_14) 17) ( = ( - w_14 w_13) 17)) |
---|
| 235 | ( or ( not v_13_2 ) ( not v_14_8 )) |
---|
| 236 | ( or ( not v_13_8 ) ( not v_14_2 )) |
---|
| 237 | ( or ( not v_13_8 ) ( not v_14_8 ) ( = ( - w_13 w_14) 17) ( = ( - w_14 w_13) 17)) |
---|
| 238 | ( or ( not v_13_2 ) ( not v_15_2 ) ( >= ( - w_13 w_15) 5) ( <= ( - w_13 w_15) ( ~ 5))) |
---|
| 239 | ( or ( not v_13_2 ) ( not v_15_8 ) ( >= ( - w_13 w_15) 5) ( <= ( - w_13 w_15) ( ~ 4))) |
---|
| 240 | ( or ( not v_13_8 ) ( not v_15_2 ) ( >= ( - w_13 w_15) 4) ( <= ( - w_13 w_15) ( ~ 5))) |
---|
| 241 | ( or ( not v_13_8 ) ( not v_15_8 ) ( >= ( - w_13 w_15) 5) ( <= ( - w_13 w_15) ( ~ 5))) |
---|
| 242 | ( or ( not v_13_2 ) ( not v_16_2 ) ( >= ( - w_13 w_16) 14) ( <= ( - w_13 w_16) ( ~ 14))) |
---|
| 243 | ( or ( not v_13_2 ) ( not v_16_8 ) ( >= ( - w_13 w_16) 14) ( <= ( - w_13 w_16) ( ~ 13))) |
---|
| 244 | ( or ( not v_13_8 ) ( not v_16_2 ) ( >= ( - w_13 w_16) 13) ( <= ( - w_13 w_16) ( ~ 14))) |
---|
| 245 | ( or ( not v_13_8 ) ( not v_16_8 ) ( >= ( - w_13 w_16) 14) ( <= ( - w_13 w_16) ( ~ 14))) |
---|
| 246 | ( or ( not v_13_2 ) ( not v_321_2 ) ( >= ( - w_13 w_321) 1) ( <= ( - w_13 w_321) ( ~ 1))) |
---|
| 247 | ( or ( not v_13_2 ) ( not v_321_8 ) ( >= ( - w_13 w_321) 2) ( <= ( - w_13 w_321) ( ~ 1))) |
---|
| 248 | ( or ( not v_13_8 ) ( not v_321_2 ) ( >= ( - w_13 w_321) 1) ( <= ( - w_13 w_321) ( ~ 2))) |
---|
| 249 | ( or ( not v_13_8 ) ( not v_321_8 ) ( >= ( - w_13 w_321) 1) ( <= ( - w_13 w_321) ( ~ 1))) |
---|
| 250 | ( or ( not v_13_2 ) ( not v_322_2 ) ( >= ( - w_13 w_322) 14) ( <= ( - w_13 w_322) ( ~ 14))) |
---|
| 251 | ( or ( not v_13_2 ) ( not v_322_8 ) ( >= ( - w_13 w_322) 14) ( <= ( - w_13 w_322) ( ~ 13))) |
---|
| 252 | ( or ( not v_13_8 ) ( not v_322_2 ) ( >= ( - w_13 w_322) 13) ( <= ( - w_13 w_322) ( ~ 14))) |
---|
| 253 | ( or ( not v_13_8 ) ( not v_322_8 ) ( >= ( - w_13 w_322) 14) ( <= ( - w_13 w_322) ( ~ 14))) |
---|
| 254 | ( or ( not v_13_2 ) ( not v_323_2 ) ( >= ( - w_13 w_323) 12) ( <= ( - w_13 w_323) ( ~ 12))) |
---|
| 255 | ( or ( not v_13_2 ) ( not v_323_8 ) ( >= ( - w_13 w_323) 13) ( <= ( - w_13 w_323) ( ~ 12))) |
---|
| 256 | ( or ( not v_13_8 ) ( not v_323_2 ) ( >= ( - w_13 w_323) 12) ( <= ( - w_13 w_323) ( ~ 13))) |
---|
| 257 | ( or ( not v_13_8 ) ( not v_323_8 ) ( >= ( - w_13 w_323) 12) ( <= ( - w_13 w_323) ( ~ 12))) |
---|
| 258 | ( or ( not v_13_2 ) ( not v_324_2 ) ( >= ( - w_13 w_324) 4) ( <= ( - w_13 w_324) ( ~ 4))) |
---|
| 259 | ( or ( not v_13_2 ) ( not v_324_8 ) ( >= ( - w_13 w_324) 5) ( <= ( - w_13 w_324) ( ~ 4))) |
---|
| 260 | ( or ( not v_13_8 ) ( not v_324_2 ) ( >= ( - w_13 w_324) 4) ( <= ( - w_13 w_324) ( ~ 5))) |
---|
| 261 | ( or ( not v_13_8 ) ( not v_324_8 ) ( >= ( - w_13 w_324) 4) ( <= ( - w_13 w_324) ( ~ 4))) |
---|
| 262 | ( or ( not v_13_2 ) ( not v_557_2 ) ( >= ( - w_13 w_557) 7) ( <= ( - w_13 w_557) ( ~ 7))) |
---|
| 263 | ( or ( not v_13_2 ) ( not v_557_8 ) ( >= ( - w_13 w_557) 7) ( <= ( - w_13 w_557) ( ~ 7))) |
---|
| 264 | ( or ( not v_13_8 ) ( not v_557_2 ) ( >= ( - w_13 w_557) 7) ( <= ( - w_13 w_557) ( ~ 7))) |
---|
| 265 | ( or ( not v_13_8 ) ( not v_557_8 ) ( >= ( - w_13 w_557) 7) ( <= ( - w_13 w_557) ( ~ 7))) |
---|
| 266 | ( or ( not v_13_2 ) ( not v_558_2 ) ( >= ( - w_13 w_558) 19) ( <= ( - w_13 w_558) ( ~ 19))) |
---|
| 267 | ( or ( not v_13_2 ) ( not v_558_8 ) ( >= ( - w_13 w_558) 20) ( <= ( - w_13 w_558) ( ~ 19))) |
---|
| 268 | ( or ( not v_13_8 ) ( not v_558_2 ) ( >= ( - w_13 w_558) 19) ( <= ( - w_13 w_558) ( ~ 20))) |
---|
| 269 | ( or ( not v_13_8 ) ( not v_558_8 ) ( >= ( - w_13 w_558) 19) ( <= ( - w_13 w_558) ( ~ 19))) |
---|
| 270 | ( or ( not v_13_2 ) ( not v_599_2 ) ( >= ( - w_13 w_599) 2) ( <= ( - w_13 w_599) ( ~ 2))) |
---|
| 271 | ( or ( not v_13_2 ) ( not v_599_8 ) ( >= ( - w_13 w_599) 3) ( <= ( - w_13 w_599) ( ~ 2))) |
---|
| 272 | ( or ( not v_13_8 ) ( not v_599_2 ) ( >= ( - w_13 w_599) 2) ( <= ( - w_13 w_599) ( ~ 3))) |
---|
| 273 | ( or ( not v_13_8 ) ( not v_599_8 ) ( >= ( - w_13 w_599) 2) ( <= ( - w_13 w_599) ( ~ 2))) |
---|
| 274 | ( or ( not v_13_2 ) ( not v_600_2 ) ( >= ( - w_13 w_600) 15) ( <= ( - w_13 w_600) ( ~ 15))) |
---|
| 275 | ( or ( not v_13_2 ) ( not v_600_8 ) ( >= ( - w_13 w_600) 15) ( <= ( - w_13 w_600) ( ~ 14))) |
---|
| 276 | ( or ( not v_13_8 ) ( not v_600_2 ) ( >= ( - w_13 w_600) 14) ( <= ( - w_13 w_600) ( ~ 15))) |
---|
| 277 | ( or ( not v_13_8 ) ( not v_600_8 ) ( >= ( - w_13 w_600) 15) ( <= ( - w_13 w_600) ( ~ 15))) |
---|
| 278 | ( or ( not v_13_2 ) ( not v_665_2 ) ( >= ( - w_13 w_665) 13) ( <= ( - w_13 w_665) ( ~ 13))) |
---|
| 279 | ( or ( not v_13_2 ) ( not v_665_8 ) ( >= ( - w_13 w_665) 14) ( <= ( - w_13 w_665) ( ~ 13))) |
---|
| 280 | ( or ( not v_13_8 ) ( not v_665_2 ) ( >= ( - w_13 w_665) 13) ( <= ( - w_13 w_665) ( ~ 14))) |
---|
| 281 | ( or ( not v_13_8 ) ( not v_665_8 ) ( >= ( - w_13 w_665) 13) ( <= ( - w_13 w_665) ( ~ 13))) |
---|
| 282 | ( or ( not v_13_2 ) ( not v_666_2 ) ( >= ( - w_13 w_666) 1) ( <= ( - w_13 w_666) ( ~ 1))) |
---|
| 283 | ( or ( not v_13_2 ) ( not v_666_8 ) ( >= ( - w_13 w_666) 1) ( <= ( - w_13 w_666) ( ~ 1))) |
---|
| 284 | ( or ( not v_13_8 ) ( not v_666_2 ) ( >= ( - w_13 w_666) 1) ( <= ( - w_13 w_666) ( ~ 1))) |
---|
| 285 | ( or ( not v_13_8 ) ( not v_666_8 ) ( >= ( - w_13 w_666) 1) ( <= ( - w_13 w_666) ( ~ 1))) |
---|
| 286 | ( or ( not v_13_2 ) ( not v_767_2 ) ( >= ( - w_13 w_767) 5) ( <= ( - w_13 w_767) ( ~ 5))) |
---|
| 287 | ( or ( not v_13_2 ) ( not v_767_8 ) ( >= ( - w_13 w_767) 5) ( <= ( - w_13 w_767) ( ~ 4))) |
---|
| 288 | ( or ( not v_13_8 ) ( not v_767_2 ) ( >= ( - w_13 w_767) 4) ( <= ( - w_13 w_767) ( ~ 5))) |
---|
| 289 | ( or ( not v_13_8 ) ( not v_767_8 ) ( >= ( - w_13 w_767) 5) ( <= ( - w_13 w_767) ( ~ 5))) |
---|
| 290 | ( or ( not v_13_2 ) ( not v_768_2 ) ( >= ( - w_13 w_768) 17) ( <= ( - w_13 w_768) ( ~ 17))) |
---|
| 291 | ( or ( not v_13_2 ) ( not v_768_8 ) ( >= ( - w_13 w_768) 18) ( <= ( - w_13 w_768) ( ~ 17))) |
---|
| 292 | ( or ( not v_13_8 ) ( not v_768_2 ) ( >= ( - w_13 w_768) 17) ( <= ( - w_13 w_768) ( ~ 18))) |
---|
| 293 | ( or ( not v_13_8 ) ( not v_768_8 ) ( >= ( - w_13 w_768) 17) ( <= ( - w_13 w_768) ( ~ 17))) |
---|
| 294 | ( or ( not v_14_2 ) ( not v_15_2 ) ( >= ( - w_14 w_15) 14) ( <= ( - w_14 w_15) ( ~ 14))) |
---|
| 295 | ( or ( not v_14_2 ) ( not v_15_8 ) ( >= ( - w_14 w_15) 14) ( <= ( - w_14 w_15) ( ~ 13))) |
---|
| 296 | ( or ( not v_14_8 ) ( not v_15_2 ) ( >= ( - w_14 w_15) 13) ( <= ( - w_14 w_15) ( ~ 14))) |
---|
| 297 | ( or ( not v_14_8 ) ( not v_15_8 ) ( >= ( - w_14 w_15) 14) ( <= ( - w_14 w_15) ( ~ 14))) |
---|
| 298 | ( or ( not v_14_2 ) ( not v_16_2 ) ( >= ( - w_14 w_16) 5) ( <= ( - w_14 w_16) ( ~ 5))) |
---|
| 299 | ( or ( not v_14_2 ) ( not v_16_8 ) ( >= ( - w_14 w_16) 5) ( <= ( - w_14 w_16) ( ~ 4))) |
---|
| 300 | ( or ( not v_14_8 ) ( not v_16_2 ) ( >= ( - w_14 w_16) 4) ( <= ( - w_14 w_16) ( ~ 5))) |
---|
| 301 | ( or ( not v_14_8 ) ( not v_16_8 ) ( >= ( - w_14 w_16) 5) ( <= ( - w_14 w_16) ( ~ 5))) |
---|
| 302 | ( or ( not v_14_2 ) ( not v_321_2 ) ( >= ( - w_14 w_321) 12) ( <= ( - w_14 w_321) ( ~ 12))) |
---|
| 303 | ( or ( not v_14_2 ) ( not v_321_8 ) ( >= ( - w_14 w_321) 13) ( <= ( - w_14 w_321) ( ~ 12))) |
---|
| 304 | ( or ( not v_14_8 ) ( not v_321_2 ) ( >= ( - w_14 w_321) 12) ( <= ( - w_14 w_321) ( ~ 13))) |
---|
| 305 | ( or ( not v_14_8 ) ( not v_321_8 ) ( >= ( - w_14 w_321) 12) ( <= ( - w_14 w_321) ( ~ 12))) |
---|
| 306 | ( or ( not v_14_2 ) ( not v_322_2 ) ( >= ( - w_14 w_322) 1) ( <= ( - w_14 w_322) ( ~ 1))) |
---|
| 307 | ( or ( not v_14_2 ) ( not v_322_8 ) ( >= ( - w_14 w_322) 2) ( <= ( - w_14 w_322) ( ~ 1))) |
---|
| 308 | ( or ( not v_14_8 ) ( not v_322_2 ) ( >= ( - w_14 w_322) 1) ( <= ( - w_14 w_322) ( ~ 2))) |
---|
| 309 | ( or ( not v_14_8 ) ( not v_322_8 ) ( >= ( - w_14 w_322) 1) ( <= ( - w_14 w_322) ( ~ 1))) |
---|
| 310 | ( or ( not v_14_2 ) ( not v_323_2 ) ( >= ( - w_14 w_323) 4) ( <= ( - w_14 w_323) ( ~ 4))) |
---|
| 311 | ( or ( not v_14_2 ) ( not v_323_8 ) ( >= ( - w_14 w_323) 5) ( <= ( - w_14 w_323) ( ~ 4))) |
---|
| 312 | ( or ( not v_14_8 ) ( not v_323_2 ) ( >= ( - w_14 w_323) 4) ( <= ( - w_14 w_323) ( ~ 5))) |
---|
| 313 | ( or ( not v_14_8 ) ( not v_323_8 ) ( >= ( - w_14 w_323) 4) ( <= ( - w_14 w_323) ( ~ 4))) |
---|
| 314 | ( or ( not v_14_2 ) ( not v_324_2 ) ( >= ( - w_14 w_324) 11) ( <= ( - w_14 w_324) ( ~ 11))) |
---|
| 315 | ( or ( not v_14_2 ) ( not v_324_8 ) ( >= ( - w_14 w_324) 12) ( <= ( - w_14 w_324) ( ~ 11))) |
---|
| 316 | ( or ( not v_14_8 ) ( not v_324_2 ) ( >= ( - w_14 w_324) 11) ( <= ( - w_14 w_324) ( ~ 12))) |
---|
| 317 | ( or ( not v_14_8 ) ( not v_324_8 ) ( >= ( - w_14 w_324) 11) ( <= ( - w_14 w_324) ( ~ 11))) |
---|
| 318 | ( or ( not v_14_2 ) ( not v_557_2 ) ( >= ( - w_14 w_557) 19) ( <= ( - w_14 w_557) ( ~ 19))) |
---|
| 319 | ( or ( not v_14_2 ) ( not v_557_8 ) ( >= ( - w_14 w_557) 20) ( <= ( - w_14 w_557) ( ~ 19))) |
---|
| 320 | ( or ( not v_14_8 ) ( not v_557_2 ) ( >= ( - w_14 w_557) 19) ( <= ( - w_14 w_557) ( ~ 20))) |
---|
| 321 | ( or ( not v_14_8 ) ( not v_557_8 ) ( >= ( - w_14 w_557) 19) ( <= ( - w_14 w_557) ( ~ 19))) |
---|
| 322 | ( or ( not v_14_2 ) ( not v_558_2 ) ( >= ( - w_14 w_558) 30) ( <= ( - w_14 w_558) ( ~ 30))) |
---|
| 323 | ( or ( not v_14_2 ) ( not v_558_8 ) ( >= ( - w_14 w_558) 30) ( <= ( - w_14 w_558) ( ~ 29))) |
---|
| 324 | ( or ( not v_14_8 ) ( not v_558_2 ) ( >= ( - w_14 w_558) 29) ( <= ( - w_14 w_558) ( ~ 30))) |
---|
| 325 | ( or ( not v_14_8 ) ( not v_558_8 ) ( >= ( - w_14 w_558) 30) ( <= ( - w_14 w_558) ( ~ 30))) |
---|
| 326 | ( or ( not v_14_2 ) ( not v_599_2 ) ( >= ( - w_14 w_599) 15) ( <= ( - w_14 w_599) ( ~ 15))) |
---|
| 327 | ( or ( not v_14_2 ) ( not v_599_8 ) ( >= ( - w_14 w_599) 15) ( <= ( - w_14 w_599) ( ~ 14))) |
---|
| 328 | ( or ( not v_14_8 ) ( not v_599_2 ) ( >= ( - w_14 w_599) 14) ( <= ( - w_14 w_599) ( ~ 15))) |
---|
| 329 | ( or ( not v_14_8 ) ( not v_599_8 ) ( >= ( - w_14 w_599) 15) ( <= ( - w_14 w_599) ( ~ 15))) |
---|
| 330 | ( or ( not v_14_2 ) ( not v_600_2 ) ( >= ( - w_14 w_600) 25) ( <= ( - w_14 w_600) ( ~ 25))) |
---|
| 331 | ( or ( not v_14_2 ) ( not v_600_8 ) ( >= ( - w_14 w_600) 25) ( <= ( - w_14 w_600) ( ~ 25))) |
---|
| 332 | ( or ( not v_14_8 ) ( not v_600_2 ) ( >= ( - w_14 w_600) 25) ( <= ( - w_14 w_600) ( ~ 25))) |
---|
| 333 | ( or ( not v_14_8 ) ( not v_600_8 ) ( >= ( - w_14 w_600) 25) ( <= ( - w_14 w_600) ( ~ 25))) |
---|
| 334 | ( or ( not v_14_2 ) ( not v_665_2 ) ( >= ( - w_14 w_665) 1) ( <= ( - w_14 w_665) ( ~ 1))) |
---|
| 335 | ( or ( not v_14_2 ) ( not v_665_8 ) ( >= ( - w_14 w_665) 1) ( <= ( - w_14 w_665) ( ~ 1))) |
---|
| 336 | ( or ( not v_14_8 ) ( not v_665_2 ) ( >= ( - w_14 w_665) 1) ( <= ( - w_14 w_665) ( ~ 1))) |
---|
| 337 | ( or ( not v_14_8 ) ( not v_665_8 ) ( >= ( - w_14 w_665) 1) ( <= ( - w_14 w_665) ( ~ 1))) |
---|
| 338 | ( or ( not v_14_2 ) ( not v_666_2 ) ( >= ( - w_14 w_666) 13) ( <= ( - w_14 w_666) ( ~ 13))) |
---|
| 339 | ( or ( not v_14_2 ) ( not v_666_8 ) ( >= ( - w_14 w_666) 14) ( <= ( - w_14 w_666) ( ~ 13))) |
---|
| 340 | ( or ( not v_14_8 ) ( not v_666_2 ) ( >= ( - w_14 w_666) 13) ( <= ( - w_14 w_666) ( ~ 14))) |
---|
| 341 | ( or ( not v_14_8 ) ( not v_666_8 ) ( >= ( - w_14 w_666) 13) ( <= ( - w_14 w_666) ( ~ 13))) |
---|
| 342 | ( or ( not v_14_2 ) ( not v_767_2 ) ( >= ( - w_14 w_767) 9) ( <= ( - w_14 w_767) ( ~ 9))) |
---|
| 343 | ( or ( not v_14_2 ) ( not v_767_8 ) ( >= ( - w_14 w_767) 10) ( <= ( - w_14 w_767) ( ~ 9))) |
---|
| 344 | ( or ( not v_14_8 ) ( not v_767_2 ) ( >= ( - w_14 w_767) 9) ( <= ( - w_14 w_767) ( ~ 10))) |
---|
| 345 | ( or ( not v_14_8 ) ( not v_767_8 ) ( >= ( - w_14 w_767) 9) ( <= ( - w_14 w_767) ( ~ 9))) |
---|
| 346 | ( or ( not v_14_2 ) ( not v_768_2 ) ( >= ( - w_14 w_768) 5) ( <= ( - w_14 w_768) ( ~ 5))) |
---|
| 347 | ( or ( not v_14_2 ) ( not v_768_8 ) ( >= ( - w_14 w_768) 5) ( <= ( - w_14 w_768) ( ~ 4))) |
---|
| 348 | ( or ( not v_14_8 ) ( not v_768_2 ) ( >= ( - w_14 w_768) 4) ( <= ( - w_14 w_768) ( ~ 5))) |
---|
| 349 | ( or ( not v_14_8 ) ( not v_768_8 ) ( >= ( - w_14 w_768) 5) ( <= ( - w_14 w_768) ( ~ 5))) |
---|
| 350 | ( or ( not v_15_2 ) ( not v_16_2 ) ( = ( - w_15 w_16) 17) ( = ( - w_16 w_15) 17)) |
---|
| 351 | ( or ( not v_15_2 ) ( not v_16_8 )) |
---|
| 352 | ( or ( not v_15_8 ) ( not v_16_2 )) |
---|
| 353 | ( or ( not v_15_8 ) ( not v_16_8 ) ( = ( - w_15 w_16) 17) ( = ( - w_16 w_15) 17)) |
---|
| 354 | ( or ( not v_15_2 ) ( not v_321_2 ) ( >= ( - w_15 w_321) 1) ( <= ( - w_15 w_321) ( ~ 1))) |
---|
| 355 | ( or ( not v_15_2 ) ( not v_321_8 ) ( >= ( - w_15 w_321) 2) ( <= ( - w_15 w_321) ( ~ 1))) |
---|
| 356 | ( or ( not v_15_8 ) ( not v_321_2 ) ( >= ( - w_15 w_321) 1) ( <= ( - w_15 w_321) ( ~ 2))) |
---|
| 357 | ( or ( not v_15_8 ) ( not v_321_8 ) ( >= ( - w_15 w_321) 1) ( <= ( - w_15 w_321) ( ~ 1))) |
---|
| 358 | ( or ( not v_15_2 ) ( not v_322_2 ) ( >= ( - w_15 w_322) 14) ( <= ( - w_15 w_322) ( ~ 14))) |
---|
| 359 | ( or ( not v_15_2 ) ( not v_322_8 ) ( >= ( - w_15 w_322) 14) ( <= ( - w_15 w_322) ( ~ 13))) |
---|
| 360 | ( or ( not v_15_8 ) ( not v_322_2 ) ( >= ( - w_15 w_322) 13) ( <= ( - w_15 w_322) ( ~ 14))) |
---|
| 361 | ( or ( not v_15_8 ) ( not v_322_8 ) ( >= ( - w_15 w_322) 14) ( <= ( - w_15 w_322) ( ~ 14))) |
---|
| 362 | ( or ( not v_15_2 ) ( not v_323_2 ) ( >= ( - w_15 w_323) 12) ( <= ( - w_15 w_323) ( ~ 12))) |
---|
| 363 | ( or ( not v_15_2 ) ( not v_323_8 ) ( >= ( - w_15 w_323) 13) ( <= ( - w_15 w_323) ( ~ 12))) |
---|
| 364 | ( or ( not v_15_8 ) ( not v_323_2 ) ( >= ( - w_15 w_323) 12) ( <= ( - w_15 w_323) ( ~ 13))) |
---|
| 365 | ( or ( not v_15_8 ) ( not v_323_8 ) ( >= ( - w_15 w_323) 12) ( <= ( - w_15 w_323) ( ~ 12))) |
---|
| 366 | ( or ( not v_15_2 ) ( not v_324_2 ) ( >= ( - w_15 w_324) 4) ( <= ( - w_15 w_324) ( ~ 4))) |
---|
| 367 | ( or ( not v_15_2 ) ( not v_324_8 ) ( >= ( - w_15 w_324) 5) ( <= ( - w_15 w_324) ( ~ 4))) |
---|
| 368 | ( or ( not v_15_8 ) ( not v_324_2 ) ( >= ( - w_15 w_324) 4) ( <= ( - w_15 w_324) ( ~ 5))) |
---|
| 369 | ( or ( not v_15_8 ) ( not v_324_8 ) ( >= ( - w_15 w_324) 4) ( <= ( - w_15 w_324) ( ~ 4))) |
---|
| 370 | ( or ( not v_15_2 ) ( not v_557_2 ) ( >= ( - w_15 w_557) 7) ( <= ( - w_15 w_557) ( ~ 7))) |
---|
| 371 | ( or ( not v_15_2 ) ( not v_557_8 ) ( >= ( - w_15 w_557) 7) ( <= ( - w_15 w_557) ( ~ 7))) |
---|
| 372 | ( or ( not v_15_8 ) ( not v_557_2 ) ( >= ( - w_15 w_557) 7) ( <= ( - w_15 w_557) ( ~ 7))) |
---|
| 373 | ( or ( not v_15_8 ) ( not v_557_8 ) ( >= ( - w_15 w_557) 7) ( <= ( - w_15 w_557) ( ~ 7))) |
---|
| 374 | ( or ( not v_15_2 ) ( not v_558_2 ) ( >= ( - w_15 w_558) 19) ( <= ( - w_15 w_558) ( ~ 19))) |
---|
| 375 | ( or ( not v_15_2 ) ( not v_558_8 ) ( >= ( - w_15 w_558) 20) ( <= ( - w_15 w_558) ( ~ 19))) |
---|
| 376 | ( or ( not v_15_8 ) ( not v_558_2 ) ( >= ( - w_15 w_558) 19) ( <= ( - w_15 w_558) ( ~ 20))) |
---|
| 377 | ( or ( not v_15_8 ) ( not v_558_8 ) ( >= ( - w_15 w_558) 19) ( <= ( - w_15 w_558) ( ~ 19))) |
---|
| 378 | ( or ( not v_15_2 ) ( not v_599_2 ) ( >= ( - w_15 w_599) 2) ( <= ( - w_15 w_599) ( ~ 2))) |
---|
| 379 | ( or ( not v_15_2 ) ( not v_599_8 ) ( >= ( - w_15 w_599) 3) ( <= ( - w_15 w_599) ( ~ 2))) |
---|
| 380 | ( or ( not v_15_8 ) ( not v_599_2 ) ( >= ( - w_15 w_599) 2) ( <= ( - w_15 w_599) ( ~ 3))) |
---|
| 381 | ( or ( not v_15_8 ) ( not v_599_8 ) ( >= ( - w_15 w_599) 2) ( <= ( - w_15 w_599) ( ~ 2))) |
---|
| 382 | ( or ( not v_15_2 ) ( not v_600_2 ) ( >= ( - w_15 w_600) 15) ( <= ( - w_15 w_600) ( ~ 15))) |
---|
| 383 | ( or ( not v_15_2 ) ( not v_600_8 ) ( >= ( - w_15 w_600) 15) ( <= ( - w_15 w_600) ( ~ 14))) |
---|
| 384 | ( or ( not v_15_8 ) ( not v_600_2 ) ( >= ( - w_15 w_600) 14) ( <= ( - w_15 w_600) ( ~ 15))) |
---|
| 385 | ( or ( not v_15_8 ) ( not v_600_8 ) ( >= ( - w_15 w_600) 15) ( <= ( - w_15 w_600) ( ~ 15))) |
---|
| 386 | ( or ( not v_15_2 ) ( not v_665_2 ) ( >= ( - w_15 w_665) 13) ( <= ( - w_15 w_665) ( ~ 13))) |
---|
| 387 | ( or ( not v_15_2 ) ( not v_665_8 ) ( >= ( - w_15 w_665) 14) ( <= ( - w_15 w_665) ( ~ 13))) |
---|
| 388 | ( or ( not v_15_8 ) ( not v_665_2 ) ( >= ( - w_15 w_665) 13) ( <= ( - w_15 w_665) ( ~ 14))) |
---|
| 389 | ( or ( not v_15_8 ) ( not v_665_8 ) ( >= ( - w_15 w_665) 13) ( <= ( - w_15 w_665) ( ~ 13))) |
---|
| 390 | ( or ( not v_15_2 ) ( not v_666_2 ) ( >= ( - w_15 w_666) 1) ( <= ( - w_15 w_666) ( ~ 1))) |
---|
| 391 | ( or ( not v_15_2 ) ( not v_666_8 ) ( >= ( - w_15 w_666) 1) ( <= ( - w_15 w_666) ( ~ 1))) |
---|
| 392 | ( or ( not v_15_8 ) ( not v_666_2 ) ( >= ( - w_15 w_666) 1) ( <= ( - w_15 w_666) ( ~ 1))) |
---|
| 393 | ( or ( not v_15_8 ) ( not v_666_8 ) ( >= ( - w_15 w_666) 1) ( <= ( - w_15 w_666) ( ~ 1))) |
---|
| 394 | ( or ( not v_15_2 ) ( not v_767_2 ) ( >= ( - w_15 w_767) 5) ( <= ( - w_15 w_767) ( ~ 5))) |
---|
| 395 | ( or ( not v_15_2 ) ( not v_767_8 ) ( >= ( - w_15 w_767) 5) ( <= ( - w_15 w_767) ( ~ 4))) |
---|
| 396 | ( or ( not v_15_8 ) ( not v_767_2 ) ( >= ( - w_15 w_767) 4) ( <= ( - w_15 w_767) ( ~ 5))) |
---|
| 397 | ( or ( not v_15_8 ) ( not v_767_8 ) ( >= ( - w_15 w_767) 5) ( <= ( - w_15 w_767) ( ~ 5))) |
---|
| 398 | ( or ( not v_15_2 ) ( not v_768_2 ) ( >= ( - w_15 w_768) 17) ( <= ( - w_15 w_768) ( ~ 17))) |
---|
| 399 | ( or ( not v_15_2 ) ( not v_768_8 ) ( >= ( - w_15 w_768) 18) ( <= ( - w_15 w_768) ( ~ 17))) |
---|
| 400 | ( or ( not v_15_8 ) ( not v_768_2 ) ( >= ( - w_15 w_768) 17) ( <= ( - w_15 w_768) ( ~ 18))) |
---|
| 401 | ( or ( not v_15_8 ) ( not v_768_8 ) ( >= ( - w_15 w_768) 17) ( <= ( - w_15 w_768) ( ~ 17))) |
---|
| 402 | ( or ( not v_16_2 ) ( not v_321_2 ) ( >= ( - w_16 w_321) 12) ( <= ( - w_16 w_321) ( ~ 12))) |
---|
| 403 | ( or ( not v_16_2 ) ( not v_321_8 ) ( >= ( - w_16 w_321) 13) ( <= ( - w_16 w_321) ( ~ 12))) |
---|
| 404 | ( or ( not v_16_8 ) ( not v_321_2 ) ( >= ( - w_16 w_321) 12) ( <= ( - w_16 w_321) ( ~ 13))) |
---|
| 405 | ( or ( not v_16_8 ) ( not v_321_8 ) ( >= ( - w_16 w_321) 12) ( <= ( - w_16 w_321) ( ~ 12))) |
---|
| 406 | ( or ( not v_16_2 ) ( not v_322_2 ) ( >= ( - w_16 w_322) 1) ( <= ( - w_16 w_322) ( ~ 1))) |
---|
| 407 | ( or ( not v_16_2 ) ( not v_322_8 ) ( >= ( - w_16 w_322) 2) ( <= ( - w_16 w_322) ( ~ 1))) |
---|
| 408 | ( or ( not v_16_8 ) ( not v_322_2 ) ( >= ( - w_16 w_322) 1) ( <= ( - w_16 w_322) ( ~ 2))) |
---|
| 409 | ( or ( not v_16_8 ) ( not v_322_8 ) ( >= ( - w_16 w_322) 1) ( <= ( - w_16 w_322) ( ~ 1))) |
---|
| 410 | ( or ( not v_16_2 ) ( not v_323_2 ) ( >= ( - w_16 w_323) 4) ( <= ( - w_16 w_323) ( ~ 4))) |
---|
| 411 | ( or ( not v_16_2 ) ( not v_323_8 ) ( >= ( - w_16 w_323) 5) ( <= ( - w_16 w_323) ( ~ 4))) |
---|
| 412 | ( or ( not v_16_8 ) ( not v_323_2 ) ( >= ( - w_16 w_323) 4) ( <= ( - w_16 w_323) ( ~ 5))) |
---|
| 413 | ( or ( not v_16_8 ) ( not v_323_8 ) ( >= ( - w_16 w_323) 4) ( <= ( - w_16 w_323) ( ~ 4))) |
---|
| 414 | ( or ( not v_16_2 ) ( not v_324_2 ) ( >= ( - w_16 w_324) 11) ( <= ( - w_16 w_324) ( ~ 11))) |
---|
| 415 | ( or ( not v_16_2 ) ( not v_324_8 ) ( >= ( - w_16 w_324) 12) ( <= ( - w_16 w_324) ( ~ 11))) |
---|
| 416 | ( or ( not v_16_8 ) ( not v_324_2 ) ( >= ( - w_16 w_324) 11) ( <= ( - w_16 w_324) ( ~ 12))) |
---|
| 417 | ( or ( not v_16_8 ) ( not v_324_8 ) ( >= ( - w_16 w_324) 11) ( <= ( - w_16 w_324) ( ~ 11))) |
---|
| 418 | ( or ( not v_16_2 ) ( not v_557_2 ) ( >= ( - w_16 w_557) 19) ( <= ( - w_16 w_557) ( ~ 19))) |
---|
| 419 | ( or ( not v_16_2 ) ( not v_557_8 ) ( >= ( - w_16 w_557) 20) ( <= ( - w_16 w_557) ( ~ 19))) |
---|
| 420 | ( or ( not v_16_8 ) ( not v_557_2 ) ( >= ( - w_16 w_557) 19) ( <= ( - w_16 w_557) ( ~ 20))) |
---|
| 421 | ( or ( not v_16_8 ) ( not v_557_8 ) ( >= ( - w_16 w_557) 19) ( <= ( - w_16 w_557) ( ~ 19))) |
---|
| 422 | ( or ( not v_16_2 ) ( not v_558_2 ) ( >= ( - w_16 w_558) 30) ( <= ( - w_16 w_558) ( ~ 30))) |
---|
| 423 | ( or ( not v_16_2 ) ( not v_558_8 ) ( >= ( - w_16 w_558) 30) ( <= ( - w_16 w_558) ( ~ 29))) |
---|
| 424 | ( or ( not v_16_8 ) ( not v_558_2 ) ( >= ( - w_16 w_558) 29) ( <= ( - w_16 w_558) ( ~ 30))) |
---|
| 425 | ( or ( not v_16_8 ) ( not v_558_8 ) ( >= ( - w_16 w_558) 30) ( <= ( - w_16 w_558) ( ~ 30))) |
---|
| 426 | ( or ( not v_16_2 ) ( not v_599_2 ) ( >= ( - w_16 w_599) 15) ( <= ( - w_16 w_599) ( ~ 15))) |
---|
| 427 | ( or ( not v_16_2 ) ( not v_599_8 ) ( >= ( - w_16 w_599) 15) ( <= ( - w_16 w_599) ( ~ 14))) |
---|
| 428 | ( or ( not v_16_8 ) ( not v_599_2 ) ( >= ( - w_16 w_599) 14) ( <= ( - w_16 w_599) ( ~ 15))) |
---|
| 429 | ( or ( not v_16_8 ) ( not v_599_8 ) ( >= ( - w_16 w_599) 15) ( <= ( - w_16 w_599) ( ~ 15))) |
---|
| 430 | ( or ( not v_16_2 ) ( not v_600_2 ) ( >= ( - w_16 w_600) 25) ( <= ( - w_16 w_600) ( ~ 25))) |
---|
| 431 | ( or ( not v_16_2 ) ( not v_600_8 ) ( >= ( - w_16 w_600) 25) ( <= ( - w_16 w_600) ( ~ 25))) |
---|
| 432 | ( or ( not v_16_8 ) ( not v_600_2 ) ( >= ( - w_16 w_600) 25) ( <= ( - w_16 w_600) ( ~ 25))) |
---|
| 433 | ( or ( not v_16_8 ) ( not v_600_8 ) ( >= ( - w_16 w_600) 25) ( <= ( - w_16 w_600) ( ~ 25))) |
---|
| 434 | ( or ( not v_16_2 ) ( not v_665_2 ) ( >= ( - w_16 w_665) 1) ( <= ( - w_16 w_665) ( ~ 1))) |
---|
| 435 | ( or ( not v_16_2 ) ( not v_665_8 ) ( >= ( - w_16 w_665) 1) ( <= ( - w_16 w_665) ( ~ 1))) |
---|
| 436 | ( or ( not v_16_8 ) ( not v_665_2 ) ( >= ( - w_16 w_665) 1) ( <= ( - w_16 w_665) ( ~ 1))) |
---|
| 437 | ( or ( not v_16_8 ) ( not v_665_8 ) ( >= ( - w_16 w_665) 1) ( <= ( - w_16 w_665) ( ~ 1))) |
---|
| 438 | ( or ( not v_16_2 ) ( not v_666_2 ) ( >= ( - w_16 w_666) 13) ( <= ( - w_16 w_666) ( ~ 13))) |
---|
| 439 | ( or ( not v_16_2 ) ( not v_666_8 ) ( >= ( - w_16 w_666) 14) ( <= ( - w_16 w_666) ( ~ 13))) |
---|
| 440 | ( or ( not v_16_8 ) ( not v_666_2 ) ( >= ( - w_16 w_666) 13) ( <= ( - w_16 w_666) ( ~ 14))) |
---|
| 441 | ( or ( not v_16_8 ) ( not v_666_8 ) ( >= ( - w_16 w_666) 13) ( <= ( - w_16 w_666) ( ~ 13))) |
---|
| 442 | ( or ( not v_16_2 ) ( not v_767_2 ) ( >= ( - w_16 w_767) 9) ( <= ( - w_16 w_767) ( ~ 9))) |
---|
| 443 | ( or ( not v_16_2 ) ( not v_767_8 ) ( >= ( - w_16 w_767) 10) ( <= ( - w_16 w_767) ( ~ 9))) |
---|
| 444 | ( or ( not v_16_8 ) ( not v_767_2 ) ( >= ( - w_16 w_767) 9) ( <= ( - w_16 w_767) ( ~ 10))) |
---|
| 445 | ( or ( not v_16_8 ) ( not v_767_8 ) ( >= ( - w_16 w_767) 9) ( <= ( - w_16 w_767) ( ~ 9))) |
---|
| 446 | ( or ( not v_16_2 ) ( not v_768_2 ) ( >= ( - w_16 w_768) 5) ( <= ( - w_16 w_768) ( ~ 5))) |
---|
| 447 | ( or ( not v_16_2 ) ( not v_768_8 ) ( >= ( - w_16 w_768) 5) ( <= ( - w_16 w_768) ( ~ 4))) |
---|
| 448 | ( or ( not v_16_8 ) ( not v_768_2 ) ( >= ( - w_16 w_768) 4) ( <= ( - w_16 w_768) ( ~ 5))) |
---|
| 449 | ( or ( not v_16_8 ) ( not v_768_8 ) ( >= ( - w_16 w_768) 5) ( <= ( - w_16 w_768) ( ~ 5))) |
---|
| 450 | ( or ( not v_321_2 ) ( not v_322_2 ) ( = ( - w_321 w_322) 17) ( = ( - w_322 w_321) 17)) |
---|
| 451 | ( or ( not v_321_2 ) ( not v_322_8 )) |
---|
| 452 | ( or ( not v_321_8 ) ( not v_322_2 )) |
---|
| 453 | ( or ( not v_321_8 ) ( not v_322_8 ) ( = ( - w_321 w_322) 17) ( = ( - w_322 w_321) 17)) |
---|
| 454 | ( or ( not v_321_2 ) ( not v_323_2 ) ( >= ( - w_321 w_323) 13) ( <= ( - w_321 w_323) ( ~ 13))) |
---|
| 455 | ( or ( not v_321_2 ) ( not v_323_8 ) ( >= ( - w_321 w_323) 14) ( <= ( - w_321 w_323) ( ~ 13))) |
---|
| 456 | ( or ( not v_321_8 ) ( not v_323_2 ) ( >= ( - w_321 w_323) 13) ( <= ( - w_321 w_323) ( ~ 14))) |
---|
| 457 | ( or ( not v_321_8 ) ( not v_323_8 ) ( >= ( - w_321 w_323) 13) ( <= ( - w_321 w_323) ( ~ 13))) |
---|
| 458 | ( or ( not v_321_2 ) ( not v_324_2 ) ( >= ( - w_321 w_324) 6) ( <= ( - w_321 w_324) ( ~ 6))) |
---|
| 459 | ( or ( not v_321_2 ) ( not v_324_8 ) ( >= ( - w_321 w_324) 7) ( <= ( - w_321 w_324) ( ~ 6))) |
---|
| 460 | ( or ( not v_321_8 ) ( not v_324_2 ) ( >= ( - w_321 w_324) 6) ( <= ( - w_321 w_324) ( ~ 7))) |
---|
| 461 | ( or ( not v_321_8 ) ( not v_324_8 ) ( >= ( - w_321 w_324) 6) ( <= ( - w_321 w_324) ( ~ 6))) |
---|
| 462 | ( or ( not v_321_2 ) ( not v_557_2 ) ( >= ( - w_321 w_557) 8) ( <= ( - w_321 w_557) ( ~ 8))) |
---|
| 463 | ( or ( not v_321_2 ) ( not v_557_8 ) ( >= ( - w_321 w_557) 8) ( <= ( - w_321 w_557) ( ~ 7))) |
---|
| 464 | ( or ( not v_321_8 ) ( not v_557_2 ) ( >= ( - w_321 w_557) 7) ( <= ( - w_321 w_557) ( ~ 8))) |
---|
| 465 | ( or ( not v_321_8 ) ( not v_557_8 ) ( >= ( - w_321 w_557) 8) ( <= ( - w_321 w_557) ( ~ 8))) |
---|
| 466 | ( or ( not v_321_2 ) ( not v_558_2 ) ( >= ( - w_321 w_558) 20) ( <= ( - w_321 w_558) ( ~ 20))) |
---|
| 467 | ( or ( not v_321_2 ) ( not v_558_8 ) ( >= ( - w_321 w_558) 20) ( <= ( - w_321 w_558) ( ~ 20))) |
---|
| 468 | ( or ( not v_321_8 ) ( not v_558_2 ) ( >= ( - w_321 w_558) 20) ( <= ( - w_321 w_558) ( ~ 20))) |
---|
| 469 | ( or ( not v_321_8 ) ( not v_558_8 ) ( >= ( - w_321 w_558) 20) ( <= ( - w_321 w_558) ( ~ 20))) |
---|
| 470 | ( or ( not v_321_2 ) ( not v_594_2 ) ( >= ( - w_321 w_594) 16) ( <= ( - w_321 w_594) ( ~ 16))) |
---|
| 471 | ( or ( not v_321_2 ) ( not v_594_8 ) ( >= ( - w_321 w_594) 16) ( <= ( - w_321 w_594) ( ~ 15))) |
---|
| 472 | ( or ( not v_321_8 ) ( not v_594_2 ) ( >= ( - w_321 w_594) 15) ( <= ( - w_321 w_594) ( ~ 16))) |
---|
| 473 | ( or ( not v_321_8 ) ( not v_594_8 ) ( >= ( - w_321 w_594) 16) ( <= ( - w_321 w_594) ( ~ 16))) |
---|
| 474 | ( or ( not v_321_2 ) ( not v_599_2 ) ( >= ( - w_321 w_599) 3) ( <= ( - w_321 w_599) ( ~ 3))) |
---|
| 475 | ( or ( not v_321_2 ) ( not v_599_8 ) ( >= ( - w_321 w_599) 3) ( <= ( - w_321 w_599) ( ~ 2))) |
---|
| 476 | ( or ( not v_321_8 ) ( not v_599_2 ) ( >= ( - w_321 w_599) 2) ( <= ( - w_321 w_599) ( ~ 3))) |
---|
| 477 | ( or ( not v_321_8 ) ( not v_599_8 ) ( >= ( - w_321 w_599) 3) ( <= ( - w_321 w_599) ( ~ 3))) |
---|
| 478 | ( or ( not v_321_2 ) ( not v_600_2 ) ( >= ( - w_321 w_600) 15) ( <= ( - w_321 w_600) ( ~ 15))) |
---|
| 479 | ( or ( not v_321_2 ) ( not v_600_8 ) ( >= ( - w_321 w_600) 16) ( <= ( - w_321 w_600) ( ~ 15))) |
---|
| 480 | ( or ( not v_321_8 ) ( not v_600_2 ) ( >= ( - w_321 w_600) 15) ( <= ( - w_321 w_600) ( ~ 16))) |
---|
| 481 | ( or ( not v_321_8 ) ( not v_600_8 ) ( >= ( - w_321 w_600) 15) ( <= ( - w_321 w_600) ( ~ 15))) |
---|
| 482 | ( or ( not v_321_2 ) ( not v_631_2 ) ( >= ( - w_321 w_631) 14) ( <= ( - w_321 w_631) ( ~ 14))) |
---|
| 483 | ( or ( not v_321_2 ) ( not v_631_8 ) ( >= ( - w_321 w_631) 15) ( <= ( - w_321 w_631) ( ~ 14))) |
---|
| 484 | ( or ( not v_321_8 ) ( not v_631_2 ) ( >= ( - w_321 w_631) 14) ( <= ( - w_321 w_631) ( ~ 15))) |
---|
| 485 | ( or ( not v_321_8 ) ( not v_631_8 ) ( >= ( - w_321 w_631) 14) ( <= ( - w_321 w_631) ( ~ 14))) |
---|
| 486 | ( or ( not v_321_2 ) ( not v_665_2 ) ( >= ( - w_321 w_665) 12) ( <= ( - w_321 w_665) ( ~ 12))) |
---|
| 487 | ( or ( not v_321_2 ) ( not v_665_8 ) ( >= ( - w_321 w_665) 13) ( <= ( - w_321 w_665) ( ~ 12))) |
---|
| 488 | ( or ( not v_321_8 ) ( not v_665_2 ) ( >= ( - w_321 w_665) 12) ( <= ( - w_321 w_665) ( ~ 13))) |
---|
| 489 | ( or ( not v_321_8 ) ( not v_665_8 ) ( >= ( - w_321 w_665) 12) ( <= ( - w_321 w_665) ( ~ 12))) |
---|
| 490 | ( or ( not v_321_2 ) ( not v_666_2 ) ( >= ( - w_321 w_666) 1) ( <= ( - w_321 w_666) ( ~ 1))) |
---|
| 491 | ( or ( not v_321_2 ) ( not v_666_8 ) ( >= ( - w_321 w_666) 2) ( <= ( - w_321 w_666) ( ~ 1))) |
---|
| 492 | ( or ( not v_321_8 ) ( not v_666_2 ) ( >= ( - w_321 w_666) 1) ( <= ( - w_321 w_666) ( ~ 2))) |
---|
| 493 | ( or ( not v_321_8 ) ( not v_666_8 ) ( >= ( - w_321 w_666) 1) ( <= ( - w_321 w_666) ( ~ 1))) |
---|
| 494 | ( or ( not v_321_2 ) ( not v_767_2 ) ( >= ( - w_321 w_767) 5) ( <= ( - w_321 w_767) ( ~ 5))) |
---|
| 495 | ( or ( not v_321_2 ) ( not v_767_8 ) ( >= ( - w_321 w_767) 5) ( <= ( - w_321 w_767) ( ~ 4))) |
---|
| 496 | ( or ( not v_321_8 ) ( not v_767_2 ) ( >= ( - w_321 w_767) 4) ( <= ( - w_321 w_767) ( ~ 5))) |
---|
| 497 | ( or ( not v_321_8 ) ( not v_767_8 ) ( >= ( - w_321 w_767) 5) ( <= ( - w_321 w_767) ( ~ 5))) |
---|
| 498 | ( or ( not v_321_2 ) ( not v_768_2 ) ( >= ( - w_321 w_768) 16) ( <= ( - w_321 w_768) ( ~ 16))) |
---|
| 499 | ( or ( not v_321_2 ) ( not v_768_8 ) ( >= ( - w_321 w_768) 17) ( <= ( - w_321 w_768) ( ~ 16))) |
---|
| 500 | ( or ( not v_321_8 ) ( not v_768_2 ) ( >= ( - w_321 w_768) 16) ( <= ( - w_321 w_768) ( ~ 17))) |
---|
| 501 | ( or ( not v_321_8 ) ( not v_768_8 ) ( >= ( - w_321 w_768) 16) ( <= ( - w_321 w_768) ( ~ 16))) |
---|
| 502 | ( or ( not v_322_2 ) ( not v_323_2 ) ( >= ( - w_322 w_323) 6) ( <= ( - w_322 w_323) ( ~ 6))) |
---|
| 503 | ( or ( not v_322_2 ) ( not v_323_8 ) ( >= ( - w_322 w_323) 7) ( <= ( - w_322 w_323) ( ~ 6))) |
---|
| 504 | ( or ( not v_322_8 ) ( not v_323_2 ) ( >= ( - w_322 w_323) 6) ( <= ( - w_322 w_323) ( ~ 7))) |
---|
| 505 | ( or ( not v_322_8 ) ( not v_323_8 ) ( >= ( - w_322 w_323) 6) ( <= ( - w_322 w_323) ( ~ 6))) |
---|
| 506 | ( or ( not v_322_2 ) ( not v_324_2 ) ( >= ( - w_322 w_324) 13) ( <= ( - w_322 w_324) ( ~ 13))) |
---|
| 507 | ( or ( not v_322_2 ) ( not v_324_8 ) ( >= ( - w_322 w_324) 14) ( <= ( - w_322 w_324) ( ~ 13))) |
---|
| 508 | ( or ( not v_322_8 ) ( not v_324_2 ) ( >= ( - w_322 w_324) 13) ( <= ( - w_322 w_324) ( ~ 14))) |
---|
| 509 | ( or ( not v_322_8 ) ( not v_324_8 ) ( >= ( - w_322 w_324) 13) ( <= ( - w_322 w_324) ( ~ 13))) |
---|
| 510 | ( or ( not v_322_2 ) ( not v_557_2 ) ( >= ( - w_322 w_557) 20) ( <= ( - w_322 w_557) ( ~ 20))) |
---|
| 511 | ( or ( not v_322_2 ) ( not v_557_8 ) ( >= ( - w_322 w_557) 20) ( <= ( - w_322 w_557) ( ~ 20))) |
---|
| 512 | ( or ( not v_322_8 ) ( not v_557_2 ) ( >= ( - w_322 w_557) 20) ( <= ( - w_322 w_557) ( ~ 20))) |
---|
| 513 | ( or ( not v_322_8 ) ( not v_557_8 ) ( >= ( - w_322 w_557) 20) ( <= ( - w_322 w_557) ( ~ 20))) |
---|
| 514 | ( or ( not v_322_2 ) ( not v_558_2 ) ( >= ( - w_322 w_558) 30) ( <= ( - w_322 w_558) ( ~ 30))) |
---|
| 515 | ( or ( not v_322_2 ) ( not v_558_8 ) ( >= ( - w_322 w_558) 31) ( <= ( - w_322 w_558) ( ~ 30))) |
---|
| 516 | ( or ( not v_322_8 ) ( not v_558_2 ) ( >= ( - w_322 w_558) 30) ( <= ( - w_322 w_558) ( ~ 31))) |
---|
| 517 | ( or ( not v_322_8 ) ( not v_558_8 ) ( >= ( - w_322 w_558) 30) ( <= ( - w_322 w_558) ( ~ 30))) |
---|
| 518 | ( or ( not v_322_2 ) ( not v_599_2 ) ( >= ( - w_322 w_599) 15) ( <= ( - w_322 w_599) ( ~ 15))) |
---|
| 519 | ( or ( not v_322_2 ) ( not v_599_8 ) ( >= ( - w_322 w_599) 16) ( <= ( - w_322 w_599) ( ~ 15))) |
---|
| 520 | ( or ( not v_322_8 ) ( not v_599_2 ) ( >= ( - w_322 w_599) 15) ( <= ( - w_322 w_599) ( ~ 16))) |
---|
| 521 | ( or ( not v_322_8 ) ( not v_599_8 ) ( >= ( - w_322 w_599) 15) ( <= ( - w_322 w_599) ( ~ 15))) |
---|
| 522 | ( or ( not v_322_2 ) ( not v_600_2 ) ( >= ( - w_322 w_600) 26) ( <= ( - w_322 w_600) ( ~ 26))) |
---|
| 523 | ( or ( not v_322_2 ) ( not v_600_8 ) ( >= ( - w_322 w_600) 26) ( <= ( - w_322 w_600) ( ~ 25))) |
---|
| 524 | ( or ( not v_322_8 ) ( not v_600_2 ) ( >= ( - w_322 w_600) 25) ( <= ( - w_322 w_600) ( ~ 26))) |
---|
| 525 | ( or ( not v_322_8 ) ( not v_600_8 ) ( >= ( - w_322 w_600) 26) ( <= ( - w_322 w_600) ( ~ 26))) |
---|
| 526 | ( or ( not v_322_2 ) ( not v_665_2 ) ( >= ( - w_322 w_665) 1) ( <= ( - w_322 w_665) ( ~ 1))) |
---|
| 527 | ( or ( not v_322_2 ) ( not v_665_8 ) ( >= ( - w_322 w_665) 2) ( <= ( - w_322 w_665) ( ~ 1))) |
---|
| 528 | ( or ( not v_322_8 ) ( not v_665_2 ) ( >= ( - w_322 w_665) 1) ( <= ( - w_322 w_665) ( ~ 2))) |
---|
| 529 | ( or ( not v_322_8 ) ( not v_665_8 ) ( >= ( - w_322 w_665) 1) ( <= ( - w_322 w_665) ( ~ 1))) |
---|
| 530 | ( or ( not v_322_2 ) ( not v_666_2 ) ( >= ( - w_322 w_666) 14) ( <= ( - w_322 w_666) ( ~ 14))) |
---|
| 531 | ( or ( not v_322_2 ) ( not v_666_8 ) ( >= ( - w_322 w_666) 14) ( <= ( - w_322 w_666) ( ~ 13))) |
---|
| 532 | ( or ( not v_322_8 ) ( not v_666_2 ) ( >= ( - w_322 w_666) 13) ( <= ( - w_322 w_666) ( ~ 14))) |
---|
| 533 | ( or ( not v_322_8 ) ( not v_666_8 ) ( >= ( - w_322 w_666) 14) ( <= ( - w_322 w_666) ( ~ 14))) |
---|
| 534 | ( or ( not v_322_2 ) ( not v_767_2 ) ( >= ( - w_322 w_767) 10) ( <= ( - w_322 w_767) ( ~ 10))) |
---|
| 535 | ( or ( not v_322_2 ) ( not v_767_8 ) ( >= ( - w_322 w_767) 10) ( <= ( - w_322 w_767) ( ~ 9))) |
---|
| 536 | ( or ( not v_322_8 ) ( not v_767_2 ) ( >= ( - w_322 w_767) 9) ( <= ( - w_322 w_767) ( ~ 10))) |
---|
| 537 | ( or ( not v_322_8 ) ( not v_767_8 ) ( >= ( - w_322 w_767) 10) ( <= ( - w_322 w_767) ( ~ 10))) |
---|
| 538 | ( or ( not v_322_2 ) ( not v_768_2 ) ( >= ( - w_322 w_768) 4) ( <= ( - w_322 w_768) ( ~ 4))) |
---|
| 539 | ( or ( not v_322_2 ) ( not v_768_8 ) ( >= ( - w_322 w_768) 5) ( <= ( - w_322 w_768) ( ~ 4))) |
---|
| 540 | ( or ( not v_322_8 ) ( not v_768_2 ) ( >= ( - w_322 w_768) 4) ( <= ( - w_322 w_768) ( ~ 5))) |
---|
| 541 | ( or ( not v_322_8 ) ( not v_768_8 ) ( >= ( - w_322 w_768) 4) ( <= ( - w_322 w_768) ( ~ 4))) |
---|
| 542 | ( or ( not v_323_2 ) ( not v_324_2 ) ( = ( - w_323 w_324) 17) ( = ( - w_324 w_323) 17)) |
---|
| 543 | ( or ( not v_323_2 ) ( not v_324_8 )) |
---|
| 544 | ( or ( not v_323_8 ) ( not v_324_2 )) |
---|
| 545 | ( or ( not v_323_8 ) ( not v_324_8 ) ( = ( - w_323 w_324) 17) ( = ( - w_324 w_323) 17)) |
---|
| 546 | ( or ( not v_323_2 ) ( not v_557_2 ) ( >= ( - w_323 w_557) 19) ( <= ( - w_323 w_557) ( ~ 19))) |
---|
| 547 | ( or ( not v_323_2 ) ( not v_557_8 ) ( >= ( - w_323 w_557) 19) ( <= ( - w_323 w_557) ( ~ 18))) |
---|
| 548 | ( or ( not v_323_8 ) ( not v_557_2 ) ( >= ( - w_323 w_557) 18) ( <= ( - w_323 w_557) ( ~ 19))) |
---|
| 549 | ( or ( not v_323_8 ) ( not v_557_8 ) ( >= ( - w_323 w_557) 19) ( <= ( - w_323 w_557) ( ~ 19))) |
---|
| 550 | ( or ( not v_323_2 ) ( not v_558_2 ) ( >= ( - w_323 w_558) 31) ( <= ( - w_323 w_558) ( ~ 31))) |
---|
| 551 | ( or ( not v_323_2 ) ( not v_558_8 ) ( >= ( - w_323 w_558) 32) ( <= ( - w_323 w_558) ( ~ 31))) |
---|
| 552 | ( or ( not v_323_8 ) ( not v_558_2 ) ( >= ( - w_323 w_558) 31) ( <= ( - w_323 w_558) ( ~ 32))) |
---|
| 553 | ( or ( not v_323_8 ) ( not v_558_8 ) ( >= ( - w_323 w_558) 31) ( <= ( - w_323 w_558) ( ~ 31))) |
---|
| 554 | ( or ( not v_323_2 ) ( not v_594_2 ) ( >= ( - w_323 w_594) 5) ( <= ( - w_323 w_594) ( ~ 5))) |
---|
| 555 | ( or ( not v_323_2 ) ( not v_594_8 ) ( >= ( - w_323 w_594) 5) ( <= ( - w_323 w_594) ( ~ 4))) |
---|
| 556 | ( or ( not v_323_8 ) ( not v_594_2 ) ( >= ( - w_323 w_594) 4) ( <= ( - w_323 w_594) ( ~ 5))) |
---|
| 557 | ( or ( not v_323_8 ) ( not v_594_8 ) ( >= ( - w_323 w_594) 5) ( <= ( - w_323 w_594) ( ~ 5))) |
---|
| 558 | ( or ( not v_323_2 ) ( not v_599_2 ) ( >= ( - w_323 w_599) 14) ( <= ( - w_323 w_599) ( ~ 14))) |
---|
| 559 | ( or ( not v_323_2 ) ( not v_599_8 ) ( >= ( - w_323 w_599) 15) ( <= ( - w_323 w_599) ( ~ 14))) |
---|
| 560 | ( or ( not v_323_8 ) ( not v_599_2 ) ( >= ( - w_323 w_599) 14) ( <= ( - w_323 w_599) ( ~ 15))) |
---|
| 561 | ( or ( not v_323_8 ) ( not v_599_8 ) ( >= ( - w_323 w_599) 14) ( <= ( - w_323 w_599) ( ~ 14))) |
---|
| 562 | ( or ( not v_323_2 ) ( not v_600_2 ) ( >= ( - w_323 w_600) 27) ( <= ( - w_323 w_600) ( ~ 27))) |
---|
| 563 | ( or ( not v_323_2 ) ( not v_600_8 ) ( >= ( - w_323 w_600) 27) ( <= ( - w_323 w_600) ( ~ 26))) |
---|
| 564 | ( or ( not v_323_8 ) ( not v_600_2 ) ( >= ( - w_323 w_600) 26) ( <= ( - w_323 w_600) ( ~ 27))) |
---|
| 565 | ( or ( not v_323_8 ) ( not v_600_8 ) ( >= ( - w_323 w_600) 27) ( <= ( - w_323 w_600) ( ~ 27))) |
---|
| 566 | ( or ( not v_323_2 ) ( not v_631_2 ) ( >= ( - w_323 w_631) 26) ( <= ( - w_323 w_631) ( ~ 26))) |
---|
| 567 | ( or ( not v_323_2 ) ( not v_631_8 ) ( >= ( - w_323 w_631) 26) ( <= ( - w_323 w_631) ( ~ 25))) |
---|
| 568 | ( or ( not v_323_8 ) ( not v_631_2 ) ( >= ( - w_323 w_631) 25) ( <= ( - w_323 w_631) ( ~ 26))) |
---|
| 569 | ( or ( not v_323_8 ) ( not v_631_8 ) ( >= ( - w_323 w_631) 26) ( <= ( - w_323 w_631) ( ~ 26))) |
---|
| 570 | ( or ( not v_323_2 ) ( not v_665_2 ) ( >= ( - w_323 w_665) 4) ( <= ( - w_323 w_665) ( ~ 4))) |
---|
| 571 | ( or ( not v_323_2 ) ( not v_665_8 ) ( >= ( - w_323 w_665) 5) ( <= ( - w_323 w_665) ( ~ 4))) |
---|
| 572 | ( or ( not v_323_8 ) ( not v_665_2 ) ( >= ( - w_323 w_665) 4) ( <= ( - w_323 w_665) ( ~ 5))) |
---|
| 573 | ( or ( not v_323_8 ) ( not v_665_8 ) ( >= ( - w_323 w_665) 4) ( <= ( - w_323 w_665) ( ~ 4))) |
---|
| 574 | ( or ( not v_323_2 ) ( not v_666_2 ) ( >= ( - w_323 w_666) 13) ( <= ( - w_323 w_666) ( ~ 13))) |
---|
| 575 | ( or ( not v_323_2 ) ( not v_666_8 ) ( >= ( - w_323 w_666) 13) ( <= ( - w_323 w_666) ( ~ 12))) |
---|
| 576 | ( or ( not v_323_8 ) ( not v_666_2 ) ( >= ( - w_323 w_666) 12) ( <= ( - w_323 w_666) ( ~ 13))) |
---|
| 577 | ( or ( not v_323_8 ) ( not v_666_8 ) ( >= ( - w_323 w_666) 13) ( <= ( - w_323 w_666) ( ~ 13))) |
---|
| 578 | ( or ( not v_323_2 ) ( not v_767_2 ) ( >= ( - w_323 w_767) 9) ( <= ( - w_323 w_767) ( ~ 9))) |
---|
| 579 | ( or ( not v_323_2 ) ( not v_767_8 ) ( >= ( - w_323 w_767) 10) ( <= ( - w_323 w_767) ( ~ 9))) |
---|
| 580 | ( or ( not v_323_8 ) ( not v_767_2 ) ( >= ( - w_323 w_767) 9) ( <= ( - w_323 w_767) ( ~ 10))) |
---|
| 581 | ( or ( not v_323_8 ) ( not v_767_8 ) ( >= ( - w_323 w_767) 9) ( <= ( - w_323 w_767) ( ~ 9))) |
---|
| 582 | ( or ( not v_323_2 ) ( not v_768_2 ) ( >= ( - w_323 w_768) 5) ( <= ( - w_323 w_768) ( ~ 5))) |
---|
| 583 | ( or ( not v_323_2 ) ( not v_768_8 ) ( >= ( - w_323 w_768) 6) ( <= ( - w_323 w_768) ( ~ 5))) |
---|
| 584 | ( or ( not v_323_8 ) ( not v_768_2 ) ( >= ( - w_323 w_768) 5) ( <= ( - w_323 w_768) ( ~ 6))) |
---|
| 585 | ( or ( not v_323_8 ) ( not v_768_8 ) ( >= ( - w_323 w_768) 5) ( <= ( - w_323 w_768) ( ~ 5))) |
---|
| 586 | ( or ( not v_324_2 ) ( not v_557_2 ) ( >= ( - w_324 w_557) 9) ( <= ( - w_324 w_557) ( ~ 9))) |
---|
| 587 | ( or ( not v_324_2 ) ( not v_557_8 ) ( >= ( - w_324 w_557) 9) ( <= ( - w_324 w_557) ( ~ 8))) |
---|
| 588 | ( or ( not v_324_8 ) ( not v_557_2 ) ( >= ( - w_324 w_557) 8) ( <= ( - w_324 w_557) ( ~ 9))) |
---|
| 589 | ( or ( not v_324_8 ) ( not v_557_8 ) ( >= ( - w_324 w_557) 9) ( <= ( - w_324 w_557) ( ~ 9))) |
---|
| 590 | ( or ( not v_324_2 ) ( not v_558_2 ) ( >= ( - w_324 w_558) 19) ( <= ( - w_324 w_558) ( ~ 19))) |
---|
| 591 | ( or ( not v_324_2 ) ( not v_558_8 ) ( >= ( - w_324 w_558) 19) ( <= ( - w_324 w_558) ( ~ 18))) |
---|
| 592 | ( or ( not v_324_8 ) ( not v_558_2 ) ( >= ( - w_324 w_558) 18) ( <= ( - w_324 w_558) ( ~ 19))) |
---|
| 593 | ( or ( not v_324_8 ) ( not v_558_8 ) ( >= ( - w_324 w_558) 19) ( <= ( - w_324 w_558) ( ~ 19))) |
---|
| 594 | ( or ( not v_324_2 ) ( not v_599_2 ) ( >= ( - w_324 w_599) 4) ( <= ( - w_324 w_599) ( ~ 4))) |
---|
| 595 | ( or ( not v_324_2 ) ( not v_599_8 ) ( >= ( - w_324 w_599) 5) ( <= ( - w_324 w_599) ( ~ 4))) |
---|
| 596 | ( or ( not v_324_8 ) ( not v_599_2 ) ( >= ( - w_324 w_599) 4) ( <= ( - w_324 w_599) ( ~ 5))) |
---|
| 597 | ( or ( not v_324_8 ) ( not v_599_8 ) ( >= ( - w_324 w_599) 4) ( <= ( - w_324 w_599) ( ~ 4))) |
---|
| 598 | ( or ( not v_324_2 ) ( not v_600_2 ) ( >= ( - w_324 w_600) 14) ( <= ( - w_324 w_600) ( ~ 14))) |
---|
| 599 | ( or ( not v_324_2 ) ( not v_600_8 ) ( >= ( - w_324 w_600) 15) ( <= ( - w_324 w_600) ( ~ 14))) |
---|
| 600 | ( or ( not v_324_8 ) ( not v_600_2 ) ( >= ( - w_324 w_600) 14) ( <= ( - w_324 w_600) ( ~ 15))) |
---|
| 601 | ( or ( not v_324_8 ) ( not v_600_8 ) ( >= ( - w_324 w_600) 14) ( <= ( - w_324 w_600) ( ~ 14))) |
---|
| 602 | ( or ( not v_324_2 ) ( not v_665_2 ) ( >= ( - w_324 w_665) 11) ( <= ( - w_324 w_665) ( ~ 11))) |
---|
| 603 | ( or ( not v_324_2 ) ( not v_665_8 ) ( >= ( - w_324 w_665) 12) ( <= ( - w_324 w_665) ( ~ 11))) |
---|
| 604 | ( or ( not v_324_8 ) ( not v_665_2 ) ( >= ( - w_324 w_665) 11) ( <= ( - w_324 w_665) ( ~ 12))) |
---|
| 605 | ( or ( not v_324_8 ) ( not v_665_8 ) ( >= ( - w_324 w_665) 11) ( <= ( - w_324 w_665) ( ~ 11))) |
---|
| 606 | ( or ( not v_324_2 ) ( not v_666_2 ) ( >= ( - w_324 w_666) 4) ( <= ( - w_324 w_666) ( ~ 4))) |
---|
| 607 | ( or ( not v_324_2 ) ( not v_666_8 ) ( >= ( - w_324 w_666) 5) ( <= ( - w_324 w_666) ( ~ 4))) |
---|
| 608 | ( or ( not v_324_8 ) ( not v_666_2 ) ( >= ( - w_324 w_666) 4) ( <= ( - w_324 w_666) ( ~ 5))) |
---|
| 609 | ( or ( not v_324_8 ) ( not v_666_8 ) ( >= ( - w_324 w_666) 4) ( <= ( - w_324 w_666) ( ~ 4))) |
---|
| 610 | ( or ( not v_324_2 ) ( not v_767_2 ) ( >= ( - w_324 w_767) 5) ( <= ( - w_324 w_767) ( ~ 5))) |
---|
| 611 | ( or ( not v_324_2 ) ( not v_767_8 ) ( >= ( - w_324 w_767) 6) ( <= ( - w_324 w_767) ( ~ 5))) |
---|
| 612 | ( or ( not v_324_8 ) ( not v_767_2 ) ( >= ( - w_324 w_767) 5) ( <= ( - w_324 w_767) ( ~ 6))) |
---|
| 613 | ( or ( not v_324_8 ) ( not v_767_8 ) ( >= ( - w_324 w_767) 5) ( <= ( - w_324 w_767) ( ~ 5))) |
---|
| 614 | ( or ( not v_324_2 ) ( not v_768_2 ) ( >= ( - w_324 w_768) 16) ( <= ( - w_324 w_768) ( ~ 16))) |
---|
| 615 | ( or ( not v_324_2 ) ( not v_768_8 ) ( >= ( - w_324 w_768) 16) ( <= ( - w_324 w_768) ( ~ 15))) |
---|
| 616 | ( or ( not v_324_8 ) ( not v_768_2 ) ( >= ( - w_324 w_768) 15) ( <= ( - w_324 w_768) ( ~ 16))) |
---|
| 617 | ( or ( not v_324_8 ) ( not v_768_8 ) ( >= ( - w_324 w_768) 16) ( <= ( - w_324 w_768) ( ~ 16))) |
---|
| 618 | ( or ( not v_519_2 ) ( not v_520_2 ) ( = ( - w_519 w_520) 17) ( = ( - w_520 w_519) 17)) |
---|
| 619 | ( or ( not v_519_2 ) ( not v_520_8 )) |
---|
| 620 | ( or ( not v_519_8 ) ( not v_520_2 )) |
---|
| 621 | ( or ( not v_519_8 ) ( not v_520_8 ) ( = ( - w_519 w_520) 17) ( = ( - w_520 w_519) 17)) |
---|
| 622 | ( or ( not v_519_2 ) ( not v_597_2 ) ( >= ( - w_519 w_597) 21) ( <= ( - w_519 w_597) ( ~ 21))) |
---|
| 623 | ( or ( not v_519_2 ) ( not v_597_8 ) ( >= ( - w_519 w_597) 22) ( <= ( - w_519 w_597) ( ~ 21))) |
---|
| 624 | ( or ( not v_519_8 ) ( not v_597_2 ) ( >= ( - w_519 w_597) 21) ( <= ( - w_519 w_597) ( ~ 22))) |
---|
| 625 | ( or ( not v_519_8 ) ( not v_597_8 ) ( >= ( - w_519 w_597) 21) ( <= ( - w_519 w_597) ( ~ 21))) |
---|
| 626 | ( or ( not v_519_2 ) ( not v_598_2 ) ( >= ( - w_519 w_598) 31) ( <= ( - w_519 w_598) ( ~ 31))) |
---|
| 627 | ( or ( not v_519_2 ) ( not v_598_8 ) ( >= ( - w_519 w_598) 32) ( <= ( - w_519 w_598) ( ~ 31))) |
---|
| 628 | ( or ( not v_519_8 ) ( not v_598_2 ) ( >= ( - w_519 w_598) 31) ( <= ( - w_519 w_598) ( ~ 32))) |
---|
| 629 | ( or ( not v_519_8 ) ( not v_598_8 ) ( >= ( - w_519 w_598) 31) ( <= ( - w_519 w_598) ( ~ 31))) |
---|
| 630 | ( or ( not v_520_2 ) ( not v_597_2 ) ( >= ( - w_520 w_597) 9) ( <= ( - w_520 w_597) ( ~ 9))) |
---|
| 631 | ( or ( not v_520_2 ) ( not v_597_8 ) ( >= ( - w_520 w_597) 9) ( <= ( - w_520 w_597) ( ~ 8))) |
---|
| 632 | ( or ( not v_520_8 ) ( not v_597_2 ) ( >= ( - w_520 w_597) 8) ( <= ( - w_520 w_597) ( ~ 9))) |
---|
| 633 | ( or ( not v_520_8 ) ( not v_597_8 ) ( >= ( - w_520 w_597) 9) ( <= ( - w_520 w_597) ( ~ 9))) |
---|
| 634 | ( or ( not v_520_2 ) ( not v_598_2 ) ( >= ( - w_520 w_598) 21) ( <= ( - w_520 w_598) ( ~ 21))) |
---|
| 635 | ( or ( not v_520_2 ) ( not v_598_8 ) ( >= ( - w_520 w_598) 22) ( <= ( - w_520 w_598) ( ~ 21))) |
---|
| 636 | ( or ( not v_520_8 ) ( not v_598_2 ) ( >= ( - w_520 w_598) 21) ( <= ( - w_520 w_598) ( ~ 22))) |
---|
| 637 | ( or ( not v_520_8 ) ( not v_598_8 ) ( >= ( - w_520 w_598) 21) ( <= ( - w_520 w_598) ( ~ 21))) |
---|
| 638 | ( or ( not v_557_2 ) ( not v_558_2 ) ( = ( - w_557 w_558) 17) ( = ( - w_558 w_557) 17)) |
---|
| 639 | ( or ( not v_557_2 ) ( not v_558_8 )) |
---|
| 640 | ( or ( not v_557_8 ) ( not v_558_2 )) |
---|
| 641 | ( or ( not v_557_8 ) ( not v_558_8 ) ( = ( - w_557 w_558) 17) ( = ( - w_558 w_557) 17)) |
---|
| 642 | ( or ( not v_557_2 ) ( not v_593_2 ) ( >= ( - w_557 w_593) 11) ( <= ( - w_557 w_593) ( ~ 11))) |
---|
| 643 | ( or ( not v_557_2 ) ( not v_593_8 ) ( >= ( - w_557 w_593) 12) ( <= ( - w_557 w_593) ( ~ 11))) |
---|
| 644 | ( or ( not v_557_8 ) ( not v_593_2 ) ( >= ( - w_557 w_593) 11) ( <= ( - w_557 w_593) ( ~ 12))) |
---|
| 645 | ( or ( not v_557_8 ) ( not v_593_8 ) ( >= ( - w_557 w_593) 11) ( <= ( - w_557 w_593) ( ~ 11))) |
---|
| 646 | ( or ( not v_557_2 ) ( not v_594_2 ) ( >= ( - w_557 w_594) 24) ( <= ( - w_557 w_594) ( ~ 24))) |
---|
| 647 | ( or ( not v_557_2 ) ( not v_594_8 ) ( >= ( - w_557 w_594) 24) ( <= ( - w_557 w_594) ( ~ 24))) |
---|
| 648 | ( or ( not v_557_8 ) ( not v_594_2 ) ( >= ( - w_557 w_594) 24) ( <= ( - w_557 w_594) ( ~ 24))) |
---|
| 649 | ( or ( not v_557_8 ) ( not v_594_8 ) ( >= ( - w_557 w_594) 24) ( <= ( - w_557 w_594) ( ~ 24))) |
---|
| 650 | ( or ( not v_557_2 ) ( not v_597_2 ) ( >= ( - w_557 w_597) 4) ( <= ( - w_557 w_597) ( ~ 4))) |
---|
| 651 | ( or ( not v_557_2 ) ( not v_597_8 ) ( >= ( - w_557 w_597) 4) ( <= ( - w_557 w_597) ( ~ 3))) |
---|
| 652 | ( or ( not v_557_8 ) ( not v_597_2 ) ( >= ( - w_557 w_597) 3) ( <= ( - w_557 w_597) ( ~ 4))) |
---|
| 653 | ( or ( not v_557_8 ) ( not v_597_8 ) ( >= ( - w_557 w_597) 4) ( <= ( - w_557 w_597) ( ~ 4))) |
---|
| 654 | ( or ( not v_557_2 ) ( not v_598_2 ) ( >= ( - w_557 w_598) 10) ( <= ( - w_557 w_598) ( ~ 10))) |
---|
| 655 | ( or ( not v_557_2 ) ( not v_598_8 ) ( >= ( - w_557 w_598) 10) ( <= ( - w_557 w_598) ( ~ 9))) |
---|
| 656 | ( or ( not v_557_8 ) ( not v_598_2 ) ( >= ( - w_557 w_598) 9) ( <= ( - w_557 w_598) ( ~ 10))) |
---|
| 657 | ( or ( not v_557_8 ) ( not v_598_8 ) ( >= ( - w_557 w_598) 10) ( <= ( - w_557 w_598) ( ~ 10))) |
---|
| 658 | ( or ( not v_557_2 ) ( not v_599_2 ) ( >= ( - w_557 w_599) 5) ( <= ( - w_557 w_599) ( ~ 5))) |
---|
| 659 | ( or ( not v_557_2 ) ( not v_599_8 ) ( >= ( - w_557 w_599) 6) ( <= ( - w_557 w_599) ( ~ 5))) |
---|
| 660 | ( or ( not v_557_8 ) ( not v_599_2 ) ( >= ( - w_557 w_599) 5) ( <= ( - w_557 w_599) ( ~ 6))) |
---|
| 661 | ( or ( not v_557_8 ) ( not v_599_8 ) ( >= ( - w_557 w_599) 5) ( <= ( - w_557 w_599) ( ~ 5))) |
---|
| 662 | ( or ( not v_557_2 ) ( not v_600_2 ) ( >= ( - w_557 w_600) 8) ( <= ( - w_557 w_600) ( ~ 8))) |
---|
| 663 | ( or ( not v_557_2 ) ( not v_600_8 ) ( >= ( - w_557 w_600) 9) ( <= ( - w_557 w_600) ( ~ 8))) |
---|
| 664 | ( or ( not v_557_8 ) ( not v_600_2 ) ( >= ( - w_557 w_600) 8) ( <= ( - w_557 w_600) ( ~ 9))) |
---|
| 665 | ( or ( not v_557_8 ) ( not v_600_8 ) ( >= ( - w_557 w_600) 8) ( <= ( - w_557 w_600) ( ~ 8))) |
---|
| 666 | ( or ( not v_557_2 ) ( not v_613_2 ) ( >= ( - w_557 w_613) 4) ( <= ( - w_557 w_613) ( ~ 4))) |
---|
| 667 | ( or ( not v_557_2 ) ( not v_613_8 ) ( >= ( - w_557 w_613) 4) ( <= ( - w_557 w_613) ( ~ 3))) |
---|
| 668 | ( or ( not v_557_8 ) ( not v_613_2 ) ( >= ( - w_557 w_613) 3) ( <= ( - w_557 w_613) ( ~ 4))) |
---|
| 669 | ( or ( not v_557_8 ) ( not v_613_8 ) ( >= ( - w_557 w_613) 4) ( <= ( - w_557 w_613) ( ~ 4))) |
---|
| 670 | ( or ( not v_557_2 ) ( not v_614_2 ) ( >= ( - w_557 w_614) 10) ( <= ( - w_557 w_614) ( ~ 10))) |
---|
| 671 | ( or ( not v_557_2 ) ( not v_614_8 ) ( >= ( - w_557 w_614) 10) ( <= ( - w_557 w_614) ( ~ 9))) |
---|
| 672 | ( or ( not v_557_8 ) ( not v_614_2 ) ( >= ( - w_557 w_614) 9) ( <= ( - w_557 w_614) ( ~ 10))) |
---|
| 673 | ( or ( not v_557_8 ) ( not v_614_8 ) ( >= ( - w_557 w_614) 10) ( <= ( - w_557 w_614) ( ~ 10))) |
---|
| 674 | ( or ( not v_557_2 ) ( not v_665_2 ) ( >= ( - w_557 w_665) 20) ( <= ( - w_557 w_665) ( ~ 20))) |
---|
| 675 | ( or ( not v_557_2 ) ( not v_665_8 ) ( >= ( - w_557 w_665) 20) ( <= ( - w_557 w_665) ( ~ 20))) |
---|
| 676 | ( or ( not v_557_8 ) ( not v_665_2 ) ( >= ( - w_557 w_665) 20) ( <= ( - w_557 w_665) ( ~ 20))) |
---|
| 677 | ( or ( not v_557_8 ) ( not v_665_8 ) ( >= ( - w_557 w_665) 20) ( <= ( - w_557 w_665) ( ~ 20))) |
---|
| 678 | ( or ( not v_557_2 ) ( not v_666_2 ) ( >= ( - w_557 w_666) 8) ( <= ( - w_557 w_666) ( ~ 8))) |
---|
| 679 | ( or ( not v_557_2 ) ( not v_666_8 ) ( >= ( - w_557 w_666) 8) ( <= ( - w_557 w_666) ( ~ 8))) |
---|
| 680 | ( or ( not v_557_8 ) ( not v_666_2 ) ( >= ( - w_557 w_666) 8) ( <= ( - w_557 w_666) ( ~ 8))) |
---|
| 681 | ( or ( not v_557_8 ) ( not v_666_8 ) ( >= ( - w_557 w_666) 8) ( <= ( - w_557 w_666) ( ~ 8))) |
---|
| 682 | ( or ( not v_557_2 ) ( not v_767_2 ) ( >= ( - w_557 w_767) 11) ( <= ( - w_557 w_767) ( ~ 11))) |
---|
| 683 | ( or ( not v_557_2 ) ( not v_767_8 ) ( >= ( - w_557 w_767) 12) ( <= ( - w_557 w_767) ( ~ 11))) |
---|
| 684 | ( or ( not v_557_8 ) ( not v_767_2 ) ( >= ( - w_557 w_767) 11) ( <= ( - w_557 w_767) ( ~ 12))) |
---|
| 685 | ( or ( not v_557_8 ) ( not v_767_8 ) ( >= ( - w_557 w_767) 11) ( <= ( - w_557 w_767) ( ~ 11))) |
---|
| 686 | ( or ( not v_557_2 ) ( not v_768_2 ) ( >= ( - w_557 w_768) 23) ( <= ( - w_557 w_768) ( ~ 23))) |
---|
| 687 | ( or ( not v_557_2 ) ( not v_768_8 ) ( >= ( - w_557 w_768) 24) ( <= ( - w_557 w_768) ( ~ 23))) |
---|
| 688 | ( or ( not v_557_8 ) ( not v_768_2 ) ( >= ( - w_557 w_768) 23) ( <= ( - w_557 w_768) ( ~ 24))) |
---|
| 689 | ( or ( not v_557_8 ) ( not v_768_8 ) ( >= ( - w_557 w_768) 23) ( <= ( - w_557 w_768) ( ~ 23))) |
---|
| 690 | ( or ( not v_557_2 ) ( not v_785_2 ) ( >= ( - w_557 w_785) 4) ( <= ( - w_557 w_785) ( ~ 4))) |
---|
| 691 | ( or ( not v_557_2 ) ( not v_785_8 ) ( >= ( - w_557 w_785) 4) ( <= ( - w_557 w_785) ( ~ 3))) |
---|
| 692 | ( or ( not v_557_8 ) ( not v_785_2 ) ( >= ( - w_557 w_785) 3) ( <= ( - w_557 w_785) ( ~ 4))) |
---|
| 693 | ( or ( not v_557_8 ) ( not v_785_8 ) ( >= ( - w_557 w_785) 4) ( <= ( - w_557 w_785) ( ~ 4))) |
---|
| 694 | ( or ( not v_557_2 ) ( not v_786_2 ) ( >= ( - w_557 w_786) 9) ( <= ( - w_557 w_786) ( ~ 9))) |
---|
| 695 | ( or ( not v_557_2 ) ( not v_786_8 ) ( >= ( - w_557 w_786) 10) ( <= ( - w_557 w_786) ( ~ 9))) |
---|
| 696 | ( or ( not v_557_8 ) ( not v_786_2 ) ( >= ( - w_557 w_786) 9) ( <= ( - w_557 w_786) ( ~ 10))) |
---|
| 697 | ( or ( not v_557_8 ) ( not v_786_8 ) ( >= ( - w_557 w_786) 9) ( <= ( - w_557 w_786) ( ~ 9))) |
---|
| 698 | ( or ( not v_558_2 ) ( not v_593_2 ) ( >= ( - w_558 w_593) 24) ( <= ( - w_558 w_593) ( ~ 24))) |
---|
| 699 | ( or ( not v_558_2 ) ( not v_593_8 ) ( >= ( - w_558 w_593) 24) ( <= ( - w_558 w_593) ( ~ 24))) |
---|
| 700 | ( or ( not v_558_8 ) ( not v_593_2 ) ( >= ( - w_558 w_593) 24) ( <= ( - w_558 w_593) ( ~ 24))) |
---|
| 701 | ( or ( not v_558_8 ) ( not v_593_8 ) ( >= ( - w_558 w_593) 24) ( <= ( - w_558 w_593) ( ~ 24))) |
---|
| 702 | ( or ( not v_558_2 ) ( not v_594_2 ) ( >= ( - w_558 w_594) 34) ( <= ( - w_558 w_594) ( ~ 34))) |
---|
| 703 | ( or ( not v_558_2 ) ( not v_594_8 ) ( >= ( - w_558 w_594) 35) ( <= ( - w_558 w_594) ( ~ 34))) |
---|
| 704 | ( or ( not v_558_8 ) ( not v_594_2 ) ( >= ( - w_558 w_594) 34) ( <= ( - w_558 w_594) ( ~ 35))) |
---|
| 705 | ( or ( not v_558_8 ) ( not v_594_8 ) ( >= ( - w_558 w_594) 34) ( <= ( - w_558 w_594) ( ~ 34))) |
---|
| 706 | ( or ( not v_558_2 ) ( not v_597_2 ) ( >= ( - w_558 w_597) 16) ( <= ( - w_558 w_597) ( ~ 16))) |
---|
| 707 | ( or ( not v_558_2 ) ( not v_597_8 ) ( >= ( - w_558 w_597) 17) ( <= ( - w_558 w_597) ( ~ 16))) |
---|
| 708 | ( or ( not v_558_8 ) ( not v_597_2 ) ( >= ( - w_558 w_597) 16) ( <= ( - w_558 w_597) ( ~ 17))) |
---|
| 709 | ( or ( not v_558_8 ) ( not v_597_8 ) ( >= ( - w_558 w_597) 16) ( <= ( - w_558 w_597) ( ~ 16))) |
---|
| 710 | ( or ( not v_558_2 ) ( not v_598_2 ) ( >= ( - w_558 w_598) 4) ( <= ( - w_558 w_598) ( ~ 4))) |
---|
| 711 | ( or ( not v_558_2 ) ( not v_598_8 ) ( >= ( - w_558 w_598) 4) ( <= ( - w_558 w_598) ( ~ 3))) |
---|
| 712 | ( or ( not v_558_8 ) ( not v_598_2 ) ( >= ( - w_558 w_598) 3) ( <= ( - w_558 w_598) ( ~ 4))) |
---|
| 713 | ( or ( not v_558_8 ) ( not v_598_8 ) ( >= ( - w_558 w_598) 4) ( <= ( - w_558 w_598) ( ~ 4))) |
---|
| 714 | ( or ( not v_558_2 ) ( not v_599_2 ) ( >= ( - w_558 w_599) 18) ( <= ( - w_558 w_599) ( ~ 18))) |
---|
| 715 | ( or ( not v_558_2 ) ( not v_599_8 ) ( >= ( - w_558 w_599) 18) ( <= ( - w_558 w_599) ( ~ 17))) |
---|
| 716 | ( or ( not v_558_8 ) ( not v_599_2 ) ( >= ( - w_558 w_599) 17) ( <= ( - w_558 w_599) ( ~ 18))) |
---|
| 717 | ( or ( not v_558_8 ) ( not v_599_8 ) ( >= ( - w_558 w_599) 18) ( <= ( - w_558 w_599) ( ~ 18))) |
---|
| 718 | ( or ( not v_558_2 ) ( not v_600_2 ) ( >= ( - w_558 w_600) 5) ( <= ( - w_558 w_600) ( ~ 5))) |
---|
| 719 | ( or ( not v_558_2 ) ( not v_600_8 ) ( >= ( - w_558 w_600) 6) ( <= ( - w_558 w_600) ( ~ 5))) |
---|
| 720 | ( or ( not v_558_8 ) ( not v_600_2 ) ( >= ( - w_558 w_600) 5) ( <= ( - w_558 w_600) ( ~ 6))) |
---|
| 721 | ( or ( not v_558_8 ) ( not v_600_8 ) ( >= ( - w_558 w_600) 5) ( <= ( - w_558 w_600) ( ~ 5))) |
---|
| 722 | ( or ( not v_558_2 ) ( not v_613_2 ) ( >= ( - w_558 w_613) 16) ( <= ( - w_558 w_613) ( ~ 16))) |
---|
| 723 | ( or ( not v_558_2 ) ( not v_613_8 ) ( >= ( - w_558 w_613) 17) ( <= ( - w_558 w_613) ( ~ 16))) |
---|
| 724 | ( or ( not v_558_8 ) ( not v_613_2 ) ( >= ( - w_558 w_613) 16) ( <= ( - w_558 w_613) ( ~ 17))) |
---|
| 725 | ( or ( not v_558_8 ) ( not v_613_8 ) ( >= ( - w_558 w_613) 16) ( <= ( - w_558 w_613) ( ~ 16))) |
---|
| 726 | ( or ( not v_558_2 ) ( not v_614_2 ) ( >= ( - w_558 w_614) 4) ( <= ( - w_558 w_614) ( ~ 4))) |
---|
| 727 | ( or ( not v_558_2 ) ( not v_614_8 ) ( >= ( - w_558 w_614) 4) ( <= ( - w_558 w_614) ( ~ 3))) |
---|
| 728 | ( or ( not v_558_8 ) ( not v_614_2 ) ( >= ( - w_558 w_614) 3) ( <= ( - w_558 w_614) ( ~ 4))) |
---|
| 729 | ( or ( not v_558_8 ) ( not v_614_8 ) ( >= ( - w_558 w_614) 4) ( <= ( - w_558 w_614) ( ~ 4))) |
---|
| 730 | ( or ( not v_558_2 ) ( not v_665_2 ) ( >= ( - w_558 w_665) 31) ( <= ( - w_558 w_665) ( ~ 31))) |
---|
| 731 | ( or ( not v_558_2 ) ( not v_665_8 ) ( >= ( - w_558 w_665) 31) ( <= ( - w_558 w_665) ( ~ 30))) |
---|
| 732 | ( or ( not v_558_8 ) ( not v_665_2 ) ( >= ( - w_558 w_665) 30) ( <= ( - w_558 w_665) ( ~ 31))) |
---|
| 733 | ( or ( not v_558_8 ) ( not v_665_8 ) ( >= ( - w_558 w_665) 31) ( <= ( - w_558 w_665) ( ~ 31))) |
---|
| 734 | ( or ( not v_558_2 ) ( not v_666_2 ) ( >= ( - w_558 w_666) 20) ( <= ( - w_558 w_666) ( ~ 20))) |
---|
| 735 | ( or ( not v_558_2 ) ( not v_666_8 ) ( >= ( - w_558 w_666) 20) ( <= ( - w_558 w_666) ( ~ 20))) |
---|
| 736 | ( or ( not v_558_8 ) ( not v_666_2 ) ( >= ( - w_558 w_666) 20) ( <= ( - w_558 w_666) ( ~ 20))) |
---|
| 737 | ( or ( not v_558_8 ) ( not v_666_8 ) ( >= ( - w_558 w_666) 20) ( <= ( - w_558 w_666) ( ~ 20))) |
---|
| 738 | ( or ( not v_558_2 ) ( not v_767_2 ) ( >= ( - w_558 w_767) 23) ( <= ( - w_558 w_767) ( ~ 23))) |
---|
| 739 | ( or ( not v_558_2 ) ( not v_767_8 ) ( >= ( - w_558 w_767) 24) ( <= ( - w_558 w_767) ( ~ 23))) |
---|
| 740 | ( or ( not v_558_8 ) ( not v_767_2 ) ( >= ( - w_558 w_767) 23) ( <= ( - w_558 w_767) ( ~ 24))) |
---|
| 741 | ( or ( not v_558_8 ) ( not v_767_8 ) ( >= ( - w_558 w_767) 23) ( <= ( - w_558 w_767) ( ~ 23))) |
---|
| 742 | ( or ( not v_558_2 ) ( not v_768_2 ) ( >= ( - w_558 w_768) 34) ( <= ( - w_558 w_768) ( ~ 34))) |
---|
| 743 | ( or ( not v_558_2 ) ( not v_768_8 ) ( >= ( - w_558 w_768) 34) ( <= ( - w_558 w_768) ( ~ 33))) |
---|
| 744 | ( or ( not v_558_8 ) ( not v_768_2 ) ( >= ( - w_558 w_768) 33) ( <= ( - w_558 w_768) ( ~ 34))) |
---|
| 745 | ( or ( not v_558_8 ) ( not v_768_8 ) ( >= ( - w_558 w_768) 34) ( <= ( - w_558 w_768) ( ~ 34))) |
---|
| 746 | ( or ( not v_558_2 ) ( not v_785_2 ) ( >= ( - w_558 w_785) 16) ( <= ( - w_558 w_785) ( ~ 16))) |
---|
| 747 | ( or ( not v_558_2 ) ( not v_785_8 ) ( >= ( - w_558 w_785) 17) ( <= ( - w_558 w_785) ( ~ 16))) |
---|
| 748 | ( or ( not v_558_8 ) ( not v_785_2 ) ( >= ( - w_558 w_785) 16) ( <= ( - w_558 w_785) ( ~ 17))) |
---|
| 749 | ( or ( not v_558_8 ) ( not v_785_8 ) ( >= ( - w_558 w_785) 16) ( <= ( - w_558 w_785) ( ~ 16))) |
---|
| 750 | ( or ( not v_558_2 ) ( not v_786_2 ) ( >= ( - w_558 w_786) 4) ( <= ( - w_558 w_786) ( ~ 4))) |
---|
| 751 | ( or ( not v_558_2 ) ( not v_786_8 ) ( >= ( - w_558 w_786) 4) ( <= ( - w_558 w_786) ( ~ 3))) |
---|
| 752 | ( or ( not v_558_8 ) ( not v_786_2 ) ( >= ( - w_558 w_786) 3) ( <= ( - w_558 w_786) ( ~ 4))) |
---|
| 753 | ( or ( not v_558_8 ) ( not v_786_8 ) ( >= ( - w_558 w_786) 4) ( <= ( - w_558 w_786) ( ~ 4))) |
---|
| 754 | ( or ( not v_593_2 ) ( not v_594_2 ) ( = ( - w_593 w_594) 17) ( = ( - w_594 w_593) 17)) |
---|
| 755 | ( or ( not v_593_2 ) ( not v_594_8 )) |
---|
| 756 | ( or ( not v_593_8 ) ( not v_594_2 )) |
---|
| 757 | ( or ( not v_593_8 ) ( not v_594_8 ) ( = ( - w_593 w_594) 17) ( = ( - w_594 w_593) 17)) |
---|
| 758 | ( or ( not v_593_2 ) ( not v_597_2 ) ( >= ( - w_593 w_597) 8) ( <= ( - w_593 w_597) ( ~ 8))) |
---|
| 759 | ( or ( not v_593_2 ) ( not v_597_8 ) ( >= ( - w_593 w_597) 9) ( <= ( - w_593 w_597) ( ~ 8))) |
---|
| 760 | ( or ( not v_593_8 ) ( not v_597_2 ) ( >= ( - w_593 w_597) 8) ( <= ( - w_593 w_597) ( ~ 9))) |
---|
| 761 | ( or ( not v_593_8 ) ( not v_597_8 ) ( >= ( - w_593 w_597) 8) ( <= ( - w_593 w_597) ( ~ 8))) |
---|
| 762 | ( or ( not v_593_2 ) ( not v_598_2 ) ( >= ( - w_593 w_598) 21) ( <= ( - w_593 w_598) ( ~ 21))) |
---|
| 763 | ( or ( not v_593_2 ) ( not v_598_8 ) ( >= ( - w_593 w_598) 21) ( <= ( - w_593 w_598) ( ~ 20))) |
---|
| 764 | ( or ( not v_593_8 ) ( not v_598_2 ) ( >= ( - w_593 w_598) 20) ( <= ( - w_593 w_598) ( ~ 21))) |
---|
| 765 | ( or ( not v_593_8 ) ( not v_598_8 ) ( >= ( - w_593 w_598) 21) ( <= ( - w_593 w_598) ( ~ 21))) |
---|
| 766 | ( or ( not v_593_2 ) ( not v_613_2 ) ( >= ( - w_593 w_613) 8) ( <= ( - w_593 w_613) ( ~ 8))) |
---|
| 767 | ( or ( not v_593_2 ) ( not v_613_8 ) ( >= ( - w_593 w_613) 9) ( <= ( - w_593 w_613) ( ~ 8))) |
---|
| 768 | ( or ( not v_593_8 ) ( not v_613_2 ) ( >= ( - w_593 w_613) 8) ( <= ( - w_593 w_613) ( ~ 9))) |
---|
| 769 | ( or ( not v_593_8 ) ( not v_613_8 ) ( >= ( - w_593 w_613) 8) ( <= ( - w_593 w_613) ( ~ 8))) |
---|
| 770 | ( or ( not v_593_2 ) ( not v_614_2 ) ( >= ( - w_593 w_614) 21) ( <= ( - w_593 w_614) ( ~ 21))) |
---|
| 771 | ( or ( not v_593_2 ) ( not v_614_8 ) ( >= ( - w_593 w_614) 21) ( <= ( - w_593 w_614) ( ~ 20))) |
---|
| 772 | ( or ( not v_593_8 ) ( not v_614_2 ) ( >= ( - w_593 w_614) 20) ( <= ( - w_593 w_614) ( ~ 21))) |
---|
| 773 | ( or ( not v_593_8 ) ( not v_614_8 ) ( >= ( - w_593 w_614) 21) ( <= ( - w_593 w_614) ( ~ 21))) |
---|
| 774 | ( or ( not v_593_2 ) ( not v_631_2 ) ( >= ( - w_593 w_631) 19) ( <= ( - w_593 w_631) ( ~ 19))) |
---|
| 775 | ( or ( not v_593_2 ) ( not v_631_8 ) ( >= ( - w_593 w_631) 20) ( <= ( - w_593 w_631) ( ~ 19))) |
---|
| 776 | ( or ( not v_593_8 ) ( not v_631_2 ) ( >= ( - w_593 w_631) 19) ( <= ( - w_593 w_631) ( ~ 20))) |
---|
| 777 | ( or ( not v_593_8 ) ( not v_631_8 ) ( >= ( - w_593 w_631) 19) ( <= ( - w_593 w_631) ( ~ 19))) |
---|
| 778 | ( or ( not v_593_2 ) ( not v_632_2 ) ( >= ( - w_593 w_632) 7) ( <= ( - w_593 w_632) ( ~ 7))) |
---|
| 779 | ( or ( not v_593_2 ) ( not v_632_8 ) ( >= ( - w_593 w_632) 7) ( <= ( - w_593 w_632) ( ~ 6))) |
---|
| 780 | ( or ( not v_593_8 ) ( not v_632_2 ) ( >= ( - w_593 w_632) 6) ( <= ( - w_593 w_632) ( ~ 7))) |
---|
| 781 | ( or ( not v_593_8 ) ( not v_632_8 ) ( >= ( - w_593 w_632) 7) ( <= ( - w_593 w_632) ( ~ 7))) |
---|
| 782 | ( or ( not v_593_2 ) ( not v_665_2 ) ( >= ( - w_593 w_665) 8) ( <= ( - w_593 w_665) ( ~ 8))) |
---|
| 783 | ( or ( not v_593_2 ) ( not v_665_8 ) ( >= ( - w_593 w_665) 9) ( <= ( - w_593 w_665) ( ~ 8))) |
---|
| 784 | ( or ( not v_593_8 ) ( not v_665_2 ) ( >= ( - w_593 w_665) 8) ( <= ( - w_593 w_665) ( ~ 9))) |
---|
| 785 | ( or ( not v_593_8 ) ( not v_665_8 ) ( >= ( - w_593 w_665) 8) ( <= ( - w_593 w_665) ( ~ 8))) |
---|
| 786 | ( or ( not v_593_2 ) ( not v_666_2 ) ( >= ( - w_593 w_666) 5) ( <= ( - w_593 w_666) ( ~ 5))) |
---|
| 787 | ( or ( not v_593_2 ) ( not v_666_8 ) ( >= ( - w_593 w_666) 6) ( <= ( - w_593 w_666) ( ~ 5))) |
---|
| 788 | ( or ( not v_593_8 ) ( not v_666_2 ) ( >= ( - w_593 w_666) 5) ( <= ( - w_593 w_666) ( ~ 6))) |
---|
| 789 | ( or ( not v_593_8 ) ( not v_666_8 ) ( >= ( - w_593 w_666) 5) ( <= ( - w_593 w_666) ( ~ 5))) |
---|
| 790 | ( or ( not v_593_2 ) ( not v_767_2 ) ( >= ( - w_593 w_767) 1) ( <= ( - w_593 w_767) ( ~ 1))) |
---|
| 791 | ( or ( not v_593_2 ) ( not v_767_8 ) ( >= ( - w_593 w_767) 2) ( <= ( - w_593 w_767) ( ~ 1))) |
---|
| 792 | ( or ( not v_593_8 ) ( not v_767_2 ) ( >= ( - w_593 w_767) 1) ( <= ( - w_593 w_767) ( ~ 2))) |
---|
| 793 | ( or ( not v_593_8 ) ( not v_767_8 ) ( >= ( - w_593 w_767) 1) ( <= ( - w_593 w_767) ( ~ 1))) |
---|
| 794 | ( or ( not v_593_2 ) ( not v_768_2 ) ( >= ( - w_593 w_768) 11) ( <= ( - w_593 w_768) ( ~ 11))) |
---|
| 795 | ( or ( not v_593_2 ) ( not v_768_8 ) ( >= ( - w_593 w_768) 12) ( <= ( - w_593 w_768) ( ~ 11))) |
---|
| 796 | ( or ( not v_593_8 ) ( not v_768_2 ) ( >= ( - w_593 w_768) 11) ( <= ( - w_593 w_768) ( ~ 12))) |
---|
| 797 | ( or ( not v_593_8 ) ( not v_768_8 ) ( >= ( - w_593 w_768) 11) ( <= ( - w_593 w_768) ( ~ 11))) |
---|
| 798 | ( or ( not v_593_2 ) ( not v_785_2 ) ( >= ( - w_593 w_785) 8) ( <= ( - w_593 w_785) ( ~ 8))) |
---|
| 799 | ( or ( not v_593_2 ) ( not v_785_8 ) ( >= ( - w_593 w_785) 9) ( <= ( - w_593 w_785) ( ~ 8))) |
---|
| 800 | ( or ( not v_593_8 ) ( not v_785_2 ) ( >= ( - w_593 w_785) 8) ( <= ( - w_593 w_785) ( ~ 9))) |
---|
| 801 | ( or ( not v_593_8 ) ( not v_785_8 ) ( >= ( - w_593 w_785) 8) ( <= ( - w_593 w_785) ( ~ 8))) |
---|
| 802 | ( or ( not v_593_2 ) ( not v_786_2 ) ( >= ( - w_593 w_786) 20) ( <= ( - w_593 w_786) ( ~ 20))) |
---|
| 803 | ( or ( not v_593_2 ) ( not v_786_8 ) ( >= ( - w_593 w_786) 21) ( <= ( - w_593 w_786) ( ~ 20))) |
---|
| 804 | ( or ( not v_593_8 ) ( not v_786_2 ) ( >= ( - w_593 w_786) 20) ( <= ( - w_593 w_786) ( ~ 21))) |
---|
| 805 | ( or ( not v_593_8 ) ( not v_786_8 ) ( >= ( - w_593 w_786) 20) ( <= ( - w_593 w_786) ( ~ 20))) |
---|
| 806 | ( or ( not v_594_2 ) ( not v_597_2 ) ( >= ( - w_594 w_597) 21) ( <= ( - w_594 w_597) ( ~ 21))) |
---|
| 807 | ( or ( not v_594_2 ) ( not v_597_8 ) ( >= ( - w_594 w_597) 21) ( <= ( - w_594 w_597) ( ~ 20))) |
---|
| 808 | ( or ( not v_594_8 ) ( not v_597_2 ) ( >= ( - w_594 w_597) 20) ( <= ( - w_594 w_597) ( ~ 21))) |
---|
| 809 | ( or ( not v_594_8 ) ( not v_597_8 ) ( >= ( - w_594 w_597) 21) ( <= ( - w_594 w_597) ( ~ 21))) |
---|
| 810 | ( or ( not v_594_2 ) ( not v_598_2 ) ( >= ( - w_594 w_598) 31) ( <= ( - w_594 w_598) ( ~ 31))) |
---|
| 811 | ( or ( not v_594_2 ) ( not v_598_8 ) ( >= ( - w_594 w_598) 31) ( <= ( - w_594 w_598) ( ~ 30))) |
---|
| 812 | ( or ( not v_594_8 ) ( not v_598_2 ) ( >= ( - w_594 w_598) 30) ( <= ( - w_594 w_598) ( ~ 31))) |
---|
| 813 | ( or ( not v_594_8 ) ( not v_598_8 ) ( >= ( - w_594 w_598) 31) ( <= ( - w_594 w_598) ( ~ 31))) |
---|
| 814 | ( or ( not v_594_2 ) ( not v_613_2 ) ( >= ( - w_594 w_613) 21) ( <= ( - w_594 w_613) ( ~ 21))) |
---|
| 815 | ( or ( not v_594_2 ) ( not v_613_8 ) ( >= ( - w_594 w_613) 21) ( <= ( - w_594 w_613) ( ~ 20))) |
---|
| 816 | ( or ( not v_594_8 ) ( not v_613_2 ) ( >= ( - w_594 w_613) 20) ( <= ( - w_594 w_613) ( ~ 21))) |
---|
| 817 | ( or ( not v_594_8 ) ( not v_613_8 ) ( >= ( - w_594 w_613) 21) ( <= ( - w_594 w_613) ( ~ 21))) |
---|
| 818 | ( or ( not v_594_2 ) ( not v_614_2 ) ( >= ( - w_594 w_614) 31) ( <= ( - w_594 w_614) ( ~ 31))) |
---|
| 819 | ( or ( not v_594_2 ) ( not v_614_8 ) ( >= ( - w_594 w_614) 31) ( <= ( - w_594 w_614) ( ~ 30))) |
---|
| 820 | ( or ( not v_594_8 ) ( not v_614_2 ) ( >= ( - w_594 w_614) 30) ( <= ( - w_594 w_614) ( ~ 31))) |
---|
| 821 | ( or ( not v_594_8 ) ( not v_614_8 ) ( >= ( - w_594 w_614) 31) ( <= ( - w_594 w_614) ( ~ 31))) |
---|
| 822 | ( or ( not v_594_2 ) ( not v_631_2 ) ( >= ( - w_594 w_631) 29) ( <= ( - w_594 w_631) ( ~ 29))) |
---|
| 823 | ( or ( not v_594_2 ) ( not v_631_8 ) ( >= ( - w_594 w_631) 30) ( <= ( - w_594 w_631) ( ~ 29))) |
---|
| 824 | ( or ( not v_594_8 ) ( not v_631_2 ) ( >= ( - w_594 w_631) 29) ( <= ( - w_594 w_631) ( ~ 30))) |
---|
| 825 | ( or ( not v_594_8 ) ( not v_631_8 ) ( >= ( - w_594 w_631) 29) ( <= ( - w_594 w_631) ( ~ 29))) |
---|
| 826 | ( or ( not v_594_2 ) ( not v_632_2 ) ( >= ( - w_594 w_632) 19) ( <= ( - w_594 w_632) ( ~ 19))) |
---|
| 827 | ( or ( not v_594_2 ) ( not v_632_8 ) ( >= ( - w_594 w_632) 20) ( <= ( - w_594 w_632) ( ~ 19))) |
---|
| 828 | ( or ( not v_594_8 ) ( not v_632_2 ) ( >= ( - w_594 w_632) 19) ( <= ( - w_594 w_632) ( ~ 20))) |
---|
| 829 | ( or ( not v_594_8 ) ( not v_632_8 ) ( >= ( - w_594 w_632) 19) ( <= ( - w_594 w_632) ( ~ 19))) |
---|
| 830 | ( or ( not v_594_2 ) ( not v_665_2 ) ( >= ( - w_594 w_665) 5) ( <= ( - w_594 w_665) ( ~ 5))) |
---|
| 831 | ( or ( not v_594_2 ) ( not v_665_8 ) ( >= ( - w_594 w_665) 6) ( <= ( - w_594 w_665) ( ~ 5))) |
---|
| 832 | ( or ( not v_594_8 ) ( not v_665_2 ) ( >= ( - w_594 w_665) 5) ( <= ( - w_594 w_665) ( ~ 6))) |
---|
| 833 | ( or ( not v_594_8 ) ( not v_665_8 ) ( >= ( - w_594 w_665) 5) ( <= ( - w_594 w_665) ( ~ 5))) |
---|
| 834 | ( or ( not v_594_2 ) ( not v_666_2 ) ( >= ( - w_594 w_666) 18) ( <= ( - w_594 w_666) ( ~ 18))) |
---|
| 835 | ( or ( not v_594_2 ) ( not v_666_8 ) ( >= ( - w_594 w_666) 18) ( <= ( - w_594 w_666) ( ~ 17))) |
---|
| 836 | ( or ( not v_594_8 ) ( not v_666_2 ) ( >= ( - w_594 w_666) 17) ( <= ( - w_594 w_666) ( ~ 18))) |
---|
| 837 | ( or ( not v_594_8 ) ( not v_666_8 ) ( >= ( - w_594 w_666) 18) ( <= ( - w_594 w_666) ( ~ 18))) |
---|
| 838 | ( or ( not v_594_2 ) ( not v_767_2 ) ( >= ( - w_594 w_767) 13) ( <= ( - w_594 w_767) ( ~ 13))) |
---|
| 839 | ( or ( not v_594_2 ) ( not v_767_8 ) ( >= ( - w_594 w_767) 13) ( <= ( - w_594 w_767) ( ~ 12))) |
---|
| 840 | ( or ( not v_594_8 ) ( not v_767_2 ) ( >= ( - w_594 w_767) 12) ( <= ( - w_594 w_767) ( ~ 13))) |
---|
| 841 | ( or ( not v_594_8 ) ( not v_767_8 ) ( >= ( - w_594 w_767) 13) ( <= ( - w_594 w_767) ( ~ 13))) |
---|
| 842 | ( or ( not v_594_2 ) ( not v_768_2 ) ( >= ( - w_594 w_768) 1) ( <= ( - w_594 w_768) ( ~ 1))) |
---|
| 843 | ( or ( not v_594_2 ) ( not v_768_8 ) ( >= ( - w_594 w_768) 2) ( <= ( - w_594 w_768) ( ~ 1))) |
---|
| 844 | ( or ( not v_594_8 ) ( not v_768_2 ) ( >= ( - w_594 w_768) 1) ( <= ( - w_594 w_768) ( ~ 2))) |
---|
| 845 | ( or ( not v_594_8 ) ( not v_768_8 ) ( >= ( - w_594 w_768) 1) ( <= ( - w_594 w_768) ( ~ 1))) |
---|
| 846 | ( or ( not v_594_2 ) ( not v_785_2 ) ( >= ( - w_594 w_785) 21) ( <= ( - w_594 w_785) ( ~ 21))) |
---|
| 847 | ( or ( not v_594_2 ) ( not v_785_8 ) ( >= ( - w_594 w_785) 21) ( <= ( - w_594 w_785) ( ~ 20))) |
---|
| 848 | ( or ( not v_594_8 ) ( not v_785_2 ) ( >= ( - w_594 w_785) 20) ( <= ( - w_594 w_785) ( ~ 21))) |
---|
| 849 | ( or ( not v_594_8 ) ( not v_785_8 ) ( >= ( - w_594 w_785) 21) ( <= ( - w_594 w_785) ( ~ 21))) |
---|
| 850 | ( or ( not v_594_2 ) ( not v_786_2 ) ( >= ( - w_594 w_786) 31) ( <= ( - w_594 w_786) ( ~ 31))) |
---|
| 851 | ( or ( not v_594_2 ) ( not v_786_8 ) ( >= ( - w_594 w_786) 31) ( <= ( - w_594 w_786) ( ~ 30))) |
---|
| 852 | ( or ( not v_594_8 ) ( not v_786_2 ) ( >= ( - w_594 w_786) 30) ( <= ( - w_594 w_786) ( ~ 31))) |
---|
| 853 | ( or ( not v_594_8 ) ( not v_786_8 ) ( >= ( - w_594 w_786) 31) ( <= ( - w_594 w_786) ( ~ 31))) |
---|
| 854 | ( or ( not v_597_2 ) ( not v_598_2 ) ( = ( - w_597 w_598) 17) ( = ( - w_598 w_597) 17)) |
---|
| 855 | ( or ( not v_597_2 ) ( not v_598_8 )) |
---|
| 856 | ( or ( not v_597_8 ) ( not v_598_2 )) |
---|
| 857 | ( or ( not v_597_8 ) ( not v_598_8 ) ( = ( - w_597 w_598) 17) ( = ( - w_598 w_597) 17)) |
---|
| 858 | ( or ( not v_597_2 ) ( not v_613_2 ) ( >= ( - w_597 w_613) 1) ( <= ( - w_597 w_613) ( ~ 1))) |
---|
| 859 | ( or ( not v_597_2 ) ( not v_613_8 ) ( >= ( - w_597 w_613) 1) ( <= ( - w_597 w_613) 0)) |
---|
| 860 | ( or ( not v_597_8 ) ( not v_613_2 ) ( >= ( - w_597 w_613) 0) ( <= ( - w_597 w_613) ( ~ 1))) |
---|
| 861 | ( or ( not v_597_8 ) ( not v_613_8 ) ( >= ( - w_597 w_613) 1) ( <= ( - w_597 w_613) ( ~ 1))) |
---|
| 862 | ( or ( not v_597_2 ) ( not v_614_2 ) ( >= ( - w_597 w_614) 13) ( <= ( - w_597 w_614) ( ~ 13))) |
---|
| 863 | ( or ( not v_597_2 ) ( not v_614_8 ) ( >= ( - w_597 w_614) 14) ( <= ( - w_597 w_614) ( ~ 13))) |
---|
| 864 | ( or ( not v_597_8 ) ( not v_614_2 ) ( >= ( - w_597 w_614) 13) ( <= ( - w_597 w_614) ( ~ 14))) |
---|
| 865 | ( or ( not v_597_8 ) ( not v_614_8 ) ( >= ( - w_597 w_614) 13) ( <= ( - w_597 w_614) ( ~ 13))) |
---|
| 866 | ( or ( not v_597_2 ) ( not v_665_2 ) ( >= ( - w_597 w_665) 16) ( <= ( - w_597 w_665) ( ~ 16))) |
---|
| 867 | ( or ( not v_597_2 ) ( not v_665_8 ) ( >= ( - w_597 w_665) 16) ( <= ( - w_597 w_665) ( ~ 16))) |
---|
| 868 | ( or ( not v_597_8 ) ( not v_665_2 ) ( >= ( - w_597 w_665) 16) ( <= ( - w_597 w_665) ( ~ 16))) |
---|
| 869 | ( or ( not v_597_8 ) ( not v_665_8 ) ( >= ( - w_597 w_665) 16) ( <= ( - w_597 w_665) ( ~ 16))) |
---|
| 870 | ( or ( not v_597_2 ) ( not v_666_2 ) ( >= ( - w_597 w_666) 4) ( <= ( - w_597 w_666) ( ~ 4))) |
---|
| 871 | ( or ( not v_597_2 ) ( not v_666_8 ) ( >= ( - w_597 w_666) 4) ( <= ( - w_597 w_666) ( ~ 3))) |
---|
| 872 | ( or ( not v_597_8 ) ( not v_666_2 ) ( >= ( - w_597 w_666) 3) ( <= ( - w_597 w_666) ( ~ 4))) |
---|
| 873 | ( or ( not v_597_8 ) ( not v_666_8 ) ( >= ( - w_597 w_666) 4) ( <= ( - w_597 w_666) ( ~ 4))) |
---|
| 874 | ( or ( not v_597_2 ) ( not v_767_2 ) ( >= ( - w_597 w_767) 8) ( <= ( - w_597 w_767) ( ~ 8))) |
---|
| 875 | ( or ( not v_597_2 ) ( not v_767_8 ) ( >= ( - w_597 w_767) 8) ( <= ( - w_597 w_767) ( ~ 7))) |
---|
| 876 | ( or ( not v_597_8 ) ( not v_767_2 ) ( >= ( - w_597 w_767) 7) ( <= ( - w_597 w_767) ( ~ 8))) |
---|
| 877 | ( or ( not v_597_8 ) ( not v_767_8 ) ( >= ( - w_597 w_767) 8) ( <= ( - w_597 w_767) ( ~ 8))) |
---|
| 878 | ( or ( not v_597_2 ) ( not v_768_2 ) ( >= ( - w_597 w_768) 19) ( <= ( - w_597 w_768) ( ~ 19))) |
---|
| 879 | ( or ( not v_597_2 ) ( not v_768_8 ) ( >= ( - w_597 w_768) 19) ( <= ( - w_597 w_768) ( ~ 19))) |
---|
| 880 | ( or ( not v_597_8 ) ( not v_768_2 ) ( >= ( - w_597 w_768) 19) ( <= ( - w_597 w_768) ( ~ 19))) |
---|
| 881 | ( or ( not v_597_8 ) ( not v_768_8 ) ( >= ( - w_597 w_768) 19) ( <= ( - w_597 w_768) ( ~ 19))) |
---|
| 882 | ( or ( not v_597_2 ) ( not v_785_2 ) ( >= ( - w_597 w_785) 1) ( <= ( - w_597 w_785) ( ~ 1))) |
---|
| 883 | ( or ( not v_597_2 ) ( not v_785_8 ) ( >= ( - w_597 w_785) 1) ( <= ( - w_597 w_785) 0)) |
---|
| 884 | ( or ( not v_597_8 ) ( not v_785_2 ) ( >= ( - w_597 w_785) 0) ( <= ( - w_597 w_785) ( ~ 1))) |
---|
| 885 | ( or ( not v_597_8 ) ( not v_785_8 ) ( >= ( - w_597 w_785) 1) ( <= ( - w_597 w_785) ( ~ 1))) |
---|
| 886 | ( or ( not v_597_2 ) ( not v_786_2 ) ( >= ( - w_597 w_786) 13) ( <= ( - w_597 w_786) ( ~ 13))) |
---|
| 887 | ( or ( not v_597_2 ) ( not v_786_8 ) ( >= ( - w_597 w_786) 13) ( <= ( - w_597 w_786) ( ~ 12))) |
---|
| 888 | ( or ( not v_597_8 ) ( not v_786_2 ) ( >= ( - w_597 w_786) 12) ( <= ( - w_597 w_786) ( ~ 13))) |
---|
| 889 | ( or ( not v_597_8 ) ( not v_786_8 ) ( >= ( - w_597 w_786) 13) ( <= ( - w_597 w_786) ( ~ 13))) |
---|
| 890 | ( or ( not v_598_2 ) ( not v_613_2 ) ( >= ( - w_598 w_613) 13) ( <= ( - w_598 w_613) ( ~ 13))) |
---|
| 891 | ( or ( not v_598_2 ) ( not v_613_8 ) ( >= ( - w_598 w_613) 14) ( <= ( - w_598 w_613) ( ~ 13))) |
---|
| 892 | ( or ( not v_598_8 ) ( not v_613_2 ) ( >= ( - w_598 w_613) 13) ( <= ( - w_598 w_613) ( ~ 14))) |
---|
| 893 | ( or ( not v_598_8 ) ( not v_613_8 ) ( >= ( - w_598 w_613) 13) ( <= ( - w_598 w_613) ( ~ 13))) |
---|
| 894 | ( or ( not v_598_2 ) ( not v_614_2 ) ( >= ( - w_598 w_614) 1) ( <= ( - w_598 w_614) ( ~ 1))) |
---|
| 895 | ( or ( not v_598_2 ) ( not v_614_8 ) ( >= ( - w_598 w_614) 1) ( <= ( - w_598 w_614) 0)) |
---|
| 896 | ( or ( not v_598_8 ) ( not v_614_2 ) ( >= ( - w_598 w_614) 0) ( <= ( - w_598 w_614) ( ~ 1))) |
---|
| 897 | ( or ( not v_598_8 ) ( not v_614_8 ) ( >= ( - w_598 w_614) 1) ( <= ( - w_598 w_614) ( ~ 1))) |
---|
| 898 | ( or ( not v_598_2 ) ( not v_665_2 ) ( >= ( - w_598 w_665) 26) ( <= ( - w_598 w_665) ( ~ 26))) |
---|
| 899 | ( or ( not v_598_2 ) ( not v_665_8 ) ( >= ( - w_598 w_665) 27) ( <= ( - w_598 w_665) ( ~ 26))) |
---|
| 900 | ( or ( not v_598_8 ) ( not v_665_2 ) ( >= ( - w_598 w_665) 26) ( <= ( - w_598 w_665) ( ~ 27))) |
---|
| 901 | ( or ( not v_598_8 ) ( not v_665_8 ) ( >= ( - w_598 w_665) 26) ( <= ( - w_598 w_665) ( ~ 26))) |
---|
| 902 | ( or ( not v_598_2 ) ( not v_666_2 ) ( >= ( - w_598 w_666) 16) ( <= ( - w_598 w_666) ( ~ 16))) |
---|
| 903 | ( or ( not v_598_2 ) ( not v_666_8 ) ( >= ( - w_598 w_666) 16) ( <= ( - w_598 w_666) ( ~ 16))) |
---|
| 904 | ( or ( not v_598_8 ) ( not v_666_2 ) ( >= ( - w_598 w_666) 16) ( <= ( - w_598 w_666) ( ~ 16))) |
---|
| 905 | ( or ( not v_598_8 ) ( not v_666_8 ) ( >= ( - w_598 w_666) 16) ( <= ( - w_598 w_666) ( ~ 16))) |
---|
| 906 | ( or ( not v_598_2 ) ( not v_768_2 ) ( >= ( - w_598 w_768) 30) ( <= ( - w_598 w_768) ( ~ 30))) |
---|
| 907 | ( or ( not v_598_2 ) ( not v_768_8 ) ( >= ( - w_598 w_768) 31) ( <= ( - w_598 w_768) ( ~ 30))) |
---|
| 908 | ( or ( not v_598_8 ) ( not v_768_2 ) ( >= ( - w_598 w_768) 30) ( <= ( - w_598 w_768) ( ~ 31))) |
---|
| 909 | ( or ( not v_598_8 ) ( not v_768_8 ) ( >= ( - w_598 w_768) 30) ( <= ( - w_598 w_768) ( ~ 30))) |
---|
| 910 | ( or ( not v_598_2 ) ( not v_785_2 ) ( >= ( - w_598 w_785) 13) ( <= ( - w_598 w_785) ( ~ 13))) |
---|
| 911 | ( or ( not v_598_2 ) ( not v_785_8 ) ( >= ( - w_598 w_785) 14) ( <= ( - w_598 w_785) ( ~ 13))) |
---|
| 912 | ( or ( not v_598_8 ) ( not v_785_2 ) ( >= ( - w_598 w_785) 13) ( <= ( - w_598 w_785) ( ~ 14))) |
---|
| 913 | ( or ( not v_598_8 ) ( not v_785_8 ) ( >= ( - w_598 w_785) 13) ( <= ( - w_598 w_785) ( ~ 13))) |
---|
| 914 | ( or ( not v_598_2 ) ( not v_786_2 ) ( >= ( - w_598 w_786) 1) ( <= ( - w_598 w_786) ( ~ 1))) |
---|
| 915 | ( or ( not v_598_2 ) ( not v_786_8 ) ( >= ( - w_598 w_786) 1) ( <= ( - w_598 w_786) 0)) |
---|
| 916 | ( or ( not v_598_8 ) ( not v_786_2 ) ( >= ( - w_598 w_786) 0) ( <= ( - w_598 w_786) ( ~ 1))) |
---|
| 917 | ( or ( not v_598_8 ) ( not v_786_8 ) ( >= ( - w_598 w_786) 1) ( <= ( - w_598 w_786) ( ~ 1))) |
---|
| 918 | ( or ( not v_599_2 ) ( not v_600_2 ) ( = ( - w_599 w_600) 17) ( = ( - w_600 w_599) 17)) |
---|
| 919 | ( or ( not v_599_2 ) ( not v_600_8 )) |
---|
| 920 | ( or ( not v_599_8 ) ( not v_600_2 )) |
---|
| 921 | ( or ( not v_599_8 ) ( not v_600_8 ) ( = ( - w_599 w_600) 17) ( = ( - w_600 w_599) 17)) |
---|
| 922 | ( or ( not v_599_2 ) ( not v_665_2 ) ( >= ( - w_599 w_665) 15) ( <= ( - w_599 w_665) ( ~ 15))) |
---|
| 923 | ( or ( not v_599_2 ) ( not v_665_8 ) ( >= ( - w_599 w_665) 15) ( <= ( - w_599 w_665) ( ~ 14))) |
---|
| 924 | ( or ( not v_599_8 ) ( not v_665_2 ) ( >= ( - w_599 w_665) 14) ( <= ( - w_599 w_665) ( ~ 15))) |
---|
| 925 | ( or ( not v_599_8 ) ( not v_665_8 ) ( >= ( - w_599 w_665) 15) ( <= ( - w_599 w_665) ( ~ 15))) |
---|
| 926 | ( or ( not v_599_2 ) ( not v_666_2 ) ( >= ( - w_599 w_666) 2) ( <= ( - w_599 w_666) ( ~ 2))) |
---|
| 927 | ( or ( not v_599_2 ) ( not v_666_8 ) ( >= ( - w_599 w_666) 3) ( <= ( - w_599 w_666) ( ~ 2))) |
---|
| 928 | ( or ( not v_599_8 ) ( not v_666_2 ) ( >= ( - w_599 w_666) 2) ( <= ( - w_599 w_666) ( ~ 3))) |
---|
| 929 | ( or ( not v_599_8 ) ( not v_666_8 ) ( >= ( - w_599 w_666) 2) ( <= ( - w_599 w_666) ( ~ 2))) |
---|
| 930 | ( or ( not v_599_2 ) ( not v_767_2 ) ( >= ( - w_599 w_767) 7) ( <= ( - w_599 w_767) ( ~ 7))) |
---|
| 931 | ( or ( not v_599_2 ) ( not v_767_8 ) ( >= ( - w_599 w_767) 7) ( <= ( - w_599 w_767) ( ~ 6))) |
---|
| 932 | ( or ( not v_599_8 ) ( not v_767_2 ) ( >= ( - w_599 w_767) 6) ( <= ( - w_599 w_767) ( ~ 7))) |
---|
| 933 | ( or ( not v_599_8 ) ( not v_767_8 ) ( >= ( - w_599 w_767) 7) ( <= ( - w_599 w_767) ( ~ 7))) |
---|
| 934 | ( or ( not v_599_2 ) ( not v_768_2 ) ( >= ( - w_599 w_768) 19) ( <= ( - w_599 w_768) ( ~ 19))) |
---|
| 935 | ( or ( not v_599_2 ) ( not v_768_8 ) ( >= ( - w_599 w_768) 19) ( <= ( - w_599 w_768) ( ~ 18))) |
---|
| 936 | ( or ( not v_599_8 ) ( not v_768_2 ) ( >= ( - w_599 w_768) 18) ( <= ( - w_599 w_768) ( ~ 19))) |
---|
| 937 | ( or ( not v_599_8 ) ( not v_768_8 ) ( >= ( - w_599 w_768) 19) ( <= ( - w_599 w_768) ( ~ 19))) |
---|
| 938 | ( or ( not v_600_2 ) ( not v_665_2 ) ( >= ( - w_600 w_665) 25) ( <= ( - w_600 w_665) ( ~ 25))) |
---|
| 939 | ( or ( not v_600_2 ) ( not v_665_8 ) ( >= ( - w_600 w_665) 25) ( <= ( - w_600 w_665) ( ~ 25))) |
---|
| 940 | ( or ( not v_600_8 ) ( not v_665_2 ) ( >= ( - w_600 w_665) 25) ( <= ( - w_600 w_665) ( ~ 25))) |
---|
| 941 | ( or ( not v_600_8 ) ( not v_665_8 ) ( >= ( - w_600 w_665) 25) ( <= ( - w_600 w_665) ( ~ 25))) |
---|
| 942 | ( or ( not v_600_2 ) ( not v_666_2 ) ( >= ( - w_600 w_666) 15) ( <= ( - w_600 w_666) ( ~ 15))) |
---|
| 943 | ( or ( not v_600_2 ) ( not v_666_8 ) ( >= ( - w_600 w_666) 15) ( <= ( - w_600 w_666) ( ~ 14))) |
---|
| 944 | ( or ( not v_600_8 ) ( not v_666_2 ) ( >= ( - w_600 w_666) 14) ( <= ( - w_600 w_666) ( ~ 15))) |
---|
| 945 | ( or ( not v_600_8 ) ( not v_666_8 ) ( >= ( - w_600 w_666) 15) ( <= ( - w_600 w_666) ( ~ 15))) |
---|
| 946 | ( or ( not v_600_2 ) ( not v_767_2 ) ( >= ( - w_600 w_767) 19) ( <= ( - w_600 w_767) ( ~ 19))) |
---|
| 947 | ( or ( not v_600_2 ) ( not v_767_8 ) ( >= ( - w_600 w_767) 19) ( <= ( - w_600 w_767) ( ~ 18))) |
---|
| 948 | ( or ( not v_600_8 ) ( not v_767_2 ) ( >= ( - w_600 w_767) 18) ( <= ( - w_600 w_767) ( ~ 19))) |
---|
| 949 | ( or ( not v_600_8 ) ( not v_767_8 ) ( >= ( - w_600 w_767) 19) ( <= ( - w_600 w_767) ( ~ 19))) |
---|
| 950 | ( or ( not v_600_2 ) ( not v_768_2 ) ( >= ( - w_600 w_768) 29) ( <= ( - w_600 w_768) ( ~ 29))) |
---|
| 951 | ( or ( not v_600_2 ) ( not v_768_8 ) ( >= ( - w_600 w_768) 30) ( <= ( - w_600 w_768) ( ~ 29))) |
---|
| 952 | ( or ( not v_600_8 ) ( not v_768_2 ) ( >= ( - w_600 w_768) 29) ( <= ( - w_600 w_768) ( ~ 30))) |
---|
| 953 | ( or ( not v_600_8 ) ( not v_768_8 ) ( >= ( - w_600 w_768) 29) ( <= ( - w_600 w_768) ( ~ 29))) |
---|
| 954 | ( or ( not v_613_2 ) ( not v_614_2 ) ( = ( - w_613 w_614) 17) ( = ( - w_614 w_613) 17)) |
---|
| 955 | ( or ( not v_613_2 ) ( not v_614_8 )) |
---|
| 956 | ( or ( not v_613_8 ) ( not v_614_2 )) |
---|
| 957 | ( or ( not v_613_8 ) ( not v_614_8 ) ( = ( - w_613 w_614) 17) ( = ( - w_614 w_613) 17)) |
---|
| 958 | ( or ( not v_613_2 ) ( not v_665_2 ) ( >= ( - w_613 w_665) 16) ( <= ( - w_613 w_665) ( ~ 16))) |
---|
| 959 | ( or ( not v_613_2 ) ( not v_665_8 ) ( >= ( - w_613 w_665) 16) ( <= ( - w_613 w_665) ( ~ 16))) |
---|
| 960 | ( or ( not v_613_8 ) ( not v_665_2 ) ( >= ( - w_613 w_665) 16) ( <= ( - w_613 w_665) ( ~ 16))) |
---|
| 961 | ( or ( not v_613_8 ) ( not v_665_8 ) ( >= ( - w_613 w_665) 16) ( <= ( - w_613 w_665) ( ~ 16))) |
---|
| 962 | ( or ( not v_613_2 ) ( not v_666_2 ) ( >= ( - w_613 w_666) 3) ( <= ( - w_613 w_666) ( ~ 3))) |
---|
| 963 | ( or ( not v_613_2 ) ( not v_666_8 ) ( >= ( - w_613 w_666) 4) ( <= ( - w_613 w_666) ( ~ 3))) |
---|
| 964 | ( or ( not v_613_8 ) ( not v_666_2 ) ( >= ( - w_613 w_666) 3) ( <= ( - w_613 w_666) ( ~ 4))) |
---|
| 965 | ( or ( not v_613_8 ) ( not v_666_8 ) ( >= ( - w_613 w_666) 3) ( <= ( - w_613 w_666) ( ~ 3))) |
---|
| 966 | ( or ( not v_613_2 ) ( not v_765_2 ) ( >= ( - w_613 w_765) 4) ( <= ( - w_613 w_765) ( ~ 4))) |
---|
| 967 | ( or ( not v_613_2 ) ( not v_765_8 ) ( >= ( - w_613 w_765) 4) ( <= ( - w_613 w_765) ( ~ 3))) |
---|
| 968 | ( or ( not v_613_8 ) ( not v_765_2 ) ( >= ( - w_613 w_765) 3) ( <= ( - w_613 w_765) ( ~ 4))) |
---|
| 969 | ( or ( not v_613_8 ) ( not v_765_8 ) ( >= ( - w_613 w_765) 4) ( <= ( - w_613 w_765) ( ~ 4))) |
---|
| 970 | ( or ( not v_613_2 ) ( not v_766_2 ) ( >= ( - w_613 w_766) 16) ( <= ( - w_613 w_766) ( ~ 16))) |
---|
| 971 | ( or ( not v_613_2 ) ( not v_766_8 ) ( >= ( - w_613 w_766) 17) ( <= ( - w_613 w_766) ( ~ 16))) |
---|
| 972 | ( or ( not v_613_8 ) ( not v_766_2 ) ( >= ( - w_613 w_766) 16) ( <= ( - w_613 w_766) ( ~ 17))) |
---|
| 973 | ( or ( not v_613_8 ) ( not v_766_8 ) ( >= ( - w_613 w_766) 16) ( <= ( - w_613 w_766) ( ~ 16))) |
---|
| 974 | ( or ( not v_613_2 ) ( not v_768_2 ) ( >= ( - w_613 w_768) 19) ( <= ( - w_613 w_768) ( ~ 19))) |
---|
| 975 | ( or ( not v_613_2 ) ( not v_768_8 ) ( >= ( - w_613 w_768) 19) ( <= ( - w_613 w_768) ( ~ 18))) |
---|
| 976 | ( or ( not v_613_8 ) ( not v_768_2 ) ( >= ( - w_613 w_768) 18) ( <= ( - w_613 w_768) ( ~ 19))) |
---|
| 977 | ( or ( not v_613_8 ) ( not v_768_8 ) ( >= ( - w_613 w_768) 19) ( <= ( - w_613 w_768) ( ~ 19))) |
---|
| 978 | ( or ( not v_613_2 ) ( not v_785_2 ) ( >= ( - w_613 w_785) 2) ( <= ( - w_613 w_785) ( ~ 2))) |
---|
| 979 | ( or ( not v_613_2 ) ( not v_785_8 ) ( >= ( - w_613 w_785) 3) ( <= ( - w_613 w_785) ( ~ 2))) |
---|
| 980 | ( or ( not v_613_8 ) ( not v_785_2 ) ( >= ( - w_613 w_785) 2) ( <= ( - w_613 w_785) ( ~ 3))) |
---|
| 981 | ( or ( not v_613_8 ) ( not v_785_8 ) ( >= ( - w_613 w_785) 2) ( <= ( - w_613 w_785) ( ~ 2))) |
---|
| 982 | ( or ( not v_613_2 ) ( not v_786_2 ) ( >= ( - w_613 w_786) 13) ( <= ( - w_613 w_786) ( ~ 13))) |
---|
| 983 | ( or ( not v_613_2 ) ( not v_786_8 ) ( >= ( - w_613 w_786) 13) ( <= ( - w_613 w_786) ( ~ 12))) |
---|
| 984 | ( or ( not v_613_8 ) ( not v_786_2 ) ( >= ( - w_613 w_786) 12) ( <= ( - w_613 w_786) ( ~ 13))) |
---|
| 985 | ( or ( not v_613_8 ) ( not v_786_8 ) ( >= ( - w_613 w_786) 13) ( <= ( - w_613 w_786) ( ~ 13))) |
---|
| 986 | ( or ( not v_614_2 ) ( not v_665_2 ) ( >= ( - w_614 w_665) 26) ( <= ( - w_614 w_665) ( ~ 26))) |
---|
| 987 | ( or ( not v_614_2 ) ( not v_665_8 ) ( >= ( - w_614 w_665) 27) ( <= ( - w_614 w_665) ( ~ 26))) |
---|
| 988 | ( or ( not v_614_8 ) ( not v_665_2 ) ( >= ( - w_614 w_665) 26) ( <= ( - w_614 w_665) ( ~ 27))) |
---|
| 989 | ( or ( not v_614_8 ) ( not v_665_8 ) ( >= ( - w_614 w_665) 26) ( <= ( - w_614 w_665) ( ~ 26))) |
---|
| 990 | ( or ( not v_614_2 ) ( not v_666_2 ) ( >= ( - w_614 w_666) 16) ( <= ( - w_614 w_666) ( ~ 16))) |
---|
| 991 | ( or ( not v_614_2 ) ( not v_666_8 ) ( >= ( - w_614 w_666) 16) ( <= ( - w_614 w_666) ( ~ 16))) |
---|
| 992 | ( or ( not v_614_8 ) ( not v_666_2 ) ( >= ( - w_614 w_666) 16) ( <= ( - w_614 w_666) ( ~ 16))) |
---|
| 993 | ( or ( not v_614_8 ) ( not v_666_8 ) ( >= ( - w_614 w_666) 16) ( <= ( - w_614 w_666) ( ~ 16))) |
---|
| 994 | ( or ( not v_614_2 ) ( not v_765_2 ) ( >= ( - w_614 w_765) 9) ( <= ( - w_614 w_765) ( ~ 9))) |
---|
| 995 | ( or ( not v_614_2 ) ( not v_765_8 ) ( >= ( - w_614 w_765) 10) ( <= ( - w_614 w_765) ( ~ 9))) |
---|
| 996 | ( or ( not v_614_8 ) ( not v_765_2 ) ( >= ( - w_614 w_765) 9) ( <= ( - w_614 w_765) ( ~ 10))) |
---|
| 997 | ( or ( not v_614_8 ) ( not v_765_8 ) ( >= ( - w_614 w_765) 9) ( <= ( - w_614 w_765) ( ~ 9))) |
---|
| 998 | ( or ( not v_614_2 ) ( not v_766_2 ) ( >= ( - w_614 w_766) 4) ( <= ( - w_614 w_766) ( ~ 4))) |
---|
| 999 | ( or ( not v_614_2 ) ( not v_766_8 ) ( >= ( - w_614 w_766) 4) ( <= ( - w_614 w_766) ( ~ 3))) |
---|
| 1000 | ( or ( not v_614_8 ) ( not v_766_2 ) ( >= ( - w_614 w_766) 3) ( <= ( - w_614 w_766) ( ~ 4))) |
---|
| 1001 | ( or ( not v_614_8 ) ( not v_766_8 ) ( >= ( - w_614 w_766) 4) ( <= ( - w_614 w_766) ( ~ 4))) |
---|
| 1002 | ( or ( not v_614_2 ) ( not v_767_2 ) ( >= ( - w_614 w_767) 19) ( <= ( - w_614 w_767) ( ~ 19))) |
---|
| 1003 | ( or ( not v_614_2 ) ( not v_767_8 ) ( >= ( - w_614 w_767) 19) ( <= ( - w_614 w_767) ( ~ 18))) |
---|
| 1004 | ( or ( not v_614_8 ) ( not v_767_2 ) ( >= ( - w_614 w_767) 18) ( <= ( - w_614 w_767) ( ~ 19))) |
---|
| 1005 | ( or ( not v_614_8 ) ( not v_767_8 ) ( >= ( - w_614 w_767) 19) ( <= ( - w_614 w_767) ( ~ 19))) |
---|
| 1006 | ( or ( not v_614_2 ) ( not v_768_2 ) ( >= ( - w_614 w_768) 30) ( <= ( - w_614 w_768) ( ~ 30))) |
---|
| 1007 | ( or ( not v_614_2 ) ( not v_768_8 ) ( >= ( - w_614 w_768) 31) ( <= ( - w_614 w_768) ( ~ 30))) |
---|
| 1008 | ( or ( not v_614_8 ) ( not v_768_2 ) ( >= ( - w_614 w_768) 30) ( <= ( - w_614 w_768) ( ~ 31))) |
---|
| 1009 | ( or ( not v_614_8 ) ( not v_768_8 ) ( >= ( - w_614 w_768) 30) ( <= ( - w_614 w_768) ( ~ 30))) |
---|
| 1010 | ( or ( not v_614_2 ) ( not v_785_2 ) ( >= ( - w_614 w_785) 13) ( <= ( - w_614 w_785) ( ~ 13))) |
---|
| 1011 | ( or ( not v_614_2 ) ( not v_785_8 ) ( >= ( - w_614 w_785) 14) ( <= ( - w_614 w_785) ( ~ 13))) |
---|
| 1012 | ( or ( not v_614_8 ) ( not v_785_2 ) ( >= ( - w_614 w_785) 13) ( <= ( - w_614 w_785) ( ~ 14))) |
---|
| 1013 | ( or ( not v_614_8 ) ( not v_785_8 ) ( >= ( - w_614 w_785) 13) ( <= ( - w_614 w_785) ( ~ 13))) |
---|
| 1014 | ( or ( not v_614_2 ) ( not v_786_2 ) ( >= ( - w_614 w_786) 2) ( <= ( - w_614 w_786) ( ~ 2))) |
---|
| 1015 | ( or ( not v_614_2 ) ( not v_786_8 ) ( >= ( - w_614 w_786) 3) ( <= ( - w_614 w_786) ( ~ 2))) |
---|
| 1016 | ( or ( not v_614_8 ) ( not v_786_2 ) ( >= ( - w_614 w_786) 2) ( <= ( - w_614 w_786) ( ~ 3))) |
---|
| 1017 | ( or ( not v_614_8 ) ( not v_786_8 ) ( >= ( - w_614 w_786) 2) ( <= ( - w_614 w_786) ( ~ 2))) |
---|
| 1018 | ( or ( not v_629_2 ) ( not v_630_2 ) ( = ( - w_629 w_630) 17) ( = ( - w_630 w_629) 17)) |
---|
| 1019 | ( or ( not v_629_2 ) ( not v_630_8 )) |
---|
| 1020 | ( or ( not v_629_8 ) ( not v_630_2 )) |
---|
| 1021 | ( or ( not v_629_8 ) ( not v_630_8 ) ( = ( - w_629 w_630) 17) ( = ( - w_630 w_629) 17)) |
---|
| 1022 | ( or ( not v_629_2 ) ( not v_631_2 ) ( >= ( - w_629 w_631) 19) ( <= ( - w_629 w_631) ( ~ 19))) |
---|
| 1023 | ( or ( not v_629_2 ) ( not v_631_8 ) ( >= ( - w_629 w_631) 20) ( <= ( - w_629 w_631) ( ~ 19))) |
---|
| 1024 | ( or ( not v_629_8 ) ( not v_631_2 ) ( >= ( - w_629 w_631) 19) ( <= ( - w_629 w_631) ( ~ 20))) |
---|
| 1025 | ( or ( not v_629_8 ) ( not v_631_8 ) ( >= ( - w_629 w_631) 19) ( <= ( - w_629 w_631) ( ~ 19))) |
---|
| 1026 | ( or ( not v_629_2 ) ( not v_632_2 ) ( >= ( - w_629 w_632) 9) ( <= ( - w_629 w_632) ( ~ 9))) |
---|
| 1027 | ( or ( not v_629_2 ) ( not v_632_8 ) ( >= ( - w_629 w_632) 10) ( <= ( - w_629 w_632) ( ~ 9))) |
---|
| 1028 | ( or ( not v_629_8 ) ( not v_632_2 ) ( >= ( - w_629 w_632) 9) ( <= ( - w_629 w_632) ( ~ 10))) |
---|
| 1029 | ( or ( not v_629_8 ) ( not v_632_8 ) ( >= ( - w_629 w_632) 9) ( <= ( - w_629 w_632) ( ~ 9))) |
---|
| 1030 | ( or ( not v_629_2 ) ( not v_768_2 ) ( >= ( - w_629 w_768) 10) ( <= ( - w_629 w_768) ( ~ 10))) |
---|
| 1031 | ( or ( not v_629_2 ) ( not v_768_8 ) ( >= ( - w_629 w_768) 10) ( <= ( - w_629 w_768) ( ~ 10))) |
---|
| 1032 | ( or ( not v_629_8 ) ( not v_768_2 ) ( >= ( - w_629 w_768) 10) ( <= ( - w_629 w_768) ( ~ 10))) |
---|
| 1033 | ( or ( not v_629_8 ) ( not v_768_8 ) ( >= ( - w_629 w_768) 10) ( <= ( - w_629 w_768) ( ~ 10))) |
---|
| 1034 | ( or ( not v_630_2 ) ( not v_631_2 ) ( >= ( - w_630 w_631) 32) ( <= ( - w_630 w_631) ( ~ 32))) |
---|
| 1035 | ( or ( not v_630_2 ) ( not v_631_8 ) ( >= ( - w_630 w_631) 32) ( <= ( - w_630 w_631) ( ~ 32))) |
---|
| 1036 | ( or ( not v_630_8 ) ( not v_631_2 ) ( >= ( - w_630 w_631) 32) ( <= ( - w_630 w_631) ( ~ 32))) |
---|
| 1037 | ( or ( not v_630_8 ) ( not v_631_8 ) ( >= ( - w_630 w_631) 32) ( <= ( - w_630 w_631) ( ~ 32))) |
---|
| 1038 | ( or ( not v_630_2 ) ( not v_632_2 ) ( >= ( - w_630 w_632) 19) ( <= ( - w_630 w_632) ( ~ 19))) |
---|
| 1039 | ( or ( not v_630_2 ) ( not v_632_8 ) ( >= ( - w_630 w_632) 20) ( <= ( - w_630 w_632) ( ~ 19))) |
---|
| 1040 | ( or ( not v_630_8 ) ( not v_632_2 ) ( >= ( - w_630 w_632) 19) ( <= ( - w_630 w_632) ( ~ 20))) |
---|
| 1041 | ( or ( not v_630_8 ) ( not v_632_8 ) ( >= ( - w_630 w_632) 19) ( <= ( - w_630 w_632) ( ~ 19))) |
---|
| 1042 | ( or ( not v_630_2 ) ( not v_768_2 ) ( >= ( - w_630 w_768) 3) ( <= ( - w_630 w_768) ( ~ 3))) |
---|
| 1043 | ( or ( not v_630_2 ) ( not v_768_8 ) ( >= ( - w_630 w_768) 3) ( <= ( - w_630 w_768) ( ~ 2))) |
---|
| 1044 | ( or ( not v_630_8 ) ( not v_768_2 ) ( >= ( - w_630 w_768) 2) ( <= ( - w_630 w_768) ( ~ 3))) |
---|
| 1045 | ( or ( not v_630_8 ) ( not v_768_8 ) ( >= ( - w_630 w_768) 3) ( <= ( - w_630 w_768) ( ~ 3))) |
---|
| 1046 | ( or ( not v_631_2 ) ( not v_632_2 ) ( = ( - w_631 w_632) 17) ( = ( - w_632 w_631) 17)) |
---|
| 1047 | ( or ( not v_631_2 ) ( not v_632_8 )) |
---|
| 1048 | ( or ( not v_631_8 ) ( not v_632_2 )) |
---|
| 1049 | ( or ( not v_631_8 ) ( not v_632_8 ) ( = ( - w_631 w_632) 17) ( = ( - w_632 w_631) 17)) |
---|
| 1050 | ( or ( not v_631_2 ) ( not v_767_2 ) ( >= ( - w_631 w_767) 18) ( <= ( - w_631 w_767) ( ~ 18))) |
---|
| 1051 | ( or ( not v_631_2 ) ( not v_767_8 ) ( >= ( - w_631 w_767) 18) ( <= ( - w_631 w_767) ( ~ 17))) |
---|
| 1052 | ( or ( not v_631_8 ) ( not v_767_2 ) ( >= ( - w_631 w_767) 17) ( <= ( - w_631 w_767) ( ~ 18))) |
---|
| 1053 | ( or ( not v_631_8 ) ( not v_767_8 ) ( >= ( - w_631 w_767) 18) ( <= ( - w_631 w_767) ( ~ 18))) |
---|
| 1054 | ( or ( not v_631_2 ) ( not v_768_2 ) ( >= ( - w_631 w_768) 29) ( <= ( - w_631 w_768) ( ~ 29))) |
---|
| 1055 | ( or ( not v_631_2 ) ( not v_768_8 ) ( >= ( - w_631 w_768) 29) ( <= ( - w_631 w_768) ( ~ 29))) |
---|
| 1056 | ( or ( not v_631_8 ) ( not v_768_2 ) ( >= ( - w_631 w_768) 29) ( <= ( - w_631 w_768) ( ~ 29))) |
---|
| 1057 | ( or ( not v_631_8 ) ( not v_768_8 ) ( >= ( - w_631 w_768) 29) ( <= ( - w_631 w_768) ( ~ 29))) |
---|
| 1058 | ( or ( not v_632_2 ) ( not v_767_2 ) ( >= ( - w_632 w_767) 6) ( <= ( - w_632 w_767) ( ~ 6))) |
---|
| 1059 | ( or ( not v_632_2 ) ( not v_767_8 ) ( >= ( - w_632 w_767) 7) ( <= ( - w_632 w_767) ( ~ 6))) |
---|
| 1060 | ( or ( not v_632_8 ) ( not v_767_2 ) ( >= ( - w_632 w_767) 6) ( <= ( - w_632 w_767) ( ~ 7))) |
---|
| 1061 | ( or ( not v_632_8 ) ( not v_767_8 ) ( >= ( - w_632 w_767) 6) ( <= ( - w_632 w_767) ( ~ 6))) |
---|
| 1062 | ( or ( not v_665_2 ) ( not v_666_2 ) ( = ( - w_665 w_666) 17) ( = ( - w_666 w_665) 17)) |
---|
| 1063 | ( or ( not v_665_2 ) ( not v_666_8 )) |
---|
| 1064 | ( or ( not v_665_8 ) ( not v_666_2 )) |
---|
| 1065 | ( or ( not v_665_8 ) ( not v_666_8 ) ( = ( - w_665 w_666) 17) ( = ( - w_666 w_665) 17)) |
---|
| 1066 | ( or ( not v_665_2 ) ( not v_767_2 ) ( >= ( - w_665 w_767) 9) ( <= ( - w_665 w_767) ( ~ 9))) |
---|
| 1067 | ( or ( not v_665_2 ) ( not v_767_8 ) ( >= ( - w_665 w_767) 10) ( <= ( - w_665 w_767) ( ~ 9))) |
---|
| 1068 | ( or ( not v_665_8 ) ( not v_767_2 ) ( >= ( - w_665 w_767) 9) ( <= ( - w_665 w_767) ( ~ 10))) |
---|
| 1069 | ( or ( not v_665_8 ) ( not v_767_8 ) ( >= ( - w_665 w_767) 9) ( <= ( - w_665 w_767) ( ~ 9))) |
---|
| 1070 | ( or ( not v_665_2 ) ( not v_768_2 ) ( >= ( - w_665 w_768) 5) ( <= ( - w_665 w_768) ( ~ 5))) |
---|
| 1071 | ( or ( not v_665_2 ) ( not v_768_8 ) ( >= ( - w_665 w_768) 5) ( <= ( - w_665 w_768) ( ~ 4))) |
---|
| 1072 | ( or ( not v_665_8 ) ( not v_768_2 ) ( >= ( - w_665 w_768) 4) ( <= ( - w_665 w_768) ( ~ 5))) |
---|
| 1073 | ( or ( not v_665_8 ) ( not v_768_8 ) ( >= ( - w_665 w_768) 5) ( <= ( - w_665 w_768) ( ~ 5))) |
---|
| 1074 | ( or ( not v_665_2 ) ( not v_785_2 ) ( >= ( - w_665 w_785) 16) ( <= ( - w_665 w_785) ( ~ 16))) |
---|
| 1075 | ( or ( not v_665_2 ) ( not v_785_8 ) ( >= ( - w_665 w_785) 16) ( <= ( - w_665 w_785) ( ~ 16))) |
---|
| 1076 | ( or ( not v_665_8 ) ( not v_785_2 ) ( >= ( - w_665 w_785) 16) ( <= ( - w_665 w_785) ( ~ 16))) |
---|
| 1077 | ( or ( not v_665_8 ) ( not v_785_8 ) ( >= ( - w_665 w_785) 16) ( <= ( - w_665 w_785) ( ~ 16))) |
---|
| 1078 | ( or ( not v_665_2 ) ( not v_786_2 ) ( >= ( - w_665 w_786) 26) ( <= ( - w_665 w_786) ( ~ 26))) |
---|
| 1079 | ( or ( not v_665_2 ) ( not v_786_8 ) ( >= ( - w_665 w_786) 27) ( <= ( - w_665 w_786) ( ~ 26))) |
---|
| 1080 | ( or ( not v_665_8 ) ( not v_786_2 ) ( >= ( - w_665 w_786) 26) ( <= ( - w_665 w_786) ( ~ 27))) |
---|
| 1081 | ( or ( not v_665_8 ) ( not v_786_8 ) ( >= ( - w_665 w_786) 26) ( <= ( - w_665 w_786) ( ~ 26))) |
---|
| 1082 | ( or ( not v_666_2 ) ( not v_767_2 ) ( >= ( - w_666 w_767) 5) ( <= ( - w_666 w_767) ( ~ 5))) |
---|
| 1083 | ( or ( not v_666_2 ) ( not v_767_8 ) ( >= ( - w_666 w_767) 5) ( <= ( - w_666 w_767) ( ~ 4))) |
---|
| 1084 | ( or ( not v_666_8 ) ( not v_767_2 ) ( >= ( - w_666 w_767) 4) ( <= ( - w_666 w_767) ( ~ 5))) |
---|
| 1085 | ( or ( not v_666_8 ) ( not v_767_8 ) ( >= ( - w_666 w_767) 5) ( <= ( - w_666 w_767) ( ~ 5))) |
---|
| 1086 | ( or ( not v_666_2 ) ( not v_768_2 ) ( >= ( - w_666 w_768) 17) ( <= ( - w_666 w_768) ( ~ 17))) |
---|
| 1087 | ( or ( not v_666_2 ) ( not v_768_8 ) ( >= ( - w_666 w_768) 18) ( <= ( - w_666 w_768) ( ~ 17))) |
---|
| 1088 | ( or ( not v_666_8 ) ( not v_768_2 ) ( >= ( - w_666 w_768) 17) ( <= ( - w_666 w_768) ( ~ 18))) |
---|
| 1089 | ( or ( not v_666_8 ) ( not v_768_8 ) ( >= ( - w_666 w_768) 17) ( <= ( - w_666 w_768) ( ~ 17))) |
---|
| 1090 | ( or ( not v_666_2 ) ( not v_785_2 ) ( >= ( - w_666 w_785) 4) ( <= ( - w_666 w_785) ( ~ 4))) |
---|
| 1091 | ( or ( not v_666_2 ) ( not v_785_8 ) ( >= ( - w_666 w_785) 4) ( <= ( - w_666 w_785) ( ~ 3))) |
---|
| 1092 | ( or ( not v_666_8 ) ( not v_785_2 ) ( >= ( - w_666 w_785) 3) ( <= ( - w_666 w_785) ( ~ 4))) |
---|
| 1093 | ( or ( not v_666_8 ) ( not v_785_8 ) ( >= ( - w_666 w_785) 4) ( <= ( - w_666 w_785) ( ~ 4))) |
---|
| 1094 | ( or ( not v_666_2 ) ( not v_786_2 ) ( >= ( - w_666 w_786) 16) ( <= ( - w_666 w_786) ( ~ 16))) |
---|
| 1095 | ( or ( not v_666_2 ) ( not v_786_8 ) ( >= ( - w_666 w_786) 16) ( <= ( - w_666 w_786) ( ~ 15))) |
---|
| 1096 | ( or ( not v_666_8 ) ( not v_786_2 ) ( >= ( - w_666 w_786) 15) ( <= ( - w_666 w_786) ( ~ 16))) |
---|
| 1097 | ( or ( not v_666_8 ) ( not v_786_8 ) ( >= ( - w_666 w_786) 16) ( <= ( - w_666 w_786) ( ~ 16))) |
---|
| 1098 | ( or ( not v_765_2 ) ( not v_766_2 ) ( = ( - w_765 w_766) 17) ( = ( - w_766 w_765) 17)) |
---|
| 1099 | ( or ( not v_765_2 ) ( not v_766_8 )) |
---|
| 1100 | ( or ( not v_765_8 ) ( not v_766_2 )) |
---|
| 1101 | ( or ( not v_765_8 ) ( not v_766_8 ) ( = ( - w_765 w_766) 17) ( = ( - w_766 w_765) 17)) |
---|
| 1102 | ( or ( not v_765_2 ) ( not v_767_2 ) ( >= ( - w_765 w_767) 11) ( <= ( - w_765 w_767) ( ~ 11))) |
---|
| 1103 | ( or ( not v_765_2 ) ( not v_767_8 ) ( >= ( - w_765 w_767) 11) ( <= ( - w_765 w_767) ( ~ 10))) |
---|
| 1104 | ( or ( not v_765_8 ) ( not v_767_2 ) ( >= ( - w_765 w_767) 10) ( <= ( - w_765 w_767) ( ~ 11))) |
---|
| 1105 | ( or ( not v_765_8 ) ( not v_767_8 ) ( >= ( - w_765 w_767) 11) ( <= ( - w_765 w_767) ( ~ 11))) |
---|
| 1106 | ( or ( not v_767_2 ) ( not v_768_2 ) ( = ( - w_767 w_768) 17) ( = ( - w_768 w_767) 17)) |
---|
| 1107 | ( or ( not v_767_2 ) ( not v_768_8 )) |
---|
| 1108 | ( or ( not v_767_8 ) ( not v_768_2 )) |
---|
| 1109 | ( or ( not v_767_8 ) ( not v_768_8 ) ( = ( - w_767 w_768) 17) ( = ( - w_768 w_767) 17)) |
---|
| 1110 | ( or ( not v_767_2 ) ( not v_785_2 ) ( >= ( - w_767 w_785) 8) ( <= ( - w_767 w_785) ( ~ 8))) |
---|
| 1111 | ( or ( not v_767_2 ) ( not v_785_8 ) ( >= ( - w_767 w_785) 8) ( <= ( - w_767 w_785) ( ~ 7))) |
---|
| 1112 | ( or ( not v_767_8 ) ( not v_785_2 ) ( >= ( - w_767 w_785) 7) ( <= ( - w_767 w_785) ( ~ 8))) |
---|
| 1113 | ( or ( not v_767_8 ) ( not v_785_8 ) ( >= ( - w_767 w_785) 8) ( <= ( - w_767 w_785) ( ~ 8))) |
---|
| 1114 | ( or ( not v_767_2 ) ( not v_786_2 ) ( >= ( - w_767 w_786) 19) ( <= ( - w_767 w_786) ( ~ 19))) |
---|
| 1115 | ( or ( not v_767_2 ) ( not v_786_8 ) ( >= ( - w_767 w_786) 19) ( <= ( - w_767 w_786) ( ~ 19))) |
---|
| 1116 | ( or ( not v_767_8 ) ( not v_786_2 ) ( >= ( - w_767 w_786) 19) ( <= ( - w_767 w_786) ( ~ 19))) |
---|
| 1117 | ( or ( not v_767_8 ) ( not v_786_8 ) ( >= ( - w_767 w_786) 19) ( <= ( - w_767 w_786) ( ~ 19))) |
---|
| 1118 | ( or ( not v_768_2 ) ( not v_785_2 ) ( >= ( - w_768 w_785) 19) ( <= ( - w_768 w_785) ( ~ 19))) |
---|
| 1119 | ( or ( not v_768_2 ) ( not v_785_8 ) ( >= ( - w_768 w_785) 19) ( <= ( - w_768 w_785) ( ~ 19))) |
---|
| 1120 | ( or ( not v_768_8 ) ( not v_785_2 ) ( >= ( - w_768 w_785) 19) ( <= ( - w_768 w_785) ( ~ 19))) |
---|
| 1121 | ( or ( not v_768_8 ) ( not v_785_8 ) ( >= ( - w_768 w_785) 19) ( <= ( - w_768 w_785) ( ~ 19))) |
---|
| 1122 | ( or ( not v_785_2 ) ( not v_786_2 ) ( = ( - w_785 w_786) 17) ( = ( - w_786 w_785) 17)) |
---|
| 1123 | ( or ( not v_785_2 ) ( not v_786_8 )) |
---|
| 1124 | ( or ( not v_785_8 ) ( not v_786_2 )) |
---|
| 1125 | ( or ( not v_785_8 ) ( not v_786_8 ) ( = ( - w_785 w_786) 17) ( = ( - w_786 w_785) 17)) |
---|
| 1126 | ) |
---|
| 1127 | ) |
---|