# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 11
• 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − x7 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ 4 − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ arg3P ≤ 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 1 2 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ −2 + arg1P − arg2 ≤ 0 ∧ 5 − arg1 + arg2P ≤ 0 ∧ 3 + arg2P − arg2 ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 4 − arg2 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg6 ≤ 0 ∧ 3 − arg2 + arg4 ≤ 0 ∧ 3 − arg2 + arg6 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg3 ≤ 0 ∧ − arg3P ≤ 0 ∧ arg3P ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 3 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg3 − arg6 ≤ 0 ∧ − arg3 ≤ 0 ∧ − arg6 ≤ 0 ∧ −1 + arg1P − arg1 ≤ 0 ∧ 5 − arg1 + arg2P ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg1 + arg3 ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg5 ≤ 0 ∧ 1 − arg3P + arg3 ≤ 0 ∧ −1 + arg3P − arg3 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 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 3 4 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3 + arg6 ≤ 0 ∧ 6 − arg1 + arg2P ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 2 − arg1 + arg3 ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg5 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 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 3 5 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg3 − arg6 ≤ 0 ∧ − arg3 ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg1 + arg3 ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg5 ≤ 0 ∧ 1 − arg3P + arg3 ≤ 0 ∧ −1 + arg3P − arg3 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 4 6 5: 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 ∧ arg1P − arg1 ≤ 0 ∧ − arg5 ≤ 0 ∧ 5 − arg1 + arg2P ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 2 − arg2 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg1 + arg3 ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg6 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 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 4 7 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 ∧ arg1P − arg1 ≤ 0 ∧ 4 − arg1 + arg2P ≤ 0 ∧ 2 + arg2P − arg2 ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 3 − arg2 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg1 + arg3 ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg6 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 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 5 8 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3 + arg6 ≤ 0 ∧ 6 − arg1 + arg2P ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 2 − arg1 + arg3 ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg5 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 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 5 9 5: 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 ∧ − arg6 ≤ 0 ∧ 1 + arg3 − arg6 ≤ 0 ∧ −1 + arg1P − arg1 ≤ 0 ∧ 5 − arg1 + arg2P ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg1 + arg3 ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg5 ≤ 0 ∧ 1 − arg3P + arg3 ≤ 0 ∧ −1 + arg3P − arg3 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 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 5 10 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 + arg3 − arg6 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg1 + arg3 ≤ 0 ∧ 5 − arg1 + arg4 ≤ 0 ∧ 5 − arg1 + arg5 ≤ 0 ∧ 1 − arg3P + arg3 ≤ 0 ∧ −1 + arg3P − arg3 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg4P + arg4P ≤ 0 ∧ arg4P − arg4P ≤ 0 ∧ − arg4 + arg4 ≤ 0 ∧ arg4 − arg4 ≤ 0 0 11 6: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg2P ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ −14 + arg1P − arg1 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 15 − arg1P ≤ 0 ∧ arg2 − arg3P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ −1 + arg4P ≤ 0 ∧ − arg5P ≤ 0 ∧ arg5P ≤ 0 ∧ 16 − arg6P ≤ 0 ∧ −16 + arg6P ≤ 0 ∧ 12 − arg7P ≤ 0 ∧ −12 + 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 6 12 6: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 2 − arg3 + arg4 ≤ 0 ∧ − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x98 ≤ 0 ∧ − x99 ≤ 0 ∧ 2 − arg6 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 3 − arg1 + arg5 ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ −1 − arg2P + arg2 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ 2 − arg4P + arg4 ≤ 0 ∧ −2 + arg4P − arg4 ≤ 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 6 13 7: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 − arg3 + arg4 ≤ 0 ∧ 2 − arg6 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x111 ≤ 0 ∧ − x112 ≤ 0 ∧ 1 + arg3P − arg6 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg5 ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ arg3 − arg5P ≤ 0 ∧ − arg3 + arg5P ≤ 0 ∧ 2 + arg4 − arg6P ≤ 0 ∧ −2 − arg4 + arg6P ≤ 0 ∧ arg5 − arg7P ≤ 0 ∧ − arg5 + arg7P ≤ 0 ∧ arg6 − arg8P ≤ 0 ∧ − arg6 + arg8P ≤ 0 ∧ arg7 − arg9P ≤ 0 ∧ − arg7 + arg9P ≤ 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 7 14 8: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 − arg8 ≤ 0 ∧ arg3P − arg4 ≤ 0 ∧ 2 − arg4 + arg8P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg8P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ 4 + arg10P − arg4 ≤ 0 ∧ − arg2P + arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 0 ∧ − arg5P + arg7 ≤ 0 ∧ arg5P − arg7 ≤ 0 ∧ − arg6P + arg8 ≤ 0 ∧ arg6P − arg8 ≤ 0 ∧ − arg7P + arg9 ≤ 0 ∧ arg7P − arg9 ≤ 0 ∧ arg2 − arg9P ≤ 0 ∧ − arg2 + arg9P ≤ 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 7 15 8: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 − arg8 ≤ 0 ∧ arg3P − arg4 ≤ 0 ∧ 2 − arg4 + arg8P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg8P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ 4 + arg10P − arg4 ≤ 0 ∧ − arg2P + arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ −1 + arg4P ≤ 0 ∧ − arg5P + arg7 ≤ 0 ∧ arg5P − arg7 ≤ 0 ∧ − arg6P + arg8 ≤ 0 ∧ arg6P − arg8 ≤ 0 ∧ − arg7P + arg9 ≤ 0 ∧ arg7P − arg9 ≤ 0 ∧ arg2 − arg9P ≤ 0 ∧ − arg2 + arg9P ≤ 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 7 16 7: 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 ∧ 1 − arg2 + x150 ≤ 0 ∧ 1 + arg4P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 7 17 7: 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 ∧ 1 + arg2 − x285 ≤ 0 ∧ 1 + arg4P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 7 18 7: 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 ∧ 2 − arg8 ≤ 0 ∧ 2 + arg4P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 7 19 7: 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 ∧ 2 − arg8 ≤ 0 ∧ 2 + arg4P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 8 20 7: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 − arg3 + arg4P ≤ 0 ∧ arg4P − arg8 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − arg8 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg5 ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 2 − arg3 + arg9 ≤ 0 ∧ 4 + arg10 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ arg4 ≤ 0 ∧ − arg2P + arg9 ≤ 0 ∧ arg2P − arg9 ≤ 0 ∧ arg2 − arg3P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ arg5 − arg7P ≤ 0 ∧ − arg5 + arg7P ≤ 0 ∧ arg6 − arg8P ≤ 0 ∧ − arg6 + arg8P ≤ 0 ∧ arg7 − arg9P ≤ 0 ∧ − arg7 + arg9P ≤ 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 7 21 9: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg3 − arg8 ≤ 0 ∧ 2 − arg8 ≤ 0 ∧ − arg7 + arg9 ≤ 0 ∧ −2⋅arg8 ≤ 0 ∧ −1073741823 + arg8 ≤ 0 ∧ −1 + arg1P − arg1 ≤ 0 ∧ 3 − arg1 + arg2P ≤ 0 ∧ −1 + arg2P − arg4 ≤ 0 ∧ 3 − arg1 + arg3P ≤ 0 ∧ −1 + arg3P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 0 ∧ 1 − arg5P + arg7 ≤ 0 ∧ −1 + arg5P − arg7 ≤ 0 ∧ − arg6P + arg9 ≤ 0 ∧ arg6P − arg9 ≤ 0 ∧ − arg7P + 2⋅arg8 ≤ 0 ∧ arg7P − 2⋅arg8 ≤ 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 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 0 7 22 9: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg3 − arg8 ≤ 0 ∧ 1073741825 − arg8 ≤ 0 ∧ −2⋅arg8 ≤ 0 ∧ − arg7 + arg9 ≤ 0 ∧ −1 + arg1P − arg1 ≤ 0 ∧ 3 − arg1 + arg2P ≤ 0 ∧ −1 + arg2P − arg4 ≤ 0 ∧ 3 − arg1 + arg3P ≤ 0 ∧ −1 + arg3P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 0 ∧ 1 − arg5P + arg7 ≤ 0 ∧ −1 + arg5P − arg7 ≤ 0 ∧ − arg6P + arg9 ≤ 0 ∧ arg6P − arg9 ≤ 0 ∧ − arg7P + 2⋅arg8 ≤ 0 ∧ arg7P − 2⋅arg8 ≤ 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 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 0 9 23 10: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg7 ≤ 0 ∧ 1 + arg4 − arg8 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 3 − arg1 + arg2P ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ 3 − arg1 + arg6P ≤ 0 ∧ − arg2 + arg6P ≤ 0 ∧ − arg3 + arg6P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ − arg4P ≤ 0 ∧ 1 − arg5P ≤ 0 ∧ 1 − arg6P ≤ 0 ∧ 3 − arg1 + arg5 ≤ 0 ∧ 3 − arg1 + arg6 ≤ 0 ∧ − arg3P + arg4 ≤ 0 ∧ arg3P − arg4 ≤ 0 ∧ arg5 − arg8P ≤ 0 ∧ − arg5 + arg8P ≤ 0 ∧ arg6 − arg9P ≤ 0 ∧ − arg6 + arg9P ≤ 0 ∧ − arg10P + arg8 ≤ 0 ∧ arg10P − arg8 ≤ 0 ∧ − arg13P + arg7 ≤ 0 ∧ arg13P − 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 10 24 10: 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 − arg13 + arg7 ≤ 0 ∧ 1 − arg13 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 3 − arg1 + arg2P ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg2P − arg4 ≤ 0 ∧ 2 + arg2P − arg5 ≤ 0 ∧ arg2P − arg6 ≤ 0 ∧ 1 + arg4P − arg4 ≤ 0 ∧ 3 + arg4P − arg5 ≤ 0 ∧ − arg4 + arg5P ≤ 0 ∧ 2 + arg5P − arg5 ≤ 0 ∧ 3 − arg1 + arg6P ≤ 0 ∧ − arg2 + arg6P ≤ 0 ∧ − arg4 + arg6P ≤ 0 ∧ 2 − arg5 + arg6P ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ 1 − arg6 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ − arg4P ≤ 0 ∧ 1 − arg5P ≤ 0 ∧ 1 − arg6P ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ 2 + arg11P − arg4 ≤ 0 ∧ 2 + arg12P − arg4 ≤ 0 ∧ 4 + arg11P − arg5 ≤ 0 ∧ 4 + arg12P − arg5 ≤ 0 ∧ 2 + arg11 − arg5 ≤ 0 ∧ 2 + arg12 − arg5 ≤ 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 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 9 25 9: 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 ∧ − arg8 ≤ 0 ∧ 1 + arg4 − arg8 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 3 − arg1 + arg2P ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ 3 − arg1 + arg3P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 3 − arg1 + arg5 ≤ 0 ∧ 3 − arg1 + arg6 ≤ 0 ∧ 1 − arg4P + arg4 ≤ 0 ∧ −1 + arg4P − arg4 ≤ 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 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 10 26 9: 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg10 ≤ 0 ∧ 1 − arg13 + arg7 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 3 − arg1 + arg2P ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ −1 + arg2P − arg4 ≤ 0 ∧ 1 + arg2P − arg5 ≤ 0 ∧ arg2P − arg6 ≤ 0 ∧ 3 − arg1 + arg3P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ −1 + arg3P − arg4 ≤ 0 ∧ 1 + arg3P − arg5 ≤ 0 ∧ arg3P − arg6 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg4 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ 1 − arg6 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ 3 − arg1 + arg9 ≤ 0 ∧ 2 + arg11 − arg5 ≤ 0 ∧ 2 + arg12 − arg5 ≤ 0 ∧ 1 + arg3 − arg4P ≤ 0 ∧ −1 − arg3 + arg4P ≤ 0 ∧ − arg5P + arg8 ≤ 0 ∧ arg5P − arg8 ≤ 0 ∧ − arg6P + arg9 ≤ 0 ∧ arg6P − arg9 ≤ 0 ∧ arg13 − arg7P ≤ 0 ∧ − arg13 + arg7P ≤ 0 ∧ arg10 − arg8P ≤ 0 ∧ − arg10 + arg8P ≤ 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 11 27 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 ≤ 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 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − arg10P + arg10 ≤ 0 ∧ arg10P − arg10 ≤ 0 ∧ − arg11P + arg11 ≤ 0 ∧ arg11P − arg11 ≤ 0 ∧ − arg12P + arg12 ≤ 0 ∧ arg12P − arg12 ≤ 0 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0

