MAYBE Initial complexity problem: 1: T: (?, 1) f1(a, b, c) -> f3(a, d, c) [ a >= 500 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ 499 >= a ] (1, 1) f2(a, b, c) -> f3(e, d, e) [ e >= 500 ] (1, 1) f2(a, b, c) -> f1(d + 1, b, d) [ 499 >= d ] start location: f2 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ 499 >= a ] (1, 1) f2(a, b, c) -> f1(d + 1, b, d) [ 499 >= d ] start location: f2 leaf cost: 2 Applied AI with 'oct' on problem 2 to obtain the following invariants: For symbol f1: -X_3 + 499 >= 0 /\ X_1 - X_3 - 1 >= 0 /\ -X_1 - X_3 + 999 >= 0 /\ -X_1 + 500 >= 0 This yielded the following problem: 3: T: (1, 1) f2(a, b, c) -> f1(d + 1, b, d) [ 499 >= d ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 1, b, d) [ 499 >= d ] with all transitions in problem 3, the following new transition is obtained: f2(a, b, c) -> f1(d + 2, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 ] We thus obtain the following problem: 4: T: (1, 2) f2(a, b, c) -> f1(d + 2, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 2, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 ] with all transitions in problem 4, the following new transition is obtained: f2(a, b, c) -> f1(d + 3, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 ] We thus obtain the following problem: 5: T: (1, 3) f2(a, b, c) -> f1(d + 3, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 3, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 ] with all transitions in problem 5, the following new transition is obtained: f2(a, b, c) -> f1(d + 4, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 ] We thus obtain the following problem: 6: T: (1, 4) f2(a, b, c) -> f1(d + 4, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 4, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 ] with all transitions in problem 6, the following new transition is obtained: f2(a, b, c) -> f1(d + 5, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 ] We thus obtain the following problem: 7: T: (1, 5) f2(a, b, c) -> f1(d + 5, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 5, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 ] with all transitions in problem 7, the following new transition is obtained: f2(a, b, c) -> f1(d + 6, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 ] We thus obtain the following problem: 8: T: (1, 6) f2(a, b, c) -> f1(d + 6, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 6, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 ] with all transitions in problem 8, the following new transition is obtained: f2(a, b, c) -> f1(d + 7, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 ] We thus obtain the following problem: 9: T: (1, 7) f2(a, b, c) -> f1(d + 7, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 7, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 ] with all transitions in problem 9, the following new transition is obtained: f2(a, b, c) -> f1(d + 8, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 ] We thus obtain the following problem: 10: T: (1, 8) f2(a, b, c) -> f1(d + 8, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 8, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 ] with all transitions in problem 10, the following new transition is obtained: f2(a, b, c) -> f1(d + 9, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 ] We thus obtain the following problem: 11: T: (1, 9) f2(a, b, c) -> f1(d + 9, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 9, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 ] with all transitions in problem 11, the following new transition is obtained: f2(a, b, c) -> f1(d + 10, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 ] We thus obtain the following problem: 12: T: (1, 10) f2(a, b, c) -> f1(d + 10, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 10, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 ] with all transitions in problem 12, the following new transition is obtained: f2(a, b, c) -> f1(d + 11, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 ] We thus obtain the following problem: 13: T: (1, 11) f2(a, b, c) -> f1(d + 11, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 11, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 ] with all transitions in problem 13, the following new transition is obtained: f2(a, b, c) -> f1(d + 12, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 ] We thus obtain the following problem: 14: T: (1, 12) f2(a, b, c) -> f1(d + 12, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 12, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 ] with all transitions in problem 14, the following new transition is obtained: f2(a, b, c) -> f1(d + 13, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 ] We thus obtain the following problem: 15: T: (1, 13) f2(a, b, c) -> f1(d + 13, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 13, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 ] with all transitions in problem 15, the following new transition is obtained: f2(a, b, c) -> f1(d + 14, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 /\ 12 >= 0 /\ -2*d + 986 >= 0 /\ -d + 487 >= 0 /\ 499 >= d + 13 ] We thus obtain the following problem: 16: T: (1, 14) f2(a, b, c) -> f1(d + 14, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 /\ 12 >= 0 /\ -2*d + 986 >= 0 /\ -d + 487 >= 0 /\ 499 >= d + 13 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 14, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 /\ 12 >= 0 /\ -2*d + 986 >= 0 /\ -d + 487 >= 0 /\ 499 >= d + 13 ] with all transitions in problem 16, the following new transition is obtained: f2(a, b, c) -> f1(d + 15, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 /\ 12 >= 0 /\ -2*d + 986 >= 0 /\ -d + 487 >= 0 /\ 499 >= d + 13 /\ 13 >= 0 /\ -2*d + 985 >= 0 /\ -d + 486 >= 0 /\ 499 >= d + 14 ] We thus obtain the following problem: 17: T: (1, 15) f2(a, b, c) -> f1(d + 15, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 /\ 12 >= 0 /\ -2*d + 986 >= 0 /\ -d + 487 >= 0 /\ 499 >= d + 13 /\ 13 >= 0 /\ -2*d + 985 >= 0 /\ -d + 486 >= 0 /\ 499 >= d + 14 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 By chaining the transition f2(a, b, c) -> f1(d + 15, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 /\ 12 >= 0 /\ -2*d + 986 >= 0 /\ -d + 487 >= 0 /\ 499 >= d + 13 /\ 13 >= 0 /\ -2*d + 985 >= 0 /\ -d + 486 >= 0 /\ 499 >= d + 14 ] with all transitions in problem 17, the following new transition is obtained: f2(a, b, c) -> f1(d + 16, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 /\ 12 >= 0 /\ -2*d + 986 >= 0 /\ -d + 487 >= 0 /\ 499 >= d + 13 /\ 13 >= 0 /\ -2*d + 985 >= 0 /\ -d + 486 >= 0 /\ 499 >= d + 14 /\ 14 >= 0 /\ -2*d + 984 >= 0 /\ -d + 485 >= 0 /\ 499 >= d + 15 ] We thus obtain the following problem: 18: T: (1, 16) f2(a, b, c) -> f1(d + 16, b, d) [ 499 >= d /\ -d + 499 >= 0 /\ 0 >= 0 /\ -2*d + 998 >= 0 /\ 499 >= d + 1 /\ 1 >= 0 /\ -2*d + 997 >= 0 /\ -d + 498 >= 0 /\ 499 >= d + 2 /\ 2 >= 0 /\ -2*d + 996 >= 0 /\ -d + 497 >= 0 /\ 499 >= d + 3 /\ 3 >= 0 /\ -2*d + 995 >= 0 /\ -d + 496 >= 0 /\ 499 >= d + 4 /\ 4 >= 0 /\ -2*d + 994 >= 0 /\ -d + 495 >= 0 /\ 499 >= d + 5 /\ 5 >= 0 /\ -2*d + 993 >= 0 /\ -d + 494 >= 0 /\ 499 >= d + 6 /\ 6 >= 0 /\ -2*d + 992 >= 0 /\ -d + 493 >= 0 /\ 499 >= d + 7 /\ 7 >= 0 /\ -2*d + 991 >= 0 /\ -d + 492 >= 0 /\ 499 >= d + 8 /\ 8 >= 0 /\ -2*d + 990 >= 0 /\ -d + 491 >= 0 /\ 499 >= d + 9 /\ 9 >= 0 /\ -2*d + 989 >= 0 /\ -d + 490 >= 0 /\ 499 >= d + 10 /\ 10 >= 0 /\ -2*d + 988 >= 0 /\ -d + 489 >= 0 /\ 499 >= d + 11 /\ 11 >= 0 /\ -2*d + 987 >= 0 /\ -d + 488 >= 0 /\ 499 >= d + 12 /\ 12 >= 0 /\ -2*d + 986 >= 0 /\ -d + 487 >= 0 /\ 499 >= d + 13 /\ 13 >= 0 /\ -2*d + 985 >= 0 /\ -d + 486 >= 0 /\ 499 >= d + 14 /\ 14 >= 0 /\ -2*d + 984 >= 0 /\ -d + 485 >= 0 /\ 499 >= d + 15 ] (?, 1) f1(a, b, c) -> f1(a + 1, b, c) [ -c + 499 >= 0 /\ a - c - 1 >= 0 /\ -a - c + 999 >= 0 /\ -a + 500 >= 0 /\ 499 >= a ] start location: f2 leaf cost: 2 Complexity upper bound ? Time: 0.904 sec (SMT: 0.788 sec)