MAYBE Initial complexity problem: 1: T: (1, 1) evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d) (?, 1) evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d) (?, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (?, 1) evalEx1bb6in(a, b, c, d) -> evalEx1returnin(a, b, c, d) [ a >= b ] (?, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 /\ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d) [ 0 >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d) [ 0 >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d - 1) [ 0 >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d - 1) [ 0 >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) (?, 1) evalEx1returnin(a, b, c, d) -> evalEx1stop(a, b, c, d) start location: evalEx1start leaf cost: 0 Testing for unsatisfiable constraints removes the following transitions from problem 1: evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 /\ e >= 1 ] evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d) [ 0 >= 1 ] evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d) [ 0 >= 1 ] evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d - 1) [ 0 >= 1 ] evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d - 1) [ 0 >= 1 ] We thus obtain the following problem: 2: T: (1, 1) evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d) (?, 1) evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d) (?, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (?, 1) evalEx1bb6in(a, b, c, d) -> evalEx1returnin(a, b, c, d) [ a >= b ] (?, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) (?, 1) evalEx1returnin(a, b, c, d) -> evalEx1stop(a, b, c, d) start location: evalEx1start leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d) (?, 1) evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d) (?, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (?, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) start location: evalEx1start leaf cost: 2 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (1, 1) evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d) (1, 1) evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d) (?, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (?, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) start location: evalEx1start leaf cost: 2 A polynomial rank function with Pol(evalEx1start) = 4*V_1 + 1 Pol(evalEx1entryin) = 4*V_1 + 1 Pol(evalEx1bb6in) = -4*V_1 + 4*V_2 + 1 Pol(evalEx1bbin) = -4*V_1 + 4*V_2 Pol(evalEx1bb4in) = -4*V_1 + 4*V_4 - 1 Pol(evalEx1bb1in) = -4*V_1 + 4*V_4 - 1 Pol(evalEx1bb5in) = -4*V_1 + 4*V_4 - 2 orients all transitions weakly and the transition evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] strictly and produces the following problem: 5: T: (1, 1) evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d) (1, 1) evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (?, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) start location: evalEx1start leaf cost: 2 Repeatedly propagating knowledge in problem 5 produces the following problem: 6: T: (1, 1) evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d) (1, 1) evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (4*a + 1, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) start location: evalEx1start leaf cost: 2 A polynomial rank function with Pol(evalEx1bb5in) = 1 Pol(evalEx1bb6in) = 0 Pol(evalEx1bb4in) = 2 Pol(evalEx1bb1in) = 2 and size complexities S("evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d)", 0-0) = ? S("evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d)", 0-1) = ? S("evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d)", 0-2) = ? S("evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d)", 0-3) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d)", 0-0) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d)", 0-1) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d)", 0-2) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d)", 0-3) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ]", 0-0) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ]", 0-1) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ]", 0-2) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ]", 0-3) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ]", 0-0) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ]", 0-1) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ]", 0-2) = ? S("evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ]", 0-3) = ? S("evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ]", 0-0) = ? S("evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ]", 0-1) = ? S("evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ]", 0-2) = ? S("evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ]", 0-3) = ? S("evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ]", 0-0) = ? S("evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ]", 0-1) = ? S("evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ]", 0-2) = ? S("evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ]", 0-3) = ? S("evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b)", 0-0) = ? S("evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b)", 0-1) = ? S("evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b)", 0-2) = ? S("evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b)", 0-3) = ? S("evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ]", 0-0) = ? S("evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ]", 0-1) = ? S("evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ]", 0-2) = ? S("evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ]", 0-3) = ? S("evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d)", 0-0) = 0 S("evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d)", 0-1) = a S("evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d)", 0-2) = c S("evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d)", 0-3) = d S("evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d)", 0-0) = a S("evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d)", 0-1) = b S("evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d)", 0-2) = c S("evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d)", 0-3) = d orients the transitions evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] weakly and the transitions evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] strictly and produces the following problem: 7: T: (1, 1) evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d) (1, 1) evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (4*a + 1, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (8*a + 2, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (8*a + 2, 1) evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1start(a, b, c, d) -> evalEx1entryin(a, b, c, d) with all transitions in problem 7, the following new transition is obtained: evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) We thus obtain the following problem: 8: T: (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) (1, 1) evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (4*a + 1, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (8*a + 2, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (8*a + 2, 1) evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) start location: evalEx1start leaf cost: 2 Testing for reachability in the complexity graph removes the following transition from problem 8: evalEx1entryin(a, b, c, d) -> evalEx1bb6in(0, a, c, d) We thus obtain the following problem: 9: T: (8*a + 2, 1) evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (8*a + 2, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (4*a + 1, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1bb5in(a, b, c, d) -> evalEx1bb6in(a + 1, d, c, d) with all transitions in problem 9, the following new transition is obtained: evalEx1bb5in(a, b, c, d) -> evalEx1bbin(a + 1, d, c, d) [ d >= a + 2 ] We thus obtain the following problem: 10: T: (8*a + 2, 2) evalEx1bb5in(a, b, c, d) -> evalEx1bbin(a + 1, d, c, d) [ d >= a + 2 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (8*a + 2, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (4*a + 1, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1bb5in(a, b, c, d) -> evalEx1bbin(a + 1, d, c, d) [ d >= a + 2 ] with all transitions in problem 10, the following new transition is obtained: evalEx1bb5in(a, b, c, d) -> evalEx1bb4in(a + 1, d, a + 2, d) [ d >= a + 2 ] We thus obtain the following problem: 11: T: (8*a + 2, 3) evalEx1bb5in(a, b, c, d) -> evalEx1bb4in(a + 1, d, a + 2, d) [ d >= a + 2 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (8*a + 2, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (4*a + 1, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1bb4in(a, b, c, d) -> evalEx1bb5in(a, b, c, d) [ c >= d ] with all transitions in problem 11, the following new transition is obtained: evalEx1bb4in(a, b, c, d) -> evalEx1bb4in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 ] We thus obtain the following problem: 12: T: (8*a + 2, 4) evalEx1bb4in(a, b, c, d) -> evalEx1bb4in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 ] (8*a + 2, 3) evalEx1bb5in(a, b, c, d) -> evalEx1bb4in(a + 1, d, a + 2, d) [ d >= a + 2 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (4*a + 1, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) start location: evalEx1start leaf cost: 2 Testing for reachability in the complexity graph removes the following transition from problem 12: evalEx1bb5in(a, b, c, d) -> evalEx1bb4in(a + 1, d, a + 2, d) [ d >= a + 2 ] We thus obtain the following problem: 13: T: (8*a + 2, 4) evalEx1bb4in(a, b, c, d) -> evalEx1bb4in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (4*a + 1, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1bb4in(a, b, c, d) -> evalEx1bb4in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 ] with all transitions in problem 13, the following new transition is obtained: evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] We thus obtain the following problem: 14: T: (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (4*a + 1, 1) evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1bbin(a, b, c, d) -> evalEx1bb4in(a, b, a + 1, b) with all transitions in problem 14, the following new transition is obtained: evalEx1bbin(a, b, c, d) -> evalEx1bb1in(a, b, a + 1, b) [ b >= a + 2 ] We thus obtain the following problem: 15: T: (4*a + 1, 2) evalEx1bbin(a, b, c, d) -> evalEx1bb1in(a, b, a + 1, b) [ b >= a + 2 ] (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (4*a + 1, 1) evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1bb6in(a, b, c, d) -> evalEx1bbin(a, b, c, d) [ b >= a + 1 ] with all transitions in problem 15, the following new transition is obtained: evalEx1bb6in(a, b, c, d) -> evalEx1bb1in(a, b, a + 1, b) [ b >= a + 1 /\ b >= a + 2 ] We thus obtain the following problem: 16: T: (4*a + 1, 3) evalEx1bb6in(a, b, c, d) -> evalEx1bb1in(a, b, a + 1, b) [ b >= a + 1 /\ b >= a + 2 ] (4*a + 1, 2) evalEx1bbin(a, b, c, d) -> evalEx1bb1in(a, b, a + 1, b) [ b >= a + 2 ] (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) start location: evalEx1start leaf cost: 2 Testing for reachability in the complexity graph removes the following transition from problem 16: evalEx1bbin(a, b, c, d) -> evalEx1bb1in(a, b, a + 1, b) [ b >= a + 2 ] We thus obtain the following problem: 17: T: (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (4*a + 1, 3) evalEx1bb6in(a, b, c, d) -> evalEx1bb1in(a, b, a + 1, b) [ b >= a + 1 /\ b >= a + 2 ] (1, 2) evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1start(a, b, c, d) -> evalEx1bb6in(0, a, c, d) with all transitions in problem 17, the following new transition is obtained: evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] We thus obtain the following problem: 18: T: (1, 5) evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (4*a + 1, 3) evalEx1bb6in(a, b, c, d) -> evalEx1bb1in(a, b, a + 1, b) [ b >= a + 1 /\ b >= a + 2 ] start location: evalEx1start leaf cost: 2 Testing for reachability in the complexity graph removes the following transition from problem 18: evalEx1bb6in(a, b, c, d) -> evalEx1bb1in(a, b, a + 1, b) [ b >= a + 1 /\ b >= a + 2 ] We thus obtain the following problem: 19: T: (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (1, 5) evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c + 1, d) with all transitions in problem 19, the following new transitions are obtained: evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c + 1 >= d /\ d >= a + 2 /\ d >= a + 3 ] evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c + 1, d) [ d >= c + 2 ] We thus obtain the following problem: 20: T: (?, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c + 1 >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c + 1, d) [ d >= c + 2 ] (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (1, 5) evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] start location: evalEx1start leaf cost: 2 A polynomial rank function with Pol(evalEx1bb1in) = -2*V_1 + 2*V_4 - 2 Pol(evalEx1bb4in) = -2*V_1 + 2*V_4 - 1 Pol(evalEx1start) = 2*V_1 - 2 orients all transitions weakly and the transition evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c + 1 >= d /\ d >= a + 2 /\ d >= a + 3 ] strictly and produces the following problem: 21: T: (2*a + 2, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c + 1 >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c + 1, d) [ d >= c + 2 ] (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (1, 5) evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ e >= 1 ] with all transitions in problem 21, the following new transitions are obtained: evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ e >= 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ e >= 1 /\ d - 1 >= c + 1 ] We thus obtain the following problem: 22: T: (?, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ e >= 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ e >= 1 /\ d - 1 >= c + 1 ] (2*a + 2, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c + 1 >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c + 1, d) [ d >= c + 2 ] (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (1, 5) evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] start location: evalEx1start leaf cost: 2 A polynomial rank function with Pol(evalEx1bb1in) = -2*V_1 + 2*V_4 - 3 Pol(evalEx1bb4in) = -2*V_1 + 2*V_4 - 2 Pol(evalEx1start) = 2*V_1 - 3 orients all transitions weakly and the transition evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ e >= 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] strictly and produces the following problem: 23: T: (2*a + 3, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ e >= 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ e >= 1 /\ d - 1 >= c + 1 ] (2*a + 2, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c + 1 >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c + 1, d) [ d >= c + 2 ] (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (?, 1) evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] (1, 5) evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] start location: evalEx1start leaf cost: 2 By chaining the transition evalEx1bb1in(a, b, c, d) -> evalEx1bb4in(a, b, c, d - 1) [ 0 >= e + 1 ] with all transitions in problem 23, the following new transitions are obtained: evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ 0 >= e + 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ 0 >= e + 1 /\ d - 1 >= c + 1 ] We thus obtain the following problem: 24: T: (?, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ 0 >= e + 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ 0 >= e + 1 /\ d - 1 >= c + 1 ] (2*a + 3, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ e >= 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ e >= 1 /\ d - 1 >= c + 1 ] (2*a + 2, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c + 1 >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c + 1, d) [ d >= c + 2 ] (8*a + 2, 5) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 1) evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] (1, 5) evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] start location: evalEx1start leaf cost: 2 Testing for reachability in the complexity graph removes the following transitions from problem 24: evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c >= d /\ d >= a + 2 /\ d >= a + 3 ] evalEx1bb4in(a, b, c, d) -> evalEx1bb1in(a, b, c, d) [ d >= c + 1 ] We thus obtain the following problem: 25: T: (?, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ 0 >= e + 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] (2*a + 3, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ e >= 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] (2*a + 2, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c + 1 >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ 0 >= e + 1 /\ d - 1 >= c + 1 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ e >= 1 /\ d - 1 >= c + 1 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c + 1, d) [ d >= c + 2 ] (1, 5) evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] start location: evalEx1start leaf cost: 2 A polynomial rank function with Pol(evalEx1bb1in) = -2*V_1 + 2*V_4 - 5 Pol(evalEx1start) = 2*V_1 - 5 orients all transitions weakly and the transition evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ 0 >= e + 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] strictly and produces the following problem: 26: T: (2*a + 5, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ 0 >= e + 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] (2*a + 3, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d - 1, a + 2, d - 1) [ e >= 1 /\ c >= d - 1 /\ d - 1 >= a + 2 /\ d - 1 >= a + 3 ] (2*a + 2, 6) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a + 1, d, a + 2, d) [ c + 1 >= d /\ d >= a + 2 /\ d >= a + 3 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ 0 >= e + 1 /\ d - 1 >= c + 1 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c, d - 1) [ e >= 1 /\ d - 1 >= c + 1 ] (?, 2) evalEx1bb1in(a, b, c, d) -> evalEx1bb1in(a, b, c + 1, d) [ d >= c + 2 ] (1, 5) evalEx1start(a, b, c, d) -> evalEx1bb1in(0, a, 1, a) [ a >= 1 /\ a >= 2 ] start location: evalEx1start leaf cost: 2 Complexity upper bound ? Time: 5.547 sec (SMT: 5.019 sec)