LTS Termination Proof

by T2Cert

Input

Integer Transition System

Proof

1 Invariant Updates

The following invariants are asserted.

0: 1 − arg1P ≤ 0 ∧ 7 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 3 − arg5P ≤ 0 ∧ 1 − arg8P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 7 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ 1 − arg8 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0 ∧ − x387 ≤ 0
1: 1 − arg1P ≤ 0 ∧ 7 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 3 − arg5P ≤ 0 ∧ 1 − arg8P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 7 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ 1 − arg8 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0 ∧ − x387 ≤ 0
2: 1 − arg1P ≤ 0 ∧ 7 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 5 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 7 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 5 − arg5 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0 ∧ − x426 ≤ 0
3: 1 − arg1P ≤ 0 ∧ 7 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 5 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 7 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 5 − arg5 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0 ∧ − x426 ≤ 0
4: 1 − arg1P ≤ 0 ∧ 8 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 3 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 8 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0
5: 1 − arg1P ≤ 0 ∧ 8 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 3 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 8 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0
6: 1 − arg1P ≤ 0 ∧ 10 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 5 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 10 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 5 − arg5 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0
7: 1 − arg1P ≤ 0 ∧ 10 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 5 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 10 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 5 − arg5 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0
8: − arg1P ≤ 0 ∧ 8 − arg2P ≤ 0 ∧ −1 + arg5P ≤ 0 ∧ 1 − arg5P ≤ 0 ∧ arg6P ≤ 0 ∧ − arg6P ≤ 0 ∧ arg7P ≤ 0 ∧ − arg7P ≤ 0 ∧ − arg1 ≤ 0 ∧ 8 − arg2 ≤ 0 ∧ −1 + arg5 ≤ 0 ∧ 1 − arg5 ≤ 0 ∧ arg6 ≤ 0 ∧ − arg6 ≤ 0 ∧ arg7 ≤ 0 ∧ − arg7 ≤ 0
9: − arg1P ≤ 0 ∧ 10 − arg2P ≤ 0 ∧ arg3P ≤ 0 ∧ − arg3P ≤ 0 ∧ arg4P ≤ 0 ∧ − arg4P ≤ 0 ∧ arg8P ≤ 0 ∧ − arg8P ≤ 0 ∧ arg9P ≤ 0 ∧ − arg9P ≤ 0 ∧ arg10P ≤ 0 ∧ − arg10P ≤ 0 ∧ −1 + arg19P ≤ 0 ∧ arg20P ≤ 0 ∧ arg23P ≤ 0 ∧ − arg1 ≤ 0 ∧ 10 − arg2 ≤ 0 ∧ arg3 ≤ 0 ∧ − arg3 ≤ 0 ∧ arg4 ≤ 0 ∧ − arg4 ≤ 0 ∧ arg8 ≤ 0 ∧ − arg8 ≤ 0 ∧ arg9 ≤ 0 ∧ − arg9 ≤ 0 ∧ arg10 ≤ 0 ∧ − arg10 ≤ 0 ∧ −1 + arg19 ≤ 0 ∧ arg20 ≤ 0 ∧ arg23 ≤ 0
10: TRUE
11: 7 − arg1P ≤ 0 ∧ 7 − arg1 ≤ 0 ∧ − x162 ≤ 0
13: 7 − arg1P ≤ 0 ∧ − arg2P ≤ 0 ∧ − arg4P ≤ 0 ∧ 7 − arg1 ≤ 0 ∧ − arg2 ≤ 0 ∧ − arg4 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0
14: − arg1P ≤ 0 ∧ − arg3P ≤ 0 ∧ − arg1 ≤ 0 ∧ − arg3 ≤ 0 ∧ − x162 ≤ 0 ∧ − x287 ≤ 0
15: 8 − arg1P ≤ 0 ∧ 5 − arg2P ≤ 0 ∧ 8 − arg1 ≤ 0 ∧ 5 − arg2 ≤ 0 ∧ − x162 ≤ 0 ∧ − x177 ≤ 0
16: 3 − arg1P ≤ 0 ∧ 1 − arg2P ≤ 0 ∧ 3 − arg1 ≤ 0 ∧ 1 − arg2 ≤ 0 ∧ − x162 ≤ 0 ∧ − x287 ≤ 0
17: 1 − arg1P ≤ 0 ∧ 7 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg4P ≤ 0 ∧ 3 − arg5P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 7 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ 1 − arg4 ≤ 0 ∧ 3 − arg5 ≤ 0 ∧ − x162 ≤ 0 ∧ − x287 ≤ 0
18: 1 − arg1P ≤ 0 ∧ 10 − arg2P ≤ 0 ∧ 5 − arg3P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ 10 − arg2 ≤ 0 ∧ 5 − arg3 ≤ 0 ∧ − x162 ≤ 0 ∧ − x287 ≤ 0
19: 1 − arg1P ≤ 0 ∧ arg12P ≤ 0 ∧ − arg12P ≤ 0 ∧ 1 − arg1 ≤ 0 ∧ arg12 ≤ 0 ∧ − arg12 ≤ 0
20: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
13 34 13: − x720 + x720 ≤ 0 ∧ x720 − x720 ≤ 0 ∧ − x685 + x685 ≤ 0 ∧ x685 − x685 ≤ 0 ∧ − x684 + x684 ≤ 0 ∧ x684 − x684 ≤ 0 ∧ − x643 + x643 ≤ 0 ∧ x643 − x643 ≤ 0 ∧ − x608 + x608 ≤ 0 ∧ x608 − x608 ≤ 0 ∧ − x607 + x607 ≤ 0 ∧ x607 − x607 ≤ 0 ∧ − x606 + x606 ≤ 0 ∧ x606 − x606 ≤ 0 ∧ − x605 + x605 ≤ 0 ∧ x605 − x605 ≤ 0 ∧ − x604 + x604 ≤ 0 ∧ x604 − x604 ≤ 0 ∧ − x603 + x603 ≤ 0 ∧ x603 − x603 ≤ 0 ∧ − x590 + x590 ≤ 0 ∧ x590 − x590 ≤ 0 ∧ − x589 + x589 ≤ 0 ∧ x589 − x589 ≤ 0 ∧ − x588 + x588 ≤ 0 ∧ x588 − x588 ≤ 0 ∧ − x587 + x587 ≤ 0 ∧ x587 − x587 ≤ 0 ∧ − x586 + x586 ≤ 0 ∧ x586 − x586 ≤ 0 ∧ − x560 + x560 ≤ 0 ∧ x560 − x560 ≤ 0 ∧ − x545 + x545 ≤ 0 ∧ x545 − x545 ≤ 0 ∧ − x544 + x544 ≤ 0 ∧ x544 − x544 ≤ 0 ∧ − x535 + x535 ≤ 0 ∧ x535 − x535 ≤ 0 ∧ − x534 + x534 ≤ 0 ∧ x534 − x534 ≤ 0 ∧ − x524 + x524 ≤ 0 ∧ x524 − x524 ≤ 0 ∧ − x513 + x513 ≤ 0 ∧ x513 − x513 ≤ 0 ∧ − x503 + x503 ≤ 0 ∧ x503 − x503 ≤ 0 ∧ − x427 + x427 ≤ 0 ∧ x427 − x427 ≤ 0 ∧ − x426 + x426 ≤ 0 ∧ x426 − x426 ≤ 0 ∧ − x425 + x425 ≤ 0 ∧ x425 − x425 ≤ 0 ∧ − x387 + x387 ≤ 0 ∧ x387 − x387 ≤ 0 ∧ − x386 + x386 ≤ 0 ∧ x386 − x386 ≤ 0 ∧ − x346 + x346 ≤ 0 ∧ x346 − x346 ≤ 0 ∧ − x345 + x345 ≤ 0 ∧ x345 − x345 ≤ 0 ∧ − x344 + x344 ≤ 0 ∧ x344 − x344 ≤ 0 ∧ − x343 + x343 ≤ 0 ∧ x343 − x343 ≤ 0 ∧ − x342 + x342 ≤ 0 ∧ x342 − x342 ≤ 0 ∧ − x341 + x341 ≤ 0 ∧ x341 − x341 ≤ 0 ∧ − x340 + x340 ≤ 0 ∧ x340 − x340 ≤ 0 ∧ − x339 + x339 ≤ 0 ∧ x339 − x339 ≤ 0 ∧ − x321 + x321 ≤ 0 ∧ x321 − x321 ≤ 0 ∧ − x320 + x320 ≤ 0 ∧ x320 − x320 ≤ 0 ∧ − x319 + x319 ≤ 0 ∧ x319 − x319 ≤ 0 ∧ − x318 + x318 ≤ 0 ∧ x318 − x318 ≤ 0 ∧ − x317 + x317 ≤ 0 ∧ x317 − x317 ≤ 0 ∧ − x316 + x316 ≤ 0 ∧ x316 − x316 ≤ 0 ∧ − x315 + x315 ≤ 0 ∧ x315 − x315 ≤ 0 ∧ − x297 + x297 ≤ 0 ∧ x297 − x297 ≤ 0 ∧ − x287 + x287 ≤ 0 ∧ x287 − x287 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x284 + x284 ≤ 0 ∧ x284 − x284 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x229 + x229 ≤ 0 ∧ x229 − x229 ≤ 0 ∧ − x211 + x211 ≤ 0 ∧ x211 − x211 ≤ 0 ∧ − x190 + x190 ≤ 0 ∧ x190 − x190 ≤ 0 ∧ − x177 + x177 ≤ 0 ∧ x177 − x177 ≤ 0 ∧ − x162 + x162 ≤ 0 ∧ x162 − x162 ≤ 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 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
14 41 14: − x720 + x720 ≤ 0 ∧ x720 − x720 ≤ 0 ∧ − x685 + x685 ≤ 0 ∧ x685 − x685 ≤ 0 ∧ − x684 + x684 ≤ 0 ∧ x684 − x684 ≤ 0 ∧ − x643 + x643 ≤ 0 ∧ x643 − x643 ≤ 0 ∧ − x608 + x608 ≤ 0 ∧ x608 − x608 ≤ 0 ∧ − x607 + x607 ≤ 0 ∧ x607 − x607 ≤ 0 ∧ − x606 + x606 ≤ 0 ∧ x606 − x606 ≤ 0 ∧ − x605 + x605 ≤ 0 ∧ x605 − x605 ≤ 0 ∧ − x604 + x604 ≤ 0 ∧ x604 − x604 ≤ 0 ∧ − x603 + x603 ≤ 0 ∧ x603 − x603 ≤ 0 ∧ − x590 + x590 ≤ 0 ∧ x590 − x590 ≤ 0 ∧ − x589 + x589 ≤ 0 ∧ x589 − x589 ≤ 0 ∧ − x588 + x588 ≤ 0 ∧ x588 − x588 ≤ 0 ∧ − x587 + x587 ≤ 0 ∧ x587 − x587 ≤ 0 ∧ − x586 + x586 ≤ 0 ∧ x586 − x586 ≤ 0 ∧ − x560 + x560 ≤ 0 ∧ x560 − x560 ≤ 0 ∧ − x545 + x545 ≤ 0 ∧ x545 − x545 ≤ 0 ∧ − x544 + x544 ≤ 0 ∧ x544 − x544 ≤ 0 ∧ − x535 + x535 ≤ 0 ∧ x535 − x535 ≤ 0 ∧ − x534 + x534 ≤ 0 ∧ x534 − x534 ≤ 0 ∧ − x524 + x524 ≤ 0 ∧ x524 − x524 ≤ 0 ∧ − x513 + x513 ≤ 0 ∧ x513 − x513 ≤ 0 ∧ − x503 + x503 ≤ 0 ∧ x503 − x503 ≤ 0 ∧ − x427 + x427 ≤ 0 ∧ x427 − x427 ≤ 0 ∧ − x426 + x426 ≤ 0 ∧ x426 − x426 ≤ 0 ∧ − x425 + x425 ≤ 0 ∧ x425 − x425 ≤ 0 ∧ − x387 + x387 ≤ 0 ∧ x387 − x387 ≤ 0 ∧ − x386 + x386 ≤ 0 ∧ x386 − x386 ≤ 0 ∧ − x346 + x346 ≤ 0 ∧ x346 − x346 ≤ 0 ∧ − x345 + x345 ≤ 0 ∧ x345 − x345 ≤ 0 ∧ − x344 + x344 ≤ 0 ∧ x344 − x344 ≤ 0 ∧ − x343 + x343 ≤ 0 ∧ x343 − x343 ≤ 0 ∧ − x342 + x342 ≤ 0 ∧ x342 − x342 ≤ 0 ∧ − x341 + x341 ≤ 0 ∧ x341 − x341 ≤ 0 ∧ − x340 + x340 ≤ 0 ∧ x340 − x340 ≤ 0 ∧ − x339 + x339 ≤ 0 ∧ x339 − x339 ≤ 0 ∧ − x321 + x321 ≤ 0 ∧ x321 − x321 ≤ 0 ∧ − x320 + x320 ≤ 0 ∧ x320 − x320 ≤ 0 ∧ − x319 + x319 ≤ 0 ∧ x319 − x319 ≤ 0 ∧ − x318 + x318 ≤ 0 ∧ x318 − x318 ≤ 0 ∧ − x317 + x317 ≤ 0 ∧ x317 − x317 ≤ 0 ∧ − x316 + x316 ≤ 0 ∧ x316 − x316 ≤ 0 ∧ − x315 + x315 ≤ 0 ∧ x315 − x315 ≤ 0 ∧ − x297 + x297 ≤ 0 ∧ x297 − x297 ≤ 0 ∧ − x287 + x287 ≤ 0 ∧ x287 − x287 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x284 + x284 ≤ 0 ∧ x284 − x284 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x229 + x229 ≤ 0 ∧ x229 − x229 ≤ 0 ∧ − x211 + x211 ≤ 0 ∧ x211 − x211 ≤ 0 ∧ − x190 + x190 ≤ 0 ∧ x190 − x190 ≤ 0 ∧ − x177 + x177 ≤ 0 ∧ x177 − x177 ≤ 0 ∧ − x162 + x162 ≤ 0 ∧ x162 − x162 ≤ 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 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
19 48 19: − x720 + x720 ≤ 0 ∧ x720 − x720 ≤ 0 ∧ − x685 + x685 ≤ 0 ∧ x685 − x685 ≤ 0 ∧ − x684 + x684 ≤ 0 ∧ x684 − x684 ≤ 0 ∧ − x643 + x643 ≤ 0 ∧ x643 − x643 ≤ 0 ∧ − x608 + x608 ≤ 0 ∧ x608 − x608 ≤ 0 ∧ − x607 + x607 ≤ 0 ∧ x607 − x607 ≤ 0 ∧ − x606 + x606 ≤ 0 ∧ x606 − x606 ≤ 0 ∧ − x605 + x605 ≤ 0 ∧ x605 − x605 ≤ 0 ∧ − x604 + x604 ≤ 0 ∧ x604 − x604 ≤ 0 ∧ − x603 + x603 ≤ 0 ∧ x603 − x603 ≤ 0 ∧ − x590 + x590 ≤ 0 ∧ x590 − x590 ≤ 0 ∧ − x589 + x589 ≤ 0 ∧ x589 − x589 ≤ 0 ∧ − x588 + x588 ≤ 0 ∧ x588 − x588 ≤ 0 ∧ − x587 + x587 ≤ 0 ∧ x587 − x587 ≤ 0 ∧ − x586 + x586 ≤ 0 ∧ x586 − x586 ≤ 0 ∧ − x560 + x560 ≤ 0 ∧ x560 − x560 ≤ 0 ∧ − x545 + x545 ≤ 0 ∧ x545 − x545 ≤ 0 ∧ − x544 + x544 ≤ 0 ∧ x544 − x544 ≤ 0 ∧ − x535 + x535 ≤ 0 ∧ x535 − x535 ≤ 0 ∧ − x534 + x534 ≤ 0 ∧ x534 − x534 ≤ 0 ∧ − x524 + x524 ≤ 0 ∧ x524 − x524 ≤ 0 ∧ − x513 + x513 ≤ 0 ∧ x513 − x513 ≤ 0 ∧ − x503 + x503 ≤ 0 ∧ x503 − x503 ≤ 0 ∧ − x427 + x427 ≤ 0 ∧ x427 − x427 ≤ 0 ∧ − x426 + x426 ≤ 0 ∧ x426 − x426 ≤ 0 ∧ − x425 + x425 ≤ 0 ∧ x425 − x425 ≤ 0 ∧ − x387 + x387 ≤ 0 ∧ x387 − x387 ≤ 0 ∧ − x386 + x386 ≤ 0 ∧ x386 − x386 ≤ 0 ∧ − x346 + x346 ≤ 0 ∧ x346 − x346 ≤ 0 ∧ − x345 + x345 ≤ 0 ∧ x345 − x345 ≤ 0 ∧ − x344 + x344 ≤ 0 ∧ x344 − x344 ≤ 0 ∧ − x343 + x343 ≤ 0 ∧ x343 − x343 ≤ 0 ∧ − x342 + x342 ≤ 0 ∧ x342 − x342 ≤ 0 ∧ − x341 + x341 ≤ 0 ∧ x341 − x341 ≤ 0 ∧ − x340 + x340 ≤ 0 ∧ x340 − x340 ≤ 0 ∧ − x339 + x339 ≤ 0 ∧ x339 − x339 ≤ 0 ∧ − x321 + x321 ≤ 0 ∧ x321 − x321 ≤ 0 ∧ − x320 + x320 ≤ 0 ∧ x320 − x320 ≤ 0 ∧ − x319 + x319 ≤ 0 ∧ x319 − x319 ≤ 0 ∧ − x318 + x318 ≤ 0 ∧ x318 − x318 ≤ 0 ∧ − x317 + x317 ≤ 0 ∧ x317 − x317 ≤ 0 ∧ − x316 + x316 ≤ 0 ∧ x316 − x316 ≤ 0 ∧ − x315 + x315 ≤ 0 ∧ x315 − x315 ≤ 0 ∧ − x297 + x297 ≤ 0 ∧ x297 − x297 ≤ 0 ∧ − x287 + x287 ≤ 0 ∧ x287 − x287 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x284 + x284 ≤ 0 ∧ x284 − x284 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x229 + x229 ≤ 0 ∧ x229 − x229 ≤ 0 ∧ − x211 + x211 ≤ 0 ∧ x211 − x211 ≤ 0 ∧ − x190 + x190 ≤ 0 ∧ x190 − x190 ≤ 0 ∧ − x177 + x177 ≤ 0 ∧ x177 − x177 ≤ 0 ∧ − x162 + x162 ≤ 0 ∧ x162 − x162 ≤ 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 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 1, 2, 3, 4, 5, 7, 13, 14, 15, 16, 17, 18, 19, 25, 26, 27, 28, 29, 30, 33 using the following ranking functions, which are bounded by −49.

