LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 5

Transitions: (pre-variables and post-variables)

0	0	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x4 ≤ 0 ∧ 2 − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ 1 + arg2P − x5 ≤ 0 ∧ − x5 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0
0	1	1:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x10 ≤ 0 ∧ 2 − arg2 ≤ 0 ∧ arg2P ≤ 0 ∧ − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0
1	2	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg2P ≤ 0 ∧ arg2P ≤ 0 ∧ arg2 − arg3P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ arg2 − arg4P ≤ 0 ∧ − arg2 + arg4P ≤ 0 ∧ − arg5P ≤ 0 ∧ arg5P ≤ 0 ∧ arg2 − arg6P ≤ 0 ∧ − arg2 + arg6P ≤ 0 ∧ arg2 − arg7P ≤ 0 ∧ − arg2 + arg7P ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
2	3	3:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 + x99 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg6 + x100 ≤ 0 ∧ − arg6 ≤ 0 ∧ 1 − x101 + x102 ≤ 0 ∧ − x100 ≤ 0 ∧ 1 + x100 − x102 ≤ 0 ∧ − x101 ≤ 0 ∧ 1 + x100 − x103 ≤ 0 ∧ 1 + x100 − x99 ≤ 0 ∧ − arg1 + x104 ≤ 0 ∧ arg1 − 2⋅x105 ≤ 0 ∧ − arg1 + 2⋅x105 ≤ 0 ∧ arg3 − arg4 ≤ 0 ∧ − arg3 + arg4 ≤ 0 ∧ arg6 − arg7 ≤ 0 ∧ − arg6 + arg7 ≤ 0 ∧ arg3 − arg4P ≤ 0 ∧ − arg3 + arg4P ≤ 0 ∧ arg6 − arg7P ≤ 0 ∧ − arg6 + arg7P ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
3	4	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 + arg4P ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg6 + x117 ≤ 0 ∧ − arg6 ≤ 0 ∧ 1 + arg5P − x118 ≤ 0 ∧ − x117 ≤ 0 ∧ 1 − arg5P + x117 ≤ 0 ∧ − x118 ≤ 0 ∧ 1 + x117 − x119 ≤ 0 ∧ 1 − arg4P + x117 ≤ 0 ∧ arg1 − 2⋅x120 ≤ 0 ∧ − arg1 + 2⋅x120 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg1 + 2⋅x120 ≤ 0 ∧ −1 + arg1 − 2⋅x120 ≤ 0 ∧ −1 − 2⋅arg1P + arg1 ≤ 0 ∧ 2⋅arg1P − arg1 ≤ 0 ∧ arg3 − arg4 ≤ 0 ∧ − arg3 + arg4 ≤ 0 ∧ arg6 − arg7 ≤ 0 ∧ − arg6 + arg7 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ −1 + arg2P ≤ 0 ∧ − arg6P ≤ 0 ∧ arg6P ≤ 0 ∧ arg5P − arg7P ≤ 0 ∧ − arg5P + arg7P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0
2	5	3:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ − arg7 ≤ 0 ∧ 1 − arg7 + x128 ≤ 0 ∧ 1 − arg4 + x129 ≤ 0 ∧ 1 − arg5 + x128 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ −1 + arg1 − 2⋅x130 ≤ 0 ∧ 1 − arg1 + 2⋅x130 ≤ 0 ∧ − x131 ≤ 0 ∧ 1 + x129 − x131 ≤ 0 ∧ − arg1 + x132 ≤ 0 ∧ − x129 ≤ 0 ∧ − x129 + x133 ≤ 0 ∧ 1 − x128 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
3	6	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ − arg7 ≤ 0 ∧ 1 + arg5P − arg7 ≤ 0 ∧ 1 − arg4 + x145 ≤ 0 ∧ 1 + arg5P − arg5 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ −1 + arg1 − 2⋅x146 ≤ 0 ∧ 1 − arg1 + 2⋅x146 ≤ 0 ∧ − x147 ≤ 0 ∧ 1 + x145 − x147 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − x145 ≤ 0 ∧ 1 − arg5P ≤ 0 ∧ arg4P − x145 ≤ 0 ∧ − arg1 + 2⋅x146 ≤ 0 ∧ −1 + arg1 − 2⋅x146 ≤ 0 ∧ −1 − 2⋅arg1P + arg1 ≤ 0 ∧ 2⋅arg1P − arg1 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ −1 + arg2P ≤ 0 ∧ − arg6P ≤ 0 ∧ arg6P ≤ 0 ∧ arg5P − arg7P ≤ 0 ∧ − arg5P + arg7P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0
2	7	3:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 + x156 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg6 + x156 ≤ 0 ∧ − arg6 ≤ 0 ∧ 1 − x157 + x158 ≤ 0 ∧ − x157 ≤ 0 ∧ −1 + arg1 − 2⋅x159 ≤ 0 ∧ 1 − arg1 + 2⋅x159 ≤ 0 ∧ 1 − x156 ≤ 0 ∧ − arg1 + x160 ≤ 0 ∧ arg3 − arg4 ≤ 0 ∧ − arg3 + arg4 ≤ 0 ∧ arg6 − arg7 ≤ 0 ∧ − arg6 + arg7 ≤ 0 ∧ arg3 − arg4P ≤ 0 ∧ − arg3 + arg4P ≤ 0 ∧ arg6 − arg7P ≤ 0 ∧ − arg6 + arg7P ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
3	8	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg3P − arg3 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 + arg3P − arg6 ≤ 0 ∧ − arg6 ≤ 0 ∧ 1 − x170 + x172 ≤ 0 ∧ − x170 ≤ 0 ∧ −1 + arg1 − 2⋅x173 ≤ 0 ∧ 1 − arg1 + 2⋅x173 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ − arg1 + 2⋅x173 ≤ 0 ∧ −1 + arg1 − 2⋅x173 ≤ 0 ∧ −1 − 2⋅arg1P + arg1 ≤ 0 ∧ 2⋅arg1P − arg1 ≤ 0 ∧ arg3 − arg4 ≤ 0 ∧ − arg3 + arg4 ≤ 0 ∧ arg6 − arg7 ≤ 0 ∧ − arg6 + arg7 ≤ 0 ∧ − arg2P ≤ 0 ∧ arg2P ≤ 0 ∧ arg3P − arg4P ≤ 0 ∧ − arg3P + arg4P ≤ 0 ∧ − arg5P ≤ 0 ∧ arg5P ≤ 0 ∧ arg3P − arg6P ≤ 0 ∧ − arg3P + arg6P ≤ 0 ∧ arg3P − arg7P ≤ 0 ∧ − arg3P + arg7P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0
2	9	3:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ − arg6 ≤ 0 ∧ 1 − arg2 + arg6 ≤ 0 ∧ 1 + arg6 − x181 ≤ 0 ∧ 1 − arg3 + arg6 ≤ 0 ∧ 1 + arg6 − x182 ≤ 0 ∧ − arg7 ≤ 0 ∧ 1 − arg7 + x183 ≤ 0 ∧ 1 + x183 − x184 ≤ 0 ∧ 1 − arg4 + x185 ≤ 0 ∧ − x183 ≤ 0 ∧ 1 + x183 − x186 ≤ 0 ∧ 1 − arg5 + x187 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 + x183 − x185 ≤ 0 ∧ 1 + x183 − x187 ≤ 0 ∧ − arg1 + x188 ≤ 0 ∧ arg1 − 2⋅x189 ≤ 0 ∧ − arg1 + 2⋅x189 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
3	10	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ − arg6 ≤ 0 ∧ 1 − arg2 + arg6 ≤ 0 ∧ 1 + arg6 − x202 ≤ 0 ∧ 1 − arg3 + arg6 ≤ 0 ∧ 1 + arg6 − x203 ≤ 0 ∧ − arg7 ≤ 0 ∧ 1 − arg7 + x204 ≤ 0 ∧ 1 − arg7P + x204 ≤ 0 ∧ 1 + arg4P − arg4 ≤ 0 ∧ − x204 ≤ 0 ∧ 1 + x204 − x205 ≤ 0 ∧ 1 + arg5P − arg5 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg4P + x204 ≤ 0 ∧ 1 − arg5P + x204 ≤ 0 ∧ arg1 − 2⋅x206 ≤ 0 ∧ − arg1 + 2⋅x206 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg1 + 2⋅x206 ≤ 0 ∧ −1 + arg1 − 2⋅x206 ≤ 0 ∧ −1 − 2⋅arg1P + arg1 ≤ 0 ∧ 2⋅arg1P − arg1 ≤ 0 ∧ arg2 − arg6P ≤ 0 ∧ − arg2 + arg6P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0
2	11	3:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ − arg7 ≤ 0 ∧ 1 − arg7 + x214 ≤ 0 ∧ 1 − arg4 + x215 ≤ 0 ∧ 1 − arg5 + x216 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ −1 + arg1 − 2⋅x217 ≤ 0 ∧ 1 − arg1 + 2⋅x217 ≤ 0 ∧ − arg3 ≤ 0 ∧ − arg3 + x218 ≤ 0 ∧ − x215 + x219 ≤ 0 ∧ − x215 ≤ 0 ∧ − x216 + x220 ≤ 0 ∧ 1 − arg6 ≤ 0 ∧ − arg1 + x221 ≤ 0 ∧ − x216 ≤ 0 ∧ 1 − x214 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
3	12	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ − arg7 ≤ 0 ∧ 1 + arg7P − arg7 ≤ 0 ∧ 1 − arg4 + x235 ≤ 0 ∧ 1 − arg5 + x236 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ −1 + arg1 − 2⋅x237 ≤ 0 ∧ 1 − arg1 + 2⋅x237 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ arg4P − x235 ≤ 0 ∧ − x235 ≤ 0 ∧ arg5P − x236 ≤ 0 ∧ 1 − arg6 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 1 − arg7P ≤ 0 ∧ − x236 ≤ 0 ∧ − arg1 + 2⋅x237 ≤ 0 ∧ −1 + arg1 − 2⋅x237 ≤ 0 ∧ −1 − 2⋅arg1P + arg1 ≤ 0 ∧ 2⋅arg1P − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0
2	13	3:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 + x245 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg6 + x246 ≤ 0 ∧ − arg6 ≤ 0 ∧ 1 + x247 − x248 ≤ 0 ∧ − x248 ≤ 0 ∧ −1 + arg1 − 2⋅x249 ≤ 0 ∧ 1 − arg1 + 2⋅x249 ≤ 0 ∧ − arg1 + x250 ≤ 0 ∧ − x245 ≤ 0 ∧ − x245 + x251 ≤ 0 ∧ 1 − x246 ≤ 0 ∧ arg3 − arg4 ≤ 0 ∧ − arg3 + arg4 ≤ 0 ∧ arg6 − arg7 ≤ 0 ∧ − arg6 + arg7 ≤ 0 ∧ arg3 − arg4P ≤ 0 ∧ − arg3 + arg4P ≤ 0 ∧ arg6 − arg7P ≤ 0 ∧ − arg6 + arg7P ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
3	14	2:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg3 + x266 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg6 + arg7P ≤ 0 ∧ − arg6 ≤ 0 ∧ 1 + x267 − x268 ≤ 0 ∧ − x268 ≤ 0 ∧ −1 + arg1 − 2⋅x269 ≤ 0 ∧ 1 − arg1 + 2⋅x269 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − x266 ≤ 0 ∧ 1 − arg7P ≤ 0 ∧ arg4P − x266 ≤ 0 ∧ − arg1 + 2⋅x269 ≤ 0 ∧ −1 + arg1 − 2⋅x269 ≤ 0 ∧ −1 − 2⋅arg1P + arg1 ≤ 0 ∧ 2⋅arg1P − arg1 ≤ 0 ∧ arg3 − arg4 ≤ 0 ∧ − arg3 + arg4 ≤ 0 ∧ arg6 − arg7 ≤ 0 ∧ − arg6 + arg7 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0
0	15	4:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x96 ≤ 0 ∧ 2 − arg2 ≤ 0 ∧ − x95 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ −1 − arg1P + x95 ≤ 0 ∧ 1 + arg1P − x95 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0
4	16	4:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ −1 − arg1P + arg1 ≤ 0 ∧ 1 + arg1P − arg1 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0
5	17	0:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0

