WORST_CASE(?, O(n^1)) Initial complexity problem: 1: T: (Comp: ?, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: ?, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 /\ 2 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb6in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 /\ Ar_2 >= 3 /\ 5 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ Ar_2 >= 11 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb6in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ Ar_2 >= 8 /\ 10 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb6in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 10, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Testing for reachability in the complexity graph removes the following transitions from problem 1: evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 /\ 2 >= Ar_2 ] evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb6in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 /\ Ar_2 >= 3 /\ 5 >= Ar_2 ] evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ Ar_2 >= 11 ] evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb6in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ Ar_2 >= 8 /\ 10 >= Ar_2 ] evalcomplexbb6in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 10, Ar_4)) We thus obtain the following problem: 2: T: (Comp: ?, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ] (Comp: ?, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ] (Comp: ?, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: ?, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: ?, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 2 produces the following problem: 3: T: (Comp: ?, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ] (Comp: ?, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ] (Comp: ?, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: ?, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: 1, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(evalcomplexbb7in) = 2 Pol(evalcomplexbb8in) = 2 Pol(evalcomplexbb9in) = 2 Pol(evalcomplexbb10in) = 2 Pol(evalcomplexbb1in) = 2 Pol(evalcomplexreturnin) = 1 Pol(evalcomplexstop) = 0 Pol(evalcomplexentryin) = 2 Pol(evalcomplexstart) = 2 Pol(koat_start) = 2 orients all transitions weakly and the transition evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) strictly and produces the following problem: 4: T: (Comp: ?, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ] (Comp: 2, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ] (Comp: ?, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: ?, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: 1, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(evalcomplexbb7in) = 1 Pol(evalcomplexbb8in) = 1 Pol(evalcomplexbb9in) = 1 Pol(evalcomplexbb10in) = 1 Pol(evalcomplexbb1in) = 1 Pol(evalcomplexreturnin) = 0 Pol(evalcomplexstop) = 0 Pol(evalcomplexentryin) = 1 Pol(evalcomplexstart) = 1 Pol(koat_start) = 1 orients all transitions weakly and the transition evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] strictly and produces the following problem: 5: T: (Comp: ?, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ] (Comp: 2, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ] (Comp: 1, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: ?, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: 1, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(evalcomplexbb7in) = -3*V_4 + 82 Pol(evalcomplexbb8in) = -3*V_4 + 84 Pol(evalcomplexbb9in) = -3*V_4 + 83 Pol(evalcomplexbb10in) = -3*V_2 + 88 Pol(evalcomplexbb1in) = -3*V_4 + 83 Pol(evalcomplexreturnin) = -3*V_2 + 88 Pol(evalcomplexstop) = -3*V_2 + 88 Pol(evalcomplexentryin) = -3*V_1 + 88 Pol(evalcomplexstart) = -3*V_1 + 88 Pol(koat_start) = -3*V_1 + 88 orients all transitions weakly and the transition evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] strictly and produces the following problem: 6: T: (Comp: ?, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ] (Comp: 2, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ] (Comp: 1, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: 1, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(evalcomplexbb9in) = 0 Pol(evalcomplexbb10in) = -1 Pol(evalcomplexbb8in) = 1 Pol(evalcomplexbb1in) = 1 Pol(evalcomplexbb7in) = 1 and size complexities S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ]", 0-0) = Ar_0 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ]", 0-1) = Ar_1 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ]", 0-2) = Ar_2 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ]", 0-3) = Ar_3 S("koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ]", 0-4) = Ar_4 S("evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-0) = Ar_0 S("evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-1) = Ar_1 S("evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-2) = Ar_2 S("evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-3) = Ar_3 S("evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-4) = Ar_4 S("evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4))", 0-0) = Ar_1 S("evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4))", 0-1) = Ar_0 S("evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4))", 0-2) = Ar_2 S("evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4))", 0-3) = Ar_3 S("evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4))", 0-4) = Ar_4 S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ]", 0-0) = ? S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ]", 0-1) = ? S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ]", 0-2) = ? S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ]", 0-3) = ? S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ]", 0-4) = ? S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ]", 0-0) = ? S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ]", 0-1) = ? S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ]", 0-2) = ? S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ]", 0-3) = ? S("evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ]", 0-4) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ]", 0-0) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ]", 0-1) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ]", 0-2) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ]", 0-3) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ]", 0-4) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ]", 0-0) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ]", 0-1) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ]", 0-2) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ]", 0-3) = ? S("evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ]", 0-4) = ? S("evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-0) = ? S("evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-1) = ? S("evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-2) = ? S("evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-3) = ? S("evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4))", 0-4) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ]", 0-0) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ]", 0-1) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ]", 0-2) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ]", 0-3) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ]", 0-4) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\\ 7 >= Ar_2 ]", 0-0) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\\ 7 >= Ar_2 ]", 0-1) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\\ 7 >= Ar_2 ]", 0-2) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\\ 7 >= Ar_2 ]", 0-3) = ? S("evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\\ 7 >= Ar_2 ]", 0-4) = ? S("evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4))", 0-0) = ? S("evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4))", 0-1) = ? S("evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4))", 0-2) = ? S("evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4))", 0-3) = ? S("evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4))", 0-4) = ? S("evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4))", 0-0) = ? S("evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4))", 0-1) = ? S("evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4))", 0-2) = ? S("evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4))", 0-3) = ? S("evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4))", 0-4) = ? orients the transitions evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ] evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ] evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ 7 >= Ar_2 ] weakly and the transition evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] strictly and produces the following problem: 7: T: (Comp: ?, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ] (Comp: 2, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ] (Comp: 1, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: 1, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Repeatedly propagating knowledge in problem 7 produces the following problem: 8: T: (Comp: ?, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ Ar_2 >= 6 ] (Comp: 2, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_2 >= Ar_3 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_3 >= Ar_2 + 1 ] (Comp: 1, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: 1, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] start location: koat_start leaf cost: 0 Applied AI with 'oct' on problem 8 to obtain the following invariants: For symbol evalcomplexbb1in: -X_3 + X_4 - 1 >= 0 /\ -X_2 + X_4 >= 0 /\ -X_1 + X_4 - 1 >= 0 /\ -X_1 + X_3 >= 0 /\ -X_2 + 29 >= 0 For symbol evalcomplexbb7in: X_4 - X_5 + 6 >= 0 /\ X_3 - X_5 + 7 >= 0 /\ -X_3 + X_5 - 2 >= 0 /\ -X_1 + X_5 - 2 >= 0 /\ -X_3 + X_4 - 1 >= 0 /\ -X_2 + X_4 >= 0 /\ -X_1 + X_4 - 1 >= 0 /\ -X_1 + X_3 >= 0 /\ -X_2 + 29 >= 0 For symbol evalcomplexbb8in: -X_2 + X_4 >= 0 /\ -X_1 + X_3 >= 0 /\ -X_2 + 29 >= 0 For symbol evalcomplexbb9in: X_3 - X_4 >= 0 /\ -X_2 + X_4 >= 0 /\ -X_2 + X_3 >= 0 /\ -X_1 + X_3 >= 0 /\ -X_2 + 29 >= 0 For symbol evalcomplexreturnin: X_2 - 30 >= 0 This yielded the following problem: 9: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] (Comp: 1, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: 1, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: ?, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ Ar_3 >= Ar_2 + 1 ] (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ Ar_2 >= Ar_3 ] (Comp: 2, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 - 30 >= 0 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ -Ar_2 + Ar_3 - 1 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_3 - 1 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ Ar_2 >= 6 ] (Comp: ?, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ -Ar_2 + Ar_3 - 1 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_3 - 1 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) [ Ar_2 - Ar_3 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_1 + Ar_2 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 ] (Comp: ?, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) [ Ar_3 - Ar_4 + 6 >= 0 /\ Ar_2 - Ar_4 + 7 >= 0 /\ -Ar_2 + Ar_4 - 2 >= 0 /\ -Ar_0 + Ar_4 - 2 >= 0 /\ -Ar_2 + Ar_3 - 1 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_3 - 1 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 ] start location: koat_start leaf cost: 0 A polynomial rank function with Pol(koat_start) = -15*V_1 - 3*V_2 + 537 Pol(evalcomplexstart) = -15*V_1 - 3*V_2 + 537 Pol(evalcomplexentryin) = -15*V_1 - 3*V_2 + 537 Pol(evalcomplexbb10in) = -3*V_1 - 15*V_2 + 537 Pol(evalcomplexbb8in) = -18*V_2 - 3*V_3 + 3*V_4 + 537 Pol(evalcomplexreturnin) = -3*V_1 - 15*V_2 + 537 Pol(evalcomplexbb1in) = -18*V_2 - 3*V_3 + 3*V_4 + 536 Pol(evalcomplexbb9in) = -3*V_3 - 15*V_4 + 537 Pol(evalcomplexstop) = -3*V_1 - 15*V_2 + 537 Pol(evalcomplexbb7in) = -18*V_2 + 3*V_4 - 3*V_5 + 541 orients all transitions weakly and the transitions evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ Ar_3 >= Ar_2 + 1 ] evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) [ Ar_3 - Ar_4 + 6 >= 0 /\ Ar_2 - Ar_4 + 7 >= 0 /\ -Ar_2 + Ar_4 - 2 >= 0 /\ -Ar_0 + Ar_4 - 2 >= 0 /\ -Ar_2 + Ar_3 - 1 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_3 - 1 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 ] evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ -Ar_2 + Ar_3 - 1 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_3 - 1 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ Ar_2 >= 6 ] evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ -Ar_2 + Ar_3 - 1 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_3 - 1 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ 5 >= Ar_2 /\ 7 >= Ar_2 ] strictly and produces the following problem: 10: T: (Comp: 1, Cost: 0) koat_start(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ 0 <= 0 ] (Comp: 1, Cost: 1) evalcomplexstart(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) (Comp: 1, Cost: 1) evalcomplexentryin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_1, Ar_0, Ar_2, Ar_3, Ar_4)) (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_0, Ar_1, Ar_4)) [ 29 >= Ar_1 ] (Comp: 1, Cost: 1) evalcomplexbb10in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 >= 30 ] (Comp: 15*Ar_0 + 3*Ar_1 + 537, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ Ar_3 >= Ar_2 + 1 ] (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb8in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ Ar_2 >= Ar_3 ] (Comp: 2, Cost: 1) evalcomplexreturnin(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexstop(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4)) [ Ar_1 - 30 >= 0 ] (Comp: 15*Ar_0 + 3*Ar_1 + 537, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 7)) [ -Ar_2 + Ar_3 - 1 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_3 - 1 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ Ar_2 >= 6 ] (Comp: 15*Ar_0 + 3*Ar_1 + 537, Cost: 1) evalcomplexbb1in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_2 + 2)) [ -Ar_2 + Ar_3 - 1 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_3 - 1 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 /\ 5 >= Ar_2 /\ 7 >= Ar_2 ] (Comp: 3*Ar_0 + 88, Cost: 1) evalcomplexbb9in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb10in(Ar_2 - 10, Ar_3 + 2, Ar_2, Ar_3, Ar_4)) [ Ar_2 - Ar_3 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_1 + Ar_2 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 ] (Comp: 15*Ar_0 + 3*Ar_1 + 537, Cost: 1) evalcomplexbb7in(Ar_0, Ar_1, Ar_2, Ar_3, Ar_4) -> Com_1(evalcomplexbb8in(Ar_0, Ar_1, Ar_4, Ar_3 + 1, Ar_4)) [ Ar_3 - Ar_4 + 6 >= 0 /\ Ar_2 - Ar_4 + 7 >= 0 /\ -Ar_2 + Ar_4 - 2 >= 0 /\ -Ar_0 + Ar_4 - 2 >= 0 /\ -Ar_2 + Ar_3 - 1 >= 0 /\ -Ar_1 + Ar_3 >= 0 /\ -Ar_0 + Ar_3 - 1 >= 0 /\ -Ar_0 + Ar_2 >= 0 /\ -Ar_1 + 29 >= 0 ] start location: koat_start leaf cost: 0 Complexity upper bound 69*Ar_0 + 12*Ar_1 + 2417 Time: 3.311 sec (SMT: 3.178 sec)