MAYBE Initial complexity problem: 1: T: (?, 1) f25(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f15(a, b, c + 1, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ a >= b + 1 ] (?, 1) f25(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f15(a, b, c + 1, y, 0, 1, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ b >= a ] (?, 1) f31(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f31(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f36(a, b, 1, d, e, f, 0, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f36(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f45(a, b, c, d, e, f, g, h, y, z, a1, b1, b1, n, o, p, q, r, s, t, u, v, w, x) [ h >= c ] (?, 1) f45(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f46(a, b, c, d, e, f, g, h, i, j, k, l, m, m, o, p, q, r, s, t, u, v, w, x) [ 0 >= m + 1 ] (?, 1) f45(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f46(a, b, c, d, e, f, g, h, i, j, k, l, m, m, o, p, q, r, s, t, u, v, w, x) [ m >= 1 ] (?, 1) f46(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f36(a, b, c + 1, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ a >= b + 1 ] (?, 1) f45(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f36(a, b, c + 1, d, e, f, g, h, i, j, k, l, 0, 0, o, p, q, r, s, t, u, v, w, x) [ m = 0 ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f63(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f65(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) (?, 1) f46(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f36(a, b, c + 1, y, 0, f, g, h, i, j, k, l, m, n, z, p, q, r, s, t, u, v, w, x) [ b >= a ] (?, 1) f46(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f45(a, b, c, d, e, f, g, h, i, y, z, a1, a1, n, o, b1, q, r, s, t, u, v, w, x) [ b >= a ] (?, 1) f36(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, 0, r, s, t, u, v, w, x) [ c >= h + 1 ] (?, 1) f15(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f25(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, y, z, a1, a1, a1, x) [ 0 >= a1 + 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f25(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, y, z, a1, a1, a1, x) [ a1 >= 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f15(a, b, c + 1, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, y, z, 0, 0, 0, x) [ r >= c + 1 ] (?, 1) f15(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f31(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) [ c >= r ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f15(a, b, 0, d, e, f, 0, z, i, j, k, l, m, n, o, p, 0, y, s, t, u, v, w, 1) (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f36(a, b, 1, d, e, f, 0, a1, i, j, k, l, m, n, o, p, 0, z, s, t, u, v, w, y) [ 0 >= y ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x) -> f36(a, b, 1, d, e, f, 0, a1, i, j, k, l, m, n, o, p, 0, z, s, t, u, v, w, y) [ y >= 2 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, h, m, r]. We thus obtain the following problem: 2: T: (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ y >= 2 ] (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ 0 >= y ] (1, 1) f0(a, b, c, h, m, r) -> f15(a, b, 0, z, m, y) (?, 1) f15(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) [ c >= r ] (?, 1) f15(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ a1 >= 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ 0 >= a1 + 1 /\ r >= c + 1 ] (?, 1) f36(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c >= h + 1 ] (?, 1) f46(a, b, c, h, m, r) -> f45(a, b, c, h, a1, r) [ b >= a ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ b >= a ] (?, 1) f63(a, b, c, h, m, r) -> f65(a, b, c, h, m, r) (?, 1) f61(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) (?, 1) f45(a, b, c, h, m, r) -> f36(a, b, c + 1, h, 0, r) [ m = 0 ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ a >= b + 1 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ m >= 1 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ 0 >= m + 1 ] (?, 1) f36(a, b, c, h, m, r) -> f45(a, b, c, h, b1, r) [ h >= c ] (?, 1) f33(a, b, c, h, m, r) -> f36(a, b, 1, h, m, r) (?, 1) f31(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ b >= a ] (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ a >= b + 1 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ y >= 2 ] (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ 0 >= y ] (1, 1) f0(a, b, c, h, m, r) -> f15(a, b, 0, z, m, y) (?, 1) f15(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) [ c >= r ] (?, 1) f15(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ a1 >= 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ 0 >= a1 + 1 /\ r >= c + 1 ] (?, 1) f36(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c >= h + 1 ] (?, 1) f46(a, b, c, h, m, r) -> f45(a, b, c, h, a1, r) [ b >= a ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ b >= a ] (?, 1) f61(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) (?, 1) f45(a, b, c, h, m, r) -> f36(a, b, c + 1, h, 0, r) [ m = 0 ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ a >= b + 1 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ m >= 1 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ 0 >= m + 1 ] (?, 1) f36(a, b, c, h, m, r) -> f45(a, b, c, h, b1, r) [ h >= c ] (?, 1) f33(a, b, c, h, m, r) -> f36(a, b, 1, h, m, r) (?, 1) f31(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ b >= a ] (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ a >= b + 1 ] start location: f0 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 3: f33(a, b, c, h, m, r) -> f36(a, b, 1, h, m, r) We thus obtain the following problem: 4: T: (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ a >= b + 1 ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ b >= a ] (?, 1) f46(a, b, c, h, m, r) -> f45(a, b, c, h, a1, r) [ b >= a ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ 0 >= m + 1 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ m >= 1 ] (?, 1) f45(a, b, c, h, m, r) -> f36(a, b, c + 1, h, 0, r) [ m = 0 ] (?, 1) f61(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ a >= b + 1 ] (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ b >= a ] (?, 1) f31(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ 0 >= a1 + 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ a1 >= 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) [ c >= r ] (?, 1) f36(a, b, c, h, m, r) -> f45(a, b, c, h, b1, r) [ h >= c ] (?, 1) f36(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c >= h + 1 ] (1, 1) f0(a, b, c, h, m, r) -> f15(a, b, 0, z, m, y) (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ 0 >= y ] (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ y >= 2 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f46) = 1 Pol(f36) = 1 Pol(f45) = 1 Pol(f61) = 0 Pol(f25) = 1 Pol(f15) = 1 Pol(f31) = 0 Pol(f0) = 1 orients all transitions weakly and the transitions f36(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c >= h + 1 ] f15(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) [ c >= r ] strictly and produces the following problem: 5: T: (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ a >= b + 1 ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ b >= a ] (?, 1) f46(a, b, c, h, m, r) -> f45(a, b, c, h, a1, r) [ b >= a ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ 0 >= m + 1 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ m >= 1 ] (?, 1) f45(a, b, c, h, m, r) -> f36(a, b, c + 1, h, 0, r) [ m = 0 ] (?, 1) f61(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ a >= b + 1 ] (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ b >= a ] (?, 1) f31(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ 0 >= a1 + 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ a1 >= 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ r >= c + 1 ] (1, 1) f15(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) [ c >= r ] (?, 1) f36(a, b, c, h, m, r) -> f45(a, b, c, h, b1, r) [ h >= c ] (1, 1) f36(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c >= h + 1 ] (1, 1) f0(a, b, c, h, m, r) -> f15(a, b, 0, z, m, y) (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ 0 >= y ] (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ y >= 2 ] start location: f0 leaf cost: 1 Applied AI with 'oct' on problem 5 to obtain the following invariants: For symbol f15: X_3 >= 0 For symbol f25: X_6 - 1 >= 0 /\ X_3 + X_6 - 1 >= 0 /\ -X_3 + X_6 - 1 >= 0 /\ X_3 >= 0 For symbol f31: X_3 - X_6 >= 0 /\ X_3 >= 0 For symbol f36: X_3 - 1 >= 0 For symbol f45: X_4 - 1 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ -X_3 + X_4 >= 0 /\ X_3 - 1 >= 0 For symbol f46: X_4 - 1 >= 0 /\ X_3 + X_4 - 2 >= 0 /\ -X_3 + X_4 >= 0 /\ X_3 - 1 >= 0 For symbol f61: X_3 - X_4 - 1 >= 0 /\ X_3 - 1 >= 0 This yielded the following problem: 6: T: (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ y >= 2 ] (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ 0 >= y ] (1, 1) f0(a, b, c, h, m, r) -> f15(a, b, 0, z, m, y) (1, 1) f36(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c - 1 >= 0 /\ c >= h + 1 ] (?, 1) f36(a, b, c, h, m, r) -> f45(a, b, c, h, b1, r) [ c - 1 >= 0 /\ h >= c ] (1, 1) f15(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) [ c >= 0 /\ c >= r ] (?, 1) f15(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ c >= 0 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ c >= 0 /\ a1 >= 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ c >= 0 /\ 0 >= a1 + 1 /\ r >= c + 1 ] (?, 1) f31(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) [ c - r >= 0 /\ c >= 0 ] (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ r - 1 >= 0 /\ c + r - 1 >= 0 /\ -c + r - 1 >= 0 /\ c >= 0 /\ b >= a ] (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ r - 1 >= 0 /\ c + r - 1 >= 0 /\ -c + r - 1 >= 0 /\ c >= 0 /\ a >= b + 1 ] (?, 1) f61(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c - h - 1 >= 0 /\ c - 1 >= 0 ] (?, 1) f45(a, b, c, h, m, r) -> f36(a, b, c + 1, h, 0, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ m = 0 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ m >= 1 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ 0 >= m + 1 ] (?, 1) f46(a, b, c, h, m, r) -> f45(a, b, c, h, a1, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ b >= a ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ b >= a ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ a >= b + 1 ] start location: f0 leaf cost: 1 By chaining the transition f36(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c - 1 >= 0 /\ c >= h + 1 ] with all transitions in problem 6, the following new transition is obtained: f36(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c - 1 >= 0 /\ c >= h + 1 /\ c - h - 1 >= 0 ] We thus obtain the following problem: 7: T: (1, 2) f36(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c - 1 >= 0 /\ c >= h + 1 /\ c - h - 1 >= 0 ] (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ y >= 2 ] (1, 1) f0(a, b, c, h, m, r) -> f36(a, b, 1, a1, m, z) [ 0 >= y ] (1, 1) f0(a, b, c, h, m, r) -> f15(a, b, 0, z, m, y) (?, 1) f36(a, b, c, h, m, r) -> f45(a, b, c, h, b1, r) [ c - 1 >= 0 /\ h >= c ] (1, 1) f15(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) [ c >= 0 /\ c >= r ] (?, 1) f15(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ c >= 0 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ c >= 0 /\ a1 >= 1 /\ r >= c + 1 ] (?, 1) f15(a, b, c, h, m, r) -> f25(a, b, c, h, m, r) [ c >= 0 /\ 0 >= a1 + 1 /\ r >= c + 1 ] (?, 1) f31(a, b, c, h, m, r) -> f31(a, b, c, h, m, r) [ c - r >= 0 /\ c >= 0 ] (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ r - 1 >= 0 /\ c + r - 1 >= 0 /\ -c + r - 1 >= 0 /\ c >= 0 /\ b >= a ] (?, 1) f25(a, b, c, h, m, r) -> f15(a, b, c + 1, h, m, r) [ r - 1 >= 0 /\ c + r - 1 >= 0 /\ -c + r - 1 >= 0 /\ c >= 0 /\ a >= b + 1 ] (?, 1) f61(a, b, c, h, m, r) -> f61(a, b, c, h, m, r) [ c - h - 1 >= 0 /\ c - 1 >= 0 ] (?, 1) f45(a, b, c, h, m, r) -> f36(a, b, c + 1, h, 0, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ m = 0 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ m >= 1 ] (?, 1) f45(a, b, c, h, m, r) -> f46(a, b, c, h, m, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ 0 >= m + 1 ] (?, 1) f46(a, b, c, h, m, r) -> f45(a, b, c, h, a1, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ b >= a ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ b >= a ] (?, 1) f46(a, b, c, h, m, r) -> f36(a, b, c + 1, h, m, r) [ h - 1 >= 0 /\ c + h - 2 >= 0 /\ -c + h >= 0 /\ c - 1 >= 0 /\ a >= b + 1 ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 1.858 sec (SMT: 1.660 sec)