## Proof

The following invariants are asserted.

 0: TRUE 1: 6 − arg1P ≤ 0 ∧ 4 − arg2P ≤ 0 ∧ arg3P ≤ 0 ∧ − arg3P ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 4 − arg2 ≤ 0 ∧ arg3 ≤ 0 ∧ − arg3 ≤ 0 ∧ − x7 ≤ 0 3: 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ − x7 ≤ 0 4: 6 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ − x7 ≤ 0 5: 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ − x7 ≤ 0 6: 1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0 7: 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x111 ≤ 0 ∧ − x112 ≤ 0 8: 4 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg8P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ − arg8 ≤ 0 ∧ − x111 ≤ 0 ∧ − x112 ≤ 0 9: 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ − x111 ≤ 0 ∧ − x112 ≤ 0 10: 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ − arg4P ≤ 0 ∧ 1 − arg5P ≤ 0 ∧ 1 − arg6P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg4 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ 1 − arg6 ≤ 0 ∧ − x111 ≤ 0 ∧ − x112 ≤ 0 11: TRUE

The invariants are proved as follows.

### IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) TRUE 1 (1) 6 − arg1P ≤ 0 ∧ 4 − arg2P ≤ 0 ∧ arg3P ≤ 0 ∧ − arg3P ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 4 − arg2 ≤ 0 ∧ arg3 ≤ 0 ∧ − arg3 ≤ 0 ∧ − x7 ≤ 0 3 (3) 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ − x7 ≤ 0 4 (4) 6 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ − x7 ≤ 0 5 (5) 6 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 6 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ − x7 ≤ 0 6 (6) 1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0 7 (7) 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x111 ≤ 0 ∧ − x112 ≤ 0 8 (8) 4 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg8P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ − arg8 ≤ 0 ∧ − x111 ≤ 0 ∧ − x112 ≤ 0 9 (9) 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ − x111 ≤ 0 ∧ − x112 ≤ 0 10 (10) 4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ − arg4P ≤ 0 ∧ 1 − arg5P ≤ 0 ∧ 1 − arg6P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg4 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ 1 − arg6 ≤ 0 ∧ − x111 ≤ 0 ∧ − x112 ≤ 0 11 (11) TRUE
• initial node: 11
• cover edges:
• transition edges:  0 0 1 0 11 6 1 2 3 3 3 3 3 4 4 3 5 4 4 6 5 4 7 4 5 8 4 5 9 5 5 10 4 6 12 6 6 13 7 7 14 8 7 15 8 7 16 7 7 17 7 7 18 7 7 19 7 7 21 9 7 22 9 8 20 7 9 23 10 9 25 9 10 24 10 10 26 9 11 27 0

