YES(?, 162*a + 12*k + 5*d + 145*b + 41) 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) -> f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= 2 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f9(a, b, 0, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= b + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f9(a, b, c, d + 1, c, s, s, h, i, j, k, l, m, n, o, p, q, r) [ c >= s + 1 /\ a >= d ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f9(a, b, s, d + 1, c, s, s, h, i, j, k, l, m, n, o, p, q, r) [ s >= c /\ a >= d ] (?, 1) f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f26(a, b, c, d + 1, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= d ] (?, 1) f32(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f32(a, b, c, d + 1, e, f, g, 0, 0, j, k, l, m, n, o, p, q, r) [ a >= d ] (?, 1) f32(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f32(a, b, c, d + 1, e, f, g, s, t, j + t, k, l, m, n, o, p, q, r) [ 0 >= s + 1 /\ a >= d ] (?, 1) f32(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f32(a, b, c, d + 1, e, f, g, s, t, j + t, k, l, m, n, o, p, q, r) [ s >= 1 /\ a >= d ] (?, 1) f52(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f55(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= k ] (?, 1) f55(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f55(a, b, c, d + 1, e, f, g, h, i, s, k, l, m, n, o, p, q, r) [ a >= d ] (?, 1) f62(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f62(a, b, c, d + 1, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= d ] (?, 1) f62(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f52(a, b, c, d, e, f, g, h, i, j, k + 1, l, m, n, o, p, q, r) [ d >= a + 1 ] (?, 1) f55(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f62(a, b, c, d, e, f, g, h, i, j, k, s, m, n, o, p, q, r) [ d >= a + 1 ] (?, 1) f52(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f5(a, b + 1, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ k >= a + 1 ] (?, 1) f32(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f52(a, b, c, d, e, f, g, h, i, j, k, l, s, t, t, p, q, r) [ u >= 0 /\ d >= a + 1 ] (?, 1) f32(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f52(a, b, c, d, e, f, g, h, i, j, k, l, m, n, -s, t, s, r) [ 0 >= u + 1 /\ d >= a + 1 ] (?, 1) f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f32(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ d >= a + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f5(a, b + 1, 0, d, e, f, g, h, i, j, k, l, m, n, o, p, q, 0) [ d >= a + 1 /\ c = 0 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f26(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ c >= 1 /\ d >= a + 1 ] (?, 1) f5(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 /\ 0 >= s + 1 ] (?, 1) f5(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 /\ s >= 1 ] (?, 1) f5(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 ] start location: f2 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, k]. We thus obtain the following problem: 2: T: (?, 1) f5(a, b, c, d, k) -> f1(a, b, c, d, k) [ b >= a ] (?, 1) f5(a, b, c, d, k) -> f1(a, b, c, d, k) [ b >= a /\ s >= 1 ] (?, 1) f5(a, b, c, d, k) -> f1(a, b, c, d, k) [ b >= a /\ 0 >= s + 1 ] (?, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (?, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] (?, 1) f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] (?, 1) f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ] (?, 1) f62(a, b, c, d, k) -> f62(a, b, c, d + 1, k) [ a >= d ] (?, 1) f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] (?, 1) f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (?, 1) f32(a, b, c, d, k) -> f32(a, b, c, d + 1, k) [ s >= 1 /\ a >= d ] (?, 1) f32(a, b, c, d, k) -> f32(a, b, c, d + 1, k) [ 0 >= s + 1 /\ a >= d ] (?, 1) f32(a, b, c, d, k) -> f32(a, b, c, d + 1, k) [ a >= d ] (?, 1) f26(a, b, c, d, k) -> f26(a, b, c, d + 1, k) [ a >= d ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ] start location: f2 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (?, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] (?, 1) f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] (?, 1) f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ] (?, 1) f62(a, b, c, d, k) -> f62(a, b, c, d + 1, k) [ a >= d ] (?, 1) f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] (?, 1) f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (?, 1) f32(a, b, c, d, k) -> f32(a, b, c, d + 1, k) [ s >= 1 /\ a >= d ] (?, 1) f32(a, b, c, d, k) -> f32(a, b, c, d + 1, k) [ 0 >= s + 1 /\ a >= d ] (?, 1) f32(a, b, c, d, k) -> f32(a, b, c, d + 1, k) [ a >= d ] (?, 1) f26(a, b, c, d, k) -> f26(a, b, c, d + 1, k) [ a >= d ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ] start location: f2 leaf cost: 3 Testing for reachability in the complexity graph removes the following transitions from problem 3: f62(a, b, c, d, k) -> f62(a, b, c, d + 1, k) [ a >= d ] f32(a, b, c, d, k) -> f32(a, b, c, d + 1, k) [ s >= 1 /\ a >= d ] f32(a, b, c, d, k) -> f32(a, b, c, d + 1, k) [ 0 >= s + 1 /\ a >= d ] f32(a, b, c, d, k) -> f32(a, b, c, d + 1, k) [ a >= d ] f26(a, b, c, d, k) -> f26(a, b, c, d + 1, k) [ a >= d ] We thus obtain the following problem: 4: T: (?, 1) f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ] (?, 1) f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] (?, 1) f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (?, 1) f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] (?, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] (?, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (?, 1) f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (?, 1) f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ] start location: f2 leaf cost: 3 A polynomial rank function with Pol(f62) = 5*V_1 - 5*V_2 - 3 Pol(f52) = 5*V_1 - 5*V_2 - 3 Pol(f55) = 5*V_1 - 5*V_2 - 3 Pol(f5) = 5*V_1 - 5*V_2 + 1 Pol(f32) = 5*V_1 - 5*V_2 - 2 Pol(f26) = 5*V_1 - 5*V_2 - 1 Pol(f9) = 5*V_1 - 5*V_2 Pol(f2) = 5*V_1 - 5*V_2 + 1 orients all transitions weakly and the transition f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ] strictly and produces the following problem: 5: T: (?, 1) f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ] (?, 1) f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] (?, 1) f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (?, 1) f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] (?, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] (?, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (?, 1) f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (?, 1) f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ] start location: f2 leaf cost: 3 A polynomial rank function with Pol(f9) = 4 Pol(f5) = 0 Pol(f26) = 3 Pol(f62) = 1 Pol(f52) = 1 Pol(f55) = 1 Pol(f32) = 2 and size complexities S("f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ]", 0-0) = a S("f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ]", 0-1) = b S("f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ]", 0-2) = c S("f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ]", 0-3) = d S("f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ]", 0-4) = k S("f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ]", 0-0) = a S("f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ]", 0-1) = ? S("f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ]", 0-2) = 0 S("f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ]", 0-3) = ? S("f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ]", 0-4) = ? S("f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-0) = a S("f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-1) = ? S("f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-2) = 0 S("f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-3) = ? S("f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-4) = ? S("f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-0) = a S("f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-1) = ? S("f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-2) = ? S("f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-3) = ? S("f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-4) = ? S("f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-0) = a S("f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-1) = ? S("f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-2) = ? S("f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-3) = ? S("f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-4) = ? S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-0) = a S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-1) = ? S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-2) = ? S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-3) = ? S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-4) = ? S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-0) = a S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-1) = ? S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-2) = ? S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-3) = ? S("f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-4) = ? S("f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ]", 0-0) = a S("f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ]", 0-1) = ? S("f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ]", 0-2) = ? S("f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ]", 0-3) = ? S("f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ]", 0-4) = ? S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-0) = a S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-1) = ? S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-2) = ? S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-3) = ? S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-4) = ? S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\\ d >= a + 1 ]", 0-0) = a S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\\ d >= a + 1 ]", 0-1) = ? S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\\ d >= a + 1 ]", 0-2) = ? S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\\ d >= a + 1 ]", 0-3) = ? S("f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\\ d >= a + 1 ]", 0-4) = ? S("f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-0) = a S("f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-1) = ? S("f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-2) = ? S("f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-3) = ? S("f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-4) = ? S("f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-0) = a S("f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-1) = ? S("f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-2) = ? S("f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-3) = ? S("f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-4) = ? S("f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ]", 0-0) = a S("f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ]", 0-1) = ? S("f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ]", 0-2) = ? S("f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ]", 0-3) = ? S("f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ]", 0-4) = ? S("f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ]", 0-0) = a S("f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ]", 0-1) = ? S("f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ]", 0-2) = ? S("f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ]", 0-3) = ? S("f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ]", 0-4) = ? S("f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-0) = a S("f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-1) = ? S("f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-2) = ? S("f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-3) = ? S("f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-4) = ? orients the transitions f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ] f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ] f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] weakly and the transitions f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] strictly and produces the following problem: 6: T: (?, 1) f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ] (?, 1) f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] (?, 1) f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (20*a + 20*b + 4, 1) f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] (20*a + 20*b + 4, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ] start location: f2 leaf cost: 3 A polynomial rank function with Pol(f62) = V_1 - V_4 + 1 Pol(f52) = V_1 - V_4 + 1 Pol(f55) = V_1 - V_4 + 1 Pol(f5) = V_1 - V_4 + 1 Pol(f32) = V_1 - V_4 + 1 Pol(f26) = V_1 - V_4 + 1 Pol(f9) = V_1 - V_4 + 1 Pol(f2) = V_1 - V_4 + 1 orients all transitions weakly and the transitions f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] strictly and produces the following problem: 7: T: (?, 1) f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ] (a + d + 1, 1) f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] (?, 1) f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (20*a + 20*b + 4, 1) f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] (20*a + 20*b + 4, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (a + d + 1, 1) f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (a + d + 1, 1) f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ] start location: f2 leaf cost: 3 A polynomial rank function with Pol(f62) = 4*V_1 - 4*V_5 - 2 Pol(f52) = 4*V_1 - 4*V_5 + 1 Pol(f55) = 4*V_1 - 4*V_5 - 1 Pol(f5) = 4*V_1 - 4*V_5 + 1 Pol(f32) = 4*V_1 - 4*V_5 + 1 Pol(f26) = 4*V_1 - 4*V_5 + 1 Pol(f9) = 4*V_1 - 4*V_5 + 1 Pol(f2) = 4*V_1 - 4*V_5 + 1 orients all transitions weakly and the transition f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] strictly and produces the following problem: 8: T: (?, 1) f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ] (a + d + 1, 1) f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] (?, 1) f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ] (4*a + 4*k + 1, 1) f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (20*a + 20*b + 4, 1) f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] (20*a + 20*b + 4, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (a + d + 1, 1) f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (a + d + 1, 1) f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ] start location: f2 leaf cost: 3 Repeatedly propagating knowledge in problem 8 produces the following problem: 9: T: (5*a + 4*k + d + 2, 1) f62(a, b, c, d, k) -> f52(a, b, c, d, k + 1) [ d >= a + 1 ] (a + d + 1, 1) f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] (5*a + 4*k + d + 2, 1) f55(a, b, c, d, k) -> f62(a, b, c, d, k) [ d >= a + 1 ] (4*a + 4*k + 1, 1) f52(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (20*a + 20*b + 4, 1) f52(a, b, c, d, k) -> f5(a, b + 1, c, d, k) [ k >= a + 1 ] (20*a + 20*b + 4, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ u >= 0 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f32(a, b, c, d, k) -> f52(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f26(a, b, c, d, k) -> f32(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f26(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (a + d + 1, 1) f9(a, b, c, d, k) -> f9(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (a + d + 1, 1) f9(a, b, c, d, k) -> f9(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (20*a + 20*b + 4, 1) f9(a, b, c, d, k) -> f5(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f5(a, b, c, d, k) -> f9(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f2(a, b, c, d, k) -> f5(a, b, c, d, k) [ a >= 2 ] start location: f2 leaf cost: 3 Complexity upper bound 162*a + 12*k + 5*d + 145*b + 41 Time: 0.670 sec (SMT: 0.618 sec)