20: 0
10: 0
11: 0
13: 0
15: 0
4: 0
5: 0
6: 0
7: 0
0: 0
1: 0
2: 0
3: 0
14: 0
16: 0
17: 0
18: 0
8: 0
9: 0
19: 0
20: −21
10: −22
11: −23
13: −24
13_var_snapshot: −24
13*: −24
15: −27
4: −28
5: −29
6: −30
7: −31
0: −32
1: −33
2: −34
3: −35
14: −36
14_var_snapshot: −36
14*: −36
16: −39
17: −40
18: −41
8: −42
9: −43
19: −44
19_var_snapshot: −44
19*: −44

4 Location Addition

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

13* 37 13: − x720 + x720 ≤ 0 ∧ x720 − x720 ≤ 0 ∧ − x685 + x685 ≤ 0 ∧ x685 − x685 ≤ 0 ∧ − x684 + x684 ≤ 0 ∧ x684 − x684 ≤ 0 ∧ − x643 + x643 ≤ 0 ∧ x643 − x643 ≤ 0 ∧ − x608 + x608 ≤ 0 ∧ x608 − x608 ≤ 0 ∧ − x607 + x607 ≤ 0 ∧ x607 − x607 ≤ 0 ∧ − x606 + x606 ≤ 0 ∧ x606 − x606 ≤ 0 ∧ − x605 + x605 ≤ 0 ∧ x605 − x605 ≤ 0 ∧ − x604 + x604 ≤ 0 ∧ x604 − x604 ≤ 0 ∧ − x603 + x603 ≤ 0 ∧ x603 − x603 ≤ 0 ∧ − x590 + x590 ≤ 0 ∧ x590 − x590 ≤ 0 ∧ − x589 + x589 ≤ 0 ∧ x589 − x589 ≤ 0 ∧ − x588 + x588 ≤ 0 ∧ x588 − x588 ≤ 0 ∧ − x587 + x587 ≤ 0 ∧ x587 − x587 ≤ 0 ∧ − x586 + x586 ≤ 0 ∧ x586 − x586 ≤ 0 ∧ − x560 + x560 ≤ 0 ∧ x560 − x560 ≤ 0 ∧ − x545 + x545 ≤ 0 ∧ x545 − x545 ≤ 0 ∧ − x544 + x544 ≤ 0 ∧ x544 − x544 ≤ 0 ∧ − x535 + x535 ≤ 0 ∧ x535 − x535 ≤ 0 ∧ − x534 + x534 ≤ 0 ∧ x534 − x534 ≤ 0 ∧ − x524 + x524 ≤ 0 ∧ x524 − x524 ≤ 0 ∧ − x513 + x513 ≤ 0 ∧ x513 − x513 ≤ 0 ∧ − x503 + x503 ≤ 0 ∧ x503 − x503 ≤ 0 ∧ − x427 + x427 ≤ 0 ∧ x427 − x427 ≤ 0 ∧ − x426 + x426 ≤ 0 ∧ x426 − x426 ≤ 0 ∧ − x425 + x425 ≤ 0 ∧ x425 − x425 ≤ 0 ∧ − x387 + x387 ≤ 0 ∧ x387 − x387 ≤ 0 ∧ − x386 + x386 ≤ 0 ∧ x386 − x386 ≤ 0 ∧ − x346 + x346 ≤ 0 ∧ x346 − x346 ≤ 0 ∧ − x345 + x345 ≤ 0 ∧ x345 − x345 ≤ 0 ∧ − x344 + x344 ≤ 0 ∧ x344 − x344 ≤ 0 ∧ − x343 + x343 ≤ 0 ∧ x343 − x343 ≤ 0 ∧ − x342 + x342 ≤ 0 ∧ x342 − x342 ≤ 0 ∧ − x341 + x341 ≤ 0 ∧ x341 − x341 ≤ 0 ∧ − x340 + x340 ≤ 0 ∧ x340 − x340 ≤ 0 ∧ − x339 + x339 ≤ 0 ∧ x339 − x339 ≤ 0 ∧ − x321 + x321 ≤ 0 ∧ x321 − x321 ≤ 0 ∧ − x320 + x320 ≤ 0 ∧ x320 − x320 ≤ 0 ∧ − x319 + x319 ≤ 0 ∧ x319 − x319 ≤ 0 ∧ − x318 + x318 ≤ 0 ∧ x318 − x318 ≤ 0 ∧ − x317 + x317 ≤ 0 ∧ x317 − x317 ≤ 0 ∧ − x316 + x316 ≤ 0 ∧ x316 − x316 ≤ 0 ∧ − x315 + x315 ≤ 0 ∧ x315 − x315 ≤ 0 ∧ − x297 + x297 ≤ 0 ∧ x297 − x297 ≤ 0 ∧ − x287 + x287 ≤ 0 ∧ x287 − x287 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x284 + x284 ≤ 0 ∧ x284 − x284 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x229 + x229 ≤ 0 ∧ x229 − x229 ≤ 0 ∧ − x211 + x211 ≤ 0 ∧ x211 − x211 ≤ 0 ∧ − x190 + x190 ≤ 0 ∧ x190 − x190 ≤ 0 ∧ − x177 + x177 ≤ 0 ∧ x177 − x177 ≤ 0 ∧ − x162 + x162 ≤ 0 ∧ x162 − x162 ≤ 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 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