Proof

1 Invariant Updates

The following invariants are asserted.

0:	TRUE
1:	− arg1P ≤ 0 ∧ − arg1 ≤ 0
2:	TRUE
3:	TRUE
4:	− x96 ≤ 0 ∧ − x95 ≤ 0
5:	TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(0)	TRUE
1	(1)	− arg1P ≤ 0 ∧ − arg1 ≤ 0
2	(2)	TRUE
3	(3)	TRUE
4	(4)	− x96 ≤ 0 ∧ − x95 ≤ 0
5	(5)	TRUE

initial node: 5
cover edges:
transition edges:

0 0 1

0 1 1

0 15 4

1 2 2

2 3 3

2 5 3

2 7 3

2 9 3

2 11 3

2 13 3

3 4 2

3 6 2

3 8 2

3 10 2

3 12 2

3 14 2

4 16 4

5 17 0

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

2	18	2:	− x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
4	25	4:	− x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

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

3 Transition Removal

We remove transitions 0, 1, 2, 15, 17 using the following ranking functions, which are bounded by −17.

5:	0
0:	0
1:	0
2:	0
3:	0
4:	0
5:	−6
0:	−7
1:	−8
2:	−9
3:	−9
2_var_snapshot:	−9
2*:	−9
4:	−12
4_var_snapshot:	−12
4*:	−12

