MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i) -> f9(0, 1, 1, 0, 0, j, g, h, i) [ j >= 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i) -> f20(a, b, c - 1, d, d, 0, a - 2, 1, a - 2) [ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, g, h, i) -> f20(a, b, c - 1, d, d, 0, a, 0, a) [ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, g, h, i) -> f20(0, b + 1, b + 1, d, d, j, g, h, i) [ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, g, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, g, h, i) [ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, g, h, i) -> f20(a, b, c, d, d, f - 1, g, j, k) [ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, g, h, i) -> f20(a, b, c, d, d, f - 1, g, j, k) [ f >= 1 /\ d = e ] (?, 1) f20(a, b, c, d, e, f, g, h, i) -> f32(a, b, c, 0, e, f, g, h, 0) [ i = 0 ] (?, 1) f20(a, b, c, d, e, f, g, h, i) -> f32(a, b, c, 1, e, f, g, h, i) [ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, g, h, i) -> f32(a, b, c, 1, e, f, g, h, i) [ i >= 1 ] (?, 1) f32(a, b, c, d, e, f, g, h, i) -> f9(a, b, c, d, 0, f, g, 0, i) [ h = 0 ] (?, 1) f32(a, b, c, d, e, f, g, h, i) -> f9(a, b, c, d, 1, f, g, h, i) [ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, g, h, i) -> f9(a, b, c, d, 1, f, g, h, i) [ h >= 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i) -> f38(a, b, c, d, e, f, g, h, i) [ e >= d + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i) -> f38(a, b, c, d, e, f, g, h, i) [ d >= e + 1 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, e, f, h, i]. We thus obtain the following problem: 2: T: (?, 1) f9(a, b, c, d, e, f, h, i) -> f38(a, b, c, d, e, f, h, i) [ d >= e + 1 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f38(a, b, c, d, e, f, h, i) [ e >= d + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ h >= 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 0, f, 0, i) [ h = 0 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ i >= 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 0, e, f, h, 0) [ i = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ f >= 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, h, i) [ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(0, b + 1, b + 1, d, d, j, h, i) [ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 0, a) [ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 1, a - 2) [ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 ] (1, 1) f0(a, b, c, d, e, f, h, i) -> f9(0, 1, 1, 0, 0, j, h, i) [ j >= 1 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ h >= 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 0, f, 0, i) [ h = 0 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ i >= 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 0, e, f, h, 0) [ i = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ f >= 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, h, i) [ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(0, b + 1, b + 1, d, d, j, h, i) [ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 0, a) [ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 1, a - 2) [ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 ] (1, 1) f0(a, b, c, d, e, f, h, i) -> f9(0, 1, 1, 0, 0, j, h, i) [ j >= 1 ] start location: f0 leaf cost: 2 Applied AI with 'oct' on problem 3 to obtain the following invariants: For symbol f20: X_4 - X_5 >= 0 /\ X_5 >= 0 /\ X_4 + X_5 >= 0 /\ -X_4 + X_5 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 >= 0 /\ X_4 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 >= 0 /\ X_2 - X_3 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ -X_1 + X_2 - 1 >= 0 /\ X_1 >= 0 For symbol f32: X_5 >= 0 /\ X_4 + X_5 >= 0 /\ -X_4 + X_5 + 1 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 >= 0 /\ -X_4 + 1 >= 0 /\ X_2 - X_4 >= 0 /\ X_1 - X_4 + 1 >= 0 /\ X_4 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 >= 0 /\ X_2 - X_3 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ -X_1 + X_2 - 1 >= 0 /\ X_1 >= 0 For symbol f9: X_5 >= 0 /\ X_4 + X_5 >= 0 /\ X_2 + X_5 - 1 >= 0 /\ X_1 + X_5 >= 0 /\ X_4 >= 0 /\ X_2 + X_4 - 1 >= 0 /\ X_1 + X_4 >= 0 /\ X_2 - X_3 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 1 >= 0 /\ -X_1 + X_2 - 1 >= 0 /\ X_1 >= 0 This yielded the following problem: 4: T: (1, 1) f0(a, b, c, d, e, f, h, i) -> f9(0, 1, 1, 0, 0, j, h, i) [ j >= 1 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(0, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ f >= 1 /\ d = e ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 0, e, f, h, 0) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i = 0 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i >= 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 0, f, 0, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h = 0 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h >= 1 ] start location: f0 leaf cost: 2 By chaining the transition f0(a, b, c, d, e, f, h, i) -> f9(0, 1, 1, 0, 0, j, h, i) [ j >= 1 ] with all transitions in problem 4, the following new transition is obtained: f0(a, b, c, d, e, f, h, i) -> f20(0, 1, 1, 0, 0, j - 1, j', k) [ j >= 1 /\ 0 >= 0 /\ 0 = 0 ] We thus obtain the following problem: 5: T: (1, 2) f0(a, b, c, d, e, f, h, i) -> f20(0, 1, 1, 0, 0, j - 1, j', k) [ j >= 1 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(0, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ f >= 1 /\ d = e ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 0, e, f, h, 0) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i = 0 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i >= 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 0, f, 0, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h = 0 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h >= 1 ] start location: f0 leaf cost: 2 By chaining the transition f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 ] with all transitions in problem 5, the following new transition is obtained: f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 1, d, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a - 2 >= 1 ] We thus obtain the following problem: 6: T: (?, 2) f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 1, d, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a - 2 >= 1 ] (1, 2) f0(a, b, c, d, e, f, h, i) -> f20(0, 1, 1, 0, 0, j - 1, j', k) [ j >= 1 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(0, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ f >= 1 /\ d = e ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 0, e, f, h, 0) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i = 0 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i >= 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 0, f, 0, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h = 0 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h >= 1 ] start location: f0 leaf cost: 2 By chaining the transition f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 1, d, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a - 2 >= 1 ] with all transitions in problem 6, the following new transition is obtained: f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 1, 1, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a - 2 >= 1 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 1 >= 1 ] We thus obtain the following problem: 7: T: (?, 3) f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 1, 1, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a - 2 >= 1 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 1 >= 1 ] (1, 2) f0(a, b, c, d, e, f, h, i) -> f20(0, 1, 1, 0, 0, j - 1, j', k) [ j >= 1 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(0, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ f >= 1 /\ d = e ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 0, e, f, h, 0) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i = 0 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i >= 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 0, f, 0, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h = 0 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h >= 1 ] start location: f0 leaf cost: 2 By chaining the transition f9(a, b, c, d, e, f, h, i) -> f20(a, b, c - 1, d, d, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 ] with all transitions in problem 7, the following new transitions are obtained: f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 1, d, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a >= 1 ] f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 0, d, 0, 0, 0) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a = 0 ] We thus obtain the following problem: 8: T: (?, 2) f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 1, d, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a >= 1 ] (?, 2) f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 0, d, 0, 0, 0) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a = 0 ] (?, 3) f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 1, 1, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a - 2 >= 1 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 1 >= 1 ] (1, 2) f0(a, b, c, d, e, f, h, i) -> f20(0, 1, 1, 0, 0, j - 1, j', k) [ j >= 1 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(0, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ f >= 1 /\ d = e ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 0, e, f, h, 0) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i = 0 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i >= 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 0, f, 0, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h = 0 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h >= 1 ] start location: f0 leaf cost: 2 By chaining the transition f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 1, d, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a >= 1 ] with all transitions in problem 8, the following new transition is obtained: f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 1, 0, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a >= 1 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 0 = 0 ] We thus obtain the following problem: 9: T: (?, 3) f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 1, 0, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a >= 1 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 0 = 0 ] (?, 2) f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 0, d, 0, 0, 0) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a = 0 ] (?, 3) f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 1, 1, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a - 2 >= 1 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 1 >= 1 ] (1, 2) f0(a, b, c, d, e, f, h, i) -> f20(0, 1, 1, 0, 0, j - 1, j', k) [ j >= 1 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(0, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ f >= 1 /\ d = e ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 0, e, f, h, 0) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i = 0 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i >= 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 0, f, 0, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h = 0 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h >= 1 ] start location: f0 leaf cost: 2 By chaining the transition f9(a, b, c, d, e, f, h, i) -> f32(a, b, c - 1, 0, d, 0, 0, 0) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a = 0 ] with all transitions in problem 9, the following new transition is obtained: f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 0, 0, 0, 0, 0) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a = 0 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 0 = 0 ] We thus obtain the following problem: 10: T: (?, 3) f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 0, 0, 0, 0, 0) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a = 0 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 0 = 0 ] (?, 3) f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 1, 0, 0, 0, a) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 2 >= a /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a >= 1 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 0 = 0 ] (?, 3) f9(a, b, c, d, e, f, h, i) -> f9(a, b, c - 1, 1, 1, 0, 1, a - 2) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ a >= 3 /\ c >= 1 /\ d = e /\ f = 0 /\ 0 >= 0 /\ 2*d >= 0 /\ b - c + 1 >= 0 /\ a - 2 >= 1 /\ d + 1 >= 0 /\ 1 >= 0 /\ b >= 0 /\ a + 1 >= 0 /\ 1 >= 1 ] (1, 2) f0(a, b, c, d, e, f, h, i) -> f20(0, 1, 1, 0, 0, j - 1, j', k) [ j >= 1 /\ 0 >= 0 /\ 0 = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(0, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ a >= 3 /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a + 1, b + 1, b + 1, d, d, j, h, i) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ j >= 1 /\ 2 >= a /\ 0 >= c /\ d = e /\ f = 0 ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= f + 1 /\ d = e ] (?, 1) f9(a, b, c, d, e, f, h, i) -> f20(a, b, c, d, d, f - 1, j, k) [ e >= 0 /\ d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ f >= 1 /\ d = e ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 0, e, f, h, 0) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i = 0 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= i + 1 ] (?, 1) f20(a, b, c, d, e, f, h, i) -> f32(a, b, c, 1, e, f, h, i) [ d - e >= 0 /\ e >= 0 /\ d + e >= 0 /\ -d + e >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ i >= 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 0, f, 0, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h = 0 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ 0 >= h + 1 ] (?, 1) f32(a, b, c, d, e, f, h, i) -> f9(a, b, c, d, 1, f, h, i) [ e >= 0 /\ d + e >= 0 /\ -d + e + 1 >= 0 /\ b + e - 1 >= 0 /\ a + e >= 0 /\ -d + 1 >= 0 /\ b - d >= 0 /\ a - d + 1 >= 0 /\ d >= 0 /\ b + d - 1 >= 0 /\ a + d >= 0 /\ b - c >= 0 /\ b - 1 >= 0 /\ a + b - 1 >= 0 /\ -a + b - 1 >= 0 /\ a >= 0 /\ h >= 1 ] start location: f0 leaf cost: 2 Complexity upper bound ? Time: 4.145 sec (SMT: 3.491 sec)