YES(?, 174*a + 162*b + 36*a*b + 12*b^2 + 24*a^2 + 151) Initial complexity problem: 1: T: (1, 1) eval1(a, b, c, d) -> eval2(a - 1, b, c, d) [ a >= 2 ] (1, 1) eval1(a, b, c, d) -> eval2(a, b - 1, c, d) [ 1 >= a ] (?, 1) eval2(a, b, c, d) -> eval3(a, b, a, 2*a) [ b >= 2 ] (?, 1) eval3(a, b, c, d) -> eval4(a, b, c, d) [ b >= d /\ b >= d + 1 ] (?, 1) eval3(a, b, c, d) -> eval4(a, b, c, d + 1) [ b >= d /\ b >= d + 1 ] (?, 1) eval3(a, b, c, d) -> eval3(a, b, d, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, c, d) -> eval3(a, b, d + 1, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, c, d) -> eval4(a, b, c, d) [ b = d ] (?, 1) eval3(a, b, c, d) -> eval3(a, b, d, 2*d) [ d >= 1 /\ b = d ] (?, 1) eval4(a, b, c, d) -> eval2(a - 1, b, c, d) [ a >= 2 /\ a >= 1 /\ b >= 2 ] (?, 1) eval4(a, b, c, d) -> eval2(a, b - 1, c, d) [ b >= 2 /\ a = 1 ] start location: eval1 leaf cost: 0 Slicing away variables that do not contribute to conditions from problem 1 leaves variables [a, b, d]. We thus obtain the following problem: 2: T: (?, 1) eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\ a = 1 ] (?, 1) eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\ a >= 1 /\ b >= 2 ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d) [ d >= 1 /\ b = d ] (?, 1) eval3(a, b, d) -> eval4(a, b, d) [ b = d ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\ b >= d + 1 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\ b >= d + 1 ] (?, 1) eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ] (1, 1) eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ] (1, 1) eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ] start location: eval1 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 2 produces the following problem: 3: T: (?, 1) eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\ a = 1 ] (?, 1) eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\ a >= 1 /\ b >= 2 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d) [ b = d ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\ b >= d + 1 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\ b >= d + 1 ] (?, 1) eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ] (1, 1) eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ] (1, 1) eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ] start location: eval1 leaf cost: 1 A polynomial rank function with Pol(eval4) = 3*V_1 + 3*V_2 - 1 Pol(eval2) = 3*V_1 + 3*V_2 + 1 Pol(eval3) = 3*V_1 + 3*V_2 Pol(eval1) = 3*V_1 + 3*V_2 - 2 orients all transitions weakly and the transitions eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\ a = 1 ] eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\ a >= 1 /\ b >= 2 ] strictly and produces the following problem: 4: T: (3*a + 3*b + 2, 1) eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\ a = 1 ] (3*a + 3*b + 2, 1) eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\ a >= 1 /\ b >= 2 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d) [ b = d ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\ b >= d + 1 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\ b >= d + 1 ] (?, 1) eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ] (1, 1) eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ] (1, 1) eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ] start location: eval1 leaf cost: 1 Repeatedly propagating knowledge in problem 4 produces the following problem: 5: T: (3*a + 3*b + 2, 1) eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\ a = 1 ] (3*a + 3*b + 2, 1) eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\ a >= 1 /\ b >= 2 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d) [ b = d ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\ b >= d + 1 ] (?, 1) eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\ b >= d + 1 ] (6*a + 6*b + 6, 1) eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ] (1, 1) eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ] (1, 1) eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ] start location: eval1 leaf cost: 1 A polynomial rank function with Pol(eval3) = 1 Pol(eval4) = 0 and size complexities S("eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ]", 0-0) = a S("eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ]", 0-1) = b S("eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ]", 0-2) = d S("eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ]", 0-0) = a S("eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ]", 0-1) = b + 1 S("eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ]", 0-2) = d S("eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ]", 0-0) = a + 1 S("eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ]", 0-1) = b + 1 S("eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ]", 0-2) = 2*a + 8 S("eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\\ b >= d + 1 ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\\ b >= d + 1 ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\\ b >= d + 1 ]", 0-2) = ? S("eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\\ b >= d + 1 ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\\ b >= d + 1 ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\\ b >= d + 1 ]", 0-2) = ? S("eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-2) = ? S("eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-2) = ? S("eval3(a, b, d) -> eval4(a, b, d) [ b = d ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval4(a, b, d) [ b = d ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval4(a, b, d) [ b = d ]", 0-2) = ? S("eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\\ a >= 1 /\\ b >= 2 ]", 0-0) = a + 1 S("eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\\ a >= 1 /\\ b >= 2 ]", 0-1) = b + 1 S("eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\\ a >= 1 /\\ b >= 2 ]", 0-2) = ? S("eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\\ a = 1 ]", 0-0) = 1 S("eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\\ a = 1 ]", 0-1) = b + 1 S("eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\\ a = 1 ]", 0-2) = ? orients the transitions eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\ b >= d + 1 ] eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\ b >= d + 1 ] eval3(a, b, d) -> eval4(a, b, d) [ b = d ] eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] weakly and the transitions eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\ b >= d + 1 ] eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\ b >= d + 1 ] eval3(a, b, d) -> eval4(a, b, d) [ b = d ] strictly and produces the following problem: 6: T: (3*a + 3*b + 2, 1) eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\ a = 1 ] (3*a + 3*b + 2, 1) eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\ a >= 1 /\ b >= 2 ] (6*a + 6*b + 6, 1) eval3(a, b, d) -> eval4(a, b, d) [ b = d ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (?, 1) eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (6*a + 6*b + 6, 1) eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\ b >= d + 1 ] (6*a + 6*b + 6, 1) eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\ b >= d + 1 ] (6*a + 6*b + 6, 1) eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ] (1, 1) eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ] (1, 1) eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ] start location: eval1 leaf cost: 1 A polynomial rank function with Pol(eval3) = V_2 - V_3 + 1 and size complexities S("eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ]", 0-0) = a S("eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ]", 0-1) = b S("eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ]", 0-2) = d S("eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ]", 0-0) = a S("eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ]", 0-1) = b + 1 S("eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ]", 0-2) = d S("eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ]", 0-0) = a + 1 S("eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ]", 0-1) = b + 1 S("eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ]", 0-2) = 2*a + 8 S("eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\\ b >= d + 1 ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\\ b >= d + 1 ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\\ b >= d + 1 ]", 0-2) = ? S("eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\\ b >= d + 1 ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\\ b >= d + 1 ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\\ b >= d + 1 ]", 0-2) = ? S("eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-2) = ? S("eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\\ b >= d + 1 /\\ d >= 1 ]", 0-2) = ? S("eval3(a, b, d) -> eval4(a, b, d) [ b = d ]", 0-0) = a + 1 S("eval3(a, b, d) -> eval4(a, b, d) [ b = d ]", 0-1) = b + 1 S("eval3(a, b, d) -> eval4(a, b, d) [ b = d ]", 0-2) = ? S("eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\\ a >= 1 /\\ b >= 2 ]", 0-0) = a + 1 S("eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\\ a >= 1 /\\ b >= 2 ]", 0-1) = b + 1 S("eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\\ a >= 1 /\\ b >= 2 ]", 0-2) = ? S("eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\\ a = 1 ]", 0-0) = 1 S("eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\\ a = 1 ]", 0-1) = b + 1 S("eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\\ a = 1 ]", 0-2) = ? orients the transitions eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] weakly and the transitions eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] strictly and produces the following problem: 7: T: (3*a + 3*b + 2, 1) eval4(a, b, d) -> eval2(a, b - 1, d) [ b >= 2 /\ a = 1 ] (3*a + 3*b + 2, 1) eval4(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 /\ a >= 1 /\ b >= 2 ] (6*a + 6*b + 6, 1) eval3(a, b, d) -> eval4(a, b, d) [ b = d ] (18*a*b + 6*b^2 + 12*a^2 + 66*b + 72*a + 60, 1) eval3(a, b, d) -> eval3(a, b, 2*d + 2) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (18*a*b + 6*b^2 + 12*a^2 + 66*b + 72*a + 60, 1) eval3(a, b, d) -> eval3(a, b, 2*d) [ b >= d /\ b >= d + 1 /\ d >= 1 ] (6*a + 6*b + 6, 1) eval3(a, b, d) -> eval4(a, b, d + 1) [ b >= d /\ b >= d + 1 ] (6*a + 6*b + 6, 1) eval3(a, b, d) -> eval4(a, b, d) [ b >= d /\ b >= d + 1 ] (6*a + 6*b + 6, 1) eval2(a, b, d) -> eval3(a, b, 2*a) [ b >= 2 ] (1, 1) eval1(a, b, d) -> eval2(a, b - 1, d) [ 1 >= a ] (1, 1) eval1(a, b, d) -> eval2(a - 1, b, d) [ a >= 2 ] start location: eval1 leaf cost: 1 Complexity upper bound 174*a + 162*b + 36*a*b + 12*b^2 + 24*a^2 + 151 Time: 0.648 sec (SMT: 0.617 sec)