YES(?, 111*c + 111*e + 111*m + 111*n + 195) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n) (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(1, c, c, e, e, p, o, 0, 1, p, o, 7, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(1, c, c, e, e, p, o, 0, 1, p, o, 7, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(1, c + 1, c + 1, e + 1, e + 1, p, 4, 1, 1, p, 4, 7, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f2(0, c, c, e, e, 3, p, 0, 0, 3, p, 2, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f2(0, c, c, e, e, 3, p, 0, 0, 3, p, 2, m, n) [ 7 >= p /\ p >= 5 ] (?, 1) f1(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f2(0, c + 1, c + 1, e + 1, e + 1, 3, 4, 1, 0, 3, 4, 2, m, n) (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(1, c, c, e, e, p, o, h, 1, p, o, 7, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(1, c, c, e, e, p, o, h, 1, p, o, 7, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(1, c + 1, c + 1, e + 1, e + 1, p, 4, 1, 1, p, 4, 7, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f3(0, c, c, e, e, p, o, h, 0, p, o, 3, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f3(0, c, c, e, e, p, o, h, 0, p, o, 3, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f3(0, c + 1, c + 1, e + 1, e + 1, p, 4, 1, 0, p, 4, 3, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f6(1, c, c, e, e, p, o, h, 1, p, o, 6, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f6(1, c, c, e, e, p, o, h, 1, p, o, 6, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f6(1, c + 1, c + 1, e + 1, e + 1, p, 4, 1, 1, p, 4, 6, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f4(p, c, c, e, e, o, 2, 0, p, o, 2, 4, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (?, 1) f6(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f4(p, c, c, e, e, o, 7, 1, p, o, 7, 4, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f2(0, c, c, e, e, p, o, 0, 0, p, o, 2, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f2(0, c, c, e, e, p, o, 0, 0, p, o, 2, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f2(0, c + 1, c + 1, e + 1, e + 1, p, 4, 0, 0, p, 4, 2, m, n) [ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(0, c, c, e, e, p, o, h, 0, p, o, 7, m, n) [ e >= m /\ c >= n /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(0, c, c, e, e, p, o, h, 0, p, o, 7, m, n) [ e >= m /\ c >= n /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(0, c + 1, c + 1, e + 1, e + 1, p, 4, 1, 0, p, 4, 7, m, n) [ e + 1 >= m /\ c + 1 >= n /\ 7 >= p /\ p >= 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(1, c, c, e, e, p, o, h, 1, p, o, 7, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(1, c, c, e, e, p, o, h, 1, p, o, 7, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l, m, n) -> f7(1, c + 1, c + 1, e + 1, e + 1, p, 4, 1, 1, p, 4, 7, m, n) [ 7 >= p /\ p >= 1 ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [c, e, h, m, n]. We thus obtain the following problem: 2: T: (?, 1) f4(c, e, h, m, n) -> f7(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f7(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f7(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f7(c + 1, e + 1, 1, m, n) [ e + 1 >= m /\ c + 1 >= n /\ 7 >= p /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f7(c, e, h, m, n) [ e >= m /\ c >= n /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f7(c, e, h, m, n) [ e >= m /\ c >= n /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f7(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f7(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f7(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n) (?, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ p >= 5 ] (?, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (?, 1) f1(c, e, h, m, n) -> f7(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f1(c, e, h, m, n) -> f7(c, e, 0, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f1(c, e, h, m, n) -> f7(c, e, 0, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (1, 1) f0(c, e, h, m, n) -> f1(c, e, h, m, n) start location: f0 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n) (?, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ p >= 5 ] (?, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (1, 1) f0(c, e, h, m, n) -> f1(c, e, h, m, n) start location: f0 leaf cost: 12 Repeatedly propagating knowledge in problem 3 produces the following problem: 4: T: (?, 1) f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (1, 1) f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n) (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ p >= 5 ] (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (1, 1) f0(c, e, h, m, n) -> f1(c, e, h, m, n) start location: f0 leaf cost: 12 A polynomial rank function with Pol(f4) = -V_1 - V_2 + V_4 + V_5 - 3 Pol(f2) = -V_1 - V_2 + V_4 + V_5 - 3 Pol(f6) = -V_1 - V_2 + V_4 + V_5 - 3 Pol(f3) = -V_1 - V_2 + V_4 + V_5 - 3 Pol(f1) = -V_1 - V_2 + V_4 + V_5 - 3 Pol(f0) = -V_1 - V_2 + V_4 + V_5 - 3 orients all transitions weakly and the transition f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] strictly and produces the following problem: 5: T: (c + e + m + n + 3, 1) f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (1, 1) f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n) (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ p >= 5 ] (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (1, 1) f0(c, e, h, m, n) -> f1(c, e, h, m, n) start location: f0 leaf cost: 12 A polynomial rank function with Pol(f6) = 1 Pol(f4) = V_3 Pol(f2) = 1 Pol(f3) = 1 and size complexities S("f0(c, e, h, m, n) -> f1(c, e, h, m, n)", 0-0) = c S("f0(c, e, h, m, n) -> f1(c, e, h, m, n)", 0-1) = e S("f0(c, e, h, m, n) -> f1(c, e, h, m, n)", 0-2) = h S("f0(c, e, h, m, n) -> f1(c, e, h, m, n)", 0-3) = m S("f0(c, e, h, m, n) -> f1(c, e, h, m, n)", 0-4) = n S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ 3 >= p /\\ p >= 1 ]", 0-0) = c S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ 3 >= p /\\ p >= 1 ]", 0-1) = e S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ 3 >= p /\\ p >= 1 ]", 0-2) = 0 S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ 3 >= p /\\ p >= 1 ]", 0-3) = m S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ 3 >= p /\\ p >= 1 ]", 0-4) = n S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ p >= 5 ]", 0-0) = c S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ p >= 5 ]", 0-1) = e S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ p >= 5 ]", 0-2) = 0 S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ p >= 5 ]", 0-3) = m S("f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\\ p >= 5 ]", 0-4) = n S("f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n)", 0-0) = c + 1 S("f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n)", 0-1) = e + 1 S("f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n)", 0-2) = 1 S("f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n)", 0-3) = m S("f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n)", 0-4) = n S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-0) = ? S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-1) = ? S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-2) = 1 S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-3) = m S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-4) = n S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-0) = ? S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-1) = ? S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-2) = 1 S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-3) = m S("f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-4) = n S("f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-0) = ? S("f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-1) = ? S("f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-2) = 1 S("f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-3) = m S("f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-4) = n S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-0) = ? S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-1) = ? S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-2) = 1 S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-3) = m S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 ]", 0-4) = n S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-0) = ? S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-1) = ? S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-2) = 1 S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-3) = m S("f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 ]", 0-4) = n S("f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-0) = ? S("f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-1) = ? S("f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-2) = 1 S("f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-3) = m S("f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\\ p >= 1 ]", 0-4) = n S("f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 ]", 0-0) = ? S("f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 ]", 0-1) = ? S("f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 ]", 0-2) = 0 S("f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 ]", 0-3) = m S("f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 ]", 0-4) = n S("f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 /\\ h = 1 ]", 0-0) = ? S("f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 /\\ h = 1 ]", 0-1) = ? S("f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 /\\ h = 1 ]", 0-2) = 1 S("f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 /\\ h = 1 ]", 0-3) = m S("f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\\ 1 >= p /\\ p >= 0 /\\ o >= 1 /\\ h = 1 ]", 0-4) = n S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 /\\ h = 1 ]", 0-0) = ? S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 /\\ h = 1 ]", 0-1) = ? S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 /\\ h = 1 ]", 0-2) = 0 S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 /\\ h = 1 ]", 0-3) = m S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ 3 >= o /\\ o >= 1 /\\ p >= 1 /\\ h = 1 ]", 0-4) = n S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 /\\ h = 1 ]", 0-0) = ? S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 /\\ h = 1 ]", 0-1) = ? S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 /\\ h = 1 ]", 0-2) = 0 S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 /\\ h = 1 ]", 0-3) = m S("f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\\ m >= e + 1 /\\ n >= 1 /\\ n >= c + 1 /\\ 7 >= o /\\ 7 >= p /\\ o >= 5 /\\ p >= 1 /\\ h = 1 ]", 0-4) = n S("f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\\ n >= c + 2 /\\ m >= 1 /\\ n >= 1 /\\ 7 >= p /\\ p >= 1 ]", 0-0) = ? S("f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\\ n >= c + 2 /\\ m >= 1 /\\ n >= 1 /\\ 7 >= p /\\ p >= 1 ]", 0-1) = ? S("f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\\ n >= c + 2 /\\ m >= 1 /\\ n >= 1 /\\ 7 >= p /\\ p >= 1 ]", 0-2) = 0 S("f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\\ n >= c + 2 /\\ m >= 1 /\\ n >= 1 /\\ 7 >= p /\\ p >= 1 ]", 0-3) = m S("f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\\ n >= c + 2 /\\ m >= 1 /\\ n >= 1 /\\ 7 >= p /\\ p >= 1 ]", 0-4) = n orients the transitions f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] weakly and the transition f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] strictly and produces the following problem: 6: T: (c + e + m + n + 3, 1) f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (c + e + m + n + 6, 1) f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ 7 >= p /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (1, 1) f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n) (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ p >= 5 ] (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (1, 1) f0(c, e, h, m, n) -> f1(c, e, h, m, n) start location: f0 leaf cost: 12 Applied AI with 'oct' on problem 6 to obtain the following invariants: For symbol f2: -X_3 + 1 >= 0 /\ X_3 >= 0 For symbol f3: -X_3 + 1 >= 0 /\ X_3 >= 0 For symbol f4: -X_3 + 1 >= 0 /\ X_3 >= 0 For symbol f6: -X_3 + 1 >= 0 /\ X_3 >= 0 This yielded the following problem: 7: T: (1, 1) f0(c, e, h, m, n) -> f1(c, e, h, m, n) (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ p >= 5 ] (1, 1) f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n) (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= p /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= p /\ p >= 1 ] (c + e + m + n + 6, 1) f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (c + e + m + n + 3, 1) f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] start location: f0 leaf cost: 12 A polynomial rank function with Pol(f0) = -V_1 - 3*V_2 + 3*V_4 + V_5 - 1 Pol(f1) = -V_1 - 3*V_2 + 3*V_4 + V_5 - 1 Pol(f2) = -V_1 - 3*V_2 + 4*V_3 + 3*V_4 + V_5 - 1 Pol(f3) = -V_1 - 3*V_2 + 4*V_3 + 3*V_4 + V_5 - 2 Pol(f6) = -V_1 - 3*V_2 + 4*V_3 + 3*V_4 + V_5 - 3 Pol(f4) = -V_1 - 3*V_2 + 3*V_3 + 3*V_4 + V_5 - 3 orients all transitions weakly and the transition f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] strictly and produces the following problem: 8: T: (1, 1) f0(c, e, h, m, n) -> f1(c, e, h, m, n) (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ p >= 5 ] (1, 1) f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n) (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= p /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= p /\ p >= 1 ] (c + e + m + n + 6, 1) f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (?, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (c + 3*e + 3*m + n + 1, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (c + e + m + n + 3, 1) f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] start location: f0 leaf cost: 12 A polynomial rank function with Pol(f0) = -3*V_1 - V_2 + V_4 + 3*V_5 - 1 Pol(f1) = -3*V_1 - V_2 + V_4 + 3*V_5 - 1 Pol(f2) = -3*V_1 - V_2 + 4*V_3 + V_4 + 3*V_5 - 1 Pol(f3) = -3*V_1 - V_2 + 4*V_3 + V_4 + 3*V_5 - 2 Pol(f6) = -3*V_1 - V_2 + 4*V_3 + V_4 + 3*V_5 - 3 Pol(f4) = -3*V_1 - V_2 + 3*V_3 + V_4 + 3*V_5 - 3 orients all transitions weakly and the transition f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] strictly and produces the following problem: 9: T: (1, 1) f0(c, e, h, m, n) -> f1(c, e, h, m, n) (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ p >= 5 ] (1, 1) f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n) (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= p /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (?, 1) f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= p /\ p >= 1 ] (c + e + m + n + 6, 1) f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (?, 1) f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (3*c + e + m + 3*n + 1, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (c + 3*e + 3*m + n + 1, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (c + e + m + n + 3, 1) f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] start location: f0 leaf cost: 12 Repeatedly propagating knowledge in problem 9 produces the following problem: 10: T: (1, 1) f0(c, e, h, m, n) -> f1(c, e, h, m, n) (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ 3 >= p /\ p >= 1 ] (1, 1) f1(c, e, h, m, n) -> f2(c, e, 0, m, n) [ 7 >= p /\ p >= 5 ] (1, 1) f1(c, e, h, m, n) -> f2(c + 1, e + 1, 1, m, n) (5*c + 5*e + 5*m + 5*n + 8, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (5*c + 5*e + 5*m + 5*n + 8, 1) f2(c, e, h, m, n) -> f3(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (5*c + 5*e + 5*m + 5*n + 8, 1) f2(c, e, h, m, n) -> f3(c + 1, e + 1, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= p /\ p >= 1 ] (15*c + 15*e + 15*m + 15*n + 24, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 ] (15*c + 15*e + 15*m + 15*n + 24, 1) f3(c, e, h, m, n) -> f6(c, e, h, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 ] (15*c + 15*e + 15*m + 15*n + 24, 1) f3(c, e, h, m, n) -> f6(c + 1, e + 1, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= p /\ p >= 1 ] (c + e + m + n + 6, 1) f6(c, e, h, m, n) -> f4(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 ] (45*c + 45*e + 45*m + 45*n + 72, 1) f6(c, e, h, m, n) -> f4(c, e, 1, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ 7 >= o /\ 1 >= p /\ p >= 0 /\ o >= 1 /\ h = 1 ] (3*c + e + m + 3*n + 1, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ 3 >= o /\ o >= 1 /\ p >= 1 /\ h = 1 ] (c + 3*e + 3*m + n + 1, 1) f4(c, e, h, m, n) -> f2(c, e, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= 1 /\ m >= e + 1 /\ n >= 1 /\ n >= c + 1 /\ 7 >= o /\ 7 >= p /\ o >= 5 /\ p >= 1 /\ h = 1 ] (c + e + m + n + 3, 1) f4(c, e, h, m, n) -> f2(c + 1, e + 1, 0, m, n) [ -h + 1 >= 0 /\ h >= 0 /\ m >= e + 2 /\ n >= c + 2 /\ m >= 1 /\ n >= 1 /\ 7 >= p /\ p >= 1 ] start location: f0 leaf cost: 12 Complexity upper bound 111*c + 111*e + 111*m + 111*n + 195 Time: 1.433 sec (SMT: 1.307 sec)