LTS Termination Proof

Input

Integer Transition System

Initial Location: f4135_0_sublistAutoDual_InvokeMethod, f2375_0_generation_InvokeMethod, f1674_0_number_greater_LT, f2374_0_generation_InvokeMethod, __init, f4661_0_sublistOddDistinctParts_InvokeMethod', f3187_0_generation_InvokeMethod, f2470_0_sublistAutoDual_InvokeMethod, f741_0_generation_Return, f3192_0_dual_LE, f789_0_generation_Return, f4740_0_sublistOddDistinctParts_NULL, f2503_0_isEqual_NONNULL, f2372_0_main_InvokeMethod, f654_0_generation_NE, f609_0_generation_NONNULL, f2504_0_union_NONNULL, f3931_0_sublistAutoDual_InvokeMethod, f2440_0_insert_NONNULL, f4854_0_sublistOddDistinctParts_EQ, f2373_0_generation_InvokeMethod, f4689_0_oddDistinctParts_NE, f4119_0_main_InvokeMethod, f740_0_generation_Return, f742_0_generation_Return, f4661_0_sublistOddDistinctParts_InvokeMethod, f283_0_partitionOf_GT, f1_0_main_Load, f4689_0_oddDistinctParts_NE'

Transitions: (pre-variables and post-variables)