### 2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 3 28 3: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 4 35 4: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 5 42 5: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 6 49 6: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 7 56 7: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 9 63 9: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 10 70 10: − x99 + x99 ≤ 0 ∧ x99 − x99 ≤ 0 ∧ − x98 + x98 ≤ 0 ∧ x98 − x98 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x150 + x150 ≤ 0 ∧ x150 − x150 ≤ 0 ∧ − x112 + x112 ≤ 0 ∧ x112 − x112 ≤ 0 ∧ − x111 + x111 ≤ 0 ∧ x111 − x111 ≤ 0 ∧ − arg9P + arg9P ≤ 0 ∧ arg9P − arg9P ≤ 0 ∧ − arg9 + arg9 ≤ 0 ∧ arg9 − arg9 ≤ 0 ∧ − arg8P + arg8P ≤ 0 ∧ arg8P − arg8P ≤ 0 ∧ − arg8 + arg8 ≤ 0 ∧ arg8 − arg8 ≤ 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 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
and for every transition t, a duplicate t is considered.

### 3 Transition Removal

We remove transitions 0, 2, 4, 5, 11, 13, 21, 22, 27 using the following ranking functions, which are bounded by −33.

 11: 0 0: 0 1: 0 3: 0 4: 0 5: 0 6: 0 7: 0 8: 0 9: 0 10: 0 11: −9 0: −10 1: −11 3: −12 3_var_snapshot: −12 3*: −12 4: −15 5: −15 4_var_snapshot: −15 4*: −15 5_var_snapshot: −15 5*: −15 6: −20 6_var_snapshot: −20 6*: −20 7: −23 8: −23 7_var_snapshot: −23 7*: −23 9: −26 10: −26 9_var_snapshot: −26 9*: −26 10_var_snapshot: −26 10*: −26

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

