MAYBE Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f) -> f8(1, 1, 0, 1, 1, f) (?, 1) f8(a, b, c, d, e, f) -> f10(a, b, c, d, e, f) [ 29 >= d ] (?, 1) f10(a, b, c, d, e, f) -> f14(a, b, c, d, g, f) [ d >= e + 1 /\ e >= 6 ] (?, 1) f10(a, b, c, d, e, f) -> f14(a, b, c, d, e + 2, f) [ d >= e + 1 /\ 5 >= e ] (?, 1) f14(a, b, c, d, e, f) -> f10(a, b, c, d + 10, e, f) [ 12 >= e /\ e >= 10 ] (?, 1) f14(a, b, c, d, e, f) -> f10(a, b, c, d + 1, e, f) [ e >= 13 ] (?, 1) f14(a, b, c, d, e, f) -> f10(a, b, c, d + 1, e, f) [ 9 >= e ] (?, 1) f10(a, b, c, d, e, f) -> f8(a, b, c, d + 2, e - 10, f) [ e >= d ] (?, 1) f8(a, b, c, d, e, f) -> f28(a, b, 1, d, e, 1) [ d >= 30 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [d, e]. We thus obtain the following problem: 2: T: (?, 1) f8(d, e) -> f28(d, e) [ d >= 30 ] (?, 1) f10(d, e) -> f8(d + 2, e - 10) [ e >= d ] (?, 1) f14(d, e) -> f10(d + 1, e) [ 9 >= e ] (?, 1) f14(d, e) -> f10(d + 1, e) [ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 10, e) [ 12 >= e /\ e >= 10 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d >= e + 1 /\ 5 >= e ] (?, 1) f10(d, e) -> f14(d, g) [ d >= e + 1 /\ e >= 6 ] (?, 1) f8(d, e) -> f10(d, e) [ 29 >= d ] (1, 1) f0(d, e) -> f8(1, 1) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f10(d, e) -> f8(d + 2, e - 10) [ e >= d ] (?, 1) f14(d, e) -> f10(d + 1, e) [ 9 >= e ] (?, 1) f14(d, e) -> f10(d + 1, e) [ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 10, e) [ 12 >= e /\ e >= 10 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d >= e + 1 /\ 5 >= e ] (?, 1) f10(d, e) -> f14(d, g) [ d >= e + 1 /\ e >= 6 ] (?, 1) f8(d, e) -> f10(d, e) [ 29 >= d ] (1, 1) f0(d, e) -> f8(1, 1) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f10) = -2*V_1 + 56 Pol(f8) = -2*V_1 + 59 Pol(f14) = -2*V_1 + 55 Pol(f0) = 57 orients all transitions weakly and the transition f8(d, e) -> f10(d, e) [ 29 >= d ] strictly and produces the following problem: 4: T: (?, 1) f10(d, e) -> f8(d + 2, e - 10) [ e >= d ] (?, 1) f14(d, e) -> f10(d + 1, e) [ 9 >= e ] (?, 1) f14(d, e) -> f10(d + 1, e) [ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 10, e) [ 12 >= e /\ e >= 10 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d >= e + 1 /\ 5 >= e ] (?, 1) f10(d, e) -> f14(d, g) [ d >= e + 1 /\ e >= 6 ] (57, 1) f8(d, e) -> f10(d, e) [ 29 >= d ] (1, 1) f0(d, e) -> f8(1, 1) start location: f0 leaf cost: 1 A polynomial rank function with Pol(f14) = 9 Pol(f10) = 9 Pol(f8) = 8 and size complexities S("f0(d, e) -> f8(1, 1)", 0-0) = 1 S("f0(d, e) -> f8(1, 1)", 0-1) = 1 S("f8(d, e) -> f10(d, e) [ 29 >= d ]", 0-0) = ? S("f8(d, e) -> f10(d, e) [ 29 >= d ]", 0-1) = ? S("f10(d, e) -> f14(d, g) [ d >= e + 1 /\\ e >= 6 ]", 0-0) = ? S("f10(d, e) -> f14(d, g) [ d >= e + 1 /\\ e >= 6 ]", 0-1) = ? S("f10(d, e) -> f14(d, e + 2) [ d >= e + 1 /\\ 5 >= e ]", 0-0) = ? S("f10(d, e) -> f14(d, e + 2) [ d >= e + 1 /\\ 5 >= e ]", 0-1) = ? S("f14(d, e) -> f10(d + 10, e) [ 12 >= e /\\ e >= 10 ]", 0-0) = ? S("f14(d, e) -> f10(d + 10, e) [ 12 >= e /\\ e >= 10 ]", 0-1) = 12 S("f14(d, e) -> f10(d + 1, e) [ e >= 13 ]", 0-0) = ? S("f14(d, e) -> f10(d + 1, e) [ e >= 13 ]", 0-1) = ? S("f14(d, e) -> f10(d + 1, e) [ 9 >= e ]", 0-0) = ? S("f14(d, e) -> f10(d + 1, e) [ 9 >= e ]", 0-1) = ? S("f10(d, e) -> f8(d + 2, e - 10) [ e >= d ]", 0-0) = ? S("f10(d, e) -> f8(d + 2, e - 10) [ e >= d ]", 0-1) = ? orients the transitions f14(d, e) -> f10(d + 10, e) [ 12 >= e /\ e >= 10 ] f14(d, e) -> f10(d + 1, e) [ 9 >= e ] f14(d, e) -> f10(d + 1, e) [ e >= 13 ] f10(d, e) -> f8(d + 2, e - 10) [ e >= d ] f10(d, e) -> f14(d, e + 2) [ d >= e + 1 /\ 5 >= e ] f10(d, e) -> f14(d, g) [ d >= e + 1 /\ e >= 6 ] weakly and the transition f10(d, e) -> f8(d + 2, e - 10) [ e >= d ] strictly and produces the following problem: 5: T: (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ e >= d ] (?, 1) f14(d, e) -> f10(d + 1, e) [ 9 >= e ] (?, 1) f14(d, e) -> f10(d + 1, e) [ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 10, e) [ 12 >= e /\ e >= 10 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d >= e + 1 /\ 5 >= e ] (?, 1) f10(d, e) -> f14(d, g) [ d >= e + 1 /\ e >= 6 ] (57, 1) f8(d, e) -> f10(d, e) [ 29 >= d ] (1, 1) f0(d, e) -> f8(1, 1) start location: f0 leaf cost: 1 Applied AI with 'oct' on problem 5 to obtain the following invariants: For symbol f10: X_1 - 1 >= 0 For symbol f14: X_1 - 1 >= 0 For symbol f8: X_1 - 1 >= 0 This yielded the following problem: 6: T: (1, 1) f0(d, e) -> f8(1, 1) (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f8(1, 1) with all transitions in problem 6, the following new transition is obtained: f0(d, e) -> f10(1, 1) [ 0 >= 0 /\ 29 >= 1 ] We thus obtain the following problem: 7: T: (1, 2) f0(d, e) -> f10(1, 1) [ 0 >= 0 /\ 29 >= 1 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f10(1, 1) [ 0 >= 0 /\ 29 >= 1 ] with all transitions in problem 7, the following new transition is obtained: f0(d, e) -> f8(3, -9) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 ] We thus obtain the following problem: 8: T: (1, 3) f0(d, e) -> f8(3, -9) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f8(3, -9) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 ] with all transitions in problem 8, the following new transition is obtained: f0(d, e) -> f10(3, -9) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 ] We thus obtain the following problem: 9: T: (1, 4) f0(d, e) -> f10(3, -9) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f10(3, -9) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 ] with all transitions in problem 9, the following new transition is obtained: f0(d, e) -> f14(3, -7) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 ] We thus obtain the following problem: 10: T: (1, 5) f0(d, e) -> f14(3, -7) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f14(3, -7) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 ] with all transitions in problem 10, the following new transition is obtained: f0(d, e) -> f10(4, -7) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 ] We thus obtain the following problem: 11: T: (1, 6) f0(d, e) -> f10(4, -7) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f10(4, -7) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 ] with all transitions in problem 11, the following new transition is obtained: f0(d, e) -> f14(4, -5) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 ] We thus obtain the following problem: 12: T: (1, 7) f0(d, e) -> f14(4, -5) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f14(4, -5) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 ] with all transitions in problem 12, the following new transition is obtained: f0(d, e) -> f10(5, -5) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 ] We thus obtain the following problem: 13: T: (1, 8) f0(d, e) -> f10(5, -5) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f10(5, -5) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 ] with all transitions in problem 13, the following new transition is obtained: f0(d, e) -> f14(5, -3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 ] We thus obtain the following problem: 14: T: (1, 9) f0(d, e) -> f14(5, -3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f14(5, -3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 ] with all transitions in problem 14, the following new transition is obtained: f0(d, e) -> f10(6, -3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 ] We thus obtain the following problem: 15: T: (1, 10) f0(d, e) -> f10(6, -3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f10(6, -3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 ] with all transitions in problem 15, the following new transition is obtained: f0(d, e) -> f14(6, -1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 ] We thus obtain the following problem: 16: T: (1, 11) f0(d, e) -> f14(6, -1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f14(6, -1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 ] with all transitions in problem 16, the following new transition is obtained: f0(d, e) -> f10(7, -1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 ] We thus obtain the following problem: 17: T: (1, 12) f0(d, e) -> f10(7, -1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f10(7, -1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 ] with all transitions in problem 17, the following new transition is obtained: f0(d, e) -> f14(7, 1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 ] We thus obtain the following problem: 18: T: (1, 13) f0(d, e) -> f14(7, 1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f14(7, 1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 ] with all transitions in problem 18, the following new transition is obtained: f0(d, e) -> f10(8, 1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 /\ 9 >= 1 ] We thus obtain the following problem: 19: T: (1, 14) f0(d, e) -> f10(8, 1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 /\ 9 >= 1 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f10(8, 1) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 /\ 9 >= 1 ] with all transitions in problem 19, the following new transition is obtained: f0(d, e) -> f14(8, 3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 /\ 9 >= 1 /\ 8 >= 2 /\ 5 >= 1 ] We thus obtain the following problem: 20: T: (1, 15) f0(d, e) -> f14(8, 3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 /\ 9 >= 1 /\ 8 >= 2 /\ 5 >= 1 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 By chaining the transition f0(d, e) -> f14(8, 3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 /\ 9 >= 1 /\ 8 >= 2 /\ 5 >= 1 ] with all transitions in problem 20, the following new transition is obtained: f0(d, e) -> f10(9, 3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 /\ 9 >= 1 /\ 8 >= 2 /\ 5 >= 1 /\ 9 >= 3 ] We thus obtain the following problem: 21: T: (1, 16) f0(d, e) -> f10(9, 3) [ 0 >= 0 /\ 29 >= 1 /\ 1 >= 1 /\ 2 >= 0 /\ 29 >= 3 /\ 3 >= -8 /\ 5 >= -9 /\ 9 >= -7 /\ 3 >= 0 /\ 4 >= -6 /\ 5 >= -7 /\ 9 >= -5 /\ 4 >= 0 /\ 5 >= -4 /\ 5 >= -5 /\ 9 >= -3 /\ 5 >= 0 /\ 6 >= -2 /\ 5 >= -3 /\ 9 >= -1 /\ 6 >= 0 /\ 7 >= 0 /\ 5 >= -1 /\ 9 >= 1 /\ 8 >= 2 /\ 5 >= 1 /\ 9 >= 3 ] (57, 1) f8(d, e) -> f10(d, e) [ d - 1 >= 0 /\ 29 >= d ] (?, 1) f10(d, e) -> f14(d, g) [ d - 1 >= 0 /\ d >= e + 1 /\ e >= 6 ] (?, 1) f10(d, e) -> f14(d, e + 2) [ d - 1 >= 0 /\ d >= e + 1 /\ 5 >= e ] (?, 1) f14(d, e) -> f10(d + 10, e) [ d - 1 >= 0 /\ 12 >= e /\ e >= 10 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ e >= 13 ] (?, 1) f14(d, e) -> f10(d + 1, e) [ d - 1 >= 0 /\ 9 >= e ] (513, 1) f10(d, e) -> f8(d + 2, e - 10) [ d - 1 >= 0 /\ e >= d ] start location: f0 leaf cost: 1 Complexity upper bound ? Time: 1.534 sec (SMT: 1.414 sec)