YES(?, 3977) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l) -> f23(1, 1, 10, m, n, 0, g, h, i, j, k, l) (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, l) -> f23(a, b, c, d, e, f + 1, g, h, i, j, k, l) [ c >= f + 1 ] (?, 1) f29(a, b, c, d, e, f, g, h, i, j, k, l) -> f33(a, b, c, d, e, f, 0, 0, i, j, k, l) [ c >= f + 1 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l) -> f33(a, b, c, d, e, f, 1, h + 1, 1, j, k, l) [ 0 >= g + 1 /\ c >= h + 1 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l) -> f33(a, b, c, d, e, f, 1, h + 1, 1, j, k, l) [ g >= 1 /\ c >= h + 1 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l) -> f33(a, b, c, d, e, f, 1, h + 1, 1, j, k, l) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l) -> f33(a, b, c, d, e, f, 0, h + 1, 0, j, k, l) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l) -> f33(a, b, c, d, e, f, 0, h + 1, 0, j, k, l) [ c >= h + 1 /\ g = 0 ] (?, 1) f44(a, b, c, d, e, f, g, h, i, j, k, l) -> f29(1, b, c, d, e, f + 1, g, h, i, 1, k, l) [ 0 >= g + 1 ] (?, 1) f44(a, b, c, d, e, f, g, h, i, j, k, l) -> f29(1, b, c, d, e, f + 1, g, h, i, 1, k, l) [ g >= 1 ] (?, 1) f44(a, b, c, d, e, f, g, h, i, j, k, l) -> f29(0, b, c, d, e, f + 1, 0, h, i, 0, k, l) [ g = 0 ] (?, 1) f52(a, b, c, d, e, f, g, h, i, j, k, l) -> f55(a, b, c, d, e, f, g, h, i, j, k, l) [ 0 >= b + 1 /\ c >= f + 2 ] (?, 1) f52(a, b, c, d, e, f, g, h, i, j, k, l) -> f55(a, b, c, d, e, f, g, h, i, j, k, l) [ b >= 1 /\ c >= f + 2 ] (?, 1) f55(a, b, c, d, e, f, g, h, i, j, k, l) -> f52(a, 1, c, d, e, f + 1, g, h, i, j, 1, l) [ m >= n + 1 ] (?, 1) f55(a, b, c, d, e, f, g, h, i, j, k, l) -> f52(a, 0, c, d, e, f + 1, g, h, i, j, 0, l) (?, 1) f52(a, b, c, d, e, f, g, h, i, j, k, l) -> f52(a, 0, c, d, e, f + 1, g, h, i, j, 0, l) [ c >= f + 2 /\ b = 0 ] (?, 1) f63(a, b, c, d, e, f, g, h, i, j, k, l) -> f71(a, b, c, d, e, f, g, h, i, j, k, 0) [ 0 >= b + 1 ] (?, 1) f63(a, b, c, d, e, f, g, h, i, j, k, l) -> f71(a, b, c, d, e, f, g, h, i, j, k, 0) [ b >= 1 ] (?, 1) f63(a, b, c, d, e, f, g, h, i, j, k, l) -> f71(a, 0, c, d, e, f, g, h, i, j, k, 1) [ b = 0 ] (?, 1) f52(a, b, c, d, e, f, g, h, i, j, k, l) -> f63(a, b, c, d, e, f, g, h, i, j, k, l) [ 0 >= a + 1 /\ f + 1 >= c ] (?, 1) f52(a, b, c, d, e, f, g, h, i, j, k, l) -> f63(a, b, c, d, e, f, g, h, i, j, k, l) [ a >= 1 /\ f + 1 >= c ] (?, 1) f52(a, b, c, d, e, f, g, h, i, j, k, l) -> f71(0, b, c, d, e, f, g, h, i, j, k, 1) [ f + 1 >= c /\ a = 0 ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l) -> f44(a, b, c, d, e, f, g, h, i, j, k, l) [ 0 >= a + 1 /\ h >= c ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l) -> f44(a, b, c, d, e, f, g, h, i, j, k, l) [ a >= 1 /\ h >= c ] (?, 1) f33(a, b, c, d, e, f, g, h, i, j, k, l) -> f29(0, b, c, d, e, f + 1, g, h, i, 0, k, l) [ h >= c /\ a = 0 ] (?, 1) f29(a, b, c, d, e, f, g, h, i, j, k, l) -> f52(a, b, c, d, e, 0, g, h, i, j, k, l) [ f >= c ] (?, 1) f23(a, b, c, d, e, f, g, h, i, j, k, l) -> f29(a, b, c, d, e, 0, g, h, i, j, k, l) [ f >= c ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, f, g, h]. We thus obtain the following problem: 2: T: (?, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (?, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (?, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (?, 1) f52(a, b, c, f, g, h) -> f71(0, b, c, f, g, h) [ f + 1 >= c /\ a = 0 ] (?, 1) f52(a, b, c, f, g, h) -> f63(a, b, c, f, g, h) [ a >= 1 /\ f + 1 >= c ] (?, 1) f52(a, b, c, f, g, h) -> f63(a, b, c, f, g, h) [ 0 >= a + 1 /\ f + 1 >= c ] (?, 1) f63(a, b, c, f, g, h) -> f71(a, 0, c, f, g, h) [ b = 0 ] (?, 1) f63(a, b, c, f, g, h) -> f71(a, b, c, f, g, h) [ b >= 1 ] (?, 1) f63(a, b, c, f, g, h) -> f71(a, b, c, f, g, h) [ 0 >= b + 1 ] (?, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (?, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (?, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (?, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (?, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ 0 >= g + 1 /\ c >= h + 1 ] (?, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (?, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (?, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (?, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (?, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (?, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (?, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (?, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (?, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ 0 >= g + 1 /\ c >= h + 1 ] (?, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (?, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 6 Testing for reachability in the complexity graph removes the following transition from problem 3: f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ 0 >= g + 1 /\ c >= h + 1 ] We thus obtain the following problem: 4: T: (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (?, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (?, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (?, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (?, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (?, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (?, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (?, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 6 A polynomial rank function with Pol(f33) = 1 Pol(f55) = -3 Pol(f52) = -3 Pol(f44) = 1 Pol(f29) = 1 Pol(f23) = 2 Pol(f0) = 2 orients all transitions weakly and the transitions f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] strictly and produces the following problem: 5: T: (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (?, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (?, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (?, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (?, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (2, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (2, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (?, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 6 Repeatedly propagating knowledge in problem 5 produces the following problem: 6: T: (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (2, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (?, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (?, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (?, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (2, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (2, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (?, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 6 A polynomial rank function with Pol(f33) = 2*V_3 - 2 Pol(f55) = 2*V_3 - 2*V_4 - 3 Pol(f52) = 2*V_3 - 2*V_4 - 2 Pol(f44) = 2*V_3 - 2 Pol(f29) = 2*V_3 - 2 Pol(f23) = 2*V_3 - 2 Pol(f0) = 18 orients all transitions weakly and the transitions f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] strictly and produces the following problem: 7: T: (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (?, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (2, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (?, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (2, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (2, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (?, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 6 Repeatedly propagating knowledge in problem 7 produces the following problem: 8: T: (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (20, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (20, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (2, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (?, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (2, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (2, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (?, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 6 A polynomial rank function with Pol(f44) = 3*V_3 - 3*V_4 - 3 Pol(f29) = 3*V_3 - 3*V_4 - 1 Pol(f33) = 3*V_3 - 3*V_4 - 2 Pol(f23) = V_3 - V_4 and size complexities S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-0) = 1 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-1) = 1 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-2) = 10 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-3) = 0 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-4) = g S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-5) = h S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-0) = 1 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-1) = 1 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-2) = 10 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-3) = ? S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-4) = g S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-5) = h S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-0) = 1 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-1) = 1 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-2) = 10 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-3) = 0 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-4) = g S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-5) = h S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-0) = 1 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-1) = 1 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-2) = 10 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-3) = 0 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-4) = g + 3 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-5) = ? S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-0) = 1 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-1) = 1 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-2) = 10 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-3) = ? S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-4) = 0 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-5) = 0 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-0) = 1 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-1) = 0 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-2) = 10 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-3) = 39 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-4) = g + 3 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-5) = ? S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-0) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-1) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-2) = 10 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-3) = 20 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-4) = g + 3 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-5) = ? S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-0) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-1) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-2) = 10 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-3) = 0 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-4) = g + 3 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-0) = 0 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-4) = 0 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-4) = 0 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-5) = ? S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-0) = 0 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-1) = 1 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-2) = 10 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-3) = ? S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-4) = 0 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-5) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-0) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-1) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-2) = 10 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-3) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-4) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-5) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-0) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-1) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-2) = 10 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-3) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-4) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-5) = ? S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-0) = 1 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-1) = 0 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-2) = 10 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-3) = 21 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-4) = g + 3 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-5) = ? S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-0) = 1 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-1) = 1 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-2) = 10 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-3) = 20 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-4) = g + 3 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-5) = ? orients the transitions f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] weakly and the transitions f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] strictly and produces the following problem: 9: T: (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (20, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (20, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (?, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (?, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (2, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (72, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (2, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (2, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (72, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 6 A polynomial rank function with Pol(f44) = 1 Pol(f29) = 0 Pol(f33) = 2 and size complexities S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-0) = 1 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-1) = 1 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-2) = 10 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-3) = 0 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-4) = g S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-5) = h S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-0) = 1 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-1) = 1 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-2) = 10 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-3) = 72 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-4) = g S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-5) = h S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-0) = 1 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-1) = 1 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-2) = 10 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-3) = 0 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-4) = g S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-5) = h S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-0) = 1 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-1) = 1 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-2) = 10 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-3) = 0 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-4) = g + 3 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-5) = ? S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-0) = 1 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-1) = 1 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-2) = 10 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-3) = ? S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-4) = 0 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-5) = 0 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-0) = 1 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-1) = 0 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-2) = 10 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-3) = 39 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-4) = g + 3 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-5) = ? S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-0) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-1) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-2) = 10 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-3) = 20 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-4) = g + 3 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-5) = ? S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-0) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-1) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-2) = 10 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-3) = 0 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-4) = g + 3 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-0) = 0 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-4) = 0 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-4) = 0 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-5) = ? S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-0) = 0 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-1) = 1 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-2) = 10 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-3) = ? S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-4) = 0 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-5) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-0) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-1) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-2) = 10 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-3) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-4) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-5) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-0) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-1) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-2) = 10 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-3) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-4) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-5) = ? S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-0) = 1 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-1) = 0 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-2) = 10 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-3) = 21 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-4) = g + 3 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-5) = ? S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-0) = 1 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-1) = 1 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-2) = 10 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-3) = 20 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-4) = g + 3 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-3) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-5) = ? orients the transitions f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] weakly and the transitions f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] strictly and produces the following problem: 10: T: (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (20, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (20, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (144, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (144, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (144, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (?, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (144, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (144, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (144, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (2, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (72, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (2, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (2, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (72, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 6 A polynomial rank function with Pol(f33) = V_3 - V_6 and size complexities S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-0) = 1 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-1) = 1 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-2) = 10 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-3) = 0 S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-4) = g S("f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h)", 0-5) = h S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-0) = 1 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-1) = 1 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-2) = 10 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-3) = 72 S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-4) = g S("f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ]", 0-5) = h S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-0) = 1 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-1) = 1 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-2) = 10 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-3) = 0 S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-4) = g S("f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ]", 0-5) = h S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-0) = 1 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-1) = 1 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-2) = 10 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-3) = 0 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-4) = g + 3 S("f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ]", 0-5) = ? S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-0) = 1 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-1) = 1 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-2) = 10 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-3) = 576 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-4) = 0 S("f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ]", 0-5) = 0 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-0) = 1 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-1) = 0 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-2) = 10 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-3) = 39 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-4) = g + 3 S("f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\\ b = 0 ]", 0-5) = ? S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-0) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-1) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-2) = 10 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-3) = 20 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-4) = g + 3 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\\ c >= f + 2 ]", 0-5) = ? S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-0) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-1) = 1 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-2) = 10 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-3) = 0 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-4) = g + 3 S("f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\\ c >= f + 2 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-0) = 0 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-3) = 576 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\\ a = 0 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-3) = 576 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\\ h >= c ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-3) = 576 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\\ h >= c ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-3) = 576 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-4) = 0 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-3) = 576 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-4) = 0 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\\ c >= h + 1 /\\ g = 0 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-3) = 576 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\\ g = 0 ]", 0-5) = ? S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-0) = 0 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-1) = 1 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-2) = 10 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-3) = 576 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-4) = 0 S("f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ]", 0-5) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-0) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-1) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-2) = 10 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-3) = 576 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-4) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ]", 0-5) = ? S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-0) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-1) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-2) = 10 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-3) = 576 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-4) = 1 S("f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ]", 0-5) = ? S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-0) = 1 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-1) = 0 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-2) = 10 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-3) = 21 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-4) = g + 3 S("f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h)", 0-5) = ? S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-0) = 1 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-1) = 1 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-2) = 10 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-3) = 20 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-4) = g + 3 S("f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ]", 0-5) = ? S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-0) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-1) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-2) = 10 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-3) = 576 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-4) = 1 S("f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\\ c >= h + 1 ]", 0-5) = ? orients the transitions f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] weakly and the transitions f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] strictly and produces the following problem: 11: T: (720, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ g >= 1 /\ c >= h + 1 ] (20, 1) f55(a, b, c, f, g, h) -> f52(a, 1, c, f + 1, g, h) [ m >= n + 1 ] (20, 1) f55(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) (144, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ 0 >= g + 1 ] (144, 1) f44(a, b, c, f, g, h) -> f29(1, b, c, f + 1, g, h) [ g >= 1 ] (144, 1) f44(a, b, c, f, g, h) -> f29(0, b, c, f + 1, 0, h) [ g = 0 ] (720, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 1, h + 1) [ c >= h + 1 /\ g = 0 ] (720, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ m >= n + 1 /\ c >= h + 1 /\ g = 0 ] (720, 1) f33(a, b, c, f, g, h) -> f33(a, b, c, f, 0, h + 1) [ c >= h + 1 /\ g = 0 ] (144, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ 0 >= a + 1 /\ h >= c ] (144, 1) f33(a, b, c, f, g, h) -> f44(a, b, c, f, g, h) [ a >= 1 /\ h >= c ] (144, 1) f33(a, b, c, f, g, h) -> f29(0, b, c, f + 1, g, h) [ h >= c /\ a = 0 ] (2, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ 0 >= b + 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f55(a, b, c, f, g, h) [ b >= 1 /\ c >= f + 2 ] (18, 1) f52(a, b, c, f, g, h) -> f52(a, 0, c, f + 1, g, h) [ c >= f + 2 /\ b = 0 ] (72, 1) f29(a, b, c, f, g, h) -> f33(a, b, c, f, 0, 0) [ c >= f + 1 ] (2, 1) f29(a, b, c, f, g, h) -> f52(a, b, c, 0, g, h) [ f >= c ] (2, 1) f23(a, b, c, f, g, h) -> f29(a, b, c, 0, g, h) [ f >= c ] (72, 1) f23(a, b, c, f, g, h) -> f23(a, b, c, f + 1, g, h) [ c >= f + 1 ] (1, 1) f0(a, b, c, f, g, h) -> f23(1, 1, 10, 0, g, h) start location: f0 leaf cost: 6 Complexity upper bound 3977 Time: 1.143 sec (SMT: 1.000 sec)