# LTS Termination Proof

by T2Cert

## Input

Integer Transition System
• Initial Location: 22
• 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 ∧ arg1P − arg1 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ arg2P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 0 1 1: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg1P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 1 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 ∧ arg1P − arg1 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg1P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 3 4 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 + arg1P − arg1 ≤ 0 ∧ 1 − arg1 + arg2P ≤ 0 ∧ 1 − arg1 + arg3P ≤ 0 ∧ 1 − arg1 + arg4P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 0 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 ∧ arg1P − arg1 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 1 7 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 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 7 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 ∧ 1 + arg1P − arg1 ≤ 0 ∧ 1 + arg1P − arg2 ≤ 0 ∧ 1 − arg1 + arg2P ≤ 0 ∧ 1 + arg2P − arg2 ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ 1 − arg1 + arg4P ≤ 0 ∧ 1 − arg2 + arg4P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ 2 − arg2 + 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 5 10 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 ∧ arg1P − arg1 ≤ 0 ∧ arg1P − arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg2 + arg4P ≤ 0 ∧ 2 − arg2 + arg4 ≤ 0 ∧ − arg3P + arg4 ≤ 0 ∧ arg3P − 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 9 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 ∧ arg1P − arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ 1 − arg1 + arg3P ≤ 0 ∧ 1 − arg2 + arg3P ≤ 0 ∧ − arg2 + arg4P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 2 − arg2 + arg4 ≤ 0 ∧ 2 − arg2 + 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 5 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 ∧ arg1P − arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg2 + arg4P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 0 13 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 ∧ 1 − arg1 ≤ 0 ∧ − 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 1 14 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 ∧ 1 − arg1 ≤ 0 ∧ − x79 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 5 15 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 ∧ 1 − arg1 ≤ 0 ∧ − x82 ≤ 0 ∧ 1 − arg2 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 10 16 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 ∧ − x88 ≤ 0 ∧ 1 − arg2P + x88 ≤ 0 ∧ − arg1P ≤ 0 ∧ arg1P ≤ 0 ∧ 1 − arg3P + x88 ≤ 0 ∧ −1 + arg3P − x88 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 10 17 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 ∧ 1 − arg2P + x90 ≤ 0 ∧ − arg1P ≤ 0 ∧ − x90 ≤ 0 ∧ 1 − arg3P + x90 ≤ 0 ∧ −1 + arg3P − x90 ≤ 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 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 11 19 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 2 − arg2P ≤ 0 ∧ 2 − arg1P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ arg2 − arg4P ≤ 0 ∧ − arg2 + arg4P ≤ 0 ∧ arg3 − arg5P ≤ 0 ∧ − arg3 + arg5P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 11 20 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 2 − arg2P ≤ 0 ∧ 2 − arg1P ≤ 0 ∧ arg1 − arg3P ≤ 0 ∧ − arg1 + arg3P ≤ 0 ∧ arg2 − arg4P ≤ 0 ∧ − arg2 + 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 13 21 14: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg4 − arg5 ≤ 0 ∧ − arg4 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ 1 − arg2 + arg4P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ 2 − arg1 + arg7P ≤ 0 ∧ 2 − arg1 + arg8P ≤ 0 ∧ 2 − arg2 + arg9P ≤ 0 ∧ − arg1P + arg3 ≤ 0 ∧ arg1P − arg3 ≤ 0 ∧ arg4 − arg5P ≤ 0 ∧ − arg4 + arg5P ≤ 0 ∧ arg5 − arg6P ≤ 0 ∧ − arg5 + arg6P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 14 22 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 + arg2P − arg3 ≤ 0 ∧ arg2P − arg4 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg2 + arg7 ≤ 0 ∧ 2 − arg2 + arg8 ≤ 0 ∧ 2 − arg3 + arg9 ≤ 0 ∧ −1 + arg1 − arg3P ≤ 0 ∧ 1 − arg1 + arg3P ≤ 0 ∧ − arg4P + arg5 ≤ 0 ∧ arg4P − arg5 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 14 23 15: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg5 − arg6 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg3P ≤ 0 ∧ 2 − arg2 + arg7 ≤ 0 ∧ 2 − arg2 + arg8 ≤ 0 ∧ 2 − arg3 + arg9 ≤ 0 ∧ − arg4P + arg5 ≤ 0 ∧ arg4P − arg5 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 0 ∧ − arg6P + arg8 ≤ 0 ∧ arg6P − arg8 ≤ 0 ∧ − arg7P + arg9 ≤ 0 ∧ arg7P − arg9 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 14 24 15: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg5 − arg6 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg3P ≤ 0 ∧ 2 − arg2 + arg7 ≤ 0 ∧ 2 − arg2 + arg8 ≤ 0 ∧ 2 − arg3 + arg9 ≤ 0 ∧ − arg4P + arg5 ≤ 0 ∧ arg4P − arg5 ≤ 0 ∧ − arg6P + arg8 ≤ 0 ∧ arg6P − arg8 ≤ 0 ∧ − arg7P + arg9 ≤ 0 ∧ arg7P − arg9 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 13 25 16: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 ≤ 0 ∧ − arg4 ≤ 0 ∧ 1 − arg4 + arg5 ≤ 0 ∧ − arg5 ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 2 − arg1 + arg7P ≤ 0 ∧ 2 − arg1 + arg8P ≤ 0 ∧ − arg1P + arg3 ≤ 0 ∧ arg1P − arg3 ≤ 0 ∧ − arg4P ≤ 0 ∧ arg4P ≤ 0 ∧ arg4 − arg5P ≤ 0 ∧ − arg4 + arg5P ≤ 0 ∧ 1 + arg5 − arg6P ≤ 0 ∧ −1 − arg5 + arg6P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 13 26 16: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 ≤ 0 ∧ − arg4 ≤ 0 ∧ 1 − arg4 + arg5 ≤ 0 ∧ − arg5 ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg1 + arg2P ≤ 0 ∧ − arg2 + arg3P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ 2 − arg1 + arg7P ≤ 0 ∧ 2 − arg1 + arg8P ≤ 0 ∧ − arg1P + arg3 ≤ 0 ∧ arg1P − arg3 ≤ 0 ∧ arg4 − arg5P ≤ 0 ∧ − arg4 + arg5P ≤ 0 ∧ 1 + arg5 − arg6P ≤ 0 ∧ −1 − arg5 + arg6P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 15 27 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg2 + arg6 ≤ 0 ∧ 2 − arg3 + arg7 ≤ 0 ∧ −1 + arg1 − arg3P ≤ 0 ∧ 1 − arg1 + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 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 15 28 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 + arg1P − arg2 ≤ 0 ∧ −2 + arg1P − arg3 ≤ 0 ∧ −2 + arg2P − arg2 ≤ 0 ∧ −2 + arg2P − arg3 ≤ 0 ∧ 2 − arg2 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 4 − arg2P ≤ 0 ∧ 2 − arg2 + arg6 ≤ 0 ∧ 2 − arg3 + arg6 ≤ 0 ∧ arg6 − arg7 ≤ 0 ∧ − arg6 + arg7 ≤ 0 ∧ −1 + arg1 − arg3P ≤ 0 ∧ 1 − arg1 + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 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 16 29 14: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 1 − arg3 + arg4P ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 1 − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ 2 − arg2 + arg7 ≤ 0 ∧ 2 − arg2 + arg8 ≤ 0 ∧ 2 − arg3 + arg9P ≤ 0 ∧ − arg4 ≤ 0 ∧ arg4 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 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 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 16 30 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 ∧ 1 − arg4 ≤ 0 ∧ 2 + arg2P − arg3 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 3 − arg3 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg2 + arg7 ≤ 0 ∧ 2 − arg2 + arg8 ≤ 0 ∧ −1 + arg1 − arg3P ≤ 0 ∧ 1 − arg1 + arg3P ≤ 0 ∧ − arg4P + arg5 ≤ 0 ∧ arg4P − arg5 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 16 31 17: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg6 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg3P ≤ 0 ∧ 2 − arg2 + arg7 ≤ 0 ∧ 2 − arg2 + arg8 ≤ 0 ∧ 2 − arg3 + arg7P ≤ 0 ∧ − arg4P + arg5 ≤ 0 ∧ arg4P − arg5 ≤ 0 ∧ − arg5P + arg6 ≤ 0 ∧ arg5P − arg6 ≤ 0 ∧ − arg6P + arg7 ≤ 0 ∧ arg6P − arg7 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 16 32 17: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg6 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg3P ≤ 0 ∧ 2 − arg2 + arg7 ≤ 0 ∧ 2 − arg2 + arg8 ≤ 0 ∧ 2 − arg3 + arg7P ≤ 0 ∧ − arg4P + arg5 ≤ 0 ∧ arg4P − arg5 ≤ 0 ∧ − arg6P + arg7 ≤ 0 ∧ arg6P − arg7 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 17 33 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 ≤ 0 ∧ 1 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 2 − arg2 + arg6 ≤ 0 ∧ 2 − arg3 + arg7 ≤ 0 ∧ −1 + arg1 − arg3P ≤ 0 ∧ 1 − arg1 + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 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 17 34 13: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 + arg1P − arg2 ≤ 0 ∧ −2 + arg1P − arg3 ≤ 0 ∧ −2 + arg2P − arg2 ≤ 0 ∧ −2 + arg2P − arg3 ≤ 0 ∧ 2 − arg2 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 4 − arg2P ≤ 0 ∧ 2 − arg2 + arg6 ≤ 0 ∧ 2 − arg3 + arg6 ≤ 0 ∧ arg6 − arg7 ≤ 0 ∧ − arg6 + arg7 ≤ 0 ∧ −1 + arg1 − arg3P ≤ 0 ∧ 1 − arg1 + arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 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 4 35 18: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg3 ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ − arg1P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 4 36 18: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 + arg1P − arg1 ≤ 0 ∧ 1 + arg1P − arg2 ≤ 0 ∧ 1 + arg1P − arg4 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ − arg1P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 4 37 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ 2 − arg1 + arg3P ≤ 0 ∧ 2 − arg2 + arg3P ≤ 0 ∧ 2 + arg3P − arg4 ≤ 0 ∧ − arg3 + arg4P ≤ 0 ∧ 2 − arg1 ≤ 0 ∧ 2 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ 2 − arg4 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 4 38 19: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg2 ≤ 0 ∧ arg1P − arg4 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 2 − arg1 + arg4P ≤ 0 ∧ 2 − arg2 + arg4P ≤ 0 ∧ 2 + arg4P − arg4 ≤ 0 ∧ 2 − arg1 + arg6P ≤ 0 ∧ 2 − arg2 + arg6P ≤ 0 ∧ 2 − arg4 + arg6P ≤ 0 ∧ 5 − arg1 ≤ 0 ∧ 5 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ 5 − arg4 ≤ 0 ∧ 5 − arg1P ≤ 0 ∧ 3 − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg6P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 4 39 19: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg2 ≤ 0 ∧ arg1P − arg4 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 2 − arg1 + arg4P ≤ 0 ∧ 2 − arg2 + arg4P ≤ 0 ∧ 2 + arg4P − arg4 ≤ 0 ∧ 2 − arg1 + arg6P ≤ 0 ∧ 2 − arg2 + arg6P ≤ 0 ∧ 2 − arg4 + arg6P ≤ 0 ∧ 5 − arg1 ≤ 0 ∧ 5 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ 5 − arg4 ≤ 0 ∧ 5 − arg1P ≤ 0 ∧ 3 − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg6P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 4 40 19: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg2 ≤ 0 ∧ arg1P − arg4 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 2 − arg1 + arg4P ≤ 0 ∧ 2 − arg2 + arg4P ≤ 0 ∧ 2 + arg4P − arg4 ≤ 0 ∧ 2 − arg1 + arg6P ≤ 0 ∧ 2 − arg2 + arg6P ≤ 0 ∧ 2 − arg4 + arg6P ≤ 0 ∧ 5 − arg1 ≤ 0 ∧ 5 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ 5 − arg4 ≤ 0 ∧ 5 − arg1P ≤ 0 ∧ 3 − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg6P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 4 41 19: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg2 ≤ 0 ∧ arg1P − arg4 ≤ 0 ∧ 2 − arg1 + arg2P ≤ 0 ∧ 2 + arg2P − arg2 ≤ 0 ∧ −2 + arg2P − arg3 ≤ 0 ∧ 2 + arg2P − arg4 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ 2 − arg1 + arg4P ≤ 0 ∧ 2 − arg2 + arg4P ≤ 0 ∧ 2 + arg4P − arg4 ≤ 0 ∧ 2 − arg1 + arg6P ≤ 0 ∧ 2 − arg2 + arg6P ≤ 0 ∧ 2 − arg4 + arg6P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 4 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ 4 − arg4 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ 2 − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg4P ≤ 0 ∧ − arg6P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 19 42 4: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ arg1P − arg3 ≤ 0 ∧ arg2P − arg3 ≤ 0 ∧ 2 − arg1 + arg3P ≤ 0 ∧ arg3P − arg4 ≤ 0 ∧ arg3P − arg6 ≤ 0 ∧ − arg3 + arg4P ≤ 0 ∧ 3 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ − arg6 ≤ 0 ∧ − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 18 43 18: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 + arg1P − arg1 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg1P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 18 44 18: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 + arg1P − arg1 ≤ 0 ∧ 2 − arg1 ≤ 0 ∧ − arg1P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 18 45 20: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg1 + arg2P ≤ 0 ∧ 2 − arg1 + arg3P ≤ 0 ∧ 5 − arg1 ≤ 0 ∧ 5 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 18 46 20: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg1 + arg2P ≤ 0 ∧ 2 − arg1 + arg3P ≤ 0 ∧ 5 − arg1 ≤ 0 ∧ 5 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 18 47 20: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg1 + arg2P ≤ 0 ∧ 2 − arg1 + arg3P ≤ 0 ∧ 5 − arg1 ≤ 0 ∧ 5 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 18 48 20: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 − arg1 + arg2P ≤ 0 ∧ 2 − arg1 + arg3P ≤ 0 ∧ 4 − arg1 ≤ 0 ∧ 4 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 0 ∧ − arg2P + arg2 ≤ 0 ∧ arg2P − arg2 ≤ 0 ∧ − arg3P + arg3 ≤ 0 ∧ arg3P − arg3 ≤ 0 ∧ − arg4P + arg4 ≤ 0 ∧ arg4P − arg4 ≤ 0 ∧ − arg5P + arg5 ≤ 0 ∧ arg5P − arg5 ≤ 0 ∧ − arg6P + arg6 ≤ 0 ∧ arg6P − arg6 ≤ 0 ∧ − arg7P + arg7 ≤ 0 ∧ arg7P − arg7 ≤ 0 ∧ − arg8P + arg8 ≤ 0 ∧ arg8P − arg8 ≤ 0 ∧ − arg9P + arg9 ≤ 0 ∧ arg9P − arg9 ≤ 0 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 20 49 18: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 + arg1P − arg1 ≤ 0 ∧ arg1P − arg2 ≤ 0 ∧ arg1P − arg3 ≤ 0 ∧ 3 − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg3 ≤ 0 ∧ − arg1P ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 11 50 21: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ 1 − arg3 ≤ 0 ∧ − arg1P + arg1 ≤ 0 ∧ arg1P − arg1 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 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 14 51 21: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ − arg5 ≤ 0 ∧ arg5 − arg6 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ − arg4 ≤ 0 ∧ 2 − arg2 + arg7 ≤ 0 ∧ 2 − arg2 + arg8 ≤ 0 ∧ 2 − arg3 + arg9 ≤ 0 ∧ − arg2P + arg5 ≤ 0 ∧ arg2P − arg5 ≤ 0 ∧ − arg3P + arg6 ≤ 0 ∧ arg3P − arg6 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 16 52 21: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 1 − arg6 ≤ 0 ∧ − arg5 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ 2 − arg3 ≤ 0 ∧ 2 − arg2 + arg7 ≤ 0 ∧ 2 − arg2 + arg8 ≤ 0 ∧ − arg2P + arg5 ≤ 0 ∧ arg2P − arg5 ≤ 0 ∧ − arg3P + arg6 ≤ 0 ∧ arg3P − arg6 ≤ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0 22 53 0: 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 0 ≤ 0 ∧ 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 ∧ − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 0

