MAYBE Initial complexity problem: 1: T: (?, 1) f0(a, b, c, d, e, f, g) -> f2(a, b, c, d, e, f, g) [ 0 >= a ] (?, 1) f0(a, b, c, d, e, f, g) -> f0(a - 1, c, c - 1, a, e, f, g) [ a >= 1 ] (?, 1) f1(a, b, c, d, e, f, g) -> f0(a - 1, b, c - 1, d, c, a, g) [ a >= 1 /\ c >= 1 ] (?, 1) f2(a, b, c, d, e, f, g) -> f4(a, b, c, d, e, f, h) [ 0 >= c ] (?, 1) f2(a, b, c, d, e, f, g) -> f0(h, b, c, d, e, f, g) [ h >= 1 /\ c >= 1 ] (1, 1) f3(a, b, c, d, e, f, g) -> f2(h, b, i, d, e, f, g) start location: f3 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, c]. We thus obtain the following problem: 2: T: (1, 1) f3(a, c) -> f2(h, i) (?, 1) f2(a, c) -> f0(h, c) [ h >= 1 /\ c >= 1 ] (?, 1) f2(a, c) -> f4(a, c) [ 0 >= c ] (?, 1) f1(a, c) -> f0(a - 1, c - 1) [ a >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] (?, 1) f0(a, c) -> f2(a, c) [ 0 >= a ] start location: f3 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) f3(a, c) -> f2(h, i) (?, 1) f2(a, c) -> f0(h, c) [ h >= 1 /\ c >= 1 ] (?, 1) f1(a, c) -> f0(a - 1, c - 1) [ a >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] (?, 1) f0(a, c) -> f2(a, c) [ 0 >= a ] start location: f3 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 3: f1(a, c) -> f0(a - 1, c - 1) [ a >= 1 /\ c >= 1 ] We thus obtain the following problem: 4: T: (?, 1) f0(a, c) -> f2(a, c) [ 0 >= a ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] (?, 1) f2(a, c) -> f0(h, c) [ h >= 1 /\ c >= 1 ] (1, 1) f3(a, c) -> f2(h, i) start location: f3 leaf cost: 1 By chaining the transition f0(a, c) -> f2(a, c) [ 0 >= a ] with all transitions in problem 4, the following new transition is obtained: f0(a, c) -> f0(h, c) [ 0 >= a /\ h >= 1 /\ c >= 1 ] We thus obtain the following problem: 5: T: (?, 2) f0(a, c) -> f0(h, c) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] (?, 1) f2(a, c) -> f0(h, c) [ h >= 1 /\ c >= 1 ] (1, 1) f3(a, c) -> f2(h, i) start location: f3 leaf cost: 1 Repeatedly propagating knowledge in problem 5 produces the following problem: 6: T: (?, 2) f0(a, c) -> f0(h, c) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] (1, 1) f2(a, c) -> f0(h, c) [ h >= 1 /\ c >= 1 ] (1, 1) f3(a, c) -> f2(h, i) start location: f3 leaf cost: 1 By chaining the transition f0(a, c) -> f0(h, c) [ 0 >= a /\ h >= 1 /\ c >= 1 ] with all transitions in problem 6, the following new transition is obtained: f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] We thus obtain the following problem: 7: T: (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] (1, 1) f2(a, c) -> f0(h, c) [ h >= 1 /\ c >= 1 ] (1, 1) f3(a, c) -> f2(h, i) start location: f3 leaf cost: 1 By chaining the transition f2(a, c) -> f0(h, c) [ h >= 1 /\ c >= 1 ] with all transitions in problem 7, the following new transition is obtained: f2(a, c) -> f0(h - 1, c - 1) [ h >= 1 /\ c >= 1 ] We thus obtain the following problem: 8: T: (1, 2) f2(a, c) -> f0(h - 1, c - 1) [ h >= 1 /\ c >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] (1, 1) f3(a, c) -> f2(h, i) start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f2(h, i) with all transitions in problem 8, the following new transition is obtained: f3(a, c) -> f0(h' - 1, i - 1) [ h' >= 1 /\ i >= 1 ] We thus obtain the following problem: 9: T: (1, 3) f3(a, c) -> f0(h' - 1, i - 1) [ h' >= 1 /\ i >= 1 ] (1, 2) f2(a, c) -> f0(h - 1, c - 1) [ h >= 1 /\ c >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 Testing for reachability in the complexity graph removes the following transition from problem 9: f2(a, c) -> f0(h - 1, c - 1) [ h >= 1 /\ c >= 1 ] We thus obtain the following problem: 10: T: (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] (1, 3) f3(a, c) -> f0(h' - 1, i - 1) [ h' >= 1 /\ i >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h' - 1, i - 1) [ h' >= 1 /\ i >= 1 ] with all transitions in problem 10, the following new transitions are obtained: f3(a, c) -> f0(h - 1, i - 2) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 ] f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] We thus obtain the following problem: 11: T: (1, 6) f3(a, c) -> f0(h - 1, i - 2) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h - 1, i - 2) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 ] with all transitions in problem 11, the following new transitions are obtained: f3(a, c) -> f0(h'' - 1, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 ] f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] We thus obtain the following problem: 12: T: (1, 9) f3(a, c) -> f0(h'' - 1, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h'' - 1, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 ] with all transitions in problem 12, the following new transitions are obtained: f3(a, c) -> f0(h''' - 1, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 ] f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] We thus obtain the following problem: 13: T: (1, 12) f3(a, c) -> f0(h''' - 1, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 ] (1, 10) f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h''' - 1, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 ] with all transitions in problem 13, the following new transitions are obtained: f3(a, c) -> f0(h'''' - 1, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 ] f3(a, c) -> f0(h''' - 2, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ h''' - 1 >= 1 ] We thus obtain the following problem: 14: T: (1, 15) f3(a, c) -> f0(h'''' - 1, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 ] (1, 13) f3(a, c) -> f0(h''' - 2, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ h''' - 1 >= 1 ] (1, 10) f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h'''' - 1, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 ] with all transitions in problem 14, the following new transitions are obtained: f3(a, c) -> f0(h''''' - 1, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 ] f3(a, c) -> f0(h'''' - 2, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ h'''' - 1 >= 1 ] We thus obtain the following problem: 15: T: (1, 18) f3(a, c) -> f0(h''''' - 1, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 ] (1, 16) f3(a, c) -> f0(h'''' - 2, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ h'''' - 1 >= 1 ] (1, 13) f3(a, c) -> f0(h''' - 2, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ h''' - 1 >= 1 ] (1, 10) f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h''''' - 1, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 ] with all transitions in problem 15, the following new transitions are obtained: f3(a, c) -> f0(h'''''' - 1, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 ] f3(a, c) -> f0(h''''' - 2, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ h''''' - 1 >= 1 ] We thus obtain the following problem: 16: T: (1, 21) f3(a, c) -> f0(h'''''' - 1, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 ] (1, 19) f3(a, c) -> f0(h''''' - 2, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ h''''' - 1 >= 1 ] (1, 16) f3(a, c) -> f0(h'''' - 2, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ h'''' - 1 >= 1 ] (1, 13) f3(a, c) -> f0(h''' - 2, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ h''' - 1 >= 1 ] (1, 10) f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h'''''' - 1, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 ] with all transitions in problem 16, the following new transitions are obtained: f3(a, c) -> f0(h''''''' - 1, i - 8) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 ] f3(a, c) -> f0(h'''''' - 2, i - 8) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ h'''''' - 1 >= 1 ] We thus obtain the following problem: 17: T: (1, 24) f3(a, c) -> f0(h''''''' - 1, i - 8) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 ] (1, 22) f3(a, c) -> f0(h'''''' - 2, i - 8) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ h'''''' - 1 >= 1 ] (1, 19) f3(a, c) -> f0(h''''' - 2, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ h''''' - 1 >= 1 ] (1, 16) f3(a, c) -> f0(h'''' - 2, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ h'''' - 1 >= 1 ] (1, 13) f3(a, c) -> f0(h''' - 2, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ h''' - 1 >= 1 ] (1, 10) f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h''''''' - 1, i - 8) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 ] with all transitions in problem 17, the following new transitions are obtained: f3(a, c) -> f0(h'''''''' - 1, i - 9) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 ] f3(a, c) -> f0(h''''''' - 2, i - 9) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ h''''''' - 1 >= 1 ] We thus obtain the following problem: 18: T: (1, 27) f3(a, c) -> f0(h'''''''' - 1, i - 9) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 ] (1, 25) f3(a, c) -> f0(h''''''' - 2, i - 9) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ h''''''' - 1 >= 1 ] (1, 22) f3(a, c) -> f0(h'''''' - 2, i - 8) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ h'''''' - 1 >= 1 ] (1, 19) f3(a, c) -> f0(h''''' - 2, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ h''''' - 1 >= 1 ] (1, 16) f3(a, c) -> f0(h'''' - 2, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ h'''' - 1 >= 1 ] (1, 13) f3(a, c) -> f0(h''' - 2, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ h''' - 1 >= 1 ] (1, 10) f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h'''''''' - 1, i - 9) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 ] with all transitions in problem 18, the following new transitions are obtained: f3(a, c) -> f0(h''''''''' - 1, i - 10) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 ] f3(a, c) -> f0(h'''''''' - 2, i - 10) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ h'''''''' - 1 >= 1 ] We thus obtain the following problem: 19: T: (1, 30) f3(a, c) -> f0(h''''''''' - 1, i - 10) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 ] (1, 28) f3(a, c) -> f0(h'''''''' - 2, i - 10) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ h'''''''' - 1 >= 1 ] (1, 25) f3(a, c) -> f0(h''''''' - 2, i - 9) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ h''''''' - 1 >= 1 ] (1, 22) f3(a, c) -> f0(h'''''' - 2, i - 8) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ h'''''' - 1 >= 1 ] (1, 19) f3(a, c) -> f0(h''''' - 2, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ h''''' - 1 >= 1 ] (1, 16) f3(a, c) -> f0(h'''' - 2, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ h'''' - 1 >= 1 ] (1, 13) f3(a, c) -> f0(h''' - 2, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ h''' - 1 >= 1 ] (1, 10) f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h''''''''' - 1, i - 10) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 ] with all transitions in problem 19, the following new transitions are obtained: f3(a, c) -> f0(h'''''''''' - 1, i - 11) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ 0 >= h''''''''' - 1 /\ h'''''''''' >= 1 /\ i - 10 >= 1 ] f3(a, c) -> f0(h''''''''' - 2, i - 11) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ h''''''''' - 1 >= 1 ] We thus obtain the following problem: 20: T: (1, 33) f3(a, c) -> f0(h'''''''''' - 1, i - 11) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ 0 >= h''''''''' - 1 /\ h'''''''''' >= 1 /\ i - 10 >= 1 ] (1, 31) f3(a, c) -> f0(h''''''''' - 2, i - 11) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ h''''''''' - 1 >= 1 ] (1, 28) f3(a, c) -> f0(h'''''''' - 2, i - 10) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ h'''''''' - 1 >= 1 ] (1, 25) f3(a, c) -> f0(h''''''' - 2, i - 9) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ h''''''' - 1 >= 1 ] (1, 22) f3(a, c) -> f0(h'''''' - 2, i - 8) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ h'''''' - 1 >= 1 ] (1, 19) f3(a, c) -> f0(h''''' - 2, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ h''''' - 1 >= 1 ] (1, 16) f3(a, c) -> f0(h'''' - 2, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ h'''' - 1 >= 1 ] (1, 13) f3(a, c) -> f0(h''' - 2, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ h''' - 1 >= 1 ] (1, 10) f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 By chaining the transition f3(a, c) -> f0(h'''''''''' - 1, i - 11) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ 0 >= h''''''''' - 1 /\ h'''''''''' >= 1 /\ i - 10 >= 1 ] with all transitions in problem 20, the following new transitions are obtained: f3(a, c) -> f0(h''''''''''' - 1, i - 12) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ 0 >= h''''''''' - 1 /\ h'''''''''' >= 1 /\ i - 10 >= 1 /\ 0 >= h'''''''''' - 1 /\ h''''''''''' >= 1 /\ i - 11 >= 1 ] f3(a, c) -> f0(h'''''''''' - 2, i - 12) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ 0 >= h''''''''' - 1 /\ h'''''''''' >= 1 /\ i - 10 >= 1 /\ h'''''''''' - 1 >= 1 ] We thus obtain the following problem: 21: T: (1, 36) f3(a, c) -> f0(h''''''''''' - 1, i - 12) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ 0 >= h''''''''' - 1 /\ h'''''''''' >= 1 /\ i - 10 >= 1 /\ 0 >= h'''''''''' - 1 /\ h''''''''''' >= 1 /\ i - 11 >= 1 ] (1, 34) f3(a, c) -> f0(h'''''''''' - 2, i - 12) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ 0 >= h''''''''' - 1 /\ h'''''''''' >= 1 /\ i - 10 >= 1 /\ h'''''''''' - 1 >= 1 ] (1, 31) f3(a, c) -> f0(h''''''''' - 2, i - 11) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ 0 >= h'''''''' - 1 /\ h''''''''' >= 1 /\ i - 9 >= 1 /\ h''''''''' - 1 >= 1 ] (1, 28) f3(a, c) -> f0(h'''''''' - 2, i - 10) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ 0 >= h''''''' - 1 /\ h'''''''' >= 1 /\ i - 8 >= 1 /\ h'''''''' - 1 >= 1 ] (1, 25) f3(a, c) -> f0(h''''''' - 2, i - 9) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ 0 >= h'''''' - 1 /\ h''''''' >= 1 /\ i - 7 >= 1 /\ h''''''' - 1 >= 1 ] (1, 22) f3(a, c) -> f0(h'''''' - 2, i - 8) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ 0 >= h''''' - 1 /\ h'''''' >= 1 /\ i - 6 >= 1 /\ h'''''' - 1 >= 1 ] (1, 19) f3(a, c) -> f0(h''''' - 2, i - 7) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ 0 >= h'''' - 1 /\ h''''' >= 1 /\ i - 5 >= 1 /\ h''''' - 1 >= 1 ] (1, 16) f3(a, c) -> f0(h'''' - 2, i - 6) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ 0 >= h''' - 1 /\ h'''' >= 1 /\ i - 4 >= 1 /\ h'''' - 1 >= 1 ] (1, 13) f3(a, c) -> f0(h''' - 2, i - 5) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ 0 >= h'' - 1 /\ h''' >= 1 /\ i - 3 >= 1 /\ h''' - 1 >= 1 ] (1, 10) f3(a, c) -> f0(h'' - 2, i - 4) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ 0 >= h - 1 /\ h'' >= 1 /\ i - 2 >= 1 /\ h'' - 1 >= 1 ] (1, 7) f3(a, c) -> f0(h - 2, i - 3) [ h' >= 1 /\ i >= 1 /\ 0 >= h' - 1 /\ h >= 1 /\ i - 1 >= 1 /\ h - 1 >= 1 ] (1, 4) f3(a, c) -> f0(h' - 2, i - 2) [ h' >= 1 /\ i >= 1 /\ h' - 1 >= 1 ] (?, 3) f0(a, c) -> f0(h - 1, c - 1) [ 0 >= a /\ h >= 1 /\ c >= 1 ] (?, 1) f0(a, c) -> f0(a - 1, c - 1) [ a >= 1 ] start location: f3 leaf cost: 1 Complexity upper bound ? Time: 1.362 sec (SMT: 1.224 sec)