1(set-logic QF_ALL_SUPPORTED)
2(set-info :status unsat)
3(define-sort Elt () Int)
4(define-sort mySet () (Set Elt ))
5(define-fun smt_set_emp () mySet (as emptyset mySet))
6(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (member x s))
7(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (singleton x)))
8(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
9(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
10(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
11(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subset s1 s2))
12(declare-fun z3v66 () Int)
13(declare-fun z3v67 () Int)
14(assert (distinct z3v66 z3v67))
15(declare-fun z3v68 () Int)
16(declare-fun z3f69 (Int) Int)
17(declare-fun z3f70 (Int) mySet)
18(declare-fun z3v71 () Int)
19(declare-fun z3f72 (Int) mySet)
20(declare-fun z3v73 () Int)
21(declare-fun z3v74 () Int)
22(declare-fun z3v75 () Int)
23(declare-fun z3f76 (Int) Bool)
24(declare-fun z3f77 (Int Int) Int)
25(declare-fun z3v78 () Int)
26(declare-fun z3f79 (Int) Bool)
27(declare-fun z3v80 () Int)
28(declare-fun z3f81 (Int) Int)
29(declare-fun z3v82 () Int)
30(declare-fun z3v83 () Int)
31(declare-fun z3v85 () Int)
32(declare-fun z3v86 () Int)
33(declare-fun z3v87 () Int)
34(declare-fun z3f88 () Int)
35(declare-fun z3v89 () Int)
36(declare-fun z3v90 () Int)
37(declare-fun z3v91 () Int)
38(declare-fun z3v92 () Int)
39(declare-fun z3v93 () Int)
40(declare-fun z3f94 (Int) Int)
41(declare-fun z3f95 (Int) Int)
42(declare-fun z3f96 (Int Int Int) Int)
43(declare-fun z3v97 () Int)
44(declare-fun z3v98 () Int)
45(declare-fun z3v99 () Int)
46(assert (= z3v99 z3v98))
47(assert (and (>= (z3f69 z3v85) 0)
48             (not (smt_set_mem z3v86 (z3f70 z3v85)))
49             (= (z3f72 z3v85) smt_set_emp)
50             (>= (z3f69 z3v87) 0)
51             (= (z3f72 z3v87) smt_set_emp)
52             (= (z3f70 z3v87) smt_set_emp)
53             (= (z3f69 z3v87) 0)
54             (= (z3f76 z3v87) true)
55             (= z3v87 z3f88)
56             (>= (z3f69 z3v87) 0)
57             (= z3v87 z3v89)
58             (>= (z3f69 z3v87) 0)
59             (= (z3f70 z3v87)
60                (z3f70 z3v90))
61             (= (z3f72 z3v87) smt_set_emp)
62             (>= (z3f69 z3v89) 0)
63             (= (z3f70 z3v89)
64                (z3f70 z3v90))
65             (= (z3f72 z3v89) smt_set_emp)
66             (>= (z3f69 z3v90) 0)
67             (= (z3f72 z3v90)
68                (ite (smt_set_mem z3v86 (z3f70 z3v85))
69                     (smt_set_cup (smt_set_add smt_set_emp z3v86)
70                                  (z3f72 z3v85))
71                     (z3f72 z3v85)))
72             (= (z3f70 z3v90)
73                (smt_set_cup (smt_set_add smt_set_emp z3v86)
74                             (z3f70 z3v85)))
75             (= (z3f69 z3v90)
76                (+ 1 (z3f69 z3v85)))
77             (= (z3f76 z3v90) false)
78             (>= (z3f69 z3v91) 0)
79             (= (z3f72 z3v91) smt_set_emp)
80             (= (z3f70 z3v91) smt_set_emp)
81             (= (z3f69 z3v91) 0)
82             (= (z3f76 z3v91) true)
83             (= z3v91 z3f88)
84             (>= (z3f69 z3v91) 0)
85             (= z3v91 z3v92)
86             (>= (z3f69 z3v91) 0)
87             (not (smt_set_mem z3v86 (z3f70 z3v91)))
88             (= (z3f72 z3v91) smt_set_emp)
89             (= (z3f94 z3v93) z3v92)
90             (= (z3f95 z3v93) z3v85)
91             (= z3v93 (z3f96 z3v86 z3v92 z3v85))
92             (= z3v93 z3v97)
93             (= (smt_set_cap (z3f70 (z3f94 z3v93))
94                             (z3f70 (z3f95 z3v93))) smt_set_emp)
95             (>= (z3f69 z3v92) 0)
96             (not (smt_set_mem z3v86 (z3f70 z3v92)))
97             (= (z3f72 z3v92) smt_set_emp)
98             (= (smt_set_cap (z3f70 (z3f94 z3v97))
99                             (z3f70 (z3f95 z3v97))) smt_set_emp)
100             (z3f79 z3v66)
101             (= (z3f81 z3v80) z3v80)
102             (= (z3f81 z3v82) z3v82)
103             (not (z3f79 z3v67))
104             (= (z3f81 z3v83) z3v83)))
105(assert (not (>  z3v99 z3v98)))
106(check-sat)
107