1(set-option :print-success false)
2(set-logic AUFLIAFS)
3(set-info :status unsat)
4(declare-sort Loc 0)
5(define-sort SetLoc () (Set Loc))
6(define-sort SetInt () (Set Int))
7(declare-sort FldLoc 0)
8(declare-sort FldInt 0)
9(declare-fun null$0 () Loc)
10(declare-fun read$0 (FldLoc Loc) Loc)
11(declare-fun write$0 (FldLoc Loc Loc) FldLoc)
12(declare-fun ep$0 (FldLoc SetLoc Loc) Loc)
13(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
14(declare-fun Frame$0 (SetLoc SetLoc FldLoc FldLoc) Bool)
15(declare-fun Alloc$0 () SetLoc)
16(declare-fun FP$0 () SetLoc)
17(declare-fun FP_1$0 () SetLoc)
18(declare-fun FP_2$0 () SetLoc)
19(declare-fun FP_Caller$0 () SetLoc)
20(declare-fun FP_Caller_1$0 () SetLoc)
21(declare-fun curr_2$0 () Loc)
22(declare-fun curr_3$0 () Loc)
23(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc)
24(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool)
25(declare-fun lst$0 () Loc)
26(declare-fun lst_1$0 () Loc)
27(declare-fun next$0 () FldLoc)
28(declare-fun next_1$0 () FldLoc)
29(declare-fun nondet_2$0 () Bool)
30(declare-fun sk_?X_27$0 () SetLoc)
31(declare-fun sk_?X_28$0 () SetLoc)
32(declare-fun sk_?X_29$0 () SetLoc)
33(declare-fun sk_?X_30$0 () SetLoc)
34(declare-fun sk_?X_31$0 () SetLoc)
35(declare-fun sk_?X_32$0 () SetLoc)
36(declare-fun sk_?X_33$0 () SetLoc)
37(declare-fun tmp_2$0 () Loc)
38
39(assert (! (forall ((?y Loc))
40           (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
41               (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y)))
42   :named btwn_reach_8))
43
44(assert (! (forall ((?y Loc))
45           (or (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y)
46               (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) ?y)))
47   :named btwn_reach_9))
48
49(assert (! (forall ((?y Loc))
50           (or (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y)
51               (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) ?y)))
52   :named btwn_reach_10))
53
54(assert (! (forall ((?y Loc))
55           (or (not (= (read$0 next$0 null$0) null$0))
56               (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
57   :named btwn_cycl_8))
58
59(assert (! (forall ((?y Loc))
60           (or (not (= (read$0 next$0 tmp_2$0) tmp_2$0))
61               (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y)))
62   :named btwn_cycl_9))
63
64(assert (! (forall ((?y Loc))
65           (or (not (= (read$0 next$0 curr_3$0) curr_3$0))
66               (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y)))
67   :named btwn_cycl_10))
68
69(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0))
70   :named btwn_step_8))
71
72(assert (! (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) (read$0 next$0 tmp_2$0))
73   :named btwn_step_9))
74
75(assert (! (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) (read$0 next$0 curr_3$0))
76   :named btwn_step_10))
77
78(assert (! (forall ((?f FldLoc))
79           (or (member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0)
80               (= null$0 (ep$0 ?f sk_?X_30$0 null$0))))
81   :named entry-point3_10))
82
83(assert (! (forall ((?f FldLoc))
84           (or (member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0)
85               (= lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0))))
86   :named entry-point3_11))
87
88(assert (! (forall ((?f FldLoc))
89           (or (member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0)
90               (= curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0))))
91   :named entry-point3_12))
92
93(assert (! (forall ((?f FldLoc))
94           (or (member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0)
95               (= tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0))))
96   :named entry-point3_13))
97
98(assert (! (forall ((?f FldLoc))
99           (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0)
100             (ep$0 ?f sk_?X_30$0 null$0)))
101   :named entry-point1_10))
102
103(assert (! (forall ((?f FldLoc))
104           (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0)
105             (ep$0 ?f sk_?X_30$0 lst_1$0)))
106   :named entry-point1_11))
107
108(assert (! (forall ((?f FldLoc))
109           (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0)
110             (ep$0 ?f sk_?X_30$0 curr_3$0)))
111   :named entry-point1_12))
112
113(assert (! (forall ((?f FldLoc))
114           (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0)
115             (ep$0 ?f sk_?X_30$0 tmp_2$0)))
116   :named entry-point1_13))
117
118(assert (! (forall ((?f FldLoc) (?y Loc))
119           (or (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) ?y)
120               (not (Btwn$0 ?f null$0 ?y ?y)) (not (member ?y sk_?X_30$0))))
121   :named entry-point4_10))
122
123(assert (! (forall ((?f FldLoc) (?y Loc))
124           (or (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) ?y)
125               (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (member ?y sk_?X_30$0))))
126   :named entry-point4_11))
127
128(assert (! (forall ((?f FldLoc) (?y Loc))
129           (or (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) ?y)
130               (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (member ?y sk_?X_30$0))))
131   :named entry-point4_12))
132
133(assert (! (forall ((?f FldLoc) (?y Loc))
134           (or (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) ?y)
135               (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (member ?y sk_?X_30$0))))
136   :named entry-point4_13))
137
138(assert (! (forall ((?f FldLoc) (?y Loc))
139           (or (not (Btwn$0 ?f null$0 ?y ?y)) (not (member ?y sk_?X_30$0))
140               (member (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0)))
141   :named entry-point2_10))
142
143(assert (! (forall ((?f FldLoc) (?y Loc))
144           (or (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (member ?y sk_?X_30$0))
145               (member (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0)))
146   :named entry-point2_11))
147
148(assert (! (forall ((?f FldLoc) (?y Loc))
149           (or (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (member ?y sk_?X_30$0))
150               (member (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0)))
151   :named entry-point2_12))
152
153(assert (! (forall ((?f FldLoc) (?y Loc))
154           (or (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (member ?y sk_?X_30$0))
155               (member (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0)))
156   :named entry-point2_13))
157
158(assert (! (= (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0)
159     (read$0 next$0 tmp_2$0))
160   :named read_write2))
161
162(assert (! (or (= null$0 curr_3$0)
163       (= (read$0 next$0 null$0)
164         (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) null$0)))
165   :named read_write1))
166
167(assert (! (or (= tmp_2$0 curr_3$0)
168       (= (read$0 next$0 tmp_2$0)
169         (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) tmp_2$0)))
170   :named read_write1_1))
171
172(assert (! (or (= curr_3$0 curr_3$0)
173       (= (read$0 next$0 curr_3$0)
174         (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0)))
175   :named read_write1_2))
176
177(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_5))
178
179(assert (! (= (read$0 next_1$0 null$0) null$0) :named read_null_6))
180
181(assert (! (forall ((l1 Loc))
182           (or
183               (and (Btwn$0 next$0 lst$0 l1 curr_2$0)
184                    (member l1 (lseg_domain$0 next$0 lst$0 curr_2$0))
185                    (not (= l1 curr_2$0)))
186               (and
187                    (or (= l1 curr_2$0)
188                        (not (Btwn$0 next$0 lst$0 l1 curr_2$0)))
189                    (not (member l1 (lseg_domain$0 next$0 lst$0 curr_2$0))))))
190   :named lseg_footprint_20))
191
192(assert (! (forall ((l1 Loc))
193           (or
194               (and (Btwn$0 next$0 curr_3$0 l1 null$0)
195                    (member l1 (lseg_domain$0 next$0 curr_3$0 null$0))
196                    (not (= l1 null$0)))
197               (and
198                    (or (= l1 null$0)
199                        (not (Btwn$0 next$0 curr_3$0 l1 null$0)))
200                    (not (member l1 (lseg_domain$0 next$0 curr_3$0 null$0))))))
201   :named lseg_footprint_21))
202
203(assert (! (not (member tmp_2$0 FP_2$0)) :named check_free_31_6))
204
205(assert (! (not (member null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15))
206
207(assert (! (not (= lst$0 null$0)) :named if_else_13_6_4))
208
209(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
210   :named precondition_of_remove_10_11_20))
211
212(assert (! (= sk_?X_33$0 FP$0) :named precondition_of_remove_10_11_21))
213
214(assert (! (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0) :named invariant_18_4_62))
215
216(assert (! (= FP$0 (union FP_1$0 FP$0)) :named invariant_18_4_63))
217
218(assert (! (= sk_?X_31$0 (lseg_domain$0 next$0 curr_2$0 null$0))
219   :named invariant_18_4_64))
220
221(assert (! (= sk_?X_30$0 (union sk_?X_31$0 sk_?X_32$0)) :named invariant_18_4_65))
222
223(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_66))
224
225(assert (! (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0)
226   :named invariant_18_4_67))
227
228(assert (! (= sk_?X_29$0 (union sk_?X_28$0 sk_?X_27$0)) :named invariant_18_4_68))
229
230(assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0))
231   :named invariant_18_4_69))
232
233(assert (! (= (as emptyset SetLoc) (intersection sk_?X_27$0 sk_?X_28$0))
234   :named invariant_18_4_70))
235
236(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
237   :named initial_footprint_of_remove_10_11_10))
238
239(assert (! (Frame$0 FP_1$0 Alloc$0 next$0 next$0)
240   :named framecondition_of_remove_loop_18_4_16))
241
242(assert (! (= next_1$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)))
243   :named assign_30_6))
244
245(assert (! (= curr_2$0 lst$0) :named assign_17_4_4))
246
247(assert (! (= FP_2$0
248     (union (setminus FP$0 FP_1$0)
249       (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0))))
250   :named framecondition_of_remove_loop_18_4_17))
251
252(assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0)
253       (not (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0)))
254   :named unnamed_23))
255
256(assert (! (or (Btwn$0 next$0 curr_3$0 null$0 null$0)
257       (not (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0)))
258   :named unnamed_24))
259
260(assert (! (or (= (read$0 next$0 curr_3$0) null$0) (not nondet_2$0))
261   :named unnamed_25))
262
263(assert (! (forall ((l1 Loc))
264           (or
265               (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0)
266                    (member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0))
267                    (not (= l1 curr_3$0)))
268               (and
269                    (or (= l1 curr_3$0)
270                        (not (Btwn$0 next$0 lst_1$0 l1 curr_3$0)))
271                    (not (member l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0))))))
272   :named lseg_footprint_22))
273
274(assert (! (forall ((l1 Loc))
275           (or
276               (and (Btwn$0 next$0 lst$0 l1 null$0)
277                    (member l1 (lseg_domain$0 next$0 lst$0 null$0))
278                    (not (= l1 null$0)))
279               (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0)))
280                    (not (member l1 (lseg_domain$0 next$0 lst$0 null$0))))))
281   :named lseg_footprint_23))
282
283(assert (! (forall ((l1 Loc))
284           (or
285               (and (Btwn$0 next$0 curr_2$0 l1 null$0)
286                    (member l1 (lseg_domain$0 next$0 curr_2$0 null$0))
287                    (not (= l1 null$0)))
288               (and
289                    (or (= l1 null$0)
290                        (not (Btwn$0 next$0 curr_2$0 l1 null$0)))
291                    (not (member l1 (lseg_domain$0 next$0 curr_2$0 null$0))))))
292   :named lseg_footprint_24))
293
294(assert (! (not (member null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11))
295
296(assert (! (not (= tmp_2$0 null$0)) :named if_else_28_8_2))
297
298(assert (! (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0)
299   :named precondition_of_remove_10_11_22))
300
301(assert (! (= sk_?X_33$0 (lseg_domain$0 next$0 lst$0 null$0))
302   :named precondition_of_remove_10_11_23))
303
304(assert (! (not (= curr_2$0 null$0)) :named invariant_18_4_71))
305
306(assert (! (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0)
307   :named invariant_18_4_72))
308
309(assert (! (= sk_?X_32$0 (lseg_domain$0 next$0 lst$0 curr_2$0))
310   :named invariant_18_4_73))
311
312(assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74))
313
314(assert (! (= (as emptyset SetLoc) (intersection sk_?X_32$0 sk_?X_31$0))
315   :named invariant_18_4_75))
316
317(assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76))
318
319(assert (! (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0)
320   :named invariant_18_4_77))
321
322(assert (! (= sk_?X_29$0
323     (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0)))
324   :named invariant_18_4_78))
325
326(assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0))
327   :named invariant_18_4_79))
328
329(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_80))
330
331(assert (! (= Alloc$0 (union FP_2$0 Alloc$0))
332   :named framecondition_of_remove_loop_18_4_18))
333
334(assert (! (= tmp_2$0 (read$0 next$0 curr_3$0)) :named assign_27_4_2))
335
336(assert (! (= lst_1$0 lst$0) :named framecondition_of_remove_loop_18_4_19))
337
338(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_13_2_5))
339
340(assert (! (or (Btwn$0 next$0 lst_1$0 curr_3$0 curr_3$0)
341       (not (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0)))
342   :named unnamed_26))
343
344(assert (! (or (Btwn$0 next$0 lst$0 null$0 null$0)
345       (not (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0)))
346   :named unnamed_27))
347
348(assert (! (or (Btwn$0 next$0 curr_2$0 null$0 null$0)
349       (not (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0)))
350   :named unnamed_28))
351
352(assert (! (forall ((?u Loc) (?v Loc) (?z Loc))
353           (and
354                (or
355                    (Btwn$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))
356                      ?z ?u ?v)
357                    (not
358                         (or
359                             (and (Btwn$0 next$0 ?z ?u ?v)
360                                  (or (Btwn$0 next$0 ?z ?v curr_3$0)
361                                      (and (Btwn$0 next$0 ?z ?v ?v)
362                                           (not
363                                                (Btwn$0 next$0 ?z curr_3$0
364                                                  curr_3$0)))))
365                             (and (not (= curr_3$0 ?v))
366                                  (or (Btwn$0 next$0 ?z curr_3$0 ?v)
367                                      (and
368                                           (Btwn$0 next$0 ?z curr_3$0
369                                             curr_3$0)
370                                           (not (Btwn$0 next$0 ?z ?v ?v))))
371                                  (Btwn$0 next$0 ?z ?u curr_3$0)
372                                  (or
373                                      (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
374                                        ?v curr_3$0)
375                                      (and
376                                           (Btwn$0 next$0
377                                             (read$0 next$0 tmp_2$0) ?v ?v)
378                                           (not
379                                                (Btwn$0 next$0
380                                                  (read$0 next$0 tmp_2$0)
381                                                  curr_3$0 curr_3$0)))))
382                             (and (not (= curr_3$0 ?v))
383                                  (or (Btwn$0 next$0 ?z curr_3$0 ?v)
384                                      (and
385                                           (Btwn$0 next$0 ?z curr_3$0
386                                             curr_3$0)
387                                           (not (Btwn$0 next$0 ?z ?v ?v))))
388                                  (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u
389                                    ?v)
390                                  (or
391                                      (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
392                                        ?v curr_3$0)
393                                      (and
394                                           (Btwn$0 next$0
395                                             (read$0 next$0 tmp_2$0) ?v ?v)
396                                           (not
397                                                (Btwn$0 next$0
398                                                  (read$0 next$0 tmp_2$0)
399                                                  curr_3$0 curr_3$0))))))))
400                (or
401                    (and (Btwn$0 next$0 ?z ?u ?v)
402                         (or (Btwn$0 next$0 ?z ?v curr_3$0)
403                             (and (Btwn$0 next$0 ?z ?v ?v)
404                                  (not (Btwn$0 next$0 ?z curr_3$0 curr_3$0)))))
405                    (and (not (= curr_3$0 ?v))
406                         (or (Btwn$0 next$0 ?z curr_3$0 ?v)
407                             (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0)
408                                  (not (Btwn$0 next$0 ?z ?v ?v))))
409                         (Btwn$0 next$0 ?z ?u curr_3$0)
410                         (or
411                             (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
412                               curr_3$0)
413                             (and
414                                  (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
415                                    ?v)
416                                  (not
417                                       (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
418                                         curr_3$0 curr_3$0)))))
419                    (and (not (= curr_3$0 ?v))
420                         (or (Btwn$0 next$0 ?z curr_3$0 ?v)
421                             (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0)
422                                  (not (Btwn$0 next$0 ?z ?v ?v))))
423                         (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u ?v)
424                         (or
425                             (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
426                               curr_3$0)
427                             (and
428                                  (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
429                                    ?v)
430                                  (not
431                                       (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
432                                         curr_3$0 curr_3$0)))))
433                    (not
434                         (Btwn$0
435                           (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))
436                           ?z ?u ?v)))))
437   :named btwn_write))
438
439(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_5))
440
441(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
442   :named btwn_sndw_5))
443
444(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
445           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
446               (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
447   :named btwn_ord1_5))
448
449(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
450           (or (not (Btwn$0 next$0 ?x ?y ?z))
451               (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
452   :named btwn_ord2_5))
453
454(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
455           (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
456               (Btwn$0 next$0 ?x ?z ?z)))
457   :named btwn_trn1_5))
458
459(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
460           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
461               (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
462   :named btwn_trn2_5))
463
464(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
465           (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
466               (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
467   :named btwn_trn3_5))
468
469(check-sat)
470(exit)
471