YES(?,O(n^1)) * Step 1: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] (?,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (?,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 (?,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A + -1*D >= 0 (?,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{4,5,6,7},2->{8,9,10},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9,10},7->{8,9,10},8->{4,5,6,7},9->{8 ,9,10},10->{8,9,10},11->{0,1,2,3}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,10),(6,10),(8,5),(9,10)] * Step 2: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] (?,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (?,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 (?,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A + -1*D >= 0 (?,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9} ,10->{8,9,10},11->{0,1,2,3}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (1,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [12 + B + -1*D >= 0 (1,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9} ,10->{8,9,10},11->{0,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl151) = 4948 + -126*x1 + 6*x2 + -21*x3 + -42*x4 p(lbl171) = 4948 + -126*x1 + 6*x2 + -21*x3 + -42*x4 p(start) = 4948 + -168*x1 + 6*x2 + -21*x3 p(start0) = 4948 + -168*x1 + -15*x3 p(stop) = 4948 + -126*x1 + 6*x2 + -21*x3 + -42*x4 Following rules are strictly oriented: [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 4948 + -126*A + 6*B + -21*C + -42*D > 4918 + -126*A + 6*B + -21*C + -42*D = lbl151(A,2 + B,C,1 + D) Following rules are weakly oriented: [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 4948 + -168*A + 6*B + -21*C >= 4948 + -126*A + 6*B + -21*C + -42*D = stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 4948 + -168*A + 6*B + -21*C >= 4804 + -126*A + 6*B + -21*C + -42*D = lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] start(A,B,C,D) = 4948 + -168*A + 6*B + -21*C >= 4948 + -126*A + 6*B + -21*C + -42*D = lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] start(A,B,C,D) = 4948 + -168*A + 6*B + -21*C >= 4918 + -126*A + 6*B + -21*C + -42*D = lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 4948 + -126*A + 6*B + -21*C + -42*D >= 4948 + -126*A + 6*B + -21*C + -42*D = stop(A,B,C,D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 4948 + -126*A + 6*B + -21*C + -42*D >= 4804 + -126*A + 6*B + -21*C + -42*D = lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 4948 + -126*A + 6*B + -21*C + -42*D >= 4948 + -126*A + 6*B + -21*C + -42*D = lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 4948 + -126*A + 6*B + -21*C + -42*D >= 4918 + -126*A + 6*B + -21*C + -42*D = lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 4948 + -126*A + 6*B + -21*C + -42*D >= 4804 + -126*A + 6*B + -21*C + -42*D = lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 4948 + -126*A + 6*B + -21*C + -42*D >= 4948 + -126*A + 6*B + -21*C + -42*D = lbl151(A,7 + B,C,1 + D) True ==> start0(A,B,C,D) = 4948 + -168*A + -15*C >= 4948 + -168*A + -15*C = start(A,C,C,A) * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (1,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [12 + B + -1*D >= 0 (1,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 (4948 + 168*A + 15*C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9} ,10->{8,9,10},11->{0,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl151) = 343 + -7*x1 + -1*x3 + -1*x4 p(lbl171) = 342 + -7*x1 + -1*x3 + -1*x4 p(start) = 347 + -7*x1 + -1*x3 + -1*x4 p(start0) = 347 + -8*x1 + -1*x3 p(stop) = 342 + -7*x1 + -1*x3 + -1*x4 Following rules are strictly oriented: [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] start(A,B,C,D) = 347 + -7*A + -1*C + -1*D > 342 + -7*A + -1*C + -1*D = lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] start(A,B,C,D) = 347 + -7*A + -1*C + -1*D > 342 + -7*A + -1*C + -1*D = lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 343 + -7*A + -1*C + -1*D > 342 + -7*A + -1*C + -1*D = lbl151(A,7 + B,C,1 + D) Following rules are weakly oriented: [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 347 + -7*A + -1*C + -1*D >= 342 + -7*A + -1*C + -1*D = stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 347 + -7*A + -1*C + -1*D >= 340 + -7*A + -1*C + -1*D = lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 342 + -7*A + -1*C + -1*D >= 342 + -7*A + -1*C + -1*D = stop(A,B,C,D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 342 + -7*A + -1*C + -1*D >= 340 + -7*A + -1*C + -1*D = lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 342 + -7*A + -1*C + -1*D >= 342 + -7*A + -1*C + -1*D = lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 342 + -7*A + -1*C + -1*D >= 342 + -7*A + -1*C + -1*D = lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 343 + -7*A + -1*C + -1*D >= 340 + -7*A + -1*C + -1*D = lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 343 + -7*A + -1*C + -1*D >= 342 + -7*A + -1*C + -1*D = lbl151(A,2 + B,C,1 + D) True ==> start0(A,B,C,D) = 347 + -8*A + -1*C >= 347 + -8*A + -1*C = start(A,C,C,A) * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (1,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [12 + B + -1*D >= 0 (1,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 (347 + 8*A + C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 (4948 + 168*A + 15*C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9} ,10->{8,9,10},11->{0,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl151) = 436 + -11*x1 + -2*x3 + -1*x4 p(lbl171) = 437 + -11*x1 + -2*x3 + -1*x4 p(start) = 435 + -12*x1 + -2*x3 p(start0) = 435 + -12*x1 + -2*x3 p(stop) = 435 + -11*x1 + -2*x3 + -1*x4 Following rules are strictly oriented: [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 437 + -11*A + -2*C + -1*D > 435 + -11*A + -2*C + -1*D = lbl151(A,2 + B,C,1 + D) Following rules are weakly oriented: [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 435 + -12*A + -2*C >= 435 + -11*A + -2*C + -1*D = stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 435 + -12*A + -2*C >= 435 + -11*A + -2*C + -1*D = lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] start(A,B,C,D) = 435 + -12*A + -2*C >= 435 + -11*A + -2*C + -1*D = lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] start(A,B,C,D) = 435 + -12*A + -2*C >= 435 + -11*A + -2*C + -1*D = lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 437 + -11*A + -2*C + -1*D >= 435 + -11*A + -2*C + -1*D = stop(A,B,C,D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 437 + -11*A + -2*C + -1*D >= 435 + -11*A + -2*C + -1*D = lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 437 + -11*A + -2*C + -1*D >= 435 + -11*A + -2*C + -1*D = lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 436 + -11*A + -2*C + -1*D >= 435 + -11*A + -2*C + -1*D = lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 436 + -11*A + -2*C + -1*D >= 435 + -11*A + -2*C + -1*D = lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 436 + -11*A + -2*C + -1*D >= 435 + -11*A + -2*C + -1*D = lbl151(A,2 + B,C,1 + D) True ==> start0(A,B,C,D) = 435 + -12*A + -2*C >= 435 + -12*A + -2*C = start(A,C,C,A) * Step 6: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (1,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [12 + B + -1*D >= 0 (1,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 (435 + 12*A + 2*C,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 (?,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 (347 + 8*A + C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 (4948 + 168*A + 15*C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9} ,10->{8,9,10},11->{0,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl151) = 9400 + -283*x1 + 2*x2 + -25*x3 + -15*x4 p(lbl171) = 9399 + -283*x1 + -2*x2 + -25*x3 + -11*x4 p(start) = 9513 + -298*x1 + 2*x2 + -29*x3 p(start0) = 9558 + -298*x1 + -27*x3 p(stop) = 9513 + -283*x1 + -2*x2 + -25*x3 + -15*x4 Following rules are strictly oriented: [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 9400 + -283*A + 2*B + -25*C + -15*D > 9397 + -283*A + -2*B + -25*C + -11*D = lbl171(A,-10 + B,C,2 + D) Following rules are weakly oriented: [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 9513 + -298*A + 2*B + -29*C >= 9513 + -283*A + -2*B + -25*C + -15*D = stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 9513 + -298*A + 2*B + -29*C >= 9397 + -283*A + -2*B + -25*C + -11*D = lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] start(A,B,C,D) = 9513 + -298*A + 2*B + -29*C >= 9399 + -283*A + 2*B + -25*C + -15*D = lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] start(A,B,C,D) = 9513 + -298*A + 2*B + -29*C >= 9389 + -283*A + 2*B + -25*C + -15*D = lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 9399 + -283*A + -2*B + -25*C + -11*D >= 9513 + -283*A + -2*B + -25*C + -15*D = stop(A,B,C,D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 9399 + -283*A + -2*B + -25*C + -11*D >= 9397 + -283*A + -2*B + -25*C + -11*D = lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 9399 + -283*A + -2*B + -25*C + -11*D >= 9399 + -283*A + 2*B + -25*C + -15*D = lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 9399 + -283*A + -2*B + -25*C + -11*D >= 9389 + -283*A + 2*B + -25*C + -15*D = lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 9400 + -283*A + 2*B + -25*C + -15*D >= 9399 + -283*A + 2*B + -25*C + -15*D = lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 9400 + -283*A + 2*B + -25*C + -15*D >= 9389 + -283*A + 2*B + -25*C + -15*D = lbl151(A,2 + B,C,1 + D) True ==> start0(A,B,C,D) = 9558 + -298*A + -27*C >= 9513 + -298*A + -27*C = start(A,C,C,A) * Step 7: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (1,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [12 + B + -1*D >= 0 (1,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 (435 + 12*A + 2*C,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 (9558 + 298*A + 27*C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 (347 + 8*A + C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 (4948 + 168*A + 15*C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9} ,10->{8,9,10},11->{0,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl151) = 12692 + -461*x1 + x2 + -1*x3 + -7*x4 p(lbl171) = 12693 + -461*x1 + x2 + -1*x3 + -7*x4 p(start) = 13711 + -472*x1 p(start0) = 13711 + -472*x1 p(stop) = 13563 + -24*x1 + -6*x2 + 6*x3 + -448*x4 Following rules are strictly oriented: [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] start(A,B,C,D) = 13711 + -472*A > 12692 + -461*A + B + -1*C + -7*D = lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] start(A,B,C,D) = 13711 + -472*A > 12687 + -461*A + B + -1*C + -7*D = lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 12693 + -461*A + B + -1*C + -7*D > 12692 + -461*A + B + -1*C + -7*D = lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 12693 + -461*A + B + -1*C + -7*D > 12687 + -461*A + B + -1*C + -7*D = lbl151(A,2 + B,C,1 + D) Following rules are weakly oriented: [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 13711 + -472*A >= 13563 + -24*A + -6*B + 6*C + -448*D = stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 13711 + -472*A >= 12669 + -461*A + B + -1*C + -7*D = lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 12693 + -461*A + B + -1*C + -7*D >= 13563 + -24*A + -6*B + 6*C + -448*D = stop(A,B,C,D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 12693 + -461*A + B + -1*C + -7*D >= 12669 + -461*A + B + -1*C + -7*D = lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 12692 + -461*A + B + -1*C + -7*D >= 12669 + -461*A + B + -1*C + -7*D = lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 12692 + -461*A + B + -1*C + -7*D >= 12692 + -461*A + B + -1*C + -7*D = lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 12692 + -461*A + B + -1*C + -7*D >= 12687 + -461*A + B + -1*C + -7*D = lbl151(A,2 + B,C,1 + D) True ==> start0(A,B,C,D) = 13711 + -472*A >= 13711 + -472*A = start(A,C,C,A) * Step 8: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (1,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [12 + B + -1*D >= 0 (1,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 (?,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 (13711 + 472*A,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 (435 + 12*A + 2*C,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 (9558 + 298*A + 27*C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 (347 + 8*A + C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 (4948 + 168*A + 15*C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9} ,10->{8,9,10},11->{0,1,2,3}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl151) = 2784 + -89*x1 + x2 + -1*x3 + -7*x4 p(lbl171) = 2785 + -89*x1 + x2 + -1*x3 + -7*x4 p(start) = 2784 + -96*x1 p(start0) = 2784 + -96*x1 p(stop) = 2784 + -89*x1 + x2 + -1*x3 + -7*x4 Following rules are strictly oriented: [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 2785 + -89*A + B + -1*C + -7*D > 2761 + -89*A + B + -1*C + -7*D = lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 2785 + -89*A + B + -1*C + -7*D > 2784 + -89*A + B + -1*C + -7*D = lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 2785 + -89*A + B + -1*C + -7*D > 2779 + -89*A + B + -1*C + -7*D = lbl151(A,2 + B,C,1 + D) Following rules are weakly oriented: [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 2784 + -96*A >= 2784 + -89*A + B + -1*C + -7*D = stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 2784 + -96*A >= 2761 + -89*A + B + -1*C + -7*D = lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] start(A,B,C,D) = 2784 + -96*A >= 2784 + -89*A + B + -1*C + -7*D = lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 ==> && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] start(A,B,C,D) = 2784 + -96*A >= 2779 + -89*A + B + -1*C + -7*D = lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 ==> && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] lbl171(A,B,C,D) = 2785 + -89*A + B + -1*C + -7*D >= 2784 + -89*A + B + -1*C + -7*D = stop(A,B,C,D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 2784 + -89*A + B + -1*C + -7*D >= 2761 + -89*A + B + -1*C + -7*D = lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 2784 + -89*A + B + -1*C + -7*D >= 2784 + -89*A + B + -1*C + -7*D = lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 ==> && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] lbl151(A,B,C,D) = 2784 + -89*A + B + -1*C + -7*D >= 2779 + -89*A + B + -1*C + -7*D = lbl151(A,2 + B,C,1 + D) True ==> start0(A,B,C,D) = 2784 + -96*A >= 2784 + -96*A = start(A,C,C,A) * Step 9: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [A + -1*D >= 0 && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && C >= A && 29 >= A && B = C && D = A] (1,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A + -1*D >= 0 (1,1) && -1*A + D >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [12 + B + -1*D >= 0 (1,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 30 && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 5. lbl171(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [12 + B + -1*D >= 0 (2784 + 96*A,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && B >= D && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 6. lbl171(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [12 + B + -1*D >= 0 (13711 + 472*A,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 7. lbl171(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [12 + B + -1*D >= 0 (435 + 12*A + 2*C,1) && -2 + -1*A + D >= 0 && 10 + -1*A + B >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 29 >= D && 29 >= A && B + 5*D >= 5*A + C && C + 7*D >= 24 + 7*A + B && 1674 + 7*B >= 35*A + 7*C + 19*D && 12 + B >= D] 8. lbl151(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [5 + -1*B + D >= 0 (9558 + 298*A + 27*C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && B >= D && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 9. lbl151(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [5 + -1*B + D >= 0 (347 + 8*A + C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && B >= 6 && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 10. lbl151(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [5 + -1*B + D >= 0 (4948 + 168*A + 15*C,1) && -1 + -1*A + D >= 0 && 29 + -1*A >= 0 && D >= 1 + B && 5 >= B && 6*D >= 7 + 5*A + C && B + 5*D >= 7 + 5*A + C && D >= 1 + A && 29 >= A && 203 + B >= 5*A + C + 2*D && 1561 + 2*B >= 35*A + 7*C + 14*D && 23*B + 140*D >= 161 + 140*A + 28*C && 5719 + 23*B >= 140*A + 28*C + 56*D && 5 + D >= B && C + 7*D >= 7*A + B] 11. start0(A,B,C,D) -> start(A,C,C,A) True (1,1) Signature: {(lbl151,4);(lbl171,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{},1->{4,5,6,7},2->{8,9},3->{8,9,10},4->{},5->{4,5,6,7},6->{8,9},7->{8,9,10},8->{4,6,7},9->{8,9} ,10->{8,9,10},11->{0,1,2,3}] + Applied Processor: KnowledgePropagation + Details: The problem is already solved. YES(?,O(n^1))