LTS Termination Proof

by T2Cert

Input

Integer Transition System

Initial Location: 12

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 ∧ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ 1 − arg2 + x32 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ − x32 ≤ 0 ∧ − x38 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 3 + arg1P − arg1 ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 3 − arg1 + arg5 ≤ 0 ∧ 3 − arg1 + arg4 ≤ 0 ∧ − arg2P ≤ 0 ∧ arg2P ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − arg3P + arg3P ≤ 0 ∧ arg3P − arg3P ≤ 0 ∧ − arg3 + arg3 ≤ 0 ∧ arg3 − arg3 ≤ 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 ∧ arg1P − arg1 ≤ 0 ∧ 1 + arg2 − arg3 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ − arg3P ≤ 0 ∧ arg3 − arg5P ≤ 0 ∧ − arg3 + arg5P ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
5	6	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 ∧ arg1P − arg1 ≤ 0 ∧ − arg5 ≤ 0 ∧ −1 + arg1P − arg3 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg3 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P + arg2 ≤ 0 ∧ −1 + arg2P − arg2 ≤ 0 ∧ − arg3P + arg5 ≤ 0 ∧ arg3P − arg5 ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0
5	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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 2 − arg5 ≤ 0 ∧ 1 + arg2 − arg5 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 + arg3P − arg3 ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0
5	8	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 ∧ 2 − arg5 ≤ 0 ∧ 1 + arg2 − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 + arg1P − arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 2 − arg3 + arg8P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg8P ≤ 0 ∧ 4 − arg3 + arg7P ≤ 0 ∧ 2 + arg10P − arg3 ≤ 0 ∧ 2 − arg3 + arg9P ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 0 ∧ arg4 − arg5P ≤ 0 ∧ − arg4 + arg5P ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
5	9	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 ∧ 2 − arg5 ≤ 0 ∧ 1 + arg2 − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 + arg1P − arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 2 − arg3 + arg8P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg8P ≤ 0 ∧ 4 − arg3 + arg7P ≤ 0 ∧ 2 + arg10P − arg3 ≤ 0 ∧ 2 − arg3 + arg9P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ −1 + arg4P ≤ 0 ∧ arg4 − arg5P ≤ 0 ∧ − arg4 + arg5P ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
5	10	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 ∧ 2 − arg5 ≤ 0 ∧ 1 + arg2 − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 1 + arg1P − arg3 ≤ 0 ∧ 2 + arg3P − arg3 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
5	11	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 ∧ 2 − arg5 ≤ 0 ∧ 1 + arg2 − arg5 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 2 + arg1P − arg3 ≤ 0 ∧ 2 + arg3P − arg3 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
7	12	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 ∧ arg1P − arg1 ≤ 0 ∧ 2 + arg1P − arg3 ≤ 0 ∧ −1 + arg1P − arg8 ≤ 0 ∧ 2 + arg3P − arg3 ≤ 0 ∧ arg3P − arg8 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − arg8 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ − arg3P ≤ 0 ∧ 4 − arg3 + arg7 ≤ 0 ∧ 2 − arg3 + arg9 ≤ 0 ∧ 2 + arg10 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ arg4 ≤ 0 ∧ − arg4P + arg5 ≤ 0 ∧ arg4P − arg5 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0 ∧ − arg2P + arg2P ≤ 0 ∧ arg2P − arg2P ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0
3	13	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 ∧ 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 ∧ − x118 ≤ 0 ∧ − x119 ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0
8	14	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 ∧ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0
8	15	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 ∧ 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 − arg4 + arg9P ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ 4 + arg12P − arg4 ≤ 0 ∧ − arg2P + arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 0 ∧ − arg11P + arg2 ≤ 0 ∧ arg11P − 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 ∧ − 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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
8	16	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 ∧ 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 − arg4 + arg9P ≤ 0 ∧ 2 + arg2 − arg4 ≤ 0 ∧ 4 + arg12P − arg4 ≤ 0 ∧ − arg2P + arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ −1 + arg4P ≤ 0 ∧ − arg11P + arg2 ≤ 0 ∧ arg11P − 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 ∧ − 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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
8	17	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 ∧ arg1P − arg1 ≤ 0 ∧ 1 − arg2 + x168 ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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	18	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 ∧ arg1P − arg1 ≤ 0 ∧ 1 + arg2 − x299 ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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	19	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 ∧ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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	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 ∧ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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
9	21	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 ∧ 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 ∧ 2 + arg11 − arg3 ≤ 0 ∧ 4 + arg12 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ arg4 ≤ 0 ∧ arg11 − arg2P ≤ 0 ∧ − arg11 + arg2P ≤ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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
8	22	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 ∧ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0
8	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 ∧ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0
10	24	11:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 ∧ − arg14P + arg7 ≤ 0 ∧ arg14P − 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0
11	25	11:	0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg14 + arg7 ≤ 0 ∧ 1 − arg14 ≤ 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 + arg13P − arg4 ≤ 0 ∧ 2 + arg11 − arg5 ≤ 0 ∧ 4 + arg11P − arg5 ≤ 0 ∧ 4 + arg12P − arg5 ≤ 0 ∧ 4 + arg13P − arg5 ≤ 0 ∧ 2 + arg12 − arg5 ≤ 0 ∧ 2 + arg13 − 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 ∧ − arg13P + arg13 ≤ 0 ∧ arg13P − arg13 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0
10	26	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 ∧ − 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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
11	27	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 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg10 ≤ 0 ∧ 1 − arg14 + 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 ∧ 2 + arg13 − arg5 ≤ 0 ∧ 1 + arg3 − arg4P ≤ 0 ∧ −1 − arg3 + arg4P ≤ 0 ∧ − arg5P + arg8 ≤ 0 ∧ arg5P − arg8 ≤ 0 ∧ − arg6P + arg9 ≤ 0 ∧ arg6P − arg9 ≤ 0 ∧ arg14 − arg7P ≤ 0 ∧ − arg14 + 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 0
12	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 ∧ 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 ∧ − arg14P + arg14 ≤ 0 ∧ arg14P − arg14 ≤ 0 ∧ − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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:	1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x38 ≤ 0
5:	1 − arg1P ≤ 0 ∧ − arg3P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg3 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x38 ≤ 0
6:	1 − arg2P ≤ 0 ∧ 1 − arg2 ≤ 0
7:	1 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg8P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ − arg8 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x38 ≤ 0
8:	4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x118 ≤ 0 ∧ − x119 ≤ 0
9:	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 ∧ − x118 ≤ 0 ∧ − x119 ≤ 0
10:	4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ − x118 ≤ 0 ∧ − x119 ≤ 0
11:	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 ∧ − x118 ≤ 0 ∧ − x119 ≤ 0
12:	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)	1 − arg1P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x38 ≤ 0
5	(5)	1 − arg1P ≤ 0 ∧ − arg3P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg3 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x38 ≤ 0
6	(6)	1 − arg2P ≤ 0 ∧ 1 − arg2 ≤ 0
7	(7)	1 − arg1P ≤ 0 ∧ 3 − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg8P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ − arg8 ≤ 0 ∧ − x7 ≤ 0 ∧ − x32 ≤ 0 ∧ − x38 ≤ 0
8	(8)	4 − arg1P ≤ 0 ∧ − arg4P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x118 ≤ 0 ∧ − x119 ≤ 0
9	(9)	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 ∧ − x118 ≤ 0 ∧ − x119 ≤ 0
10	(10)	4 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ − x118 ≤ 0 ∧ − x119 ≤ 0
11	(11)	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 ∧ − x118 ≤ 0 ∧ − x119 ≤ 0
12	(12)	TRUE

