MAYBE 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, s, t, 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, s, t, u, 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) [ 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) [ 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, t, 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) [ 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, t, 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) [ 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, t, 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, t, f + 1, j) [ b >= f ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-1) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-2) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-4) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, 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) [ f >= b + 1 ]", 0-0) = a S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-1) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-2) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-3) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-4) = 1 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ 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) [ 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, t, 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) [ 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) [ 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, t, 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, t, f + 1, j) [ b >= f ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-2) = 20*a + 2721200 S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-4) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, 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) [ f >= b + 1 ]", 0-0) = a S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-2) = 20*a + 8707840000000 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-3) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-4) = 1 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ 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, t, 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) [ 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, t, 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, t, f + 1, j) [ b >= f ]", 0-0) = a S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-1) = 20*a + 6800 S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-2) = 20*a + 2721200 S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-3) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ b >= f ]", 0-4) = ? S("f20(a, b, c, e, f, j) -> f20(a, b, c, t, 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) [ f >= b + 1 ]", 0-0) = a S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-1) = 20*a + 6800 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-2) = 20*a + 8707840000000 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-3) = ? S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f >= b + 1 ]", 0-4) = 1 S("f45(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ 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, t, f + 1, j) [ b >= f ] weakly and the transition f20(a, b, c, e, f, j) -> f20(a, b, c, t, 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) [ 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, t, 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_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_2 + X_5 - 2 >= 0 /\ X_1 + X_5 - 3 >= 0 /\ X_2 - X_3 + 1 >= 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_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_2 + X_5 - 2 >= 0 /\ X_1 + X_5 - 3 >= 0 /\ X_2 - X_3 + 1 >= 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_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_2 + X_5 - 2 >= 0 /\ X_1 + X_5 - 4 >= 0 /\ X_2 - X_3 + 1 >= 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_1 - X_2 - 2 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 4 >= 0 /\ X_1 - 3 >= 0 For symbol f60: X_5 - 1 >= 0 /\ X_3 + X_5 - 3 >= 0 /\ X_2 + X_5 - 2 >= 0 /\ X_1 + X_5 - 4 >= 0 /\ X_2 - X_3 + 1 >= 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_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) [ 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, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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) [ 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, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 By chaining the transition f2(a, b, c, e, f, j) -> f13(a, 1, c, e, f, j) [ a >= 2 ] with all transitions in problem 9, the following new transition is obtained: f2(a, b, c, e, f, j) -> f20(a, 1, 2, t, 1, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 ] We thus obtain the following problem: 10: T: (1, 2) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t, 1, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 ] (5*a + 4, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ 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, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 By chaining the transition f2(a, b, c, e, f, j) -> f20(a, 1, 2, t, 1, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 ] with all transitions in problem 10, the following new transition is obtained: f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] We thus obtain the following problem: 11: T: (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] (5*a + 4, 1) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ 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, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 By chaining the transition f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t, 1, j) [ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= b ] with all transitions in problem 11, the following new transition is obtained: f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t', 2, j) [ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= b /\ 0 >= 0 /\ 2*b - 2 >= 0 /\ b >= 1 ] We thus obtain the following problem: 12: T: (5*a + 4, 2) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t', 2, j) [ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= b /\ 0 >= 0 /\ 2*b - 2 >= 0 /\ b >= 1 ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 By chaining the transition f60(a, b, c, e, f, j) -> f13(a, b + 1, c, e, f, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 ] with all transitions in problem 12, the following new transition is obtained: f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t', 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 ] We thus obtain the following problem: 13: T: (20*a + 16, 3) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t', 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 ] (5*a + 4, 2) f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t', 2, j) [ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= b /\ 0 >= 0 /\ 2*b - 2 >= 0 /\ b >= 1 ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 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) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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 reachability in the complexity graph removes the following transition from problem 13: f13(a, b, c, e, f, j) -> f20(a, b, b + 1, t', 2, j) [ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= b /\ 0 >= 0 /\ 2*b - 2 >= 0 /\ b >= 1 ] We thus obtain the following problem: 14: T: (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (20*a + 16, 3) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t', 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ b >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t', 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 ] with all transitions in problem 14, the following new transition is obtained: f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] We thus obtain the following problem: 15: T: (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ b >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f31(a, b, c, e, f, j) -> f45(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 ] with all transitions in problem 15, the following new transition is obtained: f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] We thus obtain the following problem: 16: T: (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 ] with all transitions in problem 16, the following new transition is obtained: f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] We thus obtain the following problem: 17: T: (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 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, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 ] with all transitions in problem 17, the following new transition is obtained: f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] We thus obtain the following problem: 18: T: (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f20(a, b, c, e, f, j) -> f31(a, b, c, e, 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 ] with all transitions in problem 18, the following new transition is obtained: f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] We thus obtain the following problem: 19: T: (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] with all transitions in problem 19, the following new transitions are obtained: f20(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 ] f20(a, b, c, e, f, j) -> f31(a, b, c, e, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ b >= 2 ] We thus obtain the following problem: 20: T: (20*a + 16, 4) f20(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 ] (20*a + 16, 3) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ b >= 2 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f20(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 ] with all transitions in problem 20, the following new transition is obtained: f20(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 ] We thus obtain the following problem: 21: T: (20*a + 16, 5) f20(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 ] (20*a + 16, 3) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ b >= 2 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f20(a, b, c, e, f, j) -> f60(a, b, c, e, 1, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 ] with all transitions in problem 21, the following new transitions are obtained: f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ 1 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 0 /\ b + 1 >= 2 ] f20(a, b, c, e, f, j) -> f60(a, b, c, e, 2, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 ] We thus obtain the following problem: 22: T: (20*a + 16, 9) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ 1 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 0 /\ b + 1 >= 2 ] (20*a + 16, 6) f20(a, b, c, e, f, j) -> f60(a, b, c, e, 2, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 ] (20*a + 16, 3) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ b >= 2 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f20(a, b, c, e, f, j) -> f60(a, b, c, e, 2, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 ] with all transitions in problem 22, the following new transitions are obtained: f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ 2 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 0 /\ b + 1 >= 2 ] f20(a, b, c, e, f, j) -> f60(a, b, c, e, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 ] We thus obtain the following problem: 23: T: (20*a + 16, 10) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ 2 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 0 /\ b + 1 >= 2 ] (20*a + 16, 7) f20(a, b, c, e, f, j) -> f60(a, b, c, e, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 ] (20*a + 16, 9) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ 1 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 0 /\ b + 1 >= 2 ] (20*a + 16, 3) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ b >= 2 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f20(a, b, c, e, f, j) -> f60(a, b, c, e, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 ] with all transitions in problem 23, the following new transitions are obtained: f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ 3 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 2 ] f20(a, b, c, e, f, j) -> f60(a, b, c, e, 4, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ s >= 3 ] We thus obtain the following problem: 24: T: (20*a + 16, 11) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ 3 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 2 ] (20*a + 16, 8) f20(a, b, c, e, f, j) -> f60(a, b, c, e, 4, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ s >= 3 ] (20*a + 16, 10) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ 2 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 0 /\ b + 1 >= 2 ] (20*a + 16, 9) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ 1 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 0 /\ b + 1 >= 2 ] (20*a + 16, 3) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ b >= 2 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 By chaining the transition f20(a, b, c, e, f, j) -> f60(a, b, c, e, 4, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ s >= 3 ] with all transitions in problem 24, the following new transitions are obtained: f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ s >= 3 /\ 3 >= 0 /\ c + 1 >= 0 /\ b + 2 >= 0 /\ a >= 0 /\ 4 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 2 ] f20(a, b, c, e, f, j) -> f60(a, b, c, e, 5, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ s >= 3 /\ 3 >= 0 /\ c + 1 >= 0 /\ b + 2 >= 0 /\ a >= 0 /\ s >= 4 ] We thus obtain the following problem: 25: T: (20*a + 16, 12) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ s >= 3 /\ 3 >= 0 /\ c + 1 >= 0 /\ b + 2 >= 0 /\ a >= 0 /\ 4 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 2 ] (20*a + 16, 9) f20(a, b, c, e, f, j) -> f60(a, b, c, e, 5, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ s >= 3 /\ 3 >= 0 /\ c + 1 >= 0 /\ b + 2 >= 0 /\ a >= 0 /\ s >= 4 ] (20*a + 16, 11) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ s >= 2 /\ 2 >= 0 /\ c >= 0 /\ b + 1 >= 0 /\ 3 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 2 ] (20*a + 16, 10) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ s >= 1 /\ 2 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 0 /\ b + 1 >= 2 ] (20*a + 16, 9) f20(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, s) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ a >= c + 1 /\ 2 >= b + 1 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ 1 >= s + 1 /\ a + b - 2 >= 0 /\ a >= b + 1 /\ 2*b >= 0 /\ b + 1 >= 1 /\ b + 1 >= 0 /\ b + 1 >= 2 ] (20*a + 16, 3) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ 0 >= e + 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 /\ 1 >= 0 /\ c - 1 >= 0 /\ b >= 0 /\ a - 1 >= 0 /\ b >= 2 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ e >= 1 /\ f >= b + 1 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f20(a, b, c, e, f, j) -> f31(a, b, c, 0, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ f >= b + 1 /\ e = 0 /\ 0 >= 0 /\ b >= 1 ] (20*a + 16, 2) f31(a, b, c, e, f, j) -> f45(a, b, c, e, 2, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= c + 1 /\ f >= b + 1 /\ 0 >= 0 /\ a - 3 >= 0 /\ a - c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ a + b - 4 >= 0 /\ b >= 1 ] (20*a + 16, 4) f60(a, b, c, e, f, j) -> f20(a, b + 1, b + 2, t, 3, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= j + 1 /\ b >= 0 /\ a + b - 2 >= 0 /\ a - 2 >= 0 /\ a >= b + 1 /\ 0 >= 0 /\ 2*b >= 0 /\ b + 1 >= 1 /\ 1 >= 0 /\ b + 1 >= 0 /\ a - 1 >= 0 /\ b + 1 >= 2 ] (920*a^2 + 174156800170786*a + 139325440136040, 1) f20(a, b, c, e, f, j) -> f20(a, b, c, t, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (?, 1) f60(a, b, c, e, f, j) -> f60(a, b, c, e, f + 1, j) [ f - 1 >= 0 /\ c + f - 3 >= 0 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ j >= f ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 0 /\ f >= b + 1 ] (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 /\ b + f - 2 >= 0 /\ a + f - 4 >= 0 /\ b - c + 1 >= 0 /\ a - c - 1 >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 5 >= 0 /\ a - b - 2 >= 0 /\ b - 1 >= 0 /\ a + b - 4 >= 0 /\ a - 3 >= 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 /\ b + f - 2 >= 0 /\ a + f - 3 >= 0 /\ b - c + 1 >= 0 /\ a - c >= 0 /\ c - 2 >= 0 /\ b + c - 3 >= 0 /\ -b + c - 1 >= 0 /\ a + c - 4 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ b >= f ] (1, 3) f2(a, b, c, e, f, j) -> f20(a, 1, 2, t', 2, j) [ a >= 2 /\ a - 2 >= 0 /\ 0 >= 0 /\ a >= 1 /\ 1 >= 1 ] start location: f2 leaf cost: 4 Complexity upper bound ? Time: 5.959 sec (SMT: 5.106 sec)