[12] | 1 | (benchmark DTP_k2_n35_c175_s1.smt |
---|
| 2 | :source { |
---|
| 3 | Randomly generated benchmarks. Contact TSAT++ group at |
---|
| 4 | http://www.ai.dist.unige.it/Tsat for more information. |
---|
| 5 | |
---|
| 6 | Translated into SMT-LIB format by Albert Oliveras. |
---|
| 7 | } |
---|
| 8 | :status sat |
---|
| 9 | :category { random } |
---|
| 10 | :difficulty { 1 } |
---|
| 11 | :logic QF_IDL |
---|
| 12 | :extrafuns ((x31 Int)) |
---|
| 13 | :extrafuns ((x13 Int)) |
---|
| 14 | :extrafuns ((x10 Int)) |
---|
| 15 | :extrafuns ((x0 Int)) |
---|
| 16 | :extrafuns ((x1 Int)) |
---|
| 17 | :extrafuns ((x11 Int)) |
---|
| 18 | :extrafuns ((x12 Int)) |
---|
| 19 | :extrafuns ((x20 Int)) |
---|
| 20 | :extrafuns ((x16 Int)) |
---|
| 21 | :extrafuns ((x14 Int)) |
---|
| 22 | :extrafuns ((x15 Int)) |
---|
| 23 | :extrafuns ((x19 Int)) |
---|
| 24 | :extrafuns ((x18 Int)) |
---|
| 25 | :extrafuns ((x17 Int)) |
---|
| 26 | :extrafuns ((x2 Int)) |
---|
| 27 | :extrafuns ((x27 Int)) |
---|
| 28 | :extrafuns ((x24 Int)) |
---|
| 29 | :extrafuns ((x23 Int)) |
---|
| 30 | :extrafuns ((x22 Int)) |
---|
| 31 | :extrafuns ((x21 Int)) |
---|
| 32 | :extrafuns ((x25 Int)) |
---|
| 33 | :extrafuns ((x26 Int)) |
---|
| 34 | :extrafuns ((x28 Int)) |
---|
| 35 | :extrafuns ((x30 Int)) |
---|
| 36 | :extrafuns ((x29 Int)) |
---|
| 37 | :extrafuns ((x3 Int)) |
---|
| 38 | :extrafuns ((x4 Int)) |
---|
| 39 | :extrafuns ((x33 Int)) |
---|
| 40 | :extrafuns ((x32 Int)) |
---|
| 41 | :extrafuns ((x34 Int)) |
---|
| 42 | :extrafuns ((x8 Int)) |
---|
| 43 | :extrafuns ((x5 Int)) |
---|
| 44 | :extrafuns ((x6 Int)) |
---|
| 45 | :extrafuns ((x7 Int)) |
---|
| 46 | :extrafuns ((x9 Int)) |
---|
| 47 | :formula |
---|
| 48 | ( and |
---|
| 49 | (or ( >= ( - x31 x4 ) 67 ) (not ( >= ( - x13 x20 ) 73 )) ) |
---|
| 50 | (or ( >= ( - x16 x14 ) 86 ) ( >= ( - x16 x4 ) 60 ) ) |
---|
| 51 | (or ( >= ( - x10 x19 ) 90 ) ( >= ( - x10 x8 ) 14 ) ) |
---|
| 52 | (or ( >= ( - x16 x11 ) 22 ) (not ( >= ( - x4 x27 ) 79 )) ) |
---|
| 53 | (or (not ( >= ( - x9 x15 ) 99 )) ( >= ( - x14 x8 ) 77 ) ) |
---|
| 54 | (or ( >= ( - x31 x5 ) 71 ) (not ( >= ( - x10 x33 ) 52 )) ) |
---|
| 55 | (or (not ( >= ( - x27 x12 ) 47 )) (not ( >= ( - x20 x13 ) 88 )) ) |
---|
| 56 | (or ( >= ( - x24 x12 ) 21 ) (not ( >= ( - x25 x13 ) 10 )) ) |
---|
| 57 | (or (not ( >= ( - x32 x31 ) 19 )) ( >= ( - x6 x9 ) 91 ) ) |
---|
| 58 | (or (not ( >= ( - x28 x27 ) 88 )) ( >= ( - x24 x13 ) 64 ) ) |
---|
| 59 | (or (not ( >= ( - x31 x28 ) 53 )) ( >= ( - x30 x23 ) 57 ) ) |
---|
| 60 | (or (not ( >= ( - x34 x5 ) 97 )) ( >= ( - x0 x23 ) 35 ) ) |
---|
| 61 | (or (not ( >= ( - x16 x30 ) 74 )) (not ( >= ( - x18 x13 ) 17 )) ) |
---|
| 62 | (or (not ( >= ( - x7 x32 ) 60 )) ( >= ( - x19 x34 ) 88 ) ) |
---|
| 63 | (or (not ( >= ( - x34 x32 ) 18 )) (not ( >= ( - x19 x11 ) 32 )) ) |
---|
| 64 | (or ( >= ( - x8 x10 ) 80 ) ( >= ( - x2 x29 ) 48 ) ) |
---|
| 65 | (or (not ( >= ( - x7 x20 ) 50 )) (not ( >= ( - x25 x22 ) 65 )) ) |
---|
| 66 | (or (not ( >= ( - x17 x29 ) 51 )) (not ( >= ( - x18 x19 ) 74 )) ) |
---|
| 67 | (or ( >= ( - x14 x1 ) 93 ) ( >= ( - x27 x4 ) 64 ) ) |
---|
| 68 | (or (not ( >= ( - x17 x14 ) 14 )) ( >= ( - x27 x6 ) 50 ) ) |
---|
| 69 | (or ( >= ( - x20 x33 ) 17 ) (not ( >= ( - x2 x9 ) 13 )) ) |
---|
| 70 | (or (not ( >= ( - x21 x19 ) 54 )) (not ( >= ( - x15 x29 ) 33 )) ) |
---|
| 71 | (or ( >= ( - x20 x30 ) 19 ) (not ( >= ( - x27 x15 ) 87 )) ) |
---|
| 72 | (or ( >= ( - x14 x33 ) 68 ) (not ( >= ( - x25 x22 ) 1 )) ) |
---|
| 73 | (or (not ( >= ( - x1 x27 ) 81 )) ( >= ( - x26 x11 ) 50 ) ) |
---|
| 74 | (or (not ( >= ( - x2 x26 ) 100 )) (not ( >= ( - x28 x3 ) 98 )) ) |
---|
| 75 | (or ( >= ( - x32 x17 ) 85 ) (not ( >= ( - x27 x26 ) 9 )) ) |
---|
| 76 | (or ( >= ( - x23 x4 ) 90 ) (not ( >= ( - x3 x29 ) 25 )) ) |
---|
| 77 | (or (not ( >= ( - x20 x0 ) 76 )) (not ( >= ( - x14 x3 ) 50 )) ) |
---|
| 78 | (or ( >= ( - x15 x2 ) 77 ) (not ( >= ( - x30 x13 ) 50 )) ) |
---|
| 79 | (or (not ( >= ( - x5 x4 ) 79 )) (not ( >= ( - x29 x27 ) 63 )) ) |
---|
| 80 | (or (not ( >= ( - x14 x10 ) 72 )) (not ( >= ( - x4 x18 ) 50 )) ) |
---|
| 81 | (or (not ( >= ( - x22 x19 ) 58 )) ( >= ( - x34 x20 ) 16 ) ) |
---|
| 82 | (or ( >= ( - x0 x32 ) 3 ) (not ( >= ( - x0 x5 ) 62 )) ) |
---|
| 83 | (or (not ( >= ( - x0 x19 ) 99 )) (not ( >= ( - x10 x33 ) 1 )) ) |
---|
| 84 | (or ( >= ( - x16 x34 ) 53 ) (not ( >= ( - x22 x34 ) 62 )) ) |
---|
| 85 | (or ( >= ( - x11 x16 ) 18 ) ( >= ( - x7 x18 ) 54 ) ) |
---|
| 86 | (or (not ( >= ( - x11 x10 ) 54 )) ( >= ( - x1 x26 ) 85 ) ) |
---|
| 87 | (or ( >= ( - x28 x19 ) 61 ) (not ( >= ( - x28 x24 ) 50 )) ) |
---|
| 88 | (or (not ( >= ( - x12 x26 ) 64 )) ( >= ( - x21 x8 ) 12 ) ) |
---|
| 89 | (or ( >= ( - x34 x14 ) 71 ) (not ( >= ( - x31 x16 ) 13 )) ) |
---|
| 90 | (or ( >= ( - x34 x18 ) 89 ) ( >= ( - x24 x7 ) 18 ) ) |
---|
| 91 | (or ( >= ( - x23 x32 ) 65 ) (not ( >= ( - x6 x4 ) 22 )) ) |
---|
| 92 | (or (not ( >= ( - x2 x30 ) 42 )) ( >= ( - x4 x25 ) 40 ) ) |
---|
| 93 | (or (not ( >= ( - x6 x16 ) 66 )) ( >= ( - x4 x16 ) 93 ) ) |
---|
| 94 | (or ( >= ( - x5 x15 ) 99 ) ( >= ( - x13 x29 ) 53 ) ) |
---|
| 95 | (or (not ( >= ( - x34 x5 ) 28 )) ( >= ( - x22 x3 ) 64 ) ) |
---|
| 96 | (or (not ( >= ( - x2 x29 ) 49 )) (not ( >= ( - x14 x31 ) 74 )) ) |
---|
| 97 | (or ( >= ( - x10 x26 ) 10 ) (not ( >= ( - x32 x6 ) 96 )) ) |
---|
| 98 | (or ( >= ( - x4 x30 ) 77 ) ( >= ( - x22 x31 ) 22 ) ) |
---|
| 99 | (or ( >= ( - x34 x29 ) 64 ) (not ( >= ( - x16 x17 ) 79 )) ) |
---|
| 100 | (or (not ( >= ( - x0 x33 ) 16 )) ( >= ( - x15 x1 ) 8 ) ) |
---|
| 101 | (or ( >= ( - x11 x12 ) 68 ) (not ( >= ( - x6 x14 ) 8 )) ) |
---|
| 102 | (or ( >= ( - x21 x34 ) 94 ) (not ( >= ( - x11 x6 ) 16 )) ) |
---|
| 103 | (or ( >= ( - x15 x25 ) 66 ) (not ( >= ( - x16 x7 ) 40 )) ) |
---|
| 104 | (or ( >= ( - x26 x31 ) 21 ) (not ( >= ( - x11 x14 ) 35 )) ) |
---|
| 105 | (or (not ( >= ( - x22 x9 ) 61 )) (not ( >= ( - x7 x17 ) 37 )) ) |
---|
| 106 | (or ( >= ( - x18 x34 ) 26 ) ( >= ( - x10 x20 ) 84 ) ) |
---|
| 107 | (or (not ( >= ( - x9 x16 ) 16 )) ( >= ( - x5 x33 ) 83 ) ) |
---|
| 108 | (or ( >= ( - x29 x0 ) 21 ) (not ( >= ( - x24 x28 ) 66 )) ) |
---|
| 109 | (or (not ( >= ( - x12 x15 ) 55 )) (not ( >= ( - x14 x26 ) 44 )) ) |
---|
| 110 | (or (not ( >= ( - x4 x14 ) 95 )) (not ( >= ( - x28 x24 ) 18 )) ) |
---|
| 111 | (or (not ( >= ( - x3 x25 ) 42 )) (not ( >= ( - x11 x3 ) 48 )) ) |
---|
| 112 | (or ( >= ( - x16 x26 ) 46 ) ( >= ( - x15 x3 ) 96 ) ) |
---|
| 113 | (or ( >= ( - x26 x31 ) 54 ) (not ( >= ( - x20 x31 ) 4 )) ) |
---|
| 114 | (or ( >= ( - x14 x29 ) 12 ) ( >= ( - x28 x31 ) 20 ) ) |
---|
| 115 | (or ( >= ( - x25 x9 ) 2 ) ( >= ( - x26 x0 ) 61 ) ) |
---|
| 116 | (or (not ( >= ( - x10 x24 ) 67 )) ( >= ( - x33 x23 ) 90 ) ) |
---|
| 117 | (or (not ( >= ( - x15 x19 ) 5 )) (not ( >= ( - x22 x3 ) 68 )) ) |
---|
| 118 | (or ( >= ( - x16 x30 ) 78 ) ( >= ( - x15 x10 ) 22 ) ) |
---|
| 119 | (or ( >= ( - x4 x26 ) 65 ) (not ( >= ( - x6 x4 ) 9 )) ) |
---|
| 120 | (or (not ( >= ( - x9 x15 ) 50 )) (not ( >= ( - x17 x6 ) 5 )) ) |
---|
| 121 | (or (not ( >= ( - x22 x29 ) 15 )) (not ( >= ( - x1 x20 ) 23 )) ) |
---|
| 122 | (or (not ( >= ( - x29 x22 ) 34 )) ( >= ( - x33 x18 ) 63 ) ) |
---|
| 123 | (or ( >= ( - x1 x27 ) 6 ) ( >= ( - x0 x27 ) 18 ) ) |
---|
| 124 | (or ( >= ( - x28 x10 ) 14 ) ( >= ( - x29 x15 ) 4 ) ) |
---|
| 125 | (or ( >= ( - x3 x5 ) 91 ) (not ( >= ( - x17 x10 ) 40 )) ) |
---|
| 126 | (or ( >= ( - x2 x13 ) 11 ) (not ( >= ( - x23 x2 ) 60 )) ) |
---|
| 127 | (or ( >= ( - x12 x26 ) 8 ) ( >= ( - x29 x31 ) 52 ) ) |
---|
| 128 | (or ( >= ( - x2 x11 ) 23 ) ( >= ( - x24 x10 ) 53 ) ) |
---|
| 129 | (or ( >= ( - x22 x0 ) 64 ) ( >= ( - x33 x0 ) 55 ) ) |
---|
| 130 | (or (not ( >= ( - x10 x5 ) 40 )) (not ( >= ( - x28 x17 ) 77 )) ) |
---|
| 131 | (or ( >= ( - x18 x29 ) 84 ) ( >= ( - x6 x29 ) 41 ) ) |
---|
| 132 | (or ( >= ( - x34 x22 ) 88 ) ( >= ( - x34 x7 ) 95 ) ) |
---|
| 133 | (or (not ( >= ( - x24 x8 ) 24 )) (not ( >= ( - x13 x24 ) 68 )) ) |
---|
| 134 | (or ( >= ( - x13 x21 ) 48 ) ( >= ( - x27 x11 ) 64 ) ) |
---|
| 135 | (or ( >= ( - x10 x27 ) 63 ) ( >= ( - x1 x14 ) 26 ) ) |
---|
| 136 | (or ( >= ( - x11 x26 ) 57 ) (not ( >= ( - x21 x4 ) 90 )) ) |
---|
| 137 | (or (not ( >= ( - x10 x2 ) 12 )) (not ( >= ( - x29 x27 ) 26 )) ) |
---|
| 138 | (or (not ( >= ( - x8 x20 ) 90 )) ( >= ( - x3 x7 ) 24 ) ) |
---|
| 139 | (or (not ( >= ( - x33 x5 ) 27 )) ( >= ( - x11 x13 ) 25 ) ) |
---|
| 140 | (or (not ( >= ( - x18 x10 ) 81 )) (not ( >= ( - x4 x19 ) 26 )) ) |
---|
| 141 | (or ( >= ( - x24 x0 ) 92 ) (not ( >= ( - x0 x33 ) 95 )) ) |
---|
| 142 | (or ( >= ( - x21 x27 ) 22 ) ( >= ( - x25 x15 ) 20 ) ) |
---|
| 143 | (or (not ( >= ( - x1 x17 ) 13 )) ( >= ( - x7 x22 ) 16 ) ) |
---|
| 144 | (or ( >= ( - x7 x1 ) 89 ) (not ( >= ( - x22 x23 ) 39 )) ) |
---|
| 145 | (or ( >= ( - x24 x31 ) 39 ) (not ( >= ( - x8 x7 ) 29 )) ) |
---|
| 146 | (or ( >= ( - x33 x14 ) 71 ) (not ( >= ( - x29 x1 ) 18 )) ) |
---|
| 147 | (or (not ( >= ( - x26 x23 ) 54 )) (not ( >= ( - x28 x21 ) 44 )) ) |
---|
| 148 | (or (not ( >= ( - x32 x11 ) 89 )) ( >= ( - x14 x21 ) 80 ) ) |
---|
| 149 | (or (not ( >= ( - x23 x31 ) 38 )) (not ( >= ( - x1 x18 ) 23 )) ) |
---|
| 150 | (or (not ( >= ( - x26 x21 ) 88 )) (not ( >= ( - x29 x12 ) 39 )) ) |
---|
| 151 | (or (not ( >= ( - x28 x16 ) 18 )) ( >= ( - x25 x18 ) 14 ) ) |
---|
| 152 | (or (not ( >= ( - x1 x4 ) 78 )) (not ( >= ( - x16 x14 ) 69 )) ) |
---|
| 153 | (or (not ( >= ( - x12 x19 ) 63 )) ( >= ( - x7 x19 ) 78 ) ) |
---|
| 154 | (or (not ( >= ( - x11 x30 ) 34 )) ( >= ( - x27 x13 ) 68 ) ) |
---|
| 155 | (or (not ( >= ( - x14 x8 ) 77 )) ( >= ( - x18 x31 ) 49 ) ) |
---|
| 156 | (or (not ( >= ( - x13 x3 ) 71 )) (not ( >= ( - x20 x1 ) 1 )) ) |
---|
| 157 | (or ( >= ( - x8 x32 ) 4 ) ( >= ( - x28 x20 ) 12 ) ) |
---|
| 158 | (or (not ( >= ( - x4 x11 ) 94 )) ( >= ( - x4 x14 ) 54 ) ) |
---|
| 159 | (or (not ( >= ( - x10 x24 ) 56 )) (not ( >= ( - x1 x7 ) 2 )) ) |
---|
| 160 | (or ( >= ( - x16 x32 ) 48 ) ( >= ( - x5 x27 ) 6 ) ) |
---|
| 161 | (or (not ( >= ( - x23 x28 ) 3 )) ( >= ( - x7 x1 ) 39 ) ) |
---|
| 162 | (or ( >= ( - x14 x31 ) 44 ) ( >= ( - x34 x4 ) 57 ) ) |
---|
| 163 | (or ( >= ( - x6 x4 ) 12 ) (not ( >= ( - x2 x4 ) 76 )) ) |
---|
| 164 | (or (not ( >= ( - x27 x21 ) 17 )) (not ( >= ( - x1 x21 ) 62 )) ) |
---|
| 165 | (or (not ( >= ( - x5 x1 ) 32 )) (not ( >= ( - x12 x18 ) 99 )) ) |
---|
| 166 | (or ( >= ( - x22 x11 ) 49 ) ( >= ( - x24 x23 ) 96 ) ) |
---|
| 167 | (or ( >= ( - x24 x13 ) 21 ) (not ( >= ( - x20 x9 ) 93 )) ) |
---|
| 168 | (or (not ( >= ( - x34 x30 ) 26 )) (not ( >= ( - x6 x12 ) 3 )) ) |
---|
| 169 | (or (not ( >= ( - x1 x3 ) 71 )) (not ( >= ( - x11 x2 ) 16 )) ) |
---|
| 170 | (or (not ( >= ( - x0 x23 ) 52 )) (not ( >= ( - x19 x27 ) 56 )) ) |
---|
| 171 | (or ( >= ( - x21 x11 ) 29 ) (not ( >= ( - x19 x11 ) 1 )) ) |
---|
| 172 | (or ( >= ( - x3 x16 ) 66 ) (not ( >= ( - x15 x10 ) 3 )) ) |
---|
| 173 | (or ( >= ( - x4 x8 ) 17 ) (not ( >= ( - x33 x20 ) 71 )) ) |
---|
| 174 | (or (not ( >= ( - x3 x14 ) 56 )) (not ( >= ( - x26 x7 ) 64 )) ) |
---|
| 175 | (or ( >= ( - x8 x34 ) 92 ) (not ( >= ( - x16 x22 ) 93 )) ) |
---|
| 176 | (or ( >= ( - x10 x2 ) 92 ) ( >= ( - x30 x31 ) 51 ) ) |
---|
| 177 | (or (not ( >= ( - x15 x25 ) 25 )) (not ( >= ( - x12 x11 ) 7 )) ) |
---|
| 178 | (or (not ( >= ( - x34 x31 ) 43 )) (not ( >= ( - x25 x12 ) 67 )) ) |
---|
| 179 | (or (not ( >= ( - x22 x1 ) 75 )) ( >= ( - x14 x33 ) 73 ) ) |
---|
| 180 | (or (not ( >= ( - x16 x3 ) 69 )) (not ( >= ( - x30 x26 ) 17 )) ) |
---|
| 181 | (or ( >= ( - x13 x3 ) 65 ) (not ( >= ( - x20 x33 ) 41 )) ) |
---|
| 182 | (or ( >= ( - x32 x13 ) 88 ) (not ( >= ( - x15 x20 ) 39 )) ) |
---|
| 183 | (or ( >= ( - x18 x9 ) 46 ) ( >= ( - x12 x21 ) 65 ) ) |
---|
| 184 | (or ( >= ( - x18 x31 ) 51 ) ( >= ( - x23 x7 ) 15 ) ) |
---|
| 185 | (or (not ( >= ( - x22 x20 ) 33 )) (not ( >= ( - x16 x23 ) 40 )) ) |
---|
| 186 | (or (not ( >= ( - x2 x3 ) 87 )) (not ( >= ( - x34 x26 ) 63 )) ) |
---|
| 187 | (or ( >= ( - x1 x9 ) 78 ) ( >= ( - x6 x22 ) 55 ) ) |
---|
| 188 | (or (not ( >= ( - x1 x5 ) 74 )) (not ( >= ( - x33 x13 ) 63 )) ) |
---|
| 189 | (or ( >= ( - x28 x30 ) 60 ) (not ( >= ( - x1 x7 ) 37 )) ) |
---|
| 190 | (or ( >= ( - x29 x13 ) 25 ) ( >= ( - x24 x32 ) 31 ) ) |
---|
| 191 | (or ( >= ( - x9 x33 ) 84 ) (not ( >= ( - x14 x29 ) 74 )) ) |
---|
| 192 | (or (not ( >= ( - x9 x30 ) 94 )) ( >= ( - x4 x34 ) 93 ) ) |
---|
| 193 | (or (not ( >= ( - x6 x19 ) 8 )) (not ( >= ( - x1 x28 ) 96 )) ) |
---|
| 194 | (or (not ( >= ( - x32 x22 ) 75 )) ( >= ( - x18 x10 ) 58 ) ) |
---|
| 195 | (or (not ( >= ( - x32 x33 ) 33 )) ( >= ( - x14 x9 ) 31 ) ) |
---|
| 196 | (or (not ( >= ( - x24 x11 ) 7 )) (not ( >= ( - x1 x32 ) 73 )) ) |
---|
| 197 | (or (not ( >= ( - x27 x17 ) 65 )) ( >= ( - x29 x30 ) 54 ) ) |
---|
| 198 | (or ( >= ( - x34 x30 ) 66 ) (not ( >= ( - x24 x6 ) 17 )) ) |
---|
| 199 | (or (not ( >= ( - x6 x20 ) 42 )) (not ( >= ( - x19 x9 ) 83 )) ) |
---|
| 200 | (or (not ( >= ( - x21 x18 ) 33 )) (not ( >= ( - x8 x16 ) 35 )) ) |
---|
| 201 | (or (not ( >= ( - x19 x8 ) 41 )) ( >= ( - x5 x22 ) 31 ) ) |
---|
| 202 | (or ( >= ( - x19 x4 ) 55 ) ( >= ( - x23 x21 ) 7 ) ) |
---|
| 203 | (or ( >= ( - x32 x15 ) 83 ) (not ( >= ( - x26 x34 ) 13 )) ) |
---|
| 204 | (or ( >= ( - x24 x17 ) 1 ) (not ( >= ( - x0 x32 ) 24 )) ) |
---|
| 205 | (or ( >= ( - x28 x29 ) 23 ) (not ( >= ( - x26 x7 ) 24 )) ) |
---|
| 206 | (or ( >= ( - x34 x14 ) 23 ) ( >= ( - x11 x28 ) 82 ) ) |
---|
| 207 | (or (not ( >= ( - x22 x20 ) 70 )) ( >= ( - x27 x18 ) 55 ) ) |
---|
| 208 | (or ( >= ( - x1 x22 ) 18 ) (not ( >= ( - x11 x16 ) 93 )) ) |
---|
| 209 | (or ( >= ( - x23 x2 ) 38 ) ( >= ( - x9 x4 ) 73 ) ) |
---|
| 210 | (or (not ( >= ( - x19 x12 ) 51 )) ( >= ( - x16 x3 ) 19 ) ) |
---|
| 211 | (or (not ( >= ( - x34 x32 ) 27 )) (not ( >= ( - x30 x32 ) 41 )) ) |
---|
| 212 | (or (not ( >= ( - x10 x23 ) 22 )) (not ( >= ( - x19 x7 ) 49 )) ) |
---|
| 213 | (or ( >= ( - x34 x22 ) 43 ) (not ( >= ( - x2 x26 ) 48 )) ) |
---|
| 214 | (or ( >= ( - x19 x29 ) 69 ) (not ( >= ( - x8 x1 ) 71 )) ) |
---|
| 215 | (or ( >= ( - x2 x4 ) 29 ) (not ( >= ( - x17 x6 ) 66 )) ) |
---|
| 216 | (or ( >= ( - x21 x32 ) 70 ) (not ( >= ( - x5 x20 ) 46 )) ) |
---|
| 217 | (or (not ( >= ( - x5 x32 ) 19 )) (not ( >= ( - x16 x31 ) 35 )) ) |
---|
| 218 | (or (not ( >= ( - x6 x25 ) 37 )) (not ( >= ( - x33 x8 ) 52 )) ) |
---|
| 219 | (or ( >= ( - x10 x5 ) 52 ) (not ( >= ( - x26 x28 ) 68 )) ) |
---|
| 220 | (or ( >= ( - x3 x23 ) 91 ) ( >= ( - x4 x3 ) 78 ) ) |
---|
| 221 | (or (not ( >= ( - x15 x18 ) 98 )) ( >= ( - x22 x32 ) 51 ) ) |
---|
| 222 | (or ( >= ( - x23 x25 ) 65 ) (not ( >= ( - x20 x0 ) 81 )) ) |
---|
| 223 | (or (not ( >= ( - x7 x4 ) 12 )) (not ( >= ( - x33 x11 ) 8 )) ) |
---|
| 224 | )) |
---|