MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, 1, a, b) [ 100 >= a /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f2(a, b, c, d, e) [ d >= a /\ c >= 1 /\ b >= e ] start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, 1, a, b) [ 100 >= a /\ 0 >= c /\ b >= 1 ] start location: f0 leaf cost: 1 A polynomial rank function with Pol(f0) = 1 Pol(f1) = -V_3 + 1 orients all transitions weakly and the transitions f1(a, b, c, d, e) -> f1(a + 11, b + 1, 1, a, b) [ 100 >= a /\ 0 >= c /\ b >= 1 ] f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ a >= 101 /\ 0 >= c /\ b >= 1 ] strictly and produces the following problem: 3: T: (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ b >= 1 /\ a >= 101 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ b >= 1 /\ 100 >= a ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ a >= 101 /\ 0 >= c /\ b >= 1 ] (1, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, 1, a, b) [ 100 >= a /\ 0 >= c /\ b >= 1 ] start location: f0 leaf cost: 1 Applied AI with 'oct' on problem 3 to obtain the following invariants: For symbol f1: X_3 >= 0 This yielded the following problem: 4: T: (1, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a + 11, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 ] with all transitions in problem 4, the following new transitions are obtained: f1(a, b, c, d, e) -> f1(a + 1, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 ] f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] We thus obtain the following problem: 5: T: (1, 2) f1(a, b, c, d, e) -> f1(a + 1, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a + 1, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 ] with all transitions in problem 5, the following new transitions are obtained: f1(a, b, c, d, e) -> f1(a - 9, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 ] f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] We thus obtain the following problem: 6: T: (1, 3) f1(a, b, c, d, e) -> f1(a - 9, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a - 9, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 ] with all transitions in problem 6, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a + 2, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 ] We thus obtain the following problem: 7: T: (1, 4) f1(a, b, c, d, e) -> f1(a + 2, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a + 2, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 ] with all transitions in problem 7, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a - 8, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 ] We thus obtain the following problem: 8: T: (1, 5) f1(a, b, c, d, e) -> f1(a - 8, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a - 8, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 ] with all transitions in problem 8, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a + 3, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 ] We thus obtain the following problem: 9: T: (1, 6) f1(a, b, c, d, e) -> f1(a + 3, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a + 3, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 ] with all transitions in problem 9, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a - 7, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 ] We thus obtain the following problem: 10: T: (1, 7) f1(a, b, c, d, e) -> f1(a - 7, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a - 7, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 ] with all transitions in problem 10, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a + 4, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 ] We thus obtain the following problem: 11: T: (1, 8) f1(a, b, c, d, e) -> f1(a + 4, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a + 4, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 ] with all transitions in problem 11, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a - 6, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 ] We thus obtain the following problem: 12: T: (1, 9) f1(a, b, c, d, e) -> f1(a - 6, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a - 6, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 ] with all transitions in problem 12, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a + 5, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 ] We thus obtain the following problem: 13: T: (1, 10) f1(a, b, c, d, e) -> f1(a + 5, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a + 5, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 ] with all transitions in problem 13, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a - 5, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 ] We thus obtain the following problem: 14: T: (1, 11) f1(a, b, c, d, e) -> f1(a - 5, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a - 5, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 ] with all transitions in problem 14, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a + 6, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 ] We thus obtain the following problem: 15: T: (1, 12) f1(a, b, c, d, e) -> f1(a + 6, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a + 6, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 ] with all transitions in problem 15, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a - 4, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 ] We thus obtain the following problem: 16: T: (1, 13) f1(a, b, c, d, e) -> f1(a - 4, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a - 4, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 ] with all transitions in problem 16, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a + 7, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 /\ 100 >= a - 4 ] We thus obtain the following problem: 17: T: (1, 14) f1(a, b, c, d, e) -> f1(a + 7, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 /\ 100 >= a - 4 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a + 7, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 /\ 100 >= a - 4 ] with all transitions in problem 17, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a - 3, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 /\ 100 >= a - 4 /\ a + 7 >= 101 ] We thus obtain the following problem: 18: T: (1, 15) f1(a, b, c, d, e) -> f1(a - 3, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 /\ 100 >= a - 4 /\ a + 7 >= 101 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 By chaining the transition f1(a, b, c, d, e) -> f1(a - 3, b - 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 /\ 100 >= a - 4 /\ a + 7 >= 101 ] with all transitions in problem 18, the following new transition is obtained: f1(a, b, c, d, e) -> f1(a + 8, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 /\ 100 >= a - 4 /\ a + 7 >= 101 /\ 100 >= a - 3 ] We thus obtain the following problem: 19: T: (1, 16) f1(a, b, c, d, e) -> f1(a + 8, b, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ a + 1 >= 101 /\ b - 1 >= 1 /\ 100 >= a - 9 /\ a + 2 >= 101 /\ 100 >= a - 8 /\ a + 3 >= 101 /\ 100 >= a - 7 /\ a + 4 >= 101 /\ 100 >= a - 6 /\ a + 5 >= 101 /\ 100 >= a - 5 /\ a + 6 >= 101 /\ 100 >= a - 4 /\ a + 7 >= 101 /\ 100 >= a - 3 ] (1, 3) f1(a, b, c, d, e) -> f1(a + 12, b + 1, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ a + 11 >= 101 /\ 100 >= a + 1 ] (1, 2) f1(a, b, c, d, e) -> f1(a + 22, b + 2, 1, a, b) [ c >= 0 /\ 100 >= a /\ 0 >= c /\ b >= 1 /\ 1 >= 0 /\ b + 1 >= 1 /\ 100 >= a + 11 ] (1, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, 1, a, b) [ c >= 0 /\ a >= 101 /\ 0 >= c /\ b >= 1 ] (?, 1) f1(a, b, c, d, e) -> f1(a + 11, b + 1, c, d, e) [ c >= 0 /\ b >= 1 /\ 100 >= a ] (?, 1) f1(a, b, c, d, e) -> f1(a - 10, b - 1, c, d, e) [ c >= 0 /\ b >= 1 /\ a >= 101 ] (1, 1) f0(a, b, c, d, e) -> f1(f, 1, 0, d, e) start location: f0 leaf cost: 1 Complexity upper bound ? Time: 3.920 sec (SMT: 3.665 sec)