## Proof

### 1 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
 4 54 4: − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 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 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 13 61 13: − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 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 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0 18 68 18: − x90 + x90 ≤ 0 ∧ x90 − x90 ≤ 0 ∧ − x88 + x88 ≤ 0 ∧ x88 − x88 ≤ 0 ∧ − x82 + x82 ≤ 0 ∧ x82 − x82 ≤ 0 ∧ − x79 + x79 ≤ 0 ∧ x79 − x79 ≤ 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 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
and for every transition t, a duplicate t is considered.

### 2 Transition Removal

We remove transitions 0, 1, 3, 4, 5, 7, 9, 10, 11, 12, 13, 14, 15, 16, 17, 19, 20, 35, 36, 50, 51, 52, 53 using the following ranking functions, which are bounded by −35.

 22: 0 0: 0 1: 0 3: 0 7: 0 5: 0 9: 0 4: 0 19: 0 18: 0 20: 0 10: 0 11: 0 13: 0 14: 0 15: 0 16: 0 17: 0 21: 0 22: −14 0: −15 1: −16 3: −17 7: −18 5: −19 9: −20 4: −21 19: −21 4_var_snapshot: −21 4*: −21 18: −24 20: −24 18_var_snapshot: −24 18*: −24 10: −27 11: −28 13: −29 14: −29 15: −29 16: −29 17: −29 13_var_snapshot: −29 13*: −29 21: −33

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