4 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2* 21 2: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

5 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

2 19 2_var_snapshot: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

6 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

4* 28 4: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

7 Location Addition

The following skip-transition is inserted and corresponding redirections w.r.t. the old location are performed.

4 26 4_var_snapshot: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x96 + x96 ≤ 0 ∧ x96 − x96 ≤ 0 ∧ − x95 + x95 ≤ 0 ∧ x95 − x95 ≤ 0 ∧ − x5 + x5 ≤ 0 ∧ x5 − x5 ≤ 0 ∧ − x4 + x4 ≤ 0 ∧ x4 − x4 ≤ 0 ∧ − x269 + x269 ≤ 0 ∧ x269 − x269 ≤ 0 ∧ − x268 + x268 ≤ 0 ∧ x268 − x268 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x266 + x266 ≤ 0 ∧ x266 − x266 ≤ 0 ∧ − x251 + x251 ≤ 0 ∧ x251 − x251 ≤ 0 ∧ − x250 + x250 ≤ 0 ∧ x250 − x250 ≤ 0 ∧ − x249 + x249 ≤ 0 ∧ x249 − x249 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x246 + x246 ≤ 0 ∧ x246 − x246 ≤ 0 ∧ − x245 + x245 ≤ 0 ∧ x245 − x245 ≤ 0 ∧ − x237 + x237 ≤ 0 ∧ x237 − x237 ≤ 0 ∧ − x236 + x236 ≤ 0 ∧ x236 − x236 ≤ 0 ∧ − x235 + x235 ≤ 0 ∧ x235 − x235 ≤ 0 ∧ − x221 + x221 ≤ 0 ∧ x221 − x221 ≤ 0 ∧ − x220 + x220 ≤ 0 ∧ x220 − x220 ≤ 0 ∧ − x219 + x219 ≤ 0 ∧ x219 − x219 ≤ 0 ∧ − x218 + x218 ≤ 0 ∧ x218 − x218 ≤ 0 ∧ − x217 + x217 ≤ 0 ∧ x217 − x217 ≤ 0 ∧ − x216 + x216 ≤ 0 ∧ x216 − x216 ≤ 0 ∧ − x215 + x215 ≤ 0 ∧ x215 − x215 ≤ 0 ∧ − x214 + x214 ≤ 0 ∧ x214 − x214 ≤ 0 ∧ − x206 + x206 ≤ 0 ∧ x206 − x206 ≤ 0 ∧ − x205 + x205 ≤ 0 ∧ x205 − x205 ≤ 0 ∧ − x204 + x204 ≤ 0 ∧ x204 − x204 ≤ 0 ∧ − x203 + x203 ≤ 0 ∧ x203 − x203 ≤ 0 ∧ − x202 + x202 ≤ 0 ∧ x202 − x202 ≤ 0 ∧ − x189 + x189 ≤ 0 ∧ x189 − x189 ≤ 0 ∧ − x188 + x188 ≤ 0 ∧ x188 − x188 ≤ 0 ∧ − x187 + x187 ≤ 0 ∧ x187 − x187 ≤ 0 ∧ − x186 + x186 ≤ 0 ∧ x186 − x186 ≤ 0 ∧ − x185 + x185 ≤ 0 ∧ x185 − x185 ≤ 0 ∧ − x184 + x184 ≤ 0 ∧ x184 − x184 ≤ 0 ∧ − x183 + x183 ≤ 0 ∧ x183 − x183 ≤ 0 ∧ − x182 + x182 ≤ 0 ∧ x182 − x182 ≤ 0 ∧ − x181 + x181 ≤ 0 ∧ x181 − x181 ≤ 0 ∧ − x173 + x173 ≤ 0 ∧ x173 − x173 ≤ 0 ∧ − x172 + x172 ≤ 0 ∧ x172 − x172 ≤ 0 ∧ − x170 + x170 ≤ 0 ∧ x170 − x170 ≤ 0 ∧ − x160 + x160 ≤ 0 ∧ x160 − x160 ≤ 0 ∧ − x159 + x159 ≤ 0 ∧ x159 − x159 ≤ 0 ∧ − x158 + x158 ≤ 0 ∧ x158 − x158 ≤ 0 ∧ − x157 + x157 ≤ 0 ∧ x157 − x157 ≤ 0 ∧ − x156 + x156 ≤ 0 ∧ x156 − x156 ≤ 0 ∧ − x147 + x147 ≤ 0 ∧ x147 − x147 ≤ 0 ∧ − x146 + x146 ≤ 0 ∧ x146 − x146 ≤ 0 ∧ − x145 + x145 ≤ 0 ∧ x145 − x145 ≤ 0 ∧ − x133 + x133 ≤ 0 ∧ x133 − x133 ≤ 0 ∧ − x132 + x132 ≤ 0 ∧ x132 − x132 ≤ 0 ∧ − x131 + x131 ≤ 0 ∧ x131 − x131 ≤ 0 ∧ − x130 + x130 ≤ 0 ∧ x130 − x130 ≤ 0 ∧ − x129 + x129 ≤ 0 ∧ x129 − x129 ≤ 0 ∧ − x128 + x128 ≤ 0 ∧ x128 − x128 ≤ 0 ∧ − x120 + x120 ≤ 0 ∧ x120 − x120 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − x117 + x117 ≤ 0 ∧ x117 − x117 ≤ 0 ∧ − x105 + x105 ≤ 0 ∧ x105 − x105 ≤ 0 ∧ − x104 + x104 ≤ 0 ∧ x104 − x104 ≤ 0 ∧ − x103 + x103 ≤ 0 ∧ x103 − x103 ≤ 0 ∧ − x102 + x102 ≤ 0 ∧ x102 − x102 ≤ 0 ∧ − x101 + x101 ≤ 0 ∧ x101 − x101 ≤ 0 ∧ − x100 + x100 ≤ 0 ∧ x100 − x100 ≤ 0 ∧ − x10 + x10 ≤ 0 ∧ x10 − x10 ≤ 0 ∧ − arg7P + arg7P ≤ 0 ∧ arg7P − arg7P ≤ 0 ∧ − arg7 + arg7 ≤ 0 ∧ arg7 − arg7 ≤ 0 ∧ − arg6P + arg6P ≤ 0 ∧ arg6P − arg6P ≤ 0 ∧ − arg6 + arg6 ≤ 0 ∧ arg6 − arg6 ≤ 0 ∧ − arg5P + arg5P ≤ 0 ∧ arg5P − arg5P ≤ 0 ∧ − arg5 + arg5 ≤ 0 ∧ arg5 − arg5 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

