(set-logic QF_UFIDL)
; benchmark generated from python API
(set-info :status unknown)
(declare-fun t.R_nxt (Int Int) Bool)
(declare-fun t.curr () Int)
(declare-fun t.l () Int)
(declare-fun en_LOCATION () Int)
(declare-fun t.pc () Int)
(declare-fun NULL () Int)
(declare-fun i1 () Int)
(declare-fun t.nxt (Int) Int)
(declare-fun i2 () Int)
(declare-fun t.p () Int)
(declare-fun t.suc () Int)
(declare-fun t.data (Int) Int)
(declare-fun t.H_nxt (Int) Bool)
(declare-fun t.I_nxt (Int) Int)
(assert
 (t.R_nxt t.l t.curr))
(assert
 (let ((?x15 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION))))))))
 (let ((?x17 (+ 1 (+ 1 ?x15))))
 (let (($x19 (= t.pc ?x17)))
 (let (($x22 (not $x19)))
 (let (($x1230 (= i1 NULL)))
 (let (($x1231 (not $x1230)))
 (let (($x1267 (and $x1231 $x22)))
 (let (($x30 (= i1 t.l)))
 (let (($x31 (not $x30)))
 (let (($x1268 (and $x31 $x1267)))
 (let (($x895 (= i1 t.curr)))
 (let (($x1229 (not $x895)))
 (and $x1229 $x1268))))))))))))))

(assert
 (let ((?x93 (t.nxt t.suc)))
 (= ?x93 t.suc)))
