MAYBE Initial complexity problem: 1: T: (1, 1) f5(a, b, c, d, e) -> f300(a, b, c, d, e) (?, 1) f4(a, b, c, d, e) -> f300(a, b, c + 1, d, e) [ a >= b ] (?, 1) f4(a, b, c, d, e) -> f4(a + 1, b, c, f, e) [ f >= 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c, d, e) -> f4(a + 1, b, c, f, e) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c, d, e) -> f2(a, b, c, 0, e) [ b >= a + 1 ] (?, 1) f2(a, b, c, d, e) -> f4(a + 1, b, c, f, e) [ f >= 1 /\ b >= a + 1 ] (?, 1) f2(a, b, c, d, e) -> f4(a + 1, b, c, f, e) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f2(a, b, c, d, e) -> f2(a, b, c, 0, e) [ b >= a + 1 ] (?, 1) f300(a, b, c, d, e) -> f1(a, b, c, d, f) [ c >= a ] (?, 1) f300(a, b, c, d, e) -> f300(a, b, c + 1, d, e) [ a >= c + 1 /\ a >= b ] (?, 1) f300(a, b, c, d, e) -> f4(a + 1, b, c, f, e) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c, d, e) -> f4(a + 1, b, c, f, e) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c, d, e) -> f2(a, b, c, 0, e) [ a >= c + 1 /\ b >= a + 1 ] start location: f5 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c]. We thus obtain the following problem: 2: T: (?, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f300(a, b, c) -> f1(a, b, c) [ c >= a ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (?, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (?, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (?, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (?, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (?, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (?, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 A polynomial rank function with Pol(f4) = 1 Pol(f300) = 0 Pol(f2) = 1 and size complexities S("f5(a, b, c) -> f300(a, b, c)", 0-0) = a S("f5(a, b, c) -> f300(a, b, c)", 0-1) = b S("f5(a, b, c) -> f300(a, b, c)", 0-2) = c S("f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ]", 0-0) = ? S("f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ]", 0-1) = b S("f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ]", 0-2) = c + 1 S("f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-0) = ? S("f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-1) = b S("f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-2) = c S("f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-0) = ? S("f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-1) = b S("f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-2) = c S("f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-0) = ? S("f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-1) = b S("f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-2) = c S("f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-0) = ? S("f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-1) = b S("f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-2) = c S("f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-0) = ? S("f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-1) = b S("f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-2) = c S("f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-0) = ? S("f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-1) = b S("f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-2) = c S("f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\\ a >= b ]", 0-0) = ? S("f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\\ a >= b ]", 0-1) = b S("f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\\ a >= b ]", 0-2) = ? S("f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-0) = a + 1 S("f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-1) = b S("f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-2) = c S("f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-0) = a + 1 S("f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-1) = b S("f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-2) = c S("f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\\ b >= a + 1 ]", 0-0) = a S("f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\\ b >= a + 1 ]", 0-1) = b S("f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\\ b >= a + 1 ]", 0-2) = c orients the transitions f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ] f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] weakly and the transition f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ] strictly and produces the following problem: 5: T: (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (?, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (?, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (?, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (3, 1) f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 A polynomial rank function with Pol(f300) = -2*V_1 + 2*V_2 Pol(f2) = -2*V_1 + 2*V_2 - 1 Pol(f4) = -2*V_1 + 2*V_2 Pol(f5) = -2*V_1 + 2*V_2 orients all transitions weakly and the transitions f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] strictly and produces the following problem: 6: T: (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (?, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (3, 1) f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 A polynomial rank function with Pol(f300) = V_1 - V_3 Pol(f2) = 2*V_1 + V_3 + 1 and size complexities S("f5(a, b, c) -> f300(a, b, c)", 0-0) = a S("f5(a, b, c) -> f300(a, b, c)", 0-1) = b S("f5(a, b, c) -> f300(a, b, c)", 0-2) = c S("f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ]", 0-0) = 9*a + 9*b + 729 S("f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ]", 0-1) = b S("f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ]", 0-2) = c + 1 S("f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-0) = 9*a + 9*b + 81 S("f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-1) = b S("f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-2) = c S("f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-0) = 9*a + 9*b + 81 S("f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-1) = b S("f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-2) = c S("f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-0) = 9*a + 9*b + 81 S("f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-1) = b S("f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-2) = c S("f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-0) = 9*a + 9*b + 81 S("f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-1) = b S("f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ b >= a + 1 ]", 0-2) = c S("f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-0) = 9*a + 9*b + 81 S("f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-1) = b S("f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ b >= a + 1 ]", 0-2) = c S("f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-0) = 9*a + 9*b + 81 S("f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-1) = b S("f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ]", 0-2) = c S("f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\\ a >= b ]", 0-0) = 9*a + 9*b + 6561 S("f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\\ a >= b ]", 0-1) = b S("f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\\ a >= b ]", 0-2) = ? S("f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-0) = a + 1 S("f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-1) = b S("f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-2) = c S("f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-0) = a + 1 S("f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-1) = b S("f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\\ a >= c + 1 /\\ b >= a + 1 ]", 0-2) = c S("f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\\ b >= a + 1 ]", 0-0) = a S("f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\\ b >= a + 1 ]", 0-1) = b S("f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\\ b >= a + 1 ]", 0-2) = c orients the transitions f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] weakly and the transition f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] strictly and produces the following problem: 7: T: (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (3, 1) f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 1) [ a >= b ] with all transitions in problem 7, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 2) [ a >= b /\ a >= c + 2 ] We thus obtain the following problem: 8: T: (3, 2) f4(a, b, c) -> f300(a, b, c + 2) [ a >= b /\ a >= c + 2 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 2) [ a >= b /\ a >= c + 2 ] with all transitions in problem 8, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 3) [ a >= b /\ a >= c + 2 /\ a >= c + 3 ] We thus obtain the following problem: 9: T: (3, 3) f4(a, b, c) -> f300(a, b, c + 3) [ a >= b /\ a >= c + 2 /\ a >= c + 3 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 3) [ a >= b /\ a >= c + 2 /\ a >= c + 3 ] with all transitions in problem 9, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 4) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 ] We thus obtain the following problem: 10: T: (3, 4) f4(a, b, c) -> f300(a, b, c + 4) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 4) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 ] with all transitions in problem 10, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 5) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 ] We thus obtain the following problem: 11: T: (3, 5) f4(a, b, c) -> f300(a, b, c + 5) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 5) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 ] with all transitions in problem 11, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 6) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 ] We thus obtain the following problem: 12: T: (3, 6) f4(a, b, c) -> f300(a, b, c + 6) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 6) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 ] with all transitions in problem 12, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 7) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 ] We thus obtain the following problem: 13: T: (3, 7) f4(a, b, c) -> f300(a, b, c + 7) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 7) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 ] with all transitions in problem 13, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 8) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 ] We thus obtain the following problem: 14: T: (3, 8) f4(a, b, c) -> f300(a, b, c + 8) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 8) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 ] with all transitions in problem 14, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 9) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 ] We thus obtain the following problem: 15: T: (3, 9) f4(a, b, c) -> f300(a, b, c + 9) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 9) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 ] with all transitions in problem 15, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 10) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 ] We thus obtain the following problem: 16: T: (3, 10) f4(a, b, c) -> f300(a, b, c + 10) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 10) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 ] with all transitions in problem 16, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 11) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 ] We thus obtain the following problem: 17: T: (3, 11) f4(a, b, c) -> f300(a, b, c + 11) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 11) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 ] with all transitions in problem 17, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 12) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 ] We thus obtain the following problem: 18: T: (3, 12) f4(a, b, c) -> f300(a, b, c + 12) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 12) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 ] with all transitions in problem 18, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 13) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 ] We thus obtain the following problem: 19: T: (3, 13) f4(a, b, c) -> f300(a, b, c + 13) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 13) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 ] with all transitions in problem 19, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 14) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 /\ a >= c + 14 ] We thus obtain the following problem: 20: T: (3, 14) f4(a, b, c) -> f300(a, b, c + 14) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 /\ a >= c + 14 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 14) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 /\ a >= c + 14 ] with all transitions in problem 20, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 15) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 /\ a >= c + 14 /\ a >= c + 15 ] We thus obtain the following problem: 21: T: (3, 15) f4(a, b, c) -> f300(a, b, c + 15) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 /\ a >= c + 14 /\ a >= c + 15 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 By chaining the transition f4(a, b, c) -> f300(a, b, c + 15) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 /\ a >= c + 14 /\ a >= c + 15 ] with all transitions in problem 21, the following new transition is obtained: f4(a, b, c) -> f300(a, b, c + 16) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 /\ a >= c + 14 /\ a >= c + 15 /\ a >= c + 16 ] We thus obtain the following problem: 22: T: (3, 16) f4(a, b, c) -> f300(a, b, c + 16) [ a >= b /\ a >= c + 2 /\ a >= c + 3 /\ a >= c + 4 /\ a >= c + 5 /\ a >= c + 6 /\ a >= c + 7 /\ a >= c + 8 /\ a >= c + 9 /\ a >= c + 10 /\ a >= c + 11 /\ a >= c + 12 /\ a >= c + 13 /\ a >= c + 14 /\ a >= c + 15 /\ a >= c + 16 ] (1, 1) f300(a, b, c) -> f2(a, b, c) [ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ a >= c + 1 /\ b >= a + 1 ] (1, 1) f300(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ a >= c + 1 /\ b >= a + 1 ] (356*a + 5*c + 353*b + 36*a^2 + 72*a*b + 36*b^2 + 2*a*c + 2*b*c + 2191, 1) f300(a, b, c) -> f300(a, b, c + 1) [ a >= c + 1 /\ a >= b ] (?, 1) f2(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f2(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f2(a, b, c) [ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ 0 >= f + 1 /\ b >= a + 1 ] (2*a + 2*b, 1) f4(a, b, c) -> f4(a + 1, b, c) [ f >= 1 /\ b >= a + 1 ] (1, 1) f5(a, b, c) -> f300(a, b, c) start location: f5 leaf cost: 1 Complexity upper bound ? Time: 6.706 sec (SMT: 6.227 sec)