4* 57 4: x90 + x90 ≤ 0x90x90 ≤ 0x88 + x88 ≤ 0x88x88 ≤ 0x82 + x82 ≤ 0x82x82 ≤ 0x79 + x79 ≤ 0x79x79 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

4 55 4_var_snapshot: x90 + x90 ≤ 0x90x90 ≤ 0x88 + x88 ≤ 0x88x88 ≤ 0x82 + x82 ≤ 0x82x82 ≤ 0x79 + x79 ≤ 0x79x79 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

13* 64 13: x90 + x90 ≤ 0x90x90 ≤ 0x88 + x88 ≤ 0x88x88 ≤ 0x82 + x82 ≤ 0x82x82 ≤ 0x79 + x79 ≤ 0x79x79 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

13 62 13_var_snapshot: x90 + x90 ≤ 0x90x90 ≤ 0x88 + x88 ≤ 0x88x88 ≤ 0x82 + x82 ≤ 0x82x82 ≤ 0x79 + x79 ≤ 0x79x79 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

18* 71 18: x90 + x90 ≤ 0x90x90 ≤ 0x88 + x88 ≤ 0x88x88 ≤ 0x82 + x82 ≤ 0x82x82 ≤ 0x79 + x79 ≤ 0x79x79 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

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

18 69 18_var_snapshot: x90 + x90 ≤ 0x90x90 ≤ 0x88 + x88 ≤ 0x88x88 ≤ 0x82 + x82 ≤ 0x82x82 ≤ 0x79 + x79 ≤ 0x79x79 ≤ 0arg9P + arg9P ≤ 0arg9Parg9P ≤ 0arg9 + arg9 ≤ 0arg9arg9 ≤ 0arg8P + arg8P ≤ 0arg8Parg8P ≤ 0arg8 + arg8 ≤ 0arg8arg8 ≤ 0arg7P + arg7P ≤ 0arg7Parg7P ≤ 0arg7 + arg7 ≤ 0arg7arg7 ≤ 0arg6P + arg6P ≤ 0arg6Parg6P ≤ 0arg6 + arg6 ≤ 0arg6arg6 ≤ 0arg5P + arg5P ≤ 0arg5Parg5P ≤ 0arg5 + arg5 ≤ 0arg5arg5 ≤ 0arg4P + arg4P ≤ 0arg4Parg4P ≤ 0arg4 + arg4 ≤ 0arg4arg4 ≤ 0arg3P + arg3P ≤ 0arg3Parg3P ≤ 0arg3 + arg3 ≤ 0arg3arg3 ≤ 0arg2P + arg2P ≤ 0arg2Parg2P ≤ 0arg2 + arg2 ≤ 0arg2arg2 ≤ 0arg1P + arg1P ≤ 0arg1Parg1P ≤ 0arg1 + arg1 ≤ 0arg1arg1 ≤ 0

