MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f18(3, 3, 0, 3, e, f, g, h, i, j, k, l, m, n, o, p, q, r) (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ 0 >= a /\ a >= c ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f10(a, b + a, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= 1 /\ a >= c ] (?, 1) f18(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f25(a, b, c, d, d, d, -3, 4, 0, j, k, l, m, n, o, p, q, r) (?, 1) f25(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f25(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ 0 >= g /\ g >= i ] (?, 1) f25(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f25(a, b, c, d, e, f, g, h + g, i, j, k, l, m, n, o, p, q, r) [ g >= 1 /\ g >= i ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f40(a, b, c, d, e, f, g, h, i, k, k, k, 3, -6, 0, p, q, r) (?, 1) f40(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f40(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ 0 >= m /\ m >= o ] (?, 1) f40(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f40(a, b, c, d, e, f, g, h, i, j, k, l, m, n + m, o, p, q, r) [ m >= 1 /\ m >= o ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f52(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, q, q, q) [ 4 >= f ] (?, 1) f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f52(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, q, q, q) [ f >= 5 ] (?, 1) f40(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f48(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, n, r) [ o >= m + 1 ] (?, 1) f25(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f33(a, b, c, d, e, f, g, h, i, j, h, l, m, n, o, p, q, r) [ i >= g + 1 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f18(a, b, c, b, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ c >= a + 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, f, g, i, m, o]. We thus obtain the following problem: 2: T: (?, 1) f10(a, b, c, d, f, g, i, m, o) -> f18(a, b, c, b, f, g, i, m, o) [ c >= a + 1 ] (?, 1) f25(a, b, c, d, f, g, i, m, o) -> f33(a, b, c, d, f, g, i, m, o) [ i >= g + 1 ] (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f48(a, b, c, d, f, g, i, m, o) [ o >= m + 1 ] (?, 1) f48(a, b, c, d, f, g, i, m, o) -> f52(a, b, c, d, f, g, i, m, o) [ f >= 5 ] (?, 1) f48(a, b, c, d, f, g, i, m, o) -> f52(a, b, c, d, f, g, i, m, o) [ 4 >= f ] (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ m >= 1 /\ m >= o ] (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ 0 >= m /\ m >= o ] (?, 1) f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) (?, 1) f25(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, f, g, i, m, o) [ g >= 1 /\ g >= i ] (?, 1) f25(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, f, g, i, m, o) [ 0 >= g /\ g >= i ] (?, 1) f18(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, d, -3, 0, m, o) (?, 1) f10(a, b, c, d, f, g, i, m, o) -> f10(a, b + a, c, d, f, g, i, m, o) [ a >= 1 /\ a >= c ] (?, 1) f10(a, b, c, d, f, g, i, m, o) -> f10(a, b, c, d, f, g, i, m, o) [ 0 >= a /\ a >= c ] (1, 1) f0(a, b, c, d, f, g, i, m, o) -> f18(3, 3, 0, 3, f, g, i, m, o) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f10(a, b, c, d, f, g, i, m, o) -> f18(a, b, c, b, f, g, i, m, o) [ c >= a + 1 ] (?, 1) f25(a, b, c, d, f, g, i, m, o) -> f33(a, b, c, d, f, g, i, m, o) [ i >= g + 1 ] (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ m >= 1 /\ m >= o ] (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ 0 >= m /\ m >= o ] (?, 1) f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) (?, 1) f25(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, f, g, i, m, o) [ g >= 1 /\ g >= i ] (?, 1) f25(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, f, g, i, m, o) [ 0 >= g /\ g >= i ] (?, 1) f18(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, d, -3, 0, m, o) (?, 1) f10(a, b, c, d, f, g, i, m, o) -> f10(a, b + a, c, d, f, g, i, m, o) [ a >= 1 /\ a >= c ] (?, 1) f10(a, b, c, d, f, g, i, m, o) -> f10(a, b, c, d, f, g, i, m, o) [ 0 >= a /\ a >= c ] (1, 1) f0(a, b, c, d, f, g, i, m, o) -> f18(3, 3, 0, 3, f, g, i, m, o) start location: f0 leaf cost: 3 Testing for reachability in the complexity graph removes the following transitions from problem 3: f10(a, b, c, d, f, g, i, m, o) -> f18(a, b, c, b, f, g, i, m, o) [ c >= a + 1 ] f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ 0 >= m /\ m >= o ] f25(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, f, g, i, m, o) [ g >= 1 /\ g >= i ] f25(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, f, g, i, m, o) [ 0 >= g /\ g >= i ] f10(a, b, c, d, f, g, i, m, o) -> f10(a, b + a, c, d, f, g, i, m, o) [ a >= 1 /\ a >= c ] f10(a, b, c, d, f, g, i, m, o) -> f10(a, b, c, d, f, g, i, m, o) [ 0 >= a /\ a >= c ] We thus obtain the following problem: 4: T: (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ m >= 1 /\ m >= o ] (?, 1) f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) (?, 1) f25(a, b, c, d, f, g, i, m, o) -> f33(a, b, c, d, f, g, i, m, o) [ i >= g + 1 ] (?, 1) f18(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, d, -3, 0, m, o) (1, 1) f0(a, b, c, d, f, g, i, m, o) -> f18(3, 3, 0, 3, f, g, i, m, o) start location: f0 leaf cost: 3 Repeatedly propagating knowledge in problem 4 produces the following problem: 5: T: (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ m >= 1 /\ m >= o ] (1, 1) f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) (1, 1) f25(a, b, c, d, f, g, i, m, o) -> f33(a, b, c, d, f, g, i, m, o) [ i >= g + 1 ] (1, 1) f18(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, d, -3, 0, m, o) (1, 1) f0(a, b, c, d, f, g, i, m, o) -> f18(3, 3, 0, 3, f, g, i, m, o) start location: f0 leaf cost: 3 Applied AI with 'oct' on problem 5 to obtain the following invariants: For symbol f18: -X_4 + 3 >= 0 /\ X_3 - X_4 + 3 >= 0 /\ -X_3 - X_4 + 3 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 + 6 >= 0 /\ X_1 - X_4 >= 0 /\ -X_1 - X_4 + 6 >= 0 /\ X_4 - 3 >= 0 /\ X_3 + X_4 - 3 >= 0 /\ -X_3 + X_4 - 3 >= 0 /\ X_2 + X_4 - 6 >= 0 /\ -X_2 + X_4 >= 0 /\ X_1 + X_4 - 6 >= 0 /\ -X_1 + X_4 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 3 >= 0 /\ -X_2 - X_3 + 3 >= 0 /\ X_1 - X_3 - 3 >= 0 /\ -X_1 - X_3 + 3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 3 >= 0 /\ -X_2 + X_3 + 3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ -X_1 + X_3 + 3 >= 0 /\ -X_2 + 3 >= 0 /\ X_1 - X_2 >= 0 /\ -X_1 - X_2 + 6 >= 0 /\ X_2 - 3 >= 0 /\ X_1 + X_2 - 6 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 + 3 >= 0 /\ X_1 - 3 >= 0 For symbol f25: -X_7 >= 0 /\ X_6 - X_7 + 3 >= 0 /\ -X_6 - X_7 - 3 >= 0 /\ X_5 - X_7 - 3 >= 0 /\ -X_5 - X_7 + 3 >= 0 /\ X_4 - X_7 - 3 >= 0 /\ -X_4 - X_7 + 3 >= 0 /\ X_3 - X_7 >= 0 /\ -X_3 - X_7 >= 0 /\ X_2 - X_7 - 3 >= 0 /\ -X_2 - X_7 + 3 >= 0 /\ X_1 - X_7 - 3 >= 0 /\ -X_1 - X_7 + 3 >= 0 /\ X_7 >= 0 /\ X_6 + X_7 + 3 >= 0 /\ -X_6 + X_7 - 3 >= 0 /\ X_5 + X_7 - 3 >= 0 /\ -X_5 + X_7 + 3 >= 0 /\ X_4 + X_7 - 3 >= 0 /\ -X_4 + X_7 + 3 >= 0 /\ X_3 + X_7 >= 0 /\ -X_3 + X_7 >= 0 /\ X_2 + X_7 - 3 >= 0 /\ -X_2 + X_7 + 3 >= 0 /\ X_1 + X_7 - 3 >= 0 /\ -X_1 + X_7 + 3 >= 0 /\ -X_6 - 3 >= 0 /\ X_5 - X_6 - 6 >= 0 /\ -X_5 - X_6 >= 0 /\ X_4 - X_6 - 6 >= 0 /\ -X_4 - X_6 >= 0 /\ X_3 - X_6 - 3 >= 0 /\ -X_3 - X_6 - 3 >= 0 /\ X_2 - X_6 - 6 >= 0 /\ -X_2 - X_6 >= 0 /\ X_1 - X_6 - 6 >= 0 /\ -X_1 - X_6 >= 0 /\ X_6 + 3 >= 0 /\ X_5 + X_6 >= 0 /\ -X_5 + X_6 + 6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 + 6 >= 0 /\ X_3 + X_6 + 3 >= 0 /\ -X_3 + X_6 + 3 >= 0 /\ X_2 + X_6 >= 0 /\ -X_2 + X_6 + 6 >= 0 /\ X_1 + X_6 >= 0 /\ -X_1 + X_6 + 6 >= 0 /\ -X_5 + 3 >= 0 /\ X_4 - X_5 >= 0 /\ -X_4 - X_5 + 6 >= 0 /\ X_3 - X_5 + 3 >= 0 /\ -X_3 - X_5 + 3 >= 0 /\ X_2 - X_5 >= 0 /\ -X_2 - X_5 + 6 >= 0 /\ X_1 - X_5 >= 0 /\ -X_1 - X_5 + 6 >= 0 /\ X_5 - 3 >= 0 /\ X_4 + X_5 - 6 >= 0 /\ -X_4 + X_5 >= 0 /\ X_3 + X_5 - 3 >= 0 /\ -X_3 + X_5 - 3 >= 0 /\ X_2 + X_5 - 6 >= 0 /\ -X_2 + X_5 >= 0 /\ X_1 + X_5 - 6 >= 0 /\ -X_1 + X_5 >= 0 /\ -X_4 + 3 >= 0 /\ X_3 - X_4 + 3 >= 0 /\ -X_3 - X_4 + 3 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 + 6 >= 0 /\ X_1 - X_4 >= 0 /\ -X_1 - X_4 + 6 >= 0 /\ X_4 - 3 >= 0 /\ X_3 + X_4 - 3 >= 0 /\ -X_3 + X_4 - 3 >= 0 /\ X_2 + X_4 - 6 >= 0 /\ -X_2 + X_4 >= 0 /\ X_1 + X_4 - 6 >= 0 /\ -X_1 + X_4 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 3 >= 0 /\ -X_2 - X_3 + 3 >= 0 /\ X_1 - X_3 - 3 >= 0 /\ -X_1 - X_3 + 3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 3 >= 0 /\ -X_2 + X_3 + 3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ -X_1 + X_3 + 3 >= 0 /\ -X_2 + 3 >= 0 /\ X_1 - X_2 >= 0 /\ -X_1 - X_2 + 6 >= 0 /\ X_2 - 3 >= 0 /\ X_1 + X_2 - 6 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 + 3 >= 0 /\ X_1 - 3 >= 0 For symbol f33: -X_7 >= 0 /\ X_6 - X_7 + 3 >= 0 /\ -X_6 - X_7 - 3 >= 0 /\ X_5 - X_7 - 3 >= 0 /\ -X_5 - X_7 + 3 >= 0 /\ X_4 - X_7 - 3 >= 0 /\ -X_4 - X_7 + 3 >= 0 /\ X_3 - X_7 >= 0 /\ -X_3 - X_7 >= 0 /\ X_2 - X_7 - 3 >= 0 /\ -X_2 - X_7 + 3 >= 0 /\ X_1 - X_7 - 3 >= 0 /\ -X_1 - X_7 + 3 >= 0 /\ X_7 >= 0 /\ X_6 + X_7 + 3 >= 0 /\ -X_6 + X_7 - 3 >= 0 /\ X_5 + X_7 - 3 >= 0 /\ -X_5 + X_7 + 3 >= 0 /\ X_4 + X_7 - 3 >= 0 /\ -X_4 + X_7 + 3 >= 0 /\ X_3 + X_7 >= 0 /\ -X_3 + X_7 >= 0 /\ X_2 + X_7 - 3 >= 0 /\ -X_2 + X_7 + 3 >= 0 /\ X_1 + X_7 - 3 >= 0 /\ -X_1 + X_7 + 3 >= 0 /\ -X_6 - 3 >= 0 /\ X_5 - X_6 - 6 >= 0 /\ -X_5 - X_6 >= 0 /\ X_4 - X_6 - 6 >= 0 /\ -X_4 - X_6 >= 0 /\ X_3 - X_6 - 3 >= 0 /\ -X_3 - X_6 - 3 >= 0 /\ X_2 - X_6 - 6 >= 0 /\ -X_2 - X_6 >= 0 /\ X_1 - X_6 - 6 >= 0 /\ -X_1 - X_6 >= 0 /\ X_6 + 3 >= 0 /\ X_5 + X_6 >= 0 /\ -X_5 + X_6 + 6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 + 6 >= 0 /\ X_3 + X_6 + 3 >= 0 /\ -X_3 + X_6 + 3 >= 0 /\ X_2 + X_6 >= 0 /\ -X_2 + X_6 + 6 >= 0 /\ X_1 + X_6 >= 0 /\ -X_1 + X_6 + 6 >= 0 /\ -X_5 + 3 >= 0 /\ X_4 - X_5 >= 0 /\ -X_4 - X_5 + 6 >= 0 /\ X_3 - X_5 + 3 >= 0 /\ -X_3 - X_5 + 3 >= 0 /\ X_2 - X_5 >= 0 /\ -X_2 - X_5 + 6 >= 0 /\ X_1 - X_5 >= 0 /\ -X_1 - X_5 + 6 >= 0 /\ X_5 - 3 >= 0 /\ X_4 + X_5 - 6 >= 0 /\ -X_4 + X_5 >= 0 /\ X_3 + X_5 - 3 >= 0 /\ -X_3 + X_5 - 3 >= 0 /\ X_2 + X_5 - 6 >= 0 /\ -X_2 + X_5 >= 0 /\ X_1 + X_5 - 6 >= 0 /\ -X_1 + X_5 >= 0 /\ -X_4 + 3 >= 0 /\ X_3 - X_4 + 3 >= 0 /\ -X_3 - X_4 + 3 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 + 6 >= 0 /\ X_1 - X_4 >= 0 /\ -X_1 - X_4 + 6 >= 0 /\ X_4 - 3 >= 0 /\ X_3 + X_4 - 3 >= 0 /\ -X_3 + X_4 - 3 >= 0 /\ X_2 + X_4 - 6 >= 0 /\ -X_2 + X_4 >= 0 /\ X_1 + X_4 - 6 >= 0 /\ -X_1 + X_4 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 3 >= 0 /\ -X_2 - X_3 + 3 >= 0 /\ X_1 - X_3 - 3 >= 0 /\ -X_1 - X_3 + 3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 3 >= 0 /\ -X_2 + X_3 + 3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ -X_1 + X_3 + 3 >= 0 /\ -X_2 + 3 >= 0 /\ X_1 - X_2 >= 0 /\ -X_1 - X_2 + 6 >= 0 /\ X_2 - 3 >= 0 /\ X_1 + X_2 - 6 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 + 3 >= 0 /\ X_1 - 3 >= 0 For symbol f40: -X_9 >= 0 /\ X_8 - X_9 - 3 >= 0 /\ -X_8 - X_9 + 3 >= 0 /\ X_7 - X_9 >= 0 /\ -X_7 - X_9 >= 0 /\ X_6 - X_9 + 3 >= 0 /\ -X_6 - X_9 - 3 >= 0 /\ X_5 - X_9 - 3 >= 0 /\ -X_5 - X_9 + 3 >= 0 /\ X_4 - X_9 - 3 >= 0 /\ -X_4 - X_9 + 3 >= 0 /\ X_3 - X_9 >= 0 /\ -X_3 - X_9 >= 0 /\ X_2 - X_9 - 3 >= 0 /\ -X_2 - X_9 + 3 >= 0 /\ X_1 - X_9 - 3 >= 0 /\ -X_1 - X_9 + 3 >= 0 /\ X_9 >= 0 /\ X_8 + X_9 - 3 >= 0 /\ -X_8 + X_9 + 3 >= 0 /\ X_7 + X_9 >= 0 /\ -X_7 + X_9 >= 0 /\ X_6 + X_9 + 3 >= 0 /\ -X_6 + X_9 - 3 >= 0 /\ X_5 + X_9 - 3 >= 0 /\ -X_5 + X_9 + 3 >= 0 /\ X_4 + X_9 - 3 >= 0 /\ -X_4 + X_9 + 3 >= 0 /\ X_3 + X_9 >= 0 /\ -X_3 + X_9 >= 0 /\ X_2 + X_9 - 3 >= 0 /\ -X_2 + X_9 + 3 >= 0 /\ X_1 + X_9 - 3 >= 0 /\ -X_1 + X_9 + 3 >= 0 /\ -X_8 + 3 >= 0 /\ X_7 - X_8 + 3 >= 0 /\ -X_7 - X_8 + 3 >= 0 /\ X_6 - X_8 + 6 >= 0 /\ -X_6 - X_8 >= 0 /\ X_5 - X_8 >= 0 /\ -X_5 - X_8 + 6 >= 0 /\ X_4 - X_8 >= 0 /\ -X_4 - X_8 + 6 >= 0 /\ X_3 - X_8 + 3 >= 0 /\ -X_3 - X_8 + 3 >= 0 /\ X_2 - X_8 >= 0 /\ -X_2 - X_8 + 6 >= 0 /\ X_1 - X_8 >= 0 /\ -X_1 - X_8 + 6 >= 0 /\ X_8 - 3 >= 0 /\ X_7 + X_8 - 3 >= 0 /\ -X_7 + X_8 - 3 >= 0 /\ X_6 + X_8 >= 0 /\ -X_6 + X_8 - 6 >= 0 /\ X_5 + X_8 - 6 >= 0 /\ -X_5 + X_8 >= 0 /\ X_4 + X_8 - 6 >= 0 /\ -X_4 + X_8 >= 0 /\ X_3 + X_8 - 3 >= 0 /\ -X_3 + X_8 - 3 >= 0 /\ X_2 + X_8 - 6 >= 0 /\ -X_2 + X_8 >= 0 /\ X_1 + X_8 - 6 >= 0 /\ -X_1 + X_8 >= 0 /\ -X_7 >= 0 /\ X_6 - X_7 + 3 >= 0 /\ -X_6 - X_7 - 3 >= 0 /\ X_5 - X_7 - 3 >= 0 /\ -X_5 - X_7 + 3 >= 0 /\ X_4 - X_7 - 3 >= 0 /\ -X_4 - X_7 + 3 >= 0 /\ X_3 - X_7 >= 0 /\ -X_3 - X_7 >= 0 /\ X_2 - X_7 - 3 >= 0 /\ -X_2 - X_7 + 3 >= 0 /\ X_1 - X_7 - 3 >= 0 /\ -X_1 - X_7 + 3 >= 0 /\ X_7 >= 0 /\ X_6 + X_7 + 3 >= 0 /\ -X_6 + X_7 - 3 >= 0 /\ X_5 + X_7 - 3 >= 0 /\ -X_5 + X_7 + 3 >= 0 /\ X_4 + X_7 - 3 >= 0 /\ -X_4 + X_7 + 3 >= 0 /\ X_3 + X_7 >= 0 /\ -X_3 + X_7 >= 0 /\ X_2 + X_7 - 3 >= 0 /\ -X_2 + X_7 + 3 >= 0 /\ X_1 + X_7 - 3 >= 0 /\ -X_1 + X_7 + 3 >= 0 /\ -X_6 - 3 >= 0 /\ X_5 - X_6 - 6 >= 0 /\ -X_5 - X_6 >= 0 /\ X_4 - X_6 - 6 >= 0 /\ -X_4 - X_6 >= 0 /\ X_3 - X_6 - 3 >= 0 /\ -X_3 - X_6 - 3 >= 0 /\ X_2 - X_6 - 6 >= 0 /\ -X_2 - X_6 >= 0 /\ X_1 - X_6 - 6 >= 0 /\ -X_1 - X_6 >= 0 /\ X_6 + 3 >= 0 /\ X_5 + X_6 >= 0 /\ -X_5 + X_6 + 6 >= 0 /\ X_4 + X_6 >= 0 /\ -X_4 + X_6 + 6 >= 0 /\ X_3 + X_6 + 3 >= 0 /\ -X_3 + X_6 + 3 >= 0 /\ X_2 + X_6 >= 0 /\ -X_2 + X_6 + 6 >= 0 /\ X_1 + X_6 >= 0 /\ -X_1 + X_6 + 6 >= 0 /\ -X_5 + 3 >= 0 /\ X_4 - X_5 >= 0 /\ -X_4 - X_5 + 6 >= 0 /\ X_3 - X_5 + 3 >= 0 /\ -X_3 - X_5 + 3 >= 0 /\ X_2 - X_5 >= 0 /\ -X_2 - X_5 + 6 >= 0 /\ X_1 - X_5 >= 0 /\ -X_1 - X_5 + 6 >= 0 /\ X_5 - 3 >= 0 /\ X_4 + X_5 - 6 >= 0 /\ -X_4 + X_5 >= 0 /\ X_3 + X_5 - 3 >= 0 /\ -X_3 + X_5 - 3 >= 0 /\ X_2 + X_5 - 6 >= 0 /\ -X_2 + X_5 >= 0 /\ X_1 + X_5 - 6 >= 0 /\ -X_1 + X_5 >= 0 /\ -X_4 + 3 >= 0 /\ X_3 - X_4 + 3 >= 0 /\ -X_3 - X_4 + 3 >= 0 /\ X_2 - X_4 >= 0 /\ -X_2 - X_4 + 6 >= 0 /\ X_1 - X_4 >= 0 /\ -X_1 - X_4 + 6 >= 0 /\ X_4 - 3 >= 0 /\ X_3 + X_4 - 3 >= 0 /\ -X_3 + X_4 - 3 >= 0 /\ X_2 + X_4 - 6 >= 0 /\ -X_2 + X_4 >= 0 /\ X_1 + X_4 - 6 >= 0 /\ -X_1 + X_4 >= 0 /\ -X_3 >= 0 /\ X_2 - X_3 - 3 >= 0 /\ -X_2 - X_3 + 3 >= 0 /\ X_1 - X_3 - 3 >= 0 /\ -X_1 - X_3 + 3 >= 0 /\ X_3 >= 0 /\ X_2 + X_3 - 3 >= 0 /\ -X_2 + X_3 + 3 >= 0 /\ X_1 + X_3 - 3 >= 0 /\ -X_1 + X_3 + 3 >= 0 /\ -X_2 + 3 >= 0 /\ X_1 - X_2 >= 0 /\ -X_1 - X_2 + 6 >= 0 /\ X_2 - 3 >= 0 /\ X_1 + X_2 - 6 >= 0 /\ -X_1 + X_2 >= 0 /\ -X_1 + 3 >= 0 /\ X_1 - 3 >= 0 This yielded the following problem: 6: T: (1, 1) f0(a, b, c, d, f, g, i, m, o) -> f18(3, 3, 0, 3, f, g, i, m, o) (1, 1) f18(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, d, -3, 0, m, o) [ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 ] (1, 1) f25(a, b, c, d, f, g, i, m, o) -> f33(a, b, c, d, f, g, i, m, o) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ i >= g + 1 ] (1, 1) f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 ] (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ -o >= 0 /\ m - o - 3 >= 0 /\ -m - o + 3 >= 0 /\ i - o >= 0 /\ -i - o >= 0 /\ g - o + 3 >= 0 /\ -g - o - 3 >= 0 /\ f - o - 3 >= 0 /\ -f - o + 3 >= 0 /\ d - o - 3 >= 0 /\ -d - o + 3 >= 0 /\ c - o >= 0 /\ -c - o >= 0 /\ b - o - 3 >= 0 /\ -b - o + 3 >= 0 /\ a - o - 3 >= 0 /\ -a - o + 3 >= 0 /\ o >= 0 /\ m + o - 3 >= 0 /\ -m + o + 3 >= 0 /\ i + o >= 0 /\ -i + o >= 0 /\ g + o + 3 >= 0 /\ -g + o - 3 >= 0 /\ f + o - 3 >= 0 /\ -f + o + 3 >= 0 /\ d + o - 3 >= 0 /\ -d + o + 3 >= 0 /\ c + o >= 0 /\ -c + o >= 0 /\ b + o - 3 >= 0 /\ -b + o + 3 >= 0 /\ a + o - 3 >= 0 /\ -a + o + 3 >= 0 /\ -m + 3 >= 0 /\ i - m + 3 >= 0 /\ -i - m + 3 >= 0 /\ g - m + 6 >= 0 /\ -g - m >= 0 /\ f - m >= 0 /\ -f - m + 6 >= 0 /\ d - m >= 0 /\ -d - m + 6 >= 0 /\ c - m + 3 >= 0 /\ -c - m + 3 >= 0 /\ b - m >= 0 /\ -b - m + 6 >= 0 /\ a - m >= 0 /\ -a - m + 6 >= 0 /\ m - 3 >= 0 /\ i + m - 3 >= 0 /\ -i + m - 3 >= 0 /\ g + m >= 0 /\ -g + m - 6 >= 0 /\ f + m - 6 >= 0 /\ -f + m >= 0 /\ d + m - 6 >= 0 /\ -d + m >= 0 /\ c + m - 3 >= 0 /\ -c + m - 3 >= 0 /\ b + m - 6 >= 0 /\ -b + m >= 0 /\ a + m - 6 >= 0 /\ -a + m >= 0 /\ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ m >= 1 /\ m >= o ] start location: f0 leaf cost: 3 By chaining the transition f0(a, b, c, d, f, g, i, m, o) -> f18(3, 3, 0, 3, f, g, i, m, o) with all transitions in problem 6, the following new transition is obtained: f0(a, b, c, d, f, g, i, m, o) -> f25(3, 3, 0, 3, 3, -3, 0, m, o) [ 0 >= 0 ] We thus obtain the following problem: 7: T: (1, 2) f0(a, b, c, d, f, g, i, m, o) -> f25(3, 3, 0, 3, 3, -3, 0, m, o) [ 0 >= 0 ] (1, 1) f18(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, d, -3, 0, m, o) [ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 ] (1, 1) f25(a, b, c, d, f, g, i, m, o) -> f33(a, b, c, d, f, g, i, m, o) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ i >= g + 1 ] (1, 1) f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 ] (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ -o >= 0 /\ m - o - 3 >= 0 /\ -m - o + 3 >= 0 /\ i - o >= 0 /\ -i - o >= 0 /\ g - o + 3 >= 0 /\ -g - o - 3 >= 0 /\ f - o - 3 >= 0 /\ -f - o + 3 >= 0 /\ d - o - 3 >= 0 /\ -d - o + 3 >= 0 /\ c - o >= 0 /\ -c - o >= 0 /\ b - o - 3 >= 0 /\ -b - o + 3 >= 0 /\ a - o - 3 >= 0 /\ -a - o + 3 >= 0 /\ o >= 0 /\ m + o - 3 >= 0 /\ -m + o + 3 >= 0 /\ i + o >= 0 /\ -i + o >= 0 /\ g + o + 3 >= 0 /\ -g + o - 3 >= 0 /\ f + o - 3 >= 0 /\ -f + o + 3 >= 0 /\ d + o - 3 >= 0 /\ -d + o + 3 >= 0 /\ c + o >= 0 /\ -c + o >= 0 /\ b + o - 3 >= 0 /\ -b + o + 3 >= 0 /\ a + o - 3 >= 0 /\ -a + o + 3 >= 0 /\ -m + 3 >= 0 /\ i - m + 3 >= 0 /\ -i - m + 3 >= 0 /\ g - m + 6 >= 0 /\ -g - m >= 0 /\ f - m >= 0 /\ -f - m + 6 >= 0 /\ d - m >= 0 /\ -d - m + 6 >= 0 /\ c - m + 3 >= 0 /\ -c - m + 3 >= 0 /\ b - m >= 0 /\ -b - m + 6 >= 0 /\ a - m >= 0 /\ -a - m + 6 >= 0 /\ m - 3 >= 0 /\ i + m - 3 >= 0 /\ -i + m - 3 >= 0 /\ g + m >= 0 /\ -g + m - 6 >= 0 /\ f + m - 6 >= 0 /\ -f + m >= 0 /\ d + m - 6 >= 0 /\ -d + m >= 0 /\ c + m - 3 >= 0 /\ -c + m - 3 >= 0 /\ b + m - 6 >= 0 /\ -b + m >= 0 /\ a + m - 6 >= 0 /\ -a + m >= 0 /\ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ m >= 1 /\ m >= o ] start location: f0 leaf cost: 3 Testing for reachability in the complexity graph removes the following transition from problem 7: f18(a, b, c, d, f, g, i, m, o) -> f25(a, b, c, d, d, -3, 0, m, o) [ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 ] We thus obtain the following problem: 8: T: (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ -o >= 0 /\ m - o - 3 >= 0 /\ -m - o + 3 >= 0 /\ i - o >= 0 /\ -i - o >= 0 /\ g - o + 3 >= 0 /\ -g - o - 3 >= 0 /\ f - o - 3 >= 0 /\ -f - o + 3 >= 0 /\ d - o - 3 >= 0 /\ -d - o + 3 >= 0 /\ c - o >= 0 /\ -c - o >= 0 /\ b - o - 3 >= 0 /\ -b - o + 3 >= 0 /\ a - o - 3 >= 0 /\ -a - o + 3 >= 0 /\ o >= 0 /\ m + o - 3 >= 0 /\ -m + o + 3 >= 0 /\ i + o >= 0 /\ -i + o >= 0 /\ g + o + 3 >= 0 /\ -g + o - 3 >= 0 /\ f + o - 3 >= 0 /\ -f + o + 3 >= 0 /\ d + o - 3 >= 0 /\ -d + o + 3 >= 0 /\ c + o >= 0 /\ -c + o >= 0 /\ b + o - 3 >= 0 /\ -b + o + 3 >= 0 /\ a + o - 3 >= 0 /\ -a + o + 3 >= 0 /\ -m + 3 >= 0 /\ i - m + 3 >= 0 /\ -i - m + 3 >= 0 /\ g - m + 6 >= 0 /\ -g - m >= 0 /\ f - m >= 0 /\ -f - m + 6 >= 0 /\ d - m >= 0 /\ -d - m + 6 >= 0 /\ c - m + 3 >= 0 /\ -c - m + 3 >= 0 /\ b - m >= 0 /\ -b - m + 6 >= 0 /\ a - m >= 0 /\ -a - m + 6 >= 0 /\ m - 3 >= 0 /\ i + m - 3 >= 0 /\ -i + m - 3 >= 0 /\ g + m >= 0 /\ -g + m - 6 >= 0 /\ f + m - 6 >= 0 /\ -f + m >= 0 /\ d + m - 6 >= 0 /\ -d + m >= 0 /\ c + m - 3 >= 0 /\ -c + m - 3 >= 0 /\ b + m - 6 >= 0 /\ -b + m >= 0 /\ a + m - 6 >= 0 /\ -a + m >= 0 /\ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ m >= 1 /\ m >= o ] (1, 1) f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 ] (1, 1) f25(a, b, c, d, f, g, i, m, o) -> f33(a, b, c, d, f, g, i, m, o) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ i >= g + 1 ] (1, 2) f0(a, b, c, d, f, g, i, m, o) -> f25(3, 3, 0, 3, 3, -3, 0, m, o) [ 0 >= 0 ] start location: f0 leaf cost: 3 By chaining the transition f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 ] with all transitions in problem 8, the following new transition is obtained: f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ 0 >= 0 /\ 3 >= 1 /\ 3 >= 0 ] We thus obtain the following problem: 9: T: (1, 2) f33(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, 3, 0) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ 0 >= 0 /\ 3 >= 1 /\ 3 >= 0 ] (?, 1) f40(a, b, c, d, f, g, i, m, o) -> f40(a, b, c, d, f, g, i, m, o) [ -o >= 0 /\ m - o - 3 >= 0 /\ -m - o + 3 >= 0 /\ i - o >= 0 /\ -i - o >= 0 /\ g - o + 3 >= 0 /\ -g - o - 3 >= 0 /\ f - o - 3 >= 0 /\ -f - o + 3 >= 0 /\ d - o - 3 >= 0 /\ -d - o + 3 >= 0 /\ c - o >= 0 /\ -c - o >= 0 /\ b - o - 3 >= 0 /\ -b - o + 3 >= 0 /\ a - o - 3 >= 0 /\ -a - o + 3 >= 0 /\ o >= 0 /\ m + o - 3 >= 0 /\ -m + o + 3 >= 0 /\ i + o >= 0 /\ -i + o >= 0 /\ g + o + 3 >= 0 /\ -g + o - 3 >= 0 /\ f + o - 3 >= 0 /\ -f + o + 3 >= 0 /\ d + o - 3 >= 0 /\ -d + o + 3 >= 0 /\ c + o >= 0 /\ -c + o >= 0 /\ b + o - 3 >= 0 /\ -b + o + 3 >= 0 /\ a + o - 3 >= 0 /\ -a + o + 3 >= 0 /\ -m + 3 >= 0 /\ i - m + 3 >= 0 /\ -i - m + 3 >= 0 /\ g - m + 6 >= 0 /\ -g - m >= 0 /\ f - m >= 0 /\ -f - m + 6 >= 0 /\ d - m >= 0 /\ -d - m + 6 >= 0 /\ c - m + 3 >= 0 /\ -c - m + 3 >= 0 /\ b - m >= 0 /\ -b - m + 6 >= 0 /\ a - m >= 0 /\ -a - m + 6 >= 0 /\ m - 3 >= 0 /\ i + m - 3 >= 0 /\ -i + m - 3 >= 0 /\ g + m >= 0 /\ -g + m - 6 >= 0 /\ f + m - 6 >= 0 /\ -f + m >= 0 /\ d + m - 6 >= 0 /\ -d + m >= 0 /\ c + m - 3 >= 0 /\ -c + m - 3 >= 0 /\ b + m - 6 >= 0 /\ -b + m >= 0 /\ a + m - 6 >= 0 /\ -a + m >= 0 /\ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ m >= 1 /\ m >= o ] (1, 1) f25(a, b, c, d, f, g, i, m, o) -> f33(a, b, c, d, f, g, i, m, o) [ -i >= 0 /\ g - i + 3 >= 0 /\ -g - i - 3 >= 0 /\ f - i - 3 >= 0 /\ -f - i + 3 >= 0 /\ d - i - 3 >= 0 /\ -d - i + 3 >= 0 /\ c - i >= 0 /\ -c - i >= 0 /\ b - i - 3 >= 0 /\ -b - i + 3 >= 0 /\ a - i - 3 >= 0 /\ -a - i + 3 >= 0 /\ i >= 0 /\ g + i + 3 >= 0 /\ -g + i - 3 >= 0 /\ f + i - 3 >= 0 /\ -f + i + 3 >= 0 /\ d + i - 3 >= 0 /\ -d + i + 3 >= 0 /\ c + i >= 0 /\ -c + i >= 0 /\ b + i - 3 >= 0 /\ -b + i + 3 >= 0 /\ a + i - 3 >= 0 /\ -a + i + 3 >= 0 /\ -g - 3 >= 0 /\ f - g - 6 >= 0 /\ -f - g >= 0 /\ d - g - 6 >= 0 /\ -d - g >= 0 /\ c - g - 3 >= 0 /\ -c - g - 3 >= 0 /\ b - g - 6 >= 0 /\ -b - g >= 0 /\ a - g - 6 >= 0 /\ -a - g >= 0 /\ g + 3 >= 0 /\ f + g >= 0 /\ -f + g + 6 >= 0 /\ d + g >= 0 /\ -d + g + 6 >= 0 /\ c + g + 3 >= 0 /\ -c + g + 3 >= 0 /\ b + g >= 0 /\ -b + g + 6 >= 0 /\ a + g >= 0 /\ -a + g + 6 >= 0 /\ -f + 3 >= 0 /\ d - f >= 0 /\ -d - f + 6 >= 0 /\ c - f + 3 >= 0 /\ -c - f + 3 >= 0 /\ b - f >= 0 /\ -b - f + 6 >= 0 /\ a - f >= 0 /\ -a - f + 6 >= 0 /\ f - 3 >= 0 /\ d + f - 6 >= 0 /\ -d + f >= 0 /\ c + f - 3 >= 0 /\ -c + f - 3 >= 0 /\ b + f - 6 >= 0 /\ -b + f >= 0 /\ a + f - 6 >= 0 /\ -a + f >= 0 /\ -d + 3 >= 0 /\ c - d + 3 >= 0 /\ -c - d + 3 >= 0 /\ b - d >= 0 /\ -b - d + 6 >= 0 /\ a - d >= 0 /\ -a - d + 6 >= 0 /\ d - 3 >= 0 /\ c + d - 3 >= 0 /\ -c + d - 3 >= 0 /\ b + d - 6 >= 0 /\ -b + d >= 0 /\ a + d - 6 >= 0 /\ -a + d >= 0 /\ -c >= 0 /\ b - c - 3 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 3 >= 0 /\ -a - c + 3 >= 0 /\ c >= 0 /\ b + c - 3 >= 0 /\ -b + c + 3 >= 0 /\ a + c - 3 >= 0 /\ -a + c + 3 >= 0 /\ -b + 3 >= 0 /\ a - b >= 0 /\ -a - b + 6 >= 0 /\ b - 3 >= 0 /\ a + b - 6 >= 0 /\ -a + b >= 0 /\ -a + 3 >= 0 /\ a - 3 >= 0 /\ i >= g + 1 ] (1, 2) f0(a, b, c, d, f, g, i, m, o) -> f25(3, 3, 0, 3, 3, -3, 0, m, o) [ 0 >= 0 ] start location: f0 leaf cost: 3 Complexity upper bound ? Time: 4.090 sec (SMT: 2.098 sec)