z3.log

[tool-version] Z3 4.12.1
[mk-app] #1 true
[mk-app] #2 false
[mk-app] #1 true
[mk-app] #2 false
[mk-app] #3 pi
[mk-app] #4 euler
[mk-app] #5 x0
[mk-app] #6 x1
[mk-app] #7 x2
[mk-app] #8 x3
[mk-app] #9 x4
[mk-app] #10 y0
[mk-app] #11 y1
[mk-app] #12 y2
[mk-app] #13 y3
[mk-app] #14 y4
[mk-app] #15 Int
[attach-meaning] #15 arith 0
[mk-app] #16 >= #5 #15
[mk-app] #17 bv
[attach-meaning] #17 bv #b1
[mk-app] #18 bv
[attach-meaning] #18 bv #b0
[attach-meaning] #17 bv #b1
[attach-meaning] #18 bv #b0
[attach-meaning] #18 bv #b0
[mk-var] #19 0
[mk-var] #20 1
[mk-var] #21 2
[mk-var] #22 3
[mk-var] #23 4
[mk-var] #24 5
[mk-var] #25 6
[mk-var] #26 7
[mk-var] #27 8
[mk-var] #28 9
[mk-var] #29 10
[mk-var] #30 11
[mk-var] #31 12
[mk-var] #32 13
[mk-var] #33 14
[mk-app] #34 + #27 #25
[attach-enode] #1 0
[attach-enode] #2 0
[mk-app] #35 Int
[attach-meaning] #35 arith 10
[mk-app] #36 < #5 #35
[mk-app] #37 <= #35 #5
[mk-app] #38 not #37
[inst-discovered] theory-solving 0x0 arith# ; #36
[mk-app] #39 = #36 #38
[instance] 0x0 #39
[attach-enode] #39 0
[end-of-instance]
[mk-app] #39 Int
[attach-meaning] #39 arith (- 1)
[mk-app] #40 * #39 #5
[mk-app] #41 Int
[attach-meaning] #41 arith (- 10)
[mk-app] #42 >= #5 #35
[inst-discovered] theory-solving 0x0 arith# ; #37
[mk-app] #39 = #37 #42
[instance] 0x0 #39
[attach-enode] #39 0
[end-of-instance]
[mk-app] #39 not #42
[mk-app] #40 >= #10 #15
[mk-app] #41 < #10 #35
[mk-app] #43 <= #35 #10
[mk-app] #44 not #43
[inst-discovered] theory-solving 0x0 arith# ; #41
[mk-app] #45 = #41 #44
[instance] 0x0 #45
[attach-enode] #45 0
[end-of-instance]
[mk-app] #45 Int
[attach-meaning] #45 arith (- 1)
[mk-app] #46 * #45 #10
[mk-app] #47 Int
[attach-meaning] #47 arith (- 10)
[mk-app] #48 >= #10 #35
[inst-discovered] theory-solving 0x0 arith# ; #43
[mk-app] #45 = #43 #48
[instance] 0x0 #45
[attach-enode] #45 0
[end-of-instance]
[mk-app] #45 not #48
[mk-app] #46 >= #6 #15
[mk-app] #47 < #6 #35
[mk-app] #49 <= #35 #6
[mk-app] #50 not #49
[inst-discovered] theory-solving 0x0 arith# ; #47
[mk-app] #51 = #47 #50
[instance] 0x0 #51
[attach-enode] #51 0
[end-of-instance]
[mk-app] #51 Int
[attach-meaning] #51 arith (- 1)
[mk-app] #52 * #51 #6
[mk-app] #53 Int
[attach-meaning] #53 arith (- 10)
[mk-app] #54 >= #6 #35
[inst-discovered] theory-solving 0x0 arith# ; #49
[mk-app] #51 = #49 #54
[instance] 0x0 #51
[attach-enode] #51 0
[end-of-instance]
[mk-app] #51 not #54
[mk-app] #52 >= #11 #15
[mk-app] #53 < #11 #35
[mk-app] #55 <= #35 #11
[mk-app] #56 not #55
[inst-discovered] theory-solving 0x0 arith# ; #53
[mk-app] #57 = #53 #56
[instance] 0x0 #57
[attach-enode] #57 0
[end-of-instance]
[mk-app] #57 Int
[attach-meaning] #57 arith (- 1)
[mk-app] #58 * #57 #11
[mk-app] #59 Int
[attach-meaning] #59 arith (- 10)
[mk-app] #60 >= #11 #35
[inst-discovered] theory-solving 0x0 arith# ; #55
[mk-app] #57 = #55 #60
[instance] 0x0 #57
[attach-enode] #57 0
[end-of-instance]
[mk-app] #57 not #60
[mk-app] #58 >= #7 #15
[mk-app] #59 < #7 #35
[mk-app] #61 <= #35 #7
[mk-app] #62 not #61
[inst-discovered] theory-solving 0x0 arith# ; #59
[mk-app] #63 = #59 #62
[instance] 0x0 #63
[attach-enode] #63 0
[end-of-instance]
[mk-app] #63 Int
[attach-meaning] #63 arith (- 1)
[mk-app] #64 * #63 #7
[mk-app] #65 Int
[attach-meaning] #65 arith (- 10)
[mk-app] #66 >= #7 #35
[inst-discovered] theory-solving 0x0 arith# ; #61
[mk-app] #63 = #61 #66
[instance] 0x0 #63
[attach-enode] #63 0
[end-of-instance]
[mk-app] #63 not #66
[mk-app] #64 >= #12 #15
[mk-app] #65 < #12 #35
[mk-app] #67 <= #35 #12
[mk-app] #68 not #67
[inst-discovered] theory-solving 0x0 arith# ; #65
[mk-app] #69 = #65 #68
[instance] 0x0 #69
[attach-enode] #69 0
[end-of-instance]
[mk-app] #69 Int
[attach-meaning] #69 arith (- 1)
[mk-app] #70 * #69 #12
[mk-app] #71 Int
[attach-meaning] #71 arith (- 10)
[mk-app] #72 >= #12 #35
[inst-discovered] theory-solving 0x0 arith# ; #67
[mk-app] #69 = #67 #72
[instance] 0x0 #69
[attach-enode] #69 0
[end-of-instance]
[mk-app] #69 not #72
[mk-app] #70 >= #8 #15
[mk-app] #71 < #8 #35
[mk-app] #73 <= #35 #8
[mk-app] #74 not #73
[inst-discovered] theory-solving 0x0 arith# ; #71
[mk-app] #75 = #71 #74
[instance] 0x0 #75
[attach-enode] #75 0
[end-of-instance]
[mk-app] #75 Int
[attach-meaning] #75 arith (- 1)
[mk-app] #76 * #75 #8
[mk-app] #77 Int
[attach-meaning] #77 arith (- 10)
[mk-app] #78 >= #8 #35
[inst-discovered] theory-solving 0x0 arith# ; #73
[mk-app] #75 = #73 #78
[instance] 0x0 #75
[attach-enode] #75 0
[end-of-instance]
[mk-app] #75 not #78
[mk-app] #76 >= #13 #15
[mk-app] #77 < #13 #35
[mk-app] #79 <= #35 #13
[mk-app] #80 not #79
[inst-discovered] theory-solving 0x0 arith# ; #77
[mk-app] #81 = #77 #80
[instance] 0x0 #81
[attach-enode] #81 0
[end-of-instance]
[mk-app] #81 Int
[attach-meaning] #81 arith (- 1)
[mk-app] #82 * #81 #13
[mk-app] #83 Int
[attach-meaning] #83 arith (- 10)
[mk-app] #84 >= #13 #35
[inst-discovered] theory-solving 0x0 arith# ; #79
[mk-app] #81 = #79 #84
[instance] 0x0 #81
[attach-enode] #81 0
[end-of-instance]
[mk-app] #81 not #84
[mk-app] #82 >= #9 #15
[mk-app] #83 < #9 #35
[mk-app] #85 <= #35 #9
[mk-app] #86 not #85
[inst-discovered] theory-solving 0x0 arith# ; #83
[mk-app] #87 = #83 #86
[instance] 0x0 #87
[attach-enode] #87 0
[end-of-instance]
[mk-app] #87 Int
[attach-meaning] #87 arith (- 1)
[mk-app] #88 * #87 #9
[mk-app] #89 Int
[attach-meaning] #89 arith (- 10)
[mk-app] #90 >= #9 #35
[inst-discovered] theory-solving 0x0 arith# ; #85
[mk-app] #87 = #85 #90
[instance] 0x0 #87
[attach-enode] #87 0
[end-of-instance]
[mk-app] #87 not #90
[mk-app] #88 >= #14 #15
[mk-app] #89 < #14 #35
[mk-app] #91 <= #35 #14
[mk-app] #92 not #91
[inst-discovered] theory-solving 0x0 arith# ; #89
[mk-app] #93 = #89 #92
[instance] 0x0 #93
[attach-enode] #93 0
[end-of-instance]
[mk-app] #93 Int
[attach-meaning] #93 arith (- 1)
[mk-app] #94 * #93 #14
[mk-app] #95 Int
[attach-meaning] #95 arith (- 10)
[mk-app] #96 >= #14 #35
[inst-discovered] theory-solving 0x0 arith# ; #91
[mk-app] #93 = #91 #96
[instance] 0x0 #93
[attach-enode] #93 0
[end-of-instance]
[mk-app] #93 not #96
[mk-app] #94 distinct #5 #6
[mk-app] #95 distinct #10 #11
[mk-app] #97 or #94 #95
[mk-app] #98 = #5 #6
[mk-app] #99 not #98
[inst-discovered] theory-solving 0x0 basic# ; #94
[mk-app] #100 = #94 #99
[instance] 0x0 #100
[attach-enode] #100 0
[end-of-instance]
[mk-app] #100 = #10 #11
[mk-app] #101 not #100
[inst-discovered] theory-solving 0x0 basic# ; #95
[mk-app] #102 = #95 #101
[instance] 0x0 #102
[attach-enode] #102 0
[end-of-instance]
[mk-app] #102 or #99 #101
[mk-app] #103 distinct #5 #7
[mk-app] #104 distinct #10 #12
[mk-app] #105 or #103 #104
[mk-app] #106 = #5 #7
[mk-app] #107 not #106
[inst-discovered] theory-solving 0x0 basic# ; #103
[mk-app] #108 = #103 #107
[instance] 0x0 #108
[attach-enode] #108 0
[end-of-instance]
[mk-app] #108 = #10 #12
[mk-app] #109 not #108
[inst-discovered] theory-solving 0x0 basic# ; #104
[mk-app] #110 = #104 #109
[instance] 0x0 #110
[attach-enode] #110 0
[end-of-instance]
[mk-app] #110 or #107 #109
[mk-app] #111 distinct #5 #8
[mk-app] #112 distinct #10 #13
[mk-app] #113 or #111 #112
[mk-app] #114 = #5 #8
[mk-app] #115 not #114
[inst-discovered] theory-solving 0x0 basic# ; #111
[mk-app] #116 = #111 #115
[instance] 0x0 #116
[attach-enode] #116 0
[end-of-instance]
[mk-app] #116 = #10 #13
[mk-app] #117 not #116
[inst-discovered] theory-solving 0x0 basic# ; #112
[mk-app] #118 = #112 #117
[instance] 0x0 #118
[attach-enode] #118 0
[end-of-instance]
[mk-app] #118 or #115 #117
[mk-app] #119 distinct #5 #9
[mk-app] #120 distinct #10 #14
[mk-app] #121 or #119 #120
[mk-app] #122 = #5 #9
[mk-app] #123 not #122
[inst-discovered] theory-solving 0x0 basic# ; #119
[mk-app] #124 = #119 #123
[instance] 0x0 #124
[attach-enode] #124 0
[end-of-instance]
[mk-app] #124 = #10 #14
[mk-app] #125 not #124
[inst-discovered] theory-solving 0x0 basic# ; #120
[mk-app] #126 = #120 #125
[instance] 0x0 #126
[attach-enode] #126 0
[end-of-instance]
[mk-app] #126 or #123 #125
[mk-app] #127 distinct #6 #7
[mk-app] #128 distinct #11 #12
[mk-app] #129 or #127 #128
[mk-app] #130 = #6 #7
[mk-app] #131 not #130
[inst-discovered] theory-solving 0x0 basic# ; #127
[mk-app] #132 = #127 #131
[instance] 0x0 #132
[attach-enode] #132 0
[end-of-instance]
[mk-app] #132 = #11 #12
[mk-app] #133 not #132
[inst-discovered] theory-solving 0x0 basic# ; #128
[mk-app] #134 = #128 #133
[instance] 0x0 #134
[attach-enode] #134 0
[end-of-instance]
[mk-app] #134 or #131 #133
[mk-app] #135 distinct #6 #8
[mk-app] #136 distinct #11 #13
[mk-app] #137 or #135 #136
[mk-app] #138 = #6 #8
[mk-app] #139 not #138
[inst-discovered] theory-solving 0x0 basic# ; #135
[mk-app] #140 = #135 #139
[instance] 0x0 #140
[attach-enode] #140 0
[end-of-instance]
[mk-app] #140 = #11 #13
[mk-app] #141 not #140
[inst-discovered] theory-solving 0x0 basic# ; #136
[mk-app] #142 = #136 #141
[instance] 0x0 #142
[attach-enode] #142 0
[end-of-instance]
[mk-app] #142 or #139 #141
[mk-app] #143 distinct #6 #9
[mk-app] #144 distinct #11 #14
[mk-app] #145 or #143 #144
[mk-app] #146 = #6 #9
[mk-app] #147 not #146
[inst-discovered] theory-solving 0x0 basic# ; #143
[mk-app] #148 = #143 #147
[instance] 0x0 #148
[attach-enode] #148 0
[end-of-instance]
[mk-app] #148 = #11 #14
[mk-app] #149 not #148
[inst-discovered] theory-solving 0x0 basic# ; #144
[mk-app] #150 = #144 #149
[instance] 0x0 #150
[attach-enode] #150 0
[end-of-instance]
[mk-app] #150 or #147 #149
[mk-app] #151 distinct #7 #8
[mk-app] #152 distinct #12 #13
[mk-app] #153 or #151 #152
[mk-app] #154 = #7 #8
[mk-app] #155 not #154
[inst-discovered] theory-solving 0x0 basic# ; #151
[mk-app] #156 = #151 #155
[instance] 0x0 #156
[attach-enode] #156 0
[end-of-instance]
[mk-app] #156 = #12 #13
[mk-app] #157 not #156
[inst-discovered] theory-solving 0x0 basic# ; #152
[mk-app] #158 = #152 #157
[instance] 0x0 #158
[attach-enode] #158 0
[end-of-instance]
[mk-app] #158 or #155 #157
[mk-app] #159 distinct #7 #9
[mk-app] #160 distinct #12 #14
[mk-app] #161 or #159 #160
[mk-app] #162 = #7 #9
[mk-app] #163 not #162
[inst-discovered] theory-solving 0x0 basic# ; #159
[mk-app] #164 = #159 #163
[instance] 0x0 #164
[attach-enode] #164 0
[end-of-instance]
[mk-app] #164 = #12 #14
[mk-app] #165 not #164
[inst-discovered] theory-solving 0x0 basic# ; #160
[mk-app] #166 = #160 #165
[instance] 0x0 #166
[attach-enode] #166 0
[end-of-instance]
[mk-app] #166 or #163 #165
[mk-app] #167 distinct #8 #9
[mk-app] #168 distinct #13 #14
[mk-app] #169 or #167 #168
[mk-app] #170 = #8 #9
[mk-app] #171 not #170
[inst-discovered] theory-solving 0x0 basic# ; #167
[mk-app] #172 = #167 #171
[instance] 0x0 #172
[attach-enode] #172 0
[end-of-instance]
[mk-app] #172 = #13 #14
[mk-app] #173 not #172
[inst-discovered] theory-solving 0x0 basic# ; #168
[mk-app] #174 = #168 #173
[instance] 0x0 #174
[attach-enode] #174 0
[end-of-instance]
[mk-app] #174 or #171 #173
[mk-app] #175 Int
[attach-meaning] #175 arith 1
[mk-app] #176 + #6 #175
[mk-app] #177 = #5 #176
[mk-app] #178 and #177 #100
[mk-app] #179 - #6 #175
[mk-app] #180 = #5 #179
[mk-app] #181 and #180 #100
[mk-app] #182 + #11 #175
[mk-app] #183 = #10 #182
[mk-app] #184 and #98 #183
[mk-app] #185 - #11 #175
[mk-app] #186 = #10 #185
[mk-app] #187 and #98 #186
[mk-app] #188 or #178 #181 #184 #187
[mk-app] #189 + #175 #6
[inst-discovered] theory-solving 0x0 arith# ; #176
[mk-app] #190 = #176 #189
[instance] 0x0 #190
[attach-enode] #190 0
[end-of-instance]
[mk-app] #190 Int
[attach-meaning] #190 arith (- 1)
[mk-app] #191 * #190 #6
[mk-app] #192 + #5 #191
[mk-app] #193 = #192 #175
[mk-app] #194 = #5 #189
[inst-discovered] theory-solving 0x0 arith# ; #194
[mk-app] #195 = #194 #193
[instance] 0x0 #195
[attach-enode] #195 0
[end-of-instance]
[mk-app] #189 and #193 #100
[attach-meaning] #190 arith (- 1)
[mk-app] #194 * #190 #175
[mk-app] #195 + #6 #194
[inst-discovered] theory-solving 0x0 arith# ; #179
[mk-app] #196 = #179 #195
[instance] 0x0 #196
[attach-enode] #196 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #194
[mk-app] #196 = #194 #190
[instance] 0x0 #196
[attach-enode] #196 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #196 + #190 #6
[mk-app] #197 + #6 #190
[inst-discovered] theory-solving 0x0 arith# ; #197
[mk-app] #198 = #197 #196
[instance] 0x0 #198
[attach-enode] #198 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #197 = #192 #190
[mk-app] #198 = #5 #196
[inst-discovered] theory-solving 0x0 arith# ; #198
[mk-app] #199 = #198 #197
[instance] 0x0 #199
[attach-enode] #199 0
[end-of-instance]
[mk-app] #198 and #197 #100
[mk-app] #199 + #175 #11
[inst-discovered] theory-solving 0x0 arith# ; #182
[mk-app] #200 = #182 #199
[instance] 0x0 #200
[attach-enode] #200 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #200 * #190 #11
[mk-app] #201 + #10 #200
[mk-app] #202 = #201 #175
[mk-app] #203 = #10 #199
[inst-discovered] theory-solving 0x0 arith# ; #203
[mk-app] #204 = #203 #202
[instance] 0x0 #204
[attach-enode] #204 0
[end-of-instance]
[mk-app] #199 and #98 #202
[attach-meaning] #190 arith (- 1)
[mk-app] #203 + #11 #194
[inst-discovered] theory-solving 0x0 arith# ; #185
[mk-app] #204 = #185 #203
[instance] 0x0 #204
[attach-enode] #204 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #194
[mk-app] #204 = #194 #190
[instance] 0x0 #204
[attach-enode] #204 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #204 + #190 #11
[mk-app] #205 + #11 #190
[inst-discovered] theory-solving 0x0 arith# ; #205
[mk-app] #206 = #205 #204
[instance] 0x0 #206
[attach-enode] #206 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #205 = #201 #190
[mk-app] #206 = #10 #204
[inst-discovered] theory-solving 0x0 arith# ; #206
[mk-app] #207 = #206 #205
[instance] 0x0 #207
[attach-enode] #207 0
[end-of-instance]
[mk-app] #206 and #98 #205
[mk-app] #207 or #189 #198 #199 #206
[inst-discovered] theory-solving 0x0 basic# ; #207
[mk-app] #208 = #207 #207
[instance] 0x0 #208
[attach-enode] #208 0
[end-of-instance]
[mk-app] #208 + #7 #175
[mk-app] #209 = #5 #208
[mk-app] #210 and #209 #108
[mk-app] #211 - #7 #175
[mk-app] #212 = #5 #211
[mk-app] #213 and #212 #108
[mk-app] #214 + #12 #175
[mk-app] #215 = #10 #214
[mk-app] #216 and #106 #215
[mk-app] #217 - #12 #175
[mk-app] #218 = #10 #217
[mk-app] #219 and #106 #218
[mk-app] #220 or #210 #213 #216 #219
[mk-app] #221 + #175 #7
[inst-discovered] theory-solving 0x0 arith# ; #208
[mk-app] #222 = #208 #221
[instance] 0x0 #222
[attach-enode] #222 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #222 * #190 #7
[mk-app] #223 + #5 #222
[mk-app] #224 = #223 #175
[mk-app] #225 = #5 #221
[inst-discovered] theory-solving 0x0 arith# ; #225
[mk-app] #226 = #225 #224
[instance] 0x0 #226
[attach-enode] #226 0
[end-of-instance]
[mk-app] #221 and #224 #108
[attach-meaning] #190 arith (- 1)
[mk-app] #225 + #7 #194
[inst-discovered] theory-solving 0x0 arith# ; #211
[mk-app] #226 = #211 #225
[instance] 0x0 #226
[attach-enode] #226 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #226 + #190 #7
[mk-app] #227 + #7 #190
[inst-discovered] theory-solving 0x0 arith# ; #227
[mk-app] #228 = #227 #226
[instance] 0x0 #228
[attach-enode] #228 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #227 = #223 #190
[mk-app] #228 = #5 #226
[inst-discovered] theory-solving 0x0 arith# ; #228
[mk-app] #229 = #228 #227
[instance] 0x0 #229
[attach-enode] #229 0
[end-of-instance]
[mk-app] #228 and #227 #108
[mk-app] #229 + #175 #12
[inst-discovered] theory-solving 0x0 arith# ; #214
[mk-app] #230 = #214 #229
[instance] 0x0 #230
[attach-enode] #230 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #230 * #190 #12
[mk-app] #231 + #10 #230
[mk-app] #232 = #231 #175
[mk-app] #233 = #10 #229
[inst-discovered] theory-solving 0x0 arith# ; #233
[mk-app] #234 = #233 #232
[instance] 0x0 #234
[attach-enode] #234 0
[end-of-instance]
[mk-app] #229 and #106 #232
[attach-meaning] #190 arith (- 1)
[mk-app] #233 + #12 #194
[inst-discovered] theory-solving 0x0 arith# ; #217
[mk-app] #234 = #217 #233
[instance] 0x0 #234
[attach-enode] #234 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #234 + #190 #12
[mk-app] #235 + #12 #190
[inst-discovered] theory-solving 0x0 arith# ; #235
[mk-app] #236 = #235 #234
[instance] 0x0 #236
[attach-enode] #236 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #235 = #231 #190
[mk-app] #236 = #10 #234
[inst-discovered] theory-solving 0x0 arith# ; #236
[mk-app] #237 = #236 #235
[instance] 0x0 #237
[attach-enode] #237 0
[end-of-instance]
[mk-app] #236 and #106 #235
[mk-app] #237 or #221 #228 #229 #236
[inst-discovered] theory-solving 0x0 basic# ; #237
[mk-app] #238 = #237 #237
[instance] 0x0 #238
[attach-enode] #238 0
[end-of-instance]
[mk-app] #238 + #8 #175
[mk-app] #239 = #5 #238
[mk-app] #240 and #239 #116
[mk-app] #241 - #8 #175
[mk-app] #242 = #5 #241
[mk-app] #243 and #242 #116
[mk-app] #244 + #13 #175
[mk-app] #245 = #10 #244
[mk-app] #246 and #114 #245
[mk-app] #247 - #13 #175
[mk-app] #248 = #10 #247
[mk-app] #249 and #114 #248
[mk-app] #250 or #240 #243 #246 #249
[mk-app] #251 + #175 #8
[inst-discovered] theory-solving 0x0 arith# ; #238
[mk-app] #252 = #238 #251
[instance] 0x0 #252
[attach-enode] #252 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #252 * #190 #8
[mk-app] #253 + #5 #252
[mk-app] #254 = #253 #175
[mk-app] #255 = #5 #251
[inst-discovered] theory-solving 0x0 arith# ; #255
[mk-app] #256 = #255 #254
[instance] 0x0 #256
[attach-enode] #256 0
[end-of-instance]
[mk-app] #251 and #254 #116
[attach-meaning] #190 arith (- 1)
[mk-app] #255 + #8 #194
[inst-discovered] theory-solving 0x0 arith# ; #241
[mk-app] #256 = #241 #255
[instance] 0x0 #256
[attach-enode] #256 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #256 + #190 #8
[mk-app] #257 + #8 #190
[inst-discovered] theory-solving 0x0 arith# ; #257
[mk-app] #258 = #257 #256
[instance] 0x0 #258
[attach-enode] #258 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #257 = #253 #190
[mk-app] #258 = #5 #256
[inst-discovered] theory-solving 0x0 arith# ; #258
[mk-app] #259 = #258 #257
[instance] 0x0 #259
[attach-enode] #259 0
[end-of-instance]
[mk-app] #258 and #257 #116
[mk-app] #259 + #175 #13
[inst-discovered] theory-solving 0x0 arith# ; #244
[mk-app] #260 = #244 #259
[instance] 0x0 #260
[attach-enode] #260 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #260 * #190 #13
[mk-app] #261 + #10 #260
[mk-app] #262 = #261 #175
[mk-app] #263 = #10 #259
[inst-discovered] theory-solving 0x0 arith# ; #263
[mk-app] #264 = #263 #262
[instance] 0x0 #264
[attach-enode] #264 0
[end-of-instance]
[mk-app] #259 and #114 #262
[attach-meaning] #190 arith (- 1)
[mk-app] #263 + #13 #194
[inst-discovered] theory-solving 0x0 arith# ; #247
[mk-app] #264 = #247 #263
[instance] 0x0 #264
[attach-enode] #264 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #264 + #190 #13
[mk-app] #265 + #13 #190
[inst-discovered] theory-solving 0x0 arith# ; #265
[mk-app] #266 = #265 #264
[instance] 0x0 #266
[attach-enode] #266 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #265 = #261 #190
[mk-app] #266 = #10 #264
[inst-discovered] theory-solving 0x0 arith# ; #266
[mk-app] #267 = #266 #265
[instance] 0x0 #267
[attach-enode] #267 0
[end-of-instance]
[mk-app] #266 and #114 #265
[mk-app] #267 or #251 #258 #259 #266
[inst-discovered] theory-solving 0x0 basic# ; #267
[mk-app] #268 = #267 #267
[instance] 0x0 #268
[attach-enode] #268 0
[end-of-instance]
[mk-app] #268 + #9 #175
[mk-app] #269 = #5 #268
[mk-app] #270 and #269 #124
[mk-app] #271 - #9 #175
[mk-app] #272 = #5 #271
[mk-app] #273 and #272 #124
[mk-app] #274 + #14 #175
[mk-app] #275 = #10 #274
[mk-app] #276 and #122 #275
[mk-app] #277 - #14 #175
[mk-app] #278 = #10 #277
[mk-app] #279 and #122 #278
[mk-app] #280 or #270 #273 #276 #279
[mk-app] #281 + #175 #9
[inst-discovered] theory-solving 0x0 arith# ; #268
[mk-app] #282 = #268 #281
[instance] 0x0 #282
[attach-enode] #282 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #282 * #190 #9
[mk-app] #283 + #5 #282
[mk-app] #284 = #283 #175
[mk-app] #285 = #5 #281
[inst-discovered] theory-solving 0x0 arith# ; #285
[mk-app] #286 = #285 #284
[instance] 0x0 #286
[attach-enode] #286 0
[end-of-instance]
[mk-app] #281 and #284 #124
[attach-meaning] #190 arith (- 1)
[mk-app] #285 + #9 #194
[inst-discovered] theory-solving 0x0 arith# ; #271
[mk-app] #286 = #271 #285
[instance] 0x0 #286
[attach-enode] #286 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #286 + #190 #9
[mk-app] #287 + #9 #190
[inst-discovered] theory-solving 0x0 arith# ; #287
[mk-app] #288 = #287 #286
[instance] 0x0 #288
[attach-enode] #288 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #287 = #283 #190
[mk-app] #288 = #5 #286
[inst-discovered] theory-solving 0x0 arith# ; #288
[mk-app] #289 = #288 #287
[instance] 0x0 #289
[attach-enode] #289 0
[end-of-instance]
[mk-app] #288 and #287 #124
[mk-app] #289 + #175 #14
[inst-discovered] theory-solving 0x0 arith# ; #274
[mk-app] #290 = #274 #289
[instance] 0x0 #290
[attach-enode] #290 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #290 * #190 #14
[mk-app] #291 + #10 #290
[mk-app] #292 = #291 #175
[mk-app] #293 = #10 #289
[inst-discovered] theory-solving 0x0 arith# ; #293
[mk-app] #294 = #293 #292
[instance] 0x0 #294
[attach-enode] #294 0
[end-of-instance]
[mk-app] #289 and #122 #292
[attach-meaning] #190 arith (- 1)
[mk-app] #293 + #14 #194
[inst-discovered] theory-solving 0x0 arith# ; #277
[mk-app] #294 = #277 #293
[instance] 0x0 #294
[attach-enode] #294 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #294 + #190 #14
[mk-app] #295 + #14 #190
[inst-discovered] theory-solving 0x0 arith# ; #295
[mk-app] #296 = #295 #294
[instance] 0x0 #296
[attach-enode] #296 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #295 = #291 #190
[mk-app] #296 = #10 #294
[inst-discovered] theory-solving 0x0 arith# ; #296
[mk-app] #297 = #296 #295
[instance] 0x0 #297
[attach-enode] #297 0
[end-of-instance]
[mk-app] #296 and #122 #295
[mk-app] #297 or #281 #288 #289 #296
[inst-discovered] theory-solving 0x0 basic# ; #297
[mk-app] #298 = #297 #297
[instance] 0x0 #298
[attach-enode] #298 0
[end-of-instance]
[mk-app] #298 = #6 #208
[mk-app] #299 and #298 #132
[mk-app] #300 = #6 #211
[mk-app] #301 and #300 #132
[mk-app] #302 = #11 #214
[mk-app] #303 and #130 #302
[mk-app] #304 = #11 #217
[mk-app] #305 and #130 #304
[mk-app] #306 or #299 #301 #303 #305
[mk-app] #307 + #175 #7
[inst-discovered] theory-solving 0x0 arith# ; #208
[mk-app] #308 = #208 #307
[instance] 0x0 #308
[attach-enode] #308 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #308 + #6 #222
[mk-app] #309 = #308 #175
[mk-app] #310 = #6 #307
[inst-discovered] theory-solving 0x0 arith# ; #310
[mk-app] #311 = #310 #309
[instance] 0x0 #311
[attach-enode] #311 0
[end-of-instance]
[mk-app] #310 and #309 #132
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #211
[mk-app] #311 = #211 #225
[instance] 0x0 #311
[attach-enode] #311 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #311 = #308 #190
[mk-app] #312 = #6 #226
[inst-discovered] theory-solving 0x0 arith# ; #312
[mk-app] #313 = #312 #311
[instance] 0x0 #313
[attach-enode] #313 0
[end-of-instance]
[mk-app] #312 and #311 #132
[mk-app] #313 + #175 #12
[inst-discovered] theory-solving 0x0 arith# ; #214
[mk-app] #314 = #214 #313
[instance] 0x0 #314
[attach-enode] #314 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #314 + #11 #230
[mk-app] #315 = #314 #175
[mk-app] #316 = #11 #313
[inst-discovered] theory-solving 0x0 arith# ; #316
[mk-app] #317 = #316 #315
[instance] 0x0 #317
[attach-enode] #317 0
[end-of-instance]
[mk-app] #316 and #130 #315
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #217
[mk-app] #317 = #217 #233
[instance] 0x0 #317
[attach-enode] #317 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #317 = #314 #190
[mk-app] #318 = #11 #234
[inst-discovered] theory-solving 0x0 arith# ; #318
[mk-app] #319 = #318 #317
[instance] 0x0 #319
[attach-enode] #319 0
[end-of-instance]
[mk-app] #318 and #130 #317
[mk-app] #319 or #310 #312 #316 #318
[inst-discovered] theory-solving 0x0 basic# ; #319
[mk-app] #320 = #319 #319
[instance] 0x0 #320
[attach-enode] #320 0
[end-of-instance]
[mk-app] #320 = #6 #238
[mk-app] #321 and #320 #140
[mk-app] #322 = #6 #241
[mk-app] #323 and #322 #140
[mk-app] #324 = #11 #244
[mk-app] #325 and #138 #324
[mk-app] #326 = #11 #247
[mk-app] #327 and #138 #326
[mk-app] #328 or #321 #323 #325 #327
[mk-app] #329 + #175 #8
[inst-discovered] theory-solving 0x0 arith# ; #238
[mk-app] #330 = #238 #329
[instance] 0x0 #330
[attach-enode] #330 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #330 + #6 #252
[mk-app] #331 = #330 #175
[mk-app] #332 = #6 #329
[inst-discovered] theory-solving 0x0 arith# ; #332
[mk-app] #333 = #332 #331
[instance] 0x0 #333
[attach-enode] #333 0
[end-of-instance]
[mk-app] #332 and #331 #140
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #241
[mk-app] #333 = #241 #255
[instance] 0x0 #333
[attach-enode] #333 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #333 = #330 #190
[mk-app] #334 = #6 #256
[inst-discovered] theory-solving 0x0 arith# ; #334
[mk-app] #335 = #334 #333
[instance] 0x0 #335
[attach-enode] #335 0
[end-of-instance]
[mk-app] #334 and #333 #140
[mk-app] #335 + #175 #13
[inst-discovered] theory-solving 0x0 arith# ; #244
[mk-app] #336 = #244 #335
[instance] 0x0 #336
[attach-enode] #336 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #336 + #11 #260
[mk-app] #337 = #336 #175
[mk-app] #338 = #11 #335
[inst-discovered] theory-solving 0x0 arith# ; #338
[mk-app] #339 = #338 #337
[instance] 0x0 #339
[attach-enode] #339 0
[end-of-instance]
[mk-app] #338 and #138 #337
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #247
[mk-app] #339 = #247 #263
[instance] 0x0 #339
[attach-enode] #339 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #339 = #336 #190
[mk-app] #340 = #11 #264
[inst-discovered] theory-solving 0x0 arith# ; #340
[mk-app] #341 = #340 #339
[instance] 0x0 #341
[attach-enode] #341 0
[end-of-instance]
[mk-app] #340 and #138 #339
[mk-app] #341 or #332 #334 #338 #340
[inst-discovered] theory-solving 0x0 basic# ; #341
[mk-app] #342 = #341 #341
[instance] 0x0 #342
[attach-enode] #342 0
[end-of-instance]
[mk-app] #342 = #6 #268
[mk-app] #343 and #342 #148
[mk-app] #344 = #6 #271
[mk-app] #345 and #344 #148
[mk-app] #346 = #11 #274
[mk-app] #347 and #146 #346
[mk-app] #348 = #11 #277
[mk-app] #349 and #146 #348
[mk-app] #350 or #343 #345 #347 #349
[mk-app] #351 + #175 #9
[inst-discovered] theory-solving 0x0 arith# ; #268
[mk-app] #352 = #268 #351
[instance] 0x0 #352
[attach-enode] #352 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #352 + #6 #282
[mk-app] #353 = #352 #175
[mk-app] #354 = #6 #351
[inst-discovered] theory-solving 0x0 arith# ; #354
[mk-app] #355 = #354 #353
[instance] 0x0 #355
[attach-enode] #355 0
[end-of-instance]
[mk-app] #354 and #353 #148
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #271
[mk-app] #355 = #271 #285
[instance] 0x0 #355
[attach-enode] #355 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #355 = #352 #190
[mk-app] #356 = #6 #286
[inst-discovered] theory-solving 0x0 arith# ; #356
[mk-app] #357 = #356 #355
[instance] 0x0 #357
[attach-enode] #357 0
[end-of-instance]
[mk-app] #356 and #355 #148
[mk-app] #357 + #175 #14
[inst-discovered] theory-solving 0x0 arith# ; #274
[mk-app] #358 = #274 #357
[instance] 0x0 #358
[attach-enode] #358 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #358 + #11 #290
[mk-app] #359 = #358 #175
[mk-app] #360 = #11 #357
[inst-discovered] theory-solving 0x0 arith# ; #360
[mk-app] #361 = #360 #359
[instance] 0x0 #361
[attach-enode] #361 0
[end-of-instance]
[mk-app] #360 and #146 #359
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #277
[mk-app] #361 = #277 #293
[instance] 0x0 #361
[attach-enode] #361 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #361 = #358 #190
[mk-app] #362 = #11 #294
[inst-discovered] theory-solving 0x0 arith# ; #362
[mk-app] #363 = #362 #361
[instance] 0x0 #363
[attach-enode] #363 0
[end-of-instance]
[mk-app] #362 and #146 #361
[mk-app] #363 or #354 #356 #360 #362
[inst-discovered] theory-solving 0x0 basic# ; #363
[mk-app] #364 = #363 #363
[instance] 0x0 #364
[attach-enode] #364 0
[end-of-instance]
[mk-app] #364 = #7 #238
[mk-app] #365 and #364 #156
[mk-app] #366 = #7 #241
[mk-app] #367 and #366 #156
[mk-app] #368 = #12 #244
[mk-app] #369 and #154 #368
[mk-app] #370 = #12 #247
[mk-app] #371 and #154 #370
[mk-app] #372 or #365 #367 #369 #371
[attach-meaning] #190 arith (- 1)
[mk-app] #373 + #7 #252
[mk-app] #374 = #373 #175
[mk-app] #375 = #7 #329
[inst-discovered] theory-solving 0x0 arith# ; #375
[mk-app] #376 = #375 #374
[instance] 0x0 #376
[attach-enode] #376 0
[end-of-instance]
[mk-app] #375 and #374 #156
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #376 = #373 #190
[mk-app] #377 = #7 #256
[inst-discovered] theory-solving 0x0 arith# ; #377
[mk-app] #378 = #377 #376
[instance] 0x0 #378
[attach-enode] #378 0
[end-of-instance]
[mk-app] #377 and #376 #156
[attach-meaning] #190 arith (- 1)
[mk-app] #378 + #12 #260
[mk-app] #379 = #378 #175
[mk-app] #380 = #12 #335
[inst-discovered] theory-solving 0x0 arith# ; #380
[mk-app] #381 = #380 #379
[instance] 0x0 #381
[attach-enode] #381 0
[end-of-instance]
[mk-app] #380 and #154 #379
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #381 = #378 #190
[mk-app] #382 = #12 #264
[inst-discovered] theory-solving 0x0 arith# ; #382
[mk-app] #383 = #382 #381
[instance] 0x0 #383
[attach-enode] #383 0
[end-of-instance]
[mk-app] #382 and #154 #381
[mk-app] #383 or #375 #377 #380 #382
[inst-discovered] theory-solving 0x0 basic# ; #383
[mk-app] #384 = #383 #383
[instance] 0x0 #384
[attach-enode] #384 0
[end-of-instance]
[mk-app] #384 = #7 #268
[mk-app] #385 and #384 #164
[mk-app] #386 = #7 #271
[mk-app] #387 and #386 #164
[mk-app] #388 = #12 #274
[mk-app] #389 and #162 #388
[mk-app] #390 = #12 #277
[mk-app] #391 and #162 #390
[mk-app] #392 or #385 #387 #389 #391
[attach-meaning] #190 arith (- 1)
[mk-app] #393 + #7 #282
[mk-app] #394 = #393 #175
[mk-app] #395 = #7 #351
[inst-discovered] theory-solving 0x0 arith# ; #395
[mk-app] #396 = #395 #394
[instance] 0x0 #396
[attach-enode] #396 0
[end-of-instance]
[mk-app] #395 and #394 #164
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #396 = #393 #190
[mk-app] #397 = #7 #286
[inst-discovered] theory-solving 0x0 arith# ; #397
[mk-app] #398 = #397 #396
[instance] 0x0 #398
[attach-enode] #398 0
[end-of-instance]
[mk-app] #397 and #396 #164
[attach-meaning] #190 arith (- 1)
[mk-app] #398 + #12 #290
[mk-app] #399 = #398 #175
[mk-app] #400 = #12 #357
[inst-discovered] theory-solving 0x0 arith# ; #400
[mk-app] #401 = #400 #399
[instance] 0x0 #401
[attach-enode] #401 0
[end-of-instance]
[mk-app] #400 and #162 #399
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #401 = #398 #190
[mk-app] #402 = #12 #294
[inst-discovered] theory-solving 0x0 arith# ; #402
[mk-app] #403 = #402 #401
[instance] 0x0 #403
[attach-enode] #403 0
[end-of-instance]
[mk-app] #402 and #162 #401
[mk-app] #403 or #395 #397 #400 #402
[inst-discovered] theory-solving 0x0 basic# ; #403
[mk-app] #404 = #403 #403
[instance] 0x0 #404
[attach-enode] #404 0
[end-of-instance]
[mk-app] #404 = #8 #268
[mk-app] #405 and #404 #172
[mk-app] #406 = #8 #271
[mk-app] #407 and #406 #172
[mk-app] #408 = #13 #274
[mk-app] #409 and #170 #408
[mk-app] #410 = #13 #277
[mk-app] #411 and #170 #410
[mk-app] #412 or #405 #407 #409 #411
[attach-meaning] #190 arith (- 1)
[mk-app] #413 + #8 #282
[mk-app] #414 = #413 #175
[mk-app] #415 = #8 #351
[inst-discovered] theory-solving 0x0 arith# ; #415
[mk-app] #416 = #415 #414
[instance] 0x0 #416
[attach-enode] #416 0
[end-of-instance]
[mk-app] #415 and #414 #172
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #416 = #413 #190
[mk-app] #417 = #8 #286
[inst-discovered] theory-solving 0x0 arith# ; #417
[mk-app] #418 = #417 #416
[instance] 0x0 #418
[attach-enode] #418 0
[end-of-instance]
[mk-app] #417 and #416 #172
[attach-meaning] #190 arith (- 1)
[mk-app] #418 + #13 #290
[mk-app] #419 = #418 #175
[mk-app] #420 = #13 #357
[inst-discovered] theory-solving 0x0 arith# ; #420
[mk-app] #421 = #420 #419
[instance] 0x0 #421
[attach-enode] #421 0
[end-of-instance]
[mk-app] #420 and #170 #419
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[mk-app] #421 = #418 #190
[mk-app] #422 = #13 #294
[inst-discovered] theory-solving 0x0 arith# ; #422
[mk-app] #423 = #422 #421
[instance] 0x0 #423
[attach-enode] #423 0
[end-of-instance]
[mk-app] #422 and #170 #421
[mk-app] #423 or #415 #417 #420 #422
[inst-discovered] theory-solving 0x0 basic# ; #423
[mk-app] #424 = #423 #423
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[attach-meaning] #17 bv #b1
[attach-meaning] #18 bv #b0
[attach-meaning] #17 bv #b1
[attach-meaning] #18 bv #b0
[inst-discovered] theory-solving 0x0 arith# ; #36
[mk-app] #424 = #36 #38
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #41
[mk-app] #424 = #41 #44
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #47
[mk-app] #424 = #47 #50
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #53
[mk-app] #424 = #53 #56
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #59
[mk-app] #424 = #59 #62
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #65
[mk-app] #424 = #65 #68
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #71
[mk-app] #424 = #71 #74
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #77
[mk-app] #424 = #77 #80
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #83
[mk-app] #424 = #83 #86
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #89
[mk-app] #424 = #89 #92
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #94
[mk-app] #424 = #94 #99
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #95
[mk-app] #424 = #95 #101
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #103
[mk-app] #424 = #103 #107
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #104
[mk-app] #424 = #104 #109
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #111
[mk-app] #424 = #111 #115
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #112
[mk-app] #424 = #112 #117
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #119
[mk-app] #424 = #119 #123
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #120
[mk-app] #424 = #120 #125
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #127
[mk-app] #424 = #127 #131
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #128
[mk-app] #424 = #128 #133
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #135
[mk-app] #424 = #135 #139
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #136
[mk-app] #424 = #136 #141
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #143
[mk-app] #424 = #143 #147
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #144
[mk-app] #424 = #144 #149
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #151
[mk-app] #424 = #151 #155
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #152
[mk-app] #424 = #152 #157
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #159
[mk-app] #424 = #159 #163
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #160
[mk-app] #424 = #160 #165
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #167
[mk-app] #424 = #167 #171
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #168
[mk-app] #424 = #168 #173
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[mk-app] #424 + #175 #6
[inst-discovered] theory-solving 0x0 arith# ; #176
[mk-app] #425 = #176 #424
[instance] 0x0 #425
[attach-enode] #425 0
[end-of-instance]
[mk-app] #425 = #5 #424
[mk-app] #426 and #425 #100
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #179
[mk-app] #427 = #179 #195
[instance] 0x0 #427
[attach-enode] #427 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #194
[mk-app] #427 = #194 #190
[instance] 0x0 #427
[attach-enode] #427 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #427 + #6 #190
[inst-discovered] theory-solving 0x0 arith# ; #427
[mk-app] #428 = #427 #196
[instance] 0x0 #428
[attach-enode] #428 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #427 = #5 #196
[mk-app] #428 and #427 #100
[mk-app] #429 + #175 #11
[inst-discovered] theory-solving 0x0 arith# ; #182
[mk-app] #430 = #182 #429
[instance] 0x0 #430
[attach-enode] #430 0
[end-of-instance]
[mk-app] #430 = #10 #429
[mk-app] #431 and #98 #430
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #185
[mk-app] #432 = #185 #203
[instance] 0x0 #432
[attach-enode] #432 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #432 + #11 #190
[inst-discovered] theory-solving 0x0 arith# ; #432
[mk-app] #433 = #432 #204
[instance] 0x0 #433
[attach-enode] #433 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #432 = #10 #204
[mk-app] #433 and #98 #432
[mk-app] #434 or #426 #428 #431 #433
[inst-discovered] theory-solving 0x0 basic# ; #434
[mk-app] #435 = #434 #434
[instance] 0x0 #435
[attach-enode] #435 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #208
[mk-app] #435 = #208 #307
[instance] 0x0 #435
[attach-enode] #435 0
[end-of-instance]
[mk-app] #435 = #5 #307
[mk-app] #436 and #435 #108
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #211
[mk-app] #437 = #211 #225
[instance] 0x0 #437
[attach-enode] #437 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #437 + #7 #190
[inst-discovered] theory-solving 0x0 arith# ; #437
[mk-app] #438 = #437 #226
[instance] 0x0 #438
[attach-enode] #438 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #437 = #5 #226
[mk-app] #438 and #437 #108
[inst-discovered] theory-solving 0x0 arith# ; #214
[mk-app] #439 = #214 #313
[instance] 0x0 #439
[attach-enode] #439 0
[end-of-instance]
[mk-app] #439 = #10 #313
[mk-app] #440 and #106 #439
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #217
[mk-app] #441 = #217 #233
[instance] 0x0 #441
[attach-enode] #441 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #441 + #12 #190
[inst-discovered] theory-solving 0x0 arith# ; #441
[mk-app] #442 = #441 #234
[instance] 0x0 #442
[attach-enode] #442 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #441 = #10 #234
[mk-app] #442 and #106 #441
[mk-app] #443 or #436 #438 #440 #442
[inst-discovered] theory-solving 0x0 basic# ; #443
[mk-app] #444 = #443 #443
[instance] 0x0 #444
[attach-enode] #444 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #238
[mk-app] #444 = #238 #329
[instance] 0x0 #444
[attach-enode] #444 0
[end-of-instance]
[mk-app] #444 = #5 #329
[mk-app] #445 and #444 #116
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #241
[mk-app] #446 = #241 #255
[instance] 0x0 #446
[attach-enode] #446 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #446 + #8 #190
[inst-discovered] theory-solving 0x0 arith# ; #446
[mk-app] #447 = #446 #256
[instance] 0x0 #447
[attach-enode] #447 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #446 = #5 #256
[mk-app] #447 and #446 #116
[inst-discovered] theory-solving 0x0 arith# ; #244
[mk-app] #448 = #244 #335
[instance] 0x0 #448
[attach-enode] #448 0
[end-of-instance]
[mk-app] #448 = #10 #335
[mk-app] #449 and #114 #448
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #247
[mk-app] #450 = #247 #263
[instance] 0x0 #450
[attach-enode] #450 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #450 + #13 #190
[inst-discovered] theory-solving 0x0 arith# ; #450
[mk-app] #451 = #450 #264
[instance] 0x0 #451
[attach-enode] #451 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #450 = #10 #264
[mk-app] #451 and #114 #450
[mk-app] #452 or #445 #447 #449 #451
[inst-discovered] theory-solving 0x0 basic# ; #452
[mk-app] #453 = #452 #452
[instance] 0x0 #453
[attach-enode] #453 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #268
[mk-app] #453 = #268 #351
[instance] 0x0 #453
[attach-enode] #453 0
[end-of-instance]
[mk-app] #453 = #5 #351
[mk-app] #454 and #453 #124
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #271
[mk-app] #455 = #271 #285
[instance] 0x0 #455
[attach-enode] #455 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #455 + #9 #190
[inst-discovered] theory-solving 0x0 arith# ; #455
[mk-app] #456 = #455 #286
[instance] 0x0 #456
[attach-enode] #456 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #455 = #5 #286
[mk-app] #456 and #455 #124
[inst-discovered] theory-solving 0x0 arith# ; #274
[mk-app] #457 = #274 #357
[instance] 0x0 #457
[attach-enode] #457 0
[end-of-instance]
[mk-app] #457 = #10 #357
[mk-app] #458 and #122 #457
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #277
[mk-app] #459 = #277 #293
[instance] 0x0 #459
[attach-enode] #459 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #459 + #14 #190
[inst-discovered] theory-solving 0x0 arith# ; #459
[mk-app] #460 = #459 #294
[instance] 0x0 #460
[attach-enode] #460 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #459 = #10 #294
[mk-app] #460 and #122 #459
[mk-app] #461 or #454 #456 #458 #460
[inst-discovered] theory-solving 0x0 basic# ; #461
[mk-app] #462 = #461 #461
[instance] 0x0 #462
[attach-enode] #462 0
[end-of-instance]
[mk-app] #462 = #6 #307
[mk-app] #463 and #462 #132
[attach-meaning] #190 arith (- 1)
[mk-app] #464 = #6 #226
[mk-app] #465 and #464 #132
[mk-app] #466 = #11 #313
[mk-app] #467 and #130 #466
[attach-meaning] #190 arith (- 1)
[mk-app] #468 = #11 #234
[mk-app] #469 and #130 #468
[mk-app] #470 or #463 #465 #467 #469
[inst-discovered] theory-solving 0x0 basic# ; #470
[mk-app] #471 = #470 #470
[instance] 0x0 #471
[attach-enode] #471 0
[end-of-instance]
[mk-app] #471 = #6 #329
[mk-app] #472 and #471 #140
[attach-meaning] #190 arith (- 1)
[mk-app] #473 = #6 #256
[mk-app] #474 and #473 #140
[mk-app] #475 = #11 #335
[mk-app] #476 and #138 #475
[attach-meaning] #190 arith (- 1)
[mk-app] #477 = #11 #264
[mk-app] #478 and #138 #477
[mk-app] #479 or #472 #474 #476 #478
[inst-discovered] theory-solving 0x0 basic# ; #479
[mk-app] #480 = #479 #479
[instance] 0x0 #480
[attach-enode] #480 0
[end-of-instance]
[mk-app] #480 = #6 #351
[mk-app] #481 and #480 #148
[attach-meaning] #190 arith (- 1)
[mk-app] #482 = #6 #286
[mk-app] #483 and #482 #148
[mk-app] #484 = #11 #357
[mk-app] #485 and #146 #484
[attach-meaning] #190 arith (- 1)
[mk-app] #486 = #11 #294
[mk-app] #487 and #146 #486
[mk-app] #488 or #481 #483 #485 #487
[inst-discovered] theory-solving 0x0 basic# ; #488
[mk-app] #489 = #488 #488
[instance] 0x0 #489
[attach-enode] #489 0
[end-of-instance]
[mk-app] #489 = #7 #329
[mk-app] #490 and #489 #156
[attach-meaning] #190 arith (- 1)
[mk-app] #491 = #7 #256
[mk-app] #492 and #491 #156
[mk-app] #493 = #12 #335
[mk-app] #494 and #154 #493
[attach-meaning] #190 arith (- 1)
[mk-app] #495 = #12 #264
[mk-app] #496 and #154 #495
[mk-app] #497 or #490 #492 #494 #496
[inst-discovered] theory-solving 0x0 basic# ; #497
[mk-app] #498 = #497 #497
[instance] 0x0 #498
[attach-enode] #498 0
[end-of-instance]
[mk-app] #498 = #7 #351
[mk-app] #499 and #498 #164
[attach-meaning] #190 arith (- 1)
[mk-app] #500 = #7 #286
[mk-app] #501 and #500 #164
[mk-app] #502 = #12 #357
[mk-app] #503 and #162 #502
[attach-meaning] #190 arith (- 1)
[mk-app] #504 = #12 #294
[mk-app] #505 and #162 #504
[mk-app] #506 or #499 #501 #503 #505
[inst-discovered] theory-solving 0x0 basic# ; #506
[mk-app] #507 = #506 #506
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[mk-app] #507 = #8 #351
[mk-app] #508 and #507 #172
[attach-meaning] #190 arith (- 1)
[mk-app] #509 = #8 #286
[mk-app] #510 and #509 #172
[mk-app] #511 = #13 #357
[mk-app] #512 and #170 #511
[attach-meaning] #190 arith (- 1)
[mk-app] #513 = #13 #294
[mk-app] #514 and #170 #513
[mk-app] #515 or #508 #510 #512 #514
[inst-discovered] theory-solving 0x0 basic# ; #515
[mk-app] #516 = #515 #515
[instance] 0x0 #516
[attach-enode] #516 0
[end-of-instance]
[mk-app] #516 not #425
[mk-app] #517 or #101 #516
[mk-app] #518 not #517
[inst-discovered] theory-solving 0x0 basic# ; #426
[mk-app] #519 = #426 #518
[instance] 0x0 #519
[attach-enode] #519 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #519 not #427
[mk-app] #520 or #101 #519
[mk-app] #521 not #520
[inst-discovered] theory-solving 0x0 basic# ; #428
[mk-app] #522 = #428 #521
[instance] 0x0 #522
[attach-enode] #522 0
[end-of-instance]
[mk-app] #522 not #430
[mk-app] #523 or #99 #522
[mk-app] #524 not #523
[inst-discovered] theory-solving 0x0 basic# ; #431
[mk-app] #525 = #431 #524
[instance] 0x0 #525
[attach-enode] #525 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #525 not #432
[mk-app] #526 or #99 #525
[mk-app] #527 not #526
[inst-discovered] theory-solving 0x0 basic# ; #433
[mk-app] #528 = #433 #527
[instance] 0x0 #528
[attach-enode] #528 0
[end-of-instance]
[mk-app] #528 or #518 #521 #524 #527
[inst-discovered] theory-solving 0x0 basic# ; #528
[mk-app] #529 = #528 #528
[instance] 0x0 #529
[attach-enode] #529 0
[end-of-instance]
[mk-app] #426 not #435
[mk-app] #428 or #109 #426
[mk-app] #431 not #428
[inst-discovered] theory-solving 0x0 basic# ; #436
[mk-app] #433 = #436 #431
[instance] 0x0 #433
[attach-enode] #433 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #433 not #437
[mk-app] #434 or #109 #433
[mk-app] #529 not #434
[inst-discovered] theory-solving 0x0 basic# ; #438
[mk-app] #530 = #438 #529
[instance] 0x0 #530
[attach-enode] #530 0
[end-of-instance]
[mk-app] #530 not #439
[mk-app] #531 or #107 #530
[mk-app] #532 not #531
[inst-discovered] theory-solving 0x0 basic# ; #440
[mk-app] #533 = #440 #532
[instance] 0x0 #533
[attach-enode] #533 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #533 not #441
[mk-app] #534 or #107 #533
[mk-app] #535 not #534
[inst-discovered] theory-solving 0x0 basic# ; #442
[mk-app] #536 = #442 #535
[instance] 0x0 #536
[attach-enode] #536 0
[end-of-instance]
[mk-app] #536 or #431 #529 #532 #535
[inst-discovered] theory-solving 0x0 basic# ; #536
[mk-app] #537 = #536 #536
[instance] 0x0 #537
[attach-enode] #537 0
[end-of-instance]
[mk-app] #436 not #444
[mk-app] #438 or #117 #436
[mk-app] #440 not #438
[inst-discovered] theory-solving 0x0 basic# ; #445
[mk-app] #442 = #445 #440
[instance] 0x0 #442
[attach-enode] #442 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #442 not #446
[mk-app] #443 or #117 #442
[mk-app] #537 not #443
[inst-discovered] theory-solving 0x0 basic# ; #447
[mk-app] #538 = #447 #537
[instance] 0x0 #538
[attach-enode] #538 0
[end-of-instance]
[mk-app] #538 not #448
[mk-app] #539 or #115 #538
[mk-app] #540 not #539
[inst-discovered] theory-solving 0x0 basic# ; #449
[mk-app] #541 = #449 #540
[instance] 0x0 #541
[attach-enode] #541 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #541 not #450
[mk-app] #542 or #115 #541
[mk-app] #543 not #542
[inst-discovered] theory-solving 0x0 basic# ; #451
[mk-app] #544 = #451 #543
[instance] 0x0 #544
[attach-enode] #544 0
[end-of-instance]
[mk-app] #544 or #440 #537 #540 #543
[inst-discovered] theory-solving 0x0 basic# ; #544
[mk-app] #545 = #544 #544
[instance] 0x0 #545
[attach-enode] #545 0
[end-of-instance]
[mk-app] #445 not #453
[mk-app] #447 or #125 #445
[mk-app] #449 not #447
[inst-discovered] theory-solving 0x0 basic# ; #454
[mk-app] #451 = #454 #449
[instance] 0x0 #451
[attach-enode] #451 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #451 not #455
[mk-app] #452 or #125 #451
[mk-app] #545 not #452
[inst-discovered] theory-solving 0x0 basic# ; #456
[mk-app] #546 = #456 #545
[instance] 0x0 #546
[attach-enode] #546 0
[end-of-instance]
[mk-app] #546 not #457
[mk-app] #547 or #123 #546
[mk-app] #548 not #547
[inst-discovered] theory-solving 0x0 basic# ; #458
[mk-app] #549 = #458 #548
[instance] 0x0 #549
[attach-enode] #549 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #549 not #459
[mk-app] #550 or #123 #549
[mk-app] #551 not #550
[inst-discovered] theory-solving 0x0 basic# ; #460
[mk-app] #552 = #460 #551
[instance] 0x0 #552
[attach-enode] #552 0
[end-of-instance]
[mk-app] #552 or #449 #545 #548 #551
[inst-discovered] theory-solving 0x0 basic# ; #552
[mk-app] #553 = #552 #552
[instance] 0x0 #553
[attach-enode] #553 0
[end-of-instance]
[mk-app] #454 not #462
[mk-app] #456 or #133 #454
[mk-app] #458 not #456
[inst-discovered] theory-solving 0x0 basic# ; #463
[mk-app] #460 = #463 #458
[instance] 0x0 #460
[attach-enode] #460 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #460 not #464
[mk-app] #461 or #133 #460
[mk-app] #553 not #461
[inst-discovered] theory-solving 0x0 basic# ; #465
[mk-app] #554 = #465 #553
[instance] 0x0 #554
[attach-enode] #554 0
[end-of-instance]
[mk-app] #554 not #466
[mk-app] #555 or #131 #554
[mk-app] #556 not #555
[inst-discovered] theory-solving 0x0 basic# ; #467
[mk-app] #557 = #467 #556
[instance] 0x0 #557
[attach-enode] #557 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #557 not #468
[mk-app] #558 or #131 #557
[mk-app] #559 not #558
[inst-discovered] theory-solving 0x0 basic# ; #469
[mk-app] #560 = #469 #559
[instance] 0x0 #560
[attach-enode] #560 0
[end-of-instance]
[mk-app] #560 or #458 #553 #556 #559
[inst-discovered] theory-solving 0x0 basic# ; #560
[mk-app] #561 = #560 #560
[instance] 0x0 #561
[attach-enode] #561 0
[end-of-instance]
[mk-app] #463 not #471
[mk-app] #465 or #141 #463
[mk-app] #467 not #465
[inst-discovered] theory-solving 0x0 basic# ; #472
[mk-app] #469 = #472 #467
[instance] 0x0 #469
[attach-enode] #469 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #469 not #473
[mk-app] #470 or #141 #469
[mk-app] #561 not #470
[inst-discovered] theory-solving 0x0 basic# ; #474
[mk-app] #562 = #474 #561
[instance] 0x0 #562
[attach-enode] #562 0
[end-of-instance]
[mk-app] #562 not #475
[mk-app] #563 or #139 #562
[mk-app] #564 not #563
[inst-discovered] theory-solving 0x0 basic# ; #476
[mk-app] #565 = #476 #564
[instance] 0x0 #565
[attach-enode] #565 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #565 not #477
[mk-app] #566 or #139 #565
[mk-app] #567 not #566
[inst-discovered] theory-solving 0x0 basic# ; #478
[mk-app] #568 = #478 #567
[instance] 0x0 #568
[attach-enode] #568 0
[end-of-instance]
[mk-app] #568 or #467 #561 #564 #567
[inst-discovered] theory-solving 0x0 basic# ; #568
[mk-app] #569 = #568 #568
[instance] 0x0 #569
[attach-enode] #569 0
[end-of-instance]
[mk-app] #472 not #480
[mk-app] #474 or #149 #472
[mk-app] #476 not #474
[inst-discovered] theory-solving 0x0 basic# ; #481
[mk-app] #478 = #481 #476
[instance] 0x0 #478
[attach-enode] #478 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #478 not #482
[mk-app] #479 or #149 #478
[mk-app] #569 not #479
[inst-discovered] theory-solving 0x0 basic# ; #483
[mk-app] #570 = #483 #569
[instance] 0x0 #570
[attach-enode] #570 0
[end-of-instance]
[mk-app] #570 not #484
[mk-app] #571 or #147 #570
[mk-app] #572 not #571
[inst-discovered] theory-solving 0x0 basic# ; #485
[mk-app] #573 = #485 #572
[instance] 0x0 #573
[attach-enode] #573 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #573 not #486
[mk-app] #574 or #147 #573
[mk-app] #575 not #574
[inst-discovered] theory-solving 0x0 basic# ; #487
[mk-app] #576 = #487 #575
[instance] 0x0 #576
[attach-enode] #576 0
[end-of-instance]
[mk-app] #576 or #476 #569 #572 #575
[inst-discovered] theory-solving 0x0 basic# ; #576
[mk-app] #577 = #576 #576
[instance] 0x0 #577
[attach-enode] #577 0
[end-of-instance]
[mk-app] #481 not #489
[mk-app] #483 or #157 #481
[mk-app] #485 not #483
[inst-discovered] theory-solving 0x0 basic# ; #490
[mk-app] #487 = #490 #485
[instance] 0x0 #487
[attach-enode] #487 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #487 not #491
[mk-app] #488 or #157 #487
[mk-app] #577 not #488
[inst-discovered] theory-solving 0x0 basic# ; #492
[mk-app] #578 = #492 #577
[instance] 0x0 #578
[attach-enode] #578 0
[end-of-instance]
[mk-app] #578 not #493
[mk-app] #579 or #155 #578
[mk-app] #580 not #579
[inst-discovered] theory-solving 0x0 basic# ; #494
[mk-app] #581 = #494 #580
[instance] 0x0 #581
[attach-enode] #581 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #581 not #495
[mk-app] #582 or #155 #581
[mk-app] #583 not #582
[inst-discovered] theory-solving 0x0 basic# ; #496
[mk-app] #584 = #496 #583
[instance] 0x0 #584
[attach-enode] #584 0
[end-of-instance]
[mk-app] #584 or #485 #577 #580 #583
[inst-discovered] theory-solving 0x0 basic# ; #584
[mk-app] #585 = #584 #584
[instance] 0x0 #585
[attach-enode] #585 0
[end-of-instance]
[mk-app] #490 not #498
[mk-app] #492 or #165 #490
[mk-app] #494 not #492
[inst-discovered] theory-solving 0x0 basic# ; #499
[mk-app] #496 = #499 #494
[instance] 0x0 #496
[attach-enode] #496 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #496 not #500
[mk-app] #497 or #165 #496
[mk-app] #585 not #497
[inst-discovered] theory-solving 0x0 basic# ; #501
[mk-app] #586 = #501 #585
[instance] 0x0 #586
[attach-enode] #586 0
[end-of-instance]
[mk-app] #586 not #502
[mk-app] #587 or #163 #586
[mk-app] #588 not #587
[inst-discovered] theory-solving 0x0 basic# ; #503
[mk-app] #589 = #503 #588
[instance] 0x0 #589
[attach-enode] #589 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #589 not #504
[mk-app] #590 or #163 #589
[mk-app] #591 not #590
[inst-discovered] theory-solving 0x0 basic# ; #505
[mk-app] #592 = #505 #591
[instance] 0x0 #592
[attach-enode] #592 0
[end-of-instance]
[mk-app] #592 or #494 #585 #588 #591
[inst-discovered] theory-solving 0x0 basic# ; #592
[mk-app] #593 = #592 #592
[instance] 0x0 #593
[attach-enode] #593 0
[end-of-instance]
[mk-app] #499 not #507
[mk-app] #501 or #173 #499
[mk-app] #503 not #501
[inst-discovered] theory-solving 0x0 basic# ; #508
[mk-app] #505 = #508 #503
[instance] 0x0 #505
[attach-enode] #505 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #505 not #509
[mk-app] #506 or #173 #505
[mk-app] #593 not #506
[inst-discovered] theory-solving 0x0 basic# ; #510
[mk-app] #594 = #510 #593
[instance] 0x0 #594
[attach-enode] #594 0
[end-of-instance]
[mk-app] #594 not #511
[mk-app] #595 or #171 #594
[mk-app] #596 not #595
[inst-discovered] theory-solving 0x0 basic# ; #512
[mk-app] #597 = #512 #596
[instance] 0x0 #597
[attach-enode] #597 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #597 not #513
[mk-app] #598 or #171 #597
[mk-app] #599 not #598
[inst-discovered] theory-solving 0x0 basic# ; #514
[mk-app] #600 = #514 #599
[instance] 0x0 #600
[attach-enode] #600 0
[end-of-instance]
[mk-app] #600 or #503 #593 #596 #599
[inst-discovered] theory-solving 0x0 basic# ; #600
[mk-app] #601 = #600 #600
[instance] 0x0 #601
[attach-enode] #601 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #424
[mk-app] #508 = #424 #424
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #196
[mk-app] #508 = #196 #196
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #429
[mk-app] #508 = #429 #429
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #204
[mk-app] #508 = #204 #204
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #528
[mk-app] #508 = #528 #528
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #307
[mk-app] #508 = #307 #307
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #226
[mk-app] #508 = #226 #226
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #313
[mk-app] #508 = #313 #313
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #234
[mk-app] #508 = #234 #234
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #536
[mk-app] #508 = #536 #536
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #329
[mk-app] #508 = #329 #329
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #256
[mk-app] #508 = #256 #256
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #335
[mk-app] #508 = #335 #335
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #264
[mk-app] #508 = #264 #264
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #544
[mk-app] #508 = #544 #544
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith# ; #351
[mk-app] #508 = #351 #351
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #286
[mk-app] #508 = #286 #286
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #357
[mk-app] #508 = #357 #357
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #294
[mk-app] #508 = #294 #294
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #552
[mk-app] #508 = #552 #552
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #560
[mk-app] #508 = #560 #560
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #568
[mk-app] #508 = #568 #568
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #576
[mk-app] #508 = #576 #576
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #584
[mk-app] #508 = #584 #584
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #592
[mk-app] #508 = #592 #592
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 basic# ; #600
[mk-app] #508 = #600 #600
[instance] 0x0 #508
[attach-enode] #508 0
[end-of-instance]
[mk-app] #508 - #10 #190
[mk-app] #510 - #10 #175
[mk-app] #512 - #5 #190
[mk-app] #514 - #5 #175
[mk-app] #515 - #11 #190
[mk-app] #601 - #6 #190
[mk-app] #602 - #12 #190
[mk-app] #603 - #7 #190
[mk-app] #604 - #13 #190
[mk-app] #605 - #8 #190
[attach-meaning] #190 arith (- 1)
[mk-app] #604 * #190 #5
[mk-app] #602 Int
[attach-meaning] #602 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #37
[mk-app] #604 = #37 #42
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 * #190 #10
[mk-app] #602 Int
[attach-meaning] #602 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #43
[mk-app] #604 = #43 #48
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 Int
[attach-meaning] #604 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #49
[mk-app] #604 = #49 #54
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 Int
[attach-meaning] #604 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #55
[mk-app] #604 = #55 #60
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 Int
[attach-meaning] #604 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #61
[mk-app] #604 = #61 #66
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 Int
[attach-meaning] #604 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #67
[mk-app] #604 = #67 #72
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 Int
[attach-meaning] #604 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #73
[mk-app] #604 = #73 #78
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 Int
[attach-meaning] #604 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #79
[mk-app] #604 = #79 #84
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 Int
[attach-meaning] #604 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #85
[mk-app] #604 = #85 #90
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 Int
[attach-meaning] #604 arith (- 10)
[inst-discovered] theory-solving 0x0 arith# ; #91
[mk-app] #604 = #91 #96
[instance] 0x0 #604
[attach-enode] #604 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[mk-app] #604 = #192 #15
[inst-discovered] theory-solving 0x0 arith# ; #98
[mk-app] #602 = #98 #604
[instance] 0x0 #602
[attach-enode] #602 0
[end-of-instance]
[mk-app] #602 not #604
[attach-meaning] #190 arith (- 1)
[mk-app] #515 = #201 #15
[inst-discovered] theory-solving 0x0 arith# ; #100
[mk-app] #510 = #100 #515
[instance] 0x0 #510
[attach-enode] #510 0
[end-of-instance]
[mk-app] #510 not #515
[mk-app] #508 or #602 #510
[attach-meaning] #190 arith (- 1)
[mk-app] #605 = #223 #15
[inst-discovered] theory-solving 0x0 arith# ; #106
[mk-app] #603 = #106 #605
[instance] 0x0 #603
[attach-enode] #603 0
[end-of-instance]
[mk-app] #603 not #605
[attach-meaning] #190 arith (- 1)
[mk-app] #601 = #231 #15
[inst-discovered] theory-solving 0x0 arith# ; #108
[mk-app] #514 = #108 #601
[instance] 0x0 #514
[attach-enode] #514 0
[end-of-instance]
[mk-app] #514 not #601
[mk-app] #512 or #603 #514
[attach-meaning] #190 arith (- 1)
[mk-app] #606 = #253 #15
[inst-discovered] theory-solving 0x0 arith# ; #114
[mk-app] #607 = #114 #606
[instance] 0x0 #607
[attach-enode] #607 0
[end-of-instance]
[mk-app] #607 not #606
[attach-meaning] #190 arith (- 1)
[mk-app] #608 = #261 #15
[inst-discovered] theory-solving 0x0 arith# ; #116
[mk-app] #609 = #116 #608
[instance] 0x0 #609
[attach-enode] #609 0
[end-of-instance]
[mk-app] #609 not #608
[mk-app] #610 or #607 #609
[attach-meaning] #190 arith (- 1)
[mk-app] #611 = #283 #15
[inst-discovered] theory-solving 0x0 arith# ; #122
[mk-app] #612 = #122 #611
[instance] 0x0 #612
[attach-enode] #612 0
[end-of-instance]
[mk-app] #612 not #611
[attach-meaning] #190 arith (- 1)
[mk-app] #613 = #291 #15
[inst-discovered] theory-solving 0x0 arith# ; #124
[mk-app] #614 = #124 #613
[instance] 0x0 #614
[attach-enode] #614 0
[end-of-instance]
[mk-app] #614 not #613
[mk-app] #615 or #612 #614
[attach-meaning] #190 arith (- 1)
[mk-app] #616 = #308 #15
[inst-discovered] theory-solving 0x0 arith# ; #130
[mk-app] #617 = #130 #616
[instance] 0x0 #617
[attach-enode] #617 0
[end-of-instance]
[mk-app] #617 not #616
[attach-meaning] #190 arith (- 1)
[mk-app] #618 = #314 #15
[inst-discovered] theory-solving 0x0 arith# ; #132
[mk-app] #619 = #132 #618
[instance] 0x0 #619
[attach-enode] #619 0
[end-of-instance]
[mk-app] #619 not #618
[mk-app] #620 or #617 #619
[attach-meaning] #190 arith (- 1)
[mk-app] #621 = #330 #15
[inst-discovered] theory-solving 0x0 arith# ; #138
[mk-app] #622 = #138 #621
[instance] 0x0 #622
[attach-enode] #622 0
[end-of-instance]
[mk-app] #622 not #621
[attach-meaning] #190 arith (- 1)
[mk-app] #623 = #336 #15
[inst-discovered] theory-solving 0x0 arith# ; #140
[mk-app] #624 = #140 #623
[instance] 0x0 #624
[attach-enode] #624 0
[end-of-instance]
[mk-app] #624 not #623
[mk-app] #625 or #622 #624
[attach-meaning] #190 arith (- 1)
[mk-app] #626 = #352 #15
[inst-discovered] theory-solving 0x0 arith# ; #146
[mk-app] #627 = #146 #626
[instance] 0x0 #627
[attach-enode] #627 0
[end-of-instance]
[mk-app] #627 not #626
[attach-meaning] #190 arith (- 1)
[mk-app] #628 = #358 #15
[inst-discovered] theory-solving 0x0 arith# ; #148
[mk-app] #629 = #148 #628
[instance] 0x0 #629
[attach-enode] #629 0
[end-of-instance]
[mk-app] #629 not #628
[mk-app] #630 or #627 #629
[attach-meaning] #190 arith (- 1)
[mk-app] #631 = #373 #15
[inst-discovered] theory-solving 0x0 arith# ; #154
[mk-app] #632 = #154 #631
[instance] 0x0 #632
[attach-enode] #632 0
[end-of-instance]
[mk-app] #632 not #631
[attach-meaning] #190 arith (- 1)
[mk-app] #633 = #378 #15
[inst-discovered] theory-solving 0x0 arith# ; #156
[mk-app] #634 = #156 #633
[instance] 0x0 #634
[attach-enode] #634 0
[end-of-instance]
[mk-app] #634 not #633
[mk-app] #635 or #632 #634
[attach-meaning] #190 arith (- 1)
[mk-app] #636 = #393 #15
[inst-discovered] theory-solving 0x0 arith# ; #162
[mk-app] #637 = #162 #636
[instance] 0x0 #637
[attach-enode] #637 0
[end-of-instance]
[mk-app] #637 not #636
[attach-meaning] #190 arith (- 1)
[mk-app] #638 = #398 #15
[inst-discovered] theory-solving 0x0 arith# ; #164
[mk-app] #639 = #164 #638
[instance] 0x0 #639
[attach-enode] #639 0
[end-of-instance]
[mk-app] #639 not #638
[mk-app] #640 or #637 #639
[attach-meaning] #190 arith (- 1)
[mk-app] #641 = #413 #15
[inst-discovered] theory-solving 0x0 arith# ; #170
[mk-app] #642 = #170 #641
[instance] 0x0 #642
[attach-enode] #642 0
[end-of-instance]
[mk-app] #642 not #641
[attach-meaning] #190 arith (- 1)
[mk-app] #643 = #418 #15
[inst-discovered] theory-solving 0x0 arith# ; #172
[mk-app] #644 = #172 #643
[instance] 0x0 #644
[attach-enode] #644 0
[end-of-instance]
[mk-app] #644 not #643
[mk-app] #645 or #642 #644
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #425
[mk-app] #646 = #425 #193
[instance] 0x0 #646
[attach-enode] #646 0
[end-of-instance]
[mk-app] #646 not #193
[mk-app] #647 or #510 #646
[inst-discovered] theory-solving 0x0 basic# ; #647
[mk-app] #648 = #647 #647
[instance] 0x0 #648
[attach-enode] #648 0
[end-of-instance]
[mk-app] #648 not #647
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #427
[mk-app] #649 = #427 #197
[instance] 0x0 #649
[attach-enode] #649 0
[end-of-instance]
[mk-app] #649 not #197
[mk-app] #650 or #510 #649
[inst-discovered] theory-solving 0x0 basic# ; #650
[mk-app] #651 = #650 #650
[instance] 0x0 #651
[attach-enode] #651 0
[end-of-instance]
[mk-app] #651 not #650
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #430
[mk-app] #652 = #430 #202
[instance] 0x0 #652
[attach-enode] #652 0
[end-of-instance]
[mk-app] #652 not #202
[mk-app] #653 or #602 #652
[mk-app] #654 not #653
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #432
[mk-app] #655 = #432 #205
[instance] 0x0 #655
[attach-enode] #655 0
[end-of-instance]
[mk-app] #655 not #205
[mk-app] #656 or #602 #655
[mk-app] #657 not #656
[mk-app] #658 or #648 #651 #654 #657
[inst-discovered] theory-solving 0x0 basic# ; #658
[mk-app] #659 = #658 #658
[instance] 0x0 #659
[attach-enode] #659 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #435
[mk-app] #424 = #435 #224
[instance] 0x0 #424
[attach-enode] #424 0
[end-of-instance]
[mk-app] #424 not #224
[mk-app] #425 or #424 #514
[mk-app] #516 or #514 #424
[inst-discovered] theory-solving 0x0 basic# ; #516
[mk-app] #517 = #516 #425
[instance] 0x0 #517
[attach-enode] #517 0
[end-of-instance]
[mk-app] #516 not #425
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #437
[mk-app] #517 = #437 #227
[instance] 0x0 #517
[attach-enode] #517 0
[end-of-instance]
[mk-app] #517 not #227
[mk-app] #518 or #514 #517
[inst-discovered] theory-solving 0x0 basic# ; #518
[mk-app] #427 = #518 #518
[instance] 0x0 #427
[attach-enode] #427 0
[end-of-instance]
[mk-app] #427 not #518
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #439
[mk-app] #519 = #439 #232
[instance] 0x0 #519
[attach-enode] #519 0
[end-of-instance]
[mk-app] #519 not #232
[mk-app] #520 or #603 #519
[mk-app] #521 not #520
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #441
[mk-app] #429 = #441 #235
[instance] 0x0 #429
[attach-enode] #429 0
[end-of-instance]
[mk-app] #429 not #235
[mk-app] #430 or #603 #429
[mk-app] #522 not #430
[mk-app] #523 or #427 #516 #521 #522
[mk-app] #524 or #516 #427 #521 #522
[inst-discovered] theory-solving 0x0 basic# ; #524
[mk-app] #432 = #524 #523
[instance] 0x0 #432
[attach-enode] #432 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #444
[mk-app] #435 = #444 #254
[instance] 0x0 #435
[attach-enode] #435 0
[end-of-instance]
[mk-app] #435 not #254
[mk-app] #426 or #435 #609
[mk-app] #428 or #609 #435
[inst-discovered] theory-solving 0x0 basic# ; #428
[mk-app] #431 = #428 #426
[instance] 0x0 #431
[attach-enode] #431 0
[end-of-instance]
[mk-app] #428 not #426
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #446
[mk-app] #431 = #446 #257
[instance] 0x0 #431
[attach-enode] #431 0
[end-of-instance]
[mk-app] #431 not #257
[mk-app] #437 or #431 #609
[mk-app] #433 or #609 #431
[inst-discovered] theory-solving 0x0 basic# ; #433
[mk-app] #434 = #433 #437
[instance] 0x0 #434
[attach-enode] #434 0
[end-of-instance]
[mk-app] #433 not #437
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #448
[mk-app] #434 = #448 #262
[instance] 0x0 #434
[attach-enode] #434 0
[end-of-instance]
[mk-app] #434 not #262
[mk-app] #529 or #607 #434
[mk-app] #439 not #529
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #450
[mk-app] #530 = #450 #265
[instance] 0x0 #530
[attach-enode] #530 0
[end-of-instance]
[mk-app] #530 not #265
[mk-app] #531 or #607 #530
[mk-app] #532 not #531
[mk-app] #441 or #428 #433 #439 #532
[inst-discovered] theory-solving 0x0 basic# ; #441
[mk-app] #533 = #441 #441
[instance] 0x0 #533
[attach-enode] #533 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #453
[mk-app] #444 = #453 #284
[instance] 0x0 #444
[attach-enode] #444 0
[end-of-instance]
[mk-app] #444 not #284
[mk-app] #436 or #444 #614
[mk-app] #438 or #614 #444
[inst-discovered] theory-solving 0x0 basic# ; #438
[mk-app] #440 = #438 #436
[instance] 0x0 #440
[attach-enode] #440 0
[end-of-instance]
[mk-app] #438 not #436
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #455
[mk-app] #440 = #455 #287
[instance] 0x0 #440
[attach-enode] #440 0
[end-of-instance]
[mk-app] #440 not #287
[mk-app] #446 or #440 #614
[mk-app] #442 or #614 #440
[inst-discovered] theory-solving 0x0 basic# ; #442
[mk-app] #443 = #442 #446
[instance] 0x0 #443
[attach-enode] #443 0
[end-of-instance]
[mk-app] #442 not #446
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #457
[mk-app] #443 = #457 #292
[instance] 0x0 #443
[attach-enode] #443 0
[end-of-instance]
[mk-app] #443 not #292
[mk-app] #537 or #612 #443
[mk-app] #448 not #537
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #459
[mk-app] #538 = #459 #295
[instance] 0x0 #538
[attach-enode] #538 0
[end-of-instance]
[mk-app] #538 not #295
[mk-app] #539 or #612 #538
[mk-app] #540 not #539
[mk-app] #450 or #438 #442 #448 #540
[inst-discovered] theory-solving 0x0 basic# ; #450
[mk-app] #541 = #450 #450
[instance] 0x0 #541
[attach-enode] #541 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #462
[mk-app] #453 = #462 #309
[instance] 0x0 #453
[attach-enode] #453 0
[end-of-instance]
[mk-app] #453 not #309
[mk-app] #445 or #453 #619
[mk-app] #447 or #619 #453
[inst-discovered] theory-solving 0x0 basic# ; #447
[mk-app] #449 = #447 #445
[instance] 0x0 #449
[attach-enode] #449 0
[end-of-instance]
[mk-app] #447 not #445
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #464
[mk-app] #449 = #464 #311
[instance] 0x0 #449
[attach-enode] #449 0
[end-of-instance]
[mk-app] #449 not #311
[mk-app] #455 or #449 #619
[mk-app] #451 or #619 #449
[inst-discovered] theory-solving 0x0 basic# ; #451
[mk-app] #452 = #451 #455
[instance] 0x0 #452
[attach-enode] #452 0
[end-of-instance]
[mk-app] #451 not #455
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #466
[mk-app] #452 = #466 #315
[instance] 0x0 #452
[attach-enode] #452 0
[end-of-instance]
[mk-app] #452 not #315
[mk-app] #545 or #617 #452
[mk-app] #457 not #545
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #468
[mk-app] #546 = #468 #317
[instance] 0x0 #546
[attach-enode] #546 0
[end-of-instance]
[mk-app] #546 not #317
[mk-app] #547 or #617 #546
[mk-app] #548 not #547
[mk-app] #459 or #447 #451 #457 #548
[inst-discovered] theory-solving 0x0 basic# ; #459
[mk-app] #549 = #459 #459
[instance] 0x0 #549
[attach-enode] #549 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #471
[mk-app] #462 = #471 #331
[instance] 0x0 #462
[attach-enode] #462 0
[end-of-instance]
[mk-app] #462 not #331
[mk-app] #454 or #462 #624
[mk-app] #456 or #624 #462
[inst-discovered] theory-solving 0x0 basic# ; #456
[mk-app] #458 = #456 #454
[instance] 0x0 #458
[attach-enode] #458 0
[end-of-instance]
[mk-app] #456 not #454
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #473
[mk-app] #458 = #473 #333
[instance] 0x0 #458
[attach-enode] #458 0
[end-of-instance]
[mk-app] #458 not #333
[mk-app] #464 or #458 #624
[mk-app] #460 or #624 #458
[inst-discovered] theory-solving 0x0 basic# ; #460
[mk-app] #461 = #460 #464
[instance] 0x0 #461
[attach-enode] #461 0
[end-of-instance]
[mk-app] #460 not #464
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #475
[mk-app] #461 = #475 #337
[instance] 0x0 #461
[attach-enode] #461 0
[end-of-instance]
[mk-app] #461 not #337
[mk-app] #553 or #622 #461
[mk-app] #466 not #553
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #477
[mk-app] #554 = #477 #339
[instance] 0x0 #554
[attach-enode] #554 0
[end-of-instance]
[mk-app] #554 not #339
[mk-app] #555 or #622 #554
[mk-app] #556 not #555
[mk-app] #468 or #456 #460 #466 #556
[inst-discovered] theory-solving 0x0 basic# ; #468
[mk-app] #557 = #468 #468
[instance] 0x0 #557
[attach-enode] #557 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #480
[mk-app] #471 = #480 #353
[instance] 0x0 #471
[attach-enode] #471 0
[end-of-instance]
[mk-app] #471 not #353
[mk-app] #463 or #471 #629
[mk-app] #465 or #629 #471
[inst-discovered] theory-solving 0x0 basic# ; #465
[mk-app] #467 = #465 #463
[instance] 0x0 #467
[attach-enode] #467 0
[end-of-instance]
[mk-app] #465 not #463
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #482
[mk-app] #467 = #482 #355
[instance] 0x0 #467
[attach-enode] #467 0
[end-of-instance]
[mk-app] #467 not #355
[mk-app] #473 or #467 #629
[mk-app] #469 or #629 #467
[inst-discovered] theory-solving 0x0 basic# ; #469
[mk-app] #470 = #469 #473
[instance] 0x0 #470
[attach-enode] #470 0
[end-of-instance]
[mk-app] #469 not #473
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #484
[mk-app] #470 = #484 #359
[instance] 0x0 #470
[attach-enode] #470 0
[end-of-instance]
[mk-app] #470 not #359
[mk-app] #561 or #627 #470
[mk-app] #475 not #561
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #486
[mk-app] #562 = #486 #361
[instance] 0x0 #562
[attach-enode] #562 0
[end-of-instance]
[mk-app] #562 not #361
[mk-app] #563 or #627 #562
[mk-app] #564 not #563
[mk-app] #477 or #465 #469 #475 #564
[inst-discovered] theory-solving 0x0 basic# ; #477
[mk-app] #565 = #477 #477
[instance] 0x0 #565
[attach-enode] #565 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #489
[mk-app] #480 = #489 #374
[instance] 0x0 #480
[attach-enode] #480 0
[end-of-instance]
[mk-app] #480 not #374
[mk-app] #472 or #480 #634
[mk-app] #474 or #634 #480
[inst-discovered] theory-solving 0x0 basic# ; #474
[mk-app] #476 = #474 #472
[instance] 0x0 #476
[attach-enode] #476 0
[end-of-instance]
[mk-app] #474 not #472
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #491
[mk-app] #476 = #491 #376
[instance] 0x0 #476
[attach-enode] #476 0
[end-of-instance]
[mk-app] #476 not #376
[mk-app] #482 or #476 #634
[mk-app] #478 or #634 #476
[inst-discovered] theory-solving 0x0 basic# ; #478
[mk-app] #479 = #478 #482
[instance] 0x0 #479
[attach-enode] #479 0
[end-of-instance]
[mk-app] #478 not #482
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #493
[mk-app] #479 = #493 #379
[instance] 0x0 #479
[attach-enode] #479 0
[end-of-instance]
[mk-app] #479 not #379
[mk-app] #569 or #632 #479
[mk-app] #484 not #569
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #495
[mk-app] #570 = #495 #381
[instance] 0x0 #570
[attach-enode] #570 0
[end-of-instance]
[mk-app] #570 not #381
[mk-app] #571 or #632 #570
[mk-app] #572 not #571
[mk-app] #486 or #474 #478 #484 #572
[inst-discovered] theory-solving 0x0 basic# ; #486
[mk-app] #573 = #486 #486
[instance] 0x0 #573
[attach-enode] #573 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #498
[mk-app] #489 = #498 #394
[instance] 0x0 #489
[attach-enode] #489 0
[end-of-instance]
[mk-app] #489 not #394
[mk-app] #481 or #489 #639
[mk-app] #483 or #639 #489
[inst-discovered] theory-solving 0x0 basic# ; #483
[mk-app] #485 = #483 #481
[instance] 0x0 #485
[attach-enode] #485 0
[end-of-instance]
[mk-app] #483 not #481
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #500
[mk-app] #485 = #500 #396
[instance] 0x0 #485
[attach-enode] #485 0
[end-of-instance]
[mk-app] #485 not #396
[mk-app] #491 or #485 #639
[mk-app] #487 or #639 #485
[inst-discovered] theory-solving 0x0 basic# ; #487
[mk-app] #488 = #487 #491
[instance] 0x0 #488
[attach-enode] #488 0
[end-of-instance]
[mk-app] #487 not #491
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #502
[mk-app] #488 = #502 #399
[instance] 0x0 #488
[attach-enode] #488 0
[end-of-instance]
[mk-app] #488 not #399
[mk-app] #577 or #637 #488
[mk-app] #493 not #577
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #504
[mk-app] #578 = #504 #401
[instance] 0x0 #578
[attach-enode] #578 0
[end-of-instance]
[mk-app] #578 not #401
[mk-app] #579 or #637 #578
[mk-app] #580 not #579
[mk-app] #495 or #483 #487 #493 #580
[inst-discovered] theory-solving 0x0 basic# ; #495
[mk-app] #581 = #495 #495
[instance] 0x0 #581
[attach-enode] #581 0
[end-of-instance]
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #507
[mk-app] #498 = #507 #414
[instance] 0x0 #498
[attach-enode] #498 0
[end-of-instance]
[mk-app] #498 not #414
[mk-app] #490 or #498 #644
[mk-app] #492 or #644 #498
[inst-discovered] theory-solving 0x0 basic# ; #492
[mk-app] #494 = #492 #490
[instance] 0x0 #494
[attach-enode] #494 0
[end-of-instance]
[mk-app] #492 not #490
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #509
[mk-app] #494 = #509 #416
[instance] 0x0 #494
[attach-enode] #494 0
[end-of-instance]
[mk-app] #494 not #416
[mk-app] #500 or #494 #644
[mk-app] #496 or #644 #494
[inst-discovered] theory-solving 0x0 basic# ; #496
[mk-app] #497 = #496 #500
[instance] 0x0 #497
[attach-enode] #497 0
[end-of-instance]
[mk-app] #496 not #500
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #511
[mk-app] #497 = #511 #419
[instance] 0x0 #497
[attach-enode] #497 0
[end-of-instance]
[mk-app] #497 not #419
[mk-app] #585 or #642 #497
[mk-app] #502 not #585
[attach-meaning] #190 arith (- 1)
[attach-meaning] #190 arith (- 1)
[inst-discovered] theory-solving 0x0 arith# ; #513
[mk-app] #586 = #513 #421
[instance] 0x0 #586
[attach-enode] #586 0
[end-of-instance]
[mk-app] #586 not #421
[mk-app] #587 or #642 #586
[mk-app] #588 not #587
[mk-app] #504 or #492 #496 #502 #588
[inst-discovered] theory-solving 0x0 basic# ; #504
[mk-app] #589 = #504 #504
[instance] 0x0 #589
[attach-enode] #589 0
[end-of-instance]
[attach-meaning] #18 bv #b0
[attach-enode] #1 0
[attach-enode] #2 0
[inst-discovered] theory-solving 0x0 basic# ; #647
[mk-app] #507 = #647 #647
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #650
[mk-app] #507 = #650 #650
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #658
[mk-app] #507 = #658 #658
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #518
[mk-app] #507 = #518 #518
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #523
[mk-app] #507 = #523 #523
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #441
[mk-app] #507 = #441 #441
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #450
[mk-app] #507 = #450 #450
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #459
[mk-app] #507 = #459 #459
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #468
[mk-app] #507 = #468 #468
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #477
[mk-app] #507 = #477 #477
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #486
[mk-app] #507 = #486 #486
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #495
[mk-app] #507 = #495 #495
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #504
[mk-app] #507 = #504 #504
[instance] 0x0 #507
[attach-enode] #507 0
[end-of-instance]
[begin-check] 0
[attach-enode] #175 0
[mk-app] #507 Real
[attach-meaning] #507 arith 1
[attach-enode] #507 0
[attach-enode] #15 0
[mk-app] #499 Real
[attach-meaning] #499 arith 0
[attach-enode] #499 0
[inst-discovered] theory-solving 0x0 basic# ; #647
[mk-app] #501 = #647 #647
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #650
[mk-app] #501 = #650 #650
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #658
[mk-app] #501 = #658 #658
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #518
[mk-app] #501 = #518 #518
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #523
[mk-app] #501 = #523 #523
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #441
[mk-app] #501 = #441 #441
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #450
[mk-app] #501 = #450 #450
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #459
[mk-app] #501 = #459 #459
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #468
[mk-app] #501 = #468 #468
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #477
[mk-app] #501 = #477 #477
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #486
[mk-app] #501 = #486 #486
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #495
[mk-app] #501 = #495 #495
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #504
[mk-app] #501 = #504 #504
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #504
[mk-app] #501 = #504 #504
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #495
[mk-app] #501 = #495 #495
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #486
[mk-app] #501 = #486 #486
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #477
[mk-app] #501 = #477 #477
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #468
[mk-app] #501 = #468 #468
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #459
[mk-app] #501 = #459 #459
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #450
[mk-app] #501 = #450 #450
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #441
[mk-app] #501 = #441 #441
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #518
[mk-app] #501 = #518 #518
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #523
[mk-app] #501 = #523 #523
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #647
[mk-app] #501 = #647 #647
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #650
[mk-app] #501 = #650 #650
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #658
[mk-app] #501 = #658 #658
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #647
[mk-app] #501 = #647 #647
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #650
[mk-app] #501 = #650 #650
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #658
[mk-app] #501 = #658 #658
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #518
[mk-app] #501 = #518 #518
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #523
[mk-app] #501 = #523 #523
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #441
[mk-app] #501 = #441 #441
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #450
[mk-app] #501 = #450 #450
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #459
[mk-app] #501 = #459 #459
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #468
[mk-app] #501 = #468 #468
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #477
[mk-app] #501 = #477 #477
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #486
[mk-app] #501 = #486 #486
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #495
[mk-app] #501 = #495 #495
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #504
[mk-app] #501 = #504 #504
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #647
[mk-app] #501 = #647 #647
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #650
[mk-app] #501 = #650 #650
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #658
[mk-app] #501 = #658 #658
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #518
[mk-app] #501 = #518 #518
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #523
[mk-app] #501 = #523 #523
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #441
[mk-app] #501 = #441 #441
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #450
[mk-app] #501 = #450 #450
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #459
[mk-app] #501 = #459 #459
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #468
[mk-app] #501 = #468 #468
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #477
[mk-app] #501 = #477 #477
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #486
[mk-app] #501 = #486 #486
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #495
[mk-app] #501 = #495 #495
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #504
[mk-app] #501 = #504 #504
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #647
[mk-app] #501 = #647 #647
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #650
[mk-app] #501 = #650 #650
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #658
[mk-app] #501 = #658 #658
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #518
[mk-app] #501 = #518 #518
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #523
[mk-app] #501 = #523 #523
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #441
[mk-app] #501 = #441 #441
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #450
[mk-app] #501 = #450 #450
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #459
[mk-app] #501 = #459 #459
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #468
[mk-app] #501 = #468 #468
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #477
[mk-app] #501 = #477 #477
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #486
[mk-app] #501 = #486 #486
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #495
[mk-app] #501 = #495 #495
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #504
[mk-app] #501 = #504 #504
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #647
[mk-app] #501 = #647 #647
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #650
[mk-app] #501 = #650 #650
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #658
[mk-app] #501 = #658 #658
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #518
[mk-app] #501 = #518 #518
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #523
[mk-app] #501 = #523 #523
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #441
[mk-app] #501 = #441 #441
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #450
[mk-app] #501 = #450 #450
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #459
[mk-app] #501 = #459 #459
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #468
[mk-app] #501 = #468 #468
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #477
[mk-app] #501 = #477 #477
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #486
[mk-app] #501 = #486 #486
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #495
[mk-app] #501 = #495 #495
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[inst-discovered] theory-solving 0x0 basic# ; #504
[mk-app] #501 = #504 #504
[instance] 0x0 #501
[attach-enode] #501 0
[end-of-instance]
[attach-enode] #5 0
[assign] #16 justification -1: 
[assign] (not #42) justification -1: 
[attach-enode] #10 0
[assign] #40 justification -1: 
[assign] (not #48) justification -1: 
[attach-enode] #6 0
[assign] #46 justification -1: 
[assign] (not #54) justification -1: 
[attach-enode] #11 0
[assign] #52 justification -1: 
[assign] (not #60) justification -1: 
[attach-enode] #7 0
[assign] #58 justification -1: 
[assign] (not #66) justification -1: 
[attach-enode] #12 0
[assign] #64 justification -1: 
[assign] (not #72) justification -1: 
[attach-enode] #8 0
[assign] #70 justification -1: 
[assign] (not #78) justification -1: 
[attach-enode] #13 0
[assign] #76 justification -1: 
[assign] (not #84) justification -1: 
[attach-enode] #9 0
[assign] #82 justification -1: 
[assign] (not #90) justification -1: 
[attach-enode] #14 0
[assign] #88 justification -1: 
[assign] (not #96) justification -1: 
[attach-enode] #190 0
[attach-enode] #191 0
[attach-enode] #192 0
[attach-enode] #604 0
[mk-app] #501 = #15 #192
[mk-app] #503 <= #192 #15
[mk-app] #509 >= #192 #15
[attach-enode] #501 0
[attach-enode] #200 0
[attach-enode] #201 0
[attach-enode] #515 0
[mk-app] #505 = #15 #201
[mk-app] #506 <= #201 #15
[mk-app] #593 >= #201 #15
[attach-enode] #505 0
[attach-enode] #222 0
[attach-enode] #223 0
[attach-enode] #605 0
[mk-app] #511 = #15 #223
[mk-app] #594 <= #223 #15
[mk-app] #595 >= #223 #15
[attach-enode] #511 0
[attach-enode] #230 0
[attach-enode] #231 0
[attach-enode] #601 0
[mk-app] #596 = #15 #231
[mk-app] #513 <= #231 #15
[mk-app] #597 >= #231 #15
[attach-enode] #596 0
[attach-enode] #252 0
[attach-enode] #253 0
[attach-enode] #606 0
[mk-app] #598 = #15 #253
[mk-app] #599 <= #253 #15
[mk-app] #600 >= #253 #15
[attach-enode] #598 0
[attach-enode] #260 0
[attach-enode] #261 0
[attach-enode] #608 0
[mk-app] #589 = #15 #261
[mk-app] #590 <= #261 #15
[mk-app] #591 >= #261 #15
[attach-enode] #589 0
[attach-enode] #282 0
[attach-enode] #283 0
[attach-enode] #611 0
[mk-app] #592 = #15 #283
[mk-app] #581 <= #283 #15
[mk-app] #582 >= #283 #15
[attach-enode] #592 0
[attach-enode] #290 0
[attach-enode] #291 0
[attach-enode] #613 0
[mk-app] #583 = #15 #291
[mk-app] #584 <= #291 #15
[mk-app] #573 >= #291 #15
[attach-enode] #583 0
[attach-enode] #308 0
[attach-enode] #616 0
[mk-app] #574 = #15 #308
[mk-app] #575 <= #308 #15
[mk-app] #576 >= #308 #15
[attach-enode] #574 0
[attach-enode] #314 0
[attach-enode] #618 0
[mk-app] #565 = #15 #314
[mk-app] #566 <= #314 #15
[mk-app] #567 >= #314 #15
[attach-enode] #565 0
[attach-enode] #330 0
[attach-enode] #621 0
[mk-app] #568 = #15 #330
[mk-app] #557 <= #330 #15
[mk-app] #558 >= #330 #15
[attach-enode] #568 0
[attach-enode] #336 0
[attach-enode] #623 0
[mk-app] #559 = #15 #336
[mk-app] #560 <= #336 #15
[mk-app] #549 >= #336 #15
[attach-enode] #559 0
[attach-enode] #352 0
[attach-enode] #626 0
[mk-app] #550 = #15 #352
[mk-app] #551 <= #352 #15
[mk-app] #552 >= #352 #15
[attach-enode] #550 0
[attach-enode] #358 0
[attach-enode] #628 0
[mk-app] #541 = #15 #358
[mk-app] #542 <= #358 #15
[mk-app] #543 >= #358 #15
[attach-enode] #541 0
[attach-enode] #373 0
[attach-enode] #631 0
[mk-app] #544 = #15 #373
[mk-app] #533 <= #373 #15
[mk-app] #534 >= #373 #15
[attach-enode] #544 0
[attach-enode] #378 0
[attach-enode] #633 0
[mk-app] #535 = #15 #378
[mk-app] #536 <= #378 #15
[mk-app] #524 >= #378 #15
[attach-enode] #535 0
[attach-enode] #393 0
[attach-enode] #636 0
[mk-app] #432 = #15 #393
[mk-app] #525 <= #393 #15
[mk-app] #526 >= #393 #15
[attach-enode] #432 0
[attach-enode] #398 0
[attach-enode] #638 0
[mk-app] #527 = #15 #398
[mk-app] #528 <= #398 #15
[mk-app] #659 >= #398 #15
[attach-enode] #527 0
[attach-enode] #413 0
[attach-enode] #641 0
[mk-app] #660 = #15 #413
[mk-app] #661 <= #413 #15
[mk-app] #662 >= #413 #15
[attach-enode] #660 0
[attach-enode] #418 0
[attach-enode] #643 0
[mk-app] #663 = #15 #418
[mk-app] #664 <= #418 #15
[mk-app] #665 >= #418 #15
[attach-enode] #663 0
[attach-enode] #193 0
[mk-app] #666 = #175 #192
[mk-app] #667 <= #192 #175
[mk-app] #668 >= #192 #175
[attach-enode] #666 0
[attach-enode] #197 0
[mk-app] #669 = #190 #192
[mk-app] #670 <= #192 #190
[mk-app] #671 >= #192 #190
[attach-enode] #669 0
[attach-enode] #202 0
[mk-app] #672 = #175 #201
[mk-app] #673 <= #201 #175
[mk-app] #674 >= #201 #175
[attach-enode] #672 0
[attach-enode] #205 0
[mk-app] #675 = #190 #201
[mk-app] #676 <= #201 #190
[mk-app] #677 >= #201 #190
[attach-enode] #675 0
[attach-enode] #227 0
[mk-app] #678 = #190 #223
[mk-app] #679 <= #223 #190
[mk-app] #680 >= #223 #190
[attach-enode] #678 0
[attach-enode] #224 0
[mk-app] #681 = #175 #223
[mk-app] #682 <= #223 #175
[mk-app] #683 >= #223 #175
[attach-enode] #681 0
[attach-enode] #232 0
[mk-app] #684 = #175 #231
[mk-app] #685 <= #231 #175
[mk-app] #686 >= #231 #175
[attach-enode] #684 0
[attach-enode] #235 0
[mk-app] #687 = #190 #231
[mk-app] #688 <= #231 #190
[mk-app] #689 >= #231 #190
[attach-enode] #687 0
[attach-enode] #254 0
[mk-app] #690 = #175 #253
[mk-app] #691 <= #253 #175
[mk-app] #692 >= #253 #175
[attach-enode] #690 0
[attach-enode] #257 0
[mk-app] #693 = #190 #253
[mk-app] #694 <= #253 #190
[mk-app] #695 >= #253 #190
[attach-enode] #693 0
[attach-enode] #262 0
[mk-app] #696 = #175 #261
[mk-app] #697 <= #261 #175
[mk-app] #698 >= #261 #175
[attach-enode] #696 0
[attach-enode] #265 0
[mk-app] #699 = #190 #261
[mk-app] #700 <= #261 #190
[mk-app] #701 >= #261 #190
[attach-enode] #699 0
[attach-enode] #284 0
[mk-app] #702 = #175 #283
[mk-app] #703 <= #283 #175
[mk-app] #704 >= #283 #175
[attach-enode] #702 0
[attach-enode] #287 0
[mk-app] #705 = #190 #283
[mk-app] #706 <= #283 #190
[mk-app] #707 >= #283 #190
[attach-enode] #705 0
[attach-enode] #292 0
[mk-app] #708 = #175 #291
[mk-app] #709 <= #291 #175
[mk-app] #710 >= #291 #175
[attach-enode] #708 0
[attach-enode] #295 0
[mk-app] #711 = #190 #291
[mk-app] #712 <= #291 #190
[mk-app] #713 >= #291 #190
[attach-enode] #711 0
[attach-enode] #309 0
[mk-app] #714 = #175 #308
[mk-app] #715 <= #308 #175
[mk-app] #716 >= #308 #175
[attach-enode] #714 0
[attach-enode] #311 0
[mk-app] #717 = #190 #308
[mk-app] #718 <= #308 #190
[mk-app] #719 >= #308 #190
[attach-enode] #717 0
[attach-enode] #315 0
[mk-app] #720 = #175 #314
[mk-app] #721 <= #314 #175
[mk-app] #722 >= #314 #175
[attach-enode] #720 0
[attach-enode] #317 0
[mk-app] #723 = #190 #314
[mk-app] #724 <= #314 #190
[mk-app] #725 >= #314 #190
[attach-enode] #723 0
[attach-enode] #331 0
[mk-app] #726 = #175 #330
[mk-app] #727 <= #330 #175
[mk-app] #728 >= #330 #175
[attach-enode] #726 0
[attach-enode] #333 0
[mk-app] #729 = #190 #330
[mk-app] #730 <= #330 #190
[mk-app] #731 >= #330 #190
[attach-enode] #729 0
[attach-enode] #337 0
[mk-app] #732 = #175 #336
[mk-app] #733 <= #336 #175
[mk-app] #734 >= #336 #175
[attach-enode] #732 0
[attach-enode] #339 0
[mk-app] #735 = #190 #336
[mk-app] #736 <= #336 #190
[mk-app] #737 >= #336 #190
[attach-enode] #735 0
[attach-enode] #353 0
[mk-app] #738 = #175 #352
[mk-app] #739 <= #352 #175
[mk-app] #740 >= #352 #175
[attach-enode] #738 0
[attach-enode] #355 0
[mk-app] #741 = #190 #352
[mk-app] #742 <= #352 #190
[mk-app] #743 >= #352 #190
[attach-enode] #741 0
[attach-enode] #359 0
[mk-app] #744 = #175 #358
[mk-app] #745 <= #358 #175
[mk-app] #746 >= #358 #175
[attach-enode] #744 0
[attach-enode] #361 0
[mk-app] #747 = #190 #358
[mk-app] #748 <= #358 #190
[mk-app] #749 >= #358 #190
[attach-enode] #747 0
[attach-enode] #374 0
[mk-app] #750 = #175 #373
[mk-app] #751 <= #373 #175
[mk-app] #752 >= #373 #175
[attach-enode] #750 0
[attach-enode] #376 0
[mk-app] #753 = #190 #373
[mk-app] #754 <= #373 #190
[mk-app] #755 >= #373 #190
[attach-enode] #753 0
[attach-enode] #379 0
[mk-app] #756 = #175 #378
[mk-app] #757 <= #378 #175
[mk-app] #758 >= #378 #175
[attach-enode] #756 0
[attach-enode] #381 0
[mk-app] #759 = #190 #378
[mk-app] #760 <= #378 #190
[mk-app] #761 >= #378 #190
[attach-enode] #759 0
[attach-enode] #394 0
[mk-app] #762 = #175 #393
[mk-app] #763 <= #393 #175
[mk-app] #764 >= #393 #175
[attach-enode] #762 0
[attach-enode] #396 0
[mk-app] #765 = #190 #393
[mk-app] #766 <= #393 #190
[mk-app] #767 >= #393 #190
[attach-enode] #765 0
[attach-enode] #399 0
[mk-app] #768 = #175 #398
[mk-app] #769 <= #398 #175
[mk-app] #770 >= #398 #175
[attach-enode] #768 0
[attach-enode] #401 0
[mk-app] #771 = #190 #398
[mk-app] #772 <= #398 #190
[mk-app] #773 >= #398 #190
[attach-enode] #771 0
[attach-enode] #414 0
[mk-app] #774 = #175 #413
[mk-app] #775 <= #413 #175
[mk-app] #776 >= #413 #175
[attach-enode] #774 0
[attach-enode] #416 0
[mk-app] #777 = #190 #413
[mk-app] #778 <= #413 #190
[mk-app] #779 >= #413 #190
[attach-enode] #777 0
[attach-enode] #419 0
[mk-app] #780 = #175 #418
[mk-app] #781 <= #418 #175
[mk-app] #782 >= #418 #175
[attach-enode] #780 0
[attach-enode] #421 0
[mk-app] #783 = #190 #418
[mk-app] #784 <= #418 #190
[mk-app] #785 >= #418 #190
[attach-enode] #783 0
[push] 0
[assign] (not #587) decision axiom
[assign] #421 bin -300
[assign] #641 bin -300
[assign] (not #643) bin 93
[assign] #500 bin -97
[assign] #490 bin -97
[assign] (not #663) justification -1: -97
[assign] #783 justification -1: 296
[assign] #660 justification -1: 93
[assign] (not #416) justification -1: -97 296 93
[assign] (not #777) justification -1: -97 296 93
[assign] #785 bin 297
[assign] #784 bin 297
[assign] #662 bin 94
[assign] #661 bin 94
[assign] #664 bin 298
[assign] (not #665) bin 298
[assign] (not #778) bin 96
[assign] #779 bin 96
[assign] #775 bin 95
[assign] (not #776) bin 95
[assign] #781 bin 99
[assign] (not #782) bin 99
[assign] (not #774) bin -284
[assign] (not #780) bin -294
[mk-app] #786 = #9 #8
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[push] 1
[assign] (not #585) decision axiom
[assign] #419 bin -295
[push] 2
[assign] (not #414) decision axiom
[push] 3
[assign] (not #579) decision axiom
[assign] #401 bin -280
[assign] #636 bin -280
[assign] (not #638) bin 85
[assign] #491 bin -89
[assign] #481 bin -89
[assign] (not #527) justification -1: -89
[assign] #771 justification -1: 276
[assign] #432 justification -1: 85
[assign] #399 justification -1: 291 276 296
[assign] #768 justification -1: 291 276 296
[assign] (not #394) justification -1: -281 85 93
[assign] (not #762) justification -1: -281 85 93
[assign] (not #396) justification -1: -97 296 85
[assign] (not #765) justification -1: -97 296 85
[assign] #773 bin 277
[assign] #772 bin 277
[assign] #526 bin 86
[assign] #525 bin 86
[assign] (not #577) clause -275 -271 -85
[assign] #770 bin 272
[assign] #769 bin 272
[assign] #528 bin 278
[assign] (not #659) bin 278
[assign] (not #766) bin 88
[assign] #767 bin 88
[assign] #763 bin 87
[assign] (not #764) bin 87
[resolve-lit] 0 (not #528)
[resolve-process] #528
[resolve-lit] 0 (not #770)
[resolve-process] (not #528)
[resolve-lit] 0 (not #772)
[resolve-process] (not #770)
[resolve-lit] 0 (not #768)
[resolve-process] (not #772)
[resolve-lit] 0 (not #771)
[resolve-process] (not #768)
[resolve-lit] 2 (not #419)
[resolve-lit] 0 (not #401)
[resolve-lit] 3 (not #421)
[resolve-process] (not #771)
[conflict] (not #401) (not #419) (not #421)
[pop] 2 4
[assign] (not #401) clause -276 -291 -296
[assign] #579 bin -276
[assign] (not #771) justification -1: -276
[push] 2
[assign] (not #528) decision axiom
[assign] #770 bin -91
[assign] #659 bin -91
[assign] #773 bin -91
[assign] (not #772) bin -91
[assign] (not #527) bin -91
[assign] (not #638) justification -1: -90
[assign] (not #536) clause -83 91 -298
[assign] #524 clause 84 91 -298
[assign] (not #757) clause -253 91 -298
[assign] #758 clause 254 91 -298
[assign] (not #760) clause -258 91 -298
[assign] #761 clause 259 91 -298
[assign] #491 bin -89
[assign] #481 bin -89
[assign] (not #535) bin -83
[assign] (not #756) bin -253
[assign] (not #759) bin -258
[assign] (not #577) clause -275 -270 -280 -265
[assign] #399 bin -275
[assign] #636 bin -275
[assign] #768 justification -1: 271
[assign] #432 justification -1: 85
[resolve-lit] 0 (not #419)
[resolve-process] #419
[resolve-lit] 1 #780
[conflict] (not #419) #780
[pop] 2 3
[assign] (not #419) clause -291 292
[assign] #585 bin -291
[assign] (not #414) justification -1: -282
[push] 1
[assign] (not #770) decision axiom
[assign] #769 bin -274
[assign] #528 bin -274
[assign] (not #768) bin -274
[push] 2
[assign] (not #772) decision axiom
[assign] #659 bin -278
[assign] #773 bin -278
[assign] (not #771) bin -278
[assign] #527 clause 90 -92 -91
[push] 3
[assign] (not #401) decision axiom
[assign] #579 bin -276
[push] 4
[assign] (not #687) decision axiom
[push] 5
[assign] (not #577) decision axiom
[assign] #399 bin -275
[assign] #636 bin -275
[assign] (not #638) bin 85
[assign] #491 bin -89
[assign] #481 bin -89
[resolve-lit] 3 (not #527)
[resolve-process] #527
[resolve-lit] 0 #638
[conflict] #638 (not #527)
[pop] 3 6
[assign] #638 clause 89 -90
[assign] (not #636) bin 89
[assign] #579 bin -85
[assign] #577 bin -85
[assign] (not #401) justification -1: -277
[assign] (not #399) justification -1: -272
[assign] (not #432) justification -1: -85
[mk-app] #786 = #14 #12
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #756
[end-of-instance]
[assign] (not #536) clause -83 -92 -298
[assign] #524 clause 84 -92 -298
[assign] #758 clause 254 -92 -298
[assign] (not #760) clause -258 -92 -298
[assign] #761 clause 259 -92 -298
[assign] #757 clause 253 274 -299
[assign] (not #535) bin -83
[assign] (not #759) bin -258
[assign] #756 clause 252 -253 -254
[assign] #379 justification -1: 299 -274 298 92
[assign] (not #633) justification -1: -281 93 299 -274 298 92
[assign] (not #381) justification -1: -291 296 299 -274 298 92
[assign] #482 bin -81
[assign] #472 bin -81
[assign] #571 bin -256
[assign] (not #569) clause -255 -245 -250 -260
[assign] #631 bin -255
[assign] #544 justification -1: 77
[assign] (not #374) justification -1: -281 77 93
[assign] (not #750) justification -1: -281 77 93
[assign] (not #376) justification -1: -97 296 77
[assign] (not #753) justification -1: -97 296 77
[assign] #534 bin 78
[assign] #533 bin 78
[assign] #755 bin 80
[assign] (not #754) bin 80
[assign] #751 bin 79
[assign] (not #752) bin 79
[mk-app] #786 = #8 #7
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[push] 3
[assign] (not #520) decision axiom
[assign] #232 bin -135
[assign] #605 bin -135
[assign] (not #601) bin 29
[assign] #425 bin -33
[assign] #518 bin -33
[assign] (not #596) justification -1: -33
[assign] #684 justification -1: 131
[assign] #511 justification -1: 29
[assign] (not #235) justification -1: -291 296 131
[assign] (not #687) justification -1: -291 296 131
[assign] (not #227) justification -1: -97 296 29
[assign] (not #678) justification -1: -97 296 29
[assign] (not #224) justification -1: -281 29 93
[assign] (not #681) justification -1: -281 29 93
[assign] #686 bin 132
[assign] #685 bin 132
[assign] #595 bin 30
[assign] #594 bin 30
[assign] #430 bin -136
[assign] #597 bin 134
[assign] (not #513) bin 134
[assign] #680 bin 32
[assign] (not #679) bin 32
[assign] #682 bin 31
[assign] (not #683) bin 31
[assign] (not #688) bin 36
[assign] #689 bin 36
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #708
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #106
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #114
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #122
[end-of-instance]
[assign] (not #584) clause -51 35 -92
[assign] #573 clause 52 35 -92
[assign] #710 clause 174 35 -92
[assign] (not #712) clause -178 35 -92
[assign] #713 clause 179 35 -92
[assign] #709 clause 173 -133 274
[assign] (not #590) clause -43 35 -92 -298
[assign] #591 clause 44 35 -92 -298
[assign] (not #697) clause -153 35 -92 -298
[assign] #698 clause 154 35 -92 -298
[assign] (not #700) clause -158 35 -92 -298
[assign] #701 clause 159 35 -92 -298
[assign] (not #583) bin -51
[assign] (not #711) bin -178
[assign] #708 clause 172 -173 -174
[assign] (not #589) bin -43
[assign] (not #696) bin -153
[assign] (not #699) bin -158
[assign] #292 justification -1: 133 -35 92 -274
[assign] (not #613) justification -1: -281 93 133 -35 92 -274
[assign] (not #295) justification -1: -291 296 133 -35 92 -274
[assign] #446 bin -49
[assign] #436 bin -49
[assign] #539 bin -176
[assign] (not #537) clause -175 -165 -170 -180
[assign] #611 bin -175
[assign] #592 justification -1: 45
[assign] (not #284) justification -1: -281 45 93
[assign] (not #702) justification -1: -281 45 93
[assign] (not #287) justification -1: -97 296 45
[assign] (not #705) justification -1: -97 296 45
[assign] #582 bin 46
[assign] #581 bin 46
[assign] (not #706) bin 48
[assign] #707 bin 48
[assign] #703 bin 47
[assign] (not #704) bin 47
[push] 4
[assign] (not #491) decision axiom
[assign] #396 bin -270
[assign] #765 justification -1: 266
[assign] (not #394) justification -1: -291 266 296
[assign] (not #762) justification -1: -291 266 296
[assign] #767 bin 267
[assign] #766 bin 267
[assign] #481 bin -261
[assign] #525 bin 268
[assign] (not #526) bin 268
[assign] #763 bin 87
[assign] (not #764) bin 87
[resolve-process] true
[resolve-lit] 0 (not #766)
[resolve-lit] 1 (not #594)
[resolve-lit] 1 #706
[conflict] (not #766) (not #594) #706
[pop] 1 5
[assign] (not #766) clause -268 -31 168
[assign] #526 bin -268
[assign] #767 bin -268
[assign] (not #765) bin -268
[assign] (not #525) clause -87 -88 86
[assign] #764 bin -87
[assign] (not #396) justification -1: -267
[resolve-process] true
[resolve-lit] 0 (not #764)
[resolve-lit] 0 #679
[resolve-lit] 0 (not #581)
[resolve-process] (not #764)
[resolve-lit] 0 #525
[resolve-process] #525
[resolve-lit] 0 (not #526)
[resolve-lit] 1 #432
[resolve-process] (not #526)
[resolve-lit] 0 #766
[resolve-process] #766
[resolve-lit] 0 (not #594)
[resolve-lit] 0 #706
[resolve-process] #706
[resolve-lit] 0 (not #582)
[resolve-process] (not #581)
[resolve-lit] 0 (not #592)
[resolve-process] (not #582)
[resolve-process] (not #592)
[resolve-lit] 0 (not #611)
[resolve-process] (not #611)
[resolve-lit] 0 #537
[resolve-process] #537
[resolve-lit] 0 (not #436)
[resolve-lit] 0 (not #446)
[resolve-lit] 0 (not #539)
[resolve-process] (not #539)
[resolve-lit] 0 #295
[resolve-process] (not #436)
[resolve-lit] 0 #613
[resolve-process] (not #446)
[resolve-process] #295
[resolve-lit] 3 #419
[resolve-lit] 3 (not #421)
[resolve-lit] 0 (not #685)
[resolve-lit] 0 #513
[resolve-lit] 1 (not #659)
[resolve-lit] 2 #770
[resolve-process] #613
[resolve-lit] 3 #414
[resolve-lit] 3 (not #641)
[resolve-process] #679
[resolve-lit] 0 (not #595)
[resolve-process] #513
[resolve-lit] 0 (not #686)
[resolve-process] (not #594)
[resolve-lit] 0 (not #511)
[resolve-process] (not #595)
[resolve-process] (not #685)
[resolve-lit] 0 (not #684)
[resolve-process] (not #686)
[resolve-process] (not #511)
[resolve-lit] 0 (not #605)
[resolve-process] (not #684)
[resolve-lit] 0 (not #232)
[resolve-process] (not #605)
[resolve-lit] 0 #520
[resolve-process] (not #232)
[conflict] #520 (not #421) (not #659) #770 (not #641)
[pop] 1 4
[assign] #520 clause 135 -92 -296 274 -93
[push] 3
[assign] (not #766) decision axiom
[assign] #526 bin -268
[assign] #767 bin -268
[assign] (not #765) bin -268
[assign] (not #525) clause -87 -88 86
[assign] #764 bin -87
[assign] (not #396) justification -1: -267
[resolve-process] true
[resolve-lit] 1 (not #533)
[resolve-lit] 3 (not #661)
[resolve-lit] 0 (not #764)
[conflict] (not #764) (not #533) (not #661)
[pop] 1 4
[assign] (not #764) clause -264 -79 -95
[assign] #763 bin -264
[assign] #525 bin -264
[assign] (not #762) bin -264
[assign] (not #526) clause -88 -87 86
[assign] #766 bin -88
[assign] (not #394) justification -1: -262
[resolve-process] true
[resolve-lit] 0 #754
[resolve-lit] 2 #778
[resolve-lit] 0 #526
[resolve-process] #526
[resolve-lit] 0 (not #525)
[resolve-lit] 0 #432
[resolve-process] (not #525)
[resolve-lit] 0 #764
[resolve-process] #764
[resolve-lit] 0 (not #533)
[resolve-lit] 2 (not #661)
[resolve-process] #754
[resolve-lit] 0 (not #534)
[resolve-process] (not #533)
[resolve-lit] 0 (not #544)
[resolve-process] (not #534)
[resolve-process] (not #544)
[resolve-lit] 0 (not #631)
[resolve-process] (not #631)
[resolve-lit] 0 #569
[resolve-process] #569
[resolve-lit] 0 (not #472)
[resolve-lit] 0 (not #482)
[resolve-lit] 0 (not #571)
[resolve-process] (not #571)
[resolve-lit] 0 #381
[resolve-process] (not #472)
[resolve-lit] 0 #633
[resolve-process] (not #482)
[resolve-process] #381
[resolve-lit] 2 #419
[resolve-lit] 2 (not #421)
[resolve-lit] 2 (not #785)
[resolve-lit] 1 #770
[resolve-lit] 2 (not #784)
[resolve-lit] 0 (not #659)
[resolve-process] #633
[resolve-lit] 2 #414
[resolve-lit] 2 (not #641)
[resolve-process] #432
[resolve-lit] 0 #636
[resolve-process] #636
[resolve-lit] 0 (not #638)
[resolve-process] (not #638)
[resolve-lit] 0 (not #527)
[resolve-process] (not #527)
[resolve-lit] 1 (not #528)
[conflict] (not #659) (not #421) #770 (not #641)
[pop] 1 3
[assign] #757 clause 253 274 -299
[assign] (not #659) clause -92 274 -296 -93
[assign] #772 bin -92
[assign] (not #527) bin -92
[assign] (not #399) justification -1: -272
[assign] (not #638) justification -1: -90
[mk-app] #786 = #393 #373
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[mk-app] #786 = #283 #253
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[assign] #536 clause 83 92 -299
[assign] (not #758) clause -254 92 -299
[assign] #577 bin -271
[assign] #491 bin -89
[assign] #481 bin -89
[assign] (not #756) bin -254
[assign] (not #579) clause -280 -265 -270 -275
[assign] #401 bin -280
[assign] #636 bin -280
[assign] #771 justification -1: 276
[assign] #432 justification -1: 85
[assign] #631 justification -1: 85 95 -288
[assign] (not #394) justification -1: -281 85 93
[assign] (not #762) justification -1: -281 85 93
[assign] (not #396) justification -1: -97 296 85
[assign] (not #765) justification -1: -97 296 85
[assign] (not #374) justification -1: -281 85 93 95 -288
[assign] (not #750) justification -1: -281 85 93 95 -288
[assign] (not #376) justification -1: -97 296 85 95 -288
[assign] (not #753) justification -1: -97 296 85 95 -288
[assign] #773 bin 277
[assign] #526 bin 86
[assign] #525 bin 86
[assign] (not #633) bin 77
[assign] #472 bin -241
[assign] #482 bin -246
[assign] (not #766) bin 88
[assign] #767 bin 88
[assign] #763 bin 87
[assign] (not #764) bin 87
[assign] #544 justification -1: 77
[assign] (not #535) justification -1: -81
[assign] (not #379) justification -1: -252
[mk-app] #786 = #13 #12
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #535
[end-of-instance]
[mk-app] #786 = #231 #261
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[mk-app] #786 = #283 #223
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #154
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #162
[end-of-instance]
[assign] #524 clause 84 -279 -298
[assign] (not #760) clause -258 -279 -298
[assign] #761 clause 259 -279 -298
[assign] #534 clause 80 268 -95
[assign] (not #754) clause -248 268 -95
[assign] #755 clause 249 268 -95
[assign] #533 clause 79 -87 288
[assign] #751 clause 243 -87 288
[assign] (not #752) clause -244 -87 288
[resolve-process] true
[resolve-lit] 0 (not #524)
[resolve-lit] 0 #535
[resolve-lit] 0 (not #536)
[resolve-process] (not #524)
[resolve-lit] 0 (not #773)
[resolve-lit] 1 (not #784)
[resolve-process] #535
[resolve-lit] 0 #633
[resolve-process] #633
[resolve-lit] 0 (not #631)
[resolve-process] (not #773)
[resolve-lit] 0 (not #771)
[resolve-process] (not #631)
[resolve-lit] 0 (not #636)
[resolve-lit] 1 (not #661)
[resolve-lit] 1 #778
[resolve-process] (not #771)
[resolve-lit] 0 (not #401)
[resolve-process] (not #636)
[resolve-lit] 0 #579
[resolve-process] (not #401)
[resolve-process] #579
[resolve-lit] 0 (not #481)
[resolve-lit] 0 (not #491)
[resolve-lit] 0 (not #577)
[resolve-process] (not #481)
[resolve-lit] 0 #638
[resolve-process] (not #491)
[resolve-process] (not #577)
[resolve-lit] 0 #399
[resolve-process] (not #536)
[resolve-lit] 0 #659
[resolve-lit] 1 (not #785)
[resolve-process] #638
[resolve-lit] 0 #527
[resolve-process] #399
[resolve-lit] 0 #768
[resolve-process] #527
[resolve-process] #659
[resolve-lit] 0 #770
[resolve-lit] 1 (not #421)
[resolve-lit] 1 (not #641)
[resolve-process] #768
[conflict] #770 (not #421) (not #641)
[pop] 1 2
[assign] #770 clause 274 -296 -93
[assign] (not #528) bin 274
[assign] #659 bin 274
[assign] #773 bin -91
[assign] (not #772) bin -91
[assign] (not #527) bin -91
[assign] (not #536) clause -83 91 -298
[assign] #524 clause 84 91 -298
[assign] (not #757) clause -253 91 -298
[assign] #758 clause 254 91 -298
[assign] (not #760) clause -258 91 -298
[assign] #761 clause 259 91 -298
[assign] (not #771) bin -278
[assign] (not #535) bin -83
[assign] (not #756) bin -253
[assign] (not #759) bin -258
[assign] (not #638) justification -1: -90
[assign] (not #401) justification -1: -277
[mk-app] #786 = #393 #373
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[mk-app] #786 = #283 #253
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[assign] #491 bin -89
[assign] #481 bin -89
[assign] #579 bin -276
[assign] (not #577) clause -275 -280 -270 -265
[assign] #399 bin -275
[assign] #636 bin -275
[assign] #768 justification -1: 271
[assign] #432 justification -1: 85
[assign] #631 justification -1: 85 95 -288
[assign] (not #394) justification -1: -281 85 93
[assign] (not #762) justification -1: -281 85 93
[assign] (not #396) justification -1: -97 296 85
[assign] (not #765) justification -1: -97 296 85
[assign] (not #374) justification -1: -281 85 93 95 -288
[assign] (not #750) justification -1: -281 85 93 95 -288
[assign] (not #376) justification -1: -97 296 85 95 -288
[assign] (not #753) justification -1: -97 296 85 95 -288
[assign] #769 bin 272
[assign] #526 bin 86
[assign] #525 bin 86
[assign] (not #633) bin 77
[assign] #472 bin -241
[assign] #482 bin -246
[assign] (not #766) bin 88
[assign] #767 bin 88
[assign] #763 bin 87
[assign] (not #764) bin 87
[assign] #533 clause 79 -87 288
[assign] #751 clause 243 -87 288
[assign] (not #752) clause -244 -87 288
[assign] #534 clause 80 268 -95
[assign] (not #754) clause -248 268 -95
[assign] #755 clause 249 268 -95
[assign] #544 clause 78 -79 -80
[assign] (not #381) justification -1: -257
[assign] (not #379) justification -1: -252
[mk-app] #786 = #283 #223
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #154
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #162
[end-of-instance]
[assign] #571 bin -256
[assign] #569 bin -251
[resolve-process] true
[resolve-lit] 0 (not #569)
[resolve-lit] 0 (not #571)
[resolve-lit] 0 (not #482)
[resolve-lit] 0 (not #472)
[resolve-process] (not #569)
[resolve-lit] 0 #379
[resolve-process] (not #571)
[resolve-lit] 0 #381
[resolve-process] #379
[resolve-lit] 0 #756
[resolve-process] #381
[resolve-lit] 0 #759
[resolve-process] (not #482)
[resolve-lit] 0 #376
[resolve-process] (not #472)
[resolve-lit] 0 #374
[resolve-process] #376
[resolve-lit] 0 #643
[resolve-lit] 0 (not #421)
[resolve-lit] 0 (not #636)
[resolve-lit] 0 (not #661)
[resolve-lit] 0 #778
[resolve-process] #374
[resolve-lit] 0 #414
[resolve-lit] 0 (not #641)
[resolve-process] (not #636)
[resolve-lit] 0 #577
[resolve-process] #577
[resolve-lit] 0 (not #579)
[resolve-lit] 0 (not #491)
[resolve-lit] 0 (not #481)
[resolve-process] (not #579)
[resolve-lit] 0 #401
[resolve-process] (not #481)
[resolve-lit] 0 #638
[resolve-process] (not #491)
[resolve-process] #401
[resolve-lit] 0 #771
[resolve-process] #638
[resolve-lit] 0 #527
[resolve-process] #759
[resolve-lit] 0 #760
[resolve-process] #756
[resolve-lit] 0 #757
[resolve-process] #771
[resolve-lit] 0 #772
[resolve-process] #760
[resolve-lit] 0 #528
[resolve-lit] 0 (not #784)
[resolve-process] #757
[resolve-process] #527
[resolve-process] #772
[resolve-process] #528
[resolve-lit] 0 (not #770)
[resolve-process] (not #770)
[resolve-process] #414
[resolve-lit] 0 #774
[resolve-process] #774
[resolve-lit] 0 #776
[resolve-process] #776
[resolve-process] #778
[resolve-lit] 0 (not #662)
[resolve-process] (not #661)
[resolve-lit] 0 (not #660)
[resolve-process] (not #662)
[resolve-process] (not #784)
[resolve-lit] 0 (not #783)
[resolve-process] (not #660)
[resolve-process] (not #783)
[resolve-process] #643
[resolve-process] (not #641)
[resolve-lit] 0 #587
[resolve-process] (not #421)
[conflict] #587
[pop] 1 1
[assign] #587 axiom
[push] 0
[assign] (not #770) decision axiom
[assign] #769 bin -274
[assign] #528 bin -274
[assign] (not #768) bin -274
[push] 1
[assign] (not #421) decision axiom
[assign] (not #783) justification -1: -296
[push] 2
[assign] (not #661) decision axiom
[assign] #776 bin -95
[assign] #662 bin -95
[assign] (not #778) bin -95
[assign] #779 bin -95
[assign] (not #660) bin -95
[assign] (not #777) bin -288
[push] 3
[assign] (not #641) decision axiom
[assign] #585 bin -93
[assign] (not #416) justification -1: -287
[assign] #500 bin -286
[assign] (not #490) clause -285 -290 -300 -295
[assign] #643 bin -285
[assign] #414 bin -285
[assign] #663 justification -1: 97
[assign] #774 justification -1: 281
[assign] (not #419) justification -1: -93 97 281
[assign] (not #780) justification -1: -93 97 281
[assign] #665 bin 98
[assign] #664 bin 98
[assign] #775 bin 282
[assign] (not #784) bin 100
[assign] #785 bin 100
[assign] #781 bin 99
[assign] (not #782) bin 99
[assign] #757 clause 253 -299 274
[mk-app] #786 = #14 #13
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[mk-app] #786 = #398 #378
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[push] 4
[assign] (not #527) decision axiom
[assign] (not #659) clause -92 90 -91
[assign] #772 bin -92
[assign] #536 clause 83 92 -299
[assign] (not #758) clause -254 92 -299
[assign] (not #756) bin -254
[push] 5
[assign] (not #638) decision axiom
[assign] #491 bin -89
[assign] #481 bin -89
[assign] (not #535) justification -1: -89 99 -298
[assign] (not #633) justification -1: -89 99 -298
[assign] (not #399) justification -1: -272
[assign] (not #379) justification -1: -272 99 -298
[assign] (not #524) clause -84 -278 298
[assign] #760 clause 258 -278 298
[assign] #482 bin -81
[assign] #472 bin -81
[assign] #577 bin -271
[assign] #569 bin -251
[assign] (not #579) clause -280 -275 -270 -265
[assign] (not #571) clause -260 -255 -250 -245
[assign] #401 bin -280
[assign] #636 bin -280
[assign] #381 bin -260
[assign] #631 bin -260
[assign] #771 justification -1: 256 99 -298
[assign] #759 justification -1: 256
[assign] #432 justification -1: 85
[assign] #544 justification -1: 77
[assign] (not #394) justification -1: -291 85 97
[assign] (not #762) justification -1: -291 85 97
[assign] (not #396) justification -1: -296 85 97
[assign] (not #765) justification -1: -296 85 97
[assign] (not #374) justification -1: -291 77 97
[assign] (not #750) justification -1: -291 77 97
[assign] (not #376) justification -1: -296 77 97
[assign] (not #753) justification -1: -296 77 97
[assign] #773 bin 277
[assign] #761 bin 257
[assign] #526 bin 86
[assign] #525 bin 86
[assign] #534 bin 78
[assign] #533 bin 78
[assign] (not #766) bin 88
[assign] #767 bin 88
[assign] #763 bin 87
[assign] (not #764) bin 87
[assign] #751 clause 243 -87 288
[assign] (not #752) clause -244 -87 288
[assign] #755 bin 80
[assign] (not #754) bin 80
[resolve-process] true
[resolve-lit] 0 #754
[resolve-lit] 3 (not #776)
[resolve-lit] 0 (not #525)
[resolve-process] #754
[resolve-lit] 0 (not #534)
[resolve-process] (not #534)
[resolve-lit] 0 (not #544)
[resolve-process] (not #525)
[resolve-lit] 0 (not #432)
[resolve-process] (not #544)
[resolve-lit] 0 (not #631)
[resolve-process] (not #432)
[resolve-lit] 0 (not #636)
[resolve-process] (not #631)
[resolve-lit] 0 #571
[resolve-process] (not #636)
[resolve-lit] 0 #579
[resolve-process] #571
[resolve-lit] 0 (not #569)
[resolve-lit] 0 (not #482)
[resolve-lit] 0 (not #472)
[resolve-process] #579
[resolve-lit] 0 (not #577)
[resolve-lit] 0 (not #491)
[resolve-lit] 0 (not #481)
[resolve-process] (not #569)
[resolve-lit] 0 #379
[resolve-process] (not #577)
[resolve-lit] 0 #399
[resolve-process] (not #472)
[resolve-lit] 0 #633
[resolve-process] (not #482)
[resolve-process] #379
[resolve-lit] 5 #768
[resolve-lit] 2 (not #664)
[resolve-lit] 2 #784
[resolve-process] #399
[resolve-process] #633
[resolve-lit] 0 #638
[resolve-process] (not #481)
[resolve-process] (not #491)
[conflict] #638 (not #776) #768 (not #664) #784
[pop] 2 6
[assign] #638 clause 89 -99 272 -284 298
[assign] (not #636) bin 89
[assign] #579 bin -85
[assign] #577 bin -85
[assign] (not #399) justification -1: -272
[assign] (not #756) justification -1: -272 99 -298
[assign] (not #379) justification -1: -272 99 -298
[assign] #535 justification -1: 89 99 -298
[assign] #633 justification -1: 89 99 -298
[assign] #527 justification -1: 89
[assign] (not #432) justification -1: -85
[assign] (not #381) justification -1: -296 89 97 99 -298
[assign] (not #771) justification -1: -296 89 97 99 -298
[assign] (not #401) justification -1: -296 89 97 99 -298
[assign] (not #759) justification -1: -296 89 97 99 -298
[assign] #536 clause 83 298 274
[assign] (not #758) clause -254 298 274
[assign] #569 bin -251
[assign] #524 bin 82
[assign] (not #631) bin 81
[assign] #659 bin 90
[assign] #571 bin -256
[assign] (not #760) bin 84
[assign] #761 bin 84
[assign] (not #772) clause -278 -84 298
[assign] #773 bin 92
[assign] (not #544) justification -1: -77
[mk-app] #786 = #13 #12
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[mk-app] #786 = #231 #261
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[mk-app] #786 = #231 #291
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[push] 4
[assign] (not #491) decision axiom
[assign] #396 bin -270
[assign] #765 justification -1: 266
[assign] (not #394) justification -1: -286 281 266
[assign] (not #762) justification -1: -286 281 266
[assign] #767 bin 267
[assign] #766 bin 267
[assign] #481 bin -261
[assign] #525 bin 268
[assign] (not #526) bin 268
[assign] #763 bin 87
[assign] (not #764) bin 87
[assign] #533 clause 79 -87 288
[assign] #751 clause 243 -87 288
[assign] (not #752) clause -244 -87 288
[assign] (not #534) clause -80 -79 78
[assign] (not #750) bin -244
[assign] #754 bin -80
[assign] (not #374) justification -1: -242
[assign] (not #755) clause -249 -268 -284
[assign] #472 bin -241
[assign] (not #753) bin -249
[assign] (not #482) clause -250 -245 -255 -260
[assign] #376 bin -250
[resolve-lit] 0 (not #376)
[resolve-process] #376
[resolve-lit] 0 #753
[resolve-process] (not #376)
[resolve-lit] 0 #482
[resolve-process] #482
[resolve-lit] 0 (not #472)
[resolve-lit] 1 (not #569)
[resolve-lit] 1 (not #571)
[resolve-process] #753
[resolve-lit] 0 #755
[resolve-process] (not #472)
[resolve-lit] 0 #374
[resolve-process] #755
[resolve-lit] 0 (not #766)
[resolve-lit] 2 (not #776)
[resolve-process] #374
[resolve-lit] 0 #750
[resolve-process] #750
[resolve-lit] 0 #752
[resolve-process] #752
[resolve-lit] 0 (not #525)
[resolve-lit] 2 #778
[resolve-process] (not #525)
[conflict] (not #766) (not #569) (not #571) (not #776) #778
[pop] 1 5
[assign] (not #766) clause -268 -255 -260 -284 288
[assign] #526 bin -268
[assign] #767 bin -268
[assign] (not #765) bin -268
[assign] (not #525) clause -87 -88 86
[assign] #764 bin -87
[assign] (not #396) justification -1: -267
[assign] #534 clause 80 -264 -283
[assign] (not #754) clause -248 -264 -283
[assign] #755 clause 249 -264 -283
[assign] #491 bin -266
[assign] (not #533) clause -79 -80 78
[assign] (not #753) bin -248
[assign] (not #481) clause -265 -270 -280 -275
[assign] #752 bin -79
[assign] #394 bin -265
[assign] (not #376) justification -1: -247
[assign] #762 justification -1: 261
[assign] (not #763) clause -263 -244 -284
[assign] #482 bin -246
[resolve-lit] 0 #763
[resolve-process] (not #763)
[resolve-lit] 0 (not #762)
[resolve-process] #763
[resolve-lit] 0 (not #752)
[resolve-lit] 1 (not #776)
[resolve-process] (not #762)
[resolve-lit] 0 (not #394)
[resolve-process] (not #394)
[resolve-lit] 0 #481
[resolve-process] (not #752)
[resolve-lit] 0 #533
[resolve-process] #481
[resolve-lit] 0 (not #491)
[resolve-lit] 0 (not #579)
[resolve-lit] 0 (not #577)
[resolve-process] #533
[resolve-lit] 0 (not #534)
[resolve-lit] 0 #544
[resolve-process] (not #491)
[resolve-lit] 0 #396
[resolve-process] (not #534)
[resolve-lit] 0 (not #764)
[resolve-lit] 0 (not #775)
[resolve-process] #396
[resolve-lit] 0 #765
[resolve-process] (not #764)
[resolve-lit] 0 #525
[resolve-process] #525
[resolve-lit] 0 (not #526)
[resolve-lit] 0 #432
[resolve-process] #765
[resolve-lit] 0 #766
[resolve-process] (not #526)
[resolve-process] #766
[resolve-lit] 0 (not #569)
[resolve-lit] 0 (not #571)
[resolve-lit] 1 #778
[resolve-process] #544
[resolve-lit] 0 #631
[resolve-process] (not #571)
[resolve-lit] 0 #381
[resolve-process] #631
[resolve-lit] 0 (not #633)
[resolve-process] (not #569)
[resolve-lit] 0 #379
[resolve-process] #381
[resolve-lit] 2 #421
[resolve-lit] 0 (not #638)
[resolve-lit] 0 (not #643)
[resolve-lit] 0 (not #664)
[resolve-lit] 0 #784
[resolve-process] #432
[resolve-lit] 0 #636
[resolve-process] (not #633)
[resolve-process] #379
[resolve-lit] 3 #768
[resolve-process] (not #577)
[resolve-process] (not #579)
[resolve-process] #636
[resolve-process] (not #638)
[resolve-process] #784
[resolve-lit] 0 (not #665)
[resolve-process] (not #775)
[resolve-lit] 0 (not #774)
[resolve-process] (not #664)
[resolve-lit] 0 (not #663)
[resolve-process] (not #665)
[resolve-process] (not #774)
[resolve-lit] 0 (not #414)
[resolve-process] (not #663)
[resolve-process] (not #414)
[resolve-lit] 0 #490
[resolve-process] (not #643)
[conflict] #490 (not #776) #778 #421 #768
[pop] 1 4
[assign] #490 clause 285 -284 288 296 272
[assign] (not #416) justification -1: -287
[assign] (not #641) justification -1: -94
[assign] (not #399) justification -1: -272
[assign] #500 bin -286
[assign] #585 bin -93
[assign] #577 bin -271
[resolve-process] true
[resolve-lit] 0 (not #585)
[resolve-lit] 0 (not #500)
[resolve-lit] 0 (not #490)
[resolve-process] (not #585)
[resolve-lit] 0 #641
[resolve-process] (not #500)
[resolve-lit] 0 #416
[resolve-process] #641
[resolve-lit] 0 #660
[resolve-process] #416
[resolve-lit] 0 #777
[resolve-process] (not #490)
[resolve-lit] 0 (not #776)
[resolve-lit] 0 #778
[resolve-lit] 1 #421
[resolve-lit] 2 #768
[resolve-process] #777
[resolve-process] #660
[resolve-lit] 0 #661
[resolve-process] #778
[resolve-process] (not #776)
[conflict] #661 #421 #768
[pop] 1 3
[assign] #661 clause 95 296 272
[assign] #775 bin 95
[assign] (not #776) bin 95
[assign] (not #774) bin -284
[assign] (not #399) justification -1: -272
[assign] (not #414) justification -1: -282
[assign] #577 bin -271
[assign] #490 bin -281
[push] 2
[assign] (not #778) decision axiom
[assign] #662 bin -288
[assign] #779 bin -288
[assign] (not #777) bin -288
[assign] #660 clause 94 -96 -95
[assign] (not #416) justification -1: -287
[assign] #641 justification -1: 94
[mk-app] #786 = #393 #373
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #170
[end-of-instance]
[assign] #500 bin -286
[assign] (not #643) bin 93
[assign] (not #585) clause -295 -290 -300 -285
[assign] #419 bin -295
[assign] #780 clause 292 -291
[assign] #782 bin 292
[assign] #781 bin 292
[assign] #665 bin 294
[assign] (not #664) bin 294
[assign] (not #784) bin 100
[assign] #785 bin 100
[assign] (not #663) bin -99
[assign] #536 clause 83 298 274
[assign] (not #758) clause -254 298 274
[assign] #757 clause 253 -299 274
[assign] (not #756) bin -254
[assign] (not #524) clause -84 99 274
[assign] #760 clause 258 99 274
[assign] (not #535) bin -84
[push] 3
[assign] (not #638) decision axiom
[assign] #491 bin -89
[assign] #481 bin -89
[assign] (not #527) clause -90 89
[assign] (not #579) clause -280 -265 -270 -275
[assign] (not #659) clause -92 90 -91
[assign] #401 bin -280
[assign] #636 bin -280
[assign] #772 bin -92
[assign] #771 justification -1: 276
[assign] #544 justification -1: 85 95 96
[assign] #631 justification -1: 85 95 96
[assign] #432 justification -1: 85
[assign] (not #374) justification -1: -281 85 94 95 96
[assign] (not #762) justification -1: -281 85 94 95 96
[assign] (not #394) justification -1: -281 85 94 95 96
[assign] (not #750) justification -1: -281 85 94 95 96
[assign] (not #376) justification -1: -286 85 94 95 96
[assign] (not #765) justification -1: -286 85 94 95 96
[assign] (not #396) justification -1: -286 85 94 95 96
[assign] (not #753) justification -1: -286 85 94 95 96
[assign] (not #761) clause -259 92 99
[assign] #773 bin 277
[assign] #534 bin 78
[assign] #533 bin 78
[assign] (not #633) bin 77
[assign] #526 bin 86
[assign] #525 bin 86
[assign] #472 bin -241
[assign] #482 bin -246
[assign] (not #759) bin -259
[assign] #755 bin 80
[assign] (not #754) bin 80
[assign] #751 bin 79
[assign] (not #752) bin 79
[assign] (not #764) clause -264 -79 -95
[assign] (not #766) bin 88
[assign] #767 bin 88
[assign] #763 bin 87
[assign] (not #381) justification -1: -257
[assign] (not #379) justification -1: -252
[mk-app] #786 = #9 #7
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[assign] #571 bin -256
[assign] #569 bin -251
[resolve-process] true
[resolve-lit] 0 (not #569)
[resolve-lit] 0 (not #571)
[resolve-lit] 0 (not #472)
[resolve-lit] 0 (not #482)
[resolve-process] (not #569)
[resolve-lit] 0 #379
[resolve-process] (not #571)
[resolve-lit] 0 #381
[resolve-process] #379
[resolve-lit] 1 #756
[resolve-process] #381
[resolve-lit] 0 #759
[resolve-process] #759
[resolve-lit] 0 #761
[resolve-process] (not #482)
[resolve-lit] 0 #376
[resolve-process] (not #472)
[resolve-lit] 0 #374
[resolve-process] #761
[resolve-lit] 0 #659
[resolve-lit] 1 #664
[resolve-process] #376
[resolve-lit] 1 #416
[resolve-lit] 0 (not #636)
[resolve-lit] 1 (not #660)
[resolve-lit] 2 (not #661)
[resolve-lit] 1 (not #662)
[resolve-process] #374
[resolve-lit] 2 #414
[resolve-process] (not #636)
[resolve-lit] 0 #579
[resolve-process] #659
[resolve-lit] 0 #527
[resolve-lit] 3 (not #528)
[resolve-process] #579
[resolve-lit] 0 (not #481)
[resolve-lit] 0 (not #491)
[resolve-lit] 2 (not #577)
[resolve-process] #527
[resolve-lit] 0 #638
[resolve-process] (not #481)
[resolve-process] (not #491)
[conflict] #638 #756 #416 (not #661) (not #662) (not #528) (not #577)
[pop] 1 4
[assign] #638 clause 89 252 286 -95 -96 -91 -275
[assign] (not #636) bin 89
[assign] #579 bin -85
[assign] (not #379) justification -1: -252
[assign] (not #633) justification -1: -82
[assign] #527 justification -1: 89
[assign] (not #544) justification -1: -85 95 96
[assign] (not #631) justification -1: -85 95 96
[assign] (not #432) justification -1: -85
[assign] (not #401) justification -1: -286 89 94
[assign] (not #771) justification -1: -286 89 94
[assign] #569 bin -251
[assign] #482 bin -81
[assign] #472 bin -81
[assign] #659 bin 90
[assign] #571 bin -77
[resolve-process] true
[resolve-lit] 0 (not #571)
[resolve-lit] 0 (not #569)
[resolve-lit] 0 (not #472)
[resolve-lit] 0 (not #482)
[resolve-process] (not #571)
[resolve-lit] 0 #631
[resolve-process] (not #472)
[resolve-lit] 0 #633
[resolve-process] (not #482)
[resolve-process] (not #569)
[resolve-lit] 0 #379
[resolve-process] #631
[resolve-lit] 0 #636
[resolve-lit] 1 (not #661)
[resolve-lit] 0 (not #662)
[resolve-process] #633
[resolve-lit] 0 #535
[resolve-process] #379
[resolve-lit] 0 #756
[resolve-process] #636
[resolve-lit] 0 (not #638)
[resolve-process] (not #638)
[resolve-lit] 0 #416
[resolve-lit] 2 (not #528)
[resolve-lit] 1 (not #577)
[resolve-process] #535
[resolve-lit] 0 #524
[resolve-process] #524
[resolve-lit] 0 #664
[resolve-lit] 2 #770
[resolve-process] #756
[resolve-lit] 0 #758
[resolve-process] #758
[resolve-lit] 0 #784
[resolve-process] #784
[resolve-lit] 0 (not #665)
[resolve-process] #664
[resolve-lit] 0 (not #782)
[resolve-process] (not #665)
[resolve-process] (not #782)
[resolve-lit] 0 (not #780)
[resolve-process] (not #780)
[resolve-lit] 0 (not #419)
[resolve-process] (not #419)
[resolve-lit] 0 #585
[resolve-process] #585
[resolve-lit] 0 (not #500)
[resolve-lit] 1 (not #490)
[resolve-process] (not #500)
[resolve-process] #416
[resolve-lit] 0 #777
[resolve-process] #777
[resolve-lit] 0 #778
[resolve-process] (not #662)
[conflict] #778 (not #661) #770
[pop] 1 3
[assign] #778 clause 288 -95 274
[assign] (not #662) bin 288
[assign] (not #660) bin -96
[assign] (not #641) justification -1: -94
[assign] #585 bin -93
[assign] (not #500) clause -290 -295 -300 -285
[assign] #643 bin -290
[assign] #416 bin -290
[assign] #663 justification -1: 97
[assign] #777 justification -1: 286
[assign] #665 bin 98
[assign] #664 bin 98
[assign] #779 bin 287
[assign] (not #784) bin 100
[assign] #785 bin 100
[assign] #781 bin 99
[assign] (not #782) bin 99
[assign] #536 clause 83 298 274
[assign] (not #758) clause -254 298 274
[assign] #757 clause 253 -299 274
[assign] (not #780) bin -294
[assign] (not #756) bin -254
[assign] (not #419) clause -291 292
[mk-app] #786 = #398 #378
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[assign] (not #379) justification -1: -271 99 -298
[assign] #569 bin -251
[push] 2
[assign] (not #638) decision axiom
[assign] #491 bin -89
[assign] #481 bin -89
[assign] (not #527) clause -90 89
[assign] (not #579) clause -280 -265 -270 -275
[assign] (not #659) clause -92 90 -91
[assign] #401 bin -280
[assign] #636 bin -280
[assign] #772 bin -92
[assign] (not #524) clause -84 -278 298
[assign] #760 clause 258 -278 298
[assign] (not #535) bin -84
[assign] (not #633) justification -1: -89 99 -298
[assign] #759 justification -1: 276 99 -298
[assign] #381 justification -1: 276 99 -298
[assign] #771 justification -1: 276
[assign] #432 justification -1: 85
[assign] (not #394) justification -1: -291 85 97
[assign] (not #762) justification -1: -291 85 97
[assign] (not #396) justification -1: -296 85 97
[assign] (not #765) justification -1: -296 85 97
[assign] #482 bin -81
[assign] #472 bin -81
[assign] #761 bin 257
[assign] #773 bin 277
[assign] #526 bin 86
[assign] #525 bin 86
[assign] (not #571) clause -260 -245 -255 -250
[assign] (not #766) bin 88
[assign] #767 bin 88
[assign] #763 bin 87
[assign] (not #764) bin 87
[assign] #631 bin -260
[assign] #534 clause 80 268 -95
[assign] (not #754) clause -248 268 -95
[assign] #755 clause 249 268 -95
[assign] (not #753) bin -248
[assign] #544 justification -1: 77
[assign] (not #376) justification -1: -247
[assign] (not #374) justification -1: -291 77 97
[assign] (not #750) justification -1: -291 77 97
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #750
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #172
[end-of-instance]
[mk-app] #786 = #261 #291
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[mk-app] #786 = #9 #7
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[assign] (not #533) clause -79 268 -288
[assign] #752 clause 244 268 -288
[assign] #751 clause 243 -87 -289
[resolve-lit] 0 #533
[resolve-process] (not #533)
[resolve-lit] 0 (not #544)
[resolve-process] #533
[resolve-lit] 0 #766
[resolve-lit] 1 (not #778)
[resolve-process] (not #544)
[resolve-lit] 0 (not #631)
[resolve-process] (not #631)
[resolve-lit] 0 #571
[resolve-process] #766
[resolve-lit] 0 (not #526)
[resolve-process] #571
[resolve-lit] 0 (not #472)
[resolve-lit] 1 (not #569)
[resolve-lit] 0 (not #482)
[resolve-process] (not #526)
[resolve-lit] 0 (not #432)
[resolve-process] (not #472)
[resolve-lit] 0 #633
[resolve-process] (not #482)
[resolve-process] (not #432)
[resolve-lit] 0 (not #636)
[resolve-process] #633
[resolve-lit] 0 #638
[resolve-lit] 1 (not #664)
[resolve-lit] 1 #784
[resolve-process] (not #636)
[resolve-lit] 0 #579
[resolve-process] #579
[resolve-lit] 0 (not #481)
[resolve-lit] 0 (not #491)
[resolve-lit] 1 (not #577)
[resolve-process] (not #481)
[resolve-process] (not #491)
[conflict] #638 (not #778) (not #569) (not #664) #784 (not #577)
[pop] 1 3
[assign] #638 clause 89 -288 -255 -99 298 -275
[assign] (not #636) bin 89
[assign] #579 bin -85
[assign] #535 justification -1: 89 99 -298
[assign] #633 justification -1: 89 99 -298
[assign] #527 justification -1: 89
[assign] (not #432) justification -1: -85
[assign] (not #381) justification -1: -296 89 97 99 -298
[assign] (not #771) justification -1: -296 89 97 99 -298
[assign] (not #401) justification -1: -296 89 97 99 -298
[assign] (not #759) justification -1: -296 89 97 99 -298
[assign] #524 bin 82
[assign] (not #631) bin 81
[assign] #659 bin 90
[assign] #571 bin -256
[assign] (not #760) bin 84
[assign] #761 bin 84
[assign] (not #772) clause -278 -84 298
[assign] #773 bin 92
[assign] (not #544) justification -1: -77
[mk-app] #786 = #13 #12
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #172
[end-of-instance]
[mk-app] #786 = #231 #261
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[mk-app] #786 = #231 #291
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[push] 2
[assign] (not #482) decision axiom
[assign] #376 bin -250
[assign] #753 justification -1: 246
[assign] (not #374) justification -1: -281 246 286
[assign] (not #750) justification -1: -281 246 286
[assign] #755 bin 247
[assign] #754 bin 247
[assign] #472 bin -241
[assign] #533 bin 248
[assign] (not #534) bin 248
[assign] #766 clause 268 -248 -95
[assign] (not #764) clause -264 -248 -283
[assign] #751 bin 79
[assign] (not #752) bin 79
[assign] #525 bin 268
[assign] (not #526) bin 268
[assign] #763 bin -264
[assign] (not #762) bin -264
[assign] (not #394) justification -1: -262
[assign] (not #767) clause -269 -248 -288
[assign] #481 bin -261
[assign] (not #765) bin -269
[assign] (not #491) clause -270 -265 -280 -275
[assign] #396 bin -270
[resolve-lit] 0 (not #396)
[resolve-process] #396
[resolve-lit] 0 #765
[resolve-process] (not #396)
[resolve-lit] 0 #491
[resolve-process] #491
[resolve-lit] 0 (not #481)
[resolve-lit] 1 (not #579)
[resolve-lit] 1 (not #577)
[resolve-process] #765
[resolve-lit] 0 #767
[resolve-process] (not #481)
[resolve-lit] 0 #394
[resolve-process] #767
[resolve-lit] 0 (not #754)
[resolve-lit] 1 (not #778)
[resolve-process] #394
[resolve-lit] 0 #762
[resolve-process] #762
[resolve-lit] 0 #764
[resolve-process] #764
[resolve-lit] 1 (not #775)
[conflict] (not #754) (not #579) (not #577) (not #778) (not #775)
[pop] 1 3
[assign] (not #754) clause -248 -280 -275 -288 -283
[assign] #534 bin -248
[assign] #755 bin -248
[assign] (not #753) bin -248
[assign] (not #533) clause -79 -80 78
[assign] #752 bin -79
[assign] (not #376) justification -1: -247
[assign] #526 clause 88 -244 -289
[assign] (not #766) clause -268 -244 -289
[assign] #767 clause 269 -244 -289
[assign] #482 bin -246
[assign] (not #525) clause -87 -88 86
[assign] (not #765) bin -268
[assign] (not #472) clause -245 -250 -255 -260
[assign] #764 bin -87
[assign] #374 bin -245
[assign] (not #396) justification -1: -267
[assign] #750 justification -1: 241
[assign] (not #751) clause -243 -264 -288
[assign] #491 bin -266
[resolve-lit] 0 #751
[resolve-process] (not #751)
[resolve-lit] 0 (not #750)
[resolve-process] #751
[resolve-lit] 0 (not #764)
[resolve-lit] 0 (not #778)
[resolve-process] (not #750)
[resolve-lit] 0 (not #374)
[resolve-process] (not #374)
[resolve-lit] 0 #472
[resolve-process] (not #764)
[resolve-lit] 0 #525
[resolve-process] #472
[resolve-lit] 0 (not #482)
[resolve-lit] 0 (not #569)
[resolve-lit] 0 (not #571)
[resolve-process] #525
[resolve-lit] 0 (not #526)
[resolve-lit] 0 #432
[resolve-process] (not #482)
[resolve-lit] 0 #376
[resolve-process] (not #526)
[resolve-lit] 0 (not #752)
[resolve-lit] 0 (not #779)
[resolve-process] #376
[resolve-lit] 0 #753
[resolve-process] (not #752)
[resolve-lit] 0 #533
[resolve-process] #533
[resolve-lit] 0 (not #534)
[resolve-lit] 0 #544
[resolve-process] #753
[resolve-lit] 0 #754
[resolve-process] (not #534)
[resolve-process] #754
[resolve-lit] 0 (not #579)
[resolve-lit] 0 (not #577)
[resolve-lit] 0 (not #775)
[resolve-process] #544
[resolve-lit] 0 #631
[resolve-process] (not #571)
[resolve-lit] 0 #381
[resolve-process] #631
[resolve-lit] 0 (not #633)
[resolve-process] #381
[resolve-lit] 0 #421
[resolve-lit] 0 (not #638)
[resolve-lit] 0 (not #643)
[resolve-lit] 0 (not #664)
[resolve-lit] 0 #784
[resolve-process] #432
[resolve-lit] 0 #636
[resolve-process] (not #633)
[resolve-process] (not #579)
[resolve-process] #636
[resolve-process] (not #638)
[resolve-process] (not #569)
[resolve-lit] 0 #379
[resolve-process] #379
[resolve-lit] 0 #399
[resolve-process] #784
[resolve-lit] 0 (not #665)
[resolve-process] (not #779)
[resolve-lit] 0 (not #777)
[resolve-process] (not #664)
[resolve-lit] 0 (not #663)
[resolve-process] (not #665)
[resolve-process] (not #777)
[resolve-lit] 0 (not #416)
[resolve-process] (not #663)
[resolve-process] (not #416)
[resolve-lit] 0 #500
[resolve-process] (not #643)
[resolve-process] #500
[resolve-lit] 0 (not #585)
[resolve-lit] 0 (not #490)
[resolve-process] (not #585)
[resolve-lit] 0 #641
[resolve-process] #641
[resolve-lit] 0 #660
[resolve-process] #660
[resolve-lit] 0 #662
[resolve-process] #662
[resolve-process] (not #778)
[resolve-lit] 0 (not #661)
[resolve-lit] 1 #770
[resolve-process] (not #490)
[resolve-lit] 0 #414
[resolve-process] (not #577)
[resolve-process] #414
[resolve-lit] 0 #774
[resolve-process] #399
[resolve-lit] 1 #768
[resolve-process] #774
[resolve-lit] 0 #776
[resolve-process] #776
[resolve-process] (not #775)
[resolve-process] (not #661)
[conflict] #421 #770
[pop] 1 2
[assign] #421 clause 296 274
[assign] (not #641) clause -93 -296 274
[assign] #585 bin -93
[assign] (not #399) justification -1: -272
[assign] #783 justification -1: 296
[assign] (not #660) justification -1: -93
[assign] #577 bin -271
[assign] #785 bin 297
[assign] #784 bin 297
[assign] #757 clause 253 -299 274
[assign] #664 bin 298
[assign] (not #665) bin 298
[assign] #781 bin 99
[assign] (not #782) bin 99
[assign] (not #663) bin -100
[assign] (not #780) bin -294
[assign] (not #419) clause -291 292
[assign] (not #643) justification -1: -98
[assign] #500 bin -97
[assign] #490 bin -97
[resolve-process] true
[resolve-lit] 0 (not #490)
[resolve-lit] 0 (not #500)
[resolve-lit] 0 (not #585)
[resolve-process] (not #490)
[resolve-lit] 0 #643
[resolve-process] (not #500)
[resolve-process] #643
[resolve-lit] 0 #663
[resolve-process] #663
[resolve-lit] 0 #665
[resolve-process] #665
[resolve-lit] 0 (not #784)
[resolve-process] (not #784)
[resolve-lit] 0 (not #783)
[resolve-process] (not #783)
[resolve-lit] 0 (not #421)
[resolve-process] (not #585)
[resolve-lit] 0 #641
[resolve-process] #641
[resolve-lit] 0 #770
[resolve-process] (not #421)
[conflict] #770
[pop] 1 1
[assign] #770 axiom
[assign] (not #528) bin 274
[assign] #659 bin 274
[assign] #773 bin -91
[assign] (not #772) bin -91
[assign] (not #527) bin -91
[assign] (not #771) bin -278
[assign] (not #638) justification -1: -90
[assign] (not #401) justification -1: -277
[assign] #491 bin -89
[assign] #481 bin -89
[assign] #579 bin -276
[assign] (not #577) clause -275 -265 -280 -270
[assign] #399 bin -275
[assign] #636 bin -275
[assign] #768 justification -1: 271
[assign] #432 justification -1: 85
[assign] (not #394) justification -1: -89 271 85
[assign] (not #762) justification -1: -89 271 85
[assign] #769 bin 272
[assign] #526 bin 86
[assign] #525 bin 86
[assign] (not #766) bin 88
[assign] #767 bin 88
[assign] #763 bin 87
[assign] (not #764) bin 87
[assign] (not #765) bin -268
[assign] (not #396) justification -1: -267
[push] 0
[assign] (not #778) decision axiom
[assign] #662 bin -288
[assign] #779 bin -288
[assign] (not #777) bin -288
[assign] #533 clause 79 288
[assign] #751 clause 243 288
[assign] (not #752) clause -244 288
[assign] (not #750) bin -244
[push] 1
[assign] (not #784) decision axiom
[assign] #665 bin -298
[assign] #785 bin -298
[assign] (not #783) bin -298
[push] 2
[assign] (not #571) decision axiom
[assign] #381 bin -260
[assign] #631 bin -260
[assign] (not #633) bin 77
[assign] #482 bin -81
[assign] #472 bin -81
[assign] (not #535) justification -1: -81
[assign] #759 justification -1: 256
[assign] #544 justification -1: 77
[assign] (not #374) justification -1: -242
[assign] (not #379) justification -1: -276 271 256
[assign] (not #756) justification -1: -276 271 256
[assign] (not #376) justification -1: -266 77 85
[assign] (not #753) justification -1: -266 77 85
[assign] #761 bin 257
[assign] #760 bin 257
[assign] #534 bin 78
[assign] #569 bin -251
[assign] #536 bin 258
[assign] (not #524) bin 258
[assign] #755 bin 80
[assign] (not #754) bin 80
[assign] #757 bin 83
[assign] (not #758) bin 83
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #660
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #154
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #162
[end-of-instance]
[assign] (not #664) clause -99 -258 91
[assign] (not #781) clause -293 -258 91
[assign] #782 clause 294 -258 91
[assign] #661 clause 95 248 -87
[assign] #775 clause 283 248 -87
[assign] (not #776) clause -284 248 -87
[assign] (not #663) bin -99
[assign] (not #780) bin -293
[assign] #660 clause 94 -95 -96
[assign] (not #774) bin -284
[assign] (not #419) clause -291 292
[assign] #585 bin -291
[assign] #641 justification -1: 87 -248 -244 -268
[assign] (not #414) justification -1: -89 271 87 -248 -244 -268
[assign] (not #416) justification -1: -266 85 87 -248 -244 -268
[assign] (not #643) bin 93
[assign] (not #421) clause -296 -93
[assign] #490 bin -281
[assign] #500 bin -286
[resolve-process] true
[resolve-lit] 0 (not #500)
[resolve-lit] 0 (not #490)
[resolve-lit] 0 (not #585)
[resolve-process] (not #500)
[resolve-lit] 0 #416
[resolve-process] (not #490)
[resolve-lit] 0 #414
[resolve-process] #416
[resolve-lit] 0 #754
[resolve-lit] 2 #752
[resolve-process] #414
[resolve-process] (not #585)
[resolve-lit] 0 #419
[resolve-process] #419
[resolve-lit] 0 #780
[resolve-process] #780
[resolve-lit] 0 #781
[resolve-process] #781
[resolve-lit] 0 (not #760)
[resolve-process] #754
[resolve-lit] 0 (not #534)
[resolve-process] (not #534)
[resolve-lit] 0 (not #544)
[resolve-process] (not #760)
[resolve-lit] 0 (not #759)
[resolve-process] (not #544)
[resolve-lit] 0 (not #631)
[resolve-process] (not #759)
[resolve-lit] 0 (not #381)
[resolve-process] (not #631)
[resolve-lit] 0 #571
[resolve-process] (not #381)
[conflict] #571 #752
[pop] 2 3
[assign] #571 clause 260 244
[assign] (not #374) justification -1: -242
[assign] #472 bin -241
[push] 1
[assign] (not #784) decision axiom
[assign] #665 bin -298
[assign] #785 bin -298
[assign] (not #783) bin -298
[push] 2
[assign] (not #569) decision axiom
[assign] #379 bin -255
[assign] #631 bin -255
[assign] (not #633) bin 77
[assign] (not #381) clause -256 -77 -260
[assign] #482 bin -81
[assign] #544 justification -1: 77
[assign] (not #535) justification -1: -81
[assign] (not #759) justification -1: -256
[assign] #756 justification -1: 251
[assign] (not #376) justification -1: -266 77 85
[assign] (not #753) justification -1: -266 77 85
[assign] #534 bin 78
[assign] #758 bin 252
[assign] #757 bin 252
[assign] #755 bin 80
[assign] (not #754) bin 80
[assign] #524 bin 254
[assign] (not #536) bin 254
[assign] #661 clause 95 248 -87
[assign] #775 clause 283 248 -87
[assign] (not #776) clause -284 248 -87
[assign] (not #760) bin 84
[assign] #761 bin 84
[assign] #660 clause 94 -95 -96
[assign] (not #774) bin -284
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #660
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #154
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #162
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #663
[end-of-instance]
[mk-app] #786 = #291 #261
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[mk-app] #786 = #14 #13
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[assign] #664 clause 99 83 -273
[assign] #781 clause 293 83 -273
[assign] (not #782) clause -294 83 -273
[assign] #663 clause 98 -99 -100
[assign] (not #780) bin -294
[assign] (not #419) clause -291 292
[assign] #585 bin -291
[assign] #641 justification -1: 87 -248 -244 -268
[assign] #643 justification -1: 253 273 -83 -91
[assign] (not #414) justification -1: -89 271 87 -248 -244 -268
[assign] (not #416) justification -1: -266 85 87 -248 -244 -268
[assign] (not #421) justification -1: -266 85 253 273 -83 -91
[resolve-lit] 0 (not #643)
[resolve-process] #643
[resolve-lit] 0 (not #641)
[resolve-process] (not #643)
[resolve-lit] 0 (not #757)
[resolve-lit] 0 #536
[resolve-process] (not #641)
[resolve-lit] 0 #754
[resolve-lit] 2 #752
[resolve-process] #536
[resolve-lit] 0 (not #758)
[resolve-process] #754
[resolve-lit] 0 (not #534)
[resolve-process] (not #757)
[resolve-lit] 0 (not #756)
[resolve-process] (not #758)
[resolve-process] (not #534)
[resolve-lit] 0 (not #544)
[resolve-process] (not #756)
[resolve-lit] 0 (not #379)
[resolve-process] (not #544)
[resolve-lit] 0 (not #631)
[resolve-process] (not #631)
[resolve-lit] 0 #569
[resolve-process] (not #379)
[conflict] #569 #752
[pop] 2 3
[assign] #569 clause 255 244
[assign] (not #482) clause -250 -255 -260 -245
[assign] #633 bin -250
[assign] #376 bin -250
[assign] (not #631) bin 81
[assign] #753 justification -1: 246
[assign] (not #544) justification -1: -77
[assign] #535 justification -1: 81
[assign] (not #379) justification -1: -89 271 81
[assign] (not #756) justification -1: -89 271 81
[assign] (not #381) justification -1: -266 81 85
[assign] (not #759) justification -1: -266 81 85
[assign] #755 bin 247
[assign] #754 bin 247
[assign] (not #534) clause -80 78 -79
[assign] #524 bin 82
[assign] #536 bin 82
[assign] (not #661) clause -95 -248
[assign] (not #760) bin 84
[assign] #761 bin 84
[assign] #757 bin 83
[assign] (not #758) bin 83
[assign] (not #784) clause -298 -83
[assign] #776 bin -95
[assign] (not #660) bin -95
[assign] #665 bin -298
[assign] #785 bin -298
[assign] (not #783) bin -298
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #774
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #162
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #780
[end-of-instance]
[mk-app] #786 = #231 #261
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #156
[end-of-instance]
[assign] #775 clause 283 -249 -87
[assign] (not #664) clause -99 -83 91
[assign] #782 clause 294 -83 91
[assign] #781 clause 293 258 -273
[assign] #774 clause 282 -283 -284
[assign] (not #663) bin -99
[assign] #780 clause 292 -294 -293
[assign] #414 justification -1: 249 87 248 -268
[assign] #419 justification -1: 273 83 -91 -258
[assign] (not #641) justification -1: -89 271 249 87 248 -268
[assign] (not #416) justification -1: -276 271 249 87 248 -268
[assign] (not #643) justification -1: -89 271 273 83 -91 -258
[assign] (not #421) justification -1: -276 271 273 83 -91 -258
[assign] #585 bin -93
[assign] #500 bin -286
[assign] #490 bin -97
[resolve-process] true
[resolve-lit] 0 (not #490)
[resolve-lit] 0 (not #500)
[resolve-lit] 0 (not #585)
[resolve-process] (not #490)
[resolve-lit] 0 #643
[resolve-process] (not #500)
[resolve-lit] 0 #416
[resolve-process] (not #585)
[resolve-lit] 0 #641
[resolve-process] #643
[resolve-lit] 0 (not #536)
[resolve-lit] 0 #760
[resolve-process] #416
[resolve-lit] 0 (not #755)
[resolve-lit] 0 (not #754)
[resolve-process] #641
[resolve-process] #760
[resolve-lit] 0 (not #524)
[resolve-process] (not #536)
[resolve-lit] 0 (not #535)
[resolve-process] (not #524)
[resolve-process] (not #754)
[resolve-lit] 0 (not #753)
[resolve-process] (not #755)
[resolve-process] (not #535)
[resolve-lit] 0 (not #633)
[resolve-process] (not #753)
[resolve-lit] 0 (not #376)
[resolve-process] (not #376)
[resolve-lit] 0 #482
[resolve-process] (not #633)
[conflict] #482
[pop] 1 1
[assign] #482 axiom
[push] 0
[assign] (not #569) decision axiom
[assign] #379 bin -255
[assign] #631 bin -255
[assign] #752 clause 244 255
[assign] (not #633) bin 77
[assign] (not #533) bin 244
[assign] #534 bin 244
[assign] #778 clause 288 -244
[assign] (not #776) clause -284 -244
[assign] #472 bin -81
[assign] #755 bin -79
[assign] (not #754) bin -79
[assign] (not #544) bin -79
[assign] #661 bin 288
[assign] (not #662) bin 288
[assign] #775 bin -284
[assign] (not #774) bin -284
[assign] (not #753) bin -248
[assign] (not #660) bin -96
[assign] (not #535) justification -1: -81
[assign] #756 justification -1: 251
[resolve-lit] 0 #544
[resolve-process] (not #544)
[resolve-lit] 0 (not #631)
[resolve-process] #544
[resolve-lit] 0 #533
[resolve-process] #533
[resolve-lit] 0 (not #752)
[resolve-process] (not #752)
[resolve-lit] 0 #569
[resolve-process] (not #631)
[conflict] #569
[pop] 1 1
[assign] #569 axiom
[push] 0
[assign] (not #631) decision axiom
[assign] #571 bin -77
[assign] (not #472) clause -245 -260 -250 -255
[assign] #633 bin -245
[assign] #374 bin -245
[assign] (not #376) clause -246 -81 -250
[assign] (not #544) justification -1: -77
[assign] (not #753) justification -1: -246
[assign] #750 justification -1: 241
[assign] #535 justification -1: 81
[assign] (not #379) justification -1: -89 271 81
[assign] (not #756) justification -1: -89 271 81
[assign] (not #381) justification -1: -266 81 85
[assign] (not #759) justification -1: -266 81 85
[assign] #752 bin 242
[assign] #751 bin 242
[assign] #524 bin 82
[assign] #536 bin 82
[assign] (not #533) bin 244
[assign] #534 bin 244
[assign] #778 clause 288 -244
[assign] (not #776) clause -284 -244
[assign] (not #760) bin 84
[assign] #761 bin 84
[assign] #757 bin 83
[assign] (not #758) bin 83
[assign] (not #784) clause -298 -83
[assign] (not #664) clause -99 -83 91
[assign] #782 clause 294 -83 91
[assign] #755 bin -79
[assign] (not #754) bin -79
[assign] #661 bin 288
[assign] (not #662) bin 288
[assign] #775 bin -284
[assign] (not #774) bin -284
[assign] #781 clause 293 258 -273
[assign] #665 bin -298
[assign] #785 bin -298
[assign] (not #783) bin -298
[assign] (not #663) bin -99
[assign] #780 clause 292 -294 -293
[assign] (not #660) bin -96
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #777
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #162
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #780
[end-of-instance]
[mk-app] #786 = #231 #261
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #786
[end-of-instance]
[inst-discovered] theory-solving 0x0 arith#
[instance] 0x0 #156
[end-of-instance]
[assign] #779 clause 289 -243 268
[assign] #777 clause 287 -289 -288
[assign] #416 justification -1: 87 -79 243 -268
[assign] #419 justification -1: 273 83 -91 -258
[assign] (not #641) justification -1: -266 85 87 -79 243 -268
[assign] (not #414) justification -1: -276 271 87 -79 243 -268
[assign] (not #643) justification -1: -89 271 273 83 -91 -258
[assign] (not #421) justification -1: -276 271 273 83 -91 -258
[assign] #585 bin -93
[assign] #490 bin -281
[assign] #500 bin -97
[resolve-process] true
[resolve-lit] 0 (not #500)
[resolve-lit] 0 (not #490)
[resolve-lit] 0 (not #585)
[resolve-process] (not #500)
[resolve-lit] 0 #643
[resolve-process] (not #490)
[resolve-lit] 0 #414
[resolve-process] (not #585)
[resolve-lit] 0 #641
[resolve-process] #643
[resolve-lit] 0 (not #536)
[resolve-lit] 0 #760
[resolve-process] #414
[resolve-lit] 0 #533
[resolve-lit] 0 (not #751)
[resolve-process] #641
[resolve-process] #760
[resolve-lit] 0 (not #524)
[resolve-process] #533
[resolve-lit] 0 (not #752)
[resolve-process] (not #536)
[resolve-lit] 0 (not #535)
[resolve-process] (not #524)
[resolve-process] (not #751)
[resolve-lit] 0 (not #750)
[resolve-process] (not #752)
[resolve-process] (not #535)
[resolve-lit] 0 (not #633)
[resolve-process] (not #750)
[resolve-lit] 0 (not #374)
[resolve-process] (not #374)
[resolve-lit] 0 #472
[resolve-process] (not #633)
[conflict] #472
[pop] 1 1
[assign] #472 axiom
[assign] (not #571) clause -260 -245 -250 -255
[assign] #381 bin -260
[assign] #631 bin -260
[assign] #752 clause 244 260
[assign] (not #633) bin 77
[assign] (not #379) clause -251 -77 -255
[assign] (not #533) bin 244
[assign] #534 bin 244
[assign] #778 clause 288 -244
[assign] (not #776) clause -284 -244
[assign] #755 bin -79
[assign] (not #754) bin -79
[assign] (not #544) bin -79
[assign] #661 bin 288
[assign] (not #662) bin 288
[assign] #775 bin -284
[assign] (not #774) bin -284
[assign] (not #753) bin -248
[assign] (not #660) bin -96
[assign] (not #535) justification -1: -81
[assign] (not #756) justification -1: -251
[assign] #759 justification -1: 256
[attach-meaning] #17 bv #b1
[attach-meaning] #18 bv #b0
[attach-meaning] #17 bv #b1
[attach-meaning] #18 bv #b0
[attach-meaning] #17 bv #b1
[attach-meaning] #18 bv #b0
[attach-meaning] #17 bv #b1
[attach-meaning] #18 bv #b0
[eof]