YES(?, 13577382562501012*a + 13577382562501008*b + 4*e + 61920*a^2 + 123120*a*b + 61200*b^2 + 61200*a*e + 61200*b*e + 4) Initial complexity problem: 1: T: (?, 1) f0(a, b, c, d, e, f, g, h) -> f12(a, b, 0, b, e, f, g, h) [ a >= b + 1 ] (?, 1) f12(a, b, c, d, e, f, g, h) -> f12(a, b, c, d, e + 1, j, i, h) [ a >= e /\ i >= j ] (?, 1) f12(a, b, c, d, e, f, g, h) -> f12(a, b, j, e, e + 1, i, k, h) [ a >= e /\ i >= k + 1 ] (?, 1) f22(a, b, c, d, e, f, g, h) -> f22(a, b, c, d, e + 1, f, g, j) [ a >= e ] (?, 1) f29(a, b, c, d, e, f, g, h) -> f29(a, b, c, d, e + 1, f, g, j) [ a >= e ] (?, 1) f35(a, b, c, d, e, f, g, h) -> f37(a, b, c, d, e, f, g, h) [ 0 >= c + 1 ] (?, 1) f35(a, b, c, d, e, f, g, h) -> f37(a, b, c, d, e, f, g, h) [ c >= 1 ] (?, 1) f37(a, b, c, d, e, f, g, h) -> f43(a, b, c, d, e, f, g, j) [ a >= d /\ 0 >= i + 1 ] (?, 1) f37(a, b, c, d, e, f, g, h) -> f43(a, b, c, d, e, f, g, j) [ a >= d /\ i >= 1 ] (?, 1) f43(a, b, c, d, e, f, g, h) -> f43(a, b, c, d, e + 1, f, g, h) [ a >= e ] (?, 1) f48(a, b, c, d, e, f, g, h) -> f48(a, b, c, d, e + 1, f, g, h) [ a >= e ] (?, 1) f37(a, b, c, d, e, f, g, h) -> f37(a, b, c, d + 1, e, f, g, 0) [ a >= d ] (?, 1) f35(a, b, c, d, e, f, g, h) -> f0(a, b + 1, 0, d, e, f, g, h) [ c = 0 ] (?, 1) f48(a, b, c, d, e, f, g, h) -> f37(a, b, c, d + 1, e, f, g, h) [ e >= a + 1 ] (?, 1) f43(a, b, c, d, e, f, g, h) -> f48(a, b, c, d, e, f, g, h) [ e >= a + 1 ] (?, 1) f37(a, b, c, d, e, f, g, h) -> f0(a, b + 1, c, d, e, f, g, h) [ d >= a + 1 ] (?, 1) f29(a, b, c, d, e, f, g, h) -> f35(a, b, c, d, e, f, g, h) [ e >= a + 1 ] (?, 1) f22(a, b, c, d, e, f, g, h) -> f29(a, b, c, d, e, f, g, h) [ e >= a + 1 ] (?, 1) f12(a, b, c, d, e, f, g, h) -> f35(a, b, c, b, e, f, g, h) [ e >= a + 1 /\ b = d ] (?, 1) f12(a, b, c, d, e, f, g, h) -> f22(a, b, c, d, e, f, g, h) [ b >= d + 1 /\ e >= a + 1 ] (?, 1) f12(a, b, c, d, e, f, g, h) -> f22(a, b, c, d, e, f, g, h) [ d >= b + 1 /\ e >= a + 1 ] (?, 1) f0(a, b, c, d, e, f, g, h) -> f58(a, b, c, d, e, f, g, h) [ b >= a ] (1, 1) start(a, b, c, d, e, f, g, h) -> f0(a, b, c, d, e, f, g, h) start location: start leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, c, d, e]. We thus obtain the following problem: 2: T: (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) (?, 1) f0(a, b, c, d, e) -> f58(a, b, c, d, e) [ b >= a ] (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] (?, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] (?, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] (?, 1) f48(a, b, c, d, e) -> f48(a, b, c, d, e + 1) [ a >= e ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] (?, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] (?, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] (?, 1) f29(a, b, c, d, e) -> f29(a, b, c, d, e + 1) [ a >= e ] (?, 1) f22(a, b, c, d, e) -> f22(a, b, c, d, e + 1) [ a >= e ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] (?, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] start location: start leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] (?, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] (?, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] (?, 1) f48(a, b, c, d, e) -> f48(a, b, c, d, e + 1) [ a >= e ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] (?, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] (?, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] (?, 1) f29(a, b, c, d, e) -> f29(a, b, c, d, e + 1) [ a >= e ] (?, 1) f22(a, b, c, d, e) -> f22(a, b, c, d, e + 1) [ a >= e ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] (?, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] start location: start leaf cost: 1 Testing for reachability in the complexity graph removes the following transitions from problem 3: f48(a, b, c, d, e) -> f48(a, b, c, d, e + 1) [ a >= e ] f29(a, b, c, d, e) -> f29(a, b, c, d, e + 1) [ a >= e ] f22(a, b, c, d, e) -> f22(a, b, c, d, e + 1) [ a >= e ] We thus obtain the following problem: 4: T: (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] (?, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] (?, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] (?, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] (?, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] (?, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] (?, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] (?, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) start location: start leaf cost: 1 A polynomial rank function with Pol(f48) = 6*V_1 - 6*V_2 - 5 Pol(f37) = 6*V_1 - 6*V_2 - 5 Pol(f43) = 6*V_1 - 6*V_2 - 5 Pol(f29) = 6*V_1 - 6*V_2 - 3 Pol(f35) = 6*V_1 - 6*V_2 - 4 Pol(f0) = 6*V_1 - 6*V_2 Pol(f22) = 6*V_1 - 6*V_2 - 2 Pol(f12) = 6*V_1 - 6*V_2 - 1 Pol(start) = 6*V_1 - 6*V_2 orients all transitions weakly and the transition f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] strictly and produces the following problem: 5: T: (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] (?, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] (?, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] (?, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] (?, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] (?, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] (?, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] (6*a + 6*b, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) start location: start leaf cost: 1 A polynomial rank function with Pol(f48) = -1 Pol(f37) = -1 Pol(f43) = -1 Pol(f0) = -2 Pol(f35) = 1 Pol(f29) = 2 Pol(f22) = 3 Pol(f12) = 4 and size complexities S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-0) = a S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-1) = b S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-2) = c S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-3) = d S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-4) = e S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-0) = a S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-1) = ? S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-2) = 0 S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-3) = ? S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-0) = a S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-1) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-2) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-3) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-4) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-1) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-3) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-0) = a S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-1) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-2) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-3) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-4) = ? S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-0) = a S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-1) = ? S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-2) = 0 S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-3) = ? S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-4) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-0) = a S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-1) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-2) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-3) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-4) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-0) = a S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-1) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-2) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-3) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-1) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-3) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-1) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-3) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-4) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-1) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-4) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-0) = a S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-1) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-2) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-3) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-4) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-1) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-4) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-1) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-4) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-0) = a S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-1) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-2) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-3) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-4) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-0) = a S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-1) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-2) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-3) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-4) = ? orients the transitions f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] weakly and the transitions f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] strictly and produces the following problem: 6: T: (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] (24*a + 24*b, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] (?, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] (24*a + 24*b, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] (6*a + 6*b, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) start location: start leaf cost: 1 A polynomial rank function with Pol(f48) = 1 Pol(f37) = 1 Pol(f43) = 1 Pol(f0) = 0 Pol(f12) = -2 Pol(f22) = -3 and size complexities S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-0) = a S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-1) = b S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-2) = c S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-3) = d S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-4) = e S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-0) = a S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-1) = ? S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-2) = 0 S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-3) = ? S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-0) = a S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-1) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-2) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-3) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-4) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-1) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-3) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-0) = a S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-1) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-2) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-3) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-4) = ? S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-0) = a S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-1) = ? S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-2) = 0 S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-3) = ? S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-4) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-0) = a S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-1) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-2) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-3) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-4) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-0) = a S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-1) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-2) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-3) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-1) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-3) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-1) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-3) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-4) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-1) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-4) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-0) = a S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-1) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-2) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-3) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-4) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-1) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-4) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-1) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-4) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-0) = a S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-1) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-2) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-3) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-4) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-0) = a S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-1) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-2) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-3) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-4) = ? orients the transitions f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] weakly and the transition f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] strictly and produces the following problem: 7: T: (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] (24*a + 24*b, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] (60*a + 60*b, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] (24*a + 24*b, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] (6*a + 6*b, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) start location: start leaf cost: 1 A polynomial rank function with Pol(f48) = -1 Pol(f37) = -1 Pol(f43) = -1 Pol(f12) = 1 Pol(f22) = 0 and size complexities S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-0) = a S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-1) = b S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-2) = c S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-3) = d S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-4) = e S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-0) = a S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-1) = 85*a + 85*b S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-2) = 0 S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-3) = 85*a + 85*b S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-0) = a S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-2) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-3) = 85*a + 85*b S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\\ b = d ]", 0-4) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-3) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\\ i >= k + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-0) = a S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-2) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-3) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\\ i >= j ]", 0-4) = ? S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-0) = a S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-1) = 85*a + 85*b S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-2) = 0 S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-3) = ? S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ]", 0-4) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-0) = a S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-1) = 85*a + 85*b S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-2) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-3) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ]", 0-4) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-0) = a S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-1) = 85*a + 85*b S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-2) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-3) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-3) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\\ e >= a + 1 ]", 0-4) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-3) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\\ e >= a + 1 ]", 0-4) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-1) = 85*a + 85*b S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ]", 0-4) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-0) = a S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-1) = 85*a + 85*b S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-2) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-3) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ]", 0-4) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-1) = 85*a + 85*b S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ i >= 1 ]", 0-4) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-1) = 85*a + 85*b S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\\ 0 >= i + 1 ]", 0-4) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-0) = a S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-2) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-3) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ]", 0-4) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-0) = a S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-1) = 85*a + 85*b S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-2) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-3) = ? S("f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ]", 0-4) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-0) = a S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-2) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-3) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ]", 0-4) = ? orients the transitions f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] weakly and the transition f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] strictly and produces the following problem: 8: T: (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] (?, 1) f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] (24*a + 24*b, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] (60*a + 60*b, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] (24*a + 24*b, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] (54*a + 54*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] (?, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] (6*a + 6*b, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) start location: start leaf cost: 1 A polynomial rank function with Pol(f48) = 2*V_1 - 2*V_5 + 1 Pol(f37) = 2*V_1 - 2*V_5 + 1 Pol(f43) = 2*V_1 - 2*V_5 + 1 Pol(f29) = 2*V_1 - 2*V_5 + 1 Pol(f35) = 2*V_1 - 2*V_5 + 1 Pol(f0) = 2*V_1 - 2*V_5 + 1 Pol(f22) = 2*V_1 - 2*V_5 + 1 Pol(f12) = 2*V_1 - 2*V_5 + 1 Pol(start) = 2*V_1 - 2*V_5 + 1 orients all transitions weakly and the transitions f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] strictly and produces the following problem: 9: T: (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ e >= a + 1 ] (2*a + 2*e + 1, 1) f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ a >= e ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ e >= a + 1 ] (24*a + 24*b, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ e >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ 0 >= i + 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ a >= d ] (60*a + 60*b, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ d >= a + 1 ] (24*a + 24*b, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ e >= a + 1 ] (54*a + 54*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ b >= d + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ d >= b + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ 0 >= c + 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ c >= 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ c = 0 ] (2*a + 2*e + 1, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a >= e /\ i >= j ] (2*a + 2*e + 1, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a >= e /\ i >= k + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ e >= a + 1 /\ b = d ] (6*a + 6*b, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) start location: start leaf cost: 1 Applied AI with 'oct' on problem 9 to obtain the following invariants: For symbol f12: X_1 - X_2 - 1 >= 0 For symbol f22: -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_2 - 1 >= 0 For symbol f29: -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_2 - 1 >= 0 For symbol f35: -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_2 - 1 >= 0 For symbol f37: -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_2 - 1 >= 0 For symbol f43: -X_4 + X_5 - 1 >= 0 /\ -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ X_1 - X_2 - 1 >= 0 For symbol f48: -X_4 + X_5 - 1 >= 0 /\ -X_2 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 1 >= 0 /\ X_1 - X_4 >= 0 /\ X_1 - X_2 - 1 >= 0 This yielded the following problem: 10: T: (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) (6*a + 6*b, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ a - b - 1 >= 0 /\ e >= a + 1 /\ b = d ] (2*a + 2*e + 1, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= k + 1 ] (2*a + 2*e + 1, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= j ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c = 0 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c >= 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= c + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\ d >= b + 1 /\ e >= a + 1 ] (54*a + 54*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\ b >= d + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] (60*a + 60*b, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ d >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ 0 >= i + 1 ] (24*a + 24*b, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] (2*a + 2*e + 1, 1) f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ a >= e ] (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] start location: start leaf cost: 1 Testing for unsatisfiable constraints removes the following transition from problem 10: f43(a, b, c, d, e) -> f43(a, b, c, d, e + 1) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ a >= e ] We thus obtain the following problem: 11: T: (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) (6*a + 6*b, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ a - b - 1 >= 0 /\ e >= a + 1 /\ b = d ] (2*a + 2*e + 1, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= k + 1 ] (2*a + 2*e + 1, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= j ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c = 0 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c >= 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= c + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\ d >= b + 1 /\ e >= a + 1 ] (54*a + 54*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\ b >= d + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] (60*a + 60*b, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ d >= a + 1 ] (?, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ i >= 1 ] (?, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ 0 >= i + 1 ] (24*a + 24*b, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] (?, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] (?, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] start location: start leaf cost: 1 A polynomial rank function with Pol(f48) = 3*V_1 - 3*V_4 + 1 Pol(f37) = 3*V_1 - 3*V_4 + 3 Pol(f43) = 3*V_1 - 3*V_4 + 2 and size complexities S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-0) = a S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-2) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-3) = ? S("f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50 S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-0) = a S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-2) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-3) = ? S("f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\\ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - d >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50 S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-0) = a S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-2) = ? S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-3) = 85*a + 85*b + 85*e + 221852656250 S("f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50 S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ 0 >= i + 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ 0 >= i + 1 ]", 0-1) = 85*a + 85*b S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ 0 >= i + 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ 0 >= i + 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ 0 >= i + 1 ]", 0-4) = 5*a + 5*e + 50 S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ i >= 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ i >= 1 ]", 0-1) = 85*a + 85*b S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ i >= 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ i >= 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d /\\ i >= 1 ]", 0-4) = 5*a + 5*e + 50 S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-0) = a S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-1) = 85*a + 85*b S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-2) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-3) = ? S("f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ a >= d ]", 0-4) = 5*a + 5*e + 50 S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-0) = a S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-1) = 85*a + 85*b S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-2) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-3) = ? S("f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ d >= a + 1 ]", 0-4) = 5*a + 5*e + 50 S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-0) = a S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-2) = ? S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-3) = 85*a + 85*b + 85*e + 2610031250 S("f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50 S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-3) = 85*a + 85*b + 85*e + 30706250 S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ b >= d + 1 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50 S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-3) = 85*a + 85*b + 85*e + 30706250 S("f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\\ d >= b + 1 /\\ e >= a + 1 ]", 0-4) = 5*a + 5*e + 50 S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-0) = a S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-1) = 85*a + 85*b S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-2) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-3) = 85*a + 85*b + 85*e + 18857475781250 S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ 0 >= c + 1 ]", 0-4) = 5*a + 5*e + 50 S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-0) = a S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-1) = 85*a + 85*b S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-2) = ? S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-3) = 85*a + 85*b + 85*e + 18857475781250 S("f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c >= 1 ]", 0-4) = 5*a + 5*e + 50 S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-0) = a S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-1) = 85*a + 85*b S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-2) = 0 S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-3) = 85*a + 85*b + 85*e + 18857475781250 S("f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\\ -a + e - 1 >= 0 /\\ a - b - 1 >= 0 /\\ c = 0 ]", 0-4) = 5*a + 5*e + 50 S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-0) = a S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-2) = ? S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-3) = 85*a + 85*b + 85*e + 361250 S("f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= j ]", 0-4) = 5*a + 5*e + 50 S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-0) = a S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-2) = ? S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-3) = 5*a + 5*e + 250 S("f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\\ a >= e /\\ i >= k + 1 ]", 0-4) = 5*a + 5*e + 50 S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-0) = a S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-1) = 85*a + 85*b S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-2) = ? S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-3) = 85*a + 85*b S("f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ a - b - 1 >= 0 /\\ e >= a + 1 /\\ b = d ]", 0-4) = 5*a + 5*e + 50 S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-0) = a S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-1) = 85*a + 85*b S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-2) = 0 S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-3) = 85*a + 85*b S("f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ]", 0-4) = 5*a + 5*e + 50 S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-0) = a S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-1) = b S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-2) = c S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-3) = d S("start(a, b, c, d, e) -> f0(a, b, c, d, e)", 0-4) = e orients the transitions f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ i >= 1 ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ 0 >= i + 1 ] f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ] weakly and the transitions f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ i >= 1 ] f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ 0 >= i + 1 ] f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ] strictly and produces the following problem: 12: T: (1, 1) start(a, b, c, d, e) -> f0(a, b, c, d, e) (6*a + 6*b, 1) f0(a, b, c, d, e) -> f12(a, b, 0, b, e) [ a >= b + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f35(a, b, c, b, e) [ a - b - 1 >= 0 /\ e >= a + 1 /\ b = d ] (2*a + 2*e + 1, 1) f12(a, b, c, d, e) -> f12(a, b, j, e, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= k + 1 ] (2*a + 2*e + 1, 1) f12(a, b, c, d, e) -> f12(a, b, c, d, e + 1) [ a - b - 1 >= 0 /\ a >= e /\ i >= j ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f0(a, b + 1, 0, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c = 0 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ c >= 1 ] (24*a + 24*b, 1) f35(a, b, c, d, e) -> f37(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ 0 >= c + 1 ] (24*a + 24*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\ d >= b + 1 /\ e >= a + 1 ] (54*a + 54*b, 1) f12(a, b, c, d, e) -> f22(a, b, c, d, e) [ a - b - 1 >= 0 /\ b >= d + 1 /\ e >= a + 1 ] (24*a + 24*b, 1) f22(a, b, c, d, e) -> f29(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] (60*a + 60*b, 1) f37(a, b, c, d, e) -> f0(a, b + 1, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ d >= a + 1 ] (12384*a^2 + 24624*a*b + 12240*b^2 + 12240*a*e + 12240*b*e + 2715476512500144*a + 2715476512500144*b, 1) f37(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d ] (12384*a^2 + 24624*a*b + 12240*b^2 + 12240*a*e + 12240*b*e + 2715476512500144*a + 2715476512500144*b, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ i >= 1 ] (12384*a^2 + 24624*a*b + 12240*b^2 + 12240*a*e + 12240*b*e + 2715476512500144*a + 2715476512500144*b, 1) f37(a, b, c, d, e) -> f43(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ a >= d /\ 0 >= i + 1 ] (24*a + 24*b, 1) f29(a, b, c, d, e) -> f35(a, b, c, d, e) [ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] (12384*a^2 + 24624*a*b + 12240*b^2 + 12240*a*e + 12240*b*e + 2715476512500144*a + 2715476512500144*b, 1) f43(a, b, c, d, e) -> f48(a, b, c, d, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] (12384*a^2 + 24624*a*b + 12240*b^2 + 12240*a*e + 12240*b*e + 2715476512500144*a + 2715476512500144*b, 1) f48(a, b, c, d, e) -> f37(a, b, c, d + 1, e) [ -d + e - 1 >= 0 /\ -b + e - 2 >= 0 /\ -a + e - 1 >= 0 /\ a - d >= 0 /\ a - b - 1 >= 0 /\ e >= a + 1 ] start location: start leaf cost: 1 Complexity upper bound 13577382562501012*a + 13577382562501008*b + 4*e + 61920*a^2 + 123120*a*b + 61200*b^2 + 61200*a*e + 61200*b*e + 4 Time: 1.478 sec (SMT: 1.332 sec)