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