1(set-logic QF_UFIDL) 2; benchmark generated from python API 3(set-info :status unknown) 4(declare-fun t.R_nxt (Int Int) Bool) 5(declare-fun t.curr () Int) 6(declare-fun t.l () Int) 7(declare-fun en_LOCATION () Int) 8(declare-fun t.pc () Int) 9(declare-fun NULL () Int) 10(declare-fun i1 () Int) 11(declare-fun t.nxt (Int) Int) 12(declare-fun i2 () Int) 13(declare-fun t.p () Int) 14(declare-fun t.suc () Int) 15(declare-fun t.data (Int) Int) 16(declare-fun t.H_nxt (Int) Bool) 17(declare-fun t.I_nxt (Int) Int) 18(assert 19 (t.R_nxt t.l t.curr)) 20(assert 21 (let ((?x15 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION)))))))) 22 (let ((?x17 (+ 1 (+ 1 ?x15)))) 23 (let (($x19 (= t.pc ?x17))) 24 (let (($x22 (not $x19))) 25 (let (($x1230 (= i1 NULL))) 26 (let (($x1231 (not $x1230))) 27 (let (($x1267 (and $x1231 $x22))) 28 (let (($x30 (= i1 t.l))) 29 (let (($x31 (not $x30))) 30 (let (($x1268 (and $x31 $x1267))) 31 (let (($x895 (= i1 t.curr))) 32 (let (($x1229 (not $x895))) 33 (and $x1229 $x1268)))))))))))))) 34 35(assert 36 (let ((?x93 (t.nxt t.suc))) 37 (= ?x93 t.suc))) 38(assert 39 (let ((?x15 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION)))))))) 40 (let ((?x17 (+ 1 (+ 1 ?x15)))) 41 (let (($x19 (= t.pc ?x17))) 42 (let (($x22 (not $x19))) 43 (let (($x117 (= t.pc ?x15))) 44 (let (($x1232 (not $x117))) 45 (let (($x1319 (and $x1232 $x22))) 46 (let (($x1331 (= i2 NULL))) 47 (let (($x1332 (not $x1331))) 48 (let (($x2541 (and $x1332 $x1319))) 49 (let (($x945 (= i2 t.suc))) 50 (let (($x1329 (not $x945))) 51 (let (($x2908 (and $x1329 $x2541))) 52 (let (($x119 (= t.suc NULL))) 53 (let (($x15330 (and $x119 $x2908))) 54 (let (($x1013 (= t.curr t.suc))) 55 (let (($x1646 (not $x1013))) 56 (let (($x15331 (and $x1646 $x15330))) 57 (let (($x335 (t.H_nxt i2))) 58 (let (($x2479 (not $x335))) 59 (let (($x15332 (and $x2479 $x15331))) 60 (let (($x15333 (and $x1329 $x15332))) 61 (let (($x951 (= i2 t.p))) 62 (let (($x1351 (not $x951))) 63 (let (($x15334 (and $x1351 $x15333))) 64 (let (($x64 (= t.l t.suc))) 65 (let (($x65 (not $x64))) 66 (let (($x15335 (and $x65 $x15334))) 67 (let (($x38 (t.R_nxt t.l i2))) 68 (let (($x15336 (and $x38 $x15335))) 69 (let (($x1061 (= t.suc t.p))) 70 (let (($x1683 (not $x1061))) 71 (let (($x15337 (and $x1683 $x15336))) 72 (let ((?x398 (t.nxt i2))) 73 (let (($x430 (= t.suc ?x398))) 74 (let (($x2876 (not $x430))) 75 (let (($x15338 (and $x2876 $x15337))) 76 (let ((?x396 (t.I_nxt i2))) 77 (let (($x428 (= ?x396 t.suc))) 78 (let (($x15339 (and $x428 $x15338))) 79 (let (($x1043 (t.R_nxt t.suc i2))) 80 (let (($x1044 (not $x1043))) 81 (let (($x15340 (and $x1044 $x15339))) 82 (let (($x15341 (and $x1044 $x15340))) 83 (let (($x943 (t.R_nxt i2 t.suc))) 84 (let (($x944 (not $x943))) 85 (let (($x15342 (and $x944 $x15341))) 86 (let (($x1262 (and $x117 $x22))) 87 (let (($x2485 (and $x1332 $x1262))) 88 (let (($x39 (= i2 t.l))) 89 (let (($x40 (not $x39))) 90 (let (($x2486 (and $x40 $x2485))) 91 (let (($x939 (= i2 t.curr))) 92 (let (($x1330 (not $x939))) 93 (let (($x2487 (and $x1330 $x2486))) 94 (let (($x2488 (and $x1329 $x2487))) 95 (let (($x120 (not $x119))) 96 (let (($x2904 (and $x120 $x2488))) 97 (let (($x2905 (and $x1646 $x2904))) 98 (let (($x2906 (and $x2479 $x2905))) 99 (let (($x2907 (and $x1329 $x2906))) 100 (let (($x2878 (not (< (t.data t.suc) (t.data i2))))) 101 (let (($x15321 (and $x2878 $x2907))) 102 (let (($x15322 (and $x1351 $x15321))) 103 (let (($x15323 (and $x65 $x15322))) 104 (let (($x15324 (and $x1683 $x15323))) 105 (let (($x15325 (and $x2876 $x15324))) 106 (let (($x429 (not $x428))) 107 (let (($x15326 (and $x429 $x15325))) 108 (let (($x15327 (and $x1044 $x15326))) 109 (let (($x15328 (and $x1044 $x15327))) 110 (let (($x15313 (and $x65 $x2907))) 111 (let (($x973 (not $x38))) 112 (let (($x15314 (and $x973 $x15313))) 113 (let (($x15315 (and $x1683 $x15314))) 114 (let (($x15316 (and $x429 $x15315))) 115 (let (($x15317 (and $x1044 $x15316))) 116 (let (($x15318 (and $x1044 $x15317))) 117 (let (($x15319 (and $x943 $x15318))) 118 (let (($x2489 (and $x1332 $x22))) 119 (let (($x2490 (and $x40 $x2489))) 120 (let (($x2491 (and $x1330 $x2490))) 121 (let (($x2508 (and $x945 $x2491))) 122 (let (($x15299 (and $x120 $x2508))) 123 (let (($x15300 (and $x1646 $x15299))) 124 (let (($x15301 (and $x2479 $x15300))) 125 (let (($x15302 (and $x945 $x15301))) 126 (let (($x15303 (and $x2878 $x15302))) 127 (let (($x15304 (and $x1351 $x15303))) 128 (let (($x15305 (and $x65 $x15304))) 129 (let (($x15306 (and $x38 $x15305))) 130 (let (($x15307 (and $x1683 $x15306))) 131 (let (($x15308 (and $x429 $x15307))) 132 (let (($x15309 (and $x1043 $x15308))) 133 (let (($x15310 (and $x1043 $x15309))) 134 (let (($x15311 (and $x943 $x15310))) 135 (let (($x2855 (and $x1330 $x2489))) 136 (let (($x2856 (and $x1329 $x2855))) 137 (let (($x15285 (and $x119 $x2856))) 138 (let (($x15286 (and $x1646 $x15285))) 139 (let (($x15287 (and $x2479 $x15286))) 140 (let (($x15288 (and $x1329 $x15287))) 141 (let (($x15289 (and $x1351 $x15288))) 142 (let (($x15290 (and $x65 $x15289))) 143 (let (($x15291 (and $x38 $x15290))) 144 (let (($x15292 (and $x1683 $x15291))) 145 (let (($x15293 (and $x2876 $x15292))) 146 (let (($x15294 (and $x428 $x15293))) 147 (let (($x15295 (and $x1044 $x15294))) 148 (let (($x15296 (and $x1044 $x15295))) 149 (let (($x15297 (and $x944 $x15296))) 150 (let (($x2902 (and $x939 $x2485))) 151 (let (($x2903 (and $x1329 $x2902))) 152 (let (($x15271 (and $x119 $x2903))) 153 (let (($x15272 (and $x1646 $x15271))) 154 (let (($x15273 (and $x2479 $x15272))) 155 (let (($x15274 (and $x1329 $x15273))) 156 (let (($x15275 (and $x1351 $x15274))) 157 (let (($x15276 (and $x65 $x15275))) 158 (let (($x15277 (and $x38 $x15276))) 159 (let (($x15278 (and $x1683 $x15277))) 160 (let (($x15279 (and $x430 $x15278))) 161 (let (($x15280 (and $x428 $x15279))) 162 (let (($x15281 (and $x1044 $x15280))) 163 (let (($x15282 (and $x1044 $x15281))) 164 (let (($x15283 (and $x944 $x15282))) 165 (let (($x2769 (and $x40 $x22))) 166 (let (($x2770 (and $x1330 $x2769))) 167 (let (($x2771 (and $x1329 $x2770))) 168 (let (($x2896 (and $x120 $x2771))) 169 (let (($x2897 (and $x1646 $x2896))) 170 (let (($x2898 (and $x335 $x2897))) 171 (let (($x2899 (and $x1329 $x2898))) 172 (let (($x2900 (and $x1351 $x2899))) 173 (let (($x2901 (and $x65 $x2900))) 174 (let (($x15263 (and $x973 $x2901))) 175 (let (($x15264 (and $x1683 $x15263))) 176 (let (($x15265 (and $x2876 $x15264))) 177 (let (($x15266 (and $x429 $x15265))) 178 (let (($x15267 (and $x1044 $x15266))) 179 (let (($x15268 (and $x1044 $x15267))) 180 (let (($x15269 (and $x944 $x15268))) 181 (let (($x15255 (and $x38 $x2901))) 182 (let (($x15256 (and $x1683 $x15255))) 183 (let (($x15257 (and $x2876 $x15256))) 184 (let (($x15258 (and $x429 $x15257))) 185 (let (($x15259 (and $x1043 $x15258))) 186 (let (($x15260 (and $x1043 $x15259))) 187 (let (($x15261 (and $x944 $x15260))) 188 (let (($x2492 (and $x1329 $x2491))) 189 (let (($x15243 (and $x119 $x2492))) 190 (let (($x15244 (and $x1646 $x15243))) 191 (let (($x15245 (and $x1329 $x15244))) 192 (let (($x15246 (and $x1351 $x15245))) 193 (let (($x15247 (and $x65 $x15246))) 194 (let (($x15248 (and $x973 $x15247))) 195 (let (($x15249 (and $x1683 $x15248))) 196 (let (($x15250 (and $x428 $x15249))) 197 (let (($x15251 (and $x1044 $x15250))) 198 (let (($x15252 (and $x1044 $x15251))) 199 (let (($x15253 (and $x944 $x15252))) 200 (let (($x2891 (and $x120 $x2492))) 201 (let (($x2892 (and $x1646 $x2891))) 202 (let (($x2893 (and $x1329 $x2892))) 203 (let (($x2894 (and $x1351 $x2893))) 204 (let (($x2895 (and $x65 $x2894))) 205 (let (($x15237 (and $x38 $x2895))) 206 (let (($x15238 (and $x1683 $x15237))) 207 (let (($x15239 (and $x2876 $x15238))) 208 (let (($x15240 (and $x1043 $x15239))) 209 (let (($x15241 (and $x1043 $x15240))) 210 (let (($x2887 (and $x119 $x2488))) 211 (let (($x2888 (and $x1646 $x2887))) 212 (let (($x2889 (and $x2479 $x2888))) 213 (let (($x2890 (and $x1329 $x2889))) 214 (let (($x15229 (and $x65 $x2890))) 215 (let (($x15230 (and $x973 $x15229))) 216 (let (($x15231 (and $x1683 $x15230))) 217 (let (($x15232 (and $x428 $x15231))) 218 (let (($x15233 (and $x1044 $x15232))) 219 (let (($x15234 (and $x1044 $x15233))) 220 (let (($x15235 (and $x944 $x15234))) 221 (let (($x15221 (and $x1351 $x2890))) 222 (let (($x15222 (and $x65 $x15221))) 223 (let (($x15223 (and $x1683 $x15222))) 224 (let (($x15224 (and $x2876 $x15223))) 225 (let (($x15225 (and $x428 $x15224))) 226 (let (($x15226 (and $x1044 $x15225))) 227 (let (($x15227 (and $x1044 $x15226))) 228 (let (($x1233 (and $x19 $x1232))) 229 (let (($x2468 (and $x1331 $x1233))) 230 (let (($x2469 (and $x40 $x2468))) 231 (let (($x2470 (and $x939 $x2469))) 232 (let (($x2471 (and $x945 $x2470))) 233 (let (($x2879 (and $x119 $x2471))) 234 (let (($x2880 (and $x1013 $x2879))) 235 (let (($x2881 (and $x335 $x2880))) 236 (let (($x2882 (and $x945 $x2881))) 237 (let (($x2883 (and $x2878 $x2882))) 238 (let (($x2884 (and $x1351 $x2883))) 239 (let (($x2885 (and $x65 $x2884))) 240 (let (($x2886 (and $x1683 $x2885))) 241 (let (($x15217 (and $x1044 $x2886))) 242 (let (($x15218 (and $x1044 $x15217))) 243 (let (($x15219 (and $x944 $x15218))) 244 (let (($x15213 (and $x1043 $x2886))) 245 (let (($x15214 (and $x1043 $x15213))) 246 (let (($x15215 (and $x943 $x15214))) 247 (let (($x15203 (and $x1646 $x2488))) 248 (let (($x15204 (and $x2479 $x15203))) 249 (let (($x15205 (and $x1329 $x15204))) 250 (let (($x15206 (and $x65 $x15205))) 251 (let (($x15207 (and $x973 $x15206))) 252 (let (($x15208 (and $x1683 $x15207))) 253 (let (($x15209 (and $x2876 $x15208))) 254 (let (($x15210 (and $x1044 $x15209))) 255 (let (($x15211 (and $x1044 $x15210))) 256 (let (($x15193 (and $x1646 $x2492))) 257 (let (($x15194 (and $x1329 $x15193))) 258 (let (($x15195 (and $x1351 $x15194))) 259 (let (($x15196 (and $x65 $x15195))) 260 (let (($x15197 (and $x973 $x15196))) 261 (let (($x15198 (and $x1683 $x15197))) 262 (let (($x15199 (and $x2876 $x15198))) 263 (let (($x15200 (and $x1044 $x15199))) 264 (let (($x15201 (and $x1044 $x15200))) 265 (let (($x2457 (and $x1332 $x1233))) 266 (let (($x2458 (and $x40 $x2457))) 267 (let (($x2459 (and $x1330 $x2458))) 268 (let (($x2460 (and $x1329 $x2459))) 269 (let (($x2857 (and $x119 $x2460))) 270 (let (($x2858 (and $x1013 $x2857))) 271 (let (($x2871 (and $x2479 $x2858))) 272 (let (($x2872 (and $x1329 $x2871))) 273 (let (($x2873 (and $x65 $x2872))) 274 (let (($x2874 (and $x973 $x2873))) 275 (let (($x2875 (and $x1683 $x2874))) 276 (let (($x15190 (and $x1044 $x2875))) 277 (let (($x15191 (and $x1044 $x15190))) 278 (let (($x15187 (and $x1043 $x2875))) 279 (let (($x15188 (and $x1043 $x15187))) 280 (let (($x2805 (and $x1330 $x2457))) 281 (let (($x2806 (and $x1329 $x2805))) 282 (let (($x2863 (and $x119 $x2806))) 283 (let (($x2864 (and $x1013 $x2863))) 284 (let (($x2865 (and $x2479 $x2864))) 285 (let (($x2866 (and $x1329 $x2865))) 286 (let (($x2867 (and $x1351 $x2866))) 287 (let (($x2868 (and $x65 $x2867))) 288 (let (($x2869 (and $x1683 $x2868))) 289 (let (($x2870 (and $x428 $x2869))) 290 (let (($x15184 (and $x1044 $x2870))) 291 (let (($x15185 (and $x1044 $x15184))) 292 (let (($x15181 (and $x1043 $x2870))) 293 (let (($x15182 (and $x1043 $x15181))) 294 (let (($x2859 (and $x1329 $x2858))) 295 (let (($x2860 (and $x1351 $x2859))) 296 (let (($x2861 (and $x65 $x2860))) 297 (let (($x2862 (and $x1683 $x2861))) 298 (let (($x15178 (and $x1044 $x2862))) 299 (let (($x15179 (and $x1044 $x15178))) 300 (let (($x15176 (and $x1043 $x2862))) 301 (let (($x15177 (and $x1043 $x15176))) 302 (let (($x15180 (or $x15177 $x15179))) 303 (let (($x15183 (or $x15180 $x15182))) 304 (let (($x15186 (or $x15183 $x15185))) 305 (let (($x15189 (or $x15186 $x15188))) 306 (let (($x15192 (or $x15189 $x15191))) 307 (let (($x15202 (or $x15192 $x15201))) 308 (let (($x15212 (or $x15202 $x15211))) 309 (let (($x15216 (or $x15212 $x15215))) 310 (let (($x15220 (or $x15216 $x15219))) 311 (let (($x15228 (or $x15220 $x15227))) 312 (let (($x15236 (or $x15228 $x15235))) 313 (let (($x15242 (or $x15236 $x15241))) 314 (let (($x15254 (or $x15242 $x15253))) 315 (let (($x15262 (or $x15254 $x15261))) 316 (let (($x15270 (or $x15262 $x15269))) 317 (let (($x15284 (or $x15270 $x15283))) 318 (let (($x15298 (or $x15284 $x15297))) 319 (let (($x15312 (or $x15298 $x15311))) 320 (let (($x15320 (or $x15312 $x15319))) 321 (let (($x15329 (or $x15320 $x15328))) 322 (let (($x15343 (or $x15329 $x15342))) 323 (not $x15343)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 324 325 326 327(assert 328 (let ((?x105 (t.nxt t.curr))) 329 (let (($x548 (= ?x105 t.curr))) 330 (not $x548)))) 331 332(assert 333 (let ((?x6 (t.nxt t.l))) 334 (let (($x87 (= ?x6 t.l))) 335 (not $x87)))) 336(assert 337 (t.R_nxt t.suc i2)) 338(assert 339 (let ((?x105 (t.nxt t.curr))) 340 (let (($x390 (t.H_nxt ?x105))) 341 (let (($x527 (not $x390))) 342 (not $x527))))) 343(assert 344 (let ((?x15 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION)))))))) 345 (let ((?x17 (+ 1 (+ 1 ?x15)))) 346 (let (($x19 (= t.pc ?x17))) 347 (let (($x22 (not $x19))) 348 (let ((?x93 (t.nxt t.suc))) 349 (let (($x2017 (= ?x93 NULL))) 350 (let (($x2018 (not $x2017))) 351 (let (($x5672 (and $x2018 $x22))) 352 (let (($x99 (= ?x93 t.l))) 353 (let (($x100 (not $x99))) 354 (let (($x5673 (and $x100 $x5672))) 355 (let (($x608 (= ?x93 t.curr))) 356 (let (($x2016 (not $x608))) 357 (let (($x5674 (and $x2016 $x5673))) 358 (not $x5674)))))))))))))))) 359(assert 360 (let ((?x15 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION)))))))) 361 (let ((?x17 (+ 1 (+ 1 ?x15)))) 362 (let (($x19 (= t.pc ?x17))) 363 (let (($x22 (not $x19))) 364 (let ((?x105 (t.nxt t.curr))) 365 (let (($x2240 (= ?x105 NULL))) 366 (let (($x2241 (not $x2240))) 367 (let (($x6837 (and $x2241 $x22))) 368 (let (($x111 (= ?x105 t.l))) 369 (let (($x112 (not $x111))) 370 (let (($x6838 (and $x112 $x6837))) 371 (let (($x548 (= ?x105 t.curr))) 372 (let (($x2239 (not $x548))) 373 (let (($x6839 (and $x2239 $x6838))) 374 (let ((?x6 (t.nxt t.l))) 375 (let (($x1794 (= ?x6 NULL))) 376 (let (($x7644 (and $x1794 $x6839))) 377 (let (($x487 (= ?x6 t.curr))) 378 (let (($x1793 (not $x487))) 379 (let (($x7645 (and $x1793 $x7644))) 380 (let (($x494 (= ?x6 t.suc))) 381 (let (($x1792 (not $x494))) 382 (let (($x7646 (and $x1792 $x7645))) 383 (let (($x390 (t.H_nxt ?x105))) 384 (let (($x527 (not $x390))) 385 (let (($x7647 (and $x527 $x7646))) 386 (let (($x519 (= ?x105 ?x6))) 387 (let (($x3810 (not $x519))) 388 (let (($x7648 (and $x3810 $x7647))) 389 (let (($x562 (= ?x105 t.p))) 390 (let (($x2260 (not $x562))) 391 (let (($x7649 (and $x2260 $x7648))) 392 (let (($x87 (= ?x6 t.l))) 393 (let (($x88 (not $x87))) 394 (let (($x7650 (and $x88 $x7649))) 395 (let (($x110 (t.R_nxt t.l ?x105))) 396 (let (($x7651 (and $x110 $x7650))) 397 (let (($x501 (= ?x6 t.p))) 398 (let (($x1814 (not $x501))) 399 (let (($x7652 (and $x1814 $x7651))) 400 (let ((?x824 (t.nxt ?x105))) 401 (let (($x864 (= ?x6 ?x824))) 402 (let (($x7558 (not $x864))) 403 (let (($x31311 (and $x7558 $x7652))) 404 (let ((?x528 (t.I_nxt ?x105))) 405 (let (($x569 (= ?x528 ?x6))) 406 (let (($x31312 (and $x569 $x31311))) 407 (let (($x106 (t.R_nxt ?x6 ?x105))) 408 (let (($x1149 (not $x106))) 409 (let (($x31313 (and $x1149 $x31312))) 410 (let (($x1075 (t.R_nxt t.suc ?x105))) 411 (let (($x31314 (and $x1075 $x31313))) 412 (let (($x555 (= ?x105 t.suc))) 413 (let (($x2238 (not $x555))) 414 (let (($x7211 (and $x2238 $x6837))) 415 (let (($x1795 (not $x1794))) 416 (let (($x31298 (and $x1795 $x7211))) 417 (let (($x31299 (and $x1793 $x31298))) 418 (let (($x31300 (and $x1792 $x31299))) 419 (let (($x31301 (and $x527 $x31300))) 420 (let (($x31302 (and $x3810 $x31301))) 421 (let (($x31303 (and $x2260 $x31302))) 422 (let (($x31304 (and $x88 $x31303))) 423 (let (($x31305 (and $x110 $x31304))) 424 (let (($x31306 (and $x1814 $x31305))) 425 (let (($x31307 (and $x7558 $x31306))) 426 (let (($x863 (not $x569))) 427 (let (($x31308 (and $x863 $x31307))) 428 (let (($x1076 (not $x1075))) 429 (let (($x31309 (and $x1076 $x31308))) 430 (let (($x31284 (and $x1794 $x7211))) 431 (let (($x31285 (and $x1793 $x31284))) 432 (let (($x31286 (and $x1792 $x31285))) 433 (let (($x31287 (and $x527 $x31286))) 434 (let (($x31288 (and $x3810 $x31287))) 435 (let (($x31289 (and $x2260 $x31288))) 436 (let (($x31290 (and $x88 $x31289))) 437 (let (($x31291 (and $x110 $x31290))) 438 (let (($x31292 (and $x1814 $x31291))) 439 (let (($x31293 (and $x7558 $x31292))) 440 (let (($x31294 (and $x569 $x31293))) 441 (let (($x31295 (and $x1149 $x31294))) 442 (let (($x31296 (and $x1076 $x31295))) 443 (let (($x7203 (and $x112 $x22))) 444 (let (($x7204 (and $x2239 $x7203))) 445 (let (($x7205 (and $x2238 $x7204))) 446 (let (($x7639 (and $x1795 $x7205))) 447 (let (($x7640 (and $x1792 $x7639))) 448 (let (($x7641 (and $x390 $x7640))) 449 (let (($x7642 (and $x3810 $x7641))) 450 (let (($x7643 (and $x2260 $x7642))) 451 (let (($x992 (not $x110))) 452 (let (($x31276 (and $x992 $x7643))) 453 (let (($x31277 (and $x1814 $x31276))) 454 (let (($x31278 (and $x7558 $x31277))) 455 (let (($x31279 (and $x863 $x31278))) 456 (let (($x31280 (and $x1149 $x31279))) 457 (let (($x31281 (and $x1076 $x31280))) 458 (let (($x1025 (t.R_nxt ?x105 ?x6))) 459 (let (($x1211 (not $x1025))) 460 (let (($x31282 (and $x1211 $x31281))) 461 (let (($x31268 (and $x110 $x7643))) 462 (let (($x31269 (and $x1814 $x31268))) 463 (let (($x31270 (and $x7558 $x31269))) 464 (let (($x31271 (and $x863 $x31270))) 465 (let (($x31272 (and $x106 $x31271))) 466 (let (($x31273 (and $x1075 $x31272))) 467 (let (($x31274 (and $x1211 $x31273))) 468 (let (($x6871 (and $x2240 $x22))) 469 (let (($x6872 (and $x112 $x6871))) 470 (let (($x6873 (and $x2239 $x6872))) 471 (let (($x6874 (and $x555 $x6873))) 472 (let (($x7638 (and $x1795 $x6874))) 473 (let (($x31261 (and $x1814 (and $x992 (and $x2260 (and $x3810 (and $x390 (and $x1792 $x7638)))))))) 474 (let (($x117 (= t.pc ?x15))) 475 (let (($x1232 (not $x117))) 476 (let (($x1233 (and $x19 $x1232))) 477 (let (($x6806 (and $x2241 $x1233))) 478 (let (($x6807 (and $x112 $x6806))) 479 (let (($x6808 (and $x2239 $x6807))) 480 (let (($x6809 (and $x2238 $x6808))) 481 (let (($x7548 (and $x1795 $x6809))) 482 (let (($x7549 (and $x1793 $x7548))) 483 (let (($x7550 (and $x1792 $x7549))) 484 (let (($x7574 (and $x527 $x7550))) 485 (let (($x7632 (and $x519 $x7574))) 486 (let ((?x2234 (t.data ?x105))) 487 (let ((?x1788 (t.data ?x6))) 488 (let (($x7539 (< ?x1788 ?x2234))) 489 (let (($x7540 (not $x7539))) 490 (let (($x7633 (and $x7540 $x7632))) 491 (let (($x7634 (and $x562 $x7633))) 492 (let (($x7635 (and $x88 $x7634))) 493 (let (($x7636 (and $x992 $x7635))) 494 (let (($x7637 (and $x501 $x7636))) 495 (let (($x31253 (and $x1149 $x7637))) 496 (let (($x31254 (and $x1211 $x31253))) 497 (let (($x31250 (and $x106 $x7637))) 498 (let (($x31251 (and $x1025 $x31250))) 499 (let (($x7551 (and $x3810 $x7550))) 500 (let (($x7556 (and $x2260 $x7551))) 501 (let (($x31245 (and $x110 $x7556))) 502 (let (($x31246 (and $x1814 $x31245))) 503 (let (($x31247 (and $x7558 $x31246))) 504 (let (($x31248 (and $x106 $x31247))) 505 (let (($x7114 (and $x2239 $x6806))) 506 (let (($x7115 (and $x2238 $x7114))) 507 (let (($x7559 (and $x1795 $x7115))) 508 (let (($x7560 (and $x1793 $x7559))) 509 (let (($x7561 (and $x1792 $x7560))) 510 (let (($x7562 (and $x527 $x7561))) 511 (let (($x7563 (and $x3810 $x7562))) 512 (let (($x7591 (and $x2260 $x7563))) 513 (let (($x7592 (and $x88 $x7591))) 514 (let (($x31241 (and $x1814 $x7592))) 515 (let (($x31242 (and $x7558 $x31241))) 516 (let (($x31243 (and $x863 $x31242))) 517 (let (($x6817 (and $x2240 $x1233))) 518 (let (($x6818 (and $x112 $x6817))) 519 (let (($x6819 (and $x548 $x6818))) 520 (let (($x6820 (and $x555 $x6819))) 521 (let (($x7541 (and $x1795 $x6820))) 522 (let (($x7542 (and $x1793 $x7541))) 523 (let (($x7543 (and $x1792 $x7542))) 524 (let (($x7544 (and $x390 $x7543))) 525 (let (($x7545 (and $x3810 $x7544))) 526 (let (($x7554 (and $x2260 $x7545))) 527 (let (($x31236 (and $x110 $x7554))) 528 (let (($x31237 (and $x1814 $x31236))) 529 (let (($x31238 (and $x7558 $x31237))) 530 (let (($x31239 (and $x106 $x31238))) 531 (let (($x7623 (and $x1794 $x6820))) 532 (let (($x7624 (and $x487 $x7623))) 533 (let (($x7625 (and $x494 $x7624))) 534 (let (($x7626 (and $x390 $x7625))) 535 (let (($x7627 (and $x519 $x7626))) 536 (let (($x7628 (and $x7540 $x7627))) 537 (let (($x7629 (and $x2260 $x7628))) 538 (let (($x7630 (and $x88 $x7629))) 539 (let (($x7631 (and $x1814 $x7630))) 540 (let (($x31232 (and $x1149 $x7631))) 541 (let (($x31233 (and $x1076 $x31232))) 542 (let (($x31234 (and $x1211 $x31233))) 543 (let (($x31228 (and $x106 $x7631))) 544 (let (($x31229 (and $x1075 $x31228))) 545 (let (($x31230 (and $x1025 $x31229))) 546 (let (($x1262 (and $x117 $x22))) 547 (let (($x6833 (and $x2241 $x1262))) 548 (let (($x6834 (and $x112 $x6833))) 549 (let (($x6835 (and $x2239 $x6834))) 550 (let (($x6836 (and $x2238 $x6835))) 551 (let (($x7576 (and $x1795 $x6836))) 552 (let (($x7577 (and $x1793 $x7576))) 553 (let (($x7578 (and $x1792 $x7577))) 554 (let (($x7579 (and $x3810 $x7578))) 555 (let (($x7580 (and $x2260 $x7579))) 556 (let (($x7581 (and $x88 $x7580))) 557 (let (($x7622 (and $x992 $x7581))) 558 (let (($x31225 (and $x7558 $x7622))) 559 (let (($x31226 (and $x1076 $x31225))) 560 (let (($x7614 (and $x1792 $x7576))) 561 (let (($x7615 (and $x3810 $x7614))) 562 (let (($x7616 (and $x2260 $x7615))) 563 (let (($x31219 (and $x992 $x7616))) 564 (let (($x31220 (and $x1814 $x31219))) 565 (let (($x31221 (and $x7558 $x31220))) 566 (let (($x31222 (and $x1149 $x31221))) 567 (let (($x31223 (and $x1076 $x31222))) 568 (let (($x7617 (and $x527 $x7614))) 569 (let (($x7618 (and $x3810 $x7617))) 570 (let (($x7619 (and $x7539 $x7618))) 571 (let (($x7620 (and $x992 $x7619))) 572 (let (($x7621 (and $x1814 $x7620))) 573 (let (($x31215 (and $x7558 $x7621))) 574 (let (($x31216 (and $x1149 $x31215))) 575 (let (($x31217 (and $x1076 $x31216))) 576 (let (($x31209 (and $x110 $x7616))) 577 (let (($x31210 (and $x1814 $x31209))) 578 (let (($x31211 (and $x7558 $x31210))) 579 (let (($x31212 (and $x106 $x31211))) 580 (let (($x31213 (and $x1075 $x31212))) 581 (let (($x6840 (and $x2238 $x6839))) 582 (let (($x7613 (and $x1793 $x6840))) 583 (let (($x31199 (and $x1792 $x7613))) 584 (let (($x31200 (and $x3810 $x31199))) 585 (let (($x31201 (and $x2260 $x31200))) 586 (let (($x31202 (and $x88 $x31201))) 587 (let (($x31203 (and $x110 $x31202))) 588 (let (($x31204 (and $x1814 $x31203))) 589 (let (($x31205 (and $x7558 $x31204))) 590 (let (($x31206 (and $x1149 $x31205))) 591 (let (($x31207 (and $x1075 $x31206))) 592 (let (($x31189 (and $x1793 $x6836))) 593 (let (($x31190 (and $x527 $x31189))) 594 (let (($x31191 (and $x3810 $x31190))) 595 (let (($x31192 (and $x88 $x31191))) 596 (let (($x31193 (and $x992 $x31192))) 597 (let (($x31194 (and $x1814 $x31193))) 598 (let (($x31195 (and $x7558 $x31194))) 599 (let (($x31196 (and $x1149 $x31195))) 600 (let (($x31197 (and $x1076 $x31196))) 601 (let (($x31180 (and $x3810 $x7613))) 602 (let (($x31181 (and $x2260 $x31180))) 603 (let (($x31182 (and $x88 $x31181))) 604 (let (($x31183 (and $x992 $x31182))) 605 (let (($x31184 (and $x1814 $x31183))) 606 (let (($x31185 (and $x7558 $x31184))) 607 (let (($x31186 (and $x1149 $x31185))) 608 (let (($x31187 (and $x1076 $x31186))) 609 (let (($x7167 (and $x112 $x1262))) 610 (let (($x7168 (and $x2239 $x7167))) 611 (let (($x7169 (and $x2238 $x7168))) 612 (let (($x7606 (and $x1795 $x7169))) 613 (let (($x7607 (and $x1793 $x7606))) 614 (let (($x7608 (and $x1792 $x7607))) 615 (let (($x7609 (and $x390 $x7608))) 616 (let (($x7610 (and $x3810 $x7609))) 617 (let (($x7611 (and $x2260 $x7610))) 618 (let (($x7612 (and $x88 $x7611))) 619 (let (($x31174 (and $x992 $x7612))) 620 (let (($x31175 (and $x7558 $x31174))) 621 (let (($x31176 (and $x863 $x31175))) 622 (let (($x31177 (and $x1076 $x31176))) 623 (let (($x31178 (and $x1211 $x31177))) 624 (let (($x31168 (and $x110 $x7612))) 625 (let (($x31169 (and $x7558 $x31168))) 626 (let (($x31170 (and $x863 $x31169))) 627 (let (($x31171 (and $x1075 $x31170))) 628 (let (($x31172 (and $x1211 $x31171))) 629 (let (($x31156 (and $x1793 (and $x1795 (and $x555 (and $x2239 (and $x112 (and $x2240 $x1262)))))))) 630 (let (($x31162 (and $x992 (and $x88 (and $x2260 (and $x3810 (and $x390 (and $x1792 $x31156)))))))) 631 (let (($x6864 (and $x2241 $x1232))) 632 (let (($x6865 (and $x112 $x6864))) 633 (let (($x6866 (and $x2239 $x6865))) 634 (let (($x6867 (and $x2238 $x6866))) 635 (let (($x7602 (and $x1795 $x6867))) 636 (let (($x7603 (and $x1793 $x7602))) 637 (let (($x7604 (and $x1792 $x7603))) 638 (let (($x7605 (and $x3810 $x7604))) 639 (let (($x31149 (and $x2260 $x7605))) 640 (let (($x31150 (and $x88 $x31149))) 641 (let (($x31151 (and $x992 $x31150))) 642 (let (($x31152 (and $x1814 $x31151))) 643 (let (($x31153 (and $x1076 $x31152))) 644 (let (($x7575 (and $x3810 $x7574))) 645 (let (($x31144 (and $x7539 $x7575))) 646 (let (($x31145 (and $x992 $x31144))) 647 (let (($x31146 (and $x1814 $x31145))) 648 (let (($x31147 (and $x1149 $x31146))) 649 (let (($x7552 (and $x7540 $x7551))) 650 (let (($x7553 (and $x2260 $x7552))) 651 (let (($x31140 (and $x110 $x7553))) 652 (let (($x31141 (and $x1814 $x31140))) 653 (let (($x31142 (and $x106 $x31141))) 654 (let (($x31136 (and $x992 $x7556))) 655 (let (($x31137 (and $x1814 $x31136))) 656 (let (($x31138 (and $x1149 $x31137))) 657 (let (($x7598 (and $x7540 $x7550))) 658 (let (($x7599 (and $x2260 $x7598))) 659 (let (($x7600 (and $x88 $x7599))) 660 (let (($x7601 (and $x1814 $x7600))) 661 (let (($x31133 (and $x1149 $x7601))) 662 (let (($x31134 (and $x1211 $x31133))) 663 (let (($x31130 (and $x106 $x7601))) 664 (let (($x31131 (and $x1025 $x31130))) 665 (let (($x7567 (and $x1794 $x6809))) 666 (let (($x7568 (and $x487 $x7567))) 667 (let (($x7569 (and $x494 $x7568))) 668 (let (($x7593 (and $x527 $x7569))) 669 (let (($x7594 (and $x3810 $x7593))) 670 (let (($x7595 (and $x88 $x7594))) 671 (let (($x7596 (and $x992 $x7595))) 672 (let (($x7597 (and $x1814 $x7596))) 673 (let (($x31127 (and $x1149 $x7597))) 674 (let (($x31128 (and $x1076 $x31127))) 675 (let (($x31124 (and $x106 $x7597))) 676 (let (($x31125 (and $x1075 $x31124))) 677 (let (($x7564 (and $x7540 $x7563))) 678 (let (($x7565 (and $x2260 $x7564))) 679 (let (($x7566 (and $x88 $x7565))) 680 (let (($x31121 (and $x863 $x7566))) 681 (let (($x31122 (and $x1211 $x31121))) 682 (let (($x31117 (and $x992 $x7592))) 683 (let (($x31118 (and $x1814 $x31117))) 684 (let (($x31119 (and $x863 $x31118))) 685 (let (($x7582 (and $x1794 $x7115))) 686 (let (($x7583 (and $x487 $x7582))) 687 (let (($x7584 (and $x494 $x7583))) 688 (let (($x7585 (and $x527 $x7584))) 689 (let (($x7586 (and $x3810 $x7585))) 690 (let (($x7587 (and $x2260 $x7586))) 691 (let (($x7588 (and $x88 $x7587))) 692 (let (($x7589 (and $x1814 $x7588))) 693 (let (($x7590 (and $x569 $x7589))) 694 (let (($x31114 (and $x1149 $x7590))) 695 (let (($x31115 (and $x1076 $x31114))) 696 (let (($x31111 (and $x106 $x7590))) 697 (let (($x31112 (and $x1075 $x31111))) 698 (let (($x7546 (and $x7540 $x7545))) 699 (let (($x7547 (and $x2260 $x7546))) 700 (let (($x31107 (and $x110 $x7547))) 701 (let (($x31108 (and $x1814 $x31107))) 702 (let (($x31109 (and $x106 $x31108))) 703 (let (($x31103 (and $x992 $x7554))) 704 (let (($x31104 (and $x1814 $x31103))) 705 (let (($x31105 (and $x1149 $x31104))) 706 (let (($x31099 (and $x110 $x7581))) 707 (let (($x31100 (and $x7558 $x31099))) 708 (let (($x31101 (and $x1075 $x31100))) 709 (let (($x31095 (and $x88 $x7575))) 710 (let (($x31096 (and $x992 $x31095))) 711 (let (($x31097 (and $x1814 $x31096))) 712 (let (($x7557 (and $x88 $x7556))) 713 (let (($x31093 (and $x7558 $x7557))) 714 (let (($x7570 (and $x3810 $x7569))) 715 (let (($x7571 (and $x2260 $x7570))) 716 (let (($x7572 (and $x88 $x7571))) 717 (let (($x7573 (and $x1814 $x7572))) 718 (let (($x31090 (and $x1149 $x7573))) 719 (let (($x31091 (and $x1076 $x31090))) 720 (let (($x31087 (and $x106 $x7573))) 721 (let (($x31088 (and $x1075 $x31087))) 722 (let (($x31084 (and $x1814 $x7566))) 723 (let (($x31085 (and $x863 $x31084))) 724 (let (($x7555 (and $x88 $x7554))) 725 (let (($x31082 (and $x7558 $x7555))) 726 (let (($x31080 (and $x992 $x7557))) 727 (let (($x31078 (and $x992 $x7555))) 728 (let (($x31076 (and $x88 $x7553))) 729 (let (($x31075 (and $x88 $x7547))) 730 (let (($x31077 (or $x31075 $x31076))) 731 (let (($x31079 (or $x31077 $x31078))) 732 (let (($x31081 (or $x31079 $x31080))) 733 (let (($x31083 (or $x31081 $x31082))) 734 (let (($x31086 (or $x31083 $x31085))) 735 (let (($x31089 (or $x31086 $x31088))) 736 (let (($x31092 (or $x31089 $x31091))) 737 (let (($x31094 (or $x31092 $x31093))) 738 (let (($x31098 (or $x31094 $x31097))) 739 (let (($x31102 (or $x31098 $x31101))) 740 (let (($x31106 (or $x31102 $x31105))) 741 (let (($x31110 (or $x31106 $x31109))) 742 (let (($x31113 (or $x31110 $x31112))) 743 (let (($x31116 (or $x31113 $x31115))) 744 (let (($x31120 (or $x31116 $x31119))) 745 (let (($x31123 (or $x31120 $x31122))) 746 (let (($x31126 (or $x31123 $x31125))) 747 (let (($x31129 (or $x31126 $x31128))) 748 (let (($x31132 (or $x31129 $x31131))) 749 (let (($x31135 (or $x31132 $x31134))) 750 (let (($x31139 (or $x31135 $x31138))) 751 (let (($x31143 (or $x31139 $x31142))) 752 (let (($x31148 (or $x31143 $x31147))) 753 (let (($x31154 (or $x31148 $x31153))) 754 (let (($x31173 (or (or $x31154 (and $x1211 (and $x1075 (and $x863 (and $x7558 $x31162))))) $x31172))) 755 (let (($x31224 (or (or (or (or (or (or (or $x31173 $x31178) $x31187) $x31197) $x31207) $x31213) $x31217) $x31223))) 756 (let (($x31252 (or (or (or (or (or (or (or $x31224 $x31226) $x31230) $x31234) $x31239) $x31243) $x31248) $x31251))) 757 (let (($x31267 (or (or $x31252 $x31254) (and $x1211 (and $x1075 (and $x1149 (and $x863 (and $x7558 $x31261)))))))) 758 (or (or (or (or (or $x31267 $x31274) $x31282) $x31296) $x31309) $x31314)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) 759(assert 760 (let ((?x105 (t.nxt t.curr))) 761 (let (($x562 (= ?x105 t.p))) 762 (not $x562)))) 763(assert 764 (let (($x351 (t.H_nxt t.curr))) 765 (not $x351))) 766(assert 767 (let (($x1625 (= NULL t.curr))) 768 (not $x1625))) 769(check-sat) 770