3* 31 3: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

3 29 3_var_snapshot: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

4* 38 4: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

4 36 4_var_snapshot: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

5* 45 5: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

5 43 5_var_snapshot: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

6* 52 6: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

6 50 6_var_snapshot: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

7* 59 7: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

7 57 7_var_snapshot: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

9* 66 9: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

9 64 9_var_snapshot: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

10* 73 10: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

10 71 10_var_snapshot: x99 + x99 ≤ 0x99x99 ≤ 0x98 + x98 ≤ 0x98x98 ≤ 0x7 + x7 ≤ 0x7x7 ≤ 0x285 + x285 ≤ 0x285x285 ≤ 0x150 + x150 ≤ 0x150x150 ≤ 0x112 + x112 ≤ 0x112x112 ≤ 0x111 + x111 ≤ 0x111x111 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg13P + arg13P ≤ 0arg13Parg13P ≤ 0arg13 + arg13 ≤ 0arg13arg13 ≤ 0arg12P + arg12P ≤ 0arg12Parg12P ≤ 0arg12 + arg12 ≤ 0arg12arg12 ≤ 0arg11P + arg11P ≤ 0arg11Parg11P ≤ 0arg11 + arg11 ≤ 0arg11arg11 ≤ 0arg10P + arg10P ≤ 0arg10Parg10P ≤ 0arg10 + arg10 ≤ 0arg10arg10 ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

