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 ∧ − x7 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
0	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 ∧ 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 ∧ 16 − arg5P ≤ 0 ∧ −16 + arg5P ≤ 0 ∧ − arg6P ≤ 0 ∧ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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 ∧ 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 ∧ − x29 ≤ 0 ∧ − x30 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg6 ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 0
1	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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 + x32 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ − x32 ≤ 0 ∧ − x39 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 + x40 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ − arg2P ≤ 0 ∧ 3 − arg1 + arg5 ≤ 0 ∧ 3 − arg1 + 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 ∧ − 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
4	5	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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg2 + arg3P ≤ 0 ∧ 2 + arg1 − arg2 ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
4	6	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 ∧ arg1P − arg2 ≤ 0 ∧ 2 − arg2 + arg5P ≤ 0 ∧ 3 − arg2 ≤ 0 ∧ 3 − arg1P ≤ 0 ∧ − arg5P ≤ 0 ∧ 2 + arg1 − arg2 ≤ 0 ∧ 4 − arg2 + arg6P ≤ 0 ∧ − arg2P ≤ 0 ∧ arg2P ≤ 0 ∧ arg1 − arg4P ≤ 0 ∧ − arg1 + arg4P ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
4	7	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 ∧ arg1P − arg2 ≤ 0 ∧ 2 − arg2 + arg5P ≤ 0 ∧ 3 − arg2 ≤ 0 ∧ 3 − arg1P ≤ 0 ∧ − arg5P ≤ 0 ∧ 2 + arg1 − arg2 ≤ 0 ∧ 4 − arg2 + arg6P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ −1 + arg2P ≤ 0 ∧ arg1 − arg4P ≤ 0 ∧ − arg1 + arg4P ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
4	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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ 1 − arg1 + x64 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg2P ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
4	9	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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ 1 + arg1 − x60 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg2P ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
4	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 ∧ 2 + arg2P − arg2 ≤ 0 ∧ 2 − arg2 ≤ 0 ∧ − arg2P ≤ 0 ∧ 2 + arg1 − arg2 ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
4	11	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 ∧ 2 + arg2P − arg2 ≤ 0 ∧ 3 − arg2 ≤ 0 ∧ − arg2P ≤ 0 ∧ 2 + arg1 − arg2 ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
6	12	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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 − arg1 + arg2P ≤ 0 ∧ arg2P − arg5 ≤ 0 ∧ 3 − arg1 ≤ 0 ∧ − arg5 ≤ 0 ∧ − arg2P ≤ 0 ∧ 2 − arg1 + arg4 ≤ 0 ∧ 4 − arg1 + arg6 ≤ 0 ∧ − arg2 ≤ 0 ∧ arg2 ≤ 0 ∧ − arg1P + arg4 ≤ 0 ∧ arg1P − 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 ∧ − 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
3	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 − arg5 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x90 ≤ 0 ∧ − x91 ≤ 0 ∧ 1 + arg3P − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg6 ≤ 0 ∧ 2 + arg4 − arg5P ≤ 0 ∧ −2 − arg4 + arg5P ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 0 ∧ arg6 − arg7P ≤ 0 ∧ − arg6 + arg7P ≤ 0 ∧ arg7 − arg8P ≤ 0 ∧ − arg7 + 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 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
7	14	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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 − arg6 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ 2 + arg3P − arg4 ≤ 0 ∧ 2 + arg2 − 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 ∧ − 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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 ∧ 2 − arg6 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ arg3P − arg4 ≤ 0 ∧ 2 + arg10P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg10P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ 4 + arg11P − arg4 ≤ 0 ∧ − arg2P + arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 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 ∧ − 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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
7	16	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 ∧ 2 − arg6 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ arg3P − arg4 ≤ 0 ∧ 2 + arg10P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg10P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ 4 + arg11P − arg4 ≤ 0 ∧ − arg2P + arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ −1 + arg4P ≤ 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 ∧ − 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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
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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 1 − arg2 + x138 ≤ 0 ∧ 1 + arg4P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 1 + arg2 − x264 ≤ 0 ∧ 1 + arg4P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 − arg6 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 + arg4P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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	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 ∧ 2 − arg6 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 + arg4P − arg4 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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	21	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 ∧ arg1P − arg1 ≤ 0 ∧ 2 − arg3 + arg4P ≤ 0 ∧ − arg10 + arg4P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − arg10 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 3 − arg1 + arg7 ≤ 0 ∧ 3 − arg1 + arg8 ≤ 0 ∧ 2 − arg3 + arg9 ≤ 0 ∧ 4 + arg11 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ arg4 ≤ 0 ∧ − arg2P + arg9 ≤ 0 ∧ arg2P − arg9 ≤ 0 ∧ arg2 − arg3P ≤ 0 ∧ − arg2 + 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 ∧ − 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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
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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg3 − arg6 ≤ 0 ∧ 2 − arg6 ≤ 0 ∧ − arg7 + arg8 ≤ 0 ∧ −2⋅arg6 ≤ 0 ∧ −1073741823 + arg6 ≤ 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 + arg8 ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 0 ∧ 1 − arg5P + arg7 ≤ 0 ∧ −1 + arg5P − arg7 ≤ 0 ∧ − arg6P + arg8 ≤ 0 ∧ arg6P − arg8 ≤ 0 ∧ 2⋅arg6 − arg7P ≤ 0 ∧ −2⋅arg6 + arg7P ≤ 0 ∧ arg6 − arg8P ≤ 0 ∧ − arg6 + 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
7	23	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 ∧ 1 + arg3 − arg6 ≤ 0 ∧ 1073741825 − arg6 ≤ 0 ∧ −2⋅arg6 ≤ 0 ∧ − arg7 + 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 + arg8 ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 0 ∧ 1 − arg5P + arg7 ≤ 0 ∧ −1 + arg5P − arg7 ≤ 0 ∧ − arg6P + arg8 ≤ 0 ∧ arg6P − arg8 ≤ 0 ∧ 2⋅arg6 − arg7P ≤ 0 ∧ −2⋅arg6 + arg7P ≤ 0 ∧ arg6 − arg8P ≤ 0 ∧ − arg6 + 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
9	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 ∧ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
10	25	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 ∧ 2 + arg11 − arg5 ≤ 0 ∧ 4 + arg11P − arg5 ≤ 0 ∧ 4 + arg12P − 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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	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 ∧ − 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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	27	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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0
11	28	0:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 ∧ − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 0