(assert
 (let ((?x15 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION))))))))
 (let ((?x17 (+ 1 (+ 1 ?x15))))
 (let (($x19 (= t.pc ?x17)))
 (let (($x22 (not $x19)))
 (let (($x117 (= t.pc ?x15)))
 (let (($x1232 (not $x117)))
 (let (($x1319 (and $x1232 $x22)))
 (let (($x1331 (= i2 NULL)))
 (let (($x1332 (not $x1331)))
 (let (($x2541 (and $x1332 $x1319)))
 (let (($x945 (= i2 t.suc)))
 (let (($x1329 (not $x945)))
 (let (($x2908 (and $x1329 $x2541)))
 (let (($x119 (= t.suc NULL)))
 (let (($x15330 (and $x119 $x2908)))
 (let (($x1013 (= t.curr t.suc)))
 (let (($x1646 (not $x1013)))
 (let (($x15331 (and $x1646 $x15330)))
 (let (($x335 (t.H_nxt i2)))
 (let (($x2479 (not $x335)))
 (let (($x15332 (and $x2479 $x15331)))
 (let (($x15333 (and $x1329 $x15332)))
 (let (($x951 (= i2 t.p)))
 (let (($x1351 (not $x951)))
 (let (($x15334 (and $x1351 $x15333)))
 (let (($x64 (= t.l t.suc)))
 (let (($x65 (not $x64)))
 (let (($x15335 (and $x65 $x15334)))
 (let (($x38 (t.R_nxt t.l i2)))
 (let (($x15336 (and $x38 $x15335)))
 (let (($x1061 (= t.suc t.p)))
 (let (($x1683 (not $x1061)))
 (let (($x15337 (and $x1683 $x15336)))
 (let ((?x398 (t.nxt i2)))
 (let (($x430 (= t.suc ?x398)))
 (let (($x2876 (not $x430)))
 (let (($x15338 (and $x2876 $x15337)))
 (let ((?x396 (t.I_nxt i2)))
 (let (($x428 (= ?x396 t.suc)))
 (let (($x15339 (and $x428 $x15338)))
 (let (($x1043 (t.R_nxt t.suc i2)))
 (let (($x1044 (not $x1043)))
 (let (($x15340 (and $x1044 $x15339)))
 (let (($x15341 (and $x1044 $x15340)))
 (let (($x943 (t.R_nxt i2 t.suc)))
 (let (($x944 (not $x943)))
 (let (($x15342 (and $x944 $x15341)))
 (let (($x1262 (and $x117 $x22)))
 (let (($x2485 (and $x1332 $x1262)))
 (let (($x39 (= i2 t.l)))
 (let (($x40 (not $x39)))
 (let (($x2486 (and $x40 $x2485)))
 (let (($x939 (= i2 t.curr)))
 (let (($x1330 (not $x939)))
 (let (($x2487 (and $x1330 $x2486)))
 (let (($x2488 (and $x1329 $x2487)))
 (let (($x120 (not $x119)))
 (let (($x2904 (and $x120 $x2488)))
 (let (($x2905 (and $x1646 $x2904)))
 (let (($x2906 (and $x2479 $x2905)))
 (let (($x2907 (and $x1329 $x2906)))
 (let (($x2878 (not (< (t.data t.suc) (t.data i2)))))
 (let (($x15321 (and $x2878 $x2907)))
 (let (($x15322 (and $x1351 $x15321)))
 (let (($x15323 (and $x65 $x15322)))
 (let (($x15324 (and $x1683 $x15323)))
 (let (($x15325 (and $x2876 $x15324)))
 (let (($x429 (not $x428)))
 (let (($x15326 (and $x429 $x15325)))
 (let (($x15327 (and $x1044 $x15326)))
 (let (($x15328 (and $x1044 $x15327)))
 (let (($x15313 (and $x65 $x2907)))
 (let (($x973 (not $x38)))
 (let (($x15314 (and $x973 $x15313)))
 (let (($x15315 (and $x1683 $x15314)))
 (let (($x15316 (and $x429 $x15315)))
 (let (($x15317 (and $x1044 $x15316)))
 (let (($x15318 (and $x1044 $x15317)))
 (let (($x15319 (and $x943 $x15318)))
 (let (($x2489 (and $x1332 $x22)))
 (let (($x2490 (and $x40 $x2489)))
 (let (($x2491 (and $x1330 $x2490)))
 (let (($x2508 (and $x945 $x2491)))
 (let (($x15299 (and $x120 $x2508)))
 (let (($x15300 (and $x1646 $x15299)))
 (let (($x15301 (and $x2479 $x15300)))
 (let (($x15302 (and $x945 $x15301)))
 (let (($x15303 (and $x2878 $x15302)))
 (let (($x15304 (and $x1351 $x15303)))
 (let (($x15305 (and $x65 $x15304)))
 (let (($x15306 (and $x38 $x15305)))
 (let (($x15307 (and $x1683 $x15306)))
 (let (($x15308 (and $x429 $x15307)))
 (let (($x15309 (and $x1043 $x15308)))
 (let (($x15310 (and $x1043 $x15309)))
 (let (($x15311 (and $x943 $x15310)))
 (let (($x2855 (and $x1330 $x2489)))
 (let (($x2856 (and $x1329 $x2855)))
 (let (($x15285 (and $x119 $x2856)))
 (let (($x15286 (and $x1646 $x15285)))
 (let (($x15287 (and $x2479 $x15286)))
 (let (($x15288 (and $x1329 $x15287)))
 (let (($x15289 (and $x1351 $x15288)))
 (let (($x15290 (and $x65 $x15289)))
 (let (($x15291 (and $x38 $x15290)))
 (let (($x15292 (and $x1683 $x15291)))
 (let (($x15293 (and $x2876 $x15292)))
 (let (($x15294 (and $x428 $x15293)))
 (let (($x15295 (and $x1044 $x15294)))
 (let (($x15296 (and $x1044 $x15295)))
 (let (($x15297 (and $x944 $x15296)))
 (let (($x2902 (and $x939 $x2485)))
 (let (($x2903 (and $x1329 $x2902)))
 (let (($x15271 (and $x119 $x2903)))
 (let (($x15272 (and $x1646 $x15271)))
 (let (($x15273 (and $x2479 $x15272)))
 (let (($x15274 (and $x1329 $x15273)))
 (let (($x15275 (and $x1351 $x15274)))
 (let (($x15276 (and $x65 $x15275)))
 (let (($x15277 (and $x38 $x15276)))
 (let (($x15278 (and $x1683 $x15277)))
 (let (($x15279 (and $x430 $x15278)))
 (let (($x15280 (and $x428 $x15279)))
 (let (($x15281 (and $x1044 $x15280)))
 (let (($x15282 (and $x1044 $x15281)))
 (let (($x15283 (and $x944 $x15282)))
 (let (($x2769 (and $x40 $x22)))
 (let (($x2770 (and $x1330 $x2769)))
 (let (($x2771 (and $x1329 $x2770)))
 (let (($x2896 (and $x120 $x2771)))
 (let (($x2897 (and $x1646 $x2896)))
 (let (($x2898 (and $x335 $x2897)))
 (let (($x2899 (and $x1329 $x2898)))
 (let (($x2900 (and $x1351 $x2899)))
 (let (($x2901 (and $x65 $x2900)))
 (let (($x15263 (and $x973 $x2901)))
 (let (($x15264 (and $x1683 $x15263)))
 (let (($x15265 (and $x2876 $x15264)))
 (let (($x15266 (and $x429 $x15265)))
 (let (($x15267 (and $x1044 $x15266)))
 (let (($x15268 (and $x1044 $x15267)))
 (let (($x15269 (and $x944 $x15268)))
 (let (($x15255 (and $x38 $x2901)))
 (let (($x15256 (and $x1683 $x15255)))
 (let (($x15257 (and $x2876 $x15256)))
 (let (($x15258 (and $x429 $x15257)))
 (let (($x15259 (and $x1043 $x15258)))
 (let (($x15260 (and $x1043 $x15259)))
 (let (($x15261 (and $x944 $x15260)))
 (let (($x2492 (and $x1329 $x2491)))
 (let (($x15243 (and $x119 $x2492)))
 (let (($x15244 (and $x1646 $x15243)))
 (let (($x15245 (and $x1329 $x15244)))
 (let (($x15246 (and $x1351 $x15245)))
 (let (($x15247 (and $x65 $x15246)))
 (let (($x15248 (and $x973 $x15247)))
 (let (($x15249 (and $x1683 $x15248)))
 (let (($x15250 (and $x428 $x15249)))
 (let (($x15251 (and $x1044 $x15250)))
 (let (($x15252 (and $x1044 $x15251)))
 (let (($x15253 (and $x944 $x15252)))
 (let (($x2891 (and $x120 $x2492)))
 (let (($x2892 (and $x1646 $x2891)))
 (let (($x2893 (and $x1329 $x2892)))
 (let (($x2894 (and $x1351 $x2893)))
 (let (($x2895 (and $x65 $x2894)))
 (let (($x15237 (and $x38 $x2895)))
 (let (($x15238 (and $x1683 $x15237)))
 (let (($x15239 (and $x2876 $x15238)))
 (let (($x15240 (and $x1043 $x15239)))
 (let (($x15241 (and $x1043 $x15240)))
 (let (($x2887 (and $x119 $x2488)))
 (let (($x2888 (and $x1646 $x2887)))
 (let (($x2889 (and $x2479 $x2888)))
 (let (($x2890 (and $x1329 $x2889)))
 (let (($x15229 (and $x65 $x2890)))
 (let (($x15230 (and $x973 $x15229)))
 (let (($x15231 (and $x1683 $x15230)))
 (let (($x15232 (and $x428 $x15231)))
 (let (($x15233 (and $x1044 $x15232)))
 (let (($x15234 (and $x1044 $x15233)))
 (let (($x15235 (and $x944 $x15234)))
 (let (($x15221 (and $x1351 $x2890)))
 (let (($x15222 (and $x65 $x15221)))
 (let (($x15223 (and $x1683 $x15222)))
 (let (($x15224 (and $x2876 $x15223)))
 (let (($x15225 (and $x428 $x15224)))
 (let (($x15226 (and $x1044 $x15225)))
 (let (($x15227 (and $x1044 $x15226)))
 (let (($x1233 (and $x19 $x1232)))
 (let (($x2468 (and $x1331 $x1233)))
 (let (($x2469 (and $x40 $x2468)))
 (let (($x2470 (and $x939 $x2469)))
 (let (($x2471 (and $x945 $x2470)))
 (let (($x2879 (and $x119 $x2471)))
 (let (($x2880 (and $x1013 $x2879)))
 (let (($x2881 (and $x335 $x2880)))
 (let (($x2882 (and $x945 $x2881)))
 (let (($x2883 (and $x2878 $x2882)))
 (let (($x2884 (and $x1351 $x2883)))
 (let (($x2885 (and $x65 $x2884)))
 (let (($x2886 (and $x1683 $x2885)))
 (let (($x15217 (and $x1044 $x2886)))
 (let (($x15218 (and $x1044 $x15217)))
 (let (($x15219 (and $x944 $x15218)))
 (let (($x15213 (and $x1043 $x2886)))
 (let (($x15214 (and $x1043 $x15213)))
 (let (($x15215 (and $x943 $x15214)))
 (let (($x15203 (and $x1646 $x2488)))
 (let (($x15204 (and $x2479 $x15203)))
 (let (($x15205 (and $x1329 $x15204)))
 (let (($x15206 (and $x65 $x15205)))
 (let (($x15207 (and $x973 $x15206)))
 (let (($x15208 (and $x1683 $x15207)))
 (let (($x15209 (and $x2876 $x15208)))
 (let (($x15210 (and $x1044 $x15209)))
 (let (($x15211 (and $x1044 $x15210)))
 (let (($x15193 (and $x1646 $x2492)))
 (let (($x15194 (and $x1329 $x15193)))
 (let (($x15195 (and $x1351 $x15194)))
 (let (($x15196 (and $x65 $x15195)))
 (let (($x15197 (and $x973 $x15196)))
 (let (($x15198 (and $x1683 $x15197)))
 (let (($x15199 (and $x2876 $x15198)))
 (let (($x15200 (and $x1044 $x15199)))
 (let (($x15201 (and $x1044 $x15200)))
 (let (($x2457 (and $x1332 $x1233)))
 (let (($x2458 (and $x40 $x2457)))
 (let (($x2459 (and $x1330 $x2458)))
 (let (($x2460 (and $x1329 $x2459)))
 (let (($x2857 (and $x119 $x2460)))
 (let (($x2858 (and $x1013 $x2857)))
 (let (($x2871 (and $x2479 $x2858)))
 (let (($x2872 (and $x1329 $x2871)))
 (let (($x2873 (and $x65 $x2872)))
 (let (($x2874 (and $x973 $x2873)))
 (let (($x2875 (and $x1683 $x2874)))
 (let (($x15190 (and $x1044 $x2875)))
 (let (($x15191 (and $x1044 $x15190)))
 (let (($x15187 (and $x1043 $x2875)))
 (let (($x15188 (and $x1043 $x15187)))
 (let (($x2805 (and $x1330 $x2457)))
 (let (($x2806 (and $x1329 $x2805)))
 (let (($x2863 (and $x119 $x2806)))
 (let (($x2864 (and $x1013 $x2863)))
 (let (($x2865 (and $x2479 $x2864)))
 (let (($x2866 (and $x1329 $x2865)))
 (let (($x2867 (and $x1351 $x2866)))
 (let (($x2868 (and $x65 $x2867)))
 (let (($x2869 (and $x1683 $x2868)))
 (let (($x2870 (and $x428 $x2869)))
 (let (($x15184 (and $x1044 $x2870)))
 (let (($x15185 (and $x1044 $x15184)))
 (let (($x15181 (and $x1043 $x2870)))
 (let (($x15182 (and $x1043 $x15181)))
 (let (($x2859 (and $x1329 $x2858)))
 (let (($x2860 (and $x1351 $x2859)))
 (let (($x2861 (and $x65 $x2860)))
 (let (($x2862 (and $x1683 $x2861)))
 (let (($x15178 (and $x1044 $x2862)))
 (let (($x15179 (and $x1044 $x15178)))
 (let (($x15176 (and $x1043 $x2862)))
 (let (($x15177 (and $x1043 $x15176)))
 (let (($x15180 (or $x15177 $x15179)))
 (let (($x15183 (or $x15180 $x15182)))
 (let (($x15186 (or $x15183 $x15185)))
 (let (($x15189 (or $x15186 $x15188)))
 (let (($x15192 (or $x15189 $x15191)))
 (let (($x15202 (or $x15192 $x15201)))
 (let (($x15212 (or $x15202 $x15211)))
 (let (($x15216 (or $x15212 $x15215)))
 (let (($x15220 (or $x15216 $x15219)))
 (let (($x15228 (or $x15220 $x15227)))
 (let (($x15236 (or $x15228 $x15235)))
 (let (($x15242 (or $x15236 $x15241)))
 (let (($x15254 (or $x15242 $x15253)))
 (let (($x15262 (or $x15254 $x15261)))
 (let (($x15270 (or $x15262 $x15269)))
 (let (($x15284 (or $x15270 $x15283)))
 (let (($x15298 (or $x15284 $x15297)))
 (let (($x15312 (or $x15298 $x15311)))
 (let (($x15320 (or $x15312 $x15319)))
 (let (($x15329 (or $x15320 $x15328)))
 (let (($x15343 (or $x15329 $x15342)))
 (not $x15343))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))



(assert
 (let ((?x105 (t.nxt t.curr)))
 (let (($x548 (= ?x105 t.curr)))
 (not $x548))))

(assert
 (let ((?x6 (t.nxt t.l)))
 (let (($x87 (= ?x6 t.l)))
 (not $x87))))
(assert
 (t.R_nxt t.suc i2))
(assert
 (let ((?x105 (t.nxt t.curr)))
 (let (($x390 (t.H_nxt ?x105)))
 (let (($x527 (not $x390)))
 (not $x527)))))
(assert
 (let ((?x15 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION))))))))
 (let ((?x17 (+ 1 (+ 1 ?x15))))
 (let (($x19 (= t.pc ?x17)))
 (let (($x22 (not $x19)))
 (let ((?x93 (t.nxt t.suc)))
 (let (($x2017 (= ?x93 NULL)))
 (let (($x2018 (not $x2017)))
 (let (($x5672 (and $x2018 $x22)))
 (let (($x99 (= ?x93 t.l)))
 (let (($x100 (not $x99)))
 (let (($x5673 (and $x100 $x5672)))
 (let (($x608 (= ?x93 t.curr)))
 (let (($x2016 (not $x608)))
 (let (($x5674 (and $x2016 $x5673)))
 (not $x5674))))))))))))))))
(assert
 (let ((?x15 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION))))))))
 (let ((?x17 (+ 1 (+ 1 ?x15))))
 (let (($x19 (= t.pc ?x17)))
 (let (($x22 (not $x19)))
 (let ((?x105 (t.nxt t.curr)))
 (let (($x2240 (= ?x105 NULL)))
 (let (($x2241 (not $x2240)))
 (let (($x6837 (and $x2241 $x22)))
 (let (($x111 (= ?x105 t.l)))
 (let (($x112 (not $x111)))
 (let (($x6838 (and $x112 $x6837)))
 (let (($x548 (= ?x105 t.curr)))
 (let (($x2239 (not $x548)))
 (let (($x6839 (and $x2239 $x6838)))
 (let ((?x6 (t.nxt t.l)))
 (let (($x1794 (= ?x6 NULL)))
 (let (($x7644 (and $x1794 $x6839)))
 (let (($x487 (= ?x6 t.curr)))
 (let (($x1793 (not $x487)))
 (let (($x7645 (and $x1793 $x7644)))
 (let (($x494 (= ?x6 t.suc)))
 (let (($x1792 (not $x494)))
 (let (($x7646 (and $x1792 $x7645)))
 (let (($x390 (t.H_nxt ?x105)))
 (let (($x527 (not $x390)))
 (let (($x7647 (and $x527 $x7646)))
 (let (($x519 (= ?x105 ?x6)))
 (let (($x3810 (not $x519)))
 (let (($x7648 (and $x3810 $x7647)))
 (let (($x562 (= ?x105 t.p)))
 (let (($x2260 (not $x562)))
 (let (($x7649 (and $x2260 $x7648)))
 (let (($x87 (= ?x6 t.l)))
 (let (($x88 (not $x87)))
 (let (($x7650 (and $x88 $x7649)))
 (let (($x110 (t.R_nxt t.l ?x105)))
 (let (($x7651 (and $x110 $x7650)))
 (let (($x501 (= ?x6 t.p)))
 (let (($x1814 (not $x501)))
 (let (($x7652 (and $x1814 $x7651)))
 (let ((?x824 (t.nxt ?x105)))
 (let (($x864 (= ?x6 ?x824)))
 (let (($x7558 (not $x864)))
 (let (($x31311 (and $x7558 $x7652)))
 (let ((?x528 (t.I_nxt ?x105)))
 (let (($x569 (= ?x528 ?x6)))
 (let (($x31312 (and $x569 $x31311)))
 (let (($x106 (t.R_nxt ?x6 ?x105)))
 (let (($x1149 (not $x106)))
 (let (($x31313 (and $x1149 $x31312)))
 (let (($x1075 (t.R_nxt t.suc ?x105)))
 (let (($x31314 (and $x1075 $x31313)))
 (let (($x555 (= ?x105 t.suc)))
 (let (($x2238 (not $x555)))
 (let (($x7211 (and $x2238 $x6837)))
 (let (($x1795 (not $x1794)))
 (let (($x31298 (and $x1795 $x7211)))
 (let (($x31299 (and $x1793 $x31298)))
 (let (($x31300 (and $x1792 $x31299)))
 (let (($x31301 (and $x527 $x31300)))
 (let (($x31302 (and $x3810 $x31301)))
 (let (($x31303 (and $x2260 $x31302)))
 (let (($x31304 (and $x88 $x31303)))
 (let (($x31305 (and $x110 $x31304)))
 (let (($x31306 (and $x1814 $x31305)))
 (let (($x31307 (and $x7558 $x31306)))
 (let (($x863 (not $x569)))
 (let (($x31308 (and $x863 $x31307)))
 (let (($x1076 (not $x1075)))
 (let (($x31309 (and $x1076 $x31308)))
 (let (($x31284 (and $x1794 $x7211)))
 (let (($x31285 (and $x1793 $x31284)))
 (let (($x31286 (and $x1792 $x31285)))
 (let (($x31287 (and $x527 $x31286)))
 (let (($x31288 (and $x3810 $x31287)))
 (let (($x31289 (and $x2260 $x31288)))
 (let (($x31290 (and $x88 $x31289)))
 (let (($x31291 (and $x110 $x31290)))
 (let (($x31292 (and $x1814 $x31291)))
 (let (($x31293 (and $x7558 $x31292)))
 (let (($x31294 (and $x569 $x31293)))
 (let (($x31295 (and $x1149 $x31294)))
 (let (($x31296 (and $x1076 $x31295)))
 (let (($x7203 (and $x112 $x22)))
 (let (($x7204 (and $x2239 $x7203)))
 (let (($x7205 (and $x2238 $x7204)))
 (let (($x7639 (and $x1795 $x7205)))
 (let (($x7640 (and $x1792 $x7639)))
 (let (($x7641 (and $x390 $x7640)))
 (let (($x7642 (and $x3810 $x7641)))
 (let (($x7643 (and $x2260 $x7642)))
 (let (($x992 (not $x110)))
 (let (($x31276 (and $x992 $x7643)))
 (let (($x31277 (and $x1814 $x31276)))
 (let (($x31278 (and $x7558 $x31277)))
 (let (($x31279 (and $x863 $x31278)))
 (let (($x31280 (and $x1149 $x31279)))
 (let (($x31281 (and $x1076 $x31280)))
 (let (($x1025 (t.R_nxt ?x105 ?x6)))
 (let (($x1211 (not $x1025)))
 (let (($x31282 (and $x1211 $x31281)))
 (let (($x31268 (and $x110 $x7643)))
 (let (($x31269 (and $x1814 $x31268)))
 (let (($x31270 (and $x7558 $x31269)))
 (let (($x31271 (and $x863 $x31270)))
 (let (($x31272 (and $x106 $x31271)))
 (let (($x31273 (and $x1075 $x31272)))
 (let (($x31274 (and $x1211 $x31273)))
 (let (($x6871 (and $x2240 $x22)))
 (let (($x6872 (and $x112 $x6871)))
 (let (($x6873 (and $x2239 $x6872)))
 (let (($x6874 (and $x555 $x6873)))
 (let (($x7638 (and $x1795 $x6874)))
 (let (($x31261 (and $x1814 (and $x992 (and $x2260 (and $x3810 (and $x390 (and $x1792 $x7638))))))))
 (let (($x117 (= t.pc ?x15)))
 (let (($x1232 (not $x117)))
 (let (($x1233 (and $x19 $x1232)))
 (let (($x6806 (and $x2241 $x1233)))
 (let (($x6807 (and $x112 $x6806)))
 (let (($x6808 (and $x2239 $x6807)))
 (let (($x6809 (and $x2238 $x6808)))
 (let (($x7548 (and $x1795 $x6809)))
 (let (($x7549 (and $x1793 $x7548)))
 (let (($x7550 (and $x1792 $x7549)))
 (let (($x7574 (and $x527 $x7550)))
 (let (($x7632 (and $x519 $x7574)))
 (let ((?x2234 (t.data ?x105)))
 (let ((?x1788 (t.data ?x6)))
 (let (($x7539 (< ?x1788 ?x2234)))
 (let (($x7540 (not $x7539)))
 (let (($x7633 (and $x7540 $x7632)))
 (let (($x7634 (and $x562 $x7633)))
 (let (($x7635 (and $x88 $x7634)))
 (let (($x7636 (and $x992 $x7635)))
 (let (($x7637 (and $x501 $x7636)))
 (let (($x31253 (and $x1149 $x7637)))
 (let (($x31254 (and $x1211 $x31253)))
 (let (($x31250 (and $x106 $x7637)))
 (let (($x31251 (and $x1025 $x31250)))
 (let (($x7551 (and $x3810 $x7550)))
 (let (($x7556 (and $x2260 $x7551)))
 (let (($x31245 (and $x110 $x7556)))
 (let (($x31246 (and $x1814 $x31245)))
 (let (($x31247 (and $x7558 $x31246)))
 (let (($x31248 (and $x106 $x31247)))
 (let (($x7114 (and $x2239 $x6806)))
 (let (($x7115 (and $x2238 $x7114)))
 (let (($x7559 (and $x1795 $x7115)))
 (let (($x7560 (and $x1793 $x7559)))
 (let (($x7561 (and $x1792 $x7560)))
 (let (($x7562 (and $x527 $x7561)))
 (let (($x7563 (and $x3810 $x7562)))
 (let (($x7591 (and $x2260 $x7563)))
 (let (($x7592 (and $x88 $x7591)))
 (let (($x31241 (and $x1814 $x7592)))
 (let (($x31242 (and $x7558 $x31241)))
 (let (($x31243 (and $x863 $x31242)))
 (let (($x6817 (and $x2240 $x1233)))
 (let (($x6818 (and $x112 $x6817)))
 (let (($x6819 (and $x548 $x6818)))
 (let (($x6820 (and $x555 $x6819)))
 (let (($x7541 (and $x1795 $x6820)))
 (let (($x7542 (and $x1793 $x7541)))
 (let (($x7543 (and $x1792 $x7542)))
 (let (($x7544 (and $x390 $x7543)))
 (let (($x7545 (and $x3810 $x7544)))
 (let (($x7554 (and $x2260 $x7545)))
 (let (($x31236 (and $x110 $x7554)))
 (let (($x31237 (and $x1814 $x31236)))
 (let (($x31238 (and $x7558 $x31237)))
 (let (($x31239 (and $x106 $x31238)))
 (let (($x7623 (and $x1794 $x6820)))
 (let (($x7624 (and $x487 $x7623)))
 (let (($x7625 (and $x494 $x7624)))
 (let (($x7626 (and $x390 $x7625)))
 (let (($x7627 (and $x519 $x7626)))
 (let (($x7628 (and $x7540 $x7627)))
 (let (($x7629 (and $x2260 $x7628)))
 (let (($x7630 (and $x88 $x7629)))
 (let (($x7631 (and $x1814 $x7630)))
 (let (($x31232 (and $x1149 $x7631)))
 (let (($x31233 (and $x1076 $x31232)))
 (let (($x31234 (and $x1211 $x31233)))
 (let (($x31228 (and $x106 $x7631)))
 (let (($x31229 (and $x1075 $x31228)))
 (let (($x31230 (and $x1025 $x31229)))
 (let (($x1262 (and $x117 $x22)))
 (let (($x6833 (and $x2241 $x1262)))
 (let (($x6834 (and $x112 $x6833)))
 (let (($x6835 (and $x2239 $x6834)))
 (let (($x6836 (and $x2238 $x6835)))
 (let (($x7576 (and $x1795 $x6836)))
 (let (($x7577 (and $x1793 $x7576)))
 (let (($x7578 (and $x1792 $x7577)))
 (let (($x7579 (and $x3810 $x7578)))
 (let (($x7580 (and $x2260 $x7579)))
 (let (($x7581 (and $x88 $x7580)))
 (let (($x7622 (and $x992 $x7581)))
 (let (($x31225 (and $x7558 $x7622)))
 (let (($x31226 (and $x1076 $x31225)))
 (let (($x7614 (and $x1792 $x7576)))
 (let (($x7615 (and $x3810 $x7614)))
 (let (($x7616 (and $x2260 $x7615)))
 (let (($x31219 (and $x992 $x7616)))
 (let (($x31220 (and $x1814 $x31219)))
 (let (($x31221 (and $x7558 $x31220)))
 (let (($x31222 (and $x1149 $x31221)))
 (let (($x31223 (and $x1076 $x31222)))
 (let (($x7617 (and $x527 $x7614)))
 (let (($x7618 (and $x3810 $x7617)))
 (let (($x7619 (and $x7539 $x7618)))
 (let (($x7620 (and $x992 $x7619)))
 (let (($x7621 (and $x1814 $x7620)))
 (let (($x31215 (and $x7558 $x7621)))
 (let (($x31216 (and $x1149 $x31215)))
 (let (($x31217 (and $x1076 $x31216)))
 (let (($x31209 (and $x110 $x7616)))
 (let (($x31210 (and $x1814 $x31209)))
 (let (($x31211 (and $x7558 $x31210)))
 (let (($x31212 (and $x106 $x31211)))
 (let (($x31213 (and $x1075 $x31212)))
 (let (($x6840 (and $x2238 $x6839)))
 (let (($x7613 (and $x1793 $x6840)))
 (let (($x31199 (and $x1792 $x7613)))
 (let (($x31200 (and $x3810 $x31199)))
 (let (($x31201 (and $x2260 $x31200)))
 (let (($x31202 (and $x88 $x31201)))
 (let (($x31203 (and $x110 $x31202)))
 (let (($x31204 (and $x1814 $x31203)))
 (let (($x31205 (and $x7558 $x31204)))
 (let (($x31206 (and $x1149 $x31205)))
 (let (($x31207 (and $x1075 $x31206)))
 (let (($x31189 (and $x1793 $x6836)))
 (let (($x31190 (and $x527 $x31189)))
 (let (($x31191 (and $x3810 $x31190)))
 (let (($x31192 (and $x88 $x31191)))
 (let (($x31193 (and $x992 $x31192)))
 (let (($x31194 (and $x1814 $x31193)))
 (let (($x31195 (and $x7558 $x31194)))
 (let (($x31196 (and $x1149 $x31195)))
 (let (($x31197 (and $x1076 $x31196)))
 (let (($x31180 (and $x3810 $x7613)))
 (let (($x31181 (and $x2260 $x31180)))
 (let (($x31182 (and $x88 $x31181)))
 (let (($x31183 (and $x992 $x31182)))
 (let (($x31184 (and $x1814 $x31183)))
 (let (($x31185 (and $x7558 $x31184)))
 (let (($x31186 (and $x1149 $x31185)))
 (let (($x31187 (and $x1076 $x31186)))
 (let (($x7167 (and $x112 $x1262)))
 (let (($x7168 (and $x2239 $x7167)))
 (let (($x7169 (and $x2238 $x7168)))
 (let (($x7606 (and $x1795 $x7169)))
 (let (($x7607 (and $x1793 $x7606)))
 (let (($x7608 (and $x1792 $x7607)))
 (let (($x7609 (and $x390 $x7608)))
 (let (($x7610 (and $x3810 $x7609)))
 (let (($x7611 (and $x2260 $x7610)))
 (let (($x7612 (and $x88 $x7611)))
 (let (($x31174 (and $x992 $x7612)))
 (let (($x31175 (and $x7558 $x31174)))
 (let (($x31176 (and $x863 $x31175)))
 (let (($x31177 (and $x1076 $x31176)))
 (let (($x31178 (and $x1211 $x31177)))
 (let (($x31168 (and $x110 $x7612)))
 (let (($x31169 (and $x7558 $x31168)))
 (let (($x31170 (and $x863 $x31169)))
 (let (($x31171 (and $x1075 $x31170)))
 (let (($x31172 (and $x1211 $x31171)))
 (let (($x31156 (and $x1793 (and $x1795 (and $x555 (and $x2239 (and $x112 (and $x2240 $x1262))))))))
 (let (($x31162 (and $x992 (and $x88 (and $x2260 (and $x3810 (and $x390 (and $x1792 $x31156))))))))
 (let (($x6864 (and $x2241 $x1232)))
 (let (($x6865 (and $x112 $x6864)))
 (let (($x6866 (and $x2239 $x6865)))
 (let (($x6867 (and $x2238 $x6866)))
 (let (($x7602 (and $x1795 $x6867)))
 (let (($x7603 (and $x1793 $x7602)))
 (let (($x7604 (and $x1792 $x7603)))
 (let (($x7605 (and $x3810 $x7604)))
 (let (($x31149 (and $x2260 $x7605)))
 (let (($x31150 (and $x88 $x31149)))
 (let (($x31151 (and $x992 $x31150)))
 (let (($x31152 (and $x1814 $x31151)))
 (let (($x31153 (and $x1076 $x31152)))
 (let (($x7575 (and $x3810 $x7574)))
 (let (($x31144 (and $x7539 $x7575)))
 (let (($x31145 (and $x992 $x31144)))
 (let (($x31146 (and $x1814 $x31145)))
 (let (($x31147 (and $x1149 $x31146)))
 (let (($x7552 (and $x7540 $x7551)))
 (let (($x7553 (and $x2260 $x7552)))
 (let (($x31140 (and $x110 $x7553)))
 (let (($x31141 (and $x1814 $x31140)))
 (let (($x31142 (and $x106 $x31141)))
 (let (($x31136 (and $x992 $x7556)))
 (let (($x31137 (and $x1814 $x31136)))
 (let (($x31138 (and $x1149 $x31137)))
 (let (($x7598 (and $x7540 $x7550)))
 (let (($x7599 (and $x2260 $x7598)))
 (let (($x7600 (and $x88 $x7599)))
 (let (($x7601 (and $x1814 $x7600)))
 (let (($x31133 (and $x1149 $x7601)))
 (let (($x31134 (and $x1211 $x31133)))
 (let (($x31130 (and $x106 $x7601)))
 (let (($x31131 (and $x1025 $x31130)))
 (let (($x7567 (and $x1794 $x6809)))
 (let (($x7568 (and $x487 $x7567)))
 (let (($x7569 (and $x494 $x7568)))
 (let (($x7593 (and $x527 $x7569)))
 (let (($x7594 (and $x3810 $x7593)))
 (let (($x7595 (and $x88 $x7594)))
 (let (($x7596 (and $x992 $x7595)))
 (let (($x7597 (and $x1814 $x7596)))
 (let (($x31127 (and $x1149 $x7597)))
 (let (($x31128 (and $x1076 $x31127)))
 (let (($x31124 (and $x106 $x7597)))
 (let (($x31125 (and $x1075 $x31124)))
 (let (($x7564 (and $x7540 $x7563)))
 (let (($x7565 (and $x2260 $x7564)))
 (let (($x7566 (and $x88 $x7565)))
 (let (($x31121 (and $x863 $x7566)))
 (let (($x31122 (and $x1211 $x31121)))
 (let (($x31117 (and $x992 $x7592)))
 (let (($x31118 (and $x1814 $x31117)))
 (let (($x31119 (and $x863 $x31118)))
 (let (($x7582 (and $x1794 $x7115)))
 (let (($x7583 (and $x487 $x7582)))
 (let (($x7584 (and $x494 $x7583)))
 (let (($x7585 (and $x527 $x7584)))
 (let (($x7586 (and $x3810 $x7585)))
 (let (($x7587 (and $x2260 $x7586)))
 (let (($x7588 (and $x88 $x7587)))
 (let (($x7589 (and $x1814 $x7588)))
 (let (($x7590 (and $x569 $x7589)))
 (let (($x31114 (and $x1149 $x7590)))
 (let (($x31115 (and $x1076 $x31114)))
 (let (($x31111 (and $x106 $x7590)))
 (let (($x31112 (and $x1075 $x31111)))
 (let (($x7546 (and $x7540 $x7545)))
 (let (($x7547 (and $x2260 $x7546)))
 (let (($x31107 (and $x110 $x7547)))
 (let (($x31108 (and $x1814 $x31107)))
 (let (($x31109 (and $x106 $x31108)))
 (let (($x31103 (and $x992 $x7554)))
 (let (($x31104 (and $x1814 $x31103)))
 (let (($x31105 (and $x1149 $x31104)))
 (let (($x31099 (and $x110 $x7581)))
 (let (($x31100 (and $x7558 $x31099)))
 (let (($x31101 (and $x1075 $x31100)))
 (let (($x31095 (and $x88 $x7575)))
 (let (($x31096 (and $x992 $x31095)))
 (let (($x31097 (and $x1814 $x31096)))
 (let (($x7557 (and $x88 $x7556)))
 (let (($x31093 (and $x7558 $x7557)))
 (let (($x7570 (and $x3810 $x7569)))
 (let (($x7571 (and $x2260 $x7570)))
 (let (($x7572 (and $x88 $x7571)))
 (let (($x7573 (and $x1814 $x7572)))
 (let (($x31090 (and $x1149 $x7573)))
 (let (($x31091 (and $x1076 $x31090)))
 (let (($x31087 (and $x106 $x7573)))
 (let (($x31088 (and $x1075 $x31087)))
 (let (($x31084 (and $x1814 $x7566)))
 (let (($x31085 (and $x863 $x31084)))
 (let (($x7555 (and $x88 $x7554)))
 (let (($x31082 (and $x7558 $x7555)))
 (let (($x31080 (and $x992 $x7557)))
 (let (($x31078 (and $x992 $x7555)))
 (let (($x31076 (and $x88 $x7553)))
 (let (($x31075 (and $x88 $x7547)))
 (let (($x31077 (or $x31075 $x31076)))
 (let (($x31079 (or $x31077 $x31078)))
 (let (($x31081 (or $x31079 $x31080)))
 (let (($x31083 (or $x31081 $x31082)))
 (let (($x31086 (or $x31083 $x31085)))
 (let (($x31089 (or $x31086 $x31088)))
 (let (($x31092 (or $x31089 $x31091)))
 (let (($x31094 (or $x31092 $x31093)))
 (let (($x31098 (or $x31094 $x31097)))
 (let (($x31102 (or $x31098 $x31101)))
 (let (($x31106 (or $x31102 $x31105)))
 (let (($x31110 (or $x31106 $x31109)))
 (let (($x31113 (or $x31110 $x31112)))
 (let (($x31116 (or $x31113 $x31115)))
 (let (($x31120 (or $x31116 $x31119)))
 (let (($x31123 (or $x31120 $x31122)))
 (let (($x31126 (or $x31123 $x31125)))
 (let (($x31129 (or $x31126 $x31128)))
 (let (($x31132 (or $x31129 $x31131)))
 (let (($x31135 (or $x31132 $x31134)))
 (let (($x31139 (or $x31135 $x31138)))
 (let (($x31143 (or $x31139 $x31142)))
 (let (($x31148 (or $x31143 $x31147)))
 (let (($x31154 (or $x31148 $x31153)))
 (let (($x31173 (or (or $x31154 (and $x1211 (and $x1075 (and $x863 (and $x7558 $x31162))))) $x31172)))
 (let (($x31224 (or (or (or (or (or (or (or $x31173 $x31178) $x31187) $x31197) $x31207) $x31213) $x31217) $x31223)))
 (let (($x31252 (or (or (or (or (or (or (or $x31224 $x31226) $x31230) $x31234) $x31239) $x31243) $x31248) $x31251)))
 (let (($x31267 (or (or $x31252 $x31254) (and $x1211 (and $x1075 (and $x1149 (and $x863 (and $x7558 $x31261))))))))
 (or (or (or (or (or $x31267 $x31274) $x31282) $x31296) $x31309) $x31314))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(assert
 (let ((?x105 (t.nxt t.curr)))
 (let (($x562 (= ?x105 t.p)))
 (not $x562))))
(assert
 (let (($x351 (t.H_nxt t.curr)))
 (not $x351)))
(assert
 (let (($x1625 (= NULL t.curr)))
 (not $x1625)))
(check-sat)