LTS Termination Proof

by T2Cert

Input

Integer Transition System
• Initial Location: 31

Proof

The following invariants are asserted.

 0: TRUE 1: head_29_post ≤ 0 ∧ − head_29_post ≤ 0 ∧ i_27_post ≤ 0 ∧ − i_27_post ≤ 0 ∧ head_29_0 ≤ 0 ∧ − head_29_0 ≤ 0 ∧ i_27_0 ≤ 0 ∧ − i_27_0 ≤ 0 2: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 3: TRUE 4: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 5: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 6: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 7: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 8: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 9: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 18: −1 + i_27_post ≤ 0 ∧ 1 − i_27_post ≤ 0 ∧ −1 + i_27_0 ≤ 0 ∧ 1 − i_27_0 ≤ 0 ∧ 1 − length_26_0 ≤ 0 19: y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 20: y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 21: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ x_20_0 ≤ 0 ∧ − x_20_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 22: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ x_20_0 ≤ 0 ∧ − x_20_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 23: −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 24: 2 − length_26_0 ≤ 0 25: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 26: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 27: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 28: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 29: − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 30: 2 − length_26_0 ≤ 0 31: TRUE

The invariants are proved as follows.

IMPACT Invariant Proof

• nodes (location) invariant:  0 (0) TRUE 1 (1) head_29_post ≤ 0 ∧ − head_29_post ≤ 0 ∧ i_27_post ≤ 0 ∧ − i_27_post ≤ 0 ∧ head_29_0 ≤ 0 ∧ − head_29_0 ≤ 0 ∧ i_27_0 ≤ 0 ∧ − i_27_0 ≤ 0 2 (2) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 3 (3) TRUE 4 (4) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 5 (5) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 6 (6) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 7 (7) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 8 (8) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 ∧ − a_139_0 ≤ 0 9 (9) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 18 (18) −1 + i_27_post ≤ 0 ∧ 1 − i_27_post ≤ 0 ∧ −1 + i_27_0 ≤ 0 ∧ 1 − i_27_0 ≤ 0 ∧ 1 − length_26_0 ≤ 0 19 (19) y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 20 (20) y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 21 (21) −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ x_20_0 ≤ 0 ∧ − x_20_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 22 (22) −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ x_20_0 ≤ 0 ∧ − x_20_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 23 (23) −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0 ∧ −1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ 1 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 24 (24) 2 − length_26_0 ≤ 0 25 (25) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 26 (26) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 27 (27) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 28 (28) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 29 (29) − i_27_post ≤ 0 ∧ − i_27_0 ≤ 0 ∧ y_19_post ≤ 0 ∧ − y_19_post ≤ 0 ∧ ct_17_1 ≤ 0 ∧ − ct_17_1 ≤ 0 ∧ 2 − result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0 ∧ ct_17_0 ≤ 0 ∧ − ct_17_0 ≤ 0 ∧ y_19_0 ≤ 0 ∧ − y_19_0 ≤ 0 30 (30) 2 − length_26_0 ≤ 0 31 (31) TRUE
• initial node: 31
• cover edges:
• transition edges:  0 0 1 1 33 3 1 34 18 2 1 3 2 2 4 4 3 5 5 4 6 6 5 7 7 6 8 8 7 9 9 8 2 18 18 19 18 24 24 19 19 20 20 20 21 21 21 22 22 22 23 23 23 3 24 25 25 24 31 30 25 26 26 26 27 27 27 28 28 28 29 29 29 30 2 30 32 24 31 35 0

2 Switch to Cooperation Termination Proof

We consider the following cutpoint-transitions:
and for every transition t, a duplicate t is considered.

3 Transition Removal

We remove transitions 0, 1, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 33, 34, 35 using the following ranking functions, which are bounded by −41.

 31: 0 0: 0 1: 0 18: 0 19: 0 20: 0 21: 0 22: 0 23: 0 24: 0 30: 0 25: 0 26: 0 27: 0 28: 0 29: 0 2: 0 4: 0 5: 0 6: 0 7: 0 8: 0 9: 0 3: 0 31: −18 0: −19 1: −20 18: −21 19: −22 20: −23 21: −24 22: −25 23: −26 24: −27 30: −27 24_var_snapshot: −27 24*: −27 25: −30 26: −31 27: −32 28: −33 29: −34 2: −35 4: −35 5: −35 6: −35 7: −35 8: −35 9: −35 2_var_snapshot: −35 2*: −35 3: −39
