YES(?, 568*a + 562*d + 4*b + 2*h + 78) Initial complexity problem: 1: T: (?, 1) f69(a, b, c, d, e, f, g, h, i, j, k) -> f71(a, b, c, d, e, f, g, h, i, j, k) [ 0 >= l + 1 ] (?, 1) f69(a, b, c, d, e, f, g, h, i, j, k) -> f71(a, b, c, d, e, f, g, h, i, j, k) [ l >= 1 ] (1, 1) f2(a, b, c, d, e, f, g, h, i, j, k) -> f5(a, b, c, d, e, f, g, h, i, j, k) (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k) -> f9(a, b, 0, d, e, f, g, h, i, j, k) [ a >= b ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k) -> f9(a, b, c, d + 1, l, l, g, h, i, j, k) [ c >= l /\ a >= d ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k) -> f9(a, b, l, d + 1, l, l, g, h, i, j, k) [ l >= c + 1 /\ a >= d ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k) -> f26(a, b, c, d, e, f, g, h, i, j, k) [ a >= d ] (?, 1) f26(a, b, c, d, e, f, g, h, i, j, k) -> f30(a, b, c, d, e, f, l, h, i, j, k) [ d >= b + 1 ] (?, 1) f30(a, b, c, d, e, f, g, h, i, j, k) -> f30(a, b, c, d, e, f, l, h + 1, i, j, k) [ b >= h + 1 ] (?, 1) f40(a, b, c, d, e, f, g, h, i, j, k) -> f44(a, b, c, d, e, f, l, h, i, j, k) [ a >= b ] (?, 1) f44(a, b, c, d, e, f, g, h, i, j, k) -> f44(a, b, c, d, e, f, l, h + 1, i, j, k) [ d >= h + 1 ] (?, 1) f59(a, b, c, d, e, f, g, h, i, j, k) -> f59(a, b, c, d, e, f, g, h + 1, l, j, k) [ a >= h ] (?, 1) f69(a, b, c, d, e, f, g, h, i, j, k) -> f71(a, b, c, d, e, f, g, h, i, j, k) (?, 1) f71(a, b, c, d, e, f, g, h, i, j, k) -> f74(a, b, c, d, e, f, g, h, l, j, k) [ a >= d + 1 ] (?, 1) f71(a, b, c, d, e, f, g, h, i, j, k) -> f74(a, b, c, d, e, f, g, h, l, j, k) [ d >= a + 1 ] (?, 1) f74(a, b, c, d, e, f, g, h, i, j, k) -> f74(a, b + 1, c, d, e, f, g, h, i, j, k) [ a >= b ] (?, 1) f71(a, b, c, d, e, f, g, h, i, j, k) -> f23(a, b, c, a + 1, e, f, g, h, i, j, k) [ a = d ] (?, 1) f74(a, b, c, d, e, f, g, h, i, j, k) -> f23(a, b, c, d + 1, e, f, g, h, i, j, k) [ b >= a + 1 ] (?, 1) f59(a, b, c, d, e, f, g, h, i, j, k) -> f69(a, b, c, d, e, f, g, h, i, j, k) [ h >= a + 1 ] (?, 1) f44(a, b, c, d, e, f, g, h, i, j, k) -> f40(a, b + 1, c, d, e, f, g, h, m, l, k) [ c >= m + 1 /\ h >= d ] (?, 1) f44(a, b, c, d, e, f, g, h, i, j, k) -> f40(a, b + 1, l, d, e, f, g, h, l, m, b) [ l >= c /\ h >= d ] (?, 1) f40(a, b, c, d, e, f, g, h, i, j, k) -> f59(a, b, c, d, e, f, g, h, i, j, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f40(a, b, c, d, e, f, g, h, i, j, k) -> f59(a, b, c, d, e, f, g, h, i, j, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f40(a, b, c, d, e, f, g, h, i, j, k) -> f69(a, b, c, d, e, f, g, h, i, j, d) [ b >= a + 1 /\ d = k ] (?, 1) f30(a, b, c, d, e, f, g, h, i, j, k) -> f26(a, b + 1, c, d, e, f, g, h, i, j, k) [ h >= b ] (?, 1) f26(a, b, c, d, e, f, g, h, i, j, k) -> f40(a, b, 0, d, e, f, g, h, i, j, k) [ b >= d ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k) -> f1(a, b, c, d, e, f, g, h, i, j, k) [ d >= a + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k) -> f5(a, b + 1, c, d, e, f, g, h, i, j, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k) -> f5(a, b + 1, c, d, e, f, g, h, i, j, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, e, f, g, h, i, j, k) -> f5(a, b + 1, 0, d, e, f, g, h, i, j, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f5(a, b, c, d, e, f, g, h, i, j, k) -> f23(a, b, c, d, e, f, g, h, i, j, k) [ b >= a + 1 ] start location: f2 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, h, k]. We thus obtain the following problem: 2: T: (?, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f23(a, b, c, d, h, k) -> f1(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (?, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f23(a, b, c, a + 1, h, k) [ a = d ] (?, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (?, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (?, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (?, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (?, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (?, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 A polynomial rank function with Pol(f5) = 1 Pol(f23) = -2 Pol(f9) = 1 Pol(f26) = -2 Pol(f40) = -2 Pol(f30) = -2 Pol(f69) = -2 Pol(f59) = -2 Pol(f44) = -2 Pol(f74) = -2 Pol(f71) = -2 Pol(f2) = 1 orients all transitions weakly and the transition f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] strictly and produces the following problem: 4: T: (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (?, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (?, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (?, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 A polynomial rank function with Pol(f5) = 7*V_1 - 7*V_4 + 1 Pol(f23) = 9*V_1 - 2*V_2 - 7*V_4 - 3 Pol(f9) = 7*V_1 - 7*V_4 + 1 Pol(f26) = 9*V_1 - 2*V_2 - 7*V_4 - 4 Pol(f40) = 9*V_1 - 2*V_2 - 7*V_4 - 5 Pol(f30) = 9*V_1 - 2*V_2 - 7*V_4 - 5 Pol(f69) = 9*V_1 - 2*V_2 - 7*V_4 - 7 Pol(f59) = 9*V_1 - 2*V_2 - 7*V_4 - 6 Pol(f44) = 9*V_1 - 2*V_2 - 7*V_4 - 6 Pol(f74) = 9*V_1 - 2*V_2 - 7*V_4 - 9 Pol(f71) = 9*V_1 - 2*V_2 - 7*V_4 - 8 Pol(f2) = 7*V_1 - 7*V_4 + 1 orients all transitions weakly and the transitions f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] strictly and produces the following problem: 5: T: (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (?, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 Repeatedly propagating knowledge in problem 5 produces the following problem: 6: T: (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (?, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 A polynomial rank function with Pol(f5) = 8*V_1 - 8*V_4 + 1 Pol(f23) = 8*V_1 - 8*V_4 + 1 Pol(f9) = 8*V_1 - 8*V_4 + 1 Pol(f26) = 8*V_1 - 8*V_4 - 1 Pol(f40) = 8*V_1 - 8*V_4 - 2 Pol(f30) = 8*V_1 - 8*V_4 - 1 Pol(f69) = 8*V_1 - 8*V_4 - 4 Pol(f59) = 8*V_1 - 8*V_4 - 3 Pol(f44) = 8*V_1 - 8*V_4 - 2 Pol(f74) = 8*V_1 - 8*V_4 - 6 Pol(f71) = 8*V_1 - 8*V_4 - 5 Pol(f2) = 8*V_1 - 8*V_4 + 1 orients all transitions weakly and the transitions f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] strictly and produces the following problem: 7: T: (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (?, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 A polynomial rank function with Pol(f9) = 0 Pol(f5) = 0 Pol(f74) = 1 Pol(f23) = 0 Pol(f71) = 2 Pol(f69) = 3 Pol(f59) = 4 Pol(f44) = 5 Pol(f40) = 5 Pol(f30) = 6 Pol(f26) = 6 and size complexities S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-0) = a S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-1) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-2) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-3) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-4) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-5) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-0) = a S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-1) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-2) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-3) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-4) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-5) = ? S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-0) = a S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-1) = b S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-2) = c S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-3) = d S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-4) = h S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-5) = k S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-0) = a S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-1) = ? S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-2) = 0 S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-3) = 15*a + 15*d + 450 S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-4) = h S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-5) = k S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-1) = ? S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-2) = ? S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-5) = k S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-1) = ? S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-2) = ? S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-5) = k S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-0) = a S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-1) = ? S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-2) = ? S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-3) = ? S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-4) = ? S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-5) = ? S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-0) = a S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-1) = ? S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-2) = ? S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-3) = ? S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-4) = ? S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-5) = ? S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-2) = ? S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-3) = ? S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-5) = ? S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-0) = a S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-1) = ? S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-2) = ? S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-3) = ? S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-4) = ? S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-5) = ? S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-0) = a S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-1) = ? S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-2) = ? S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-3) = ? S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-4) = ? S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-5) = ? S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-0) = a S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-1) = ? S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-2) = ? S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-3) = ? S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-4) = ? S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-5) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-0) = a S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-1) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-2) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-3) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-4) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-5) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-3) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-5) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-3) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-5) = ? S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-0) = a S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-1) = ? S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-2) = ? S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-3) = ? S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-4) = ? S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-5) = ? S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-0) = a S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-1) = ? S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-2) = ? S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-3) = ? S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-4) = ? S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-5) = ? S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-0) = a S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-1) = ? S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-2) = ? S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-3) = ? S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-4) = ? S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-5) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-0) = a S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-1) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-2) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-3) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-4) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-5) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-0) = a S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-1) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-2) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-3) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-4) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-5) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-0) = a S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-1) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-2) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-3) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-4) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-5) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-0) = a S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-1) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-2) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-3) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-4) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-5) = ? S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-0) = a S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-1) = ? S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-2) = ? S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-3) = ? S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-4) = ? S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-5) = ? S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-2) = ? S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-3) = ? S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-5) = ? S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-0) = a S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-1) = ? S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-2) = 0 S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-3) = ? S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-4) = ? S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-5) = ? S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-1) = ? S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-2) = ? S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-5) = k S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-1) = ? S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-2) = ? S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-5) = k S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-1) = ? S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-2) = 0 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-5) = k S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-0) = a S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-1) = ? S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-2) = ? S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-3) = 15*a + 15*d + 6750 S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-4) = h S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-5) = k orients the transitions f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] weakly and the transitions f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] strictly and produces the following problem: 8: T: (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (56*a + 56*d + 7, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (56*a + 56*d + 7, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (56*a + 56*d + 7, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (56*a + 56*d + 7, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 A polynomial rank function with Pol(f5) = 2*V_1 - 2*V_2 + 1 Pol(f23) = 2*V_1 - 2*V_2 + 1 Pol(f9) = 2*V_1 - 2*V_2 Pol(f26) = 2*V_1 - 2*V_2 + 1 Pol(f40) = 2*V_1 - 2*V_2 + 1 Pol(f30) = 2*V_1 - 2*V_2 Pol(f69) = 2*V_1 - 2*V_2 + 1 Pol(f59) = 2*V_1 - 2*V_2 + 1 Pol(f44) = 2*V_1 - 2*V_2 Pol(f74) = 2*V_1 - 2*V_2 + 1 Pol(f71) = 2*V_1 - 2*V_2 + 1 Pol(f2) = 2*V_1 - 2*V_2 + 1 orients all transitions weakly and the transitions f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] strictly and produces the following problem: 9: T: (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (56*a + 56*d + 7, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (56*a + 56*d + 7, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (56*a + 56*d + 7, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (2*a + 2*b + 1, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (56*a + 56*d + 7, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (2*a + 2*b + 1, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (2*a + 2*b + 1, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 Repeatedly propagating knowledge in problem 9 produces the following problem: 10: T: (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (16*a + 2*b + 14*d + 3, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (56*a + 56*d + 7, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (56*a + 56*d + 7, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (56*a + 56*d + 7, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (2*a + 2*b + 1, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (56*a + 56*d + 7, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (2*a + 2*b + 1, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (2*a + 2*b + 1, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 A polynomial rank function with Pol(f59) = 0 Pol(f44) = 1 Pol(f40) = 0 Pol(f30) = -1 Pol(f26) = -1 and size complexities S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-0) = a S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-1) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-2) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-4) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ]", 0-5) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-0) = a S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-1) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-2) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-4) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ]", 0-5) = ? S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-0) = a S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-1) = b S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-2) = c S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-3) = d S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-4) = h S("f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k)", 0-5) = k S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-0) = a S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-2) = 0 S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-3) = 15*a + 15*d + 450 S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-4) = h S("f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ]", 0-5) = k S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-2) = ? S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-5) = k S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-2) = ? S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-5) = k S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-0) = a S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-1) = ? S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-2) = ? S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-3) = 71*a + 71*d + 2303737 S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-4) = ? S("f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ]", 0-5) = ? S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-0) = a S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-1) = ? S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-2) = ? S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-4) = ? S("f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ]", 0-5) = ? S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-2) = ? S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-5) = ? S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-0) = a S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-1) = ? S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-2) = ? S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-3) = 71*a + 71*d + 2303737 S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-4) = ? S("f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ]", 0-5) = ? S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-0) = a S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-1) = ? S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-2) = ? S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-4) = ? S("f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-5) = ? S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-0) = a S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-1) = ? S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-2) = ? S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-3) = 71*a + 71*d + 2303737 S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-4) = ? S("f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ]", 0-5) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-0) = a S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-1) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-2) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-3) = 71*a + 71*d + 2303737 S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-4) = ? S("f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k)", 0-5) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ]", 0-5) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ]", 0-5) = ? S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-0) = a S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-1) = ? S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-2) = ? S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-3) = 71*a + 71*d + 2303737 S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-4) = ? S("f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ]", 0-5) = ? S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-0) = a S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-1) = ? S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-2) = ? S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-4) = ? S("f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-5) = ? S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-0) = a S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-1) = ? S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-2) = ? S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-4) = ? S("f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ]", 0-5) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-0) = a S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-1) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-2) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-3) = 71*a + 71*d + 2303737 S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-4) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-5) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-0) = a S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-1) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-2) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-3) = 71*a + 71*d + 2303737 S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-4) = ? S("f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-5) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-0) = a S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-1) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-2) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-4) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-5) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-0) = a S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-1) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-2) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-3) = 71*a + 71*d + 2303737 S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-4) = ? S("f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-5) = ? S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-0) = a S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-1) = ? S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-2) = ? S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-3) = 71*a + 71*d + 2303737 S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-4) = ? S("f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-5) = 71*a + 71*d + 163565327 S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-2) = ? S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-3) = 71*a + 71*d + 2303737 S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ]", 0-5) = ? S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-0) = a S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-1) = ? S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-2) = 0 S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-3) = 71*a + 71*d + 2303737 S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-4) = ? S("f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ]", 0-5) = ? S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-2) = ? S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-5) = k S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-2) = ? S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-5) = k S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-0) = a S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-2) = 0 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-3) = 15*a + 15*d + 450 S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-4) = h S("f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-5) = k S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-0) = a S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-1) = 45*a + 45*b + 45*d + 637875 S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-2) = ? S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-3) = 15*a + 15*d + 6750 S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-4) = h S("f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ]", 0-5) = k orients the transitions f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] weakly and the transitions f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] strictly and produces the following problem: 11: T: (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (16*a + 2*b + 14*d + 3, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (56*a + 56*d + 7, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (10*a + 2*b + 8*d + 2, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (10*a + 2*b + 8*d + 2, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (56*a + 56*d + 7, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (56*a + 56*d + 7, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (2*a + 2*b + 1, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (56*a + 56*d + 7, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (2*a + 2*b + 1, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (2*a + 2*b + 1, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 A polynomial rank function with Pol(f5) = 2*V_1 - 2*V_5 + 1 Pol(f23) = 2*V_1 - 2*V_5 + 1 Pol(f9) = 2*V_1 - 2*V_5 + 1 Pol(f26) = 2*V_1 - 2*V_5 + 1 Pol(f40) = 2*V_1 - 2*V_5 + 1 Pol(f30) = 2*V_1 - 2*V_5 + 1 Pol(f69) = 2*V_1 - 2*V_5 + 1 Pol(f59) = 2*V_1 - 2*V_5 + 1 Pol(f44) = 2*V_1 - 2*V_5 + 1 Pol(f74) = 2*V_1 - 2*V_5 + 1 Pol(f71) = 2*V_1 - 2*V_5 + 1 Pol(f2) = 2*V_1 - 2*V_5 + 1 orients all transitions weakly and the transition f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] strictly and produces the following problem: 12: T: (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] (16*a + 2*b + 14*d + 3, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (56*a + 56*d + 7, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b >= d ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ h >= b ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (10*a + 2*b + 8*d + 2, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (10*a + 2*b + 8*d + 2, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (56*a + 56*d + 7, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (56*a + 56*d + 7, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b >= a + 1 ] (2*a + 2*b + 1, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ a >= b ] (56*a + 56*d + 7, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ a >= d + 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (2*a + 2*h + 1, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ d >= h + 1 ] (2*a + 2*b + 1, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ a >= b ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (2*a + 2*b + 1, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ l >= 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f2 leaf cost: 2 Applied AI with 'oct' on problem 12 to obtain the following invariants: For symbol f23: -X_1 + X_2 - 1 >= 0 For symbol f26: X_2 - X_4 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ -X_1 + X_2 - 1 >= 0 For symbol f30: -1 >= 0 For symbol f40: X_2 - X_4 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ -X_3 >= 0 /\ X_3 >= 0 /\ -X_1 + X_2 - 1 >= 0 For symbol f44: -1 >= 0 For symbol f59: X_2 - X_4 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ -X_3 >= 0 /\ X_3 >= 0 /\ -X_1 + X_2 - 1 >= 0 For symbol f69: X_2 - X_4 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ -X_3 >= 0 /\ X_3 >= 0 /\ -X_1 + X_2 - 1 >= 0 For symbol f71: X_2 - X_4 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ -X_3 >= 0 /\ X_3 >= 0 /\ -X_1 + X_2 - 1 >= 0 For symbol f74: X_2 - X_4 - 2 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ -X_3 >= 0 /\ X_3 >= 0 /\ -X_1 + X_2 - 1 >= 0 For symbol f9: X_3 >= 0 /\ X_1 - X_2 >= 0 This yielded the following problem: 13: T: (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ 0 >= l + 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ l >= 1 ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (2*a + 2*b + 1, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= 0 /\ a - b >= 0 /\ c >= l /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ c >= 0 /\ a - b >= 0 /\ l >= c + 1 /\ a >= d ] (8*a + 8*d + 1, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ -a + b - 1 >= 0 /\ a >= d ] (?, 1) f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -a + b - 1 >= 0 /\ d >= b + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ -1 >= 0 /\ b >= h + 1 ] (2*a + 2*b + 1, 1) f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= b ] (?, 1) f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ -1 >= 0 /\ d >= h + 1 ] (2*a + 2*h + 1, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= h ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= d + 1 ] (56*a + 56*d + 7, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ d >= a + 1 ] (2*a + 2*b + 1, 1) f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ b - d - 2 >= 0 /\ a - d - 1 >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= b ] (56*a + 56*d + 7, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b - d - 2 >= 0 /\ a - d - 1 >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ b >= a + 1 ] (56*a + 56*d + 7, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ h >= a + 1 ] (10*a + 2*b + 8*d + 2, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ -1 >= 0 /\ c >= m + 1 /\ h >= d ] (10*a + 2*b + 8*d + 2, 1) f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ -1 >= 0 /\ l >= c /\ h >= d ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ b >= a + 1 /\ k >= d + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ b >= a + 1 /\ d >= k + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ b >= a + 1 /\ d = k ] (?, 1) f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ -1 >= 0 /\ h >= b ] (56*a + 56*d + 7, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -a + b - 1 >= 0 /\ b >= d ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 0 /\ a - b >= 0 /\ 0 >= c + 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 0 /\ a - b >= 0 /\ c >= 1 /\ d >= a + 1 ] (16*a + 2*b + 14*d + 3, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ c >= 0 /\ a - b >= 0 /\ d >= a + 1 /\ c = 0 ] (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] start location: f2 leaf cost: 2 Testing for unsatisfiable constraints removes the following transitions from problem 13: f26(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -a + b - 1 >= 0 /\ d >= b + 1 ] f30(a, b, c, d, h, k) -> f30(a, b, c, d, h + 1, k) [ -1 >= 0 /\ b >= h + 1 ] f40(a, b, c, d, h, k) -> f44(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= b ] f44(a, b, c, d, h, k) -> f44(a, b, c, d, h + 1, k) [ -1 >= 0 /\ d >= h + 1 ] f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ d >= a + 1 ] f74(a, b, c, d, h, k) -> f74(a, b + 1, c, d, h, k) [ b - d - 2 >= 0 /\ a - d - 1 >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= b ] f44(a, b, c, d, h, k) -> f40(a, b + 1, c, d, h, k) [ -1 >= 0 /\ c >= m + 1 /\ h >= d ] f44(a, b, c, d, h, k) -> f40(a, b + 1, l, d, h, b) [ -1 >= 0 /\ l >= c /\ h >= d ] f30(a, b, c, d, h, k) -> f26(a, b + 1, c, d, h, k) [ -1 >= 0 /\ h >= b ] f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 0 /\ a - b >= 0 /\ 0 >= c + 1 /\ d >= a + 1 ] We thus obtain the following problem: 14: T: (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ 0 >= l + 1 ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ l >= 1 ] (1, 1) f2(a, b, c, d, h, k) -> f5(a, b, c, d, h, k) (2*a + 2*b + 1, 1) f5(a, b, c, d, h, k) -> f9(a, b, 0, d, h, k) [ a >= b ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, c, d + 1, h, k) [ c >= 0 /\ a - b >= 0 /\ c >= l /\ a >= d ] (7*a + 7*d + 1, 1) f9(a, b, c, d, h, k) -> f9(a, b, l, d + 1, h, k) [ c >= 0 /\ a - b >= 0 /\ l >= c + 1 /\ a >= d ] (8*a + 8*d + 1, 1) f23(a, b, c, d, h, k) -> f26(a, b, c, d, h, k) [ -a + b - 1 >= 0 /\ a >= d ] (2*a + 2*h + 1, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= h ] (56*a + 56*d + 7, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f74(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= d + 1 ] (56*a + 56*d + 7, 1) f74(a, b, c, d, h, k) -> f23(a, b, c, d + 1, h, k) [ b - d - 2 >= 0 /\ a - d - 1 >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ b >= a + 1 ] (56*a + 56*d + 7, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ h >= a + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ b >= a + 1 /\ k >= d + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ b >= a + 1 /\ d >= k + 1 ] (56*a + 56*d + 7, 1) f40(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ b >= a + 1 /\ d = k ] (56*a + 56*d + 7, 1) f26(a, b, c, d, h, k) -> f40(a, b, 0, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -a + b - 1 >= 0 /\ b >= d ] (14*a + 14*d + 2, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, c, d, h, k) [ c >= 0 /\ a - b >= 0 /\ c >= 1 /\ d >= a + 1 ] (16*a + 2*b + 14*d + 3, 1) f9(a, b, c, d, h, k) -> f5(a, b + 1, 0, d, h, k) [ c >= 0 /\ a - b >= 0 /\ d >= a + 1 /\ c = 0 ] (1, 1) f5(a, b, c, d, h, k) -> f23(a, b, c, d, h, k) [ b >= a + 1 ] start location: f2 leaf cost: 2 Complexity upper bound 568*a + 562*d + 4*b + 2*h + 78 Time: 2.756 sec (SMT: 2.427 sec)