blob: 0df4535ab7732ecd1d61607dff3afbdc5b0aecf2 (
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
|
(set-logic QF_UF)
(set-info :source |
Generating minimum transitivity constraints in P-time for deciding Equality Logic,
Ofer Strichman and Mirron Rozanov,
SMT Workshop 2005.
Translator: Leonardo de Moura. |)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort U 0)
(declare-fun x0 () U)
(declare-fun y0 () U)
(declare-fun z0 () U)
(declare-fun x1 () U)
(declare-fun y1 () U)
(declare-fun z1 () U)
(declare-fun x2 () U)
(declare-fun y2 () U)
(declare-fun z2 () U)
(declare-fun x3 () U)
(declare-fun y3 () U)
(declare-fun z3 () U)
(declare-fun x4 () U)
(declare-fun y4 () U)
(declare-fun z4 () U)
(declare-fun x5 () U)
(declare-fun y5 () U)
(declare-fun z5 () U)
(declare-fun x6 () U)
(declare-fun y6 () U)
(declare-fun z6 () U)
(declare-fun x7 () U)
(declare-fun y7 () U)
(declare-fun z7 () U)
(declare-fun x8 () U)
(declare-fun y8 () U)
(declare-fun z8 () U)
(declare-fun x9 () U)
(declare-fun y9 () U)
(declare-fun z9 () U)
(declare-fun x10 () U)
(declare-fun y10 () U)
(declare-fun z10 () U)
(declare-fun x11 () U)
(declare-fun y11 () U)
(declare-fun z11 () U)
(declare-fun x12 () U)
(declare-fun y12 () U)
(declare-fun z12 () U)
(declare-fun x13 () U)
(declare-fun y13 () U)
(declare-fun z13 () U)
(declare-fun x14 () U)
(declare-fun y14 () U)
(declare-fun z14 () U)
(declare-fun x15 () U)
(declare-fun y15 () U)
(declare-fun z15 () U)
(declare-fun x16 () U)
(declare-fun y16 () U)
(declare-fun z16 () U)
(declare-fun x17 () U)
(declare-fun y17 () U)
(declare-fun z17 () U)
(declare-fun x18 () U)
(declare-fun y18 () U)
(declare-fun z18 () U)
(declare-fun x19 () U)
(declare-fun y19 () U)
(declare-fun z19 () U)
(declare-fun x20 () U)
(declare-fun y20 () U)
(declare-fun z20 () U)
(declare-fun x21 () U)
(declare-fun y21 () U)
(declare-fun z21 () U)
(declare-fun x22 () U)
(declare-fun y22 () U)
(declare-fun z22 () U)
(declare-fun x23 () U)
(declare-fun y23 () U)
(declare-fun z23 () U)
(declare-fun x24 () U)
(declare-fun y24 () U)
(declare-fun z24 () U)
(declare-fun x25 () U)
(declare-fun y25 () U)
(declare-fun z25 () U)
(declare-fun x26 () U)
(declare-fun y26 () U)
(declare-fun z26 () U)
(declare-fun x27 () U)
(declare-fun y27 () U)
(declare-fun z27 () U)
(declare-fun x28 () U)
(declare-fun y28 () U)
(declare-fun z28 () U)
(declare-fun x29 () U)
(declare-fun y29 () U)
(declare-fun z29 () U)
(declare-fun x30 () U)
(declare-fun y30 () U)
(declare-fun z30 () U)
(declare-fun x31 () U)
(declare-fun y31 () U)
(declare-fun z31 () U)
(declare-fun x32 () U)
(declare-fun y32 () U)
(declare-fun z32 () U)
(declare-fun x33 () U)
(declare-fun y33 () U)
(declare-fun z33 () U)
(declare-fun x34 () U)
(declare-fun y34 () U)
(declare-fun z34 () U)
(declare-fun x35 () U)
(declare-fun y35 () U)
(declare-fun z35 () U)
(declare-fun x36 () U)
(declare-fun y36 () U)
(declare-fun z36 () U)
(assert
(and (or (and (= x0 y0) (= y0 x1)) (and (= x0 z0) (= z0 x1)))
(and (or (and (= x1 y1) (= y1 x2)) (and (= x1 z1) (= z1 x2)))
(and (or (and (= x2 y2) (= y2 x3)) (and (= x2 z2) (= z2 x3)))
(and (or (and (= x3 y3) (= y3 x4)) (and (= x3 z3) (= z3 x4)))
(and (or (and (= x4 y4) (= y4 x5)) (and (= x4 z4) (= z4 x5)))
(and (or (and (= x5 y5) (= y5 x6)) (and (= x5 z5) (= z5 x6)))
(and (or (and (= x6 y6) (= y6 x7)) (and (= x6 z6) (= z6 x7)))
(and (or (and (= x7 y7) (= y7 x8)) (and (= x7 z7) (= z7 x8)))
(and (or (and (= x8 y8) (= y8 x9)) (and (= x8 z8) (= z8 x9)))
(and (or (and (= x9 y9) (= y9 x10)) (and (= x9 z9) (= z9 x10)))
(and (or (and (= x10 y10) (= y10 x11)) (and (= x10 z10) (= z10 x11)))
(and (or (and (= x11 y11) (= y11 x12)) (and (= x11 z11) (= z11 x12)))
(and (or (and (= x12 y12) (= y12 x13)) (and (= x12 z12) (= z12 x13)))
(and (or (and (= x13 y13) (= y13 x14)) (and (= x13 z13) (= z13 x14)))
(and (or (and (= x14 y14) (= y14 x15)) (and (= x14 z14) (= z14 x15)))
(and (or (and (= x15 y15) (= y15 x16)) (and (= x15 z15) (= z15 x16)))
(and (or (and (= x16 y16) (= y16 x17)) (and (= x16 z16) (= z16 x17)))
(and (or (and (= x17 y17) (= y17 x18)) (and (= x17 z17) (= z17 x18)))
(and (or (and (= x18 y18) (= y18 x19)) (and (= x18 z18) (= z18 x19)))
(and (or (and (= x19 y19) (= y19 x20)) (and (= x19 z19) (= z19 x20)))
(and (or (and (= x20 y20) (= y20 x21)) (and (= x20 z20) (= z20 x21)))
(and (or (and (= x21 y21) (= y21 x22)) (and (= x21 z21) (= z21 x22)))
(and (or (and (= x22 y22) (= y22 x23)) (and (= x22 z22) (= z22 x23)))
(and (or (and (= x23 y23) (= y23 x24)) (and (= x23 z23) (= z23 x24)))
(and (or (and (= x24 y24) (= y24 x25)) (and (= x24 z24) (= z24 x25)))
(and (or (and (= x25 y25) (= y25 x26)) (and (= x25 z25) (= z25 x26)))
(and (or (and (= x26 y26) (= y26 x27)) (and (= x26 z26) (= z26 x27)))
(and (or (and (= x27 y27) (= y27 x28)) (and (= x27 z27) (= z27 x28)))
(and (or (and (= x28 y28) (= y28 x29)) (and (= x28 z28) (= z28 x29)))
(and (or (and (= x29 y29) (= y29 x30)) (and (= x29 z29) (= z29 x30)))
(and (or (and (= x30 y30) (= y30 x31)) (and (= x30 z30) (= z30 x31)))
(and (or (and (= x31 y31) (= y31 x32)) (and (= x31 z31) (= z31 x32)))
(and (or (and (= x32 y32) (= y32 x33)) (and (= x32 z32) (= z32 x33)))
(and (or (and (= x33 y33) (= y33 x34)) (and (= x33 z33) (= z33 x34)))
(and (or (and (= x34 y34) (= y34 x35)) (and (= x34 z34) (= z34 x35)))
(and (or (and (= x35 y35) (= y35 x36)) (and (= x35 z35) (= z35 x36)))
(not (= x0 x36)))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
|