### 9 SCC Decomposition

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

### 9.1 SCC Subproblem 1/3

Here we consider the SCC { 18, 20, 18_var_snapshot, 18* }.

### 9.1.1 Transition Removal

We remove transitions 43, 44, 45, 46, 47, 48, 49 using the following ranking functions, which are bounded by 0.

 18: −1 + 3⋅arg1 20: 1 + 3⋅arg3 18_var_snapshot: −2 + 3⋅arg1 18*: 3⋅arg1

### 9.1.2 Transition Removal

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

 18: 0 20: 0 18_var_snapshot: −1 18*: 1

### 9.1.3 Splitting Cut-Point Transitions

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

### 9.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 68.

### 9.1.3.1.1 Splitting Cut-Point Transitions

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

### 9.2 SCC Subproblem 2/3

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

### 9.2.1 Transition Removal

We remove transitions 37, 38, 39, 40, 41, 42 using the following ranking functions, which are bounded by −1.

 4: −4 + arg2 + 3⋅arg3 + 2⋅arg4 19: 3⋅arg3 + 3⋅arg6 4_var_snapshot: −5 + arg2 + 3⋅arg3 + 2⋅arg4 4*: −3 + arg2 + 3⋅arg3 + 2⋅arg4

### 9.2.2 Transition Removal

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

 4: −1 19: 0 4_var_snapshot: −2 4*: 0

