YES(?, 52*h + 52*i + 3*p + 6*q + 16*j + 16*k + a + 50) 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, s, t, u, v, w) -> f13(1, x, y, z, a1, b1, c1, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ a = 1 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ h >= i ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f16(a, b, c, d, e, f, g, h, i, j, k + 1, l + 2, m, n, o, p, q, r, s, t, u, v, w) [ j >= k ] (1, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f27(a, x, y, z, a1, b1, c1, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ 0 >= a ] (1, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f27(a, x, y, z, a1, b1, c1, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ a >= 2 ] (?, 1) f27(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f35(a, b, c, d, e, f, g, h, i, j, k, l, h - i + 2, 1, 0, p, q, r, s, t, u, v, w) [ 0 >= i /\ h >= i ] (?, 1) f27(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f35(a, b, c, d, e, f, g, h, i, j, k, l, h - i + 2, 1, 0, p, q, r, s, t, u, v, w) [ i >= 2 /\ h >= i ] (?, 1) f27(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f35(a, b, c, d, e, f, g, h, 1, j, k, l, 1, 1, 0, p, q, r, s, t, u, v, w) [ h >= 1 /\ i = 1 ] (?, 1) f35(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ 0 >= q /\ j >= k ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ q >= 2 /\ j >= k ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f38(a, b, c, d, e, f, g, h, i, j, k + 1, x + 3, m, n, o, p, 1, b*y + b*z, a1*b - b*b1, c*c1 - c*d1, -c*e1 - c*f1, v, w) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f38(a, b, c, d, e, f, g, h, i, j, k + 1, x + 3, m, n, o, p, 1, b*y + b*z, a1*b - b*b1, c*c1 - c*d1, -c*e1 - c*f1, v, w) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f38(a, b, c, d, e, f, g, h, i, j, 2, 1, m, n, o, p, 1, b*x + b*y, b*z - a1*b, b1*c - c*c1, -c*d1 - c*e1, v, w) [ j >= 1 /\ k = 1 /\ q = 1 ] (?, 1) f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f38(a, b, c, d, e, f, g, h, i, j, k + 1, j - k + 2, m, n, o, p, q, b*x + b*y, b*z - a1*b, b1*c - c*c1, -c*d1 - c*e1, p - f1 + 3, w) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (?, 1) f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f38(a, b, c, d, e, f, g, h, i, j, k + 1, j - k + 2, m, n, o, p, q, b*x + b*y, b*z - a1*b, b1*c - c*c1, -c*d1 - c*e1, p - f1 + 3, w) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f38(a, b, c, d, e, f, g, h, i, j, 2, 1, m, n, o, p, q, b*x + b*y, b*z - a1*b, b1*c - c*c1, -c*d1 - c*e1, p - f1 + 3, w) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f38(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f35(a, b, c, d, n, f, g, h, i, j, k, l, m, f*n - g*o + n, f*o + g*n + o, p, q + 1, r, s, t, u, v, w + 2) [ k >= j + 1 ] (?, 1) f35(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f27(a, b, c, d, e, f, g, h, i + 1, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (?, 1) f27(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ 0 >= a + 2 /\ i >= h + 1 ] (?, 1) f27(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ a >= 0 /\ i >= h + 1 ] (?, 1) f27(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f1(-1, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ i >= h + 1 /\ a + 1 = 0 ] (?, 1) f16(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f13(a, b, c, d, e, f, g, h, i + 1, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ k >= j + 1 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) -> f27(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w) [ i >= h + 1 ] start location: f2 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, h, i, j, k, p, q]. We thus obtain the following problem: 2: T: (?, 1) f13(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ i >= h + 1 ] (?, 1) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (?, 1) f27(a, h, i, j, k, p, q) -> f1(-1, h, i, j, k, p, q) [ i >= h + 1 /\ a + 1 = 0 ] (?, 1) f27(a, h, i, j, k, p, q) -> f1(a, h, i, j, k, p, q) [ a >= 0 /\ i >= h + 1 ] (?, 1) f27(a, h, i, j, k, p, q) -> f1(a, h, i, j, k, p, q) [ 0 >= a + 2 /\ i >= h + 1 ] (?, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (?, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (?, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ 0 >= q /\ j >= k ] (?, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (?, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (?, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (?, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (?, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (?, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ 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) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (?, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (?, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (?, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (?, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (?, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (?, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (?, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (?, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ] start location: f2 leaf cost: 5 A polynomial rank function with Pol(f16) = 2*V_2 - 2*V_3 Pol(f13) = 2*V_2 - 2*V_3 + 1 Pol(f35) = 2*V_2 - 2*V_3 Pol(f27) = 2*V_2 - 2*V_3 + 1 Pol(f38) = 2*V_2 - 2*V_3 Pol(f53) = 2*V_2 - 2*V_3 Pol(f2) = 2*V_2 - 2*V_3 + 1 orients all transitions weakly and the transitions f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] strictly and produces the following problem: 4: T: (?, 1) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (?, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (?, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (?, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (?, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (2*h + 2*i + 1, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ] start location: f2 leaf cost: 5 A polynomial rank function with Pol(f53) = -6 Pol(f38) = -6 Pol(f35) = -6 Pol(f27) = -7 Pol(f16) = 1 Pol(f13) = 0 and size complexities S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-0) = 1 S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-1) = h S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-2) = i S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-3) = j S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-4) = k S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-5) = p S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-6) = q S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-0) = 1 S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-1) = h S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-2) = ? S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-3) = j S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-4) = ? S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-5) = p S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-6) = q S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-0) = 1 S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-1) = h S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-2) = ? S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-3) = j S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-4) = ? S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-5) = p S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-6) = q S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-0) = a S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-1) = h S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-2) = i S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-3) = j S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-4) = k S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-5) = p S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-6) = q S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-0) = a S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-1) = h S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-2) = i S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-3) = j S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-4) = k S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-5) = p S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-6) = q S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-0) = a S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-1) = h S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-2) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-3) = j S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-4) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-5) = p S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-6) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-0) = a S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-1) = h S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-2) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-3) = j S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-4) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-5) = p S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-6) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-0) = a S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-1) = h S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-2) = 1 S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-3) = j S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-4) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-5) = p S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-6) = ? S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-0) = a S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-1) = h S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-2) = ? S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-3) = j S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-4) = ? S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-5) = p S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-6) = ? S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-4) = ? S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-6) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-4) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-6) = 1 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-4) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-6) = 1 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-4) = 2 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-6) = 1 S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-0) = a S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-1) = h S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-2) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-3) = j S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-4) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-5) = p S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-6) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-0) = a S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-1) = h S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-2) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-3) = j S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-4) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-5) = p S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-6) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-0) = a S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-1) = h S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-2) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-3) = j S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-4) = 2 S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-5) = p S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-6) = ? S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-4) = ? S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-6) = ? S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-0) = a S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-1) = h S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-2) = ? S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-3) = j S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-4) = ? S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-5) = p S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-6) = ? S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-0) = 1 S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-1) = h S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-2) = ? S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-3) = j S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-4) = ? S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-5) = p S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-6) = q orients the transitions f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] weakly and the transition f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] strictly and produces the following problem: 5: T: (38*h + 38*i + 19, 1) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (?, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (?, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (?, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (?, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (2*h + 2*i + 1, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ] start location: f2 leaf cost: 5 A polynomial rank function with Pol(f53) = 1 Pol(f38) = 1 Pol(f35) = 1 Pol(f27) = 0 Pol(f16) = 0 and size complexities S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-0) = 1 S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-1) = h S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-2) = i S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-3) = j S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-4) = k S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-5) = p S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-6) = q S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-0) = 1 S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-1) = h S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-2) = 39*h + 39*i + 28899 S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-3) = j S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-4) = ? S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-5) = p S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-6) = q S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-0) = 1 S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-1) = h S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-2) = 39*h + 39*i + 28899 S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-3) = j S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-4) = ? S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-5) = p S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-6) = q S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-0) = a S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-1) = h S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-2) = i S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-3) = j S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-4) = k S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-5) = p S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-6) = q S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-0) = a S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-1) = h S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-2) = i S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-3) = j S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-4) = k S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-5) = p S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-6) = q S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-0) = a S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-1) = h S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-2) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-3) = j S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-4) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-5) = p S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-6) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-0) = a S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-1) = h S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-2) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-3) = j S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-4) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-5) = p S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-6) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-0) = a S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-1) = h S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-2) = 1 S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-3) = j S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-4) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-5) = p S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-6) = ? S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-0) = a S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-1) = h S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-2) = ? S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-3) = j S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-4) = ? S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-5) = p S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-6) = ? S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-4) = ? S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-6) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-4) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-6) = 1 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-4) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-6) = 1 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-4) = 2 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-6) = 1 S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-0) = a S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-1) = h S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-2) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-3) = j S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-4) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-5) = p S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-6) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-0) = a S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-1) = h S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-2) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-3) = j S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-4) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-5) = p S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-6) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-0) = a S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-1) = h S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-2) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-3) = j S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-4) = 2 S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-5) = p S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-6) = ? S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-2) = ? S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-4) = ? S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-6) = ? S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-0) = a S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-1) = h S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-2) = ? S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-3) = j S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-4) = ? S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-5) = p S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-6) = ? S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-0) = 1 S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-1) = h S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-2) = 39*h + 39*i + 28899 S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-3) = j S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-4) = ? S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-5) = p S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-6) = q orients the transitions f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] weakly and the transition f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] strictly and produces the following problem: 6: T: (38*h + 38*i + 19, 1) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (6*h + 6*i + 3, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (?, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (?, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (?, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (2*h + 2*i + 1, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ] start location: f2 leaf cost: 5 A polynomial rank function with Pol(f16) = 2*V_4 - 2*V_5 + 1 Pol(f13) = 2*V_4 - 2*V_5 + 1 Pol(f35) = V_1 + 2*V_4 - 2*V_5 Pol(f27) = V_1 + 2*V_4 - 2*V_5 Pol(f38) = V_1 + 2*V_4 - 2*V_5 Pol(f53) = V_1 + 2*V_4 - 2*V_5 - 1 Pol(f2) = V_1 + 2*V_4 - 2*V_5 orients all transitions weakly and the transition f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] strictly and produces the following problem: 7: T: (38*h + 38*i + 19, 1) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (6*h + 6*i + 3, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (?, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (?, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (a + 2*j + 2*k, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (2*h + 2*i + 1, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ] start location: f2 leaf cost: 5 A polynomial rank function with Pol(f16) = 3*V_1 + V_6 - 2*V_7 Pol(f13) = 3*V_1 + V_6 - 2*V_7 Pol(f35) = V_6 - 2*V_7 + 3 Pol(f27) = V_6 - 2*V_7 + 3 Pol(f38) = V_6 - 2*V_7 + 2 Pol(f53) = V_6 - 2*V_7 + 2 Pol(f2) = V_6 - 2*V_7 + 3 orients all transitions weakly and the transition f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] strictly and produces the following problem: 8: T: (38*h + 38*i + 19, 1) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (6*h + 6*i + 3, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (?, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (p + 2*q + 3, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (a + 2*j + 2*k, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (2*h + 2*i + 1, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ] start location: f2 leaf cost: 5 A polynomial rank function with Pol(f53) = 2 Pol(f38) = 2 Pol(f35) = 1 and size complexities S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-0) = 1 S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-1) = h S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-2) = i S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-3) = j S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-4) = k S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-5) = p S("f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ]", 0-6) = q S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-0) = 1 S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-1) = h S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-2) = 39*h + 39*i + 28899 S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-3) = j S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-4) = 3*a + 3*j + 3*k S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-5) = p S("f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ]", 0-6) = q S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-0) = 1 S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-1) = h S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-2) = 39*h + 39*i + 28899 S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-3) = j S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-4) = 3*a + 3*j + 3*k S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-5) = p S("f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ]", 0-6) = q S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-0) = a S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-1) = h S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-2) = i S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-3) = j S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-4) = k S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-5) = p S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ]", 0-6) = q S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-0) = a S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-1) = h S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-2) = i S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-3) = j S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-4) = k S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-5) = p S("f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ]", 0-6) = q S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-0) = a S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-1) = h S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-2) = 7*h + 7*i + 196 S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-3) = j S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-4) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-5) = p S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\\ h >= i ]", 0-6) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-0) = a S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-1) = h S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-2) = 7*h + 7*i + 196 S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-3) = j S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-4) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-5) = p S("f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\\ h >= i ]", 0-6) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-0) = a S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-1) = h S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-2) = 1 S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-3) = j S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-4) = ? S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-5) = p S("f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\\ i = 1 ]", 0-6) = ? S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-0) = a S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-1) = h S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-2) = 7*h + 7*i + 196 S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-3) = j S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-4) = ? S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-5) = p S("f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ x + 1 >= q ]", 0-6) = ? S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-2) = 7*h + 7*i + 196 S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-4) = ? S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\\ j >= k ]", 0-6) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-2) = 7*h + 7*i + 196 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-4) = ? S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ 0 >= k /\\ j >= k /\\ q = 1 ]", 0-6) = 1 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-2) = 7*h + 7*i + 1372 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-4) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\\ 5*x + k >= j + 1 /\\ j >= k /\\ k >= 2 /\\ q = 1 ]", 0-6) = 1 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-2) = 7*h + 7*i + 196 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-4) = 2 S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\\ k = 1 /\\ q = 1 ]", 0-6) = 1 S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-0) = a S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-1) = h S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-2) = 7*h + 7*i + 196 S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-3) = j S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-4) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-5) = p S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ 0 >= k ]", 0-6) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-0) = a S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-1) = h S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-2) = 7*h + 7*i + 196 S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-3) = j S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-4) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-5) = p S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k >= 2 ]", 0-6) = ? S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-0) = a S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-1) = h S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-2) = 7*h + 7*i + 196 S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-3) = j S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-4) = 2 S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-5) = p S("f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\\ 3*f1 >= q + 1 /\\ k = 1 ]", 0-6) = ? S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-0) = a S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-1) = h S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-2) = 7*h + 7*i + 196 S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-3) = j S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-4) = ? S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-5) = p S("f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ]", 0-6) = ? S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-0) = a S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-1) = h S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-2) = 7*h + 7*i + 196 S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-3) = j S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-4) = ? S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-5) = p S("f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\\ 3*x >= p + 1 /\\ q >= x + 2 ]", 0-6) = ? S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-0) = 1 S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-1) = h S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-2) = 39*h + 39*i + 28899 S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-3) = j S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-4) = 3*a + 3*j + 3*k S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-5) = p S("f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ]", 0-6) = q orients the transitions f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] weakly and the transition f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] strictly and produces the following problem: 9: T: (38*h + 38*i + 19, 1) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (6*h + 6*i + 3, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (2*p + 4*q + 6, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (?, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (p + 2*q + 3, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (a + 2*j + 2*k, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (2*h + 2*i + 1, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ] start location: f2 leaf cost: 5 A polynomial rank function with Pol(f16) = V_1 + 2*V_4 - 2*V_5 Pol(f13) = V_1 + 2*V_4 - 2*V_5 Pol(f35) = 2*V_4 - 2*V_5 + 1 Pol(f27) = 2*V_4 - 2*V_5 + 1 Pol(f38) = 2*V_4 - 2*V_5 + 1 Pol(f53) = 2*V_4 - 2*V_5 Pol(f2) = 2*V_4 - 2*V_5 + 1 orients all transitions weakly and the transitions f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] strictly and produces the following problem: 10: T: (38*h + 38*i + 19, 1) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (6*h + 6*i + 3, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (2*p + 4*q + 6, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (?, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (2*j + 2*k + 1, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (2*j + 2*k + 1, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (2*j + 2*k + 1, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (2*j + 2*k + 1, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (p + 2*q + 3, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (a + 2*j + 2*k, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (2*h + 2*i + 1, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ] start location: f2 leaf cost: 5 Repeatedly propagating knowledge in problem 10 produces the following problem: 11: T: (38*h + 38*i + 19, 1) f16(a, h, i, j, k, p, q) -> f13(a, h, i + 1, j, k, p, q) [ k >= j + 1 ] (6*h + 6*i + 3, 1) f35(a, h, i, j, k, p, q) -> f27(a, h, i + 1, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ q >= x + 2 ] (2*p + 4*q + 6, 1) f38(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q + 1) [ k >= j + 1 ] (2*j + 2*k + 1, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k = 1 ] (2*j + 2*k + 1, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ k >= 2 ] (2*j + 2*k + 1, 1) f53(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, q) [ q >= 2*f1 /\ 3*f1 >= q + 1 /\ 0 >= k ] (2*j + 2*k + 1, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, 2, p, 1) [ j >= 1 /\ k = 1 /\ q = 1 ] (2*j + 2*k + 1, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ j >= k /\ k >= 2 /\ q = 1 ] (2*j + 2*k + 1, 1) f38(a, h, i, j, k, p, q) -> f38(a, h, i, j, k + 1, p, 1) [ j >= k + 4*x /\ 5*x + k >= j + 1 /\ 0 >= k /\ j >= k /\ q = 1 ] (2*j + 2*k + 1, 1) f38(a, h, i, j, k, p, q) -> f53(a, h, i, j, k, p, q) [ q >= 2 /\ j >= k ] (p + 2*q + 3, 1) f35(a, h, i, j, k, p, q) -> f38(a, h, i, j, k, p, q) [ p >= 2*x /\ 3*x >= p + 1 /\ x + 1 >= q ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, 1, j, k, p, q) [ h >= 1 /\ i = 1 ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ i >= 2 /\ h >= i ] (2*h + 2*i + 1, 1) f27(a, h, i, j, k, p, q) -> f35(a, h, i, j, k, p, q) [ 0 >= i /\ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ a >= 2 ] (1, 1) f2(a, h, i, j, k, p, q) -> f27(a, h, i, j, k, p, q) [ 0 >= a ] (a + 2*j + 2*k, 1) f16(a, h, i, j, k, p, q) -> f16(a, h, i, j, k + 1, p, q) [ j >= k ] (2*h + 2*i + 1, 1) f13(a, h, i, j, k, p, q) -> f16(a, h, i, j, k, p, q) [ h >= i ] (1, 1) f2(a, h, i, j, k, p, q) -> f13(1, h, i, j, k, p, q) [ a = 1 ] start location: f2 leaf cost: 5 Complexity upper bound 52*h + 52*i + 3*p + 6*q + 16*j + 16*k + a + 50 Time: 3.044 sec (SMT: 2.640 sec)