Hints:
 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 6 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 8 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 18 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

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

2* 39 2: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_postresult_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_84_post + rcd_84_post ≤ 0rcd_84_postrcd_84_post ≤ 0rcd_84_0 + rcd_84_0 ≤ 0rcd_84_0rcd_84_0 ≤ 0rcd_54_post + rcd_54_post ≤ 0rcd_54_postrcd_54_post ≤ 0rcd_54_0 + rcd_54_0 ≤ 0rcd_54_0rcd_54_0 ≤ 0r_35_post + r_35_post ≤ 0r_35_postr_35_post ≤ 0r_35_0 + r_35_0 ≤ 0r_35_0r_35_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_26_post + length_26_post ≤ 0length_26_postlength_26_post ≤ 0length_26_0 + length_26_0 ≤ 0length_26_0length_26_0 ≤ 0i_90_post + i_90_post ≤ 0i_90_posti_90_post ≤ 0i_90_0 + i_90_0 ≤ 0i_90_0i_90_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_162_post + a_162_post ≤ 0a_162_posta_162_post ≤ 0a_162_0 + a_162_0 ≤ 0a_162_0a_162_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0a_117_post + a_117_post ≤ 0a_117_posta_117_post ≤ 0a_117_0 + a_117_0 ≤ 0a_117_0a_117_0 ≤ 0

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

2 37 2_var_snapshot: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_postresult_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_84_post + rcd_84_post ≤ 0rcd_84_postrcd_84_post ≤ 0rcd_84_0 + rcd_84_0 ≤ 0rcd_84_0rcd_84_0 ≤ 0rcd_54_post + rcd_54_post ≤ 0rcd_54_postrcd_54_post ≤ 0rcd_54_0 + rcd_54_0 ≤ 0rcd_54_0rcd_54_0 ≤ 0r_35_post + r_35_post ≤ 0r_35_postr_35_post ≤ 0r_35_0 + r_35_0 ≤ 0r_35_0r_35_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_26_post + length_26_post ≤ 0length_26_postlength_26_post ≤ 0length_26_0 + length_26_0 ≤ 0length_26_0length_26_0 ≤ 0i_90_post + i_90_post ≤ 0i_90_posti_90_post ≤ 0i_90_0 + i_90_0 ≤ 0i_90_0i_90_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_162_post + a_162_post ≤ 0a_162_posta_162_post ≤ 0a_162_0 + a_162_0 ≤ 0a_162_0a_162_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0a_117_post + a_117_post ≤ 0a_117_posta_117_post ≤ 0a_117_0 + a_117_0 ≤ 0a_117_0a_117_0 ≤ 0

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

24* 46 24: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_postresult_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_84_post + rcd_84_post ≤ 0rcd_84_postrcd_84_post ≤ 0rcd_84_0 + rcd_84_0 ≤ 0rcd_84_0rcd_84_0 ≤ 0rcd_54_post + rcd_54_post ≤ 0rcd_54_postrcd_54_post ≤ 0rcd_54_0 + rcd_54_0 ≤ 0rcd_54_0rcd_54_0 ≤ 0r_35_post + r_35_post ≤ 0r_35_postr_35_post ≤ 0r_35_0 + r_35_0 ≤ 0r_35_0r_35_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_26_post + length_26_post ≤ 0length_26_postlength_26_post ≤ 0length_26_0 + length_26_0 ≤ 0length_26_0length_26_0 ≤ 0i_90_post + i_90_post ≤ 0i_90_posti_90_post ≤ 0i_90_0 + i_90_0 ≤ 0i_90_0i_90_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_162_post + a_162_post ≤ 0a_162_posta_162_post ≤ 0a_162_0 + a_162_0 ≤ 0a_162_0a_162_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0a_117_post + a_117_post ≤ 0a_117_posta_117_post ≤ 0a_117_0 + a_117_0 ≤ 0a_117_0a_117_0 ≤ 0

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

