YES(?, 42136*a + 42076*b + 21368*f + 21308*d + 320*a^2 + 608*a*b + 480*a*f + 448*a*d + 464*b*f + 160*f^2 + 304*d*f + 288*b^2 + 432*b*d + 144*d^2 + 77869) Initial complexity problem: 1: T: (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l) -> f3(a, b, c, d, e, f, g, h, i, j, k, l) (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l) -> f4(a, b, c, d, e, f, g, h, i, j, k, l) (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l) -> f8(a, b, c, d, e, f, g, h, i, j, k, l) (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l) -> f4(a, b, d, d, f, f, a, b, i, j, k, l) [ a >= b + 1 ] (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l) -> f4(a, b, d, d, f, f, a, b, i, j, k, l) [ b >= a + 1 ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l) -> f3(f, d, d, d, f, f, a, b, i, j, k, l) (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l) -> f3(f, d, d, d, f, f, m, n, m, n, k, l) (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l) -> f8(o, p, d, m, f, n, a, b, m, n, o, p) (?, 1) f3(a, b, c, d, e, f, g, h, i, j, k, l) -> f8(o, p, d, m, f, n, a, a, m, n, o, p) [ a = b ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l) -> f3(a + 1, b, d, d, f, f, a, b, i, j, k, l) (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l) -> f3(a + 1, b, d, d, f, f, a, b, i, j, k, l) [ b >= a + 1 ] (1, 1) f0(a, b, c, d, e, f, g, h, i, j, k, l) -> f3(a, b + 1, d, d, f, f, a, b, i, j, k, l) (?, 1) f4(a, b, c, d, e, f, g, h, i, j, k, l) -> f3(a, b + 1, d, d, f, f, a, b, i, j, k, l) [ a >= b ] start location: f0 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, d, f]. We thus obtain the following problem: 2: T: (?, 1) f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ] (1, 1) f0(a, b, d, f) -> f3(a, b + 1, d, f) (?, 1) f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ] (1, 1) f0(a, b, d, f) -> f3(a + 1, b, d, f) (?, 1) f3(a, b, d, f) -> f8(o, p, m, n) [ a = b ] (1, 1) f0(a, b, d, f) -> f8(o, p, m, n) (1, 1) f0(a, b, d, f) -> f3(f, d, d, f) (1, 1) f0(a, b, d, f) -> f3(f, d, d, f) (?, 1) f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ] (?, 1) f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ] (1, 1) f0(a, b, d, f) -> f8(a, b, d, f) (1, 1) f0(a, b, d, f) -> f4(a, b, d, f) (1, 1) f0(a, b, d, f) -> f3(a, b, d, f) 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, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ] (1, 1) f0(a, b, d, f) -> f3(a, b + 1, d, f) (?, 1) f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ] (1, 1) f0(a, b, d, f) -> f3(a + 1, b, d, f) (1, 1) f0(a, b, d, f) -> f3(f, d, d, f) (1, 1) f0(a, b, d, f) -> f3(f, d, d, f) (?, 1) f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ] (?, 1) f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ] (1, 1) f0(a, b, d, f) -> f4(a, b, d, f) (1, 1) f0(a, b, d, f) -> f3(a, b, d, f) start location: f0 leaf cost: 3 A polynomial rank function with Pol(f4) = 2*V_1 - 2*V_2 + 1 Pol(f3) = 2*V_1 - 2*V_2 + 2 and size complexities S("f0(a, b, d, f) -> f3(a, b, d, f)", 0-0) = a S("f0(a, b, d, f) -> f3(a, b, d, f)", 0-1) = b S("f0(a, b, d, f) -> f3(a, b, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(a, b, d, f)", 0-3) = f S("f0(a, b, d, f) -> f4(a, b, d, f)", 0-0) = a S("f0(a, b, d, f) -> f4(a, b, d, f)", 0-1) = b S("f0(a, b, d, f) -> f4(a, b, d, f)", 0-2) = d S("f0(a, b, d, f) -> f4(a, b, d, f)", 0-3) = f S("f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ]", 0-0) = a + f + 1 S("f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ]", 0-1) = ? S("f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ]", 0-2) = d S("f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ]", 0-3) = f S("f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ]", 0-0) = ? S("f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ]", 0-1) = ? S("f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ]", 0-2) = d S("f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ]", 0-3) = f S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-0) = f S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-1) = d S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-3) = f S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-0) = f S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-1) = d S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-3) = f S("f0(a, b, d, f) -> f3(a + 1, b, d, f)", 0-0) = a + 1 S("f0(a, b, d, f) -> f3(a + 1, b, d, f)", 0-1) = b S("f0(a, b, d, f) -> f3(a + 1, b, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(a + 1, b, d, f)", 0-3) = f S("f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ]", 0-0) = ? S("f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ]", 0-1) = ? S("f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ]", 0-2) = d S("f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ]", 0-3) = f S("f0(a, b, d, f) -> f3(a, b + 1, d, f)", 0-0) = a S("f0(a, b, d, f) -> f3(a, b + 1, d, f)", 0-1) = b + 1 S("f0(a, b, d, f) -> f3(a, b + 1, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(a, b + 1, d, f)", 0-3) = f S("f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ]", 0-0) = a + f + 1 S("f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ]", 0-1) = ? S("f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ]", 0-2) = d S("f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ]", 0-3) = f orients the transitions f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ] f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ] weakly and the transitions f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ] f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ] strictly and produces the following problem: 4: T: (8*a + 8*b + 4*f + 4*d + 15, 1) f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ] (1, 1) f0(a, b, d, f) -> f3(a, b + 1, d, f) (?, 1) f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ] (1, 1) f0(a, b, d, f) -> f3(a + 1, b, d, f) (1, 1) f0(a, b, d, f) -> f3(f, d, d, f) (1, 1) f0(a, b, d, f) -> f3(f, d, d, f) (?, 1) f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ] (8*a + 8*b + 4*f + 4*d + 15, 1) f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ] (1, 1) f0(a, b, d, f) -> f4(a, b, d, f) (1, 1) f0(a, b, d, f) -> f3(a, b, d, f) start location: f0 leaf cost: 3 A polynomial rank function with Pol(f4) = -2*V_1 + 2*V_2 - 1 Pol(f3) = -2*V_1 + 2*V_2 and size complexities S("f0(a, b, d, f) -> f3(a, b, d, f)", 0-0) = a S("f0(a, b, d, f) -> f3(a, b, d, f)", 0-1) = b S("f0(a, b, d, f) -> f3(a, b, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(a, b, d, f)", 0-3) = f S("f0(a, b, d, f) -> f4(a, b, d, f)", 0-0) = a S("f0(a, b, d, f) -> f4(a, b, d, f)", 0-1) = b S("f0(a, b, d, f) -> f4(a, b, d, f)", 0-2) = d S("f0(a, b, d, f) -> f4(a, b, d, f)", 0-3) = f S("f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ]", 0-0) = a + f + 1 S("f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ]", 0-1) = 9*a + 9*b + 9*d + 9*f + 1296 S("f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ]", 0-2) = d S("f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ]", 0-3) = f S("f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ]", 0-0) = ? S("f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ]", 0-1) = 9*a + 9*b + 9*d + 9*f + 11664 S("f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ]", 0-2) = d S("f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ]", 0-3) = f S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-0) = f S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-1) = d S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-3) = f S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-0) = f S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-1) = d S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(f, d, d, f)", 0-3) = f S("f0(a, b, d, f) -> f3(a + 1, b, d, f)", 0-0) = a + 1 S("f0(a, b, d, f) -> f3(a + 1, b, d, f)", 0-1) = b S("f0(a, b, d, f) -> f3(a + 1, b, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(a + 1, b, d, f)", 0-3) = f S("f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ]", 0-0) = ? S("f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ]", 0-1) = 9*a + 9*b + 9*d + 9*f + 11664 S("f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ]", 0-2) = d S("f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ]", 0-3) = f S("f0(a, b, d, f) -> f3(a, b + 1, d, f)", 0-0) = a S("f0(a, b, d, f) -> f3(a, b + 1, d, f)", 0-1) = b + 1 S("f0(a, b, d, f) -> f3(a, b + 1, d, f)", 0-2) = d S("f0(a, b, d, f) -> f3(a, b + 1, d, f)", 0-3) = f S("f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ]", 0-0) = a + f + 1 S("f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ]", 0-1) = 9*a + 9*b + 9*d + 9*f + 1296 S("f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ]", 0-2) = d S("f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ]", 0-3) = f orients the transitions f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ] f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ] weakly and the transitions f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ] f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ] strictly and produces the following problem: 5: T: (8*a + 8*b + 4*f + 4*d + 15, 1) f4(a, b, d, f) -> f3(a, b + 1, d, f) [ a >= b ] (1, 1) f0(a, b, d, f) -> f3(a, b + 1, d, f) (21060*a + 21030*b + 10680*f + 10650*d + 160*a^2 + 304*a*b + 240*a*f + 224*a*d + 232*b*f + 80*f^2 + 152*d*f + 144*b^2 + 216*b*d + 72*d^2 + 38915, 1) f4(a, b, d, f) -> f3(a + 1, b, d, f) [ b >= a + 1 ] (1, 1) f0(a, b, d, f) -> f3(a + 1, b, d, f) (1, 1) f0(a, b, d, f) -> f3(f, d, d, f) (1, 1) f0(a, b, d, f) -> f3(f, d, d, f) (21060*a + 21030*b + 10680*f + 10650*d + 160*a^2 + 304*a*b + 240*a*f + 224*a*d + 232*b*f + 80*f^2 + 152*d*f + 144*b^2 + 216*b*d + 72*d^2 + 38915, 1) f3(a, b, d, f) -> f4(a, b, d, f) [ b >= a + 1 ] (8*a + 8*b + 4*f + 4*d + 15, 1) f3(a, b, d, f) -> f4(a, b, d, f) [ a >= b + 1 ] (1, 1) f0(a, b, d, f) -> f4(a, b, d, f) (1, 1) f0(a, b, d, f) -> f3(a, b, d, f) start location: f0 leaf cost: 3 Complexity upper bound 42136*a + 42076*b + 21368*f + 21308*d + 320*a^2 + 608*a*b + 480*a*f + 448*a*d + 464*b*f + 160*f^2 + 304*d*f + 288*b^2 + 432*b*d + 144*d^2 + 77869 Time: 0.330 sec (SMT: 0.307 sec)