5 Location Addition

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

13 35 13_var_snapshot: − x720 + x720 ≤ 0 ∧ x720 − x720 ≤ 0 ∧ − x685 + x685 ≤ 0 ∧ x685 − x685 ≤ 0 ∧ − x684 + x684 ≤ 0 ∧ x684 − x684 ≤ 0 ∧ − x643 + x643 ≤ 0 ∧ x643 − x643 ≤ 0 ∧ − x608 + x608 ≤ 0 ∧ x608 − x608 ≤ 0 ∧ − x607 + x607 ≤ 0 ∧ x607 − x607 ≤ 0 ∧ − x606 + x606 ≤ 0 ∧ x606 − x606 ≤ 0 ∧ − x605 + x605 ≤ 0 ∧ x605 − x605 ≤ 0 ∧ − x604 + x604 ≤ 0 ∧ x604 − x604 ≤ 0 ∧ − x603 + x603 ≤ 0 ∧ x603 − x603 ≤ 0 ∧ − x590 + x590 ≤ 0 ∧ x590 − x590 ≤ 0 ∧ − x589 + x589 ≤ 0 ∧ x589 − x589 ≤ 0 ∧ − x588 + x588 ≤ 0 ∧ x588 − x588 ≤ 0 ∧ − x587 + x587 ≤ 0 ∧ x587 − x587 ≤ 0 ∧ − x586 + x586 ≤ 0 ∧ x586 − x586 ≤ 0 ∧ − x560 + x560 ≤ 0 ∧ x560 − x560 ≤ 0 ∧ − x545 + x545 ≤ 0 ∧ x545 − x545 ≤ 0 ∧ − x544 + x544 ≤ 0 ∧ x544 − x544 ≤ 0 ∧ − x535 + x535 ≤ 0 ∧ x535 − x535 ≤ 0 ∧ − x534 + x534 ≤ 0 ∧ x534 − x534 ≤ 0 ∧ − x524 + x524 ≤ 0 ∧ x524 − x524 ≤ 0 ∧ − x513 + x513 ≤ 0 ∧ x513 − x513 ≤ 0 ∧ − x503 + x503 ≤ 0 ∧ x503 − x503 ≤ 0 ∧ − x427 + x427 ≤ 0 ∧ x427 − x427 ≤ 0 ∧ − x426 + x426 ≤ 0 ∧ x426 − x426 ≤ 0 ∧ − x425 + x425 ≤ 0 ∧ x425 − x425 ≤ 0 ∧ − x387 + x387 ≤ 0 ∧ x387 − x387 ≤ 0 ∧ − x386 + x386 ≤ 0 ∧ x386 − x386 ≤ 0 ∧ − x346 + x346 ≤ 0 ∧ x346 − x346 ≤ 0 ∧ − x345 + x345 ≤ 0 ∧ x345 − x345 ≤ 0 ∧ − x344 + x344 ≤ 0 ∧ x344 − x344 ≤ 0 ∧ − x343 + x343 ≤ 0 ∧ x343 − x343 ≤ 0 ∧ − x342 + x342 ≤ 0 ∧ x342 − x342 ≤ 0 ∧ − x341 + x341 ≤ 0 ∧ x341 − x341 ≤ 0 ∧ − x340 + x340 ≤ 0 ∧ x340 − x340 ≤ 0 ∧ − x339 + x339 ≤ 0 ∧ x339 − x339 ≤ 0 ∧ − x321 + x321 ≤ 0 ∧ x321 − x321 ≤ 0 ∧ − x320 + x320 ≤ 0 ∧ x320 − x320 ≤ 0 ∧ − x319 + x319 ≤ 0 ∧ x319 − x319 ≤ 0 ∧ − x318 + x318 ≤ 0 ∧ x318 − x318 ≤ 0 ∧ − x317 + x317 ≤ 0 ∧ x317 − x317 ≤ 0 ∧ − x316 + x316 ≤ 0 ∧ x316 − x316 ≤ 0 ∧ − x315 + x315 ≤ 0 ∧ x315 − x315 ≤ 0 ∧ − x297 + x297 ≤ 0 ∧ x297 − x297 ≤ 0 ∧ − x287 + x287 ≤ 0 ∧ x287 − x287 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x284 + x284 ≤ 0 ∧ x284 − x284 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x229 + x229 ≤ 0 ∧ x229 − x229 ≤ 0 ∧ − x211 + x211 ≤ 0 ∧ x211 − x211 ≤ 0 ∧ − x190 + x190 ≤ 0 ∧ x190 − x190 ≤ 0 ∧ − x177 + x177 ≤ 0 ∧ x177 − x177 ≤ 0 ∧ − x162 + x162 ≤ 0 ∧ x162 − x162 ≤ 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 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