24 44 24_var_snapshot: y_19_post + y_19_post ≤ 0y_19_posty_19_post ≤ 0y_19_2 + y_19_2 ≤ 0y_19_2y_19_2 ≤ 0y_19_1 + y_19_1 ≤ 0y_19_1y_19_1 ≤ 0y_19_0 + y_19_0 ≤ 0y_19_0y_19_0 ≤ 0x_SLAM_f_18_post + x_SLAM_f_18_post ≤ 0x_SLAM_f_18_postx_SLAM_f_18_post ≤ 0x_SLAM_f_18_2 + x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_2x_SLAM_f_18_2 ≤ 0x_SLAM_f_18_1 + x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_1x_SLAM_f_18_1 ≤ 0x_SLAM_f_18_0 + x_SLAM_f_18_0 ≤ 0x_SLAM_f_18_0x_SLAM_f_18_0 ≤ 0x_20_post + x_20_post ≤ 0x_20_postx_20_post ≤ 0x_20_2 + x_20_2 ≤ 0x_20_2x_20_2 ≤ 0x_20_1 + x_20_1 ≤ 0x_20_1x_20_1 ≤ 0x_20_0 + x_20_0 ≤ 0x_20_0x_20_0 ≤ 0x_16_post + x_16_post ≤ 0x_16_postx_16_post ≤ 0x_16_1 + x_16_1 ≤ 0x_16_1x_16_1 ≤ 0x_16_0 + x_16_0 ≤ 0x_16_0x_16_0 ≤ 0tmp_31_post + tmp_31_post ≤ 0tmp_31_posttmp_31_post ≤ 0tmp_31_0 + tmp_31_0 ≤ 0tmp_31_0tmp_31_0 ≤ 0temp_32_post + temp_32_post ≤ 0temp_32_posttemp_32_post ≤ 0temp_32_0 + temp_32_0 ≤ 0temp_32_0temp_32_0 ≤ 0temp0_28_post + temp0_28_post ≤ 0temp0_28_posttemp0_28_post ≤ 0temp0_28_1 + temp0_28_1 ≤ 0temp0_28_1temp0_28_1 ≤ 0temp0_28_0 + temp0_28_0 ≤ 0temp0_28_0temp0_28_0 ≤ 0temp0_15_0 + temp0_15_0 ≤ 0temp0_15_0temp0_15_0 ≤ 0t_23_post + t_23_post ≤ 0t_23_postt_23_post ≤ 0t_23_1 + t_23_1 ≤ 0t_23_1t_23_1 ≤ 0t_23_0 + t_23_0 ≤ 0t_23_0t_23_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_post + result_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_postresult_dot_nondet_sdv_special_RETURN_VALUE_13_post ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1 + result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_1result_dot_nondet_sdv_special_RETURN_VALUE_13_1 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 + result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_nondet_sdv_special_RETURN_VALUE_13_0result_dot_nondet_sdv_special_RETURN_VALUE_13_0 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_postresult_dot_SLL_create_sdv_special_RETURN_VALUE_14_post ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1result_dot_SLL_create_sdv_special_RETURN_VALUE_14_1 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 + result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0result_dot_SLL_create_sdv_special_RETURN_VALUE_14_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_postresult_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_post ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 + result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0result_dot_SLAyer_malloc_sdv_special_RETURN_VALUE_30_0 ≤ 0result_11_post + result_11_post ≤ 0result_11_postresult_11_post ≤ 0result_11_2 + result_11_2 ≤ 0result_11_2result_11_2 ≤ 0result_11_1 + result_11_1 ≤ 0result_11_1result_11_1 ≤ 0result_11_0 + result_11_0 ≤ 0result_11_0result_11_0 ≤ 0rcd_84_post + rcd_84_post ≤ 0rcd_84_postrcd_84_post ≤ 0rcd_84_0 + rcd_84_0 ≤ 0rcd_84_0rcd_84_0 ≤ 0rcd_54_post + rcd_54_post ≤ 0rcd_54_postrcd_54_post ≤ 0rcd_54_0 + rcd_54_0 ≤ 0rcd_54_0rcd_54_0 ≤ 0r_35_post + r_35_post ≤ 0r_35_postr_35_post ≤ 0r_35_0 + r_35_0 ≤ 0r_35_0r_35_0 ≤ 0nondet_12_post + nondet_12_post ≤ 0nondet_12_postnondet_12_post ≤ 0nondet_12_1 + nondet_12_1 ≤ 0nondet_12_1nondet_12_1 ≤ 0nondet_12_0 + nondet_12_0 ≤ 0nondet_12_0nondet_12_0 ≤ 0length_26_post + length_26_post ≤ 0length_26_postlength_26_post ≤ 0length_26_0 + length_26_0 ≤ 0length_26_0length_26_0 ≤ 0i_90_post + i_90_post ≤ 0i_90_posti_90_post ≤ 0i_90_0 + i_90_0 ≤ 0i_90_0i_90_0 ≤ 0i_27_post + i_27_post ≤ 0i_27_posti_27_post ≤ 0i_27_0 + i_27_0 ≤ 0i_27_0i_27_0 ≤ 0i_108_post + i_108_post ≤ 0i_108_posti_108_post ≤ 0i_108_0 + i_108_0 ≤ 0i_108_0i_108_0 ≤ 0head_29_post + head_29_post ≤ 0head_29_posthead_29_post ≤ 0head_29_0 + head_29_0 ≤ 0head_29_0head_29_0 ≤ 0ct_17_post + ct_17_post ≤ 0ct_17_postct_17_post ≤ 0ct_17_2 + ct_17_2 ≤ 0ct_17_2ct_17_2 ≤ 0ct_17_1 + ct_17_1 ≤ 0ct_17_1ct_17_1 ≤ 0ct_17_0 + ct_17_0 ≤ 0ct_17_0ct_17_0 ≤ 0a_162_post + a_162_post ≤ 0a_162_posta_162_post ≤ 0a_162_0 + a_162_0 ≤ 0a_162_0a_162_0 ≤ 0a_139_post + a_139_post ≤ 0a_139_posta_139_post ≤ 0a_139_0 + a_139_0 ≤ 0a_139_0a_139_0 ≤ 0a_117_post + a_117_post ≤ 0a_117_posta_117_post ≤ 0a_117_0 + a_117_0 ≤ 0a_117_0a_117_0 ≤ 0

