-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathairplane-single-nl-sat_3.smt2
324 lines (324 loc) · 19.9 KB
/
airplane-single-nl-sat_3.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
(set-logic QF_NRA_ODE)
(declare-fun tau () Real)
(declare-fun r () Real)
(declare-fun psi () Real)
(declare-fun phi () Real)
(declare-fun p () Real)
(declare-fun gRDR () Real)
(declare-fun gAIL () Real)
(declare-fun gDir () Real)
(declare-fun beta () Real)
(declare-fun xAIL () Real)
(declare-fun xRDR () Real)
(define-ode flow_1 ((= d/dt[beta] (+ (- (/ (* (* 13.97 300) (+ (+ (* (/ (* -0.02 180) 3.14159) beta) (/ (* 0.021 xAIL) 20)) (/ (* 0.086 xRDR) 30))) (* 20500 111.64)) r) (* (* (/ 111.64 9.80555) (cos beta)) (sin phi)))) (= d/dt[p] (+ (* (* (+ (* -0.77 r) (* 0.02755 p)) r) (/ (sin phi) (cos phi))) (* (* (* 13.97 30) 300) (+ (* 0.0001055 (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))) (* 1.642e-06 (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30))))))) (= d/dt[r] (+ (* (* (- (* -0.7336 p) (* 0.02755 r)) r) (/ (sin phi) (cos phi))) (* (* (* 13.97 30) 300) (+ (* 1.642e-06 (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))) (* 1.587e-05 (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30))))))) (= d/dt[phi] p) (= d/dt[psi] (* (/ 9.80555 111.64) (/ (sin phi) (cos phi)))) (= d/dt[xAIL] 0.25) (= d/dt[xRDR] 0.5) (= d/dt[gAIL] 0) (= d/dt[gRDR] 0) (= d/dt[gDir] 0) (= d/dt[tau] 1)))
(define-ode flow_2 ((= d/dt[beta] (+ (- (/ (* (* 13.97 300) (+ (+ (* (/ (* -0.02 180) 3.14159) beta) (/ (* 0.021 xAIL) 20)) (/ (* 0.086 xRDR) 30))) (* 20500 111.64)) r) (* (* (/ 111.64 9.80555) (cos beta)) (sin phi)))) (= d/dt[p] (+ (* (* (+ (* -0.77 r) (* 0.02755 p)) r) (/ (sin phi) (cos phi))) (* (* (* 13.97 30) 300) (+ (* 0.0001055 (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))) (* 1.642e-06 (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30))))))) (= d/dt[r] (+ (* (* (- (* -0.7336 p) (* 0.02755 r)) r) (/ (sin phi) (cos phi))) (* (* (* 13.97 30) 300) (+ (* 1.642e-06 (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))) (* 1.587e-05 (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30))))))) (= d/dt[phi] p) (= d/dt[psi] (* (/ 9.80555 111.64) (/ (sin phi) (cos phi)))) (= d/dt[xAIL] 0.25) (= d/dt[xRDR] -0.5) (= d/dt[gAIL] 0) (= d/dt[gRDR] 0) (= d/dt[gDir] 0) (= d/dt[tau] 1)))
(define-ode flow_3 ((= d/dt[beta] (+ (- (/ (* (* 13.97 300) (+ (+ (* (/ (* -0.02 180) 3.14159) beta) (/ (* 0.021 xAIL) 20)) (/ (* 0.086 xRDR) 30))) (* 20500 111.64)) r) (* (* (/ 111.64 9.80555) (cos beta)) (sin phi)))) (= d/dt[p] (+ (* (* (+ (* -0.77 r) (* 0.02755 p)) r) (/ (sin phi) (cos phi))) (* (* (* 13.97 30) 300) (+ (* 0.0001055 (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))) (* 1.642e-06 (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30))))))) (= d/dt[r] (+ (* (* (- (* -0.7336 p) (* 0.02755 r)) r) (/ (sin phi) (cos phi))) (* (* (* 13.97 30) 300) (+ (* 1.642e-06 (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))) (* 1.587e-05 (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30))))))) (= d/dt[phi] p) (= d/dt[psi] (* (/ 9.80555 111.64) (/ (sin phi) (cos phi)))) (= d/dt[xAIL] -0.25) (= d/dt[xRDR] 0.5) (= d/dt[gAIL] 0) (= d/dt[gRDR] 0) (= d/dt[gDir] 0) (= d/dt[tau] 1)))
(define-ode flow_4 ((= d/dt[beta] (+ (- (/ (* (* 13.97 300) (+ (+ (* (/ (* -0.02 180) 3.14159) beta) (/ (* 0.021 xAIL) 20)) (/ (* 0.086 xRDR) 30))) (* 20500 111.64)) r) (* (* (/ 111.64 9.80555) (cos beta)) (sin phi)))) (= d/dt[p] (+ (* (* (+ (* -0.77 r) (* 0.02755 p)) r) (/ (sin phi) (cos phi))) (* (* (* 13.97 30) 300) (+ (* 0.0001055 (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))) (* 1.642e-06 (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30))))))) (= d/dt[r] (+ (* (* (- (* -0.7336 p) (* 0.02755 r)) r) (/ (sin phi) (cos phi))) (* (* (* 13.97 30) 300) (+ (* 1.642e-06 (+ (+ (* (/ (* -0.0008 180) 3.14159) beta) (/ (* 0.05 xAIL) 20)) (/ (* 0.013 xRDR) 30))) (* 1.587e-05 (+ (+ (* (/ (* 0.02 180) 3.14159) beta) (/ (* -0.01 xAIL) 20)) (/ (* -0.04 xRDR) 30))))))) (= d/dt[phi] p) (= d/dt[psi] (* (/ 9.80555 111.64) (/ (sin phi) (cos phi)))) (= d/dt[xAIL] -0.25) (= d/dt[xRDR] -0.5) (= d/dt[gAIL] 0) (= d/dt[gRDR] 0) (= d/dt[gDir] 0) (= d/dt[tau] 1)))
(declare-fun time_0 () Real)
(declare-fun tau_0_0 () Real)
(declare-fun tau_0_t () Real)
(declare-fun r_0_0 () Real)
(declare-fun r_0_t () Real)
(declare-fun psi_0_0 () Real)
(declare-fun psi_0_t () Real)
(declare-fun phi_0_0 () Real)
(declare-fun phi_0_t () Real)
(declare-fun p_0_0 () Real)
(declare-fun p_0_t () Real)
(declare-fun gRDR_0_0 () Real)
(declare-fun gRDR_0_t () Real)
(declare-fun gAIL_0_0 () Real)
(declare-fun gAIL_0_t () Real)
(declare-fun gDir_0_0 () Real)
(declare-fun gDir_0_t () Real)
(declare-fun beta_0_0 () Real)
(declare-fun beta_0_t () Real)
(declare-fun modeA_0 () Bool)
(declare-fun xAIL_0_0 () Real)
(declare-fun xAIL_0_t () Real)
(declare-fun modeR_0 () Bool)
(declare-fun xRDR_0_0 () Real)
(declare-fun xRDR_0_t () Real)
(declare-fun time_1 () Real)
(declare-fun tau_1_0 () Real)
(declare-fun tau_1_t () Real)
(declare-fun r_1_0 () Real)
(declare-fun r_1_t () Real)
(declare-fun psi_1_0 () Real)
(declare-fun psi_1_t () Real)
(declare-fun phi_1_0 () Real)
(declare-fun phi_1_t () Real)
(declare-fun p_1_0 () Real)
(declare-fun p_1_t () Real)
(declare-fun gRDR_1_0 () Real)
(declare-fun gRDR_1_t () Real)
(declare-fun gAIL_1_0 () Real)
(declare-fun gAIL_1_t () Real)
(declare-fun gDir_1_0 () Real)
(declare-fun gDir_1_t () Real)
(declare-fun beta_1_0 () Real)
(declare-fun beta_1_t () Real)
(declare-fun modeA_1 () Bool)
(declare-fun xAIL_1_0 () Real)
(declare-fun xAIL_1_t () Real)
(declare-fun modeR_1 () Bool)
(declare-fun xRDR_1_0 () Real)
(declare-fun xRDR_1_t () Real)
(declare-fun time_2 () Real)
(declare-fun tau_2_0 () Real)
(declare-fun tau_2_t () Real)
(declare-fun r_2_0 () Real)
(declare-fun r_2_t () Real)
(declare-fun psi_2_0 () Real)
(declare-fun psi_2_t () Real)
(declare-fun phi_2_0 () Real)
(declare-fun phi_2_t () Real)
(declare-fun p_2_0 () Real)
(declare-fun p_2_t () Real)
(declare-fun gRDR_2_0 () Real)
(declare-fun gRDR_2_t () Real)
(declare-fun gAIL_2_0 () Real)
(declare-fun gAIL_2_t () Real)
(declare-fun gDir_2_0 () Real)
(declare-fun gDir_2_t () Real)
(declare-fun beta_2_0 () Real)
(declare-fun beta_2_t () Real)
(declare-fun modeA_2 () Bool)
(declare-fun xAIL_2_0 () Real)
(declare-fun xAIL_2_t () Real)
(declare-fun modeR_2 () Bool)
(declare-fun xRDR_2_0 () Real)
(declare-fun xRDR_2_t () Real)
(declare-fun time_3 () Real)
(declare-fun tau_3_0 () Real)
(declare-fun tau_3_t () Real)
(declare-fun r_3_0 () Real)
(declare-fun r_3_t () Real)
(declare-fun psi_3_0 () Real)
(declare-fun psi_3_t () Real)
(declare-fun phi_3_0 () Real)
(declare-fun phi_3_t () Real)
(declare-fun p_3_0 () Real)
(declare-fun p_3_t () Real)
(declare-fun gRDR_3_0 () Real)
(declare-fun gRDR_3_t () Real)
(declare-fun gAIL_3_0 () Real)
(declare-fun gAIL_3_t () Real)
(declare-fun gDir_3_0 () Real)
(declare-fun gDir_3_t () Real)
(declare-fun beta_3_0 () Real)
(declare-fun beta_3_t () Real)
(declare-fun modeA_3 () Bool)
(declare-fun xAIL_3_0 () Real)
(declare-fun xAIL_3_t () Real)
(declare-fun modeR_3 () Bool)
(declare-fun xRDR_3_0 () Real)
(declare-fun xRDR_3_t () Real)
(assert (<= 0 time_0)) (assert (<= time_0 1))
(assert (<= 0 tau_0_0)) (assert (<= tau_0_0 0.5))
(assert (<= 0 tau_0_t)) (assert (<= tau_0_t 0.5))
(assert (<= -1.5 r_0_0)) (assert (<= r_0_0 1.5))
(assert (<= -1.5 r_0_t)) (assert (<= r_0_t 1.5))
(assert (<= -1.5 psi_0_0)) (assert (<= psi_0_0 1.5))
(assert (<= -1.5 psi_0_t)) (assert (<= psi_0_t 1.5))
(assert (<= -1.5 phi_0_0)) (assert (<= phi_0_0 1.5))
(assert (<= -1.5 phi_0_t)) (assert (<= phi_0_t 1.5))
(assert (<= -1.5 p_0_0)) (assert (<= p_0_0 1.5))
(assert (<= -1.5 p_0_t)) (assert (<= p_0_t 1.5))
(assert (<= -3.14159 gRDR_0_0)) (assert (<= gRDR_0_0 3.14159))
(assert (<= -3.14159 gRDR_0_t)) (assert (<= gRDR_0_t 3.14159))
(assert (<= -3.14159 gAIL_0_0)) (assert (<= gAIL_0_0 3.14159))
(assert (<= -3.14159 gAIL_0_t)) (assert (<= gAIL_0_t 3.14159))
(assert (<= -3.14159 gDir_0_0)) (assert (<= gDir_0_0 3.14159))
(assert (<= -3.14159 gDir_0_t)) (assert (<= gDir_0_t 3.14159))
(assert (<= -3.14159 beta_0_0)) (assert (<= beta_0_0 3.14159))
(assert (<= -3.14159 beta_0_t)) (assert (<= beta_0_t 3.14159))
(assert (<= -3.14159 xAIL_0_0)) (assert (<= xAIL_0_0 3.14159))
(assert (<= -3.14159 xAIL_0_t)) (assert (<= xAIL_0_t 3.14159))
(assert (<= -3.14159 xRDR_0_0)) (assert (<= xRDR_0_0 3.14159))
(assert (<= -3.14159 xRDR_0_t)) (assert (<= xRDR_0_t 3.14159))
(assert (<= 0 time_1)) (assert (<= time_1 1))
(assert (<= 0 tau_1_0)) (assert (<= tau_1_0 0.5))
(assert (<= 0 tau_1_t)) (assert (<= tau_1_t 0.5))
(assert (<= -1.5 r_1_0)) (assert (<= r_1_0 1.5))
(assert (<= -1.5 r_1_t)) (assert (<= r_1_t 1.5))
(assert (<= -1.5 psi_1_0)) (assert (<= psi_1_0 1.5))
(assert (<= -1.5 psi_1_t)) (assert (<= psi_1_t 1.5))
(assert (<= -1.5 phi_1_0)) (assert (<= phi_1_0 1.5))
(assert (<= -1.5 phi_1_t)) (assert (<= phi_1_t 1.5))
(assert (<= -1.5 p_1_0)) (assert (<= p_1_0 1.5))
(assert (<= -1.5 p_1_t)) (assert (<= p_1_t 1.5))
(assert (<= -3.14159 gRDR_1_0)) (assert (<= gRDR_1_0 3.14159))
(assert (<= -3.14159 gRDR_1_t)) (assert (<= gRDR_1_t 3.14159))
(assert (<= -3.14159 gAIL_1_0)) (assert (<= gAIL_1_0 3.14159))
(assert (<= -3.14159 gAIL_1_t)) (assert (<= gAIL_1_t 3.14159))
(assert (<= -3.14159 gDir_1_0)) (assert (<= gDir_1_0 3.14159))
(assert (<= -3.14159 gDir_1_t)) (assert (<= gDir_1_t 3.14159))
(assert (<= -3.14159 beta_1_0)) (assert (<= beta_1_0 3.14159))
(assert (<= -3.14159 beta_1_t)) (assert (<= beta_1_t 3.14159))
(assert (<= -3.14159 xAIL_1_0)) (assert (<= xAIL_1_0 3.14159))
(assert (<= -3.14159 xAIL_1_t)) (assert (<= xAIL_1_t 3.14159))
(assert (<= -3.14159 xRDR_1_0)) (assert (<= xRDR_1_0 3.14159))
(assert (<= -3.14159 xRDR_1_t)) (assert (<= xRDR_1_t 3.14159))
(assert (<= 0 time_2)) (assert (<= time_2 1))
(assert (<= 0 tau_2_0)) (assert (<= tau_2_0 0.5))
(assert (<= 0 tau_2_t)) (assert (<= tau_2_t 0.5))
(assert (<= -1.5 r_2_0)) (assert (<= r_2_0 1.5))
(assert (<= -1.5 r_2_t)) (assert (<= r_2_t 1.5))
(assert (<= -1.5 psi_2_0)) (assert (<= psi_2_0 1.5))
(assert (<= -1.5 psi_2_t)) (assert (<= psi_2_t 1.5))
(assert (<= -1.5 phi_2_0)) (assert (<= phi_2_0 1.5))
(assert (<= -1.5 phi_2_t)) (assert (<= phi_2_t 1.5))
(assert (<= -1.5 p_2_0)) (assert (<= p_2_0 1.5))
(assert (<= -1.5 p_2_t)) (assert (<= p_2_t 1.5))
(assert (<= -3.14159 gRDR_2_0)) (assert (<= gRDR_2_0 3.14159))
(assert (<= -3.14159 gRDR_2_t)) (assert (<= gRDR_2_t 3.14159))
(assert (<= -3.14159 gAIL_2_0)) (assert (<= gAIL_2_0 3.14159))
(assert (<= -3.14159 gAIL_2_t)) (assert (<= gAIL_2_t 3.14159))
(assert (<= -3.14159 gDir_2_0)) (assert (<= gDir_2_0 3.14159))
(assert (<= -3.14159 gDir_2_t)) (assert (<= gDir_2_t 3.14159))
(assert (<= -3.14159 beta_2_0)) (assert (<= beta_2_0 3.14159))
(assert (<= -3.14159 beta_2_t)) (assert (<= beta_2_t 3.14159))
(assert (<= -3.14159 xAIL_2_0)) (assert (<= xAIL_2_0 3.14159))
(assert (<= -3.14159 xAIL_2_t)) (assert (<= xAIL_2_t 3.14159))
(assert (<= -3.14159 xRDR_2_0)) (assert (<= xRDR_2_0 3.14159))
(assert (<= -3.14159 xRDR_2_t)) (assert (<= xRDR_2_t 3.14159))
(assert (<= 0 time_3)) (assert (<= time_3 1))
(assert (<= 0 tau_3_0)) (assert (<= tau_3_0 0.5))
(assert (<= 0 tau_3_t)) (assert (<= tau_3_t 0.5))
(assert (<= -1.5 r_3_0)) (assert (<= r_3_0 1.5))
(assert (<= -1.5 r_3_t)) (assert (<= r_3_t 1.5))
(assert (<= -1.5 psi_3_0)) (assert (<= psi_3_0 1.5))
(assert (<= -1.5 psi_3_t)) (assert (<= psi_3_t 1.5))
(assert (<= -1.5 phi_3_0)) (assert (<= phi_3_0 1.5))
(assert (<= -1.5 phi_3_t)) (assert (<= phi_3_t 1.5))
(assert (<= -1.5 p_3_0)) (assert (<= p_3_0 1.5))
(assert (<= -1.5 p_3_t)) (assert (<= p_3_t 1.5))
(assert (<= -3.14159 gRDR_3_0)) (assert (<= gRDR_3_0 3.14159))
(assert (<= -3.14159 gRDR_3_t)) (assert (<= gRDR_3_t 3.14159))
(assert (<= -3.14159 gAIL_3_0)) (assert (<= gAIL_3_0 3.14159))
(assert (<= -3.14159 gAIL_3_t)) (assert (<= gAIL_3_t 3.14159))
(assert (<= -3.14159 gDir_3_0)) (assert (<= gDir_3_0 3.14159))
(assert (<= -3.14159 gDir_3_t)) (assert (<= gDir_3_t 3.14159))
(assert (<= -3.14159 beta_3_0)) (assert (<= beta_3_0 3.14159))
(assert (<= -3.14159 beta_3_t)) (assert (<= beta_3_t 3.14159))
(assert (<= -3.14159 xAIL_3_0)) (assert (<= xAIL_3_0 3.14159))
(assert (<= -3.14159 xAIL_3_t)) (assert (<= xAIL_3_t 3.14159))
(assert (<= -3.14159 xRDR_3_0)) (assert (<= xRDR_3_0 3.14159))
(assert (<= -3.14159 xRDR_3_t)) (assert (<= xRDR_3_t 3.14159))
(assert (and (= tau_0_0 0) (= gRDR_0_0 0) (= gAIL_0_0 0) (= psi_0_0 0)
(= phi_0_0 0) (= r_0_0 0) (= p_0_0 0) (= beta_0_0 0)
(< 0.5 gDir_0_0) (< gDir_0_0 0.7)))
(assert (and (= xAIL_0_0 0) (= modeA_0 true)))
(assert (and (= xRDR_0_0 0) (= modeR_0 true)))
(assert (and (>= tau_0_0 0) (<= tau_0_0 0.5)
(>= tau_0_t 0) (<= tau_0_t 0.5)))
(assert (or (and (= modeA_0 true) (= modeR_0 true)
(= [beta_0_t p_0_t r_0_t phi_0_t psi_0_t xAIL_0_t xRDR_0_t gAIL_0_t gRDR_0_t gDir_0_t tau_0_t]
(integral 0. time_0
[beta_0_0 p_0_0 r_0_0 phi_0_0 psi_0_0 xAIL_0_0 xRDR_0_0 gAIL_0_0 gRDR_0_0 gDir_0_0 tau_0_0] flow_1)))
(and (= modeA_0 true) (= modeR_0 false)
(= [beta_0_t p_0_t r_0_t phi_0_t psi_0_t xAIL_0_t xRDR_0_t gAIL_0_t gRDR_0_t gDir_0_t tau_0_t]
(integral 0. time_0
[beta_0_0 p_0_0 r_0_0 phi_0_0 psi_0_0 xAIL_0_0 xRDR_0_0 gAIL_0_0 gRDR_0_0 gDir_0_0 tau_0_0] flow_2)))
(and (= modeA_0 false) (= modeR_0 true)
(= [beta_0_t p_0_t r_0_t phi_0_t psi_0_t xAIL_0_t xRDR_0_t gAIL_0_t gRDR_0_t gDir_0_t tau_0_t]
(integral 0. time_0
[beta_0_0 p_0_0 r_0_0 phi_0_0 psi_0_0 xAIL_0_0 xRDR_0_0 gAIL_0_0 gRDR_0_0 gDir_0_0 tau_0_0] flow_3)))
(and (= modeA_0 false) (= modeR_0 false)
(= [beta_0_t p_0_t r_0_t phi_0_t psi_0_t xAIL_0_t xRDR_0_t gAIL_0_t gRDR_0_t gDir_0_t tau_0_t]
(integral 0. time_0
[beta_0_0 p_0_0 r_0_0 phi_0_0 psi_0_0 xAIL_0_0 xRDR_0_0 gAIL_0_0 gRDR_0_0 gDir_0_0 tau_0_0] flow_4)))))
(assert (and (= tau_0_t 0.5) (= tau_1_0 0)
(= gRDR_1_0 (* beta_0_t 0.35))
(= gAIL_1_0 (* (- gDir_0_t (/ (* psi_0_t 180) 3.14)) 0.5))
(= psi_1_0 psi_0_t) (= phi_1_0 phi_0_t)
(= r_1_0 r_0_t) (= p_1_0 p_0_t)
(= gDir_1_0 gDir_0_t) (= beta_1_0 beta_0_t)))
(assert (and (= xAIL_1_0 xAIL_0_t)))
(assert (or (and (>= gAIL_0_t xAIL_0_t) (= modeA_1 true))
(and (< gAIL_0_t xAIL_0_t) (= modeA_1 false))))
(assert (= xRDR_1_0 xRDR_0_t))
(assert (or (and (>= gRDR_0_t xRDR_0_t) (= modeR_1 true))
(and (< gRDR_0_t xRDR_0_t) (= modeR_1 false))))
(assert (and (>= tau_1_0 0) (<= tau_1_0 0.5)
(>= tau_1_t 0) (<= tau_1_t 0.5)))
(assert (or (and (= modeA_1 true) (= modeR_1 true)
(= [beta_1_t p_1_t r_1_t phi_1_t psi_1_t xAIL_1_t xRDR_1_t gAIL_1_t gRDR_1_t gDir_1_t tau_1_t]
(integral 0. time_1
[beta_1_0 p_1_0 r_1_0 phi_1_0 psi_1_0 xAIL_1_0 xRDR_1_0 gAIL_1_0 gRDR_1_0 gDir_1_0 tau_1_0] flow_1)))
(and (= modeA_1 true) (= modeR_1 false)
(= [beta_1_t p_1_t r_1_t phi_1_t psi_1_t xAIL_1_t xRDR_1_t gAIL_1_t gRDR_1_t gDir_1_t tau_1_t]
(integral 0. time_1
[beta_1_0 p_1_0 r_1_0 phi_1_0 psi_1_0 xAIL_1_0 xRDR_1_0 gAIL_1_0 gRDR_1_0 gDir_1_0 tau_1_0] flow_2)))
(and (= modeA_1 false) (= modeR_1 true)
(= [beta_1_t p_1_t r_1_t phi_1_t psi_1_t xAIL_1_t xRDR_1_t gAIL_1_t gRDR_1_t gDir_1_t tau_1_t]
(integral 0. time_1
[beta_1_0 p_1_0 r_1_0 phi_1_0 psi_1_0 xAIL_1_0 xRDR_1_0 gAIL_1_0 gRDR_1_0 gDir_1_0 tau_1_0] flow_3)))
(and (= modeA_1 false) (= modeR_1 false)
(= [beta_1_t p_1_t r_1_t phi_1_t psi_1_t xAIL_1_t xRDR_1_t gAIL_1_t gRDR_1_t gDir_1_t tau_1_t]
(integral 0. time_1
[beta_1_0 p_1_0 r_1_0 phi_1_0 psi_1_0 xAIL_1_0 xRDR_1_0 gAIL_1_0 gRDR_1_0 gDir_1_0 tau_1_0] flow_4)))))
(assert (and (= tau_1_t 0.5) (= tau_2_0 0)
(= gRDR_2_0 (* beta_1_t 0.35))
(= gAIL_2_0 (* (- gDir_1_t (/ (* psi_1_t 180) 3.14)) 0.5))
(= psi_2_0 psi_1_t) (= phi_2_0 phi_1_t)
(= r_2_0 r_1_t) (= p_2_0 p_1_t)
(= gDir_2_0 gDir_1_t) (= beta_2_0 beta_1_t)))
(assert (and (= xAIL_2_0 xAIL_1_t)))
(assert (or (and (>= gAIL_1_t xAIL_1_t) (= modeA_2 true))
(and (< gAIL_1_t xAIL_1_t) (= modeA_2 false))))
(assert (= xRDR_2_0 xRDR_1_t))
(assert (or (and (>= gRDR_1_t xRDR_1_t) (= modeR_2 true))
(and (< gRDR_1_t xRDR_1_t) (= modeR_2 false))))
(assert (and (>= tau_2_0 0) (<= tau_2_0 0.5)
(>= tau_2_t 0) (<= tau_2_t 0.5)))
(assert (or (and (= modeA_2 true) (= modeR_2 true)
(= [beta_2_t p_2_t r_2_t phi_2_t psi_2_t xAIL_2_t xRDR_2_t gAIL_2_t gRDR_2_t gDir_2_t tau_2_t]
(integral 0. time_2
[beta_2_0 p_2_0 r_2_0 phi_2_0 psi_2_0 xAIL_2_0 xRDR_2_0 gAIL_2_0 gRDR_2_0 gDir_2_0 tau_2_0] flow_1)))
(and (= modeA_2 true) (= modeR_2 false)
(= [beta_2_t p_2_t r_2_t phi_2_t psi_2_t xAIL_2_t xRDR_2_t gAIL_2_t gRDR_2_t gDir_2_t tau_2_t]
(integral 0. time_2
[beta_2_0 p_2_0 r_2_0 phi_2_0 psi_2_0 xAIL_2_0 xRDR_2_0 gAIL_2_0 gRDR_2_0 gDir_2_0 tau_2_0] flow_2)))
(and (= modeA_2 false) (= modeR_2 true)
(= [beta_2_t p_2_t r_2_t phi_2_t psi_2_t xAIL_2_t xRDR_2_t gAIL_2_t gRDR_2_t gDir_2_t tau_2_t]
(integral 0. time_2
[beta_2_0 p_2_0 r_2_0 phi_2_0 psi_2_0 xAIL_2_0 xRDR_2_0 gAIL_2_0 gRDR_2_0 gDir_2_0 tau_2_0] flow_3)))
(and (= modeA_2 false) (= modeR_2 false)
(= [beta_2_t p_2_t r_2_t phi_2_t psi_2_t xAIL_2_t xRDR_2_t gAIL_2_t gRDR_2_t gDir_2_t tau_2_t]
(integral 0. time_2
[beta_2_0 p_2_0 r_2_0 phi_2_0 psi_2_0 xAIL_2_0 xRDR_2_0 gAIL_2_0 gRDR_2_0 gDir_2_0 tau_2_0] flow_4)))))
(assert (and (= tau_2_t 0.5) (= tau_3_0 0)
(= gRDR_3_0 (* beta_2_t 0.35))
(= gAIL_3_0 (* (- gDir_2_t (/ (* psi_2_t 180) 3.14)) 0.5))
(= psi_3_0 psi_2_t) (= phi_3_0 phi_2_t)
(= r_3_0 r_2_t) (= p_3_0 p_2_t)
(= gDir_3_0 gDir_2_t) (= beta_3_0 beta_2_t)))
(assert (and (= xAIL_3_0 xAIL_2_t)))
(assert (or (and (>= gAIL_2_t xAIL_2_t) (= modeA_3 true))
(and (< gAIL_2_t xAIL_2_t) (= modeA_3 false))))
(assert (= xRDR_3_0 xRDR_2_t))
(assert (or (and (>= gRDR_2_t xRDR_2_t) (= modeR_3 true))
(and (< gRDR_2_t xRDR_2_t) (= modeR_3 false))))
(assert (and (>= tau_3_0 0) (<= tau_3_0 0.5)
(>= tau_3_t 0) (<= tau_3_t 0.5)))
(assert (or (and (= modeA_3 true) (= modeR_3 true)
(= [beta_3_t p_3_t r_3_t phi_3_t psi_3_t xAIL_3_t xRDR_3_t gAIL_3_t gRDR_3_t gDir_3_t tau_3_t]
(integral 0. time_3
[beta_3_0 p_3_0 r_3_0 phi_3_0 psi_3_0 xAIL_3_0 xRDR_3_0 gAIL_3_0 gRDR_3_0 gDir_3_0 tau_3_0] flow_1)))
(and (= modeA_3 true) (= modeR_3 false)
(= [beta_3_t p_3_t r_3_t phi_3_t psi_3_t xAIL_3_t xRDR_3_t gAIL_3_t gRDR_3_t gDir_3_t tau_3_t]
(integral 0. time_3
[beta_3_0 p_3_0 r_3_0 phi_3_0 psi_3_0 xAIL_3_0 xRDR_3_0 gAIL_3_0 gRDR_3_0 gDir_3_0 tau_3_0] flow_2)))
(and (= modeA_3 false) (= modeR_3 true)
(= [beta_3_t p_3_t r_3_t phi_3_t psi_3_t xAIL_3_t xRDR_3_t gAIL_3_t gRDR_3_t gDir_3_t tau_3_t]
(integral 0. time_3
[beta_3_0 p_3_0 r_3_0 phi_3_0 psi_3_0 xAIL_3_0 xRDR_3_0 gAIL_3_0 gRDR_3_0 gDir_3_0 tau_3_0] flow_3)))
(and (= modeA_3 false) (= modeR_3 false)
(= [beta_3_t p_3_t r_3_t phi_3_t psi_3_t xAIL_3_t xRDR_3_t gAIL_3_t gRDR_3_t gDir_3_t tau_3_t]
(integral 0. time_3
[beta_3_0 p_3_0 r_3_0 phi_3_0 psi_3_0 xAIL_3_0 xRDR_3_0 gAIL_3_0 gRDR_3_0 gDir_3_0 tau_3_0] flow_4)))))
(assert (< (^ (^ beta_3_t 2) 0.5) 1))
(check-sat)
(exit)