### 18 SCC Decomposition

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

### 18.1 SCC Subproblem 1/5

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

### 18.1.1 Transition Removal

We remove transitions 9, 10 using the following ranking functions, which are bounded by 4.

 4: −5⋅arg3 + 5⋅arg5 5: −5⋅arg3 + 5⋅arg6 4_var_snapshot: −5⋅arg3 + 5⋅arg5 4*: −5⋅arg3 + 5⋅arg5 5_var_snapshot: −5⋅arg3 + 5⋅arg6 5*: −5⋅arg3 + 5⋅arg6

### 18.1.2 Transition Removal

We remove transitions 36, 38, 43, 45, 6, 7, 8 using the following ranking functions, which are bounded by −1.

 4: 1 + 3⋅arg2 5: 1 + 3⋅arg2 4_var_snapshot: 3⋅arg2 4*: 2 + 3⋅arg2 5_var_snapshot: 3⋅arg2 5*: 2 + 3⋅arg2

### 18.1.3 Splitting Cut-Point Transitions

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

### 18.1.3.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 35.

### 18.1.3.1.1 Splitting Cut-Point Transitions

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

### 18.1.3.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 42.

### 18.1.3.2.1 Splitting Cut-Point Transitions

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

### 18.2 SCC Subproblem 2/5

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

### 18.2.1 Transition Removal

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

 3: −4⋅arg3 + 4⋅arg6 3_var_snapshot: −4⋅arg3 + 4⋅arg6 3*: 1 − 4⋅arg3 + 4⋅arg6

### 18.2.2 Transition Removal

We remove transitions 29, 31 using the following ranking functions, which are bounded by −2.

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

### 18.2.3 Splitting Cut-Point Transitions

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

### 18.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 28.

### 18.2.3.1.1 Splitting Cut-Point Transitions

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

### 18.3 SCC Subproblem 3/5

Here we consider the SCC { 9, 10, 9_var_snapshot, 9*, 10_var_snapshot, 10* }.

### 18.3.1 Transition Removal

We remove transitions 23, 25 using the following ranking functions, which are bounded by 7.

 9: 2 − 7⋅arg4 + 7⋅arg8 10: 7⋅arg10 − 7⋅arg3 9_var_snapshot: 1 − 7⋅arg4 + 7⋅arg8 9*: 3 − 7⋅arg4 + 7⋅arg8 10_var_snapshot: 7⋅arg10 − 7⋅arg3 10*: 7⋅arg10 − 7⋅arg3

### 18.3.2 Transition Removal

We remove transitions 64, 71, 73, 24, 26 using the following ranking functions, which are bounded by −3.

 9: −2 10: 1 + 3⋅arg4 9_var_snapshot: −3⋅arg2P 9*: −1 10_var_snapshot: 3⋅arg4 10*: 2 + 3⋅arg4

### 18.3.3 Transition Removal

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

 9: 0 10: 0 9_var_snapshot: 0 9*: arg2P 10_var_snapshot: 0 10*: 0

### 18.3.4 Splitting Cut-Point Transitions

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

### 18.3.4.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 63.

### 18.3.4.1.1 Splitting Cut-Point Transitions

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

### 18.3.4.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 70.

### 18.3.4.2.1 Splitting Cut-Point Transitions

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

### 18.4 SCC Subproblem 4/5

Here we consider the SCC { 7, 8, 7_var_snapshot, 7* }.

### 18.4.1 Transition Removal

We remove transitions 57, 59, 14, 15, 16, 17, 18, 19, 20 using the following ranking functions, which are bounded by −3.

 7: −1 + 3⋅arg4 8: 1 + 3⋅arg8 7_var_snapshot: −2 + 3⋅arg4 7*: 3⋅arg4

### 18.4.2 Splitting Cut-Point Transitions

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

### 18.4.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 56.

### 18.4.2.1.1 Splitting Cut-Point Transitions

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

### 18.5 SCC Subproblem 5/5

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

### 18.5.1 Transition Removal

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

 6: 1 + arg2 + arg3 − arg4 6_var_snapshot: arg2 + arg3 − arg4 6*: 2 + arg2 + arg3 − arg4

### 18.5.2 Transition Removal

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

 6: 0 6_var_snapshot: − arg1 6*: arg1P

### 18.5.3 Transition Removal

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

 6: 0 6_var_snapshot: −1 6*: 0

### 18.5.4 Splitting Cut-Point Transitions

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

### 18.5.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 49.

### 18.5.4.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0