f1_0_main_Load	1	f283_0_partitionOf_GT:	x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ 1 = _arg5P ∧ _arg2 = _arg4P ∧ 2 = _arg3P ∧ 2 ≤ _arg2P − 1 ∧ 0 ≤ _arg1P − 1 ∧ 0 ≤ _arg1 − 1 ∧ _arg2P − 2 ≤ _arg1 ∧ −1 ≤ _arg2 − 1 ∧ _arg1P ≤ _arg1
f283_0_partitionOf_GT	2	f609_0_generation_NONNULL:	x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x1 = _x6 ∧ x2 = _x7 ∧ x3 = _x8 ∧ x4 = _x9 ∧ x5 = _x10 ∧ x6 = _x11 ∧ _x3 = _x6 ∧ _x4 + 2 ≤ _x1 ∧ 0 ≤ _x8 − 1 ∧ 0 ≤ _x7 − 1 ∧ 0 ≤ _x1 − 1 ∧ 0 ≤ _x − 1 ∧ _x8 ≤ _x1 ∧ _x3 ≤ _x2 − 1 ∧ _x7 ≤ _x1
f283_0_partitionOf_GT	3	f283_0_partitionOf_GT:	x1 = _x12 ∧ x2 = _x13 ∧ x3 = _x14 ∧ x4 = _x15 ∧ x5 = _x16 ∧ x6 = _x17 ∧ x1 = _x18 ∧ x2 = _x19 ∧ x3 = _x20 ∧ x4 = _x21 ∧ x5 = _x22 ∧ x6 = _x23 ∧ _x14 = _x22 ∧ _x15 = _x21 ∧ _x14 + 1 = _x20 ∧ _x16 + 2 ≤ _x13 ∧ 2 ≤ _x19 − 1 ∧ 0 ≤ _x18 − 1 ∧ 0 ≤ _x13 − 1 ∧ 0 ≤ _x12 − 1 ∧ _x18 ≤ _x13 ∧ _x14 ≤ _x15 ∧ _x18 ≤ _x12
f283_0_partitionOf_GT	4	f2372_0_main_InvokeMethod:	x1 = _x24 ∧ x2 = _x25 ∧ x3 = _x26 ∧ x4 = _x27 ∧ x5 = _x28 ∧ x6 = _x29 ∧ x1 = _x30 ∧ x2 = _x31 ∧ x3 = _x32 ∧ x4 = _x33 ∧ x5 = _x34 ∧ x6 = _x35 ∧ _x28 + 2 ≤ _x25 ∧ −1 ≤ _x30 − 1 ∧ 0 ≤ _x25 − 1 ∧ 0 ≤ _x24 − 1 ∧ _x30 + 1 ≤ _x25 ∧ _x27 ≤ _x26 − 1 ∧ _x30 + 1 ≤ _x24
f283_0_partitionOf_GT	5	f2372_0_main_InvokeMethod:	x1 = _x36 ∧ x2 = _x37 ∧ x3 = _x38 ∧ x4 = _x39 ∧ x5 = _x40 ∧ x6 = _x41 ∧ x1 = _x42 ∧ x2 = _x43 ∧ x3 = _x44 ∧ x4 = _x45 ∧ x5 = _x46 ∧ x6 = _x47 ∧ _x40 + 2 ≤ _x37 ∧ −1 ≤ _x42 − 1 ∧ 0 ≤ _x37 − 1 ∧ _x39 ≤ _x38 − 1 ∧ 0 ≤ _x36 − 1
f740_0_generation_Return	6	f2372_0_main_InvokeMethod:	x1 = _x48 ∧ x2 = _x49 ∧ x3 = _x50 ∧ x4 = _x51 ∧ x5 = _x52 ∧ x6 = _x53 ∧ x1 = _x54 ∧ x2 = _x55 ∧ x3 = _x56 ∧ x4 = _x57 ∧ x5 = _x58 ∧ x6 = _x59 ∧ −1 ≤ _x54 − 1 ∧ 0 ≤ _x48 − 1 ∧ _x54 + 1 ≤ _x48
f2372_0_main_InvokeMethod	7	f4119_0_main_InvokeMethod:	x1 = _x60 ∧ x2 = _x61 ∧ x3 = _x62 ∧ x4 = _x63 ∧ x5 = _x64 ∧ x6 = _x65 ∧ x1 = _x67 ∧ x2 = _x68 ∧ x3 = _x69 ∧ x4 = _x70 ∧ x5 = _x71 ∧ x6 = _x72 ∧ _x68 + 4 ≤ _x60 ∧ 4 ≤ _x67 − 1 ∧ 4 ≤ _x60 − 1 ∧ _x67 ≤ _x60
f2372_0_main_InvokeMethod	8	f4119_0_main_InvokeMethod:	x1 = _x73 ∧ x2 = _x74 ∧ x3 = _x75 ∧ x4 = _x76 ∧ x5 = _x77 ∧ x6 = _x78 ∧ x1 = _x79 ∧ x2 = _x80 ∧ x3 = _x81 ∧ x4 = _x82 ∧ x5 = _x83 ∧ x6 = _x84 ∧ _x80 + 4 ≤ _x73 ∧ 2 ≤ _x79 − 1 ∧ 2 ≤ _x73 − 1 ∧ _x79 ≤ _x73
f2372_0_main_InvokeMethod	9	f4119_0_main_InvokeMethod:	x1 = _x85 ∧ x2 = _x86 ∧ x3 = _x87 ∧ x4 = _x88 ∧ x5 = _x89 ∧ x6 = _x90 ∧ x1 = _x91 ∧ x2 = _x92 ∧ x3 = _x93 ∧ x4 = _x94 ∧ x5 = _x95 ∧ x6 = _x96 ∧ _x92 + 4 ≤ _x85 ∧ 3 ≤ _x91 − 1 ∧ 3 ≤ _x85 − 1 ∧ _x91 ≤ _x85
f609_0_generation_NONNULL	10	f654_0_generation_NE:	x1 = _x97 ∧ x2 = _x98 ∧ x3 = _x99 ∧ x4 = _x100 ∧ x5 = _x101 ∧ x6 = _x102 ∧ x1 = _x103 ∧ x2 = _x104 ∧ x3 = _x105 ∧ x4 = _x106 ∧ x5 = _x107 ∧ x6 = _x108 ∧ _x97 − _x106 = _x105 ∧ _x97 = _x103 ∧ _x106 + 2 ≤ _x99 ∧ _x106 + 2 ≤ _x98 ∧ −1 ≤ _x107 − 1 ∧ 0 ≤ _x104 − 1 ∧ 0 ≤ _x99 − 1 ∧ 0 ≤ _x98 − 1 ∧ _x107 + 1 ≤ _x99 ∧ _x107 + 1 ≤ _x98 ∧ _x104 ≤ _x99 ∧ _x97 − _x106 ≤ 0 ∧ _x104 ≤ _x98
f609_0_generation_NONNULL	11	f654_0_generation_NE:	x1 = _x109 ∧ x2 = _x110 ∧ x3 = _x111 ∧ x4 = _x112 ∧ x5 = _x113 ∧ x6 = _x114 ∧ x1 = _x115 ∧ x2 = _x116 ∧ x3 = _x117 ∧ x4 = _x118 ∧ x5 = _x119 ∧ x6 = _x120 ∧ _x109 − _x118 = _x117 ∧ _x109 = _x115 ∧ _x118 + 2 ≤ _x111 ∧ _x118 + 2 ≤ _x110 ∧ −1 ≤ _x119 − 1 ∧ 0 ≤ _x116 − 1 ∧ 0 ≤ _x111 − 1 ∧ 0 ≤ _x110 − 1 ∧ _x119 + 1 ≤ _x111 ∧ _x119 + 1 ≤ _x110 ∧ _x116 ≤ _x111 ∧ _x116 ≤ _x110 ∧ 0 ≤ _x109 − _x118 − 1 ∧ _x109 ≤ _x109 − _x118
f609_0_generation_NONNULL	12	f609_0_generation_NONNULL:	x1 = _x121 ∧ x2 = _x122 ∧ x3 = _x123 ∧ x4 = _x124 ∧ x5 = _x125 ∧ x6 = _x126 ∧ x1 = _x127 ∧ x2 = _x128 ∧ x3 = _x129 ∧ x4 = _x130 ∧ x5 = _x131 ∧ x6 = _x132 ∧ _x121 − _x133 ≤ _x121 − 1 ∧ 0 ≤ _x121 − _x133 − 1 ∧ _x128 ≤ _x122 ∧ _x128 ≤ _x123 ∧ _x129 ≤ _x122 ∧ _x129 ≤ _x123 ∧ 0 ≤ _x122 − 1 ∧ 0 ≤ _x123 − 1 ∧ 0 ≤ _x128 − 1 ∧ 0 ≤ _x129 − 1 ∧ _x133 + 2 ≤ _x122 ∧ _x133 + 2 ≤ _x123 ∧ _x121 − _x133 = _x127
f654_0_generation_NE	13	f609_0_generation_NONNULL:	x1 = _x134 ∧ x2 = _x135 ∧ x3 = _x136 ∧ x4 = _x137 ∧ x5 = _x138 ∧ x6 = _x139 ∧ x1 = _x140 ∧ x2 = _x141 ∧ x3 = _x142 ∧ x4 = _x143 ∧ x5 = _x144 ∧ x6 = _x145 ∧ _x134 = _x140 ∧ _x137 + 2 ≤ _x135 ∧ −1 ≤ _x142 − 1 ∧ −1 ≤ _x141 − 1 ∧ −1 ≤ _x138 − 1 ∧ 0 ≤ _x135 − 1 ∧ _x142 ≤ _x138 ∧ _x142 + 1 ≤ _x135 ∧ _x141 ≤ _x138 ∧ _x136 ≤ −1 ∧ _x141 + 1 ≤ _x135
f654_0_generation_NE	14	f609_0_generation_NONNULL:	x1 = _x146 ∧ x2 = _x147 ∧ x3 = _x148 ∧ x4 = _x149 ∧ x5 = _x150 ∧ x6 = _x151 ∧ x1 = _x152 ∧ x2 = _x153 ∧ x3 = _x154 ∧ x4 = _x155 ∧ x5 = _x156 ∧ x6 = _x157 ∧ _x146 = _x152 ∧ _x149 + 2 ≤ _x147 ∧ −1 ≤ _x154 − 1 ∧ −1 ≤ _x153 − 1 ∧ −1 ≤ _x150 − 1 ∧ 0 ≤ _x147 − 1 ∧ _x154 ≤ _x150 ∧ _x154 + 1 ≤ _x147 ∧ _x153 ≤ _x150 ∧ 0 ≤ _x148 − 1 ∧ _x153 + 1 ≤ _x147
f654_0_generation_NE	15	f609_0_generation_NONNULL:	x1 = _x158 ∧ x2 = _x159 ∧ x3 = _x160 ∧ x4 = _x161 ∧ x5 = _x162 ∧ x6 = _x163 ∧ x1 = _x164 ∧ x2 = _x165 ∧ x3 = _x166 ∧ x4 = _x167 ∧ x5 = _x168 ∧ x6 = _x169 ∧ _x158 = _x164 ∧ 0 = _x160 ∧ _x161 + 2 ≤ _x159 ∧ −1 ≤ _x166 − 1 ∧ −1 ≤ _x165 − 1 ∧ −1 ≤ _x162 − 1 ∧ 0 ≤ _x159 − 1 ∧ _x166 ≤ _x162 ∧ _x166 + 1 ≤ _x159 ∧ _x165 ≤ _x162 ∧ _x165 + 1 ≤ _x159
f609_0_generation_NONNULL	16	f2373_0_generation_InvokeMethod:	x1 = _x170 ∧ x2 = _x171 ∧ x3 = _x172 ∧ x4 = _x173 ∧ x5 = _x174 ∧ x6 = _x175 ∧ x1 = _x176 ∧ x2 = _x177 ∧ x3 = _x178 ∧ x4 = _x179 ∧ x5 = _x180 ∧ x6 = _x181 ∧ _x170 = _x176 ∧ _x179 + 2 ≤ _x172 ∧ _x179 + 2 ≤ _x171 ∧ −1 ≤ _x180 − 1 ∧ −1 ≤ _x178 − 1 ∧ 0 ≤ _x177 − 1 ∧ 0 ≤ _x172 − 1 ∧ 0 ≤ _x171 − 1 ∧ _x180 + 1 ≤ _x172 ∧ _x180 + 1 ≤ _x171 ∧ _x178 + 1 ≤ _x172 ∧ _x178 + 1 ≤ _x171 ∧ _x177 ≤ _x172 ∧ _x177 ≤ _x171 ∧ 0 ≤ _x170 − _x179 − 1 ∧ _x170 − _x179 ≤ _x170 − 1
f609_0_generation_NONNULL	17	f2373_0_generation_InvokeMethod:	x1 = _x182 ∧ x2 = _x183 ∧ x3 = _x184 ∧ x4 = _x185 ∧ x5 = _x186 ∧ x6 = _x187 ∧ x1 = _x188 ∧ x2 = _x189 ∧ x3 = _x190 ∧ x4 = _x191 ∧ x5 = _x192 ∧ x6 = _x193 ∧ _x182 = _x188 ∧ _x191 + 2 ≤ _x184 ∧ _x191 + 2 ≤ _x183 ∧ −1 ≤ _x192 − 1 ∧ −1 ≤ _x190 − 1 ∧ 0 ≤ _x189 − 1 ∧ 0 ≤ _x184 − 1 ∧ 0 ≤ _x183 − 1 ∧ _x192 + 1 ≤ _x184 ∧ _x192 + 1 ≤ _x183 ∧ _x189 ≤ _x184 ∧ _x189 ≤ _x183 ∧ 0 ≤ _x182 − _x191 − 1 ∧ _x182 − _x191 ≤ _x182 − 1
f741_0_generation_Return	18	f2373_0_generation_InvokeMethod:	x1 = _x194 ∧ x2 = _x195 ∧ x3 = _x196 ∧ x4 = _x197 ∧ x5 = _x198 ∧ x6 = _x199 ∧ x1 = _x200 ∧ x2 = _x201 ∧ x3 = _x202 ∧ x4 = _x203 ∧ x5 = _x204 ∧ x6 = _x205 ∧ _x196 = _x203 ∧ _x194 = _x200 ∧ _x196 + 2 ≤ _x195 ∧ −1 ≤ _x204 − 1 ∧ −1 ≤ _x202 − 1 ∧ 0 ≤ _x201 − 1 ∧ −1 ≤ _x197 − 1 ∧ 0 ≤ _x195 − 1 ∧ _x204 ≤ _x197 ∧ _x204 + 1 ≤ _x195 ∧ _x202 ≤ _x197 ∧ _x202 + 1 ≤ _x195 ∧ _x201 ≤ _x195
f654_0_generation_NE	19	f2374_0_generation_InvokeMethod:	x1 = _x206 ∧ x2 = _x207 ∧ x3 = _x208 ∧ x4 = _x209 ∧ x5 = _x210 ∧ x6 = _x211 ∧ x1 = _x212 ∧ x2 = _x213 ∧ x3 = _x214 ∧ x4 = _x215 ∧ x5 = _x216 ∧ x6 = _x217 ∧ _x206 = _x212 ∧ _x209 + 2 ≤ _x207 ∧ −1 ≤ _x210 − 1 ∧ _x208 ≤ −1 ∧ 0 ≤ _x207 − 1
f654_0_generation_NE	20	f2374_0_generation_InvokeMethod:	x1 = _x218 ∧ x2 = _x219 ∧ x3 = _x220 ∧ x4 = _x221 ∧ x5 = _x222 ∧ x6 = _x223 ∧ x1 = _x224 ∧ x2 = _x225 ∧ x3 = _x226 ∧ x4 = _x227 ∧ x5 = _x228 ∧ x6 = _x229 ∧ _x218 = _x224 ∧ _x221 + 2 ≤ _x219 ∧ −1 ≤ _x222 − 1 ∧ 0 ≤ _x220 − 1 ∧ 0 ≤ _x219 − 1
f742_0_generation_Return	21	f2374_0_generation_InvokeMethod:	x1 = _x230 ∧ x2 = _x231 ∧ x3 = _x232 ∧ x4 = _x233 ∧ x5 = _x234 ∧ x6 = _x235 ∧ x1 = _x236 ∧ x2 = _x237 ∧ x3 = _x238 ∧ x4 = _x239 ∧ x5 = _x240 ∧ x6 = _x241 ∧ _x231 = _x237 ∧ _x230 = _x236
f654_0_generation_NE	22	f2375_0_generation_InvokeMethod:	x1 = _x242 ∧ x2 = _x243 ∧ x3 = _x244 ∧ x4 = _x245 ∧ x5 = _x246 ∧ x6 = _x247 ∧ x1 = _x248 ∧ x2 = _x249 ∧ x3 = _x250 ∧ x4 = _x251 ∧ x5 = _x252 ∧ x6 = _x253 ∧ _x245 = _x249 ∧ 0 = _x244 ∧ _x245 + 2 ≤ _x243 ∧ 3 ≤ _x248 − 1 ∧ −1 ≤ _x246 − 1 ∧ 0 ≤ _x243 − 1 ∧ _x248 − 3 ≤ _x243
f789_0_generation_Return	23	f2375_0_generation_InvokeMethod:	x1 = _x254 ∧ x2 = _x255 ∧ x3 = _x256 ∧ x4 = _x257 ∧ x5 = _x258 ∧ x6 = _x259 ∧ x1 = _x260 ∧ x2 = _x261 ∧ x3 = _x262 ∧ x4 = _x263 ∧ x5 = _x264 ∧ x6 = _x265 ∧ _x255 = _x261 ∧ _x255 + 4 ≤ _x254 ∧ 3 ≤ _x260 − 1 ∧ 3 ≤ _x254 − 1 ∧ _x260 ≤ _x254
f2373_0_generation_InvokeMethod	24	f2440_0_insert_NONNULL:	x1 = _x266 ∧ x2 = _x267 ∧ x3 = _x268 ∧ x4 = _x269 ∧ x5 = _x270 ∧ x6 = _x271 ∧ x1 = _x272 ∧ x2 = _x273 ∧ x3 = _x274 ∧ x4 = _x275 ∧ x5 = _x276 ∧ x6 = _x277 ∧ _x269 + 2 ≤ _x267 ∧ −1 ≤ _x272 − 1 ∧ −1 ≤ _x270 − 1 ∧ −1 ≤ _x268 − 1 ∧ 0 ≤ _x267 − 1 ∧ _x272 ≤ _x268
f2374_0_generation_InvokeMethod	25	f2504_0_union_NONNULL:	x1 = _x278 ∧ x2 = _x279 ∧ x3 = _x280 ∧ x4 = _x281 ∧ x5 = _x282 ∧ x6 = _x283 ∧ x1 = _x284 ∧ x2 = _x285 ∧ x3 = _x286 ∧ x4 = _x287 ∧ x5 = _x288 ∧ x6 = _x289 ∧ −1 ≤ _x284 − 1
f2375_0_generation_InvokeMethod	26	f2504_0_union_NONNULL:	x1 = _x290 ∧ x2 = _x291 ∧ x3 = _x292 ∧ x4 = _x293 ∧ x5 = _x294 ∧ x6 = _x295 ∧ x1 = _x296 ∧ x2 = _x297 ∧ x3 = _x298 ∧ x4 = _x299 ∧ x5 = _x300 ∧ x6 = _x301 ∧ _x291 + 4 ≤ _x290 ∧ 3 ≤ _x296 − 1 ∧ 3 ≤ _x290 − 1 ∧ _x296 ≤ _x290
f2373_0_generation_InvokeMethod	27	f609_0_generation_NONNULL:	x1 = _x302 ∧ x2 = _x303 ∧ x3 = _x304 ∧ x4 = _x305 ∧ x5 = _x306 ∧ x6 = _x307 ∧ x1 = _x308 ∧ x2 = _x309 ∧ x3 = _x310 ∧ x4 = _x311 ∧ x5 = _x312 ∧ x6 = _x313 ∧ _x302 = _x308 ∧ _x305 + 2 ≤ _x303 ∧ −1 ≤ _x310 − 1 ∧ −1 ≤ _x309 − 1 ∧ −1 ≤ _x306 − 1 ∧ −1 ≤ _x304 − 1 ∧ 0 ≤ _x303 − 1 ∧ _x310 ≤ _x306 ∧ _x310 + 1 ≤ _x303 ∧ _x309 ≤ _x306 ∧ _x309 + 1 ≤ _x303
f2373_0_generation_InvokeMethod	28	f2504_0_union_NONNULL:	x1 = _x314 ∧ x2 = _x315 ∧ x3 = _x316 ∧ x4 = _x317 ∧ x5 = _x318 ∧ x6 = _x319 ∧ x1 = _x320 ∧ x2 = _x321 ∧ x3 = _x322 ∧ x4 = _x323 ∧ x5 = _x324 ∧ x6 = _x325 ∧ _x317 + 2 ≤ _x315 ∧ −1 ≤ _x320 − 1 ∧ −1 ≤ _x318 − 1 ∧ −1 ≤ _x316 − 1 ∧ 0 ≤ _x315 − 1 ∧ _x320 ≤ _x318 ∧ _x320 ≤ _x316 ∧ _x320 + 1 ≤ _x315
f2373_0_generation_InvokeMethod	29	f3187_0_generation_InvokeMethod:	x1 = _x326 ∧ x2 = _x327 ∧ x3 = _x328 ∧ x4 = _x329 ∧ x5 = _x330 ∧ x6 = _x331 ∧ x1 = _x332 ∧ x2 = _x333 ∧ x3 = _x334 ∧ x4 = _x335 ∧ x5 = _x336 ∧ x6 = _x337 ∧ _x329 = _x335 ∧ _x326 = _x333 ∧ _x329 + 2 ≤ _x327 ∧ −1 ≤ _x334 − 1 ∧ 2 ≤ _x332 − 1 ∧ −1 ≤ _x330 − 1 ∧ −1 ≤ _x328 − 1 ∧ 0 ≤ _x327 − 1 ∧ _x334 ≤ _x330 ∧ _x334 + 1 ≤ _x327
f2373_0_generation_InvokeMethod	30	f3187_0_generation_InvokeMethod:	x1 = _x338 ∧ x2 = _x339 ∧ x3 = _x340 ∧ x4 = _x341 ∧ x5 = _x342 ∧ x6 = _x343 ∧ x1 = _x344 ∧ x2 = _x345 ∧ x3 = _x346 ∧ x4 = _x347 ∧ x5 = _x348 ∧ x6 = _x349 ∧ _x341 = _x347 ∧ _x338 = _x345 ∧ _x341 + 2 ≤ _x339 ∧ −1 ≤ _x346 − 1 ∧ 4 ≤ _x344 − 1 ∧ −1 ≤ _x342 − 1 ∧ −1 ≤ _x340 − 1 ∧ 0 ≤ _x339 − 1 ∧ _x346 ≤ _x342 ∧ _x346 + 1 ≤ _x339
f3187_0_generation_InvokeMethod	31	f609_0_generation_NONNULL:	x1 = _x350 ∧ x2 = _x351 ∧ x3 = _x352 ∧ x4 = _x353 ∧ x5 = _x354 ∧ x6 = _x355 ∧ x1 = _x356 ∧ x2 = _x357 ∧ x3 = _x358 ∧ x4 = _x359 ∧ x5 = _x360 ∧ x6 = _x361 ∧ _x351 = _x356 ∧ _x354 + 4 ≤ _x350 ∧ _x353 + 4 ≤ _x350 ∧ −1 ≤ _x358 − 1 ∧ −1 ≤ _x357 − 1 ∧ −1 ≤ _x352 − 1 ∧ 2 ≤ _x350 − 1 ∧ _x358 ≤ _x352 ∧ _x357 ≤ _x352
f3187_0_generation_InvokeMethod	32	f2504_0_union_NONNULL:	x1 = _x362 ∧ x2 = _x363 ∧ x3 = _x364 ∧ x4 = _x365 ∧ x5 = _x366 ∧ x6 = _x367 ∧ x1 = _x368 ∧ x2 = _x369 ∧ x3 = _x370 ∧ x4 = _x371 ∧ x5 = _x372 ∧ x6 = _x373 ∧ _x366 + 4 ≤ _x362 ∧ _x365 + 4 ≤ _x362 ∧ 2 ≤ _x368 − 1 ∧ −1 ≤ _x364 − 1 ∧ 2 ≤ _x362 − 1 ∧ _x368 ≤ _x362
f2440_0_insert_NONNULL	33	f2440_0_insert_NONNULL:	x1 = _x374 ∧ x2 = _x375 ∧ x3 = _x376 ∧ x4 = _x377 ∧ x5 = _x378 ∧ x6 = _x379 ∧ x1 = _x380 ∧ x2 = _x381 ∧ x3 = _x382 ∧ x4 = _x383 ∧ x5 = _x384 ∧ x6 = _x385 ∧ −1 ≤ _x380 − 1 ∧ 0 ≤ _x374 − 1 ∧ _x380 + 1 ≤ _x374
f2504_0_union_NONNULL	34	f2504_0_union_NONNULL:	x1 = _x386 ∧ x2 = _x387 ∧ x3 = _x388 ∧ x4 = _x389 ∧ x5 = _x390 ∧ x6 = _x391 ∧ x1 = _x392 ∧ x2 = _x393 ∧ x3 = _x394 ∧ x4 = _x395 ∧ x5 = _x396 ∧ x6 = _x397 ∧ −1 ≤ _x392 − 1 ∧ 0 ≤ _x386 − 1 ∧ _x392 + 1 ≤ _x386
f2372_0_main_InvokeMethod	35	f2470_0_sublistAutoDual_InvokeMethod:	x1 = _x398 ∧ x2 = _x399 ∧ x3 = _x400 ∧ x4 = _x401 ∧ x5 = _x402 ∧ x6 = _x403 ∧ x1 = _x404 ∧ x2 = _x405 ∧ x3 = _x406 ∧ x4 = _x407 ∧ x5 = _x408 ∧ x6 = _x409 ∧ _x406 + 2 ≤ _x398 ∧ −1 ≤ _x405 − 1 ∧ 0 ≤ _x404 − 1 ∧ 0 ≤ _x398 − 1 ∧ _x405 + 1 ≤ _x398 ∧ _x404 ≤ _x398
f2470_0_sublistAutoDual_InvokeMethod	36	f3192_0_dual_LE:	x1 = _x410 ∧ x2 = _x411 ∧ x3 = _x412 ∧ x4 = _x413 ∧ x5 = _x414 ∧ x6 = _x415 ∧ x1 = _x416 ∧ x2 = _x417 ∧ x3 = _x418 ∧ x4 = _x419 ∧ x5 = _x420 ∧ x6 = _x421 ∧ _x419 = _x421 ∧ _x419 = _x420 ∧ _x419 + 2 ≤ _x411 ∧ _x412 + 2 ≤ _x410 ∧ _x419 + 4 ≤ _x410 ∧ −1 ≤ _x418 − 1 ∧ 0 ≤ _x417 − 1 ∧ 2 ≤ _x416 − 1 ∧ 0 ≤ _x411 − 1 ∧ 2 ≤ _x410 − 1 ∧ _x418 + 1 ≤ _x411 ∧ _x418 + 3 ≤ _x410 ∧ _x417 ≤ _x411 ∧ _x417 + 2 ≤ _x410 ∧ _x416 ≤ _x410
f3192_0_dual_LE	37	f2470_0_sublistAutoDual_InvokeMethod:	x1 = _x422 ∧ x2 = _x423 ∧ x3 = _x424 ∧ x4 = _x425 ∧ x5 = _x426 ∧ x6 = _x427 ∧ x1 = _x428 ∧ x2 = _x429 ∧ x3 = _x430 ∧ x4 = _x431 ∧ x5 = _x432 ∧ x6 = _x433 ∧ _x426 = _x427 ∧ _x426 + 2 ≤ _x423 ∧ _x430 + 4 ≤ _x422 ∧ _x426 + 4 ≤ _x422 ∧ −1 ≤ _x429 − 1 ∧ 0 ≤ _x428 − 1 ∧ −1 ≤ _x424 − 1 ∧ 0 ≤ _x423 − 1 ∧ 2 ≤ _x422 − 1 ∧ _x429 + 3 ≤ _x422 ∧ _x425 ≤ 0 ∧ _x428 + 2 ≤ _x422
f3192_0_dual_LE	38	f2503_0_isEqual_NONNULL:	x1 = _x434 ∧ x2 = _x435 ∧ x3 = _x436 ∧ x4 = _x437 ∧ x5 = _x438 ∧ x6 = _x439 ∧ x1 = _x440 ∧ x2 = _x441 ∧ x3 = _x442 ∧ x4 = _x443 ∧ x5 = _x444 ∧ x6 = _x445 ∧ _x438 = _x439 ∧ _x438 + 2 ≤ _x435 ∧ _x438 + 4 ≤ _x434 ∧ −1 ≤ _x441 − 1 ∧ 0 ≤ _x440 − 1 ∧ −1 ≤ _x436 − 1 ∧ 0 ≤ _x435 − 1 ∧ 2 ≤ _x434 − 1 ∧ _x441 ≤ _x436 ∧ _x440 ≤ _x435 ∧ _x437 ≤ 0 ∧ _x440 + 2 ≤ _x434
f3192_0_dual_LE	39	f3327_0_sublistAutoDual_NE:	x1 = _x446 ∧ x2 = _x447 ∧ x3 = _x448 ∧ x4 = _x449 ∧ x5 = _x450 ∧ x6 = _x451 ∧ x1 = _x452 ∧ x2 = _x453 ∧ x3 = _x454 ∧ x4 = _x455 ∧ x5 = _x456 ∧ x6 = _x457 ∧ 0 = _x454 ∧ _x450 = _x451 ∧ _x450 + 2 ≤ _x447 ∧ _x450 + 4 ≤ _x446 ∧ 0 ≤ _x453 − 1 ∧ 3 ≤ _x452 − 1 ∧ 0 ≤ _x448 − 1 ∧ 1 ≤ _x447 − 1 ∧ 3 ≤ _x446 − 1 ∧ _x453 ≤ _x448 ∧ _x452 − 2 ≤ _x447 ∧ _x449 ≤ 0 ∧ _x452 ≤ _x446
f3192_0_dual_LE	40	f3327_0_sublistAutoDual_NE:	x1 = _x458 ∧ x2 = _x459 ∧ x3 = _x460 ∧ x4 = _x461 ∧ x5 = _x462 ∧ x6 = _x463 ∧ x1 = _x464 ∧ x2 = _x465 ∧ x3 = _x466 ∧ x4 = _x467 ∧ x5 = _x468 ∧ x6 = _x469 ∧ 0 = _x466 ∧ _x462 = _x463 ∧ _x462 + 2 ≤ _x460 ∧ _x462 + 2 ≤ _x459 ∧ _x462 + 4 ≤ _x458 ∧ 2 ≤ _x465 − 1 ∧ 3 ≤ _x464 − 1 ∧ 2 ≤ _x460 − 1 ∧ 1 ≤ _x459 − 1 ∧ 3 ≤ _x458 − 1 ∧ _x465 ≤ _x460 ∧ _x464 − 2 ≤ _x460 ∧ _x464 − 2 ≤ _x459 ∧ _x461 ≤ 0 ∧ _x464 ≤ _x458
f3192_0_dual_LE	41	f3327_0_sublistAutoDual_NE:	x1 = _x470 ∧ x2 = _x471 ∧ x3 = _x472 ∧ x4 = _x473 ∧ x5 = _x474 ∧ x6 = _x475 ∧ x1 = _x476 ∧ x2 = _x477 ∧ x3 = _x478 ∧ x4 = _x479 ∧ x5 = _x480 ∧ x6 = _x481 ∧ 1 = _x478 ∧ _x474 = _x475 ∧ _x474 + 2 ≤ _x472 ∧ _x474 + 2 ≤ _x471 ∧ _x474 + 4 ≤ _x470 ∧ 1 ≤ _x477 − 1 ∧ 3 ≤ _x476 − 1 ∧ 1 ≤ _x472 − 1 ∧ 1 ≤ _x471 − 1 ∧ 3 ≤ _x470 − 1 ∧ _x477 ≤ _x472 ∧ _x477 ≤ _x471 ∧ _x477 + 2 ≤ _x470 ∧ _x476 − 2 ≤ _x472 ∧ _x476 − 2 ≤ _x471 ∧ _x473 ≤ 0 ∧ _x476 ≤ _x470
f3192_0_dual_LE	42	f3328_0_sublistAutoDual_NE:	x1 = _x482 ∧ x2 = _x483 ∧ x3 = _x484 ∧ x4 = _x485 ∧ x5 = _x486 ∧ x6 = _x487 ∧ x1 = _x488 ∧ x2 = _x489 ∧ x3 = _x490 ∧ x4 = _x491 ∧ x5 = _x492 ∧ x6 = _x493 ∧ 0 = _x490 ∧ _x486 = _x487 ∧ _x486 + 2 ≤ _x483 ∧ _x486 + 4 ≤ _x482 ∧ 0 ≤ _x489 − 1 ∧ 4 ≤ _x488 − 1 ∧ 0 ≤ _x484 − 1 ∧ 2 ≤ _x483 − 1 ∧ 4 ≤ _x482 − 1 ∧ _x489 ≤ _x484 ∧ _x488 − 2 ≤ _x483 ∧ _x485 ≤ 0 ∧ _x488 ≤ _x482
f3192_0_dual_LE	43	f3328_0_sublistAutoDual_NE:	x1 = _x494 ∧ x2 = _x495 ∧ x3 = _x496 ∧ x4 = _x497 ∧ x5 = _x498 ∧ x6 = _x499 ∧ x1 = _x500 ∧ x2 = _x501 ∧ x3 = _x502 ∧ x4 = _x503 ∧ x5 = _x504 ∧ x6 = _x505 ∧ 0 = _x502 ∧ _x498 = _x499 ∧ _x498 + 2 ≤ _x496 ∧ _x498 + 2 ≤ _x495 ∧ _x498 + 4 ≤ _x494 ∧ 1 ≤ _x501 − 1 ∧ 4 ≤ _x500 − 1 ∧ 1 ≤ _x496 − 1 ∧ 2 ≤ _x495 − 1 ∧ 4 ≤ _x494 − 1 ∧ _x501 ≤ _x496 ∧ _x501 ≤ _x495 ∧ _x501 + 2 ≤ _x494 ∧ _x500 − 2 ≤ _x495 ∧ _x497 ≤ 0 ∧ _x500 ≤ _x494
f3192_0_dual_LE	44	f3328_0_sublistAutoDual_NE:	x1 = _x506 ∧ x2 = _x507 ∧ x3 = _x508 ∧ x4 = _x509 ∧ x5 = _x510 ∧ x6 = _x511 ∧ x1 = _x512 ∧ x2 = _x513 ∧ x3 = _x514 ∧ x4 = _x515 ∧ x5 = _x516 ∧ x6 = _x517 ∧ 0 = _x514 ∧ _x510 = _x511 ∧ _x510 + 2 ≤ _x508 ∧ _x510 + 2 ≤ _x507 ∧ _x510 + 4 ≤ _x506 ∧ 2 ≤ _x513 − 1 ∧ 5 ≤ _x512 − 1 ∧ 2 ≤ _x508 − 1 ∧ 3 ≤ _x507 − 1 ∧ 5 ≤ _x506 − 1 ∧ _x513 ≤ _x508 ∧ _x512 − 2 ≤ _x507 ∧ _x509 ≤ 0 ∧ _x512 ≤ _x506
f3192_0_dual_LE	45	f3328_0_sublistAutoDual_NE:	x1 = _x518 ∧ x2 = _x519 ∧ x3 = _x520 ∧ x4 = _x521 ∧ x5 = _x522 ∧ x6 = _x523 ∧ x1 = _x524 ∧ x2 = _x525 ∧ x3 = _x526 ∧ x4 = _x527 ∧ x5 = _x528 ∧ x6 = _x529 ∧ 1 = _x526 ∧ _x522 = _x523 ∧ _x522 + 2 ≤ _x520 ∧ _x522 + 2 ≤ _x519 ∧ _x522 + 4 ≤ _x518 ∧ 2 ≤ _x525 − 1 ∧ 5 ≤ _x524 − 1 ∧ 2 ≤ _x520 − 1 ∧ 3 ≤ _x519 − 1 ∧ 5 ≤ _x518 − 1 ∧ _x525 ≤ _x520 ∧ _x524 − 2 ≤ _x519 ∧ _x521 ≤ 0 ∧ _x524 ≤ _x518
f3192_0_dual_LE	46	f3328_0_sublistAutoDual_NE:	x1 = _x530 ∧ x2 = _x531 ∧ x3 = _x532 ∧ x4 = _x533 ∧ x5 = _x534 ∧ x6 = _x535 ∧ x1 = _x536 ∧ x2 = _x537 ∧ x3 = _x538 ∧ x4 = _x539 ∧ x5 = _x540 ∧ x6 = _x541 ∧ 0 = _x538 ∧ _x534 = _x535 ∧ _x534 + 2 ≤ _x532 ∧ _x534 + 2 ≤ _x531 ∧ _x534 + 4 ≤ _x530 ∧ 2 ≤ _x537 − 1 ∧ 6 ≤ _x536 − 1 ∧ 2 ≤ _x532 − 1 ∧ 4 ≤ _x531 − 1 ∧ 6 ≤ _x530 − 1 ∧ _x537 ≤ _x532 ∧ _x536 − 2 ≤ _x531 ∧ _x533 ≤ 0 ∧ _x536 ≤ _x530
f3192_0_dual_LE	47	f3328_0_sublistAutoDual_NE:	x1 = _x542 ∧ x2 = _x543 ∧ x3 = _x544 ∧ x4 = _x545 ∧ x5 = _x546 ∧ x6 = _x547 ∧ x1 = _x548 ∧ x2 = _x549 ∧ x3 = _x550 ∧ x4 = _x551 ∧ x5 = _x552 ∧ x6 = _x553 ∧ 1 = _x550 ∧ _x546 = _x547 ∧ _x546 + 2 ≤ _x544 ∧ _x546 + 2 ≤ _x543 ∧ _x546 + 4 ≤ _x542 ∧ 2 ≤ _x549 − 1 ∧ 6 ≤ _x548 − 1 ∧ 2 ≤ _x544 − 1 ∧ 4 ≤ _x543 − 1 ∧ 6 ≤ _x542 − 1 ∧ _x549 ≤ _x544 ∧ _x548 − 2 ≤ _x543 ∧ _x545 ≤ 0 ∧ _x548 ≤ _x542
f3192_0_dual_LE	48	f3192_0_dual_LE:	x1 = _x554 ∧ x2 = _x555 ∧ x3 = _x556 ∧ x4 = _x557 ∧ x5 = _x558 ∧ x6 = _x559 ∧ x1 = _x560 ∧ x2 = _x561 ∧ x3 = _x562 ∧ x4 = _x563 ∧ x5 = _x564 ∧ x6 = _x565 ∧ _x558 = _x565 ∧ _x558 = _x564 ∧ _x557 − 1 = _x563 ∧ _x558 = _x559 ∧ _x558 + 2 ≤ _x555 ∧ _x558 + 4 ≤ _x554 ∧ 0 ≤ _x562 − 1 ∧ 2 ≤ _x561 − 1 ∧ 4 ≤ _x560 − 1 ∧ −1 ≤ _x556 − 1 ∧ 2 ≤ _x555 − 1 ∧ 4 ≤ _x554 − 1 ∧ _x561 ≤ _x555 ∧ _x561 + 2 ≤ _x554 ∧ 0 ≤ _x557 − 1 ∧ _x560 ≤ _x554
f3192_0_dual_LE	49	f3192_0_dual_LE:	x1 = _x566 ∧ x2 = _x567 ∧ x3 = _x568 ∧ x4 = _x569 ∧ x5 = _x570 ∧ x6 = _x571 ∧ x1 = _x572 ∧ x2 = _x573 ∧ x3 = _x574 ∧ x4 = _x575 ∧ x5 = _x576 ∧ x6 = _x577 ∧ _x570 = _x577 ∧ _x570 = _x576 ∧ _x569 − 1 = _x575 ∧ _x570 = _x571 ∧ _x570 + 2 ≤ _x567 ∧ _x570 + 4 ≤ _x566 ∧ 1 ≤ _x574 − 1 ∧ 1 ≤ _x573 − 1 ∧ 3 ≤ _x572 − 1 ∧ −1 ≤ _x568 − 1 ∧ 1 ≤ _x567 − 1 ∧ 3 ≤ _x566 − 1 ∧ _x574 − 2 ≤ _x568 ∧ _x573 ≤ _x567 ∧ _x573 + 2 ≤ _x566 ∧ 0 ≤ _x569 − 1 ∧ _x572 ≤ _x566
f3192_0_dual_LE	50	f3192_0_dual_LE:	x1 = _x578 ∧ x2 = _x579 ∧ x3 = _x580 ∧ x4 = _x581 ∧ x5 = _x582 ∧ x6 = _x583 ∧ x1 = _x584 ∧ x2 = _x585 ∧ x3 = _x586 ∧ x4 = _x587 ∧ x5 = _x588 ∧ x6 = _x589 ∧ _x582 = _x589 ∧ _x582 = _x588 ∧ _x581 − 1 = _x587 ∧ _x582 = _x583 ∧ _x582 + 2 ≤ _x579 ∧ _x582 + 4 ≤ _x578 ∧ 2 ≤ _x586 − 1 ∧ 1 ≤ _x585 − 1 ∧ 3 ≤ _x584 − 1 ∧ −1 ≤ _x580 − 1 ∧ 1 ≤ _x579 − 1 ∧ 3 ≤ _x578 − 1 ∧ _x586 − 3 ≤ _x580 ∧ _x585 ≤ _x579 ∧ _x585 + 2 ≤ _x578 ∧ 0 ≤ _x581 − 1 ∧ _x584 ≤ _x578
f3192_0_dual_LE	51	f3931_0_sublistAutoDual_InvokeMethod:	x1 = _x590 ∧ x2 = _x591 ∧ x3 = _x592 ∧ x4 = _x593 ∧ x5 = _x594 ∧ x6 = _x595 ∧ x1 = _x596 ∧ x2 = _x597 ∧ x3 = _x598 ∧ x4 = _x599 ∧ x5 = _x600 ∧ x6 = _x601 ∧ _x594 = _x600 ∧ _x594 = _x595 ∧ _x594 + 2 ≤ _x591 ∧ _x599 + 6 ≤ _x590 ∧ _x594 + 4 ≤ _x590 ∧ −1 ≤ _x598 − 1 ∧ 0 ≤ _x597 − 1 ∧ 6 ≤ _x596 − 1 ∧ −1 ≤ _x592 − 1 ∧ 0 ≤ _x591 − 1 ∧ 6 ≤ _x590 − 1 ∧ _x598 ≤ _x592 ∧ _x597 ≤ _x591 ∧ _x597 + 2 ≤ _x590 ∧ _x593 ≤ 0 ∧ _x596 ≤ _x590
f3192_0_dual_LE	52	f3931_0_sublistAutoDual_InvokeMethod:	x1 = _x602 ∧ x2 = _x603 ∧ x3 = _x604 ∧ x4 = _x605 ∧ x5 = _x606 ∧ x6 = _x607 ∧ x1 = _x608 ∧ x2 = _x609 ∧ x3 = _x610 ∧ x4 = _x611 ∧ x5 = _x612 ∧ x6 = _x613 ∧ _x606 = _x612 ∧ _x606 = _x607 ∧ _x606 + 2 ≤ _x603 ∧ _x611 + 6 ≤ _x602 ∧ _x606 + 4 ≤ _x602 ∧ −1 ≤ _x610 − 1 ∧ 0 ≤ _x609 − 1 ∧ 4 ≤ _x608 − 1 ∧ −1 ≤ _x604 − 1 ∧ 0 ≤ _x603 − 1 ∧ 4 ≤ _x602 − 1 ∧ _x610 ≤ _x604 ∧ _x609 ≤ _x603 ∧ _x609 + 2 ≤ _x602 ∧ _x605 ≤ 0 ∧ _x608 ≤ _x602
f3192_0_dual_LE	53	f3931_0_sublistAutoDual_InvokeMethod:	x1 = _x614 ∧ x2 = _x615 ∧ x3 = _x616 ∧ x4 = _x617 ∧ x5 = _x618 ∧ x6 = _x619 ∧ x1 = _x620 ∧ x2 = _x621 ∧ x3 = _x622 ∧ x4 = _x623 ∧ x5 = _x624 ∧ x6 = _x625 ∧ _x618 = _x624 ∧ _x618 = _x619 ∧ _x618 + 2 ≤ _x615 ∧ _x623 + 6 ≤ _x614 ∧ _x618 + 4 ≤ _x614 ∧ −1 ≤ _x622 − 1 ∧ 0 ≤ _x621 − 1 ∧ 5 ≤ _x620 − 1 ∧ −1 ≤ _x616 − 1 ∧ 0 ≤ _x615 − 1 ∧ 5 ≤ _x614 − 1 ∧ _x622 ≤ _x616 ∧ _x621 ≤ _x615 ∧ _x621 + 2 ≤ _x614 ∧ _x617 ≤ 0 ∧ _x620 ≤ _x614
f3931_0_sublistAutoDual_InvokeMethod	54	f2503_0_isEqual_NONNULL:	x1 = _x626 ∧ x2 = _x627 ∧ x3 = _x628 ∧ x4 = _x629 ∧ x5 = _x632 ∧ x6 = _x633 ∧ x1 = _x634 ∧ x2 = _x637 ∧ x3 = _x638 ∧ x4 = _x639 ∧ x5 = _x640 ∧ x6 = _x642 ∧ _x632 + 2 ≤ _x627 ∧ _x629 + 6 ≤ _x626 ∧ _x632 + 4 ≤ _x626 ∧ −1 ≤ _x637 − 1 ∧ 0 ≤ _x634 − 1 ∧ −1 ≤ _x628 − 1 ∧ 0 ≤ _x627 − 1 ∧ 4 ≤ _x626 − 1 ∧ _x637 ≤ _x628 ∧ _x634 ≤ _x627 ∧ _x634 + 2 ≤ _x626
f3931_0_sublistAutoDual_InvokeMethod	55	f3984_0_sublistAutoDual_NE:	x1 = _x643 ∧ x2 = _x644 ∧ x3 = _x645 ∧ x4 = _x647 ∧ x5 = _x648 ∧ x6 = _x649 ∧ x1 = _x650 ∧ x2 = _x652 ∧ x3 = _x653 ∧ x4 = _x654 ∧ x5 = _x655 ∧ x6 = _x657 ∧ 0 = _x653 ∧ _x648 + 2 ≤ _x644 ∧ _x647 + 6 ≤ _x643 ∧ _x648 + 4 ≤ _x643 ∧ 0 ≤ _x652 − 1 ∧ 4 ≤ _x650 − 1 ∧ 0 ≤ _x645 − 1 ∧ 1 ≤ _x644 − 1 ∧ 4 ≤ _x643 − 1 ∧ _x652 ≤ _x645 ∧ _x650 ≤ _x643
f3931_0_sublistAutoDual_InvokeMethod	56	f3984_0_sublistAutoDual_NE:	x1 = _x658 ∧ x2 = _x659 ∧ x3 = _x660 ∧ x4 = _x661 ∧ x5 = _x662 ∧ x6 = _x663 ∧ x1 = _x664 ∧ x2 = _x665 ∧ x3 = _x666 ∧ x4 = _x667 ∧ x5 = _x668 ∧ x6 = _x669 ∧ 0 = _x666 ∧ _x662 + 2 ≤ _x660 ∧ _x662 + 2 ≤ _x659 ∧ _x661 + 6 ≤ _x658 ∧ _x662 + 4 ≤ _x658 ∧ 2 ≤ _x665 − 1 ∧ 4 ≤ _x664 − 1 ∧ 2 ≤ _x660 − 1 ∧ 1 ≤ _x659 − 1 ∧ 4 ≤ _x658 − 1 ∧ _x665 ≤ _x660 ∧ _x664 ≤ _x658
f3931_0_sublistAutoDual_InvokeMethod	57	f3984_0_sublistAutoDual_NE:	x1 = _x670 ∧ x2 = _x671 ∧ x3 = _x672 ∧ x4 = _x673 ∧ x5 = _x674 ∧ x6 = _x675 ∧ x1 = _x676 ∧ x2 = _x677 ∧ x3 = _x678 ∧ x4 = _x679 ∧ x5 = _x680 ∧ x6 = _x681 ∧ 1 = _x678 ∧ _x674 + 2 ≤ _x672 ∧ _x674 + 2 ≤ _x671 ∧ _x673 + 6 ≤ _x670 ∧ _x674 + 4 ≤ _x670 ∧ 1 ≤ _x677 − 1 ∧ 4 ≤ _x676 − 1 ∧ 1 ≤ _x672 − 1 ∧ 1 ≤ _x671 − 1 ∧ 4 ≤ _x670 − 1 ∧ _x677 ≤ _x672 ∧ _x677 ≤ _x671 ∧ _x677 + 2 ≤ _x670 ∧ _x676 ≤ _x670
f3931_0_sublistAutoDual_InvokeMethod	58	f3985_0_sublistAutoDual_NE:	x1 = _x682 ∧ x2 = _x683 ∧ x3 = _x684 ∧ x4 = _x685 ∧ x5 = _x686 ∧ x6 = _x687 ∧ x1 = _x688 ∧ x2 = _x689 ∧ x3 = _x690 ∧ x4 = _x692 ∧ x5 = _x693 ∧ x6 = _x694 ∧ 0 = _x690 ∧ _x686 + 2 ≤ _x683 ∧ _x685 + 6 ≤ _x682 ∧ _x686 + 4 ≤ _x682 ∧ 0 ≤ _x689 − 1 ∧ 4 ≤ _x688 − 1 ∧ 0 ≤ _x684 − 1 ∧ 2 ≤ _x683 − 1 ∧ 4 ≤ _x682 − 1 ∧ _x689 ≤ _x684 ∧ _x688 ≤ _x682
f3931_0_sublistAutoDual_InvokeMethod	59	f3985_0_sublistAutoDual_NE:	x1 = _x697 ∧ x2 = _x698 ∧ x3 = _x699 ∧ x4 = _x702 ∧ x5 = _x703 ∧ x6 = _x704 ∧ x1 = _x707 ∧ x2 = _x708 ∧ x3 = _x709 ∧ x4 = _x710 ∧ x5 = _x711 ∧ x6 = _x713 ∧ 0 = _x709 ∧ _x703 + 2 ≤ _x699 ∧ _x703 + 2 ≤ _x698 ∧ _x702 + 6 ≤ _x697 ∧ _x703 + 4 ≤ _x697 ∧ 1 ≤ _x708 − 1 ∧ 4 ≤ _x707 − 1 ∧ 1 ≤ _x699 − 1 ∧ 2 ≤ _x698 − 1 ∧ 4 ≤ _x697 − 1 ∧ _x708 ≤ _x699 ∧ _x708 ≤ _x698 ∧ _x708 + 2 ≤ _x697 ∧ _x707 ≤ _x697
f3931_0_sublistAutoDual_InvokeMethod	60	f3985_0_sublistAutoDual_NE:	x1 = _x714 ∧ x2 = _x715 ∧ x3 = _x716 ∧ x4 = _x717 ∧ x5 = _x719 ∧ x6 = _x720 ∧ x1 = _x721 ∧ x2 = _x722 ∧ x3 = _x723 ∧ x4 = _x725 ∧ x5 = _x726 ∧ x6 = _x727 ∧ 0 = _x723 ∧ _x719 + 2 ≤ _x716 ∧ _x719 + 2 ≤ _x715 ∧ _x717 + 6 ≤ _x714 ∧ _x719 + 4 ≤ _x714 ∧ 2 ≤ _x722 − 1 ∧ 5 ≤ _x721 − 1 ∧ 2 ≤ _x716 − 1 ∧ 3 ≤ _x715 − 1 ∧ 5 ≤ _x714 − 1 ∧ _x722 ≤ _x716 ∧ _x721 ≤ _x714
f3931_0_sublistAutoDual_InvokeMethod	61	f3985_0_sublistAutoDual_NE:	x1 = _x728 ∧ x2 = _x729 ∧ x3 = _x731 ∧ x4 = _x732 ∧ x5 = _x733 ∧ x6 = _x734 ∧ x1 = _x736 ∧ x2 = _x737 ∧ x3 = _x738 ∧ x4 = _x739 ∧ x5 = _x741 ∧ x6 = _x742 ∧ 1 = _x738 ∧ _x733 + 2 ≤ _x731 ∧ _x733 + 2 ≤ _x729 ∧ _x732 + 6 ≤ _x728 ∧ _x733 + 4 ≤ _x728 ∧ 2 ≤ _x737 − 1 ∧ 5 ≤ _x736 − 1 ∧ 2 ≤ _x731 − 1 ∧ 3 ≤ _x729 − 1 ∧ 5 ≤ _x728 − 1 ∧ _x737 ≤ _x731 ∧ _x736 ≤ _x728
f3931_0_sublistAutoDual_InvokeMethod	62	f3985_0_sublistAutoDual_NE:	x1 = _x743 ∧ x2 = _x744 ∧ x3 = _x746 ∧ x4 = _x747 ∧ x5 = _x748 ∧ x6 = _x749 ∧ x1 = _x751 ∧ x2 = _x752 ∧ x3 = _x753 ∧ x4 = _x754 ∧ x5 = _x756 ∧ x6 = _x757 ∧ 0 = _x753 ∧ _x748 + 2 ≤ _x746 ∧ _x748 + 2 ≤ _x744 ∧ _x747 + 6 ≤ _x743 ∧ _x748 + 4 ≤ _x743 ∧ 2 ≤ _x752 − 1 ∧ 6 ≤ _x751 − 1 ∧ 2 ≤ _x746 − 1 ∧ 4 ≤ _x744 − 1 ∧ 6 ≤ _x743 − 1 ∧ _x752 ≤ _x746 ∧ _x751 ≤ _x743
f3931_0_sublistAutoDual_InvokeMethod	63	f3985_0_sublistAutoDual_NE:	x1 = _x758 ∧ x2 = _x759 ∧ x3 = _x761 ∧ x4 = _x762 ∧ x5 = _x763 ∧ x6 = _x764 ∧ x1 = _x766 ∧ x2 = _x767 ∧ x3 = _x768 ∧ x4 = _x769 ∧ x5 = _x771 ∧ x6 = _x772 ∧ 1 = _x768 ∧ _x763 + 2 ≤ _x761 ∧ _x763 + 2 ≤ _x759 ∧ _x762 + 6 ≤ _x758 ∧ _x763 + 4 ≤ _x758 ∧ 2 ≤ _x767 − 1 ∧ 6 ≤ _x766 − 1 ∧ 2 ≤ _x761 − 1 ∧ 4 ≤ _x759 − 1 ∧ 6 ≤ _x758 − 1 ∧ _x767 ≤ _x761 ∧ _x766 ≤ _x758
f3192_0_dual_LE	64	f4135_0_sublistAutoDual_InvokeMethod:	x1 = _x773 ∧ x2 = _x774 ∧ x3 = _x776 ∧ x4 = _x777 ∧ x5 = _x778 ∧ x6 = _x779 ∧ x1 = _x781 ∧ x2 = _x782 ∧ x3 = _x783 ∧ x4 = _x784 ∧ x5 = _x786 ∧ x6 = _x787 ∧ _x778 = _x786 ∧ _x778 = _x779 ∧ _x778 + 2 ≤ _x774 ∧ _x784 + 6 ≤ _x773 ∧ _x778 + 4 ≤ _x773 ∧ −1 ≤ _x783 − 1 ∧ 0 ≤ _x782 − 1 ∧ 6 ≤ _x781 − 1 ∧ −1 ≤ _x776 − 1 ∧ 0 ≤ _x774 − 1 ∧ 6 ≤ _x773 − 1 ∧ _x783 ≤ _x776 ∧ _x782 ≤ _x774 ∧ _x782 + 2 ≤ _x773 ∧ _x777 ≤ 0 ∧ _x781 ≤ _x773
f3192_0_dual_LE	65	f4135_0_sublistAutoDual_InvokeMethod:	x1 = _x788 ∧ x2 = _x789 ∧ x3 = _x791 ∧ x4 = _x792 ∧ x5 = _x793 ∧ x6 = _x794 ∧ x1 = _x795 ∧ x2 = _x796 ∧ x3 = _x797 ∧ x4 = _x798 ∧ x5 = _x799 ∧ x6 = _x800 ∧ _x793 = _x799 ∧ _x793 = _x794 ∧ _x793 + 2 ≤ _x789 ∧ _x798 + 6 ≤ _x788 ∧ _x793 + 4 ≤ _x788 ∧ −1 ≤ _x797 − 1 ∧ 0 ≤ _x796 − 1 ∧ 5 ≤ _x795 − 1 ∧ −1 ≤ _x791 − 1 ∧ 0 ≤ _x789 − 1 ∧ 5 ≤ _x788 − 1 ∧ _x797 ≤ _x791 ∧ _x796 ≤ _x789 ∧ _x796 + 2 ≤ _x788 ∧ _x792 ≤ 0 ∧ _x795 ≤ _x788
f4135_0_sublistAutoDual_InvokeMethod	66	f2503_0_isEqual_NONNULL:	x1 = _x801 ∧ x2 = _x802 ∧ x3 = _x803 ∧ x4 = _x804 ∧ x5 = _x805 ∧ x6 = _x806 ∧ x1 = _x807 ∧ x2 = _x808 ∧ x3 = _x809 ∧ x4 = _x810 ∧ x5 = _x811 ∧ x6 = _x812 ∧ _x805 + 2 ≤ _x802 ∧ _x804 + 6 ≤ _x801 ∧ _x805 + 4 ≤ _x801 ∧ −1 ≤ _x808 − 1 ∧ 0 ≤ _x807 − 1 ∧ −1 ≤ _x803 − 1 ∧ 0 ≤ _x802 − 1 ∧ 4 ≤ _x801 − 1 ∧ _x808 ≤ _x803 ∧ _x807 ≤ _x802 ∧ _x807 + 2 ≤ _x801
f4135_0_sublistAutoDual_InvokeMethod	67	f3984_0_sublistAutoDual_NE:	x1 = _x813 ∧ x2 = _x814 ∧ x3 = _x815 ∧ x4 = _x816 ∧ x5 = _x817 ∧ x6 = _x818 ∧ x1 = _x819 ∧ x2 = _x820 ∧ x3 = _x821 ∧ x4 = _x822 ∧ x5 = _x823 ∧ x6 = _x824 ∧ 0 = _x821 ∧ _x817 + 2 ≤ _x814 ∧ _x816 + 6 ≤ _x813 ∧ _x817 + 4 ≤ _x813 ∧ 0 ≤ _x820 − 1 ∧ 4 ≤ _x819 − 1 ∧ 0 ≤ _x815 − 1 ∧ 1 ≤ _x814 − 1 ∧ 4 ≤ _x813 − 1 ∧ _x820 ≤ _x815 ∧ _x819 ≤ _x813
f4135_0_sublistAutoDual_InvokeMethod	68	f3984_0_sublistAutoDual_NE:	x1 = _x825 ∧ x2 = _x826 ∧ x3 = _x827 ∧ x4 = _x828 ∧ x5 = _x829 ∧ x6 = _x830 ∧ x1 = _x831 ∧ x2 = _x832 ∧ x3 = _x833 ∧ x4 = _x834 ∧ x5 = _x835 ∧ x6 = _x836 ∧ 0 = _x833 ∧ _x829 + 2 ≤ _x827 ∧ _x829 + 2 ≤ _x826 ∧ _x828 + 6 ≤ _x825 ∧ _x829 + 4 ≤ _x825 ∧ 2 ≤ _x832 − 1 ∧ 4 ≤ _x831 − 1 ∧ 2 ≤ _x827 − 1 ∧ 1 ≤ _x826 − 1 ∧ 4 ≤ _x825 − 1 ∧ _x832 ≤ _x827 ∧ _x831 ≤ _x825
f4135_0_sublistAutoDual_InvokeMethod	69	f3984_0_sublistAutoDual_NE:	x1 = _x837 ∧ x2 = _x838 ∧ x3 = _x839 ∧ x4 = _x840 ∧ x5 = _x841 ∧ x6 = _x842 ∧ x1 = _x843 ∧ x2 = _x844 ∧ x3 = _x845 ∧ x4 = _x846 ∧ x5 = _x847 ∧ x6 = _x848 ∧ 1 = _x845 ∧ _x841 + 2 ≤ _x839 ∧ _x841 + 2 ≤ _x838 ∧ _x840 + 6 ≤ _x837 ∧ _x841 + 4 ≤ _x837 ∧ 1 ≤ _x844 − 1 ∧ 4 ≤ _x843 − 1 ∧ 1 ≤ _x839 − 1 ∧ 1 ≤ _x838 − 1 ∧ 4 ≤ _x837 − 1 ∧ _x844 ≤ _x839 ∧ _x844 ≤ _x838 ∧ _x844 + 2 ≤ _x837 ∧ _x843 ≤ _x837
f4135_0_sublistAutoDual_InvokeMethod	70	f3985_0_sublistAutoDual_NE:	x1 = _x849 ∧ x2 = _x850 ∧ x3 = _x851 ∧ x4 = _x852 ∧ x5 = _x853 ∧ x6 = _x854 ∧ x1 = _x855 ∧ x2 = _x856 ∧ x3 = _x857 ∧ x4 = _x858 ∧ x5 = _x859 ∧ x6 = _x860 ∧ 0 = _x857 ∧ _x853 + 2 ≤ _x850 ∧ _x852 + 6 ≤ _x849 ∧ _x853 + 4 ≤ _x849 ∧ 0 ≤ _x856 − 1 ∧ 4 ≤ _x855 − 1 ∧ 0 ≤ _x851 − 1 ∧ 2 ≤ _x850 − 1 ∧ 4 ≤ _x849 − 1 ∧ _x856 ≤ _x851 ∧ _x855 ≤ _x849
f4135_0_sublistAutoDual_InvokeMethod	71	f3985_0_sublistAutoDual_NE:	x1 = _x861 ∧ x2 = _x862 ∧ x3 = _x863 ∧ x4 = _x864 ∧ x5 = _x865 ∧ x6 = _x866 ∧ x1 = _x867 ∧ x2 = _x868 ∧ x3 = _x869 ∧ x4 = _x870 ∧ x5 = _x871 ∧ x6 = _x872 ∧ 0 = _x869 ∧ _x865 + 2 ≤ _x863 ∧ _x865 + 2 ≤ _x862 ∧ _x864 + 6 ≤ _x861 ∧ _x865 + 4 ≤ _x861 ∧ 1 ≤ _x868 − 1 ∧ 4 ≤ _x867 − 1 ∧ 1 ≤ _x863 − 1 ∧ 2 ≤ _x862 − 1 ∧ 4 ≤ _x861 − 1 ∧ _x868 ≤ _x863 ∧ _x868 ≤ _x862 ∧ _x868 + 2 ≤ _x861 ∧ _x867 ≤ _x861
f4135_0_sublistAutoDual_InvokeMethod	72	f3985_0_sublistAutoDual_NE:	x1 = _x873 ∧ x2 = _x874 ∧ x3 = _x875 ∧ x4 = _x876 ∧ x5 = _x877 ∧ x6 = _x878 ∧ x1 = _x879 ∧ x2 = _x880 ∧ x3 = _x881 ∧ x4 = _x882 ∧ x5 = _x883 ∧ x6 = _x884 ∧ 0 = _x881 ∧ _x877 + 2 ≤ _x875 ∧ _x877 + 2 ≤ _x874 ∧ _x876 + 6 ≤ _x873 ∧ _x877 + 4 ≤ _x873 ∧ 2 ≤ _x880 − 1 ∧ 5 ≤ _x879 − 1 ∧ 2 ≤ _x875 − 1 ∧ 3 ≤ _x874 − 1 ∧ 5 ≤ _x873 − 1 ∧ _x880 ≤ _x875 ∧ _x879 ≤ _x873
f4135_0_sublistAutoDual_InvokeMethod	73	f3985_0_sublistAutoDual_NE:	x1 = _x885 ∧ x2 = _x886 ∧ x3 = _x887 ∧ x4 = _x888 ∧ x5 = _x889 ∧ x6 = _x890 ∧ x1 = _x891 ∧ x2 = _x892 ∧ x3 = _x893 ∧ x4 = _x894 ∧ x5 = _x895 ∧ x6 = _x896 ∧ 1 = _x893 ∧ _x889 + 2 ≤ _x887 ∧ _x889 + 2 ≤ _x886 ∧ _x888 + 6 ≤ _x885 ∧ _x889 + 4 ≤ _x885 ∧ 2 ≤ _x892 − 1 ∧ 5 ≤ _x891 − 1 ∧ 2 ≤ _x887 − 1 ∧ 3 ≤ _x886 − 1 ∧ 5 ≤ _x885 − 1 ∧ _x892 ≤ _x887 ∧ _x891 ≤ _x885
f4135_0_sublistAutoDual_InvokeMethod	74	f3985_0_sublistAutoDual_NE:	x1 = _x897 ∧ x2 = _x898 ∧ x3 = _x899 ∧ x4 = _x900 ∧ x5 = _x901 ∧ x6 = _x902 ∧ x1 = _x903 ∧ x2 = _x904 ∧ x3 = _x905 ∧ x4 = _x906 ∧ x5 = _x907 ∧ x6 = _x908 ∧ 0 = _x905 ∧ _x901 + 2 ≤ _x899 ∧ _x901 + 2 ≤ _x898 ∧ _x900 + 6 ≤ _x897 ∧ _x901 + 4 ≤ _x897 ∧ 2 ≤ _x904 − 1 ∧ 6 ≤ _x903 − 1 ∧ 2 ≤ _x899 − 1 ∧ 4 ≤ _x898 − 1 ∧ 6 ≤ _x897 − 1 ∧ _x904 ≤ _x899 ∧ _x903 ≤ _x897
f4135_0_sublistAutoDual_InvokeMethod	75	f3985_0_sublistAutoDual_NE:	x1 = _x909 ∧ x2 = _x910 ∧ x3 = _x911 ∧ x4 = _x912 ∧ x5 = _x913 ∧ x6 = _x914 ∧ x1 = _x915 ∧ x2 = _x916 ∧ x3 = _x917 ∧ x4 = _x918 ∧ x5 = _x919 ∧ x6 = _x920 ∧ 1 = _x917 ∧ _x913 + 2 ≤ _x911 ∧ _x913 + 2 ≤ _x910 ∧ _x912 + 6 ≤ _x909 ∧ _x913 + 4 ≤ _x909 ∧ 2 ≤ _x916 − 1 ∧ 6 ≤ _x915 − 1 ∧ 2 ≤ _x911 − 1 ∧ 4 ≤ _x910 − 1 ∧ 6 ≤ _x909 − 1 ∧ _x916 ≤ _x911 ∧ _x915 ≤ _x909
f3192_0_dual_LE	76	f1674_0_number_greater_LT:	x1 = _x921 ∧ x2 = _x922 ∧ x3 = _x923 ∧ x4 = _x924 ∧ x5 = _x925 ∧ x6 = _x926 ∧ x1 = _x927 ∧ x2 = _x928 ∧ x3 = _x929 ∧ x4 = _x930 ∧ x5 = _x931 ∧ x6 = _x932 ∧ _x925 = _x929 ∧ _x924 = _x928 ∧ _x925 = _x926 ∧ _x925 + 2 ≤ _x922 ∧ _x925 + 4 ≤ _x921 ∧ 0 ≤ _x927 − 1 ∧ −1 ≤ _x923 − 1 ∧ 0 ≤ _x922 − 1 ∧ 2 ≤ _x921 − 1 ∧ _x927 ≤ _x922 ∧ 0 ≤ _x924 − 1 ∧ _x927 + 2 ≤ _x921
f1674_0_number_greater_LT	77	f1674_0_number_greater_LT:	x1 = _x933 ∧ x2 = _x934 ∧ x3 = _x935 ∧ x4 = _x936 ∧ x5 = _x937 ∧ x6 = _x938 ∧ x1 = _x939 ∧ x2 = _x940 ∧ x3 = _x941 ∧ x4 = _x942 ∧ x5 = _x943 ∧ x6 = _x944 ∧ _x934 = _x940 ∧ _x941 + 4 ≤ _x933 ∧ _x935 + 2 ≤ _x933 ∧ 0 ≤ _x939 − 1 ∧ 2 ≤ _x933 − 1 ∧ _x939 + 2 ≤ _x933 ∧ _x935 ≤ _x934 − 1 ∧ 0 ≤ _x934 − 1
f1674_0_number_greater_LT	78	f1674_0_number_greater_LT:	x1 = _x945 ∧ x2 = _x946 ∧ x3 = _x947 ∧ x4 = _x948 ∧ x5 = _x949 ∧ x6 = _x950 ∧ x1 = _x951 ∧ x2 = _x952 ∧ x3 = _x953 ∧ x4 = _x954 ∧ x5 = _x955 ∧ x6 = _x956 ∧ _x946 = _x952 ∧ _x953 + 4 ≤ _x945 ∧ _x947 + 2 ≤ _x945 ∧ 0 ≤ _x951 − 1 ∧ 2 ≤ _x945 − 1 ∧ _x951 + 2 ≤ _x945 ∧ 0 ≤ _x946 − 1 ∧ _x946 ≤ _x947 ∧ 0 ≤ _x947 − 1
f2503_0_isEqual_NONNULL	79	f2503_0_isEqual_NONNULL:	x1 = _x957 ∧ x2 = _x958 ∧ x3 = _x959 ∧ x4 = _x960 ∧ x5 = _x961 ∧ x6 = _x962 ∧ x1 = _x963 ∧ x2 = _x964 ∧ x3 = _x965 ∧ x4 = _x966 ∧ x5 = _x967 ∧ x6 = _x968 ∧ −1 ≤ _x964 − 1 ∧ 0 ≤ _x963 − 1 ∧ 0 ≤ _x958 − 1 ∧ 2 ≤ _x957 − 1 ∧ _x964 + 1 ≤ _x958 ∧ _x963 + 2 ≤ _x957
f2503_0_isEqual_NONNULL	80	f2881_0_isEqual_EQ:	x1 = _x969 ∧ x2 = _x970 ∧ x3 = _x971 ∧ x4 = _x972 ∧ x5 = _x973 ∧ x6 = _x974 ∧ x1 = _x975 ∧ x2 = _x976 ∧ x3 = _x977 ∧ x4 = _x978 ∧ x5 = _x979 ∧ x6 = _x980 ∧ 0 = _x977 ∧ 2 ≤ _x976 − 1 ∧ 4 ≤ _x975 − 1 ∧ 2 ≤ _x970 − 1 ∧ 4 ≤ _x969 − 1 ∧ _x976 ≤ _x970 ∧ _x975 ≤ _x969
f2503_0_isEqual_NONNULL	81	f2881_0_isEqual_EQ:	x1 = _x981 ∧ x2 = _x982 ∧ x3 = _x983 ∧ x4 = _x984 ∧ x5 = _x985 ∧ x6 = _x986 ∧ x1 = _x987 ∧ x2 = _x988 ∧ x3 = _x989 ∧ x4 = _x990 ∧ x5 = _x991 ∧ x6 = _x992 ∧ 0 = _x989 ∧ 3 ≤ _x988 − 1 ∧ 4 ≤ _x987 − 1 ∧ 3 ≤ _x982 − 1 ∧ 4 ≤ _x981 − 1 ∧ _x988 ≤ _x982 ∧ _x988 ≤ _x981 ∧ _x987 ≤ _x981
f2503_0_isEqual_NONNULL	82	f2881_0_isEqual_EQ:	x1 = _x993 ∧ x2 = _x994 ∧ x3 = _x995 ∧ x4 = _x996 ∧ x5 = _x997 ∧ x6 = _x998 ∧ x1 = _x999 ∧ x2 = _x1000 ∧ x3 = _x1001 ∧ x4 = _x1002 ∧ x5 = _x1003 ∧ x6 = _x1004 ∧ 0 = _x1001 ∧ 4 ≤ _x1000 − 1 ∧ 5 ≤ _x999 − 1 ∧ 4 ≤ _x994 − 1 ∧ 5 ≤ _x993 − 1 ∧ _x1000 ≤ _x994 ∧ _x999 ≤ _x993
f2503_0_isEqual_NONNULL	83	f2881_0_isEqual_EQ:	x1 = _x1005 ∧ x2 = _x1006 ∧ x3 = _x1007 ∧ x4 = _x1008 ∧ x5 = _x1009 ∧ x6 = _x1010 ∧ x1 = _x1011 ∧ x2 = _x1012 ∧ x3 = _x1013 ∧ x4 = _x1014 ∧ x5 = _x1015 ∧ x6 = _x1016 ∧ 1 = _x1013 ∧ 4 ≤ _x1012 − 1 ∧ 5 ≤ _x1011 − 1 ∧ 4 ≤ _x1006 − 1 ∧ 5 ≤ _x1005 − 1 ∧ _x1012 ≤ _x1006 ∧ _x1011 ≤ _x1005
f2503_0_isEqual_NONNULL	84	f2881_0_isEqual_EQ:	x1 = _x1017 ∧ x2 = _x1018 ∧ x3 = _x1019 ∧ x4 = _x1020 ∧ x5 = _x1021 ∧ x6 = _x1022 ∧ x1 = _x1023 ∧ x2 = _x1024 ∧ x3 = _x1025 ∧ x4 = _x1026 ∧ x5 = _x1027 ∧ x6 = _x1028 ∧ 0 = _x1025 ∧ 4 ≤ _x1024 − 1 ∧ 6 ≤ _x1023 − 1 ∧ 4 ≤ _x1018 − 1 ∧ 6 ≤ _x1017 − 1 ∧ _x1024 ≤ _x1018 ∧ _x1023 ≤ _x1017
f2503_0_isEqual_NONNULL	85	f2881_0_isEqual_EQ:	x1 = _x1029 ∧ x2 = _x1030 ∧ x3 = _x1031 ∧ x4 = _x1032 ∧ x5 = _x1033 ∧ x6 = _x1034 ∧ x1 = _x1035 ∧ x2 = _x1036 ∧ x3 = _x1037 ∧ x4 = _x1038 ∧ x5 = _x1039 ∧ x6 = _x1040 ∧ 1 = _x1037 ∧ 4 ≤ _x1036 − 1 ∧ 6 ≤ _x1035 − 1 ∧ 4 ≤ _x1030 − 1 ∧ 6 ≤ _x1029 − 1 ∧ _x1036 ≤ _x1030 ∧ _x1035 ≤ _x1029
f2503_0_isEqual_NONNULL	86	f2774_0_isEqual_EQ:	x1 = _x1041 ∧ x2 = _x1042 ∧ x3 = _x1043 ∧ x4 = _x1044 ∧ x5 = _x1045 ∧ x6 = _x1046 ∧ x1 = _x1047 ∧ x2 = _x1048 ∧ x3 = _x1049 ∧ x4 = _x1050 ∧ x5 = _x1051 ∧ x6 = _x1052 ∧ 0 = _x1049 ∧ 2 ≤ _x1048 − 1 ∧ 3 ≤ _x1047 − 1 ∧ 2 ≤ _x1042 − 1 ∧ 3 ≤ _x1041 − 1 ∧ _x1048 ≤ _x1042 ∧ _x1047 ≤ _x1041
f2503_0_isEqual_NONNULL	87	f2774_0_isEqual_EQ:	x1 = _x1053 ∧ x2 = _x1054 ∧ x3 = _x1055 ∧ x4 = _x1056 ∧ x5 = _x1057 ∧ x6 = _x1058 ∧ x1 = _x1059 ∧ x2 = _x1060 ∧ x3 = _x1061 ∧ x4 = _x1062 ∧ x5 = _x1063 ∧ x6 = _x1064 ∧ 0 = _x1061 ∧ 4 ≤ _x1060 − 1 ∧ 3 ≤ _x1059 − 1 ∧ 4 ≤ _x1054 − 1 ∧ 3 ≤ _x1053 − 1 ∧ _x1060 ≤ _x1054 ∧ _x1059 ≤ _x1054 ∧ _x1059 ≤ _x1053
f2503_0_isEqual_NONNULL	88	f2774_0_isEqual_EQ:	x1 = _x1065 ∧ x2 = _x1066 ∧ x3 = _x1067 ∧ x4 = _x1068 ∧ x5 = _x1069 ∧ x6 = _x1070 ∧ x1 = _x1071 ∧ x2 = _x1072 ∧ x3 = _x1073 ∧ x4 = _x1074 ∧ x5 = _x1075 ∧ x6 = _x1076 ∧ 1 = _x1073 ∧ 3 ≤ _x1072 − 1 ∧ 3 ≤ _x1071 − 1 ∧ 3 ≤ _x1066 − 1 ∧ 3 ≤ _x1065 − 1 ∧ _x1072 ≤ _x1066 ∧ _x1072 ≤ _x1065 ∧ _x1071 ≤ _x1066 ∧ _x1071 ≤ _x1065
f4119_0_main_InvokeMethod	89	f4661_0_sublistOddDistinctParts_InvokeMethod:	x1 = _x1077 ∧ x2 = _x1078 ∧ x3 = _x1079 ∧ x4 = _x1080 ∧ x5 = _x1081 ∧ x6 = _x1082 ∧ x1 = _x1083 ∧ x2 = _x1084 ∧ x3 = _x1085 ∧ x4 = _x1086 ∧ x5 = _x1087 ∧ x6 = _x1088 ∧ _x1078 + 4 ≤ _x1077 ∧ 0 ≤ _x1084 − 1 ∧ 2 ≤ _x1083 − 1 ∧ 2 ≤ _x1077 − 1 ∧ _x1084 + 2 ≤ _x1077 ∧ _x1083 ≤ _x1077
f4661_0_sublistOddDistinctParts_InvokeMethod	90	f4740_0_sublistOddDistinctParts_NULL:	x1 = _x1089 ∧ x2 = _x1090 ∧ x3 = _x1091 ∧ x4 = _x1092 ∧ x5 = _x1093 ∧ x6 = _x1094 ∧ x1 = _x1095 ∧ x2 = _x1096 ∧ x3 = _x1097 ∧ x4 = _x1098 ∧ x5 = _x1099 ∧ x6 = _x1100 ∧ _x1097 + 2 ≤ _x1090 ∧ _x1097 + 4 ≤ _x1089 ∧ −1 ≤ _x1096 − 1 ∧ 2 ≤ _x1095 − 1 ∧ 0 ≤ _x1090 − 1 ∧ 2 ≤ _x1089 − 1 ∧ _x1096 + 2 ≤ _x1089 ∧ _x1095 ≤ _x1089
f4740_0_sublistOddDistinctParts_NULL	91	f4661_0_sublistOddDistinctParts_InvokeMethod:	x1 = _x1101 ∧ x2 = _x1102 ∧ x3 = _x1103 ∧ x4 = _x1104 ∧ x5 = _x1105 ∧ x6 = _x1106 ∧ x1 = _x1107 ∧ x2 = _x1108 ∧ x3 = _x1109 ∧ x4 = _x1110 ∧ x5 = _x1111 ∧ x6 = _x1112 ∧ _x1103 + 4 ≤ _x1101 ∧ −1 ≤ _x1108 − 1 ∧ 0 ≤ _x1107 − 1 ∧ 0 ≤ _x1102 − 1 ∧ 2 ≤ _x1101 − 1 ∧ _x1108 + 1 ≤ _x1102 ∧ _x1108 + 3 ≤ _x1101 ∧ _x1107 ≤ _x1102 ∧ _x1107 + 2 ≤ _x1101
f4661_0_sublistOddDistinctParts_InvokeMethod	92	f4661_0_sublistOddDistinctParts_InvokeMethod:	x1 = _x1113 ∧ x2 = _x1114 ∧ x3 = _x1115 ∧ x4 = _x1116 ∧ x5 = _x1117 ∧ x6 = _x1118 ∧ x1 = _x1119 ∧ x2 = _x1120 ∧ x3 = _x1121 ∧ x4 = _x1122 ∧ x5 = _x1123 ∧ x6 = _x1124 ∧ −1 ≤ _x1120 − 1 ∧ 0 ≤ _x1119 − 1 ∧ 1 ≤ _x1114 − 1 ∧ 3 ≤ _x1113 − 1 ∧ _x1120 + 4 ≤ _x1113 ∧ _x1119 + 2 ≤ _x1113
f4661_0_sublistOddDistinctParts_InvokeMethod	93	f4854_0_sublistOddDistinctParts_EQ:	x1 = _x1125 ∧ x2 = _x1126 ∧ x3 = _x1127 ∧ x4 = _x1128 ∧ x5 = _x1129 ∧ x6 = _x1130 ∧ x1 = _x1131 ∧ x2 = _x1132 ∧ x3 = _x1133 ∧ x4 = _x1134 ∧ x5 = _x1135 ∧ x6 = _x1136 ∧ 1 = _x1132 ∧ _x1134 + 4 ≤ _x1126 ∧ _x1133 + 2 ≤ _x1126 ∧ _x1134 + 6 ≤ _x1125 ∧ _x1133 + 4 ≤ _x1125 ∧ 5 ≤ _x1131 − 1 ∧ 3 ≤ _x1126 − 1 ∧ 5 ≤ _x1125 − 1 ∧ _x1131 ≤ _x1125
f4661_0_sublistOddDistinctParts_InvokeMethod	94	f4854_0_sublistOddDistinctParts_EQ:	x1 = _x1137 ∧ x2 = _x1138 ∧ x3 = _x1139 ∧ x4 = _x1140 ∧ x5 = _x1141 ∧ x6 = _x1142 ∧ x1 = _x1143 ∧ x2 = _x1144 ∧ x3 = _x1145 ∧ x4 = _x1146 ∧ x5 = _x1147 ∧ x6 = _x1148 ∧ 0 = _x1144 ∧ _x1146 + 4 ≤ _x1138 ∧ _x1145 + 2 ≤ _x1138 ∧ _x1146 + 6 ≤ _x1137 ∧ _x1145 + 4 ≤ _x1137 ∧ 6 ≤ _x1143 − 1 ∧ 4 ≤ _x1138 − 1 ∧ 6 ≤ _x1137 − 1 ∧ _x1143 ≤ _x1137
f4661_0_sublistOddDistinctParts_InvokeMethod	95	f4854_0_sublistOddDistinctParts_EQ:	x1 = _x1149 ∧ x2 = _x1150 ∧ x3 = _x1151 ∧ x4 = _x1152 ∧ x5 = _x1153 ∧ x6 = _x1154 ∧ x1 = _x1155 ∧ x2 = _x1156 ∧ x3 = _x1157 ∧ x4 = _x1158 ∧ x5 = _x1159 ∧ x6 = _x1160 ∧ 1 = _x1156 ∧ _x1158 + 4 ≤ _x1150 ∧ _x1157 + 2 ≤ _x1150 ∧ _x1158 + 6 ≤ _x1149 ∧ _x1157 + 4 ≤ _x1149 ∧ 6 ≤ _x1155 − 1 ∧ 4 ≤ _x1150 − 1 ∧ 6 ≤ _x1149 − 1 ∧ _x1155 ≤ _x1149
f4661_0_sublistOddDistinctParts_InvokeMethod	96	f4854_0_sublistOddDistinctParts_EQ:	x1 = _x1161 ∧ x2 = _x1162 ∧ x3 = _x1163 ∧ x4 = _x1164 ∧ x5 = _x1165 ∧ x6 = _x1166 ∧ x1 = _x1167 ∧ x2 = _x1168 ∧ x3 = _x1169 ∧ x4 = _x1170 ∧ x5 = _x1171 ∧ x6 = _x1172 ∧ _x1169 = _x1170 ∧ 0 = _x1168 ∧ _x1169 + 4 ≤ _x1162 ∧ _x1169 + 6 ≤ _x1161 ∧ 4 ≤ _x1167 − 1 ∧ 2 ≤ _x1162 − 1 ∧ 4 ≤ _x1161 − 1 ∧ _x1167 ≤ _x1161
f4661_0_sublistOddDistinctParts_InvokeMethod	97	f4854_0_sublistOddDistinctParts_EQ:	x1 = _x1173 ∧ x2 = _x1174 ∧ x3 = _x1175 ∧ x4 = _x1176 ∧ x5 = _x1177 ∧ x6 = _x1178 ∧ x1 = _x1179 ∧ x2 = _x1180 ∧ x3 = _x1181 ∧ x4 = _x1182 ∧ x5 = _x1183 ∧ x6 = _x1184 ∧ 0 = _x1180 ∧ _x1182 + 4 ≤ _x1174 ∧ _x1181 + 2 ≤ _x1174 ∧ _x1182 + 6 ≤ _x1173 ∧ _x1181 + 4 ≤ _x1173 ∧ 4 ≤ _x1179 − 1 ∧ 2 ≤ _x1174 − 1 ∧ 4 ≤ _x1173 − 1 ∧ _x1179 ≤ _x1173
f4854_0_sublistOddDistinctParts_EQ	98	f4740_0_sublistOddDistinctParts_NULL:	x1 = _x1185 ∧ x2 = _x1186 ∧ x3 = _x1187 ∧ x4 = _x1188 ∧ x5 = _x1189 ∧ x6 = _x1190 ∧ x1 = _x1191 ∧ x2 = _x1192 ∧ x3 = _x1193 ∧ x4 = _x1194 ∧ x5 = _x1195 ∧ x6 = _x1196 ∧ _x1187 = _x1193 ∧ 0 = _x1186 ∧ _x1188 + 6 ≤ _x1185 ∧ _x1187 + 4 ≤ _x1185 ∧ −1 ≤ _x1192 − 1 ∧ 4 ≤ _x1191 − 1 ∧ 4 ≤ _x1185 − 1 ∧ _x1192 + 2 ≤ _x1185 ∧ _x1191 ≤ _x1185
f4854_0_sublistOddDistinctParts_EQ	99	f4661_0_sublistOddDistinctParts_InvokeMethod:	x1 = _x1197 ∧ x2 = _x1198 ∧ x3 = _x1199 ∧ x4 = _x1200 ∧ x5 = _x1201 ∧ x6 = _x1202 ∧ x1 = _x1203 ∧ x2 = _x1204 ∧ x3 = _x1205 ∧ x4 = _x1206 ∧ x5 = _x1207 ∧ x6 = _x1208 ∧ 1 = _x1198 ∧ _x1200 + 6 ≤ _x1197 ∧ _x1199 + 4 ≤ _x1197 ∧ −1 ≤ _x1204 − 1 ∧ 0 ≤ _x1203 − 1 ∧ 4 ≤ _x1197 − 1 ∧ _x1204 + 4 ≤ _x1197 ∧ _x1203 + 2 ≤ _x1197
f4661_0_sublistOddDistinctParts_InvokeMethod	100	f4661_0_sublistOddDistinctParts_InvokeMethod':	x1 = _x1209 ∧ x2 = _x1210 ∧ x3 = _x1211 ∧ x4 = _x1212 ∧ x5 = _x1213 ∧ x6 = _x1214 ∧ x1 = _x1215 ∧ x2 = _x1216 ∧ x3 = _x1217 ∧ x4 = _x1218 ∧ x5 = _x1219 ∧ x6 = _x1220 ∧ _x1221 + 2 ≤ _x1209 ∧ _x1221 ≤ _x1210 ∧ 2 ≤ _x1209 − 1 ∧ 0 ≤ _x1210 − 1 ∧ 0 ≤ _x1221 − 1 ∧ _x1222 + 4 ≤ _x1209 ∧ _x1222 + 2 ≤ _x1210 ∧ _x1209 = _x1215 ∧ _x1210 = _x1216
f4661_0_sublistOddDistinctParts_InvokeMethod'	101	f4689_0_oddDistinctParts_NE:	x1 = _x1223 ∧ x2 = _x1224 ∧ x3 = _x1225 ∧ x4 = _x1226 ∧ x5 = _x1227 ∧ x6 = _x1228 ∧ x1 = _x1229 ∧ x2 = _x1230 ∧ x3 = _x1231 ∧ x4 = _x1232 ∧ x5 = _x1233 ∧ x6 = _x1234 ∧ _x1229 + 2 ≤ _x1223 ∧ _x1229 ≤ _x1224 ∧ 2 ≤ _x1223 − 1 ∧ 0 ≤ _x1224 − 1 ∧ 0 ≤ _x1229 − 1 ∧ _x1231 + 4 ≤ _x1223 ∧ _x1231 + 2 ≤ _x1224 ∧ _x1231 − 2⋅_x1235 ≤ 1 ∧ 0 ≤ _x1231 − 2⋅_x1235 ∧ _x1231 − 2⋅_x1235 = _x1230
f4689_0_oddDistinctParts_NE	102	f4689_0_oddDistinctParts_NE':	x1 = _x1236 ∧ x2 = _x1237 ∧ x3 = _x1238 ∧ x4 = _x1239 ∧ x5 = _x1240 ∧ x6 = _x1241 ∧ x1 = _x1242 ∧ x2 = _x1243 ∧ x3 = _x1244 ∧ x4 = _x1245 ∧ x5 = _x1246 ∧ x6 = _x1247 ∧ _x1237 ≤ −1 ∧ _x1238 ≤ _x1248 − 1 ∧ _x1249 + 2 ≤ _x1236 ∧ 2 ≤ _x1236 − 1 ∧ 0 ≤ _x1249 − 1 ∧ _x1238 + 2 ≤ _x1236 ∧ _x1248 + 4 ≤ _x1236 ∧ _x1236 = _x1242 ∧ _x1237 = _x1243 ∧ _x1238 = _x1244
f4689_0_oddDistinctParts_NE	103	f4689_0_oddDistinctParts_NE':	x1 = _x1250 ∧ x2 = _x1251 ∧ x3 = _x1252 ∧ x4 = _x1253 ∧ x5 = _x1254 ∧ x6 = _x1255 ∧ x1 = _x1256 ∧ x2 = _x1257 ∧ x3 = _x1258 ∧ x4 = _x1259 ∧ x5 = _x1260 ∧ x6 = _x1261 ∧ 0 ≤ _x1251 − 1 ∧ _x1252 ≤ _x1262 − 1 ∧ _x1263 + 2 ≤ _x1250 ∧ 2 ≤ _x1250 − 1 ∧ 0 ≤ _x1263 − 1 ∧ _x1252 + 2 ≤ _x1250 ∧ _x1262 + 4 ≤ _x1250 ∧ _x1250 = _x1256 ∧ _x1251 = _x1257 ∧ _x1252 = _x1258
f4689_0_oddDistinctParts_NE	104	f4689_0_oddDistinctParts_NE':	x1 = _x1264 ∧ x2 = _x1265 ∧ x3 = _x1266 ∧ x4 = _x1267 ∧ x5 = _x1268 ∧ x6 = _x1269 ∧ x1 = _x1270 ∧ x2 = _x1271 ∧ x3 = _x1272 ∧ x4 = _x1273 ∧ x5 = _x1274 ∧ x6 = _x1275 ∧ _x1265 ≤ −1 ∧ _x1276 ≤ _x1266 − 1 ∧ _x1277 + 2 ≤ _x1264 ∧ 2 ≤ _x1264 − 1 ∧ 0 ≤ _x1277 − 1 ∧ _x1266 + 2 ≤ _x1264 ∧ _x1276 + 4 ≤ _x1264 ∧ _x1264 = _x1270 ∧ _x1265 = _x1271 ∧ _x1266 = _x1272
f4689_0_oddDistinctParts_NE	105	f4689_0_oddDistinctParts_NE':	x1 = _x1278 ∧ x2 = _x1279 ∧ x3 = _x1280 ∧ x4 = _x1281 ∧ x5 = _x1282 ∧ x6 = _x1283 ∧ x1 = _x1284 ∧ x2 = _x1285 ∧ x3 = _x1286 ∧ x4 = _x1287 ∧ x5 = _x1288 ∧ x6 = _x1289 ∧ 0 ≤ _x1279 − 1 ∧ _x1290 ≤ _x1280 − 1 ∧ _x1291 + 2 ≤ _x1278 ∧ 2 ≤ _x1278 − 1 ∧ 0 ≤ _x1291 − 1 ∧ _x1280 + 2 ≤ _x1278 ∧ _x1290 + 4 ≤ _x1278 ∧ _x1278 = _x1284 ∧ _x1279 = _x1285 ∧ _x1280 = _x1286
f4689_0_oddDistinctParts_NE'	106	f4689_0_oddDistinctParts_NE:	x1 = _x1292 ∧ x2 = _x1293 ∧ x3 = _x1294 ∧ x4 = _x1295 ∧ x5 = _x1296 ∧ x6 = _x1297 ∧ x1 = _x1298 ∧ x2 = _x1299 ∧ x3 = _x1300 ∧ x4 = _x1301 ∧ x5 = _x1302 ∧ x6 = _x1303 ∧ _x1293 ≤ −1 ∧ _x1294 ≤ _x1300 − 1 ∧ _x1298 + 2 ≤ _x1292 ∧ 2 ≤ _x1292 − 1 ∧ 0 ≤ _x1298 − 1 ∧ _x1294 + 2 ≤ _x1292 ∧ _x1300 + 4 ≤ _x1292 ∧ _x1300 − 2⋅_x1304 ≤ 1 ∧ 0 ≤ _x1300 − 2⋅_x1304 ∧ _x1300 − 2⋅_x1304 = _x1299
f4689_0_oddDistinctParts_NE'	107	f4689_0_oddDistinctParts_NE:	x1 = _x1305 ∧ x2 = _x1306 ∧ x3 = _x1307 ∧ x4 = _x1308 ∧ x5 = _x1309 ∧ x6 = _x1310 ∧ x1 = _x1311 ∧ x2 = _x1312 ∧ x3 = _x1313 ∧ x4 = _x1314 ∧ x5 = _x1315 ∧ x6 = _x1316 ∧ 0 ≤ _x1306 − 1 ∧ _x1307 ≤ _x1313 − 1 ∧ _x1311 + 2 ≤ _x1305 ∧ 2 ≤ _x1305 − 1 ∧ 0 ≤ _x1311 − 1 ∧ _x1307 + 2 ≤ _x1305 ∧ _x1313 + 4 ≤ _x1305 ∧ _x1313 − 2⋅_x1317 ≤ 1 ∧ 0 ≤ _x1313 − 2⋅_x1317 ∧ _x1313 − 2⋅_x1317 = _x1312
f4689_0_oddDistinctParts_NE'	108	f4689_0_oddDistinctParts_NE:	x1 = _x1318 ∧ x2 = _x1319 ∧ x3 = _x1320 ∧ x4 = _x1321 ∧ x5 = _x1322 ∧ x6 = _x1323 ∧ x1 = _x1324 ∧ x2 = _x1325 ∧ x3 = _x1326 ∧ x4 = _x1327 ∧ x5 = _x1328 ∧ x6 = _x1329 ∧ _x1319 ≤ −1 ∧ _x1326 ≤ _x1320 − 1 ∧ _x1324 + 2 ≤ _x1318 ∧ 2 ≤ _x1318 − 1 ∧ 0 ≤ _x1324 − 1 ∧ _x1320 + 2 ≤ _x1318 ∧ _x1326 + 4 ≤ _x1318 ∧ _x1326 − 2⋅_x1330 ≤ 1 ∧ 0 ≤ _x1326 − 2⋅_x1330 ∧ _x1326 − 2⋅_x1330 = _x1325
f4689_0_oddDistinctParts_NE'	109	f4689_0_oddDistinctParts_NE:	x1 = _x1331 ∧ x2 = _x1332 ∧ x3 = _x1333 ∧ x4 = _x1334 ∧ x5 = _x1335 ∧ x6 = _x1336 ∧ x1 = _x1337 ∧ x2 = _x1338 ∧ x3 = _x1339 ∧ x4 = _x1340 ∧ x5 = _x1341 ∧ x6 = _x1342 ∧ 0 ≤ _x1332 − 1 ∧ _x1339 ≤ _x1333 − 1 ∧ _x1337 + 2 ≤ _x1331 ∧ 2 ≤ _x1331 − 1 ∧ 0 ≤ _x1337 − 1 ∧ _x1333 + 2 ≤ _x1331 ∧ _x1339 + 4 ≤ _x1331 ∧ _x1339 − 2⋅_x1343 ≤ 1 ∧ 0 ≤ _x1339 − 2⋅_x1343 ∧ _x1339 − 2⋅_x1343 = _x1338
f4689_0_oddDistinctParts_NE	110	f4841_0_oddDistinctParts_EQ:	x1 = _x1344 ∧ x2 = _x1345 ∧ x3 = _x1346 ∧ x4 = _x1347 ∧ x5 = _x1348 ∧ x6 = _x1349 ∧ x1 = _x1350 ∧ x2 = _x1351 ∧ x3 = _x1352 ∧ x4 = _x1353 ∧ x5 = _x1354 ∧ x6 = _x1355 ∧ _x1345 ≤ −1 ∧ _x1346 ≤ _x1356 − 1 ∧ _x1350 ≤ _x1344 ∧ 5 ≤ _x1344 − 1 ∧ 5 ≤ _x1350 − 1 ∧ _x1346 + 2 ≤ _x1344 ∧ 1 = _x1351
f4689_0_oddDistinctParts_NE	111	f4841_0_oddDistinctParts_EQ:	x1 = _x1357 ∧ x2 = _x1358 ∧ x3 = _x1359 ∧ x4 = _x1360 ∧ x5 = _x1361 ∧ x6 = _x1362 ∧ x1 = _x1363 ∧ x2 = _x1364 ∧ x3 = _x1365 ∧ x4 = _x1366 ∧ x5 = _x1367 ∧ x6 = _x1368 ∧ 0 ≤ _x1358 − 1 ∧ _x1359 ≤ _x1369 − 1 ∧ _x1363 ≤ _x1357 ∧ 5 ≤ _x1357 − 1 ∧ 5 ≤ _x1363 − 1 ∧ _x1359 + 2 ≤ _x1357 ∧ 1 = _x1364
f4689_0_oddDistinctParts_NE	112	f4841_0_oddDistinctParts_EQ:	x1 = _x1370 ∧ x2 = _x1371 ∧ x3 = _x1372 ∧ x4 = _x1373 ∧ x5 = _x1374 ∧ x6 = _x1375 ∧ x1 = _x1376 ∧ x2 = _x1377 ∧ x3 = _x1378 ∧ x4 = _x1379 ∧ x5 = _x1380 ∧ x6 = _x1381 ∧ _x1371 ≤ −1 ∧ _x1382 ≤ _x1372 − 1 ∧ _x1376 ≤ _x1370 ∧ 5 ≤ _x1370 − 1 ∧ 5 ≤ _x1376 − 1 ∧ _x1372 + 2 ≤ _x1370 ∧ 1 = _x1377
f4689_0_oddDistinctParts_NE	113	f4841_0_oddDistinctParts_EQ:	x1 = _x1383 ∧ x2 = _x1384 ∧ x3 = _x1385 ∧ x4 = _x1386 ∧ x5 = _x1387 ∧ x6 = _x1388 ∧ x1 = _x1389 ∧ x2 = _x1390 ∧ x3 = _x1391 ∧ x4 = _x1392 ∧ x5 = _x1393 ∧ x6 = _x1394 ∧ 0 ≤ _x1384 − 1 ∧ _x1395 ≤ _x1385 − 1 ∧ _x1389 ≤ _x1383 ∧ 5 ≤ _x1383 − 1 ∧ 5 ≤ _x1389 − 1 ∧ _x1385 + 2 ≤ _x1383 ∧ 1 = _x1390
f4689_0_oddDistinctParts_NE	114	f4841_0_oddDistinctParts_EQ:	x1 = _x1396 ∧ x2 = _x1397 ∧ x3 = _x1398 ∧ x4 = _x1399 ∧ x5 = _x1400 ∧ x6 = _x1401 ∧ x1 = _x1402 ∧ x2 = _x1403 ∧ x3 = _x1404 ∧ x4 = _x1405 ∧ x5 = _x1406 ∧ x6 = _x1407 ∧ _x1397 ≤ −1 ∧ _x1398 ≤ _x1408 − 1 ∧ _x1402 ≤ _x1396 ∧ 6 ≤ _x1396 − 1 ∧ 6 ≤ _x1402 − 1 ∧ _x1398 + 2 ≤ _x1396 ∧ 0 = _x1403
f4689_0_oddDistinctParts_NE	115	f4841_0_oddDistinctParts_EQ:	x1 = _x1409 ∧ x2 = _x1410 ∧ x3 = _x1411 ∧ x4 = _x1412 ∧ x5 = _x1413 ∧ x6 = _x1414 ∧ x1 = _x1415 ∧ x2 = _x1416 ∧ x3 = _x1417 ∧ x4 = _x1418 ∧ x5 = _x1419 ∧ x6 = _x1420 ∧ 0 ≤ _x1410 − 1 ∧ _x1411 ≤ _x1421 − 1 ∧ _x1415 ≤ _x1409 ∧ 6 ≤ _x1409 − 1 ∧ 6 ≤ _x1415 − 1 ∧ _x1411 + 2 ≤ _x1409 ∧ 0 = _x1416
f4689_0_oddDistinctParts_NE	116	f4841_0_oddDistinctParts_EQ:	x1 = _x1422 ∧ x2 = _x1423 ∧ x3 = _x1424 ∧ x4 = _x1425 ∧ x5 = _x1426 ∧ x6 = _x1427 ∧ x1 = _x1428 ∧ x2 = _x1429 ∧ x3 = _x1430 ∧ x4 = _x1431 ∧ x5 = _x1432 ∧ x6 = _x1433 ∧ _x1423 ≤ −1 ∧ _x1434 ≤ _x1424 − 1 ∧ _x1428 ≤ _x1422 ∧ 6 ≤ _x1422 − 1 ∧ 6 ≤ _x1428 − 1 ∧ _x1424 + 2 ≤ _x1422 ∧ 0 = _x1429
f4689_0_oddDistinctParts_NE	117	f4841_0_oddDistinctParts_EQ:	x1 = _x1435 ∧ x2 = _x1436 ∧ x3 = _x1437 ∧ x4 = _x1438 ∧ x5 = _x1439 ∧ x6 = _x1440 ∧ x1 = _x1441 ∧ x2 = _x1442 ∧ x3 = _x1443 ∧ x4 = _x1444 ∧ x5 = _x1445 ∧ x6 = _x1446 ∧ 0 ≤ _x1436 − 1 ∧ _x1447 ≤ _x1437 − 1 ∧ _x1441 ≤ _x1435 ∧ 6 ≤ _x1435 − 1 ∧ 6 ≤ _x1441 − 1 ∧ _x1437 + 2 ≤ _x1435 ∧ 0 = _x1442
f4689_0_oddDistinctParts_NE	118	f4841_0_oddDistinctParts_EQ:	x1 = _x1448 ∧ x2 = _x1449 ∧ x3 = _x1450 ∧ x4 = _x1451 ∧ x5 = _x1452 ∧ x6 = _x1453 ∧ x1 = _x1454 ∧ x2 = _x1455 ∧ x3 = _x1456 ∧ x4 = _x1457 ∧ x5 = _x1458 ∧ x6 = _x1459 ∧ _x1449 ≤ −1 ∧ _x1450 ≤ _x1460 − 1 ∧ _x1454 ≤ _x1448 ∧ 6 ≤ _x1448 − 1 ∧ 6 ≤ _x1454 − 1 ∧ _x1450 + 2 ≤ _x1448 ∧ 1 = _x1455
f4689_0_oddDistinctParts_NE	119	f4841_0_oddDistinctParts_EQ:	x1 = _x1461 ∧ x2 = _x1462 ∧ x3 = _x1463 ∧ x4 = _x1464 ∧ x5 = _x1465 ∧ x6 = _x1466 ∧ x1 = _x1467 ∧ x2 = _x1468 ∧ x3 = _x1469 ∧ x4 = _x1470 ∧ x5 = _x1471 ∧ x6 = _x1472 ∧ 0 ≤ _x1462 − 1 ∧ _x1463 ≤ _x1473 − 1 ∧ _x1467 ≤ _x1461 ∧ 6 ≤ _x1461 − 1 ∧ 6 ≤ _x1467 − 1 ∧ _x1463 + 2 ≤ _x1461 ∧ 1 = _x1468
f4689_0_oddDistinctParts_NE	120	f4841_0_oddDistinctParts_EQ:	x1 = _x1474 ∧ x2 = _x1475 ∧ x3 = _x1476 ∧ x4 = _x1477 ∧ x5 = _x1478 ∧ x6 = _x1479 ∧ x1 = _x1480 ∧ x2 = _x1481 ∧ x3 = _x1482 ∧ x4 = _x1483 ∧ x5 = _x1484 ∧ x6 = _x1485 ∧ _x1475 ≤ −1 ∧ _x1486 ≤ _x1476 − 1 ∧ _x1480 ≤ _x1474 ∧ 6 ≤ _x1474 − 1 ∧ 6 ≤ _x1480 − 1 ∧ _x1476 + 2 ≤ _x1474 ∧ 1 = _x1481
f4689_0_oddDistinctParts_NE	121	f4841_0_oddDistinctParts_EQ:	x1 = _x1487 ∧ x2 = _x1488 ∧ x3 = _x1489 ∧ x4 = _x1490 ∧ x5 = _x1491 ∧ x6 = _x1492 ∧ x1 = _x1493 ∧ x2 = _x1494 ∧ x3 = _x1495 ∧ x4 = _x1496 ∧ x5 = _x1497 ∧ x6 = _x1498 ∧ 0 ≤ _x1488 − 1 ∧ _x1499 ≤ _x1489 − 1 ∧ _x1493 ≤ _x1487 ∧ 6 ≤ _x1487 − 1 ∧ 6 ≤ _x1493 − 1 ∧ _x1489 + 2 ≤ _x1487 ∧ 1 = _x1494
f4689_0_oddDistinctParts_NE	122	f4841_0_oddDistinctParts_EQ:	x1 = _x1500 ∧ x2 = _x1501 ∧ x3 = _x1502 ∧ x4 = _x1503 ∧ x5 = _x1504 ∧ x6 = _x1505 ∧ x1 = _x1506 ∧ x2 = _x1507 ∧ x3 = _x1508 ∧ x4 = _x1509 ∧ x5 = _x1510 ∧ x6 = _x1511 ∧ _x1501 ≤ −1 ∧ _x1502 ≤ _x1512 − 1 ∧ _x1506 ≤ _x1500 ∧ 4 ≤ _x1500 − 1 ∧ 4 ≤ _x1506 − 1 ∧ _x1502 + 2 ≤ _x1500 ∧ 0 = _x1507
f4689_0_oddDistinctParts_NE	123	f4841_0_oddDistinctParts_EQ:	x1 = _x1513 ∧ x2 = _x1514 ∧ x3 = _x1515 ∧ x4 = _x1516 ∧ x5 = _x1517 ∧ x6 = _x1518 ∧ x1 = _x1519 ∧ x2 = _x1520 ∧ x3 = _x1521 ∧ x4 = _x1522 ∧ x5 = _x1523 ∧ x6 = _x1524 ∧ 0 ≤ _x1514 − 1 ∧ _x1515 ≤ _x1525 − 1 ∧ _x1519 ≤ _x1513 ∧ 4 ≤ _x1513 − 1 ∧ 4 ≤ _x1519 − 1 ∧ _x1515 + 2 ≤ _x1513 ∧ 0 = _x1520
f4689_0_oddDistinctParts_NE	124	f4841_0_oddDistinctParts_EQ:	x1 = _x1526 ∧ x2 = _x1527 ∧ x3 = _x1528 ∧ x4 = _x1529 ∧ x5 = _x1530 ∧ x6 = _x1531 ∧ x1 = _x1532 ∧ x2 = _x1533 ∧ x3 = _x1534 ∧ x4 = _x1535 ∧ x5 = _x1536 ∧ x6 = _x1537 ∧ _x1527 ≤ −1 ∧ _x1538 ≤ _x1528 − 1 ∧ _x1532 ≤ _x1526 ∧ 4 ≤ _x1526 − 1 ∧ 4 ≤ _x1532 − 1 ∧ _x1528 + 2 ≤ _x1526 ∧ 0 = _x1533
f4689_0_oddDistinctParts_NE	125	f4841_0_oddDistinctParts_EQ:	x1 = _x1539 ∧ x2 = _x1540 ∧ x3 = _x1541 ∧ x4 = _x1542 ∧ x5 = _x1543 ∧ x6 = _x1544 ∧ x1 = _x1545 ∧ x2 = _x1546 ∧ x3 = _x1547 ∧ x4 = _x1548 ∧ x5 = _x1549 ∧ x6 = _x1550 ∧ 0 ≤ _x1540 − 1 ∧ _x1551 ≤ _x1541 − 1 ∧ _x1545 ≤ _x1539 ∧ 4 ≤ _x1539 − 1 ∧ 4 ≤ _x1545 − 1 ∧ _x1541 + 2 ≤ _x1539 ∧ 0 = _x1546
__init	126	f1_0_main_Load:	x1 = _x1552 ∧ x2 = _x1553 ∧ x3 = _x1554 ∧ x4 = _x1555 ∧ x5 = _x1556 ∧ x6 = _x1557 ∧ x1 = _x1558 ∧ x2 = _x1559 ∧ x3 = _x1560 ∧ x4 = _x1561 ∧ x5 = _x1562 ∧ x6 = _x1563 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

