2016-Problem7-ltl.go.formulae.txt 51.7 KB
Newer Older
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
(! "main_final_output == 21" W "main_main___RERS__ == 8")
(! "main_final_output == 22" W "main_main___RERS__ == 4")
(! "main_final_output == 24" W "main_final_output == 23")
(! (true U "main_final_output == 21") || (! "main_final_output == 21" U (("main_main___RERS__ == 3" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_main___RERS__ == 7"))))
(! (true U "main_final_output == 22") || (! (("main_final_output == 24" && ! "main_final_output == 22") && X (! "main_final_output == 22" U ("main_final_output == 21" && ! "main_final_output == 22"))) U ("main_final_output == 22" || "main_main___RERS__ == 3")))
(! (true U "main_final_output == 22") || ((! "main_main___RERS__ == 17" || (! "main_final_output == 22" U (("main_final_output == 21" && ! "main_final_output == 22") && X (! "main_final_output == 22" U "main_final_output == 25")))) U "main_final_output == 22"))
(! (true U "main_final_output == 24") || (! "main_final_output == 23" U ("main_final_output == 24" || (("main_main___RERS__ == 14" && ! "main_final_output == 23") && X (! "main_final_output == 23" U "main_main___RERS__ == 12")))))
(! (true U "main_final_output == 24") || (! "main_final_output == 24" U (("main_final_output == 25" && ! "main_final_output == 24") && X (! "main_final_output == 24" U "main_final_output == 26"))))
(! (true U "main_final_output == 25") || (! (("main_final_output == 23" && ! "main_final_output == 25") && X (! "main_final_output == 25" U ("main_final_output == 26" && ! "main_final_output == 25"))) U ("main_final_output == 25" || "main_main___RERS__ == 10")))
(! (true U "main_final_output == 26") || (! "main_final_output == 26" U (("main_final_output == 21" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_main___RERS__ == 20"))))
(! (true U "main_main___RERS__ == 1") || ((! "main_main___RERS__ == 19" || (! "main_main___RERS__ == 1" U ((("main_final_output == 26" && ! "main_main___RERS__ == 1") && ! "main_final_output == 25") && X ((! "main_main___RERS__ == 1" && ! "main_final_output == 25") U "main_final_output == 23")))) U "main_main___RERS__ == 1"))
(! (true U "main_main___RERS__ == 1") || (("main_main___RERS__ == 7" && (! X (! "main_main___RERS__ == 1" U "main_main___RERS__ == 20") || X (! "main_main___RERS__ == 1" U ("main_main___RERS__ == 20" && (true U "main_final_output == 21"))))) U "main_main___RERS__ == 1"))
(! (true U "main_main___RERS__ == 17") || (! "main_final_output == 26" U ("main_main___RERS__ == 20" || "main_main___RERS__ == 17")))
(! (true U "main_main___RERS__ == 17") || (! (("main_final_output == 22" && ! "main_main___RERS__ == 17") && X (! "main_main___RERS__ == 17" U ("main_final_output == 23" && ! "main_main___RERS__ == 17"))) U ("main_main___RERS__ == 17" || "main_main___RERS__ == 12")))
(! (true U "main_main___RERS__ == 18") || ((! "main_main___RERS__ == 10" || (! "main_main___RERS__ == 18" U (("main_final_output == 21" && ! "main_main___RERS__ == 18") && X (! "main_main___RERS__ == 18" U "main_final_output == 25")))) U "main_main___RERS__ == 18"))
(! (true U "main_main___RERS__ == 19") || ((! "main_main___RERS__ == 14" || (! "main_main___RERS__ == 19" U (("main_final_output == 24" && ! "main_main___RERS__ == 19") && X (! "main_main___RERS__ == 19" U "main_final_output == 26")))) U "main_main___RERS__ == 19"))
(! (true U "main_main___RERS__ == 3") || (! "main_final_output == 22" U ("main_main___RERS__ == 3" || (("main_main___RERS__ == 6" && ! "main_final_output == 22") && X (! "main_final_output == 22" U "main_main___RERS__ == 1")))))
(! (true U "main_main___RERS__ == 3") || (("main_main___RERS__ == 13" && (! X (! "main_main___RERS__ == 3" U "main_main___RERS__ == 9") || X (! "main_main___RERS__ == 3" U ("main_main___RERS__ == 9" && (true U "main_final_output == 23"))))) U "main_main___RERS__ == 3"))
(! (true U "main_main___RERS__ == 5") || ((! "main_main___RERS__ == 13" || (! "main_main___RERS__ == 5" U (("main_final_output == 24" && ! "main_main___RERS__ == 5") && X (! "main_main___RERS__ == 5" U "main_final_output == 26")))) U "main_main___RERS__ == 5"))
(! (true U "main_main___RERS__ == 5") || (("main_main___RERS__ == 4" && (! X (! "main_main___RERS__ == 5" U "main_main___RERS__ == 6") || X (! "main_main___RERS__ == 5" U ("main_main___RERS__ == 6" && (true U "main_final_output == 24"))))) U "main_main___RERS__ == 5"))
(! (true U "main_main___RERS__ == 6") || ((! "main_main___RERS__ == 11" || (! "main_main___RERS__ == 6" U (("main_final_output == 26" && ! "main_main___RERS__ == 6") && X (! "main_main___RERS__ == 6" U "main_final_output == 25")))) U "main_main___RERS__ == 6"))
(! (true U "main_main___RERS__ == 7") || (! "main_final_output == 24" U ("main_main___RERS__ == 7" || (("main_main___RERS__ == 4" && ! "main_final_output == 24") && X (! "main_final_output == 24" U "main_main___RERS__ == 1")))))
(! (true U "main_main___RERS__ == 7") || ((! "main_main___RERS__ == 20" || (! "main_main___RERS__ == 7" U (("main_final_output == 21" && ! "main_main___RERS__ == 7") && X (! "main_main___RERS__ == 7" U "main_final_output == 26")))) U "main_main___RERS__ == 7"))
(! (true U "main_main___RERS__ == 7") || ((! "main_main___RERS__ == 20" || (! "main_main___RERS__ == 7" U ((("main_final_output == 23" && ! "main_main___RERS__ == 7") && ! "main_final_output == 26") && X ((! "main_main___RERS__ == 7" && ! "main_final_output == 26") U "main_final_output == 22")))) U "main_main___RERS__ == 7"))
(! (true U "main_main___RERS__ == 9") || ((! "main_main___RERS__ == 6" || (! "main_main___RERS__ == 9" U ("main_final_output == 25" && ! "main_main___RERS__ == 9"))) U "main_main___RERS__ == 9"))
(! (true U "main_main___RERS__ == 9") || (("main_main___RERS__ == 16" && (! X (! "main_main___RERS__ == 9" U "main_main___RERS__ == 18") || X (! "main_main___RERS__ == 9" U ("main_main___RERS__ == 18" && (true U "main_final_output == 23"))))) U "main_main___RERS__ == 9"))
(! (true U ("main_final_output == 21" && X (true U "main_final_output == 24"))) || (! "main_final_output == 21" U "main_main___RERS__ == 15"))
(! (true U ("main_final_output == 22" && X (true U "main_final_output == 25"))) || (! "main_final_output == 22" U "main_main___RERS__ == 16"))
(! (true U ("main_final_output == 23" && X (true U "main_final_output == 22"))) || (! "main_final_output == 23" U "main_final_output == 24"))
(! (true U ("main_final_output == 24" && X (true U "main_final_output == 21"))) || (! "main_final_output == 24" U "main_main___RERS__ == 5"))
(! (true U ("main_final_output == 24" && X (true U "main_final_output == 23"))) || (! "main_final_output == 24" U "main_main___RERS__ == 15"))
(! (true U ("main_final_output == 24" && X (true U "main_final_output == 25"))) || (! "main_final_output == 24" U "main_main___RERS__ == 17"))
(! (true U ("main_final_output == 26" && X (true U "main_final_output == 23"))) || (! "main_final_output == 26" U "main_main___RERS__ == 14"))
((false R ! "main_final_output == 23") || (true U ("main_final_output == 23" && (! "main_final_output == 25" W "main_main___RERS__ == 2"))))
((false R ! "main_final_output == 26") || (true U ("main_final_output == 26" && (! "main_final_output == 24" W "main_main___RERS__ == 15"))))
((false R ! "main_main___RERS__ == 13") || (! "main_main___RERS__ == 13" U ("main_main___RERS__ == 13" && (! (true U ("main_final_output == 23" && X (true U "main_final_output == 21"))) || (! "main_final_output == 23" U "main_main___RERS__ == 1")))))
((false R ! "main_main___RERS__ == 15") || (true U ("main_main___RERS__ == 15" && (! "main_final_output == 21" W "main_main___RERS__ == 6"))))
((false R ! "main_main___RERS__ == 16") || (! "main_main___RERS__ == 16" U ("main_main___RERS__ == 16" && (! (true U ("main_final_output == 25" && X (true U "main_final_output == 23"))) || (! "main_final_output == 25" U "main_main___RERS__ == 7")))))
((false R ! "main_main___RERS__ == 17") || (true U ("main_main___RERS__ == 17" && (! "main_final_output == 23" W "main_main___RERS__ == 13"))))
((false R ! "main_main___RERS__ == 2") || (! "main_main___RERS__ == 2" U ("main_main___RERS__ == 2" && (! (true U "main_final_output == 25") || (! "main_final_output == 25" U (("main_main___RERS__ == 18" && ! "main_final_output == 25") && X (! "main_final_output == 25" U "main_main___RERS__ == 6")))))))
((false R ! "main_main___RERS__ == 3") || (! "main_main___RERS__ == 3" U ("main_main___RERS__ == 3" && (! (true U ("main_final_output == 24" && X (true U "main_final_output == 22"))) || (! "main_final_output == 24" U "main_main___RERS__ == 10")))))
((false R ! "main_main___RERS__ == 6") || (! "main_main___RERS__ == 6" U ("main_main___RERS__ == 6" && (! (true U "main_final_output == 25") || (! "main_final_output == 25" U (("main_main___RERS__ == 16" && ! "main_final_output == 25") && X (! "main_final_output == 25" U "main_main___RERS__ == 4")))))))
(false R (! "main_final_output == 21" || ((! "main_main___RERS__ == 15" || (! "main_main___RERS__ == 12" U (("main_final_output == 23" && ! "main_main___RERS__ == 12") && X (! "main_main___RERS__ == 12" U "main_final_output == 26")))) U ("main_main___RERS__ == 12" || (false R (! "main_main___RERS__ == 15" || ("main_final_output == 23" && X (true U "main_final_output == 26"))))))))
(false R (! "main_final_output == 21" || (false R (! "main_main___RERS__ == 19" || ("main_final_output == 24" && X (true U "main_final_output == 23"))))))
(false R (! "main_final_output == 23" || (false R (! "main_main___RERS__ == 11" || ("main_final_output == 26" && X (true U "main_final_output == 21"))))))
(false R (! "main_final_output == 24" || ((! (("main_final_output == 25" && ! "main_main___RERS__ == 17") && X (! "main_main___RERS__ == 17" U ("main_final_output == 21" && ! "main_main___RERS__ == 17"))) U ("main_main___RERS__ == 17" || "main_main___RERS__ == 2")) || (false R ! ("main_final_output == 25" && X (true U "main_final_output == 21"))))))
(false R (! "main_final_output == 25" || (("main_main___RERS__ == 2" && (! X (! "main_main___RERS__ == 6" U "main_main___RERS__ == 8") || X (! "main_main___RERS__ == 6" U ("main_main___RERS__ == 8" && (true U "main_final_output == 21"))))) U ("main_main___RERS__ == 6" || (false R ("main_main___RERS__ == 2" && (! X (! "main_main___RERS__ == 6" U "main_main___RERS__ == 8") || X (! "main_main___RERS__ == 6" U ("main_main___RERS__ == 8" && (true U "main_final_output == 21"))))))))))
(false R (! "main_final_output == 26" || ((! (("main_final_output == 21" && ! "main_main___RERS__ == 12") && X (! "main_main___RERS__ == 12" U ("main_final_output == 25" && ! "main_main___RERS__ == 12"))) U ("main_main___RERS__ == 12" || "main_main___RERS__ == 4")) || (false R ! ("main_final_output == 21" && X (true U "main_final_output == 25"))))))
(false R (! "main_main___RERS__ == 1" || (false R (! "main_main___RERS__ == 16" || (true U "main_final_output == 22")))))
(false R (! "main_main___RERS__ == 1" || (false R (! "main_main___RERS__ == 19" || (true U "main_final_output == 25")))))
(false R (! "main_main___RERS__ == 11" || ((! "main_main___RERS__ == 4" || (! "main_main___RERS__ == 15" U ((("main_final_output == 22" && ! "main_main___RERS__ == 15") && ! "main_final_output == 26") && X ((! "main_main___RERS__ == 15" && ! "main_final_output == 26") U "main_final_output == 25")))) U ("main_main___RERS__ == 15" || (false R (! "main_main___RERS__ == 4" || (("main_final_output == 22" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_final_output == 25"))))))))
(false R (! "main_main___RERS__ == 11" || (("main_main___RERS__ == 16" && (! X (! "main_final_output == 24" U "main_main___RERS__ == 3") || X (! "main_final_output == 24" U ("main_main___RERS__ == 3" && (true U "main_final_output == 25"))))) U ("main_final_output == 24" || (false R ("main_main___RERS__ == 16" && (! X (! "main_final_output == 24" U "main_main___RERS__ == 3") || X (! "main_final_output == 24" U ("main_main___RERS__ == 3" && (true U "main_final_output == 25"))))))))))
(false R (! "main_main___RERS__ == 11" || (("main_main___RERS__ == 3" && (! X (! "main_final_output == 25" U "main_main___RERS__ == 13") || X (! "main_final_output == 25" U ("main_main___RERS__ == 13" && (true U "main_final_output == 21"))))) U ("main_final_output == 25" || (false R ("main_main___RERS__ == 3" && (! X (! "main_final_output == 25" U "main_main___RERS__ == 13") || X (! "main_final_output == 25" U ("main_main___RERS__ == 13" && (true U "main_final_output == 21"))))))))))
(false R (! "main_main___RERS__ == 12" || ((! "main_main___RERS__ == 11" || (! "main_main___RERS__ == 3" U (("main_final_output == 26" && ! "main_main___RERS__ == 3") && X (! "main_main___RERS__ == 3" U "main_final_output == 23")))) U ("main_main___RERS__ == 3" || (false R (! "main_main___RERS__ == 11" || ("main_final_output == 26" && X (true U "main_final_output == 23"))))))))
(false R (! "main_main___RERS__ == 18" || ((! "main_main___RERS__ == 2" || (! "main_main___RERS__ == 4" U (("main_final_output == 22" && ! "main_main___RERS__ == 4") && X (! "main_main___RERS__ == 4" U "main_final_output == 26")))) U ("main_main___RERS__ == 4" || (false R (! "main_main___RERS__ == 2" || ("main_final_output == 22" && X (true U "main_final_output == 26"))))))))
(false R (! "main_main___RERS__ == 18" || (false R (! "main_main___RERS__ == 14" || (("main_final_output == 23" && ! "main_final_output == 25") && X (! "main_final_output == 25" U "main_final_output == 26"))))))
(false R (! "main_main___RERS__ == 2" || (! (true U "main_final_output == 24") || (! "main_final_output == 24" U ("main_final_output == 25" || (("main_final_output == 21" && ! "main_final_output == 24") && X (! "main_final_output == 24" U "main_main___RERS__ == 6")))))))
(false R (! "main_main___RERS__ == 2" || ((! "main_main___RERS__ == 17" || (! "main_main___RERS__ == 18" U (("main_final_output == 24" && ! "main_main___RERS__ == 18") && X (! "main_main___RERS__ == 18" U "main_final_output == 21")))) U ("main_main___RERS__ == 18" || (false R (! "main_main___RERS__ == 17" || ("main_final_output == 24" && X (true U "main_final_output == 21"))))))))
(false R (! "main_main___RERS__ == 2" || (true U (("main_final_output == 25" && ! "main_final_output == 23") && X (! "main_final_output == 23" U "main_final_output == 26")))))
(false R (! "main_main___RERS__ == 20" || (! (true U "main_final_output == 22") || (! "main_final_output == 22" U ("main_main___RERS__ == 10" || (("main_main___RERS__ == 12" && ! "main_final_output == 22") && X (! "main_final_output == 22" U "main_main___RERS__ == 18")))))))
(false R (! "main_main___RERS__ == 20" || ((! (("main_final_output == 24" && ! "main_main___RERS__ == 4") && X (! "main_main___RERS__ == 4" U ("main_final_output == 25" && ! "main_main___RERS__ == 4"))) U ("main_main___RERS__ == 4" || "main_final_output == 21")) || (false R ! ("main_final_output == 24" && X (true U "main_final_output == 25"))))))
(false R (! "main_main___RERS__ == 20" || (true U ("main_final_output == 25" && X (true U "main_final_output == 26")))))
(false R (! "main_main___RERS__ == 3" || (! (true U "main_final_output == 25") || (! "main_final_output == 25" U ("main_main___RERS__ == 1" || (("main_final_output == 22" && ! "main_final_output == 25") && X (! "main_final_output == 25" U "main_final_output == 21")))))))
(false R (! "main_main___RERS__ == 3" || (false R (! "main_main___RERS__ == 20" || (true U "main_final_output == 24")))))
(false R (! "main_main___RERS__ == 4" || ((! (("main_final_output == 26" && ! "main_main___RERS__ == 10") && X (! "main_main___RERS__ == 10" U ("main_final_output == 24" && ! "main_main___RERS__ == 10"))) U ("main_main___RERS__ == 10" || "main_main___RERS__ == 15")) || (false R ! ("main_final_output == 26" && X (true U "main_final_output == 24"))))))
(false R (! "main_main___RERS__ == 4" || (("main_main___RERS__ == 18" && (! X (! "main_main___RERS__ == 1" U "main_main___RERS__ == 3") || X (! "main_main___RERS__ == 1" U ("main_main___RERS__ == 3" && (true U "main_final_output == 26"))))) U ("main_main___RERS__ == 1" || (false R ("main_main___RERS__ == 18" && (! X (! "main_main___RERS__ == 1" U "main_main___RERS__ == 3") || X (! "main_main___RERS__ == 1" U ("main_main___RERS__ == 3" && (true U "main_final_output == 26"))))))))))
(false R (! "main_main___RERS__ == 4" || (false R (! "main_main___RERS__ == 17" || ("main_final_output == 25" && X (true U "main_final_output == 26"))))))
(false R (! "main_main___RERS__ == 4" || (false R (! "main_main___RERS__ == 20" || (("main_final_output == 22" && ! "main_final_output == 23") && X (! "main_final_output == 23" U "main_final_output == 26"))))))
(false R (! "main_main___RERS__ == 7" || ((! "main_main___RERS__ == 9" || (! "main_final_output == 24" U ((("main_final_output == 21" && ! "main_final_output == 24") && ! "main_final_output == 26") && X ((! "main_final_output == 24" && ! "main_final_output == 26") U "main_final_output == 25")))) U ("main_final_output == 24" || (false R (! "main_main___RERS__ == 9" || (("main_final_output == 21" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_final_output == 25"))))))))
(false R (! "main_main___RERS__ == 8" || (true U ("main_final_output == 23" && X (true U "main_final_output == 22")))))
(false R (! "main_main___RERS__ == 9" || ((! "main_main___RERS__ == 19" || (! "main_main___RERS__ == 20" U ((("main_final_output == 24" && ! "main_main___RERS__ == 20") && ! "main_final_output == 21") && X ((! "main_main___RERS__ == 20" && ! "main_final_output == 21") U "main_final_output == 23")))) U ("main_main___RERS__ == 20" || (false R (! "main_main___RERS__ == 19" || (("main_final_output == 24" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_final_output == 23"))))))))
(false R (! "main_main___RERS__ == 9" || ((! (("main_final_output == 22" && ! "main_main___RERS__ == 14") && X (! "main_main___RERS__ == 14" U ("main_final_output == 23" && ! "main_main___RERS__ == 14"))) U ("main_main___RERS__ == 14" || "main_main___RERS__ == 1")) || (false R ! ("main_final_output == 22" && X (true U "main_final_output == 23"))))))
(false R (! "main_main___RERS__ == 9" || ((! (("main_final_output == 24" && ! "main_final_output == 21") && X (! "main_final_output == 21" U ("main_final_output == 22" && ! "main_final_output == 21"))) U ("main_final_output == 21" || "main_main___RERS__ == 10")) || (false R ! ("main_final_output == 24" && X (true U "main_final_output == 22"))))))
(false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 17")) || (("main_main___RERS__ == 14" && (! X (! "main_main___RERS__ == 17" U "main_main___RERS__ == 12") || X (! "main_main___RERS__ == 17" U ("main_main___RERS__ == 12" && (true U "main_final_output == 22"))))) U "main_main___RERS__ == 17")))
(false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 2")) || (! (("main_final_output == 22" && ! "main_main___RERS__ == 2") && X (! "main_main___RERS__ == 2" U ("main_final_output == 23" && ! "main_main___RERS__ == 2"))) U ("main_main___RERS__ == 2" || "main_main___RERS__ == 10"))))
(false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 4")) || (! "main_final_output == 23" U ("main_main___RERS__ == 4" || (("main_final_output == 26" && ! "main_final_output == 23") && X (! "main_final_output == 23" U "main_main___RERS__ == 3"))))))
(false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 7")) || (! "main_final_output == 21" U ("main_main___RERS__ == 7" || (("main_main___RERS__ == 20" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_main___RERS__ == 3"))))))
(false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 7")) || ((! "main_main___RERS__ == 18" || (! "main_main___RERS__ == 7" U (("main_final_output == 21" && ! "main_main___RERS__ == 7") && X (! "main_main___RERS__ == 7" U "main_final_output == 25")))) U "main_main___RERS__ == 7")))
(false R (! ("main_main___RERS__ == 10" && (true U "main_main___RERS__ == 1")) || ((! "main_main___RERS__ == 19" || (! "main_main___RERS__ == 1" U (("main_final_output == 25" && ! "main_main___RERS__ == 1") && X (! "main_main___RERS__ == 1" U "main_final_output == 23")))) U "main_main___RERS__ == 1")))
(false R (! ("main_main___RERS__ == 10" && (true U "main_main___RERS__ == 16")) || (("main_main___RERS__ == 14" && (! X (! "main_main___RERS__ == 16" U "main_main___RERS__ == 8") || X (! "main_main___RERS__ == 16" U ("main_main___RERS__ == 8" && (true U "main_final_output == 24"))))) U "main_main___RERS__ == 16")))
(false R (! ("main_main___RERS__ == 13" && (true U "main_final_output == 22")) || (! "main_final_output == 26" U ("main_final_output == 22" || (("main_main___RERS__ == 1" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_main___RERS__ == 2"))))))
(false R (! ("main_main___RERS__ == 13" && (true U "main_main___RERS__ == 1")) || ((! "main_main___RERS__ == 16" || (! "main_main___RERS__ == 1" U (("main_final_output == 21" && ! "main_main___RERS__ == 1") && X (! "main_main___RERS__ == 1" U "main_final_output == 25")))) U "main_main___RERS__ == 1")))
(false R (! ("main_main___RERS__ == 14" && (true U "main_final_output == 21")) || ((! "main_main___RERS__ == 16" || (! "main_final_output == 21" U (("main_final_output == 26" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_final_output == 23")))) U "main_final_output == 21")))
(false R (! ("main_main___RERS__ == 16" && (true U "main_main___RERS__ == 9")) || ((! "main_main___RERS__ == 4" || (! "main_main___RERS__ == 9" U ((("main_final_output == 25" && ! "main_main___RERS__ == 9") && ! "main_final_output == 26") && X ((! "main_main___RERS__ == 9" && ! "main_final_output == 26") U "main_final_output == 24")))) U "main_main___RERS__ == 9")))
(false R (! ("main_main___RERS__ == 18" && (true U "main_main___RERS__ == 19")) || ((! "main_main___RERS__ == 9" || (! "main_main___RERS__ == 19" U ((("main_final_output == 24" && ! "main_main___RERS__ == 19") && ! "main_final_output == 23") && X ((! "main_main___RERS__ == 19" && ! "main_final_output == 23") U "main_final_output == 26")))) U "main_main___RERS__ == 19")))
(false R (! ("main_main___RERS__ == 19" && (true U "main_main___RERS__ == 11")) || (! "main_final_output == 26" U ("main_main___RERS__ == 11" || (("main_main___RERS__ == 17" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_final_output == 21"))))))
(false R (! ("main_main___RERS__ == 19" && (true U "main_main___RERS__ == 7")) || ((! "main_main___RERS__ == 20" || (! "main_main___RERS__ == 7" U (("main_final_output == 24" && ! "main_main___RERS__ == 7") && X (! "main_main___RERS__ == 7" U "main_final_output == 21")))) U "main_main___RERS__ == 7")))
(false R (! ("main_main___RERS__ == 19" && (true U "main_main___RERS__ == 8")) || (("main_main___RERS__ == 7" && (! X (! "main_main___RERS__ == 8" U "main_main___RERS__ == 18") || X (! "main_main___RERS__ == 8" U ("main_main___RERS__ == 18" && (true U "main_final_output == 21"))))) U "main_main___RERS__ == 8")))
(false R (! ("main_main___RERS__ == 2" && (true U "main_main___RERS__ == 3")) || (! "main_final_output == 22" U ("main_main___RERS__ == 3" || (("main_main___RERS__ == 4" && ! "main_final_output == 22") && X (! "main_final_output == 22" U "main_main___RERS__ == 12"))))))
(false R (! ("main_main___RERS__ == 5" && (true U "main_main___RERS__ == 18")) || ((! "main_main___RERS__ == 14" || (! "main_main___RERS__ == 18" U (("main_final_output == 22" && ! "main_main___RERS__ == 18") && X (! "main_main___RERS__ == 18" U "main_final_output == 21")))) U "main_main___RERS__ == 18")))
(false R (! ("main_main___RERS__ == 5" && (true U "main_main___RERS__ == 19")) || ((! "main_main___RERS__ == 15" || (! "main_main___RERS__ == 19" U ((("main_final_output == 24" && ! "main_main___RERS__ == 19") && ! "main_final_output == 22") && X ((! "main_main___RERS__ == 19" && ! "main_final_output == 22") U "main_final_output == 23")))) U "main_main___RERS__ == 19")))
(false R (! ("main_main___RERS__ == 6" && (true U "main_main___RERS__ == 3")) || (! "main_final_output == 21" U ("main_main___RERS__ == 3" || (("main_main___RERS__ == 16" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_main___RERS__ == 18"))))))
(false R (! ("main_main___RERS__ == 8" && (true U "main_main___RERS__ == 10")) || ((! "main_main___RERS__ == 11" || (! "main_main___RERS__ == 10" U ((("main_final_output == 26" && ! "main_main___RERS__ == 10") && ! "main_final_output == 22") && X ((! "main_main___RERS__ == 10" && ! "main_final_output == 22") U "main_final_output == 21")))) U "main_main___RERS__ == 10")))
(false R (! (("main_final_output == 21" && ! "main_main___RERS__ == 16") && (true U "main_main___RERS__ == 16")) || (! "main_final_output == 24" U ("main_main___RERS__ == 2" || "main_main___RERS__ == 16"))))
(false R (! (("main_final_output == 25" && ! "main_main___RERS__ == 6") && (true U "main_main___RERS__ == 6")) || ((! "main_main___RERS__ == 18" || (! "main_main___RERS__ == 6" U ("main_final_output == 21" && ! "main_main___RERS__ == 6"))) U "main_main___RERS__ == 6")))
(false R (! (("main_main___RERS__ == 1" && ! "main_main___RERS__ == 12") && (true U "main_main___RERS__ == 12")) || ((! "main_main___RERS__ == 7" || (! "main_main___RERS__ == 12" U ("main_final_output == 23" && ! "main_main___RERS__ == 12"))) U "main_main___RERS__ == 12")))
(false R (! (("main_main___RERS__ == 18" && ! "main_main___RERS__ == 9") && (true U "main_main___RERS__ == 9")) || ((! "main_main___RERS__ == 15" || (! "main_main___RERS__ == 9" U ("main_final_output == 22" && ! "main_main___RERS__ == 9"))) U "main_main___RERS__ == 9")))
(false R (! (("main_main___RERS__ == 5" && ! "main_final_output == 24") && (true U "main_final_output == 24")) || ((! "main_main___RERS__ == 2" || (! "main_final_output == 24" U ("main_final_output == 22" && ! "main_final_output == 24"))) U "main_final_output == 24")))
(false R (! (("main_main___RERS__ == 7" && ! "main_main___RERS__ == 1") && (true U "main_main___RERS__ == 1")) || ((! "main_main___RERS__ == 19" || (! "main_main___RERS__ == 1" U ("main_final_output == 21" && ! "main_main___RERS__ == 1"))) U "main_main___RERS__ == 1")))
(false R ("main_main___RERS__ == 16" && (! X (true U "main_main___RERS__ == 7") || X (true U ("main_main___RERS__ == 7" && (true U "main_final_output == 26"))))))
! (! "main_final_output == 21" W "main_main___RERS__ == 8")
! (! "main_final_output == 22" W "main_main___RERS__ == 4")
! (! "main_final_output == 24" W "main_final_output == 23")
! (! (true U "main_final_output == 21") || (! "main_final_output == 21" U (("main_main___RERS__ == 3" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_main___RERS__ == 7"))))
! (! (true U "main_final_output == 22") || (! (("main_final_output == 24" && ! "main_final_output == 22") && X (! "main_final_output == 22" U ("main_final_output == 21" && ! "main_final_output == 22"))) U ("main_final_output == 22" || "main_main___RERS__ == 3")))
! (! (true U "main_final_output == 22") || ((! "main_main___RERS__ == 17" || (! "main_final_output == 22" U (("main_final_output == 21" && ! "main_final_output == 22") && X (! "main_final_output == 22" U "main_final_output == 25")))) U "main_final_output == 22"))
! (! (true U "main_final_output == 24") || (! "main_final_output == 23" U ("main_final_output == 24" || (("main_main___RERS__ == 14" && ! "main_final_output == 23") && X (! "main_final_output == 23" U "main_main___RERS__ == 12")))))
! (! (true U "main_final_output == 24") || (! "main_final_output == 24" U (("main_final_output == 25" && ! "main_final_output == 24") && X (! "main_final_output == 24" U "main_final_output == 26"))))
! (! (true U "main_final_output == 25") || (! (("main_final_output == 23" && ! "main_final_output == 25") && X (! "main_final_output == 25" U ("main_final_output == 26" && ! "main_final_output == 25"))) U ("main_final_output == 25" || "main_main___RERS__ == 10")))
! (! (true U "main_final_output == 26") || (! "main_final_output == 26" U (("main_final_output == 21" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_main___RERS__ == 20"))))
! (! (true U "main_main___RERS__ == 1") || ((! "main_main___RERS__ == 19" || (! "main_main___RERS__ == 1" U ((("main_final_output == 26" && ! "main_main___RERS__ == 1") && ! "main_final_output == 25") && X ((! "main_main___RERS__ == 1" && ! "main_final_output == 25") U "main_final_output == 23")))) U "main_main___RERS__ == 1"))
! (! (true U "main_main___RERS__ == 1") || (("main_main___RERS__ == 7" && (! X (! "main_main___RERS__ == 1" U "main_main___RERS__ == 20") || X (! "main_main___RERS__ == 1" U ("main_main___RERS__ == 20" && (true U "main_final_output == 21"))))) U "main_main___RERS__ == 1"))
! (! (true U "main_main___RERS__ == 17") || (! "main_final_output == 26" U ("main_main___RERS__ == 20" || "main_main___RERS__ == 17")))
! (! (true U "main_main___RERS__ == 17") || (! (("main_final_output == 22" && ! "main_main___RERS__ == 17") && X (! "main_main___RERS__ == 17" U ("main_final_output == 23" && ! "main_main___RERS__ == 17"))) U ("main_main___RERS__ == 17" || "main_main___RERS__ == 12")))
! (! (true U "main_main___RERS__ == 18") || ((! "main_main___RERS__ == 10" || (! "main_main___RERS__ == 18" U (("main_final_output == 21" && ! "main_main___RERS__ == 18") && X (! "main_main___RERS__ == 18" U "main_final_output == 25")))) U "main_main___RERS__ == 18"))
! (! (true U "main_main___RERS__ == 19") || ((! "main_main___RERS__ == 14" || (! "main_main___RERS__ == 19" U (("main_final_output == 24" && ! "main_main___RERS__ == 19") && X (! "main_main___RERS__ == 19" U "main_final_output == 26")))) U "main_main___RERS__ == 19"))
! (! (true U "main_main___RERS__ == 3") || (! "main_final_output == 22" U ("main_main___RERS__ == 3" || (("main_main___RERS__ == 6" && ! "main_final_output == 22") && X (! "main_final_output == 22" U "main_main___RERS__ == 1")))))
! (! (true U "main_main___RERS__ == 3") || (("main_main___RERS__ == 13" && (! X (! "main_main___RERS__ == 3" U "main_main___RERS__ == 9") || X (! "main_main___RERS__ == 3" U ("main_main___RERS__ == 9" && (true U "main_final_output == 23"))))) U "main_main___RERS__ == 3"))
! (! (true U "main_main___RERS__ == 5") || ((! "main_main___RERS__ == 13" || (! "main_main___RERS__ == 5" U (("main_final_output == 24" && ! "main_main___RERS__ == 5") && X (! "main_main___RERS__ == 5" U "main_final_output == 26")))) U "main_main___RERS__ == 5"))
! (! (true U "main_main___RERS__ == 5") || (("main_main___RERS__ == 4" && (! X (! "main_main___RERS__ == 5" U "main_main___RERS__ == 6") || X (! "main_main___RERS__ == 5" U ("main_main___RERS__ == 6" && (true U "main_final_output == 24"))))) U "main_main___RERS__ == 5"))
! (! (true U "main_main___RERS__ == 6") || ((! "main_main___RERS__ == 11" || (! "main_main___RERS__ == 6" U (("main_final_output == 26" && ! "main_main___RERS__ == 6") && X (! "main_main___RERS__ == 6" U "main_final_output == 25")))) U "main_main___RERS__ == 6"))
! (! (true U "main_main___RERS__ == 7") || (! "main_final_output == 24" U ("main_main___RERS__ == 7" || (("main_main___RERS__ == 4" && ! "main_final_output == 24") && X (! "main_final_output == 24" U "main_main___RERS__ == 1")))))
! (! (true U "main_main___RERS__ == 7") || ((! "main_main___RERS__ == 20" || (! "main_main___RERS__ == 7" U (("main_final_output == 21" && ! "main_main___RERS__ == 7") && X (! "main_main___RERS__ == 7" U "main_final_output == 26")))) U "main_main___RERS__ == 7"))
! (! (true U "main_main___RERS__ == 7") || ((! "main_main___RERS__ == 20" || (! "main_main___RERS__ == 7" U ((("main_final_output == 23" && ! "main_main___RERS__ == 7") && ! "main_final_output == 26") && X ((! "main_main___RERS__ == 7" && ! "main_final_output == 26") U "main_final_output == 22")))) U "main_main___RERS__ == 7"))
! (! (true U "main_main___RERS__ == 9") || ((! "main_main___RERS__ == 6" || (! "main_main___RERS__ == 9" U ("main_final_output == 25" && ! "main_main___RERS__ == 9"))) U "main_main___RERS__ == 9"))
! (! (true U "main_main___RERS__ == 9") || (("main_main___RERS__ == 16" && (! X (! "main_main___RERS__ == 9" U "main_main___RERS__ == 18") || X (! "main_main___RERS__ == 9" U ("main_main___RERS__ == 18" && (true U "main_final_output == 23"))))) U "main_main___RERS__ == 9"))
! (! (true U ("main_final_output == 21" && X (true U "main_final_output == 24"))) || (! "main_final_output == 21" U "main_main___RERS__ == 15"))
! (! (true U ("main_final_output == 22" && X (true U "main_final_output == 25"))) || (! "main_final_output == 22" U "main_main___RERS__ == 16"))
! (! (true U ("main_final_output == 23" && X (true U "main_final_output == 22"))) || (! "main_final_output == 23" U "main_final_output == 24"))
! (! (true U ("main_final_output == 24" && X (true U "main_final_output == 21"))) || (! "main_final_output == 24" U "main_main___RERS__ == 5"))
! (! (true U ("main_final_output == 24" && X (true U "main_final_output == 23"))) || (! "main_final_output == 24" U "main_main___RERS__ == 15"))
! (! (true U ("main_final_output == 24" && X (true U "main_final_output == 25"))) || (! "main_final_output == 24" U "main_main___RERS__ == 17"))
! (! (true U ("main_final_output == 26" && X (true U "main_final_output == 23"))) || (! "main_final_output == 26" U "main_main___RERS__ == 14"))
! ((false R ! "main_final_output == 23") || (true U ("main_final_output == 23" && (! "main_final_output == 25" W "main_main___RERS__ == 2"))))
! ((false R ! "main_final_output == 26") || (true U ("main_final_output == 26" && (! "main_final_output == 24" W "main_main___RERS__ == 15"))))
! ((false R ! "main_main___RERS__ == 13") || (! "main_main___RERS__ == 13" U ("main_main___RERS__ == 13" && (! (true U ("main_final_output == 23" && X (true U "main_final_output == 21"))) || (! "main_final_output == 23" U "main_main___RERS__ == 1")))))
! ((false R ! "main_main___RERS__ == 15") || (true U ("main_main___RERS__ == 15" && (! "main_final_output == 21" W "main_main___RERS__ == 6"))))
! ((false R ! "main_main___RERS__ == 16") || (! "main_main___RERS__ == 16" U ("main_main___RERS__ == 16" && (! (true U ("main_final_output == 25" && X (true U "main_final_output == 23"))) || (! "main_final_output == 25" U "main_main___RERS__ == 7")))))
! ((false R ! "main_main___RERS__ == 17") || (true U ("main_main___RERS__ == 17" && (! "main_final_output == 23" W "main_main___RERS__ == 13"))))
! ((false R ! "main_main___RERS__ == 2") || (! "main_main___RERS__ == 2" U ("main_main___RERS__ == 2" && (! (true U "main_final_output == 25") || (! "main_final_output == 25" U (("main_main___RERS__ == 18" && ! "main_final_output == 25") && X (! "main_final_output == 25" U "main_main___RERS__ == 6")))))))
! ((false R ! "main_main___RERS__ == 3") || (! "main_main___RERS__ == 3" U ("main_main___RERS__ == 3" && (! (true U ("main_final_output == 24" && X (true U "main_final_output == 22"))) || (! "main_final_output == 24" U "main_main___RERS__ == 10")))))
! ((false R ! "main_main___RERS__ == 6") || (! "main_main___RERS__ == 6" U ("main_main___RERS__ == 6" && (! (true U "main_final_output == 25") || (! "main_final_output == 25" U (("main_main___RERS__ == 16" && ! "main_final_output == 25") && X (! "main_final_output == 25" U "main_main___RERS__ == 4")))))))
! (false R (! "main_final_output == 21" || ((! "main_main___RERS__ == 15" || (! "main_main___RERS__ == 12" U (("main_final_output == 23" && ! "main_main___RERS__ == 12") && X (! "main_main___RERS__ == 12" U "main_final_output == 26")))) U ("main_main___RERS__ == 12" || (false R (! "main_main___RERS__ == 15" || ("main_final_output == 23" && X (true U "main_final_output == 26"))))))))
! (false R (! "main_final_output == 21" || (false R (! "main_main___RERS__ == 19" || ("main_final_output == 24" && X (true U "main_final_output == 23"))))))
! (false R (! "main_final_output == 23" || (false R (! "main_main___RERS__ == 11" || ("main_final_output == 26" && X (true U "main_final_output == 21"))))))
! (false R (! "main_final_output == 24" || ((! (("main_final_output == 25" && ! "main_main___RERS__ == 17") && X (! "main_main___RERS__ == 17" U ("main_final_output == 21" && ! "main_main___RERS__ == 17"))) U ("main_main___RERS__ == 17" || "main_main___RERS__ == 2")) || (false R ! ("main_final_output == 25" && X (true U "main_final_output == 21"))))))
! (false R (! "main_final_output == 25" || (("main_main___RERS__ == 2" && (! X (! "main_main___RERS__ == 6" U "main_main___RERS__ == 8") || X (! "main_main___RERS__ == 6" U ("main_main___RERS__ == 8" && (true U "main_final_output == 21"))))) U ("main_main___RERS__ == 6" || (false R ("main_main___RERS__ == 2" && (! X (! "main_main___RERS__ == 6" U "main_main___RERS__ == 8") || X (! "main_main___RERS__ == 6" U ("main_main___RERS__ == 8" && (true U "main_final_output == 21"))))))))))
! (false R (! "main_final_output == 26" || ((! (("main_final_output == 21" && ! "main_main___RERS__ == 12") && X (! "main_main___RERS__ == 12" U ("main_final_output == 25" && ! "main_main___RERS__ == 12"))) U ("main_main___RERS__ == 12" || "main_main___RERS__ == 4")) || (false R ! ("main_final_output == 21" && X (true U "main_final_output == 25"))))))
! (false R (! "main_main___RERS__ == 1" || (false R (! "main_main___RERS__ == 16" || (true U "main_final_output == 22")))))
! (false R (! "main_main___RERS__ == 1" || (false R (! "main_main___RERS__ == 19" || (true U "main_final_output == 25")))))
! (false R (! "main_main___RERS__ == 11" || ((! "main_main___RERS__ == 4" || (! "main_main___RERS__ == 15" U ((("main_final_output == 22" && ! "main_main___RERS__ == 15") && ! "main_final_output == 26") && X ((! "main_main___RERS__ == 15" && ! "main_final_output == 26") U "main_final_output == 25")))) U ("main_main___RERS__ == 15" || (false R (! "main_main___RERS__ == 4" || (("main_final_output == 22" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_final_output == 25"))))))))
! (false R (! "main_main___RERS__ == 11" || (("main_main___RERS__ == 16" && (! X (! "main_final_output == 24" U "main_main___RERS__ == 3") || X (! "main_final_output == 24" U ("main_main___RERS__ == 3" && (true U "main_final_output == 25"))))) U ("main_final_output == 24" || (false R ("main_main___RERS__ == 16" && (! X (! "main_final_output == 24" U "main_main___RERS__ == 3") || X (! "main_final_output == 24" U ("main_main___RERS__ == 3" && (true U "main_final_output == 25"))))))))))
! (false R (! "main_main___RERS__ == 11" || (("main_main___RERS__ == 3" && (! X (! "main_final_output == 25" U "main_main___RERS__ == 13") || X (! "main_final_output == 25" U ("main_main___RERS__ == 13" && (true U "main_final_output == 21"))))) U ("main_final_output == 25" || (false R ("main_main___RERS__ == 3" && (! X (! "main_final_output == 25" U "main_main___RERS__ == 13") || X (! "main_final_output == 25" U ("main_main___RERS__ == 13" && (true U "main_final_output == 21"))))))))))
! (false R (! "main_main___RERS__ == 12" || ((! "main_main___RERS__ == 11" || (! "main_main___RERS__ == 3" U (("main_final_output == 26" && ! "main_main___RERS__ == 3") && X (! "main_main___RERS__ == 3" U "main_final_output == 23")))) U ("main_main___RERS__ == 3" || (false R (! "main_main___RERS__ == 11" || ("main_final_output == 26" && X (true U "main_final_output == 23"))))))))
! (false R (! "main_main___RERS__ == 18" || ((! "main_main___RERS__ == 2" || (! "main_main___RERS__ == 4" U (("main_final_output == 22" && ! "main_main___RERS__ == 4") && X (! "main_main___RERS__ == 4" U "main_final_output == 26")))) U ("main_main___RERS__ == 4" || (false R (! "main_main___RERS__ == 2" || ("main_final_output == 22" && X (true U "main_final_output == 26"))))))))
! (false R (! "main_main___RERS__ == 18" || (false R (! "main_main___RERS__ == 14" || (("main_final_output == 23" && ! "main_final_output == 25") && X (! "main_final_output == 25" U "main_final_output == 26"))))))
! (false R (! "main_main___RERS__ == 2" || (! (true U "main_final_output == 24") || (! "main_final_output == 24" U ("main_final_output == 25" || (("main_final_output == 21" && ! "main_final_output == 24") && X (! "main_final_output == 24" U "main_main___RERS__ == 6")))))))
! (false R (! "main_main___RERS__ == 2" || ((! "main_main___RERS__ == 17" || (! "main_main___RERS__ == 18" U (("main_final_output == 24" && ! "main_main___RERS__ == 18") && X (! "main_main___RERS__ == 18" U "main_final_output == 21")))) U ("main_main___RERS__ == 18" || (false R (! "main_main___RERS__ == 17" || ("main_final_output == 24" && X (true U "main_final_output == 21"))))))))
! (false R (! "main_main___RERS__ == 2" || (true U (("main_final_output == 25" && ! "main_final_output == 23") && X (! "main_final_output == 23" U "main_final_output == 26")))))
! (false R (! "main_main___RERS__ == 20" || (! (true U "main_final_output == 22") || (! "main_final_output == 22" U ("main_main___RERS__ == 10" || (("main_main___RERS__ == 12" && ! "main_final_output == 22") && X (! "main_final_output == 22" U "main_main___RERS__ == 18")))))))
! (false R (! "main_main___RERS__ == 20" || ((! (("main_final_output == 24" && ! "main_main___RERS__ == 4") && X (! "main_main___RERS__ == 4" U ("main_final_output == 25" && ! "main_main___RERS__ == 4"))) U ("main_main___RERS__ == 4" || "main_final_output == 21")) || (false R ! ("main_final_output == 24" && X (true U "main_final_output == 25"))))))
! (false R (! "main_main___RERS__ == 20" || (true U ("main_final_output == 25" && X (true U "main_final_output == 26")))))
! (false R (! "main_main___RERS__ == 3" || (! (true U "main_final_output == 25") || (! "main_final_output == 25" U ("main_main___RERS__ == 1" || (("main_final_output == 22" && ! "main_final_output == 25") && X (! "main_final_output == 25" U "main_final_output == 21")))))))
! (false R (! "main_main___RERS__ == 3" || (false R (! "main_main___RERS__ == 20" || (true U "main_final_output == 24")))))
! (false R (! "main_main___RERS__ == 4" || ((! (("main_final_output == 26" && ! "main_main___RERS__ == 10") && X (! "main_main___RERS__ == 10" U ("main_final_output == 24" && ! "main_main___RERS__ == 10"))) U ("main_main___RERS__ == 10" || "main_main___RERS__ == 15")) || (false R ! ("main_final_output == 26" && X (true U "main_final_output == 24"))))))
! (false R (! "main_main___RERS__ == 4" || (("main_main___RERS__ == 18" && (! X (! "main_main___RERS__ == 1" U "main_main___RERS__ == 3") || X (! "main_main___RERS__ == 1" U ("main_main___RERS__ == 3" && (true U "main_final_output == 26"))))) U ("main_main___RERS__ == 1" || (false R ("main_main___RERS__ == 18" && (! X (! "main_main___RERS__ == 1" U "main_main___RERS__ == 3") || X (! "main_main___RERS__ == 1" U ("main_main___RERS__ == 3" && (true U "main_final_output == 26"))))))))))
! (false R (! "main_main___RERS__ == 4" || (false R (! "main_main___RERS__ == 17" || ("main_final_output == 25" && X (true U "main_final_output == 26"))))))
! (false R (! "main_main___RERS__ == 4" || (false R (! "main_main___RERS__ == 20" || (("main_final_output == 22" && ! "main_final_output == 23") && X (! "main_final_output == 23" U "main_final_output == 26"))))))
! (false R (! "main_main___RERS__ == 7" || ((! "main_main___RERS__ == 9" || (! "main_final_output == 24" U ((("main_final_output == 21" && ! "main_final_output == 24") && ! "main_final_output == 26") && X ((! "main_final_output == 24" && ! "main_final_output == 26") U "main_final_output == 25")))) U ("main_final_output == 24" || (false R (! "main_main___RERS__ == 9" || (("main_final_output == 21" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_final_output == 25"))))))))
! (false R (! "main_main___RERS__ == 8" || (true U ("main_final_output == 23" && X (true U "main_final_output == 22")))))
! (false R (! "main_main___RERS__ == 9" || ((! "main_main___RERS__ == 19" || (! "main_main___RERS__ == 20" U ((("main_final_output == 24" && ! "main_main___RERS__ == 20") && ! "main_final_output == 21") && X ((! "main_main___RERS__ == 20" && ! "main_final_output == 21") U "main_final_output == 23")))) U ("main_main___RERS__ == 20" || (false R (! "main_main___RERS__ == 19" || (("main_final_output == 24" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_final_output == 23"))))))))
! (false R (! "main_main___RERS__ == 9" || ((! (("main_final_output == 22" && ! "main_main___RERS__ == 14") && X (! "main_main___RERS__ == 14" U ("main_final_output == 23" && ! "main_main___RERS__ == 14"))) U ("main_main___RERS__ == 14" || "main_main___RERS__ == 1")) || (false R ! ("main_final_output == 22" && X (true U "main_final_output == 23"))))))
! (false R (! "main_main___RERS__ == 9" || ((! (("main_final_output == 24" && ! "main_final_output == 21") && X (! "main_final_output == 21" U ("main_final_output == 22" && ! "main_final_output == 21"))) U ("main_final_output == 21" || "main_main___RERS__ == 10")) || (false R ! ("main_final_output == 24" && X (true U "main_final_output == 22"))))))
! (false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 17")) || (("main_main___RERS__ == 14" && (! X (! "main_main___RERS__ == 17" U "main_main___RERS__ == 12") || X (! "main_main___RERS__ == 17" U ("main_main___RERS__ == 12" && (true U "main_final_output == 22"))))) U "main_main___RERS__ == 17")))
! (false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 2")) || (! (("main_final_output == 22" && ! "main_main___RERS__ == 2") && X (! "main_main___RERS__ == 2" U ("main_final_output == 23" && ! "main_main___RERS__ == 2"))) U ("main_main___RERS__ == 2" || "main_main___RERS__ == 10"))))
! (false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 4")) || (! "main_final_output == 23" U ("main_main___RERS__ == 4" || (("main_final_output == 26" && ! "main_final_output == 23") && X (! "main_final_output == 23" U "main_main___RERS__ == 3"))))))
! (false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 7")) || (! "main_final_output == 21" U ("main_main___RERS__ == 7" || (("main_main___RERS__ == 20" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_main___RERS__ == 3"))))))
! (false R (! ("main_final_output == 24" && (true U "main_main___RERS__ == 7")) || ((! "main_main___RERS__ == 18" || (! "main_main___RERS__ == 7" U (("main_final_output == 21" && ! "main_main___RERS__ == 7") && X (! "main_main___RERS__ == 7" U "main_final_output == 25")))) U "main_main___RERS__ == 7")))
! (false R (! ("main_main___RERS__ == 10" && (true U "main_main___RERS__ == 1")) || ((! "main_main___RERS__ == 19" || (! "main_main___RERS__ == 1" U (("main_final_output == 25" && ! "main_main___RERS__ == 1") && X (! "main_main___RERS__ == 1" U "main_final_output == 23")))) U "main_main___RERS__ == 1")))
! (false R (! ("main_main___RERS__ == 10" && (true U "main_main___RERS__ == 16")) || (("main_main___RERS__ == 14" && (! X (! "main_main___RERS__ == 16" U "main_main___RERS__ == 8") || X (! "main_main___RERS__ == 16" U ("main_main___RERS__ == 8" && (true U "main_final_output == 24"))))) U "main_main___RERS__ == 16")))
! (false R (! ("main_main___RERS__ == 13" && (true U "main_final_output == 22")) || (! "main_final_output == 26" U ("main_final_output == 22" || (("main_main___RERS__ == 1" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_main___RERS__ == 2"))))))
! (false R (! ("main_main___RERS__ == 13" && (true U "main_main___RERS__ == 1")) || ((! "main_main___RERS__ == 16" || (! "main_main___RERS__ == 1" U (("main_final_output == 21" && ! "main_main___RERS__ == 1") && X (! "main_main___RERS__ == 1" U "main_final_output == 25")))) U "main_main___RERS__ == 1")))
! (false R (! ("main_main___RERS__ == 14" && (true U "main_final_output == 21")) || ((! "main_main___RERS__ == 16" || (! "main_final_output == 21" U (("main_final_output == 26" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_final_output == 23")))) U "main_final_output == 21")))
! (false R (! ("main_main___RERS__ == 16" && (true U "main_main___RERS__ == 9")) || ((! "main_main___RERS__ == 4" || (! "main_main___RERS__ == 9" U ((("main_final_output == 25" && ! "main_main___RERS__ == 9") && ! "main_final_output == 26") && X ((! "main_main___RERS__ == 9" && ! "main_final_output == 26") U "main_final_output == 24")))) U "main_main___RERS__ == 9")))
! (false R (! ("main_main___RERS__ == 18" && (true U "main_main___RERS__ == 19")) || ((! "main_main___RERS__ == 9" || (! "main_main___RERS__ == 19" U ((("main_final_output == 24" && ! "main_main___RERS__ == 19") && ! "main_final_output == 23") && X ((! "main_main___RERS__ == 19" && ! "main_final_output == 23") U "main_final_output == 26")))) U "main_main___RERS__ == 19")))
! (false R (! ("main_main___RERS__ == 19" && (true U "main_main___RERS__ == 11")) || (! "main_final_output == 26" U ("main_main___RERS__ == 11" || (("main_main___RERS__ == 17" && ! "main_final_output == 26") && X (! "main_final_output == 26" U "main_final_output == 21"))))))
! (false R (! ("main_main___RERS__ == 19" && (true U "main_main___RERS__ == 7")) || ((! "main_main___RERS__ == 20" || (! "main_main___RERS__ == 7" U (("main_final_output == 24" && ! "main_main___RERS__ == 7") && X (! "main_main___RERS__ == 7" U "main_final_output == 21")))) U "main_main___RERS__ == 7")))
! (false R (! ("main_main___RERS__ == 19" && (true U "main_main___RERS__ == 8")) || (("main_main___RERS__ == 7" && (! X (! "main_main___RERS__ == 8" U "main_main___RERS__ == 18") || X (! "main_main___RERS__ == 8" U ("main_main___RERS__ == 18" && (true U "main_final_output == 21"))))) U "main_main___RERS__ == 8")))
! (false R (! ("main_main___RERS__ == 2" && (true U "main_main___RERS__ == 3")) || (! "main_final_output == 22" U ("main_main___RERS__ == 3" || (("main_main___RERS__ == 4" && ! "main_final_output == 22") && X (! "main_final_output == 22" U "main_main___RERS__ == 12"))))))
! (false R (! ("main_main___RERS__ == 5" && (true U "main_main___RERS__ == 18")) || ((! "main_main___RERS__ == 14" || (! "main_main___RERS__ == 18" U (("main_final_output == 22" && ! "main_main___RERS__ == 18") && X (! "main_main___RERS__ == 18" U "main_final_output == 21")))) U "main_main___RERS__ == 18")))
! (false R (! ("main_main___RERS__ == 5" && (true U "main_main___RERS__ == 19")) || ((! "main_main___RERS__ == 15" || (! "main_main___RERS__ == 19" U ((("main_final_output == 24" && ! "main_main___RERS__ == 19") && ! "main_final_output == 22") && X ((! "main_main___RERS__ == 19" && ! "main_final_output == 22") U "main_final_output == 23")))) U "main_main___RERS__ == 19")))
! (false R (! ("main_main___RERS__ == 6" && (true U "main_main___RERS__ == 3")) || (! "main_final_output == 21" U ("main_main___RERS__ == 3" || (("main_main___RERS__ == 16" && ! "main_final_output == 21") && X (! "main_final_output == 21" U "main_main___RERS__ == 18"))))))
! (false R (! ("main_main___RERS__ == 8" && (true U "main_main___RERS__ == 10")) || ((! "main_main___RERS__ == 11" || (! "main_main___RERS__ == 10" U ((("main_final_output == 26" && ! "main_main___RERS__ == 10") && ! "main_final_output == 22") && X ((! "main_main___RERS__ == 10" && ! "main_final_output == 22") U "main_final_output == 21")))) U "main_main___RERS__ == 10")))
! (false R (! (("main_final_output == 21" && ! "main_main___RERS__ == 16") && (true U "main_main___RERS__ == 16")) || (! "main_final_output == 24" U ("main_main___RERS__ == 2" || "main_main___RERS__ == 16"))))
! (false R (! (("main_final_output == 25" && ! "main_main___RERS__ == 6") && (true U "main_main___RERS__ == 6")) || ((! "main_main___RERS__ == 18" || (! "main_main___RERS__ == 6" U ("main_final_output == 21" && ! "main_main___RERS__ == 6"))) U "main_main___RERS__ == 6")))
! (false R (! (("main_main___RERS__ == 1" && ! "main_main___RERS__ == 12") && (true U "main_main___RERS__ == 12")) || ((! "main_main___RERS__ == 7" || (! "main_main___RERS__ == 12" U ("main_final_output == 23" && ! "main_main___RERS__ == 12"))) U "main_main___RERS__ == 12")))
! (false R (! (("main_main___RERS__ == 18" && ! "main_main___RERS__ == 9") && (true U "main_main___RERS__ == 9")) || ((! "main_main___RERS__ == 15" || (! "main_main___RERS__ == 9" U ("main_final_output == 22" && ! "main_main___RERS__ == 9"))) U "main_main___RERS__ == 9")))
! (false R (! (("main_main___RERS__ == 5" && ! "main_final_output == 24") && (true U "main_final_output == 24")) || ((! "main_main___RERS__ == 2" || (! "main_final_output == 24" U ("main_final_output == 22" && ! "main_final_output == 24"))) U "main_final_output == 24")))
! (false R (! (("main_main___RERS__ == 7" && ! "main_main___RERS__ == 1") && (true U "main_main___RERS__ == 1")) || ((! "main_main___RERS__ == 19" || (! "main_main___RERS__ == 1" U ("main_final_output == 21" && ! "main_main___RERS__ == 1"))) U "main_main___RERS__ == 1")))
! (false R ("main_main___RERS__ == 16" && (! X (true U "main_main___RERS__ == 7") || X (true U ("main_main___RERS__ == 7" && (true U "main_final_output == 26"))))))