-
Notifications
You must be signed in to change notification settings - Fork 0
/
div.c.50-sfxp_16.16_RU_WP.smt2
367 lines (367 loc) · 18 KB
/
div.c.50-sfxp_16.16_RU_WP.smt2
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
(set-info :smt-lib-version 2.6)
(set-logic QF_FXP)
(set-info :category "crafted")
(set-info :source |Alberto Griggio <[email protected]>. These benchmarks were used for the evaluation in the following paper: L. Haller, A. Griggio, M. Brain, D. Kroening: Deciding floating-point logic with systematic abstraction. FMCAD 2012. Real-numbered literals have been automatically translated by MathSAT|)
(set-info :status sat)
;; MathSAT API call trace ;; generated on 05/20/15 17:24:51
(declare-fun b149 () (_ SFXP 32 16))
(declare-fun b152 () (_ SFXP 32 16))
(declare-fun b50 () (_ SFXP 32 16))
(declare-fun b146 () (_ SFXP 32 16))
(declare-fun b98 () (_ SFXP 32 16))
(declare-fun b269 () (_ SFXP 32 16))
(declare-fun b86 () (_ SFXP 32 16))
(declare-fun b116 () (_ SFXP 32 16))
(declare-fun b26 () (_ SFXP 32 16))
(declare-fun b107 () (_ SFXP 32 16))
(declare-fun b101 () (_ SFXP 32 16))
(declare-fun b83 () (_ SFXP 32 16))
(declare-fun b113 () (_ SFXP 32 16))
(declare-fun b128 () (_ SFXP 32 16))
(declare-fun b44 () (_ SFXP 32 16))
(declare-fun b89 () (_ SFXP 32 16))
(declare-fun b104 () (_ SFXP 32 16))
(declare-fun b32 () (_ SFXP 32 16))
(declare-fun b77 () (_ SFXP 32 16))
(declare-fun b125 () (_ SFXP 32 16))
(declare-fun b68 () (_ SFXP 32 16))
(declare-fun b35 () (_ SFXP 32 16))
(declare-fun b161 () (_ SFXP 32 16))
(declare-fun b14 () (_ SFXP 32 16))
(declare-fun b131 () (_ SFXP 32 16))
(declare-fun b47 () (_ SFXP 32 16))
(declare-fun b29 () (_ SFXP 32 16))
(declare-fun b158 () (_ SFXP 32 16))
(declare-fun b62 () (_ SFXP 32 16))
(declare-fun b134 () (_ SFXP 32 16))
(declare-fun b38 () (_ SFXP 32 16))
(declare-fun b20 () (_ SFXP 32 16))
(declare-fun b11 () (_ SFXP 32 16))
(declare-fun b56 () (_ SFXP 32 16))
(declare-fun b80 () (_ SFXP 32 16))
(declare-fun b23 () (_ SFXP 32 16))
(declare-fun b53 () (_ SFXP 32 16))
(declare-fun b71 () (_ SFXP 32 16))
(declare-fun b17 () (_ SFXP 32 16))
(declare-fun b41 () (_ SFXP 32 16))
(declare-fun b10 () (_ SFXP 32 16))
(declare-fun b140 () (_ SFXP 32 16))
(declare-fun b92 () (_ SFXP 32 16))
(declare-fun b119 () (_ SFXP 32 16))
(declare-fun b110 () (_ SFXP 32 16))
(declare-fun b143 () (_ SFXP 32 16))
(declare-fun b65 () (_ SFXP 32 16))
(declare-fun b137 () (_ SFXP 32 16))
(declare-fun b122 () (_ SFXP 32 16))
(declare-fun b95 () (_ SFXP 32 16))
(declare-fun b59 () (_ SFXP 32 16))
(declare-fun b155 () (_ SFXP 32 16))
(declare-fun b74 () (_ SFXP 32 16))
(define-fun _t_3 () RoundingMode roundUp)
(define-fun _t_9 () (_ SFXP 32 16) b11)
(define-fun _t_10 () (_ SFXP 32 16) b269)
(define-fun _t_11 () Bool (sfxp.lt _t_9 _t_10))
(define-fun _t_12 () (_ SFXP 32 16) b10)
(define-fun _t_13 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_12 _t_9))
(define-fun _t_14 () (_ SFXP 32 16) b14)
(define-fun _t_15 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_13 _t_14))
(define-fun _t_16 () (_ SFXP 32 16) b17)
(define-fun _t_17 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_15 _t_16))
(define-fun _t_18 () (_ SFXP 32 16) b20)
(define-fun _t_19 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_17 _t_18))
(define-fun _t_20 () (_ SFXP 32 16) b23)
(define-fun _t_21 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_19 _t_20))
(define-fun _t_22 () (_ SFXP 32 16) b26)
(define-fun _t_23 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_21 _t_22))
(define-fun _t_24 () (_ SFXP 32 16) b29)
(define-fun _t_25 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_23 _t_24))
(define-fun _t_26 () (_ SFXP 32 16) b32)
(define-fun _t_27 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_25 _t_26))
(define-fun _t_28 () (_ SFXP 32 16) b35)
(define-fun _t_29 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_27 _t_28))
(define-fun _t_30 () (_ SFXP 32 16) b38)
(define-fun _t_31 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_29 _t_30))
(define-fun _t_32 () (_ SFXP 32 16) b41)
(define-fun _t_33 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_31 _t_32))
(define-fun _t_34 () (_ SFXP 32 16) b44)
(define-fun _t_35 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_33 _t_34))
(define-fun _t_36 () (_ SFXP 32 16) b47)
(define-fun _t_37 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_35 _t_36))
(define-fun _t_38 () (_ SFXP 32 16) b50)
(define-fun _t_39 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_37 _t_38))
(define-fun _t_40 () (_ SFXP 32 16) b53)
(define-fun _t_41 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_39 _t_40))
(define-fun _t_42 () (_ SFXP 32 16) b56)
(define-fun _t_43 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_41 _t_42))
(define-fun _t_44 () (_ SFXP 32 16) b59)
(define-fun _t_45 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_43 _t_44))
(define-fun _t_46 () (_ SFXP 32 16) b62)
(define-fun _t_47 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_45 _t_46))
(define-fun _t_48 () (_ SFXP 32 16) b65)
(define-fun _t_49 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_47 _t_48))
(define-fun _t_50 () (_ SFXP 32 16) b68)
(define-fun _t_51 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_49 _t_50))
(define-fun _t_52 () (_ SFXP 32 16) b71)
(define-fun _t_53 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_51 _t_52))
(define-fun _t_54 () (_ SFXP 32 16) b74)
(define-fun _t_55 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_53 _t_54))
(define-fun _t_56 () (_ SFXP 32 16) b77)
(define-fun _t_57 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_55 _t_56))
(define-fun _t_58 () (_ SFXP 32 16) b80)
(define-fun _t_59 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_57 _t_58))
(define-fun _t_60 () (_ SFXP 32 16) b83)
(define-fun _t_61 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_59 _t_60))
(define-fun _t_62 () (_ SFXP 32 16) b86)
(define-fun _t_63 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_61 _t_62))
(define-fun _t_64 () (_ SFXP 32 16) b89)
(define-fun _t_65 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_63 _t_64))
(define-fun _t_66 () (_ SFXP 32 16) b92)
(define-fun _t_67 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_65 _t_66))
(define-fun _t_68 () (_ SFXP 32 16) b95)
(define-fun _t_69 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_67 _t_68))
(define-fun _t_70 () (_ SFXP 32 16) b98)
(define-fun _t_71 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_69 _t_70))
(define-fun _t_72 () (_ SFXP 32 16) b101)
(define-fun _t_73 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_71 _t_72))
(define-fun _t_74 () (_ SFXP 32 16) b104)
(define-fun _t_75 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_73 _t_74))
(define-fun _t_76 () (_ SFXP 32 16) b107)
(define-fun _t_77 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_75 _t_76))
(define-fun _t_78 () (_ SFXP 32 16) b110)
(define-fun _t_79 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_77 _t_78))
(define-fun _t_80 () (_ SFXP 32 16) b113)
(define-fun _t_81 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_79 _t_80))
(define-fun _t_82 () (_ SFXP 32 16) b116)
(define-fun _t_83 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_81 _t_82))
(define-fun _t_84 () (_ SFXP 32 16) b119)
(define-fun _t_85 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_83 _t_84))
(define-fun _t_86 () (_ SFXP 32 16) b122)
(define-fun _t_87 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_85 _t_86))
(define-fun _t_88 () (_ SFXP 32 16) b125)
(define-fun _t_89 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_87 _t_88))
(define-fun _t_90 () (_ SFXP 32 16) b128)
(define-fun _t_91 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_89 _t_90))
(define-fun _t_92 () (_ SFXP 32 16) b131)
(define-fun _t_93 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_91 _t_92))
(define-fun _t_94 () (_ SFXP 32 16) b134)
(define-fun _t_95 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_93 _t_94))
(define-fun _t_96 () (_ SFXP 32 16) b137)
(define-fun _t_97 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_95 _t_96))
(define-fun _t_98 () (_ SFXP 32 16) b140)
(define-fun _t_99 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_97 _t_98))
(define-fun _t_100 () (_ SFXP 32 16) b143)
(define-fun _t_101 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_99 _t_100))
(define-fun _t_102 () (_ SFXP 32 16) b146)
(define-fun _t_103 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_101 _t_102))
(define-fun _t_104 () (_ SFXP 32 16) b149)
(define-fun _t_105 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_103 _t_104))
(define-fun _t_106 () (_ SFXP 32 16) b152)
(define-fun _t_107 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_105 _t_106))
(define-fun _t_108 () (_ SFXP 32 16) b155)
(define-fun _t_109 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_107 _t_108))
(define-fun _t_110 () (_ SFXP 32 16) b158)
(define-fun _t_111 () (_ SFXP 32 16) (sfxp.div wrapAround _t_3 _t_109 _t_110))
(define-fun _t_112 () (_ SFXP 32 16) b161)
(define-fun _t_113 () Bool (sfxp.lt _t_111 _t_112))
(define-fun _t_114 () Bool (and _t_11 _t_113))
(define-fun _t_115 () Bool (sfxp.leq _t_112 _t_9))
(define-fun _t_116 () Bool (and _t_114 _t_115))
(define-fun _t_117 () Bool (sfxp.lt _t_14 _t_10))
(define-fun _t_118 () Bool (and _t_116 _t_117))
(define-fun _t_119 () Bool (sfxp.leq _t_112 _t_14))
(define-fun _t_120 () Bool (and _t_118 _t_119))
(define-fun _t_121 () Bool (sfxp.lt _t_16 _t_10))
(define-fun _t_122 () Bool (and _t_120 _t_121))
(define-fun _t_123 () Bool (sfxp.leq _t_112 _t_16))
(define-fun _t_124 () Bool (and _t_122 _t_123))
(define-fun _t_125 () Bool (sfxp.lt _t_18 _t_10))
(define-fun _t_126 () Bool (and _t_124 _t_125))
(define-fun _t_127 () Bool (sfxp.leq _t_112 _t_18))
(define-fun _t_128 () Bool (and _t_126 _t_127))
(define-fun _t_129 () Bool (sfxp.lt _t_20 _t_10))
(define-fun _t_130 () Bool (and _t_128 _t_129))
(define-fun _t_131 () Bool (sfxp.leq _t_112 _t_20))
(define-fun _t_132 () Bool (and _t_130 _t_131))
(define-fun _t_133 () Bool (sfxp.lt _t_22 _t_10))
(define-fun _t_134 () Bool (and _t_132 _t_133))
(define-fun _t_135 () Bool (sfxp.leq _t_112 _t_22))
(define-fun _t_136 () Bool (and _t_134 _t_135))
(define-fun _t_137 () Bool (sfxp.lt _t_24 _t_10))
(define-fun _t_138 () Bool (and _t_136 _t_137))
(define-fun _t_139 () Bool (sfxp.leq _t_112 _t_24))
(define-fun _t_140 () Bool (and _t_138 _t_139))
(define-fun _t_141 () Bool (sfxp.lt _t_26 _t_10))
(define-fun _t_142 () Bool (and _t_140 _t_141))
(define-fun _t_143 () Bool (sfxp.leq _t_112 _t_26))
(define-fun _t_144 () Bool (and _t_142 _t_143))
(define-fun _t_145 () Bool (sfxp.lt _t_28 _t_10))
(define-fun _t_146 () Bool (and _t_144 _t_145))
(define-fun _t_147 () Bool (sfxp.leq _t_112 _t_28))
(define-fun _t_148 () Bool (and _t_146 _t_147))
(define-fun _t_149 () Bool (sfxp.lt _t_30 _t_10))
(define-fun _t_150 () Bool (and _t_148 _t_149))
(define-fun _t_151 () Bool (sfxp.leq _t_112 _t_30))
(define-fun _t_152 () Bool (and _t_150 _t_151))
(define-fun _t_153 () Bool (sfxp.lt _t_32 _t_10))
(define-fun _t_154 () Bool (and _t_152 _t_153))
(define-fun _t_155 () Bool (sfxp.leq _t_112 _t_32))
(define-fun _t_156 () Bool (and _t_154 _t_155))
(define-fun _t_157 () Bool (sfxp.lt _t_34 _t_10))
(define-fun _t_158 () Bool (and _t_156 _t_157))
(define-fun _t_159 () Bool (sfxp.leq _t_112 _t_34))
(define-fun _t_160 () Bool (and _t_158 _t_159))
(define-fun _t_161 () Bool (sfxp.lt _t_36 _t_10))
(define-fun _t_162 () Bool (and _t_160 _t_161))
(define-fun _t_163 () Bool (sfxp.leq _t_112 _t_36))
(define-fun _t_164 () Bool (and _t_162 _t_163))
(define-fun _t_165 () Bool (sfxp.lt _t_38 _t_10))
(define-fun _t_166 () Bool (and _t_164 _t_165))
(define-fun _t_167 () Bool (sfxp.leq _t_112 _t_38))
(define-fun _t_168 () Bool (and _t_166 _t_167))
(define-fun _t_169 () Bool (sfxp.lt _t_40 _t_10))
(define-fun _t_170 () Bool (and _t_168 _t_169))
(define-fun _t_171 () Bool (sfxp.leq _t_112 _t_40))
(define-fun _t_172 () Bool (and _t_170 _t_171))
(define-fun _t_173 () Bool (sfxp.lt _t_42 _t_10))
(define-fun _t_174 () Bool (and _t_172 _t_173))
(define-fun _t_175 () Bool (sfxp.leq _t_112 _t_42))
(define-fun _t_176 () Bool (and _t_174 _t_175))
(define-fun _t_177 () Bool (sfxp.lt _t_44 _t_10))
(define-fun _t_178 () Bool (and _t_176 _t_177))
(define-fun _t_179 () Bool (sfxp.leq _t_112 _t_44))
(define-fun _t_180 () Bool (and _t_178 _t_179))
(define-fun _t_181 () Bool (sfxp.lt _t_46 _t_10))
(define-fun _t_182 () Bool (and _t_180 _t_181))
(define-fun _t_183 () Bool (sfxp.leq _t_112 _t_46))
(define-fun _t_184 () Bool (and _t_182 _t_183))
(define-fun _t_185 () Bool (sfxp.lt _t_48 _t_10))
(define-fun _t_186 () Bool (and _t_184 _t_185))
(define-fun _t_187 () Bool (sfxp.leq _t_112 _t_48))
(define-fun _t_188 () Bool (and _t_186 _t_187))
(define-fun _t_189 () Bool (sfxp.lt _t_50 _t_10))
(define-fun _t_190 () Bool (and _t_188 _t_189))
(define-fun _t_191 () Bool (sfxp.leq _t_112 _t_50))
(define-fun _t_192 () Bool (and _t_190 _t_191))
(define-fun _t_193 () Bool (sfxp.lt _t_52 _t_10))
(define-fun _t_194 () Bool (and _t_192 _t_193))
(define-fun _t_195 () Bool (sfxp.leq _t_112 _t_52))
(define-fun _t_196 () Bool (and _t_194 _t_195))
(define-fun _t_197 () Bool (sfxp.lt _t_54 _t_10))
(define-fun _t_198 () Bool (and _t_196 _t_197))
(define-fun _t_199 () Bool (sfxp.leq _t_112 _t_54))
(define-fun _t_200 () Bool (and _t_198 _t_199))
(define-fun _t_201 () Bool (sfxp.lt _t_56 _t_10))
(define-fun _t_202 () Bool (and _t_200 _t_201))
(define-fun _t_203 () Bool (sfxp.leq _t_112 _t_56))
(define-fun _t_204 () Bool (and _t_202 _t_203))
(define-fun _t_205 () Bool (sfxp.lt _t_58 _t_10))
(define-fun _t_206 () Bool (and _t_204 _t_205))
(define-fun _t_207 () Bool (sfxp.leq _t_112 _t_58))
(define-fun _t_208 () Bool (and _t_206 _t_207))
(define-fun _t_209 () Bool (sfxp.lt _t_60 _t_10))
(define-fun _t_210 () Bool (and _t_208 _t_209))
(define-fun _t_211 () Bool (sfxp.leq _t_112 _t_60))
(define-fun _t_212 () Bool (and _t_210 _t_211))
(define-fun _t_213 () Bool (sfxp.lt _t_62 _t_10))
(define-fun _t_214 () Bool (and _t_212 _t_213))
(define-fun _t_215 () Bool (sfxp.leq _t_112 _t_62))
(define-fun _t_216 () Bool (and _t_214 _t_215))
(define-fun _t_217 () Bool (sfxp.lt _t_64 _t_10))
(define-fun _t_218 () Bool (and _t_216 _t_217))
(define-fun _t_219 () Bool (sfxp.leq _t_112 _t_64))
(define-fun _t_220 () Bool (and _t_218 _t_219))
(define-fun _t_221 () Bool (sfxp.lt _t_66 _t_10))
(define-fun _t_222 () Bool (and _t_220 _t_221))
(define-fun _t_223 () Bool (sfxp.leq _t_112 _t_66))
(define-fun _t_224 () Bool (and _t_222 _t_223))
(define-fun _t_225 () Bool (sfxp.lt _t_68 _t_10))
(define-fun _t_226 () Bool (and _t_224 _t_225))
(define-fun _t_227 () Bool (sfxp.leq _t_112 _t_68))
(define-fun _t_228 () Bool (and _t_226 _t_227))
(define-fun _t_229 () Bool (sfxp.lt _t_70 _t_10))
(define-fun _t_230 () Bool (and _t_228 _t_229))
(define-fun _t_231 () Bool (sfxp.leq _t_112 _t_70))
(define-fun _t_232 () Bool (and _t_230 _t_231))
(define-fun _t_233 () Bool (sfxp.lt _t_72 _t_10))
(define-fun _t_234 () Bool (and _t_232 _t_233))
(define-fun _t_235 () Bool (sfxp.leq _t_112 _t_72))
(define-fun _t_236 () Bool (and _t_234 _t_235))
(define-fun _t_237 () Bool (sfxp.lt _t_74 _t_10))
(define-fun _t_238 () Bool (and _t_236 _t_237))
(define-fun _t_239 () Bool (sfxp.leq _t_112 _t_74))
(define-fun _t_240 () Bool (and _t_238 _t_239))
(define-fun _t_241 () Bool (sfxp.lt _t_76 _t_10))
(define-fun _t_242 () Bool (and _t_240 _t_241))
(define-fun _t_243 () Bool (sfxp.leq _t_112 _t_76))
(define-fun _t_244 () Bool (and _t_242 _t_243))
(define-fun _t_245 () Bool (sfxp.lt _t_78 _t_10))
(define-fun _t_246 () Bool (and _t_244 _t_245))
(define-fun _t_247 () Bool (sfxp.leq _t_112 _t_78))
(define-fun _t_248 () Bool (and _t_246 _t_247))
(define-fun _t_249 () Bool (sfxp.lt _t_80 _t_10))
(define-fun _t_250 () Bool (and _t_248 _t_249))
(define-fun _t_251 () Bool (sfxp.leq _t_112 _t_80))
(define-fun _t_252 () Bool (and _t_250 _t_251))
(define-fun _t_253 () Bool (sfxp.lt _t_82 _t_10))
(define-fun _t_254 () Bool (and _t_252 _t_253))
(define-fun _t_255 () Bool (sfxp.leq _t_112 _t_82))
(define-fun _t_256 () Bool (and _t_254 _t_255))
(define-fun _t_257 () Bool (sfxp.lt _t_84 _t_10))
(define-fun _t_258 () Bool (and _t_256 _t_257))
(define-fun _t_259 () Bool (sfxp.leq _t_112 _t_84))
(define-fun _t_260 () Bool (and _t_258 _t_259))
(define-fun _t_261 () Bool (sfxp.lt _t_86 _t_10))
(define-fun _t_262 () Bool (and _t_260 _t_261))
(define-fun _t_263 () Bool (sfxp.leq _t_112 _t_86))
(define-fun _t_264 () Bool (and _t_262 _t_263))
(define-fun _t_265 () Bool (sfxp.lt _t_88 _t_10))
(define-fun _t_266 () Bool (and _t_264 _t_265))
(define-fun _t_267 () Bool (sfxp.leq _t_112 _t_88))
(define-fun _t_268 () Bool (and _t_266 _t_267))
(define-fun _t_269 () Bool (sfxp.lt _t_90 _t_10))
(define-fun _t_270 () Bool (and _t_268 _t_269))
(define-fun _t_271 () Bool (sfxp.leq _t_112 _t_90))
(define-fun _t_272 () Bool (and _t_270 _t_271))
(define-fun _t_273 () Bool (sfxp.lt _t_92 _t_10))
(define-fun _t_274 () Bool (and _t_272 _t_273))
(define-fun _t_275 () Bool (sfxp.leq _t_112 _t_92))
(define-fun _t_276 () Bool (and _t_274 _t_275))
(define-fun _t_277 () Bool (sfxp.lt _t_94 _t_10))
(define-fun _t_278 () Bool (and _t_276 _t_277))
(define-fun _t_279 () Bool (sfxp.leq _t_112 _t_94))
(define-fun _t_280 () Bool (and _t_278 _t_279))
(define-fun _t_281 () Bool (sfxp.lt _t_96 _t_10))
(define-fun _t_282 () Bool (and _t_280 _t_281))
(define-fun _t_283 () Bool (sfxp.leq _t_112 _t_96))
(define-fun _t_284 () Bool (and _t_282 _t_283))
(define-fun _t_285 () Bool (sfxp.lt _t_98 _t_10))
(define-fun _t_286 () Bool (and _t_284 _t_285))
(define-fun _t_287 () Bool (sfxp.leq _t_112 _t_98))
(define-fun _t_288 () Bool (and _t_286 _t_287))
(define-fun _t_289 () Bool (sfxp.lt _t_100 _t_10))
(define-fun _t_290 () Bool (and _t_288 _t_289))
(define-fun _t_291 () Bool (sfxp.leq _t_112 _t_100))
(define-fun _t_292 () Bool (and _t_290 _t_291))
(define-fun _t_293 () Bool (sfxp.lt _t_102 _t_10))
(define-fun _t_294 () Bool (and _t_292 _t_293))
(define-fun _t_295 () Bool (sfxp.leq _t_112 _t_102))
(define-fun _t_296 () Bool (and _t_294 _t_295))
(define-fun _t_297 () Bool (sfxp.lt _t_104 _t_10))
(define-fun _t_298 () Bool (and _t_296 _t_297))
(define-fun _t_299 () Bool (sfxp.leq _t_112 _t_104))
(define-fun _t_300 () Bool (and _t_298 _t_299))
(define-fun _t_301 () Bool (sfxp.lt _t_106 _t_10))
(define-fun _t_302 () Bool (and _t_300 _t_301))
(define-fun _t_303 () Bool (sfxp.leq _t_112 _t_106))
(define-fun _t_304 () Bool (and _t_302 _t_303))
(define-fun _t_305 () Bool (sfxp.lt _t_108 _t_10))
(define-fun _t_306 () Bool (and _t_304 _t_305))
(define-fun _t_307 () Bool (sfxp.leq _t_112 _t_108))
(define-fun _t_308 () Bool (and _t_306 _t_307))
(define-fun _t_309 () Bool (sfxp.lt _t_110 _t_10))
(define-fun _t_310 () Bool (and _t_308 _t_309))
(define-fun _t_311 () Bool (sfxp.leq _t_112 _t_110))
(define-fun _t_312 () Bool (and _t_310 _t_311))
(assert _t_312)
(check-sat)
(exit)