6 Location Addition

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

14* 44 14: − x720 + x720 ≤ 0 ∧ x720 − x720 ≤ 0 ∧ − x685 + x685 ≤ 0 ∧ x685 − x685 ≤ 0 ∧ − x684 + x684 ≤ 0 ∧ x684 − x684 ≤ 0 ∧ − x643 + x643 ≤ 0 ∧ x643 − x643 ≤ 0 ∧ − x608 + x608 ≤ 0 ∧ x608 − x608 ≤ 0 ∧ − x607 + x607 ≤ 0 ∧ x607 − x607 ≤ 0 ∧ − x606 + x606 ≤ 0 ∧ x606 − x606 ≤ 0 ∧ − x605 + x605 ≤ 0 ∧ x605 − x605 ≤ 0 ∧ − x604 + x604 ≤ 0 ∧ x604 − x604 ≤ 0 ∧ − x603 + x603 ≤ 0 ∧ x603 − x603 ≤ 0 ∧ − x590 + x590 ≤ 0 ∧ x590 − x590 ≤ 0 ∧ − x589 + x589 ≤ 0 ∧ x589 − x589 ≤ 0 ∧ − x588 + x588 ≤ 0 ∧ x588 − x588 ≤ 0 ∧ − x587 + x587 ≤ 0 ∧ x587 − x587 ≤ 0 ∧ − x586 + x586 ≤ 0 ∧ x586 − x586 ≤ 0 ∧ − x560 + x560 ≤ 0 ∧ x560 − x560 ≤ 0 ∧ − x545 + x545 ≤ 0 ∧ x545 − x545 ≤ 0 ∧ − x544 + x544 ≤ 0 ∧ x544 − x544 ≤ 0 ∧ − x535 + x535 ≤ 0 ∧ x535 − x535 ≤ 0 ∧ − x534 + x534 ≤ 0 ∧ x534 − x534 ≤ 0 ∧ − x524 + x524 ≤ 0 ∧ x524 − x524 ≤ 0 ∧ − x513 + x513 ≤ 0 ∧ x513 − x513 ≤ 0 ∧ − x503 + x503 ≤ 0 ∧ x503 − x503 ≤ 0 ∧ − x427 + x427 ≤ 0 ∧ x427 − x427 ≤ 0 ∧ − x426 + x426 ≤ 0 ∧ x426 − x426 ≤ 0 ∧ − x425 + x425 ≤ 0 ∧ x425 − x425 ≤ 0 ∧ − x387 + x387 ≤ 0 ∧ x387 − x387 ≤ 0 ∧ − x386 + x386 ≤ 0 ∧ x386 − x386 ≤ 0 ∧ − x346 + x346 ≤ 0 ∧ x346 − x346 ≤ 0 ∧ − x345 + x345 ≤ 0 ∧ x345 − x345 ≤ 0 ∧ − x344 + x344 ≤ 0 ∧ x344 − x344 ≤ 0 ∧ − x343 + x343 ≤ 0 ∧ x343 − x343 ≤ 0 ∧ − x342 + x342 ≤ 0 ∧ x342 − x342 ≤ 0 ∧ − x341 + x341 ≤ 0 ∧ x341 − x341 ≤ 0 ∧ − x340 + x340 ≤ 0 ∧ x340 − x340 ≤ 0 ∧ − x339 + x339 ≤ 0 ∧ x339 − x339 ≤ 0 ∧ − x321 + x321 ≤ 0 ∧ x321 − x321 ≤ 0 ∧ − x320 + x320 ≤ 0 ∧ x320 − x320 ≤ 0 ∧ − x319 + x319 ≤ 0 ∧ x319 − x319 ≤ 0 ∧ − x318 + x318 ≤ 0 ∧ x318 − x318 ≤ 0 ∧ − x317 + x317 ≤ 0 ∧ x317 − x317 ≤ 0 ∧ − x316 + x316 ≤ 0 ∧ x316 − x316 ≤ 0 ∧ − x315 + x315 ≤ 0 ∧ x315 − x315 ≤ 0 ∧ − x297 + x297 ≤ 0 ∧ x297 − x297 ≤ 0 ∧ − x287 + x287 ≤ 0 ∧ x287 − x287 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x284 + x284 ≤ 0 ∧ x284 − x284 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x229 + x229 ≤ 0 ∧ x229 − x229 ≤ 0 ∧ − x211 + x211 ≤ 0 ∧ x211 − x211 ≤ 0 ∧ − x190 + x190 ≤ 0 ∧ x190 − x190 ≤ 0 ∧ − x177 + x177 ≤ 0 ∧ x177 − x177 ≤ 0 ∧ − x162 + x162 ≤ 0 ∧ x162 − x162 ≤ 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 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