initial node: 12
cover edges:

transition edges:

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

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:

3	29	3:	− x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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:	− x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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	43	5:	− x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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	50	8:	− x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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:	− x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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	64	11:	− x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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, 7, 13, 14, 22, 23, 28 using the following ranking functions, which are bounded by −31.

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

4 Location Addition

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

3* 32 3: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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.

5* 46 5: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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.

5 44 5_var_snapshot: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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.

8* 53 8: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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.

8 51 8_var_snapshot: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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 Location Addition

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

11* 67 11: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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

15 Location Addition

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

11 65 11_var_snapshot: − x7 + x7 ≤ 0 ∧ x7 − x7 ≤ 0 ∧ − x38 + x38 ≤ 0 ∧ x38 − x38 ≤ 0 ∧ − x32 + x32 ≤ 0 ∧ x32 − x32 ≤ 0 ∧ − x30 + x30 ≤ 0 ∧ x30 − x30 ≤ 0 ∧ − x299 + x299 ≤ 0 ∧ x299 − x299 ≤ 0 ∧ − x29 + x29 ≤ 0 ∧ x29 − x29 ≤ 0 ∧ − x168 + x168 ≤ 0 ∧ x168 − x168 ≤ 0 ∧ − x119 + x119 ≤ 0 ∧ x119 − x119 ≤ 0 ∧ − x118 + x118 ≤ 0 ∧ x118 − x118 ≤ 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 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 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

