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

Hints:

55	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
62	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
69	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
21	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
22	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
23	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
24	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
25	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
26	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
27	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
28	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
29	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
30	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
31	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
32	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
33	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
34	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
37	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
38	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
39	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
40	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
41	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
42	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
43	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
44	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
45	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
46	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
47	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
48	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
49	lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
0	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
3	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
4	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
5	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
7	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
9	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
10	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
11	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
12	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
13	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
14	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
15	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
16	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
17	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
19	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
20	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
35	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
36	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
50	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
51	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
52	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]
53	lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]