7 Location Addition

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

14 42 14_var_snapshot: − x720 + x720 ≤ 0 ∧ x720 − x720 ≤ 0 ∧ − x685 + x685 ≤ 0 ∧ x685 − x685 ≤ 0 ∧ − x684 + x684 ≤ 0 ∧ x684 − x684 ≤ 0 ∧ − x643 + x643 ≤ 0 ∧ x643 − x643 ≤ 0 ∧ − x608 + x608 ≤ 0 ∧ x608 − x608 ≤ 0 ∧ − x607 + x607 ≤ 0 ∧ x607 − x607 ≤ 0 ∧ − x606 + x606 ≤ 0 ∧ x606 − x606 ≤ 0 ∧ − x605 + x605 ≤ 0 ∧ x605 − x605 ≤ 0 ∧ − x604 + x604 ≤ 0 ∧ x604 − x604 ≤ 0 ∧ − x603 + x603 ≤ 0 ∧ x603 − x603 ≤ 0 ∧ − x590 + x590 ≤ 0 ∧ x590 − x590 ≤ 0 ∧ − x589 + x589 ≤ 0 ∧ x589 − x589 ≤ 0 ∧ − x588 + x588 ≤ 0 ∧ x588 − x588 ≤ 0 ∧ − x587 + x587 ≤ 0 ∧ x587 − x587 ≤ 0 ∧ − x586 + x586 ≤ 0 ∧ x586 − x586 ≤ 0 ∧ − x560 + x560 ≤ 0 ∧ x560 − x560 ≤ 0 ∧ − x545 + x545 ≤ 0 ∧ x545 − x545 ≤ 0 ∧ − x544 + x544 ≤ 0 ∧ x544 − x544 ≤ 0 ∧ − x535 + x535 ≤ 0 ∧ x535 − x535 ≤ 0 ∧ − x534 + x534 ≤ 0 ∧ x534 − x534 ≤ 0 ∧ − x524 + x524 ≤ 0 ∧ x524 − x524 ≤ 0 ∧ − x513 + x513 ≤ 0 ∧ x513 − x513 ≤ 0 ∧ − x503 + x503 ≤ 0 ∧ x503 − x503 ≤ 0 ∧ − x427 + x427 ≤ 0 ∧ x427 − x427 ≤ 0 ∧ − x426 + x426 ≤ 0 ∧ x426 − x426 ≤ 0 ∧ − x425 + x425 ≤ 0 ∧ x425 − x425 ≤ 0 ∧ − x387 + x387 ≤ 0 ∧ x387 − x387 ≤ 0 ∧ − x386 + x386 ≤ 0 ∧ x386 − x386 ≤ 0 ∧ − x346 + x346 ≤ 0 ∧ x346 − x346 ≤ 0 ∧ − x345 + x345 ≤ 0 ∧ x345 − x345 ≤ 0 ∧ − x344 + x344 ≤ 0 ∧ x344 − x344 ≤ 0 ∧ − x343 + x343 ≤ 0 ∧ x343 − x343 ≤ 0 ∧ − x342 + x342 ≤ 0 ∧ x342 − x342 ≤ 0 ∧ − x341 + x341 ≤ 0 ∧ x341 − x341 ≤ 0 ∧ − x340 + x340 ≤ 0 ∧ x340 − x340 ≤ 0 ∧ − x339 + x339 ≤ 0 ∧ x339 − x339 ≤ 0 ∧ − x321 + x321 ≤ 0 ∧ x321 − x321 ≤ 0 ∧ − x320 + x320 ≤ 0 ∧ x320 − x320 ≤ 0 ∧ − x319 + x319 ≤ 0 ∧ x319 − x319 ≤ 0 ∧ − x318 + x318 ≤ 0 ∧ x318 − x318 ≤ 0 ∧ − x317 + x317 ≤ 0 ∧ x317 − x317 ≤ 0 ∧ − x316 + x316 ≤ 0 ∧ x316 − x316 ≤ 0 ∧ − x315 + x315 ≤ 0 ∧ x315 − x315 ≤ 0 ∧ − x297 + x297 ≤ 0 ∧ x297 − x297 ≤ 0 ∧ − x287 + x287 ≤ 0 ∧ x287 − x287 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x284 + x284 ≤ 0 ∧ x284 − x284 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x229 + x229 ≤ 0 ∧ x229 − x229 ≤ 0 ∧ − x211 + x211 ≤ 0 ∧ x211 − x211 ≤ 0 ∧ − x190 + x190 ≤ 0 ∧ x190 − x190 ≤ 0 ∧ − x177 + x177 ≤ 0 ∧ x177 − x177 ≤ 0 ∧ − x162 + x162 ≤ 0 ∧ x162 − x162 ≤ 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 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