Proof

1 Invariant Updates

The following invariants are asserted.

0:	TRUE
1:	4 − arg1P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − x7 ≤ 0
3:	1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0
4:	− arg2P ≤ 0 ∧ − arg2 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x39 ≤ 0
5:	1 − arg2P ≤ 0 ∧ 1 − arg2 ≤ 0
6:	3 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg5P ≤ 0 ∧ 3 − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg5 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x39 ≤ 0
7:	4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x90 ≤ 0 ∧ − x91 ≤ 0
8:	4 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg10P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ 2 − arg6 ≤ 0 ∧ − arg10 ≤ 0 ∧ − x90 ≤ 0 ∧ − x91 ≤ 0
9:	4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ − x90 ≤ 0 ∧ − x91 ≤ 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 ∧ − x90 ≤ 0 ∧ − x91 ≤ 0
11:	TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

nodes (location) invariant:

0	(0)	TRUE
1	(1)	4 − arg1P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − x7 ≤ 0
3	(3)	1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0
4	(4)	− arg2P ≤ 0 ∧ − arg2 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x39 ≤ 0
5	(5)	1 − arg2P ≤ 0 ∧ 1 − arg2 ≤ 0
6	(6)	3 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg5P ≤ 0 ∧ 3 − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg5 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x39 ≤ 0
7	(7)	4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x90 ≤ 0 ∧ − x91 ≤ 0
8	(8)	4 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg10P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ 2 − arg6 ≤ 0 ∧ − arg10 ≤ 0 ∧ − x90 ≤ 0 ∧ − x91 ≤ 0
9	(9)	4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ − x90 ≤ 0 ∧ − x91 ≤ 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 ∧ − x90 ≤ 0 ∧ − x91 ≤ 0
11	(11)	TRUE

initial node: 11
cover edges:

transition edges:

0	0 1
0	2 3
1	4 4
3	3 3
3	13 7
4	5 5
4	6 6
4	7 6
4	8 4
4	9 4
4	10 4
4	11 4
6	12 4
7	14 5
7	15 8
7	16 8
7	17 7
7	18 7
7	19 7
7	20 7
7	22 9
7	23 9
8	21 7
9	24 10
9	26 9
10	25 10
10	27 9
11	28 0

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