8 SCC Decomposition

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

8.1 SCC Subproblem 1/2

Here we consider the SCC { 2, 4, 5, 6, 7, 8, 9, 2_var_snapshot, 2* }.

8.1.1 Transition Removal

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

 2: −1 + 7⋅a_139_0 4: −2 + 7⋅a_139_0 5: −3 + 7⋅a_139_0 6: 4 + 7⋅a_162_0 7: 3 + 7⋅a_162_0 8: 2 + 7⋅a_162_0 9: 1 + 7⋅a_139_0 2_var_snapshot: −1 + 7⋅a_139_0 2*: 7⋅a_139_0
Hints:
 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ] 2 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 7, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 6 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 7 lexWeak[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 7, 0, 7, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 8 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0] ]

8.1.2 Transition Removal

We remove transitions 37, 39, 2, 5, 6, 7, 8 using the following ranking functions, which are bounded by −3.

 2: −1 4: −3 5: 5⋅result_dot_nondet_sdv_special_RETURN_VALUE_13_1 6: 4 + 2⋅result_dot_nondet_sdv_special_RETURN_VALUE_13_1 7: 2 + 2⋅result_dot_nondet_sdv_special_RETURN_VALUE_13_1 8: 2⋅result_dot_nondet_sdv_special_RETURN_VALUE_13_1 9: 2 2_var_snapshot: −2 2*: 0
Hints:
 37 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 lexWeak[ [0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 6 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, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ] 8 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

8.1.3 Transition Removal

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

 2: 0 4: 0 5: result_dot_nondet_sdv_special_RETURN_VALUE_13_1 6: 0 7: 0 8: 0 9: 0 2_var_snapshot: 0 2*: 0
Hints:
 4 lexStrict[ [0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

8.1.4 Splitting Cut-Point Transitions

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

8.1.4.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 36.

8.1.4.1.1 Splitting Cut-Point Transitions

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

8.2 SCC Subproblem 2/2

Here we consider the SCC { 24, 30, 24_var_snapshot, 24* }.

8.2.1 Transition Removal

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

 24: −1 − 4⋅i_27_0 + 4⋅length_26_0 30: 1 − 4⋅i_27_0 + 4⋅length_26_0 24_var_snapshot: −2 − 4⋅i_27_0 + 4⋅length_26_0 24*: −4⋅i_27_0 + 4⋅length_26_0
Hints:
 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 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] ] 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 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] ] 31 lexStrict[ [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 4, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 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] ]

8.2.2 Transition Removal

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

 24: 0 30: 1 + length_26_0 24_var_snapshot: −1 24*: length_26_0
Hints:
 44 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 lexStrict[ [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 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 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, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] , [1, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0] ]

8.2.3 Splitting Cut-Point Transitions

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

8.2.3.1 Cut-Point Subproblem 1/1

Here we consider cut-point transition 43.

8.2.3.1.1 Splitting Cut-Point Transitions

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

T2Cert

• version: 1.0