8 Location Addition

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

19* 51 19: − x720 + x720 ≤ 0 ∧ x720 − x720 ≤ 0 ∧ − x685 + x685 ≤ 0 ∧ x685 − x685 ≤ 0 ∧ − x684 + x684 ≤ 0 ∧ x684 − x684 ≤ 0 ∧ − x643 + x643 ≤ 0 ∧ x643 − x643 ≤ 0 ∧ − x608 + x608 ≤ 0 ∧ x608 − x608 ≤ 0 ∧ − x607 + x607 ≤ 0 ∧ x607 − x607 ≤ 0 ∧ − x606 + x606 ≤ 0 ∧ x606 − x606 ≤ 0 ∧ − x605 + x605 ≤ 0 ∧ x605 − x605 ≤ 0 ∧ − x604 + x604 ≤ 0 ∧ x604 − x604 ≤ 0 ∧ − x603 + x603 ≤ 0 ∧ x603 − x603 ≤ 0 ∧ − x590 + x590 ≤ 0 ∧ x590 − x590 ≤ 0 ∧ − x589 + x589 ≤ 0 ∧ x589 − x589 ≤ 0 ∧ − x588 + x588 ≤ 0 ∧ x588 − x588 ≤ 0 ∧ − x587 + x587 ≤ 0 ∧ x587 − x587 ≤ 0 ∧ − x586 + x586 ≤ 0 ∧ x586 − x586 ≤ 0 ∧ − x560 + x560 ≤ 0 ∧ x560 − x560 ≤ 0 ∧ − x545 + x545 ≤ 0 ∧ x545 − x545 ≤ 0 ∧ − x544 + x544 ≤ 0 ∧ x544 − x544 ≤ 0 ∧ − x535 + x535 ≤ 0 ∧ x535 − x535 ≤ 0 ∧ − x534 + x534 ≤ 0 ∧ x534 − x534 ≤ 0 ∧ − x524 + x524 ≤ 0 ∧ x524 − x524 ≤ 0 ∧ − x513 + x513 ≤ 0 ∧ x513 − x513 ≤ 0 ∧ − x503 + x503 ≤ 0 ∧ x503 − x503 ≤ 0 ∧ − x427 + x427 ≤ 0 ∧ x427 − x427 ≤ 0 ∧ − x426 + x426 ≤ 0 ∧ x426 − x426 ≤ 0 ∧ − x425 + x425 ≤ 0 ∧ x425 − x425 ≤ 0 ∧ − x387 + x387 ≤ 0 ∧ x387 − x387 ≤ 0 ∧ − x386 + x386 ≤ 0 ∧ x386 − x386 ≤ 0 ∧ − x346 + x346 ≤ 0 ∧ x346 − x346 ≤ 0 ∧ − x345 + x345 ≤ 0 ∧ x345 − x345 ≤ 0 ∧ − x344 + x344 ≤ 0 ∧ x344 − x344 ≤ 0 ∧ − x343 + x343 ≤ 0 ∧ x343 − x343 ≤ 0 ∧ − x342 + x342 ≤ 0 ∧ x342 − x342 ≤ 0 ∧ − x341 + x341 ≤ 0 ∧ x341 − x341 ≤ 0 ∧ − x340 + x340 ≤ 0 ∧ x340 − x340 ≤ 0 ∧ − x339 + x339 ≤ 0 ∧ x339 − x339 ≤ 0 ∧ − x321 + x321 ≤ 0 ∧ x321 − x321 ≤ 0 ∧ − x320 + x320 ≤ 0 ∧ x320 − x320 ≤ 0 ∧ − x319 + x319 ≤ 0 ∧ x319 − x319 ≤ 0 ∧ − x318 + x318 ≤ 0 ∧ x318 − x318 ≤ 0 ∧ − x317 + x317 ≤ 0 ∧ x317 − x317 ≤ 0 ∧ − x316 + x316 ≤ 0 ∧ x316 − x316 ≤ 0 ∧ − x315 + x315 ≤ 0 ∧ x315 − x315 ≤ 0 ∧ − x297 + x297 ≤ 0 ∧ x297 − x297 ≤ 0 ∧ − x287 + x287 ≤ 0 ∧ x287 − x287 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x284 + x284 ≤ 0 ∧ x284 − x284 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x229 + x229 ≤ 0 ∧ x229 − x229 ≤ 0 ∧ − x211 + x211 ≤ 0 ∧ x211 − x211 ≤ 0 ∧ − x190 + x190 ≤ 0 ∧ x190 − x190 ≤ 0 ∧ − x177 + x177 ≤ 0 ∧ x177 − x177 ≤ 0 ∧ − x162 + x162 ≤ 0 ∧ x162 − x162 ≤ 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 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

