YES(?, 162*a + 12*k + 5*d + 145*b + 40) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= 2 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f13(a, b, 0, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= b + 1 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f13(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) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f13(a, b, s, d + 1, c, s, s, h, i, j, k, l, m, n, o, p, q, r) [ s >= c /\ a >= d ] (?, 1) f29(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f29(a, b, c, d + 1, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= d ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f34(a, b, c, d + 1, e, f, g, 0, 0, j, k, l, m, n, o, p, q, r) [ a >= d ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f34(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) f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f34(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) f53(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) f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f61(a, b, c, d + 1, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ a >= d ] (?, 1) f61(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f53(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) -> f61(a, b, c, d, e, f, g, h, i, j, k, s, m, n, o, p, q, r) [ d >= a + 1 ] (?, 1) f53(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f10(a, b + 1, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ k >= a + 1 ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f53(a, b, c, d, e, f, g, h, i, j, k, l, s, t, t, p, q, r) [ d >= a + 1 ] (?, 1) f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f53(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) f29(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f34(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ d >= a + 1 ] (?, 1) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f10(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) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f29(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) f13(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f29(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ c >= 1 /\ d >= a + 1 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f73(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ b >= a /\ 0 >= s + 1 ] (?, 1) f10(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) -> f73(a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r) [ b >= a ] start location: f0 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) f10(a, b, c, d, k) -> f73(a, b, c, d, k) [ b >= a ] (?, 1) f10(a, b, c, d, k) -> f73(a, b, c, d, k) [ b >= a /\ 0 >= s + 1 ] (?, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (?, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] (?, 1) f55(a, b, c, d, k) -> f61(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f61(a, b, c, d, k) -> f53(a, b, c, d, k + 1) [ d >= a + 1 ] (?, 1) f61(a, b, c, d, k) -> f61(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) f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (?, 1) f34(a, b, c, d, k) -> f34(a, b, c, d + 1, k) [ s >= 1 /\ a >= d ] (?, 1) f34(a, b, c, d, k) -> f34(a, b, c, d + 1, k) [ 0 >= s + 1 /\ a >= d ] (?, 1) f34(a, b, c, d, k) -> f34(a, b, c, d + 1, k) [ a >= d ] (?, 1) f29(a, b, c, d, k) -> f29(a, b, c, d + 1, k) [ a >= d ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (?, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] (?, 1) f55(a, b, c, d, k) -> f61(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f61(a, b, c, d, k) -> f53(a, b, c, d, k + 1) [ d >= a + 1 ] (?, 1) f61(a, b, c, d, k) -> f61(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) f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (?, 1) f34(a, b, c, d, k) -> f34(a, b, c, d + 1, k) [ s >= 1 /\ a >= d ] (?, 1) f34(a, b, c, d, k) -> f34(a, b, c, d + 1, k) [ 0 >= s + 1 /\ a >= d ] (?, 1) f34(a, b, c, d, k) -> f34(a, b, c, d + 1, k) [ a >= d ] (?, 1) f29(a, b, c, d, k) -> f29(a, b, c, d + 1, k) [ a >= d ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ] start location: f0 leaf cost: 2 Testing for reachability in the complexity graph removes the following transitions from problem 3: f61(a, b, c, d, k) -> f61(a, b, c, d + 1, k) [ a >= d ] f34(a, b, c, d, k) -> f34(a, b, c, d + 1, k) [ s >= 1 /\ a >= d ] f34(a, b, c, d, k) -> f34(a, b, c, d + 1, k) [ 0 >= s + 1 /\ a >= d ] f34(a, b, c, d, k) -> f34(a, b, c, d + 1, k) [ a >= d ] f29(a, b, c, d, k) -> f29(a, b, c, d + 1, k) [ a >= d ] We thus obtain the following problem: 4: T: (?, 1) f61(a, b, c, d, k) -> f53(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) -> f61(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (?, 1) f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] (?, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (?, 1) f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (?, 1) f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f61) = 5*V_1 - 5*V_2 - 3 Pol(f53) = 5*V_1 - 5*V_2 - 3 Pol(f55) = 5*V_1 - 5*V_2 - 3 Pol(f10) = 5*V_1 - 5*V_2 + 1 Pol(f34) = 5*V_1 - 5*V_2 - 2 Pol(f29) = 5*V_1 - 5*V_2 - 1 Pol(f13) = 5*V_1 - 5*V_2 Pol(f0) = 5*V_1 - 5*V_2 + 1 orients all transitions weakly and the transition f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ] strictly and produces the following problem: 5: T: (?, 1) f61(a, b, c, d, k) -> f53(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) -> f61(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (?, 1) f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] (?, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (?, 1) f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (?, 1) f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f61) = 1 Pol(f53) = 1 Pol(f55) = 1 Pol(f10) = 0 Pol(f34) = 2 Pol(f29) = 3 Pol(f13) = 4 and size complexities S("f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ]", 0-0) = a S("f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ]", 0-1) = b S("f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ]", 0-2) = c S("f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ]", 0-3) = d S("f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ]", 0-4) = k S("f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ]", 0-0) = a S("f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ]", 0-1) = ? S("f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ]", 0-2) = 0 S("f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ]", 0-3) = ? S("f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ]", 0-4) = ? S("f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-0) = a S("f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-1) = ? S("f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-2) = 0 S("f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-3) = ? S("f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\\ c = 0 ]", 0-4) = ? S("f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-0) = a S("f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-1) = ? S("f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-2) = ? S("f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-3) = ? S("f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\\ a >= d ]", 0-4) = ? S("f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-0) = a S("f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-1) = ? S("f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-2) = ? S("f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-3) = ? S("f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\\ a >= d ]", 0-4) = ? S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-0) = a S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-1) = ? S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-2) = ? S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-3) = ? S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\\ d >= a + 1 ]", 0-4) = ? S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-0) = a S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-1) = ? S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-2) = ? S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-3) = ? S("f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-4) = ? S("f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ]", 0-0) = a S("f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ]", 0-1) = ? S("f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ]", 0-2) = ? S("f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ]", 0-3) = ? S("f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ]", 0-4) = ? S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-0) = a S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-1) = ? S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-2) = ? S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-3) = ? S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\\ d >= a + 1 ]", 0-4) = ? S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ]", 0-0) = a S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ]", 0-1) = ? S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ]", 0-2) = ? S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ]", 0-3) = ? S("f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ]", 0-4) = ? S("f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-0) = a S("f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-1) = ? S("f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-2) = ? S("f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-3) = ? S("f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ]", 0-4) = ? S("f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-0) = a S("f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-1) = ? S("f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-2) = ? S("f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-3) = ? S("f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ]", 0-4) = ? S("f55(a, b, c, d, k) -> f61(a, b, c, d, k) [ d >= a + 1 ]", 0-0) = a S("f55(a, b, c, d, k) -> f61(a, b, c, d, k) [ d >= a + 1 ]", 0-1) = ? S("f55(a, b, c, d, k) -> f61(a, b, c, d, k) [ d >= a + 1 ]", 0-2) = ? S("f55(a, b, c, d, k) -> f61(a, b, c, d, k) [ d >= a + 1 ]", 0-3) = ? S("f55(a, b, c, d, k) -> f61(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("f61(a, b, c, d, k) -> f53(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-0) = a S("f61(a, b, c, d, k) -> f53(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-1) = ? S("f61(a, b, c, d, k) -> f53(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-2) = ? S("f61(a, b, c, d, k) -> f53(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-3) = ? S("f61(a, b, c, d, k) -> f53(a, b, c, d, k + 1) [ d >= a + 1 ]", 0-4) = ? orients the transitions f61(a, b, c, d, k) -> f53(a, b, c, d, k + 1) [ d >= a + 1 ] f55(a, b, c, d, k) -> f61(a, b, c, d, k) [ d >= a + 1 ] f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] weakly and the transitions f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] strictly and produces the following problem: 6: T: (?, 1) f61(a, b, c, d, k) -> f53(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) -> f61(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (20*a + 20*b + 4, 1) f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] (20*a + 20*b + 4, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (?, 1) f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f61) = V_1 - V_4 + 1 Pol(f53) = V_1 - V_4 + 1 Pol(f55) = V_1 - V_4 + 1 Pol(f10) = V_1 - V_4 + 1 Pol(f34) = V_1 - V_4 + 1 Pol(f29) = V_1 - V_4 + 1 Pol(f13) = V_1 - V_4 + 1 Pol(f0) = V_1 - V_4 + 1 orients all transitions weakly and the transitions f55(a, b, c, d, k) -> f55(a, b, c, d + 1, k) [ a >= d ] f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] strictly and produces the following problem: 7: T: (?, 1) f61(a, b, c, d, k) -> f53(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) -> f61(a, b, c, d, k) [ d >= a + 1 ] (?, 1) f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (20*a + 20*b + 4, 1) f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] (20*a + 20*b + 4, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (a + d + 1, 1) f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (a + d + 1, 1) f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f61) = 4*V_1 - 4*V_5 - 2 Pol(f53) = 4*V_1 - 4*V_5 + 1 Pol(f55) = 4*V_1 - 4*V_5 - 1 Pol(f10) = 4*V_1 - 4*V_5 + 1 Pol(f34) = 4*V_1 - 4*V_5 + 1 Pol(f29) = 4*V_1 - 4*V_5 + 1 Pol(f13) = 4*V_1 - 4*V_5 + 1 Pol(f0) = 4*V_1 - 4*V_5 + 1 orients all transitions weakly and the transition f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] strictly and produces the following problem: 8: T: (?, 1) f61(a, b, c, d, k) -> f53(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) -> f61(a, b, c, d, k) [ d >= a + 1 ] (4*a + 4*k + 1, 1) f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (20*a + 20*b + 4, 1) f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] (20*a + 20*b + 4, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (a + d + 1, 1) f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (a + d + 1, 1) f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ] start location: f0 leaf cost: 2 Repeatedly propagating knowledge in problem 8 produces the following problem: 9: T: (5*a + 4*k + d + 2, 1) f61(a, b, c, d, k) -> f53(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) -> f61(a, b, c, d, k) [ d >= a + 1 ] (4*a + 4*k + 1, 1) f53(a, b, c, d, k) -> f55(a, b, c, d, k) [ a >= k ] (20*a + 20*b + 4, 1) f53(a, b, c, d, k) -> f10(a, b + 1, c, d, k) [ k >= a + 1 ] (20*a + 20*b + 4, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f34(a, b, c, d, k) -> f53(a, b, c, d, k) [ 0 >= u + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f29(a, b, c, d, k) -> f34(a, b, c, d, k) [ d >= a + 1 ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ 0 >= c + 1 /\ d >= a + 1 ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f29(a, b, c, d, k) [ c >= 1 /\ d >= a + 1 ] (a + d + 1, 1) f13(a, b, c, d, k) -> f13(a, b, c, d + 1, k) [ c >= s + 1 /\ a >= d ] (a + d + 1, 1) f13(a, b, c, d, k) -> f13(a, b, s, d + 1, k) [ s >= c /\ a >= d ] (20*a + 20*b + 4, 1) f13(a, b, c, d, k) -> f10(a, b + 1, 0, d, k) [ d >= a + 1 /\ c = 0 ] (5*a + 5*b + 1, 1) f10(a, b, c, d, k) -> f13(a, b, 0, d, k) [ a >= b + 1 ] (1, 1) f0(a, b, c, d, k) -> f10(a, b, c, d, k) [ a >= 2 ] start location: f0 leaf cost: 2 Complexity upper bound 162*a + 12*k + 5*d + 145*b + 40 Time: 0.650 sec (SMT: 0.601 sec)