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