9 Location Addition

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

19 49 19_var_snapshot: − x720 + x720 ≤ 0 ∧ x720 − x720 ≤ 0 ∧ − x685 + x685 ≤ 0 ∧ x685 − x685 ≤ 0 ∧ − x684 + x684 ≤ 0 ∧ x684 − x684 ≤ 0 ∧ − x643 + x643 ≤ 0 ∧ x643 − x643 ≤ 0 ∧ − x608 + x608 ≤ 0 ∧ x608 − x608 ≤ 0 ∧ − x607 + x607 ≤ 0 ∧ x607 − x607 ≤ 0 ∧ − x606 + x606 ≤ 0 ∧ x606 − x606 ≤ 0 ∧ − x605 + x605 ≤ 0 ∧ x605 − x605 ≤ 0 ∧ − x604 + x604 ≤ 0 ∧ x604 − x604 ≤ 0 ∧ − x603 + x603 ≤ 0 ∧ x603 − x603 ≤ 0 ∧ − x590 + x590 ≤ 0 ∧ x590 − x590 ≤ 0 ∧ − x589 + x589 ≤ 0 ∧ x589 − x589 ≤ 0 ∧ − x588 + x588 ≤ 0 ∧ x588 − x588 ≤ 0 ∧ − x587 + x587 ≤ 0 ∧ x587 − x587 ≤ 0 ∧ − x586 + x586 ≤ 0 ∧ x586 − x586 ≤ 0 ∧ − x560 + x560 ≤ 0 ∧ x560 − x560 ≤ 0 ∧ − x545 + x545 ≤ 0 ∧ x545 − x545 ≤ 0 ∧ − x544 + x544 ≤ 0 ∧ x544 − x544 ≤ 0 ∧ − x535 + x535 ≤ 0 ∧ x535 − x535 ≤ 0 ∧ − x534 + x534 ≤ 0 ∧ x534 − x534 ≤ 0 ∧ − x524 + x524 ≤ 0 ∧ x524 − x524 ≤ 0 ∧ − x513 + x513 ≤ 0 ∧ x513 − x513 ≤ 0 ∧ − x503 + x503 ≤ 0 ∧ x503 − x503 ≤ 0 ∧ − x427 + x427 ≤ 0 ∧ x427 − x427 ≤ 0 ∧ − x426 + x426 ≤ 0 ∧ x426 − x426 ≤ 0 ∧ − x425 + x425 ≤ 0 ∧ x425 − x425 ≤ 0 ∧ − x387 + x387 ≤ 0 ∧ x387 − x387 ≤ 0 ∧ − x386 + x386 ≤ 0 ∧ x386 − x386 ≤ 0 ∧ − x346 + x346 ≤ 0 ∧ x346 − x346 ≤ 0 ∧ − x345 + x345 ≤ 0 ∧ x345 − x345 ≤ 0 ∧ − x344 + x344 ≤ 0 ∧ x344 − x344 ≤ 0 ∧ − x343 + x343 ≤ 0 ∧ x343 − x343 ≤ 0 ∧ − x342 + x342 ≤ 0 ∧ x342 − x342 ≤ 0 ∧ − x341 + x341 ≤ 0 ∧ x341 − x341 ≤ 0 ∧ − x340 + x340 ≤ 0 ∧ x340 − x340 ≤ 0 ∧ − x339 + x339 ≤ 0 ∧ x339 − x339 ≤ 0 ∧ − x321 + x321 ≤ 0 ∧ x321 − x321 ≤ 0 ∧ − x320 + x320 ≤ 0 ∧ x320 − x320 ≤ 0 ∧ − x319 + x319 ≤ 0 ∧ x319 − x319 ≤ 0 ∧ − x318 + x318 ≤ 0 ∧ x318 − x318 ≤ 0 ∧ − x317 + x317 ≤ 0 ∧ x317 − x317 ≤ 0 ∧ − x316 + x316 ≤ 0 ∧ x316 − x316 ≤ 0 ∧ − x315 + x315 ≤ 0 ∧ x315 − x315 ≤ 0 ∧ − x297 + x297 ≤ 0 ∧ x297 − x297 ≤ 0 ∧ − x287 + x287 ≤ 0 ∧ x287 − x287 ≤ 0 ∧ − x285 + x285 ≤ 0 ∧ x285 − x285 ≤ 0 ∧ − x284 + x284 ≤ 0 ∧ x284 − x284 ≤ 0 ∧ − x267 + x267 ≤ 0 ∧ x267 − x267 ≤ 0 ∧ − x248 + x248 ≤ 0 ∧ x248 − x248 ≤ 0 ∧ − x247 + x247 ≤ 0 ∧ x247 − x247 ≤ 0 ∧ − x229 + x229 ≤ 0 ∧ x229 − x229 ≤ 0 ∧ − x211 + x211 ≤ 0 ∧ x211 − x211 ≤ 0 ∧ − x190 + x190 ≤ 0 ∧ x190 − x190 ≤ 0 ∧ − x177 + x177 ≤ 0 ∧ x177 − x177 ≤ 0 ∧ − x162 + x162 ≤ 0 ∧ x162 − x162 ≤ 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 ∧ − arg29P + arg29P ≤ 0 ∧ arg29P − arg29P ≤ 0 ∧ − arg29 + arg29 ≤ 0 ∧ arg29 − arg29 ≤ 0 ∧ − arg28P + arg28P ≤ 0 ∧ arg28P − arg28P ≤ 0 ∧ − arg28 + arg28 ≤ 0 ∧ arg28 − arg28 ≤ 0 ∧ − arg27P + arg27P ≤ 0 ∧ arg27P − arg27P ≤ 0 ∧ − arg27 + arg27 ≤ 0 ∧ arg27 − arg27 ≤ 0 ∧ − arg26P + arg26P ≤ 0 ∧ arg26P − arg26P ≤ 0 ∧ − arg26 + arg26 ≤ 0 ∧ arg26 − arg26 ≤ 0 ∧ − arg25P + arg25P ≤ 0 ∧ arg25P − arg25P ≤ 0 ∧ − arg25 + arg25 ≤ 0 ∧ arg25 − arg25 ≤ 0 ∧ − arg24P + arg24P ≤ 0 ∧ arg24P − arg24P ≤ 0 ∧ − arg24 + arg24 ≤ 0 ∧ arg24 − arg24 ≤ 0 ∧ − arg23P + arg23P ≤ 0 ∧ arg23P − arg23P ≤ 0 ∧ − arg23 + arg23 ≤ 0 ∧ arg23 − arg23 ≤ 0 ∧ − arg22P + arg22P ≤ 0 ∧ arg22P − arg22P ≤ 0 ∧ − arg22 + arg22 ≤ 0 ∧ arg22 − arg22 ≤ 0 ∧ − arg21P + arg21P ≤ 0 ∧ arg21P − arg21P ≤ 0 ∧ − arg21 + arg21 ≤ 0 ∧ arg21 − arg21 ≤ 0 ∧ − arg20P + arg20P ≤ 0 ∧ arg20P − arg20P ≤ 0 ∧ − arg20 + arg20 ≤ 0 ∧ arg20 − arg20 ≤ 0 ∧ − arg2 + arg2 ≤ 0 ∧ arg2 − arg2 ≤ 0 ∧ − arg1P + arg1P ≤ 0 ∧ arg1P − arg1P ≤ 0 ∧ − arg19P + arg19P ≤ 0 ∧ arg19P − arg19P ≤ 0 ∧ − arg19 + arg19 ≤ 0 ∧ arg19 − arg19 ≤ 0 ∧ − arg18P + arg18P ≤ 0 ∧ arg18P − arg18P ≤ 0 ∧ − arg18 + arg18 ≤ 0 ∧ arg18 − arg18 ≤ 0 ∧ − arg17P + arg17P ≤ 0 ∧ arg17P − arg17P ≤ 0 ∧ − arg17 + arg17 ≤ 0 ∧ arg17 − arg17 ≤ 0 ∧ − arg16P + arg16P ≤ 0 ∧ arg16P − arg16P ≤ 0 ∧ − arg16 + arg16 ≤ 0 ∧ arg16 − arg16 ≤ 0 ∧ − arg15P + arg15P ≤ 0 ∧ arg15P − arg15P ≤ 0 ∧ − arg15 + arg15 ≤ 0 ∧ arg15 − arg15 ≤ 0 ∧ − arg14P + arg14P ≤ 0 ∧ arg14P − arg14P ≤ 0 ∧ − arg14 + arg14 ≤ 0 ∧ arg14 − arg14 ≤ 0 ∧ − arg13P + arg13P ≤ 0 ∧ arg13P − arg13P ≤ 0 ∧ − arg13 + arg13 ≤ 0 ∧ arg13 − arg13 ≤ 0 ∧ − arg12P + arg12P ≤ 0 ∧ arg12P − arg12P ≤ 0 ∧ − arg12 + arg12 ≤ 0 ∧ arg12 − arg12 ≤ 0 ∧ − arg11P + arg11P ≤ 0 ∧ arg11P − arg11P ≤ 0 ∧ − arg11 + arg11 ≤ 0 ∧ arg11 − arg11 ≤ 0 ∧ − arg10P + arg10P ≤ 0 ∧ arg10P − arg10P ≤ 0 ∧ − arg10 + arg10 ≤ 0 ∧ arg10 − arg10 ≤ 0 ∧ − arg1 + arg1 ≤ 0 ∧ arg1 − arg1 ≤ 0