f4135_0_sublistAutoDual_InvokeMethod	f4135_0_sublistAutoDual_InvokeMethod	f4135_0_sublistAutoDual_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f2375_0_generation_InvokeMethod	f2375_0_generation_InvokeMethod	f2375_0_generation_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f1674_0_number_greater_LT	f1674_0_number_greater_LT	f1674_0_number_greater_LT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f2374_0_generation_InvokeMethod	f2374_0_generation_InvokeMethod	f2374_0_generation_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
__init	__init	__init:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f4661_0_sublistOddDistinctParts_InvokeMethod'	f4661_0_sublistOddDistinctParts_InvokeMethod'	f4661_0_sublistOddDistinctParts_InvokeMethod':	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f3187_0_generation_InvokeMethod	f3187_0_generation_InvokeMethod	f3187_0_generation_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f2470_0_sublistAutoDual_InvokeMethod	f2470_0_sublistAutoDual_InvokeMethod	f2470_0_sublistAutoDual_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f741_0_generation_Return	f741_0_generation_Return	f741_0_generation_Return:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f3192_0_dual_LE	f3192_0_dual_LE	f3192_0_dual_LE:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f789_0_generation_Return	f789_0_generation_Return	f789_0_generation_Return:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f4740_0_sublistOddDistinctParts_NULL	f4740_0_sublistOddDistinctParts_NULL	f4740_0_sublistOddDistinctParts_NULL:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f2503_0_isEqual_NONNULL	f2503_0_isEqual_NONNULL	f2503_0_isEqual_NONNULL:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f2372_0_main_InvokeMethod	f2372_0_main_InvokeMethod	f2372_0_main_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f654_0_generation_NE	f654_0_generation_NE	f654_0_generation_NE:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f609_0_generation_NONNULL	f609_0_generation_NONNULL	f609_0_generation_NONNULL:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f2504_0_union_NONNULL	f2504_0_union_NONNULL	f2504_0_union_NONNULL:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f3931_0_sublistAutoDual_InvokeMethod	f3931_0_sublistAutoDual_InvokeMethod	f3931_0_sublistAutoDual_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f2440_0_insert_NONNULL	f2440_0_insert_NONNULL	f2440_0_insert_NONNULL:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f4854_0_sublistOddDistinctParts_EQ	f4854_0_sublistOddDistinctParts_EQ	f4854_0_sublistOddDistinctParts_EQ:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f2373_0_generation_InvokeMethod	f2373_0_generation_InvokeMethod	f2373_0_generation_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f4689_0_oddDistinctParts_NE	f4689_0_oddDistinctParts_NE	f4689_0_oddDistinctParts_NE:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f4119_0_main_InvokeMethod	f4119_0_main_InvokeMethod	f4119_0_main_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f740_0_generation_Return	f740_0_generation_Return	f740_0_generation_Return:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f742_0_generation_Return	f742_0_generation_Return	f742_0_generation_Return:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f4661_0_sublistOddDistinctParts_InvokeMethod	f4661_0_sublistOddDistinctParts_InvokeMethod	f4661_0_sublistOddDistinctParts_InvokeMethod:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f283_0_partitionOf_GT	f283_0_partitionOf_GT	f283_0_partitionOf_GT:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f1_0_main_Load	f1_0_main_Load	f1_0_main_Load:	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6
f4689_0_oddDistinctParts_NE'	f4689_0_oddDistinctParts_NE'	f4689_0_oddDistinctParts_NE':	x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6

