YES(?, 522470403373181*a + 7370*a^2 + 417976322693833) Initial complexity problem: 1: T: (1, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f1(1, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a = 1 ] (1, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f13(a, 1, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ 0 >= a ] (1, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f13(a, 1, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= 2 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f20(a, b, b + 1, s, t, 1, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= b ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f20(a, b, c, d + s*t, e + u*v, f + 1, g, h, i, j, k, l, m, n, o, p, q, r) [ b >= f ] (?, 1) f31(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f31(a, b, c, d, e, f + 1, g, h, i, j, k, l, m, n, o, p, q, r) [ b >= f ] (?, 1) f45(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f45(a, b, c, d, e, f + 1, g + s*t, h + u*v, i + w*x, j, k, l, m, n, o, p, q, r) [ b >= f ] (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f60(a, b, c, d, e, f + 1, g, h, i, j, k - 1, s, t, u, v, k, q, r) [ j >= f ] (?, 1) f60(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f13(a, b + 1, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ f >= j + 1 ] (?, 1) f45(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f60(a, b, c, d, e, 1, g, h, i, s, b, l, m, n, o, p, t, u) [ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (?, 1) f31(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f1(a, b, a, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ f >= b + 1 /\ a = c ] (?, 1) f31(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f45(a, b, c, d, e, 1, s, t, u, j, k, l, m, n, o, p, q, r) [ a >= c + 1 /\ f >= b + 1 ] (?, 1) f31(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f45(a, b, c, d, e, 1, s, t, u, j, k, l, m, n, o, p, q, r) [ c >= a + 1 /\ f >= b + 1 ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f31(a, b, c, d, e, 1, g, h, i, j, k, l, m, n, o, p, q, r) [ 0 >= e + 1 /\ f >= b + 1 ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f31(a, b, c, d, e, 1, g, h, i, j, k, l, m, n, o, p, q, r) [ e >= 1 /\ f >= b + 1 ] (?, 1) f20(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f31(a, b, c, d, 0, 1, g, h, i, j, k, l, m, n, o, p, q, r) [ f >= b + 1 /\ e = 0 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ b >= a + 1 ] start location: f2 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, e, f, j]. We thus obtain the following problem: 2: T: (?, 1) f13(a, b, c, e, f, j) -> f1(a, b, c, e, f, j) [ b >= a + 1 ] (?, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\ e = 0 ] (?, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\ f >= b + 1 ] (?, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\ f >= b + 1 ] (?, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\ f >= b + 1 ] (?, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\ f >= b + 1 ] (?, 1) f31(a, b, c, e, f, j) -> f1(a, b, a, e, f, j) [ f >= b + 1 /\ a = c ] (?, 1) f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (?, 1) f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ] (?, 1) f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ] (?, 1) f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ] (?, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] (?, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ] (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ 0 >= a ] (1, 1) f2(a, b, c, e, f, j) -> f1(1, b, c, e, f, j) [ a = 1 ] start location: f2 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\ e = 0 ] (?, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\ f >= b + 1 ] (?, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\ f >= b + 1 ] (?, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\ f >= b + 1 ] (?, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\ f >= b + 1 ] (?, 1) f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (?, 1) f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ] (?, 1) f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ] (?, 1) f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ] (?, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] (?, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ] (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] start location: f2 leaf cost: 4 A polynomial rank function with Pol(f20) = 5*V_1 - 5*V_2 Pol(f31) = 5*V_1 - 5*V_2 - 1 Pol(f45) = 5*V_1 - 5*V_2 - 2 Pol(f60) = 5*V_1 - 5*V_2 - 3 Pol(f13) = 5*V_1 - 5*V_2 + 1 Pol(f2) = 5*V_1 - 4 orients all transitions weakly and the transition f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ] strictly and produces the following problem: 4: T: (?, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\ e = 0 ] (?, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\ f >= b + 1 ] (?, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\ f >= b + 1 ] (?, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\ f >= b + 1 ] (?, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\ f >= b + 1 ] (?, 1) f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (?, 1) f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ] (?, 1) f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ] (?, 1) f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ] (?, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] (5*a + 4, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ] (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] start location: f2 leaf cost: 4 A polynomial rank function with Pol(f60) = 1 Pol(f13) = 0 Pol(f45) = 2 Pol(f31) = 3 Pol(f20) = 4 and size complexities S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-0) = a S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-1) = 1 S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-2) = c S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-3) = e S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-4) = f S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-5) = j S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-0) = a S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-1) = ? S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-2) = ? S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-3) = ? S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-4) = 1 S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-1) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-2) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-4) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-5) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-0) = a S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-1) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-2) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-3) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-4) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-5) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-0) = a S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-1) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-2) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-3) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-4) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-5) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-0) = a S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-1) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-2) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-3) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-4) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-5) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-0) = a S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-1) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-2) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-3) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-4) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-5) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-0) = a S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-1) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-2) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-3) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-4) = 1 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-5) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-0) = a S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-1) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-2) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-3) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-5) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-0) = a S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-1) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-2) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-3) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-1) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-2) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-1) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-2) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-1) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-2) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-3) = 0 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-4) = 1 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-5) = ? orients the transitions f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ] f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ] f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ] f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\ f >= b + 1 ] f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\ f >= b + 1 ] f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ] f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\ f >= b + 1 ] f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\ f >= b + 1 ] f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\ e = 0 ] f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] weakly and the transitions f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ] f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\ f >= b + 1 ] f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\ f >= b + 1 ] f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\ f >= b + 1 ] f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\ f >= b + 1 ] f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\ e = 0 ] strictly and produces the following problem: 5: T: (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\ e = 0 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\ f >= b + 1 ] (20*a + 16, 1) f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (20*a + 16, 1) f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ] (?, 1) f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ] (?, 1) f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ] (?, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] (5*a + 4, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ] (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] start location: f2 leaf cost: 4 A polynomial rank function with Pol(f60) = V_1 + V_2 + V_3 - 2*V_5 Pol(f45) = V_2 - V_5 + 1 Pol(f31) = V_2 - V_5 + 1 Pol(f20) = V_1 + 3*V_2 + V_3 - V_5 and size complexities S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-0) = a S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-1) = 1 S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-2) = c S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-3) = e S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-4) = f S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-5) = j S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-0) = a S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-1) = 20*a + 6800 S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-2) = 20*a + 136060 S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-3) = ? S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-4) = 1 S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-2) = 20*a + 2721200 S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-4) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-5) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-0) = a S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-1) = 20*a + 6800 S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-2) = 20*a + 1088480000 S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-3) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-4) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-5) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-0) = a S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-1) = 20*a + 6800 S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-2) = 20*a + 435392000000 S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-3) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-4) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-5) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-0) = a S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-1) = 20*a + 6800 S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-2) = 20*a + 174156800000000 S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-3) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-4) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-5) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-0) = a S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-1) = 20*a + 6800 S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-2) = 20*a + 3483136000000000 S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-3) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-4) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-5) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-0) = a S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-2) = 20*a + 8707840000000 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-3) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-4) = 1 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-5) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-0) = a S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-2) = 20*a + 21769600000 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-3) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-5) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-0) = a S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-2) = 20*a + 21769600000 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-3) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-2) = 20*a + 54424000 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-2) = 20*a + 54424000 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-2) = 20*a + 54424000 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-3) = 0 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-4) = 1 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-5) = ? orients the transitions f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ] f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ] f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ] f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] weakly and the transitions f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ] f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ] strictly and produces the following problem: 6: T: (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\ e = 0 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\ f >= b + 1 ] (20*a + 16, 1) f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (20*a + 16, 1) f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ] (?, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] (5*a + 4, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ] (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] start location: f2 leaf cost: 4 A polynomial rank function with Pol(f60) = V_1 + V_2 + V_3 - 2*V_5 Pol(f20) = V_2 - V_5 + 1 and size complexities S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-0) = a S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-1) = 1 S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-2) = c S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-3) = e S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-4) = f S("f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ]", 0-5) = j S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-0) = a S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-1) = 20*a + 6800 S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-2) = 20*a + 136060 S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-3) = ? S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-4) = 1 S("f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-2) = 20*a + 2721200 S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-4) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ]", 0-5) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-0) = a S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-1) = 20*a + 6800 S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-2) = 20*a + 1088480000 S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-3) = ? S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-4) = 3225*a^2 + 174156801601125*a + 139325441278837 S("f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ]", 0-5) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-0) = a S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-1) = 20*a + 6800 S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-2) = 20*a + 435392000000 S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-3) = ? S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-4) = 3225*a^2 + 174156801601125*a + 139325441278837 S("f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ]", 0-5) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-0) = a S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-1) = 20*a + 6800 S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-2) = 20*a + 174156800000000 S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-3) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-4) = ? S("f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ]", 0-5) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-0) = a S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-1) = 20*a + 6800 S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-2) = 20*a + 3483136000000000 S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-3) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-4) = ? S("f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ]", 0-5) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-0) = a S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-2) = 20*a + 8707840000000 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-3) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-4) = 1 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\\ 3*v >= b + 2 /\\ v >= s /\\ b + 1 >= 2*w /\\ 3*w >= b + 2 /\\ s >= w /\\ f >= b + 1 ]", 0-5) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-0) = a S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-2) = 20*a + 21769600000 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-3) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\\ f >= b + 1 ]", 0-5) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-0) = a S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-2) = 20*a + 21769600000 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-3) = ? S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\\ f >= b + 1 ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-2) = 20*a + 54424000 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\\ f >= b + 1 ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-2) = 20*a + 54424000 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-4) = 1 S("f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\\ f >= b + 1 ]", 0-5) = ? S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-2) = 20*a + 54424000 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-3) = 0 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-4) = 1 S("f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\\ e = 0 ]", 0-5) = ? orients the transitions f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ] f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] weakly and the transition f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] strictly and produces the following problem: 7: T: (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f >= b + 1 /\ e = 0 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ e >= 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ 0 >= e + 1 /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ c >= a + 1 /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ a >= c + 1 /\ f >= b + 1 ] (20*a + 16, 1) f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (20*a + 16, 1) f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f >= j + 1 ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ j >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ b >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ b >= f ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ b >= f ] (5*a + 4, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a >= b ] (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] start location: f2 leaf cost: 4 Applied AI with 'oct' on problem 7 to obtain the following invariants: For symbol f13: -X_2 + 2 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0 For symbol f20: X_5 - 1 >= 0 /\ X_3 + X_5 - 3 >= 0 /\ -X_3 + X_5 + 2 >= 0 /\ X_2 + X_5 - 2 >= 0 /\ -X_2 + X_5 + 1 >= 0 /\ X_1 + X_5 - 3 >= 0 /\ -X_3 + 3 >= 0 /\ X_2 - X_3 + 1 >= 0 /\ -X_2 - X_3 + 5 >= 0 /\ X_1 - X_3 >= 0 /\ X_3 - 2 >= 0 /\ X_2 + X_3 - 3 >= 0 /\ -X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 4 >= 0 /\ -X_2 + 2 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0 For symbol f31: X_5 - 1 >= 0 /\ X_3 + X_5 - 3 >= 0 /\ -X_3 + X_5 + 2 >= 0 /\ X_2 + X_5 - 2 >= 0 /\ -X_2 + X_5 + 1 >= 0 /\ X_1 + X_5 - 3 >= 0 /\ -X_3 + 3 >= 0 /\ X_2 - X_3 + 1 >= 0 /\ -X_2 - X_3 + 5 >= 0 /\ X_1 - X_3 >= 0 /\ X_3 - 2 >= 0 /\ X_2 + X_3 - 3 >= 0 /\ -X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 4 >= 0 /\ -X_2 + 2 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0 For symbol f45: X_5 - 1 >= 0 /\ X_3 + X_5 - 3 >= 0 /\ -X_3 + X_5 + 2 >= 0 /\ X_2 + X_5 - 2 >= 0 /\ -X_2 + X_5 + 1 >= 0 /\ X_1 + X_5 - 4 >= 0 /\ -X_3 + 3 >= 0 /\ X_2 - X_3 + 1 >= 0 /\ -X_2 - X_3 + 5 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 - 2 >= 0 /\ X_2 + X_3 - 3 >= 0 /\ -X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 5 >= 0 /\ -X_2 + 2 >= 0 /\ X_1 - X_2 - 2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 3 >= 0 For symbol f60: -X_6 + 1 >= 0 /\ X_5 - X_6 >= 0 /\ X_3 - X_6 - 1 >= 0 /\ -X_3 - X_6 + 3 >= 0 /\ X_2 - X_6 >= 0 /\ -X_2 - X_6 + 2 >= 0 /\ X_1 - X_6 - 2 >= 0 /\ X_6 - 1 >= 0 /\ X_5 + X_6 - 2 >= 0 /\ X_3 + X_6 - 3 >= 0 /\ -X_3 + X_6 + 1 >= 0 /\ X_2 + X_6 - 2 >= 0 /\ -X_2 + X_6 >= 0 /\ X_1 + X_6 - 4 >= 0 /\ X_5 - 1 >= 0 /\ X_3 + X_5 - 3 >= 0 /\ -X_3 + X_5 + 1 >= 0 /\ X_2 + X_5 - 2 >= 0 /\ -X_2 + X_5 >= 0 /\ X_1 + X_5 - 4 >= 0 /\ -X_3 + 2 >= 0 /\ X_2 - X_3 + 1 >= 0 /\ -X_2 - X_3 + 3 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ X_3 - 2 >= 0 /\ X_2 + X_3 - 3 >= 0 /\ -X_2 + X_3 - 1 >= 0 /\ X_1 + X_3 - 5 >= 0 /\ -X_2 + 1 >= 0 /\ X_1 - X_2 - 2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 3 >= 0 This yielded the following problem: 8: T: (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] (5*a + 4, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= b ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 4 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 2 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ -j + 1 >= 0 /\ f - j >= 0 /\ c - j - 1 >= 0 /\ -c - j + 3 >= 0 /\ b - j >= 0 /\ -b - j + 2 >= 0 /\ a - j - 2 >= 0 /\ j - 1 >= 0 /\ f + j - 2 >= 0 /\ c + j - 3 >= 0 /\ -c + j + 1 >= 0 /\ b + j - 2 >= 0 /\ -b + j >= 0 /\ a + j - 4 >= 0 /\ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 1 >= 0 /\ b + f - 2 >= 0 /\ -b + f >= 0 /\ a + f - 4 >= 0 /\ -c + 2 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 1 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (20*a + 16, 1) f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ -j + 1 >= 0 /\ f - j >= 0 /\ c - j - 1 >= 0 /\ -c - j + 3 >= 0 /\ b - j >= 0 /\ -b - j + 2 >= 0 /\ a - j - 2 >= 0 /\ j - 1 >= 0 /\ f + j - 2 >= 0 /\ c + j - 3 >= 0 /\ -c + j + 1 >= 0 /\ b + j - 2 >= 0 /\ -b + j >= 0 /\ a + j - 4 >= 0 /\ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 1 >= 0 /\ b + f - 2 >= 0 /\ -b + f >= 0 /\ a + f - 4 >= 0 /\ -c + 2 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 1 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 ] (20*a + 16, 1) f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 4 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 2 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ c >= a + 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 ] start location: f2 leaf cost: 4 Testing for unsatisfiable constraints removes the following transition from problem 8: f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ c >= a + 1 /\ f >= b + 1 ] We thus obtain the following problem: 9: T: (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] (5*a + 4, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= b ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 4 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 2 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ -j + 1 >= 0 /\ f - j >= 0 /\ c - j - 1 >= 0 /\ -c - j + 3 >= 0 /\ b - j >= 0 /\ -b - j + 2 >= 0 /\ a - j - 2 >= 0 /\ j - 1 >= 0 /\ f + j - 2 >= 0 /\ c + j - 3 >= 0 /\ -c + j + 1 >= 0 /\ b + j - 2 >= 0 /\ -b + j >= 0 /\ a + j - 4 >= 0 /\ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 1 >= 0 /\ b + f - 2 >= 0 /\ -b + f >= 0 /\ a + f - 4 >= 0 /\ -c + 2 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 1 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (20*a + 16, 1) f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ -j + 1 >= 0 /\ f - j >= 0 /\ c - j - 1 >= 0 /\ -c - j + 3 >= 0 /\ b - j >= 0 /\ -b - j + 2 >= 0 /\ a - j - 2 >= 0 /\ j - 1 >= 0 /\ f + j - 2 >= 0 /\ c + j - 3 >= 0 /\ -c + j + 1 >= 0 /\ b + j - 2 >= 0 /\ -b + j >= 0 /\ a + j - 4 >= 0 /\ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 1 >= 0 /\ b + f - 2 >= 0 /\ -b + f >= 0 /\ a + f - 4 >= 0 /\ -c + 2 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 1 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 ] (20*a + 16, 1) f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 4 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 2 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 ] start location: f2 leaf cost: 4 Repeatedly propagating knowledge in problem 9 produces the following problem: 10: T: (1, 1) f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] (5*a + 4, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= b ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, e + u*v, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f31(a, b, c, e, f, j) -> f31(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (3225*a^2 + 174156801601125*a + 139325441278836, 1) f45(a, b, c, e, f, j) -> f45(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 4 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 2 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ b >= f ] (20*a + 16, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ -j + 1 >= 0 /\ f - j >= 0 /\ c - j - 1 >= 0 /\ -c - j + 3 >= 0 /\ b - j >= 0 /\ -b - j + 2 >= 0 /\ a - j - 2 >= 0 /\ j - 1 >= 0 /\ f + j - 2 >= 0 /\ c + j - 3 >= 0 /\ -c + j + 1 >= 0 /\ b + j - 2 >= 0 /\ -b + j >= 0 /\ a + j - 4 >= 0 /\ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 1 >= 0 /\ b + f - 2 >= 0 /\ -b + f >= 0 /\ a + f - 4 >= 0 /\ -c + 2 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 1 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (20*a + 16, 1) f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ -j + 1 >= 0 /\ f - j >= 0 /\ c - j - 1 >= 0 /\ -c - j + 3 >= 0 /\ b - j >= 0 /\ -b - j + 2 >= 0 /\ a - j - 2 >= 0 /\ j - 1 >= 0 /\ f + j - 2 >= 0 /\ c + j - 3 >= 0 /\ -c + j + 1 >= 0 /\ b + j - 2 >= 0 /\ -b + j >= 0 /\ a + j - 4 >= 0 /\ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 1 >= 0 /\ b + f - 2 >= 0 /\ -b + f >= 0 /\ a + f - 4 >= 0 /\ -c + 2 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 3 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 1 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 ] (20*a + 16, 1) f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 4 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ -b + 2 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ b + 1 >= 2*v /\ 3*v >= b + 2 /\ v >= s /\ b + 1 >= 2*w /\ 3*w >= b + 2 /\ s >= w /\ f >= b + 1 ] (20*a + 16, 1) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 ] (20*a + 16, 1) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ -c + f + 2 >= 0 /\ b + f - 2 >= 0 /\ -b + f + 1 >= 0 /\ a + f - 3 >= 0 /\ -c + 3 >= 0 /\ b - c + 1 >= 0 /\ -b - c + 5 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ -b + 2 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 ] start location: f2 leaf cost: 4 Complexity upper bound 522470403373181*a + 7370*a^2 + 417976322693833 Time: 1.953 sec (SMT: 1.800 sec)