MAYBE Initial complexity problem: 1: T: (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) (?, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (?, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (?, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ b >= d ] (?, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4returnin(a, b, c, d) [ d >= b + 1 ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ c >= 1 ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ 0 >= c ] (?, 1) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d + a) (?, 1) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d - a) (?, 1) evalspeedFails4returnin(a, b, c, d) -> evalspeedFails4stop(a, b, c, d) start location: evalspeedFails4start leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) (?, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (?, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (?, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ b >= d ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ c >= 1 ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ 0 >= c ] (?, 1) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d + a) (?, 1) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d - a) start location: evalspeedFails4start leaf cost: 2 Repeatedly propagating knowledge in problem 2 produces the following problem: 3: T: (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (?, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ b >= d ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ c >= 1 ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ 0 >= c ] (?, 1) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d + a) (?, 1) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d - a) start location: evalspeedFails4start leaf cost: 2 Applied AI with 'oct' on problem 3 to obtain the following invariants: For symbol evalspeedFails4bb3in: X_2 - X_4 >= 0 /\ -X_1 + 1 >= 0 /\ X_1 + 1 >= 0 For symbol evalspeedFails4bb4in: X_2 - X_4 >= 0 /\ X_3 - 1 >= 0 /\ X_1 + X_3 >= 0 /\ -X_1 + X_3 >= 0 /\ -X_1 + 1 >= 0 /\ X_1 + 1 >= 0 For symbol evalspeedFails4bb5in: X_2 - X_4 >= 0 /\ -X_3 >= 0 /\ X_1 - X_3 + 1 >= 0 /\ -X_1 - X_3 + 1 >= 0 /\ -X_1 + 1 >= 0 /\ X_1 + 1 >= 0 For symbol evalspeedFails4bb6in: -X_1 + 1 >= 0 /\ X_1 + 1 >= 0 This yielded the following problem: 4: T: (?, 1) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 ] (?, 1) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (?, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 ] with all transitions in problem 4, the following new transition is obtained: evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a ] We thus obtain the following problem: 5: T: (?, 2) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a ] (?, 1) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (?, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a ] with all transitions in problem 5, the following new transition is obtained: evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] We thus obtain the following problem: 6: T: (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (?, 1) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (?, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 A polynomial rank function with Pol(evalspeedFails4bb5in) = -5 Pol(evalspeedFails4bb4in) = 1 Pol(evalspeedFails4bb6in) = 1 Pol(evalspeedFails4bb3in) = 1 Pol(evalspeedFails4entryin) = 1 Pol(evalspeedFails4start) = 1 orients all transitions weakly and the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] strictly and produces the following problem: 7: T: (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (?, 1) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 ] (1, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (?, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb6in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 ] with all transitions in problem 7, the following new transition is obtained: evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a ] We thus obtain the following problem: 8: T: (?, 2) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (1, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (?, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 Repeatedly propagating knowledge in problem 8 produces the following problem: 9: T: (?, 2) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (1, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a ] with all transitions in problem 9, the following new transition is obtained: evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] We thus obtain the following problem: 10: T: (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (1, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] (?, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 Repeatedly propagating knowledge in problem 10 produces the following problem: 11: T: (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (1, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c ] with all transitions in problem 11, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 ] We thus obtain the following problem: 12: T: (1, 4) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 ] with all transitions in problem 12, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 2*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 ] We thus obtain the following problem: 13: T: (1, 7) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 2*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 2*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 ] with all transitions in problem 13, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 3*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 ] We thus obtain the following problem: 14: T: (1, 10) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 3*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 3*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 ] with all transitions in problem 14, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 4*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 ] We thus obtain the following problem: 15: T: (1, 13) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 4*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 4*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 ] with all transitions in problem 15, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 5*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 ] We thus obtain the following problem: 16: T: (1, 16) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 5*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 5*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 ] with all transitions in problem 16, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 6*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 ] We thus obtain the following problem: 17: T: (1, 19) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 6*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 6*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 ] with all transitions in problem 17, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 7*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 ] We thus obtain the following problem: 18: T: (1, 22) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 7*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 7*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 ] with all transitions in problem 18, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 8*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 ] We thus obtain the following problem: 19: T: (1, 25) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 8*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 8*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 ] with all transitions in problem 19, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 9*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 /\ b >= d - 9*a /\ b - d + 9*a >= 0 ] We thus obtain the following problem: 20: T: (1, 28) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 9*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 /\ b >= d - 9*a /\ b - d + 9*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 9*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 /\ b >= d - 9*a /\ b - d + 9*a >= 0 ] with all transitions in problem 20, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 10*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 /\ b >= d - 9*a /\ b - d + 9*a >= 0 /\ b >= d - 10*a /\ b - d + 10*a >= 0 ] We thus obtain the following problem: 21: T: (1, 31) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 10*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 /\ b >= d - 9*a /\ b - d + 9*a >= 0 /\ b >= d - 10*a /\ b - d + 10*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 By chaining the transition evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 10*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 /\ b >= d - 9*a /\ b - d + 9*a >= 0 /\ b >= d - 10*a /\ b - d + 10*a >= 0 ] with all transitions in problem 21, the following new transition is obtained: evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 11*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 /\ b >= d - 9*a /\ b - d + 9*a >= 0 /\ b >= d - 10*a /\ b - d + 10*a >= 0 /\ b >= d - 11*a /\ b - d + 11*a >= 0 ] We thus obtain the following problem: 22: T: (1, 34) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - 11*a) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ 0 >= c /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ b >= d - 2*a /\ b - d + 2*a >= 0 /\ b >= d - 3*a /\ b - d + 3*a >= 0 /\ b >= d - 4*a /\ b - d + 4*a >= 0 /\ b >= d - 5*a /\ b - d + 5*a >= 0 /\ b >= d - 6*a /\ b - d + 6*a >= 0 /\ b >= d - 7*a /\ b - d + 7*a >= 0 /\ b >= d - 8*a /\ b - d + 8*a >= 0 /\ b >= d - 9*a /\ b - d + 9*a >= 0 /\ b >= d - 10*a /\ b - d + 10*a >= 0 /\ b >= d - 11*a /\ b - d + 11*a >= 0 ] (?, 3) evalspeedFails4bb4in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d + a) [ b - d >= 0 /\ c - 1 >= 0 /\ a + c >= 0 /\ -a + c >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d + a /\ b - d - a >= 0 /\ c >= 1 ] (?, 3) evalspeedFails4bb5in(a, b, c, d) -> evalspeedFails4bb5in(a, b, c, d - a) [ b - d >= 0 /\ -c >= 0 /\ a - c + 1 >= 0 /\ -a - c + 1 >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d - a /\ b - d + a >= 0 /\ 0 >= c ] (2, 1) evalspeedFails4bb3in(a, b, c, d) -> evalspeedFails4bb4in(a, b, c, d) [ b - d >= 0 /\ -a + 1 >= 0 /\ a + 1 >= 0 /\ c >= 1 ] (2, 1) evalspeedFails4bb6in(a, b, c, d) -> evalspeedFails4bb3in(a, b, c, d) [ -a + 1 >= 0 /\ a + 1 >= 0 /\ b >= d ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(-1, c, a, b) [ 0 >= a ] (1, 1) evalspeedFails4entryin(a, b, c, d) -> evalspeedFails4bb6in(1, c, a, b) [ a >= 1 ] (1, 1) evalspeedFails4start(a, b, c, d) -> evalspeedFails4entryin(a, b, c, d) start location: evalspeedFails4start leaf cost: 2 Complexity upper bound ? Time: 3.318 sec (SMT: 3.080 sec)