and for every transition t, a duplicate t is considered.

2 SCC Decomposition

We consider subproblems for each of the 9 SCC(s) of the program graph.

2.1 SCC Subproblem 1/9

Here we consider the SCC { f283_0_partitionOf_GT }.

2.1.1 Transition Removal

We remove transition 3 using the following ranking functions, which are bounded by 0.

f283_0_partitionOf_GT:

− x3 + x4

2.1.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.2 SCC Subproblem 2/9

Here we consider the SCC { f2470_0_sublistAutoDual_InvokeMethod, f3192_0_dual_LE }.

2.2.1 Transition Removal

We remove transition 37 using the following ranking functions, which are bounded by 0.

f2470_0_sublistAutoDual_InvokeMethod:	x1 + 1
f3192_0_dual_LE:	x1

2.2.2 Transition Removal

We remove transitions 36, 48, 49, 50 using the following ranking functions, which are bounded by 0.

f2470_0_sublistAutoDual_InvokeMethod:	x1
f3192_0_dual_LE:	−1 + x1 + x4 − x5

2.2.3 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.3 SCC Subproblem 3/9

Here we consider the SCC { f1674_0_number_greater_LT }.

2.3.1 Transition Removal

We remove transitions 77, 78 using the following ranking functions, which are bounded by 0.