16 SCC Decomposition

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

16.1 SCC Subproblem 1/4

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

16.1.1 Transition Removal

We remove transitions 5, 9 using the following ranking functions, which are bounded by 3.

4:	2 − 4⋅arg2 + 4⋅arg3
5:	−4⋅arg2 + 4⋅arg5
7:	−4⋅arg2 − arg4 + 4⋅arg6
4_var_snapshot:	1 − 4⋅arg2 + 4⋅arg3
4*:	3 − 4⋅arg2 + 4⋅arg3
5_var_snapshot:	−4⋅arg2 + 4⋅arg5
5*:	−4⋅arg2 + 4⋅arg5

16.1.2 Transition Removal

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

4:	−2
5:	1 + 2⋅arg3
7:	−1 + 2⋅arg3
4_var_snapshot:	−3
4*:	−1
5_var_snapshot:	2⋅arg3
5*:	2 + 2⋅arg3

16.1.3 Splitting Cut-Point Transitions

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

16.1.3.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 36.

16.1.3.1.1 Splitting Cut-Point Transitions

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

16.1.3.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 43.

16.1.3.2.1 Splitting Cut-Point Transitions

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

16.2 SCC Subproblem 2/4

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

16.2.1 Transition Removal

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

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

16.2.2 Transition Removal

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

10:	2 − 6⋅arg4 + 6⋅arg8
11:	6⋅arg10 − 6⋅arg3
10_var_snapshot:	1 − 6⋅arg4 + 6⋅arg8
10*:	3 − 6⋅arg4 + 6⋅arg8
11_var_snapshot:	6⋅arg10 − 6⋅arg3
11*:	6⋅arg10 − 6⋅arg3

16.2.3 Transition Removal

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

10:	2⋅arg2P
11:	2 + 2⋅arg5
10_var_snapshot:	2⋅arg2P − arg3P
10*:	1 + 2⋅arg2P
11_var_snapshot:	2⋅arg5
11*:	3 + 2⋅arg5

16.2.4 Transition Removal

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

10:	0
11:	0
10_var_snapshot:	−1
10*:	0
11_var_snapshot:	0
11*:	0

16.2.5 Splitting Cut-Point Transitions

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

16.2.5.1 Cut-Point Subproblem 1/2

Here we consider cut-point transition 57.

16.2.5.1.1 Splitting Cut-Point Transitions

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

16.2.5.2 Cut-Point Subproblem 2/2

Here we consider cut-point transition 64.

16.2.5.2.1 Splitting Cut-Point Transitions

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

16.3 SCC Subproblem 3/4

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

16.3.1 Transition Removal

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

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

16.3.2 Splitting Cut-Point Transitions

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

16.3.2.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 50.

16.3.2.1.1 Splitting Cut-Point Transitions

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

16.4 SCC Subproblem 4/4

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

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

16.4.2 Transition Removal

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

3:	0
3_var_snapshot:	−1
3*:	arg1P

16.4.3 Splitting Cut-Point Transitions

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

16.4.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 29.

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