YES(?, 932*a + 926*d + 4*b + 2*h + 141) 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) (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k) -> f12(a, b, c, d, e, f, g, h, i, j, k) (?, 1) f12(a, b, c, d, e, f, g, h, i, j, k) -> f15(a, b, 0, d, e, f, g, h, i, j, k) [ a >= b ] (?, 1) f15(a, b, c, d, e, f, g, h, i, j, k) -> f15(a, b, c, d + 1, l, l, g, h, i, j, k) [ c >= l /\ a >= d ] (?, 1) f15(a, b, c, d, e, f, g, h, i, j, k) -> f15(a, b, l, d + 1, l, l, g, h, i, j, k) [ l >= c + 1 /\ a >= d ] (?, 1) f28(a, b, c, d, e, f, g, h, i, j, k) -> f30(a, b, c, d, e, f, g, h, i, j, k) [ a >= d ] (?, 1) f30(a, b, c, d, e, f, g, h, i, j, k) -> f33(a, b, c, d, e, f, l, h, i, j, k) [ d >= b + 1 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k) -> f33(a, b, c, d, e, f, l, h + 1, i, j, k) [ b >= h + 1 ] (?, 1) f42(a, b, c, d, e, f, g, h, i, j, k) -> f45(a, b, c, d, e, f, l, h, i, j, k) [ a >= b ] (?, 1) f45(a, b, c, d, e, f, g, h, i, j, k) -> f45(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) f71(a, b, c, d, e, f, g, h, i, j, k) -> f73(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) -> f73(a, b, c, d, e, f, g, h, l, j, k) [ d >= a + 1 ] (?, 1) f73(a, b, c, d, e, f, g, h, i, j, k) -> f73(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) -> f28(a, b, c, a + 1, e, f, g, h, i, j, k) [ a = d ] (?, 1) f73(a, b, c, d, e, f, g, h, i, j, k) -> f28(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) f45(a, b, c, d, e, f, g, h, i, j, k) -> f42(a, b + 1, c, d, e, f, g, h, m, l, k) [ c >= m + 1 /\ h >= d ] (?, 1) f45(a, b, c, d, e, f, g, h, i, j, k) -> f42(a, b + 1, l, d, e, f, g, h, l, m, b) [ l >= c /\ h >= d ] (?, 1) f42(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) f42(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) f42(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) f33(a, b, c, d, e, f, g, h, i, j, k) -> f30(a, b + 1, c, d, e, f, g, h, i, j, k) [ h >= b ] (?, 1) f30(a, b, c, d, e, f, g, h, i, j, k) -> f42(a, b, 0, d, e, f, g, h, i, j, k) [ b >= d ] (?, 1) f28(a, b, c, d, e, f, g, h, i, j, k) -> f82(a, b, c, d, e, f, g, h, i, j, k) [ d >= a + 1 ] (?, 1) f15(a, b, c, d, e, f, g, h, i, j, k) -> f12(a, b + 1, c, d, e, f, g, h, i, j, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f15(a, b, c, d, e, f, g, h, i, j, k) -> f12(a, b + 1, c, d, e, f, g, h, i, j, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f15(a, b, c, d, e, f, g, h, i, j, k) -> f12(a, b + 1, 0, d, e, f, g, h, i, j, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f12(a, b, c, d, e, f, g, h, i, j, k) -> f28(a, b, c, d, e, f, g, h, i, j, k) [ b >= a + 1 ] start location: f0 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) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f28(a, b, c, d, h, k) -> f82(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(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) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f28(a, b, c, a + 1, h, k) [ a = d ] (?, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (?, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (?, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(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) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (?, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (?, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f12) = 1 Pol(f28) = -2 Pol(f15) = 1 Pol(f30) = -2 Pol(f42) = -2 Pol(f33) = -2 Pol(f69) = -2 Pol(f59) = -2 Pol(f45) = -2 Pol(f73) = -2 Pol(f71) = -2 Pol(f0) = 1 orients all transitions weakly and the transition f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] strictly and produces the following problem: 4: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(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) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (?, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (?, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f12) = 7*V_1 - 7*V_4 + 1 Pol(f28) = 9*V_1 - 2*V_2 - 7*V_4 - 3 Pol(f15) = 7*V_1 - 7*V_4 + 1 Pol(f30) = 9*V_1 - 2*V_2 - 7*V_4 - 4 Pol(f42) = 9*V_1 - 2*V_2 - 7*V_4 - 5 Pol(f33) = 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(f45) = 9*V_1 - 2*V_2 - 7*V_4 - 6 Pol(f73) = 9*V_1 - 2*V_2 - 7*V_4 - 9 Pol(f71) = 9*V_1 - 2*V_2 - 7*V_4 - 8 Pol(f0) = 7*V_1 - 7*V_4 + 1 orients all transitions weakly and the transitions f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] strictly and produces the following problem: 5: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(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) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 Repeatedly propagating knowledge in problem 5 produces the following problem: 6: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(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) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (?, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f12) = 8*V_1 - 8*V_4 + 1 Pol(f28) = 8*V_1 - 8*V_4 + 1 Pol(f15) = 8*V_1 - 8*V_4 + 1 Pol(f30) = 8*V_1 - 8*V_4 - 1 Pol(f42) = 8*V_1 - 8*V_4 - 2 Pol(f33) = 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(f45) = 8*V_1 - 8*V_4 - 2 Pol(f73) = 8*V_1 - 8*V_4 - 6 Pol(f71) = 8*V_1 - 8*V_4 - 5 Pol(f0) = 8*V_1 - 8*V_4 + 1 orients all transitions weakly and the transitions f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] strictly and produces the following problem: 7: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (?, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(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) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (?, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (?, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f73) = -1 Pol(f28) = -2 Pol(f71) = 1 Pol(f69) = 2 Pol(f59) = 3 Pol(f45) = 4 Pol(f42) = 4 Pol(f33) = 5 Pol(f30) = 5 Pol(f15) = -1 Pol(f12) = -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) = ? 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)", 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("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-0) = a S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-1) = b S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-2) = c S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-3) = d S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-4) = h S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-5) = k S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-0) = a S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-1) = ? S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-2) = 0 S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-3) = 15*a + 15*d + 450 S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-4) = h S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-5) = k S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-0) = a S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-1) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-2) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-3) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-4) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-5) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-2) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-3) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-5) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-0) = a S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-1) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-2) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-3) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-4) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-3) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-5) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-0) = a S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-1) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-2) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-3) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-4) = ? S("f45(a, b, c, d, h, k) -> f45(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("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-3) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-5) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-3) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-5) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-0) = a S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-1) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-2) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-3) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-4) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-5) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-0) = a S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-1) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-2) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-3) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-4) = ? S("f73(a, b, c, d, h, k) -> f28(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("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-0) = a S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-1) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-2) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-3) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-4) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-5) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-0) = a S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-1) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-2) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-3) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-4) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-3) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-3) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-3) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-5) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-0) = a S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-1) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-2) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-3) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-4) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-5) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-2) = 0 S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-3) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-5) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-2) = 0 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-5) = k S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-1) = ? S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-3) = 15*a + 15*d + 6750 S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-4) = h S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-5) = k orients the transitions f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 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 ] f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] weakly and the transitions f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 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 ] f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] strictly and produces the following problem: 8: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (90*a + 90*d + 13, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (90*a + 90*d + 13, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (?, 1) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (90*a + 90*d + 13, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f73) = 1 Pol(f28) = 0 Pol(f59) = 0 Pol(f45) = -1 Pol(f42) = -1 Pol(f33) = -1 Pol(f30) = -1 Pol(f15) = -1 Pol(f12) = -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) = ? 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)", 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("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-0) = a S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-1) = b S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-2) = c S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-3) = d S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-4) = h S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-5) = k S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-0) = a S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-1) = ? S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-2) = 0 S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-3) = 15*a + 15*d + 450 S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-4) = h S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-5) = k S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-0) = a S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-1) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-2) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-3) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-4) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-5) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-2) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-3) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-5) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-0) = a S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-1) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-2) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-3) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-4) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-3) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-5) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-0) = a S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-1) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-2) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-3) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-4) = ? S("f45(a, b, c, d, h, k) -> f45(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("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-3) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-5) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-3) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-5) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-0) = a S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-1) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-2) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-3) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-4) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-5) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-0) = a S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-1) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-2) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-3) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-4) = ? S("f73(a, b, c, d, h, k) -> f28(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("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-0) = a S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-1) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-2) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-3) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-4) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-5) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-0) = a S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-1) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-2) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-3) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-4) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-3) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-3) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-3) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-5) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-0) = a S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-1) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-2) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-3) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-4) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-5) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-2) = 0 S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-3) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-5) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-1) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-2) = 0 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-5) = k S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-1) = ? S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-3) = 15*a + 15*d + 6750 S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-4) = h S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-5) = k orients the transitions f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] weakly and the transition f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] strictly and produces the following problem: 9: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (90*a + 90*d + 13, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (90*a + 90*d + 13, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (238*a + 238*d + 35, 1) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (?, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (90*a + 90*d + 13, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (?, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (?, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f12) = 2*V_1 - 2*V_2 + 1 Pol(f28) = 2*V_1 - 2*V_2 + 1 Pol(f15) = 2*V_1 - 2*V_2 Pol(f30) = 2*V_1 - 2*V_2 + 1 Pol(f42) = 2*V_1 - 2*V_2 + 1 Pol(f33) = 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(f45) = 2*V_1 - 2*V_2 Pol(f73) = 2*V_1 - 2*V_2 + 1 Pol(f71) = 2*V_1 - 2*V_2 + 1 Pol(f0) = 2*V_1 - 2*V_2 + 1 orients all transitions weakly and the transitions f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] strictly and produces the following problem: 10: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (?, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (90*a + 90*d + 13, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (90*a + 90*d + 13, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (238*a + 238*d + 35, 1) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (2*a + 2*b + 1, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (90*a + 90*d + 13, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (2*a + 2*b + 1, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (2*a + 2*b + 1, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 Repeatedly propagating knowledge in problem 10 produces the following problem: 11: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (16*a + 2*b + 14*d + 3, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (90*a + 90*d + 13, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ k >= d + 1 ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (?, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (90*a + 90*d + 13, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (238*a + 238*d + 35, 1) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (2*a + 2*b + 1, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (90*a + 90*d + 13, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (2*a + 2*b + 1, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (2*a + 2*b + 1, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f59) = 0 Pol(f45) = 1 Pol(f42) = 0 Pol(f33) = -1 Pol(f30) = -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) = 253*a + 253*d + 31044365 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)", 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) = 253*a + 253*d + 31044365 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("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-0) = a S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-1) = b S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-2) = c S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-3) = d S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-4) = h S("f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k)", 0-5) = k S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-0) = a S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-2) = 0 S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-3) = 15*a + 15*d + 450 S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-4) = h S("f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\\ a >= d ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\\ a >= d ]", 0-5) = k S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-0) = a S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-1) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-2) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-3) = 253*a + 253*d + 31044365 S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-4) = ? S("f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ]", 0-5) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-2) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-3) = 253*a + 253*d + 31044365 S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ]", 0-5) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-0) = a S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-1) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-2) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-3) = 253*a + 253*d + 31044365 S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-4) = ? S("f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-3) = 253*a + 253*d + 31044365 S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ]", 0-5) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-0) = a S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-1) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-2) = ? S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-3) = 253*a + 253*d + 31044365 S("f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ]", 0-4) = ? S("f45(a, b, c, d, h, k) -> f45(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) = 253*a + 253*d + 31044365 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("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-3) = 253*a + 253*d + 31044365 S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ]", 0-5) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-0) = a S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-1) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-2) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-3) = 253*a + 253*d + 31044365 S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-4) = ? S("f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ]", 0-5) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-0) = a S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-1) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-2) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-3) = 253*a + 253*d + 31044365 S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-4) = ? S("f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ]", 0-5) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-0) = a S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-1) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-2) = ? S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-3) = 253*a + 253*d + 31044365 S("f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ]", 0-4) = ? S("f73(a, b, c, d, h, k) -> f28(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) = 253*a + 253*d + 31044365 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("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-0) = a S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-1) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-2) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-3) = 253*a + 253*d + 31044365 S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-4) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\\ h >= d ]", 0-5) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-0) = a S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-1) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-2) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-3) = 253*a + 253*d + 31044365 S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-4) = ? S("f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\\ h >= d ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-3) = 253*a + 253*d + 31044365 S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ k >= d + 1 ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-3) = 253*a + 253*d + 31044365 S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\\ d >= k + 1 ]", 0-5) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-0) = a S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-1) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-2) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-3) = 253*a + 253*d + 31044365 S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-4) = ? S("f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\\ d = k ]", 0-5) = 253*a + 253*d + 7854224345 S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-0) = a S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-1) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-2) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-3) = 253*a + 253*d + 31044365 S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-4) = ? S("f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ]", 0-5) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-0) = a S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-1) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-2) = 0 S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-3) = 253*a + 253*d + 31044365 S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-4) = ? S("f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ]", 0-5) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\\ d >= a + 1 ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-2) = ? S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\\ d >= a + 1 ]", 0-5) = k S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-0) = a S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-1) = 45*a + 45*b + 45*d + 14175 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-2) = 0 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-3) = 15*a + 15*d + 450 S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-4) = h S("f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\\ c = 0 ]", 0-5) = k S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-1) = 45*a + 45*b + 45*d + 637875 S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-3) = 15*a + 15*d + 6750 S("f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ]", 0-4) = h S("f12(a, b, c, d, h, k) -> f28(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 ] f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] weakly and the transitions f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] strictly and produces the following problem: 12: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (16*a + 2*b + 14*d + 3, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (90*a + 90*d + 13, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (90*a + 90*d + 13, 1) f42(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) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (10*a + 2*b + 8*d + 2, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (90*a + 90*d + 13, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (238*a + 238*d + 35, 1) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (2*a + 2*b + 1, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (90*a + 90*d + 13, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (?, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (2*a + 2*b + 1, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (2*a + 2*b + 1, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 A polynomial rank function with Pol(f12) = 2*V_1 - 2*V_5 + 1 Pol(f28) = 2*V_1 - 2*V_5 + 1 Pol(f15) = 2*V_1 - 2*V_5 + 1 Pol(f30) = 2*V_1 - 2*V_5 + 1 Pol(f42) = 2*V_1 - 2*V_5 + 1 Pol(f33) = 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(f45) = 2*V_1 - 2*V_5 + 1 Pol(f73) = 2*V_1 - 2*V_5 + 1 Pol(f71) = 2*V_1 - 2*V_5 + 1 Pol(f0) = 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: 13: T: (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] (16*a + 2*b + 14*d + 3, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ d >= a + 1 /\ c = 0 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ 0 >= c + 1 /\ d >= a + 1 ] (90*a + 90*d + 13, 1) f30(a, b, c, d, h, k) -> f42(a, b, 0, d, h, k) [ b >= d ] (?, 1) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ h >= b ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f69(a, b, c, d, h, d) [ b >= a + 1 /\ d = k ] (90*a + 90*d + 13, 1) f42(a, b, c, d, h, k) -> f59(a, b, c, d, h, k) [ b >= a + 1 /\ d >= k + 1 ] (90*a + 90*d + 13, 1) f42(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) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ l >= c /\ h >= d ] (10*a + 2*b + 8*d + 2, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ c >= m + 1 /\ h >= d ] (90*a + 90*d + 13, 1) f59(a, b, c, d, h, k) -> f69(a, b, c, d, h, k) [ h >= a + 1 ] (238*a + 238*d + 35, 1) f73(a, b, c, d, h, k) -> f28(a, b, c, d + 1, h, k) [ b >= a + 1 ] (2*a + 2*b + 1, 1) f73(a, b, c, d, h, k) -> f73(a, b + 1, c, d, h, k) [ a >= b ] (90*a + 90*d + 13, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ d >= a + 1 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ a >= d + 1 ] (2*a + 2*h + 1, 1) f59(a, b, c, d, h, k) -> f59(a, b, c, d, h + 1, k) [ a >= h ] (?, 1) f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ d >= h + 1 ] (2*a + 2*b + 1, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ a >= b ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ b >= h + 1 ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ d >= b + 1 ] (8*a + 8*d + 1, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ l >= c + 1 /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= l /\ a >= d ] (2*a + 2*b + 1, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) (90*a + 90*d + 13, 1) f69(a, b, c, d, h, k) -> f71(a, b, c, d, h, k) [ 0 >= l + 1 ] start location: f0 leaf cost: 2 Applied AI with 'oct' on problem 13 to obtain the following invariants: For symbol f15: X_3 >= 0 /\ X_1 - X_2 >= 0 For symbol f28: -X_1 + X_2 - 1 >= 0 For symbol f30: X_2 - X_4 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ -X_1 + X_2 - 1 >= 0 For symbol f33: -1 >= 0 For symbol f42: 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 f45: -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 f73: X_2 - X_4 - 2 >= 0 /\ X_1 - X_4 - 1 >= 0 /\ -X_3 >= 0 /\ X_3 >= 0 /\ -X_1 + X_2 - 1 >= 0 This yielded the following problem: 14: T: (90*a + 90*d + 13, 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 ] (90*a + 90*d + 13, 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 ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (2*a + 2*b + 1, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= 0 /\ a - b >= 0 /\ c >= l /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ c >= 0 /\ a - b >= 0 /\ l >= c + 1 /\ a >= d ] (8*a + 8*d + 1, 1) f28(a, b, c, d, h, k) -> f30(a, b, c, d, h, k) [ -a + b - 1 >= 0 /\ a >= d ] (?, 1) f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -a + b - 1 >= 0 /\ d >= b + 1 ] (?, 1) f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ -1 >= 0 /\ b >= h + 1 ] (2*a + 2*b + 1, 1) f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= b ] (?, 1) f45(a, b, c, d, h, k) -> f45(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 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= d + 1 ] (90*a + 90*d + 13, 1) f71(a, b, c, d, h, k) -> f73(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) f73(a, b, c, d, h, k) -> f73(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 ] (238*a + 238*d + 35, 1) f73(a, b, c, d, h, k) -> f28(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 ] (90*a + 90*d + 13, 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) f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ -1 >= 0 /\ c >= m + 1 /\ h >= d ] (10*a + 2*b + 8*d + 2, 1) f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ -1 >= 0 /\ l >= c /\ h >= d ] (90*a + 90*d + 13, 1) f42(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 ] (90*a + 90*d + 13, 1) f42(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 ] (90*a + 90*d + 13, 1) f42(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) f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ -1 >= 0 /\ h >= b ] (90*a + 90*d + 13, 1) f30(a, b, c, d, h, k) -> f42(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) f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 0 /\ a - b >= 0 /\ 0 >= c + 1 /\ d >= a + 1 ] (14*a + 14*d + 2, 1) f15(a, b, c, d, h, k) -> f12(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) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ c >= 0 /\ a - b >= 0 /\ d >= a + 1 /\ c = 0 ] (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] start location: f0 leaf cost: 2 Testing for unsatisfiable constraints removes the following transitions from problem 14: f30(a, b, c, d, h, k) -> f33(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -a + b - 1 >= 0 /\ d >= b + 1 ] f33(a, b, c, d, h, k) -> f33(a, b, c, d, h + 1, k) [ -1 >= 0 /\ b >= h + 1 ] f42(a, b, c, d, h, k) -> f45(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= b ] f45(a, b, c, d, h, k) -> f45(a, b, c, d, h + 1, k) [ -1 >= 0 /\ d >= h + 1 ] f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ d >= a + 1 ] f73(a, b, c, d, h, k) -> f73(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 ] f45(a, b, c, d, h, k) -> f42(a, b + 1, c, d, h, k) [ -1 >= 0 /\ c >= m + 1 /\ h >= d ] f45(a, b, c, d, h, k) -> f42(a, b + 1, l, d, h, b) [ -1 >= 0 /\ l >= c /\ h >= d ] f33(a, b, c, d, h, k) -> f30(a, b + 1, c, d, h, k) [ -1 >= 0 /\ h >= b ] f15(a, b, c, d, h, k) -> f12(a, b + 1, c, d, h, k) [ c >= 0 /\ a - b >= 0 /\ 0 >= c + 1 /\ d >= a + 1 ] We thus obtain the following problem: 15: T: (90*a + 90*d + 13, 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 ] (90*a + 90*d + 13, 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 ] (1, 1) f0(a, b, c, d, h, k) -> f12(a, b, c, d, h, k) (2*a + 2*b + 1, 1) f12(a, b, c, d, h, k) -> f15(a, b, 0, d, h, k) [ a >= b ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, c, d + 1, h, k) [ c >= 0 /\ a - b >= 0 /\ c >= l /\ a >= d ] (7*a + 7*d + 1, 1) f15(a, b, c, d, h, k) -> f15(a, b, l, d + 1, h, k) [ c >= 0 /\ a - b >= 0 /\ l >= c + 1 /\ a >= d ] (8*a + 8*d + 1, 1) f28(a, b, c, d, h, k) -> f30(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 ] (8*a + 8*d + 1, 1) f71(a, b, c, d, h, k) -> f73(a, b, c, d, h, k) [ b - d - 1 >= 0 /\ a - d >= 0 /\ -c >= 0 /\ c >= 0 /\ -a + b - 1 >= 0 /\ a >= d + 1 ] (238*a + 238*d + 35, 1) f73(a, b, c, d, h, k) -> f28(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 ] (90*a + 90*d + 13, 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 ] (90*a + 90*d + 13, 1) f42(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 ] (90*a + 90*d + 13, 1) f42(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 ] (90*a + 90*d + 13, 1) f42(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 ] (90*a + 90*d + 13, 1) f30(a, b, c, d, h, k) -> f42(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) f15(a, b, c, d, h, k) -> f12(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) f15(a, b, c, d, h, k) -> f12(a, b + 1, 0, d, h, k) [ c >= 0 /\ a - b >= 0 /\ d >= a + 1 /\ c = 0 ] (1, 1) f12(a, b, c, d, h, k) -> f28(a, b, c, d, h, k) [ b >= a + 1 ] start location: f0 leaf cost: 2 Complexity upper bound 932*a + 926*d + 4*b + 2*h + 141 Time: 2.517 sec (SMT: 2.204 sec)