f1674_0_number_greater_LT:

−3 + x1

2.3.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.4 SCC Subproblem 4/9

Here we consider the SCC { f2503_0_isEqual_NONNULL }.

2.4.1 Transition Removal

We remove transition 79 using the following ranking functions, which are bounded by 0.

f2503_0_isEqual_NONNULL:

2.4.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.5 SCC Subproblem 5/9

Here we consider the SCC { f4661_0_sublistOddDistinctParts_InvokeMethod, f4854_0_sublistOddDistinctParts_EQ, f4740_0_sublistOddDistinctParts_NULL }.

2.5.1 Transition Removal

We remove transitions 90, 91, 98, 93, 92, 99, 97, 96, 95, 94 using the following ranking functions, which are bounded by 0.

f4661_0_sublistOddDistinctParts_InvokeMethod:	1 + 2⋅x1
f4740_0_sublistOddDistinctParts_NULL:	−1 + 2⋅x1
f4854_0_sublistOddDistinctParts_EQ:	2⋅x1

2.5.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.6 SCC Subproblem 6/9

Here we consider the SCC { f4689_0_oddDistinctParts_NE, f4689_0_oddDistinctParts_NE' }.

2.6.1 Transition Removal

We remove transitions 102, 106, 103, 107, 104, 108, 105, 109 using the following ranking functions, which are bounded by 0.

f4689_0_oddDistinctParts_NE:	1 + x1
f4689_0_oddDistinctParts_NE':	x1

2.6.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.7 SCC Subproblem 7/9

Here we consider the SCC { f3187_0_generation_InvokeMethod, f654_0_generation_NE, f609_0_generation_NONNULL, f2373_0_generation_InvokeMethod }.

2.7.1 Transition Removal

We remove transitions 10, 13, 11, 27, 16, 31, 30, 29, 17, 15, 14 using the following ranking functions, which are bounded by 0.

f609_0_generation_NONNULL:	3⋅x3 − 1
f654_0_generation_NE:	3⋅x2 − 2
f2373_0_generation_InvokeMethod:	3⋅x2 − 2
f3187_0_generation_InvokeMethod:	3⋅x3

2.7.2 Transition Removal

We remove transition 12 using the following ranking functions, which are bounded by 0.

f609_0_generation_NONNULL:

2.7.3 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.8 SCC Subproblem 8/9

Here we consider the SCC { f2504_0_union_NONNULL }.

2.8.1 Transition Removal

We remove transition 34 using the following ranking functions, which are bounded by 0.

f2504_0_union_NONNULL:

2.8.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.9 SCC Subproblem 9/9

Here we consider the SCC { f2440_0_insert_NONNULL }.

2.9.1 Transition Removal

We remove transition 33 using the following ranking functions, which are bounded by 0.

f2440_0_insert_NONNULL:

2.9.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

Tool configuration

AProVE

version: AProVE Commit ID: unknown
strategy: Statistics for single proof: 100.00 % (31 real / 0 unknown / 0 assumptions / 31 total proof steps)