### 9.2.3 Splitting Cut-Point Transitions

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

### 9.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 54.

### 9.2.3.1.1 Splitting Cut-Point Transitions

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

### 9.3 SCC Subproblem 3/3

Here we consider the SCC { 13, 14, 15, 16, 17, 13_var_snapshot, 13* }.

### 9.3.1 Transition Removal

We remove transitions 21, 23, 24, 25, 31, 32 using the following ranking functions, which are bounded by 1.

 13: −1 + 7⋅arg3 14: −5 + 7⋅arg1 15: −6 + 7⋅arg1 16: −3 + 7⋅arg1 17: −4 + 7⋅arg1 13_var_snapshot: −2 + 7⋅arg3 13*: 7⋅arg3

### 9.3.2 Transition Removal

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

 13: −1 + arg3 + 3⋅arg4 − 3⋅arg5 14: −1 + arg1 + 3⋅arg5 − 3⋅arg6 15: arg1 + 3⋅arg4 − 3⋅arg5 16: arg1 + 3⋅arg5 − 3⋅arg6 17: arg1 + 3⋅arg4 − 3⋅arg5 13_var_snapshot: −2 + arg3 + 3⋅arg4 − 3⋅arg5 13*: arg3 + 3⋅arg4 − 3⋅arg5

### 9.3.3 Transition Removal

We remove transitions 62, 64, 22, 27, 28, 29, 30, 33, 34 using the following ranking functions, which are bounded by −2.

 13: −1 14: 1 15: arg2 16: 2 17: arg2 13_var_snapshot: −2 13*: 0

### 9.3.4 Splitting Cut-Point Transitions

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

### 9.3.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 61.

### 9.3.4.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0