blob: 35ebb28e9b40bd967cd73eb608a8cde05a30f5fc (
plain)
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
|
(set-logic AUFLIA)
(set-info :status unsat)
(declare-sort U 0)
(declare-fun A (U U U
U U U U
U U U U
U U U U
U U U U
U U U U
U U U U
U U U U
U U U U
U U U U
U U U U
U U U U
U U U U
U U U U
U U
U) (Array Int U))
(assert
(forall ((v_184 U) (v_185 U)
(v_186 U) (v_187 U)
(v_188 U) (v_189 U)
(v_190 U) (v_191 U)
(v_192 U) (v_193 U)
(v_194 U) (v_195 U)
(v_196 U) (v_197 U)
(v_198 U) (v_199 U)
(v_200 U) (v_201 U)
(v_202 U) (v_203 U)
(v_204 U) (v_205 U)
(v_206 U) (v_207 U)
(v_208 U) (v_209 U)
(v_210 U) (v_211 U)
(v_212 U) (v_213 U)
(v_214 U) (v_215 U)
(v_216 U) (v_217 U)
(v_218 U) (v_219 U)
(v_220 U) (v_221 U)
(v_222 U) (v_223 U)
(v_224 U) (v_225 U)
(v_226 U) (v_227 U)
(v_228 U) (v_229 U)
(v_230 U) (v_231 U)
(v_232 U) (v_233 U)
(v_234 U) (v_235 U)
(v_236 U) (v_237 U)
(v_238 U) (v_239 U)
(v_240 U) (v_241 U) (v_242 Int))
(let ((v_183 (A v_184 v_185 v_186 v_187
v_188 v_189 v_190 v_191 v_192
v_193 v_194 v_195 v_196 v_197
v_198 v_199 v_200 v_201 v_202
v_203 v_204 v_205 v_206 v_207
v_208 v_209 v_210 v_211 v_212
v_213 v_214 v_215 v_216 v_217
v_218 v_219 v_220 v_221 v_222
v_223 v_224 v_225 v_226 v_227
v_228 v_229 v_230 v_231 v_232
v_233 v_234 v_235 v_236 v_237
v_238 v_239 v_240 v_241)))
(ite (= v_242 59) (= (select v_183 v_242) v_240)
(ite (= v_242 58) (= (select v_183 v_242) v_239)
(ite (= v_242 57) (= (select v_183 v_242) v_238)
(ite (= v_242 56) (= (select v_183 v_242) v_237)
(ite (= v_242 55) (= (select v_183 v_242) v_236)
(ite (= v_242 54) (= (select v_183 v_242) v_235)
(ite (= v_242 53) (= (select v_183 v_242) v_234)
(ite (= v_242 52) (= (select v_183 v_242) v_233)
(ite (= v_242 51) (= (select v_183 v_242) v_232)
(ite (= v_242 50) (= (select v_183 v_242) v_231)
(ite (= v_242 49) (= (select v_183 v_242) v_230)
(ite (= v_242 48) (= (select v_183 v_242) v_229)
(ite (= v_242 47) (= (select v_183 v_242) v_228)
(ite (= v_242 46) (= (select v_183 v_242) v_227)
(ite (= v_242 45) (= (select v_183 v_242) v_226)
(ite (= v_242 44) (= (select v_183 v_242) v_225)
(ite (= v_242 43) (= (select v_183 v_242) v_224)
(ite (= v_242 41) (= (select v_183 v_242) v_223)
(ite (= v_242 40) (= (select v_183 v_242) v_222)
(ite (= v_242 39) (= (select v_183 v_242) v_221)
(ite (= v_242 37) (= (select v_183 v_242) v_220)
(ite (= v_242 36) (= (select v_183 v_242) v_219)
(ite (= v_242 34) (= (select v_183 v_242) v_218)
(ite (= v_242 33) (= (select v_183 v_242) v_217)
(ite (= v_242 32) (= (select v_183 v_242) v_216)
(ite (= v_242 31) (= (select v_183 v_242) v_215)
(ite (= v_242 30) (= (select v_183 v_242) v_214)
(ite (= v_242 29) (= (select v_183 v_242) v_213)
(ite (= v_242 28) (= (select v_183 v_242) v_212)
(ite (= v_242 27) (= (select v_183 v_242) v_211)
(ite (= v_242 26) (= (select v_183 v_242) v_210)
(ite (= v_242 25) (= (select v_183 v_242) v_209)
(ite (= v_242 24) (= (select v_183 v_242) v_208)
(ite (= v_242 23) (= (select v_183 v_242) v_207)
(ite (= v_242 22) (= (select v_183 v_242) v_206)
(ite (= v_242 21) (= (select v_183 v_242) v_205)
(ite (= v_242 20) (= (select v_183 v_242) v_204)
(ite (= v_242 19) (= (select v_183 v_242) v_203)
(ite (= v_242 18) (= (select v_183 v_242) v_202)
(ite (= v_242 17) (= (select v_183 v_242) v_201)
(ite (= v_242 16) (= (select v_183 v_242) v_200)
(ite (= v_242 15) (= (select v_183 v_242) v_199)
(ite (= v_242 14) (= (select v_183 v_242) v_198)
(ite (= v_242 13) (= (select v_183 v_242) v_197)
(ite (= v_242 12) (= (select v_183 v_242) v_196)
(ite (= v_242 11) (= (select v_183 v_242) v_195)
(ite (= v_242 10) (= (select v_183 v_242) v_194)
(ite (= v_242 9) (= (select v_183 v_242) v_193)
(ite (= v_242 8) (= (select v_183 v_242) v_192)
(ite (= v_242 7) (= (select v_183 v_242) v_191)
(ite (= v_242 6) (= (select v_183 v_242) v_190)
(ite (= v_242 5) (= (select v_183 v_242) v_189)
(ite (= v_242 4) (= (select v_183 v_242) v_188)
(ite (= v_242 3) (= (select v_183 v_242) v_187)
(ite (= v_242 2) (= (select v_183 v_242) v_186)
(ite (= v_242 1) (= (select v_183 v_242) v_185)
(ite (= v_242 0) (= (select v_183 v_242) v_184)
(= (select v_183 v_242) v_241)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(declare-const c_184 U) (declare-const c_185 U)
(declare-const c_186 U) (declare-const c_187 U)
(declare-const c_188 U) (declare-const c_189 U)
(declare-const c_190 U) (declare-const c_191 U)
(declare-const c_192 U) (declare-const c_193 U)
(declare-const c_194 U) (declare-const c_195 U)
(declare-const c_196 U) (declare-const c_197 U)
(declare-const c_198 U) (declare-const c_199 U)
(declare-const c_200 U) (declare-const c_201 U)
(declare-const c_202 U) (declare-const c_203 U)
(declare-const c_204 U) (declare-const c_205 U)
(declare-const c_206 U) (declare-const c_207 U)
(declare-const c_208 U) (declare-const c_209 U)
(declare-const c_210 U) (declare-const c_211 U)
(declare-const c_212 U) (declare-const c_213 U)
(declare-const c_214 U) (declare-const c_215 U)
(declare-const c_216 U) (declare-const c_217 U)
(declare-const c_218 U) (declare-const c_219 U)
(declare-const c_220 U) (declare-const c_221 U)
(declare-const c_222 U) (declare-const c_223 U)
(declare-const c_224 U) (declare-const c_225 U)
(declare-const c_226 U) (declare-const c_227 U)
(declare-const c_228 U) (declare-const c_229 U)
(declare-const c_230 U) (declare-const c_231 U)
(declare-const c_232 U) (declare-const c_233 U)
(declare-const c_234 U) (declare-const c_235 U)
(declare-const c_236 U) (declare-const c_237 U)
(declare-const c_238 U) (declare-const c_239 U)
(declare-const c_240 U) (declare-const c_241 U)
(declare-fun b () Int)
(declare-fun c () U)
(assert (not (= (select (A c_184 c_185 c_186 c_187
c_188 c_189 c_190 c_191 c_192
c_193 c_194 c_195 c_196 c_197
c_198 c_199 c_200 c_201 c_202
c_203 c_204 c_205 c_206 c_207
c_208 c_209 c_210 c_211 c_212
c_213 c_214 c_215 c_216 c_217
c_218 c_219 c_220 c_221 c_222
c_223 c_224 c_225 c_226 c_227
c_228 c_229 c_230 c_231 c_232
c_233 c_234 c_235 c_236 c_237
c_238 c_239 c_240 c_241) b) c)))
(assert (and (= b 28) (= c c_212)))
(check-sat)
|