8 SCC Decomposition

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

8.1 SCC Subproblem 1/2

Here we consider the SCC { 2, 3, 2_var_snapshot, 2* }.

8.1.1 Transition Removal

We remove transitions 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14 using the following ranking functions, which are bounded by 3.

2:	2 + 4⋅arg4
3:	4⋅arg4
2_var_snapshot:	1 + 4⋅arg4
2*:	3 + 4⋅arg4

8.1.2 Transition Removal

We remove transition 19 using the following ranking functions, which are bounded by −1.

2:	0
3:	0
2_var_snapshot:	−1
2*:	1

8.1.3 Transition Removal

We remove transition 21 using the following ranking functions, which are bounded by −1.

2:	−1
3:	0
2_var_snapshot:	0
2*:	0

8.1.4 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

8.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 18.

8.1.4.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

8.2 SCC Subproblem 2/2

Here we consider the SCC { 4, 4_var_snapshot, 4* }.

8.2.1 Transition Removal

We remove transition 16 using the following ranking functions, which are bounded by 2.

4:	1 + 3⋅arg1
4_var_snapshot:	3⋅arg1
4*:	2 + 3⋅arg1

8.2.2 Transition Removal

We remove transition 26 using the following ranking functions, which are bounded by −1.

4:	0
4_var_snapshot:	−1
4*:	1

8.2.3 Transition Removal

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

4:	0
4_var_snapshot:	0
4*:	1

8.2.4 Splitting Cut-Point Transitions

We consider 1 subproblems corresponding to sets of cut-point transitions as follows.

8.2.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 25.

8.2.4.1.1 Splitting Cut-Point Transitions

There remain no cut-point transition to consider. Hence the cooperation termination is trivial.

Tool configuration

T2Cert

version: 1.0

0	0 1
0	1 1
0	15 4
1	2 2
2	3 3
2	5 3
2	7 3
2	9 3
2	11 3
2	13 3
3	4 2
3	6 2
3	8 2
3	10 2
3	12 2
3	14 2
4	16 4
5	17 0