10 SCC Decomposition

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

10.1 SCC Subproblem 1/3

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

10.1.1 Transition Removal

We remove transitions 8, 9, 10, 11, 12 using the following ranking functions, which are bounded by 2.

13: 1 + 3⋅arg3
13_var_snapshot: 3⋅arg3
13*: 2 + 3⋅arg3

10.1.2 Transition Removal

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

13: 0
13_var_snapshot: −1
13*: arg1P

10.1.3 Splitting Cut-Point Transitions

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

10.1.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 34.

10.1.3.1.1 Splitting Cut-Point Transitions

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

10.2 SCC Subproblem 2/3

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

10.2.1 Transition Removal

We remove transitions 20, 21, 22, 23, 24 using the following ranking functions, which are bounded by −3.

14: −1 − 3⋅arg2 + 3⋅arg3
14_var_snapshot: −2 − 3⋅arg2 + 3⋅arg3
14*: −3⋅arg2 + 3⋅arg3

10.2.2 Transition Removal

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

14: 0
14_var_snapshot: −1
14*: 1

10.2.3 Splitting Cut-Point Transitions

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

10.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 41.

10.2.3.1.1 Splitting Cut-Point Transitions

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

10.3 SCC Subproblem 3/3

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

10.3.1 Transition Removal

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

19: 1
19_var_snapshot: 0
19*: 2

10.3.2 Transition Removal

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

19: 0
19_var_snapshot: arg10
19*: 0

10.3.3 Splitting Cut-Point Transitions

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

10.3.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 48.

10.3.3.1.1 Splitting Cut-Point Transitions

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

Tool configuration

T2Cert