MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b) -> f1(c, 1) (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c, 1) with all transitions in problem 1, the following new transitions are obtained: f0(a, b) -> f1(c + 11, 2) [ 1 >= 1 /\ 100 >= c ] f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] We thus obtain the following problem: 2: T: (1, 2) f0(a, b) -> f1(c + 11, 2) [ 1 >= 1 /\ 100 >= c ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 11, 2) [ 1 >= 1 /\ 100 >= c ] with all transitions in problem 2, the following new transitions are obtained: f0(a, b) -> f1(c + 22, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 ] f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] We thus obtain the following problem: 3: T: (1, 3) f0(a, b) -> f1(c + 22, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 22, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 ] with all transitions in problem 3, the following new transitions are obtained: f0(a, b) -> f1(c + 33, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 ] f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] We thus obtain the following problem: 4: T: (1, 4) f0(a, b) -> f1(c + 33, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 33, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 ] with all transitions in problem 4, the following new transitions are obtained: f0(a, b) -> f1(c + 44, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 ] f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] We thus obtain the following problem: 5: T: (1, 5) f0(a, b) -> f1(c + 44, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 44, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 ] with all transitions in problem 5, the following new transitions are obtained: f0(a, b) -> f1(c + 55, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 ] f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] We thus obtain the following problem: 6: T: (1, 6) f0(a, b) -> f1(c + 55, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 55, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 ] with all transitions in problem 6, the following new transitions are obtained: f0(a, b) -> f1(c + 66, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 ] f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] We thus obtain the following problem: 7: T: (1, 7) f0(a, b) -> f1(c + 66, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 66, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 ] with all transitions in problem 7, the following new transitions are obtained: f0(a, b) -> f1(c + 77, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 ] f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] We thus obtain the following problem: 8: T: (1, 8) f0(a, b) -> f1(c + 77, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 ] (1, 8) f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 77, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 ] with all transitions in problem 8, the following new transitions are obtained: f0(a, b) -> f1(c + 88, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 ] f0(a, b) -> f1(c + 67, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ c + 77 >= 101 ] We thus obtain the following problem: 9: T: (1, 9) f0(a, b) -> f1(c + 88, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 ] (1, 9) f0(a, b) -> f1(c + 67, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ c + 77 >= 101 ] (1, 8) f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 88, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 ] with all transitions in problem 9, the following new transitions are obtained: f0(a, b) -> f1(c + 99, 10) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 ] f0(a, b) -> f1(c + 78, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ c + 88 >= 101 ] We thus obtain the following problem: 10: T: (1, 10) f0(a, b) -> f1(c + 99, 10) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 ] (1, 10) f0(a, b) -> f1(c + 78, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ c + 88 >= 101 ] (1, 9) f0(a, b) -> f1(c + 67, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ c + 77 >= 101 ] (1, 8) f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 99, 10) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 ] with all transitions in problem 10, the following new transitions are obtained: f0(a, b) -> f1(c + 110, 11) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 ] f0(a, b) -> f1(c + 89, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ c + 99 >= 101 ] We thus obtain the following problem: 11: T: (1, 11) f0(a, b) -> f1(c + 110, 11) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 ] (1, 11) f0(a, b) -> f1(c + 89, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ c + 99 >= 101 ] (1, 10) f0(a, b) -> f1(c + 78, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ c + 88 >= 101 ] (1, 9) f0(a, b) -> f1(c + 67, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ c + 77 >= 101 ] (1, 8) f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 110, 11) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 ] with all transitions in problem 11, the following new transitions are obtained: f0(a, b) -> f1(c + 121, 12) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 ] f0(a, b) -> f1(c + 100, 10) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ c + 110 >= 101 ] We thus obtain the following problem: 12: T: (1, 12) f0(a, b) -> f1(c + 121, 12) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 ] (1, 12) f0(a, b) -> f1(c + 100, 10) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ c + 110 >= 101 ] (1, 11) f0(a, b) -> f1(c + 89, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ c + 99 >= 101 ] (1, 10) f0(a, b) -> f1(c + 78, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ c + 88 >= 101 ] (1, 9) f0(a, b) -> f1(c + 67, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ c + 77 >= 101 ] (1, 8) f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 121, 12) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 ] with all transitions in problem 12, the following new transitions are obtained: f0(a, b) -> f1(c + 132, 13) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 ] f0(a, b) -> f1(c + 111, 11) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ c + 121 >= 101 ] We thus obtain the following problem: 13: T: (1, 13) f0(a, b) -> f1(c + 132, 13) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 ] (1, 13) f0(a, b) -> f1(c + 111, 11) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ c + 121 >= 101 ] (1, 12) f0(a, b) -> f1(c + 100, 10) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ c + 110 >= 101 ] (1, 11) f0(a, b) -> f1(c + 89, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ c + 99 >= 101 ] (1, 10) f0(a, b) -> f1(c + 78, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ c + 88 >= 101 ] (1, 9) f0(a, b) -> f1(c + 67, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ c + 77 >= 101 ] (1, 8) f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 132, 13) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 ] with all transitions in problem 13, the following new transitions are obtained: f0(a, b) -> f1(c + 143, 14) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 ] f0(a, b) -> f1(c + 122, 12) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ c + 132 >= 101 ] We thus obtain the following problem: 14: T: (1, 14) f0(a, b) -> f1(c + 143, 14) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 ] (1, 14) f0(a, b) -> f1(c + 122, 12) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ c + 132 >= 101 ] (1, 13) f0(a, b) -> f1(c + 111, 11) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ c + 121 >= 101 ] (1, 12) f0(a, b) -> f1(c + 100, 10) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ c + 110 >= 101 ] (1, 11) f0(a, b) -> f1(c + 89, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ c + 99 >= 101 ] (1, 10) f0(a, b) -> f1(c + 78, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ c + 88 >= 101 ] (1, 9) f0(a, b) -> f1(c + 67, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ c + 77 >= 101 ] (1, 8) f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 143, 14) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 ] with all transitions in problem 14, the following new transitions are obtained: f0(a, b) -> f1(c + 154, 15) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ 100 >= c + 143 ] f0(a, b) -> f1(c + 133, 13) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ c + 143 >= 101 ] We thus obtain the following problem: 15: T: (1, 15) f0(a, b) -> f1(c + 154, 15) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ 100 >= c + 143 ] (1, 15) f0(a, b) -> f1(c + 133, 13) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ c + 143 >= 101 ] (1, 14) f0(a, b) -> f1(c + 122, 12) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ c + 132 >= 101 ] (1, 13) f0(a, b) -> f1(c + 111, 11) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ c + 121 >= 101 ] (1, 12) f0(a, b) -> f1(c + 100, 10) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ c + 110 >= 101 ] (1, 11) f0(a, b) -> f1(c + 89, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ c + 99 >= 101 ] (1, 10) f0(a, b) -> f1(c + 78, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ c + 88 >= 101 ] (1, 9) f0(a, b) -> f1(c + 67, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ c + 77 >= 101 ] (1, 8) f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 By chaining the transition f0(a, b) -> f1(c + 154, 15) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ 100 >= c + 143 ] with all transitions in problem 15, the following new transitions are obtained: f0(a, b) -> f1(c + 165, 16) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ 100 >= c + 143 /\ 15 >= 1 /\ 100 >= c + 154 ] f0(a, b) -> f1(c + 144, 14) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ 100 >= c + 143 /\ 15 >= 1 /\ c + 154 >= 101 ] We thus obtain the following problem: 16: T: (1, 16) f0(a, b) -> f1(c + 165, 16) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ 100 >= c + 143 /\ 15 >= 1 /\ 100 >= c + 154 ] (1, 16) f0(a, b) -> f1(c + 144, 14) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ 100 >= c + 143 /\ 15 >= 1 /\ c + 154 >= 101 ] (1, 15) f0(a, b) -> f1(c + 133, 13) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ 100 >= c + 132 /\ 14 >= 1 /\ c + 143 >= 101 ] (1, 14) f0(a, b) -> f1(c + 122, 12) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ 100 >= c + 121 /\ 13 >= 1 /\ c + 132 >= 101 ] (1, 13) f0(a, b) -> f1(c + 111, 11) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ 100 >= c + 110 /\ 12 >= 1 /\ c + 121 >= 101 ] (1, 12) f0(a, b) -> f1(c + 100, 10) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ 100 >= c + 99 /\ 11 >= 1 /\ c + 110 >= 101 ] (1, 11) f0(a, b) -> f1(c + 89, 9) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ 100 >= c + 88 /\ 10 >= 1 /\ c + 99 >= 101 ] (1, 10) f0(a, b) -> f1(c + 78, 8) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ 100 >= c + 77 /\ 9 >= 1 /\ c + 88 >= 101 ] (1, 9) f0(a, b) -> f1(c + 67, 7) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ 100 >= c + 66 /\ 8 >= 1 /\ c + 77 >= 101 ] (1, 8) f0(a, b) -> f1(c + 56, 6) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ 100 >= c + 55 /\ 7 >= 1 /\ c + 66 >= 101 ] (1, 7) f0(a, b) -> f1(c + 45, 5) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ 100 >= c + 44 /\ 6 >= 1 /\ c + 55 >= 101 ] (1, 6) f0(a, b) -> f1(c + 34, 4) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ 100 >= c + 33 /\ 5 >= 1 /\ c + 44 >= 101 ] (1, 5) f0(a, b) -> f1(c + 23, 3) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ 100 >= c + 22 /\ 4 >= 1 /\ c + 33 >= 101 ] (1, 4) f0(a, b) -> f1(c + 12, 2) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ 100 >= c + 11 /\ 3 >= 1 /\ c + 22 >= 101 ] (1, 3) f0(a, b) -> f1(c + 1, 1) [ 1 >= 1 /\ 100 >= c /\ 2 >= 1 /\ c + 11 >= 101 ] (1, 2) f0(a, b) -> f1(c - 10, 0) [ 1 >= 1 /\ c >= 101 ] (?, 1) f1(a, b) -> f1(a - 10, b - 1) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b) -> f1(a + 11, b + 1) [ b >= 1 /\ 100 >= a ] start location: f0 leaf cost: 0 Complexity upper bound ? Time: 1.854 sec (SMT: 1.698 sec)