3	29	3:	− x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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	36	4:	− x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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	43	7:	− x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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	50	9:	− x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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	57	10:	− x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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, 13, 14, 22, 23, 28 using the following ranking functions, which are bounded by −29.

11:	0
0:	0
1:	0
4:	0
6:	0
3:	0
7:	0
8:	0
5:	0
9:	0
10:	0
11:	−9
0:	−10
1:	−11
4:	−12
6:	−12
4_var_snapshot:	−12
4*:	−12
3:	−15
3_var_snapshot:	−15
3*:	−15
7:	−18
8:	−18
7_var_snapshot:	−18
7*:	−18
5:	−21
9:	−22
10:	−22
9_var_snapshot:	−22
9*:	−22
10_var_snapshot:	−22
10*:	−22

4 Location Addition

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

3* 32 3: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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 Location Addition

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

3 30 3_var_snapshot: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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 Location Addition

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

4* 39 4: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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 Location Addition

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

4 37 4_var_snapshot: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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

8 Location Addition

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

7* 46 7: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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 Location Addition

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

7 44 7_var_snapshot: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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 Location Addition

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

9* 53 9: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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

11 Location Addition

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

9 51 9_var_snapshot: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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

12 Location Addition

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

10* 60 10: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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

13 Location Addition

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

10 58 10_var_snapshot: − x91 + x91 ≤ 0 ∧ x91 − x91 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x64 + x64 ≤ 0 ∧ x64 − x64 ≤ 0 ∧ − x60 + x60 ≤ 0 ∧ x60 − x60 ≤ 0 ∧ − x40 + x40 ≤ 0 ∧ x40 − x40 ≤ 0 ∧ − x39 + x39 ≤ 0 ∧ x39 − x39 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x264 + x264 ≤ 0 ∧ x264 − x264 ≤ 0 ∧ − x138 + x138 ≤ 0 ∧ x138 − x138 ≤ 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

14 SCC Decomposition

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

14.1 SCC Subproblem 1/4

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

14.1.1 Transition Removal

We remove transitions 37, 39, 6, 7, 8, 9, 10, 11, 12 using the following ranking functions, which are bounded by −3.

4:	−1 + 3⋅arg2
6:	1 + 3⋅arg5
4_var_snapshot:	−2 + 3⋅arg2
4*:	3⋅arg2

14.1.2 Splitting Cut-Point Transitions

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

14.1.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 36.

14.1.2.1.1 Splitting Cut-Point Transitions

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

14.2 SCC Subproblem 2/4

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

14.2.1 Transition Removal

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

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

14.2.2 Transition Removal

We remove transitions 58, 60, 25, 27 using the following ranking functions, which are bounded by −1.

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

14.2.3 Transition Removal

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

9:	−3⋅arg4 + 3⋅arg8
10:	0
9_var_snapshot:	−1 − 3⋅arg4 + 3⋅arg8
9*:	1 − 3⋅arg4 + 3⋅arg8
10_var_snapshot:	0
10*:	0

14.2.4 Transition Removal

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

9:	0
10:	0
9_var_snapshot:	− arg1P
9*:	arg3P
10_var_snapshot:	0
10*:	0

14.2.5 Transition Removal

We remove transition 53 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

14.2.6 Splitting Cut-Point Transitions

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

14.2.6.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 50.

14.2.6.1.1 Splitting Cut-Point Transitions

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

14.2.6.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 57.

14.2.6.2.1 Splitting Cut-Point Transitions

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

14.3 SCC Subproblem 3/4

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

14.3.1 Transition Removal

We remove transitions 44, 46, 15, 16, 17, 18, 19, 20, 21 using the following ranking functions, which are bounded by −3.

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

14.3.2 Splitting Cut-Point Transitions

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

14.3.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 43.

14.3.2.1.1 Splitting Cut-Point Transitions

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

14.4 SCC Subproblem 4/4

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

14.4.1 Transition Removal

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

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

14.4.2 Transition Removal

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

3:	0
3_var_snapshot:	−1
3*:	arg1

14.4.3 Transition Removal

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

3:	0
3_var_snapshot:	0
3*:	arg1

14.4.4 Splitting Cut-Point Transitions

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

14.4.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 29.

14.4.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