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 >= 30 && B = C && D = A] (?,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [C >= A && 29 >= A && B = C && D = A] (?,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] (?,1) 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (?,1) 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (?,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (?,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (?,1) && 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 >= 30 && B = C && D = A] (?,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [C >= A && 29 >= A && B = C && D = A] (?,1) 2. start(A,B,C,D) -> lbl151(A,7 + B,C,1 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] (?,1) 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (?,1) 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (?,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (?,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (?,1) && 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 >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [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 + C && C >= 6 && 29 >= A && B = C && D = A] (1,1) 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (1,1) 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (1,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (?,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (?,1) && 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) = 1643 + -50*x1 + -6*x3 + -1*x4 p(lbl171) = 1642 + -50*x1 + -6*x3 + -1*x4 p(start) = 1642 + -51*x1 + -6*x3 p(start0) = 1642 + -51*x1 + -6*x3 p(stop) = 1642 + -50*x1 + -6*x3 + -1*x4 Following rules are strictly oriented: [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) = 1643 + -50*A + -6*C + -1*D > 1642 + -50*A + -6*C + -1*D = lbl151(A,2 + B,C,1 + D) Following rules are weakly oriented: [A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 1642 + -51*A + -6*C >= 1642 + -50*A + -6*C + -1*D = stop(A,B,C,D) [C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 1642 + -51*A + -6*C >= 1640 + -50*A + -6*C + -1*D = lbl171(A,-10 + B,C,2 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 1642 + -51*A + -6*C >= 1642 + -50*A + -6*C + -1*D = lbl151(A,7 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 1642 + -51*A + -6*C >= 1642 + -50*A + -6*C + -1*D = lbl151(A,2 + B,C,1 + D) [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) = 1642 + -50*A + -6*C + -1*D >= 1642 + -50*A + -6*C + -1*D = stop(A,B,C,D) [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) = 1642 + -50*A + -6*C + -1*D >= 1640 + -50*A + -6*C + -1*D = lbl171(A,-10 + B,C,2 + D) [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) = 1642 + -50*A + -6*C + -1*D >= 1642 + -50*A + -6*C + -1*D = lbl151(A,7 + B,C,1 + D) [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) = 1642 + -50*A + -6*C + -1*D >= 1642 + -50*A + -6*C + -1*D = lbl151(A,2 + B,C,1 + D) [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) = 1643 + -50*A + -6*C + -1*D >= 1640 + -50*A + -6*C + -1*D = lbl171(A,-10 + B,C,2 + D) [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) = 1643 + -50*A + -6*C + -1*D >= 1642 + -50*A + -6*C + -1*D = lbl151(A,7 + B,C,1 + D) True ==> start0(A,B,C,D) = 1642 + -51*A + -6*C >= 1642 + -51*A + -6*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 >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [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 + C && C >= 6 && 29 >= A && B = C && D = A] (1,1) 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (1,1) 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (1,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (?,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (1642 + 51*A + 6*C,1) && 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) = 3326 + -89*x1 + 2*x2 + -13*x3 + -15*x4 p(lbl171) = 3325 + -89*x1 + 2*x2 + -13*x3 + -15*x4 p(start) = 3347 + -104*x1 + 2*x2 + -13*x3 p(start0) = 3347 + -104*x1 + -11*x3 p(stop) = 3347 + -82*x1 + 3*x2 + -14*x3 + -22*x4 Following rules are strictly oriented: [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) = 3326 + -89*A + 2*B + -13*C + -15*D > 3325 + -89*A + 2*B + -13*C + -15*D = lbl151(A,7 + B,C,1 + D) Following rules are weakly oriented: [A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 3347 + -104*A + 2*B + -13*C >= 3347 + -82*A + 3*B + -14*C + -22*D = stop(A,B,C,D) [C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 3347 + -104*A + 2*B + -13*C >= 3275 + -89*A + 2*B + -13*C + -15*D = lbl171(A,-10 + B,C,2 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 3347 + -104*A + 2*B + -13*C >= 3325 + -89*A + 2*B + -13*C + -15*D = lbl151(A,7 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 3347 + -104*A + 2*B + -13*C >= 3315 + -89*A + 2*B + -13*C + -15*D = lbl151(A,2 + B,C,1 + D) [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) = 3325 + -89*A + 2*B + -13*C + -15*D >= 3347 + -82*A + 3*B + -14*C + -22*D = stop(A,B,C,D) [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) = 3325 + -89*A + 2*B + -13*C + -15*D >= 3275 + -89*A + 2*B + -13*C + -15*D = lbl171(A,-10 + B,C,2 + D) [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) = 3325 + -89*A + 2*B + -13*C + -15*D >= 3325 + -89*A + 2*B + -13*C + -15*D = lbl151(A,7 + B,C,1 + D) [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) = 3325 + -89*A + 2*B + -13*C + -15*D >= 3315 + -89*A + 2*B + -13*C + -15*D = lbl151(A,2 + B,C,1 + D) [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) = 3326 + -89*A + 2*B + -13*C + -15*D >= 3275 + -89*A + 2*B + -13*C + -15*D = lbl171(A,-10 + B,C,2 + D) [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) = 3326 + -89*A + 2*B + -13*C + -15*D >= 3315 + -89*A + 2*B + -13*C + -15*D = lbl151(A,2 + B,C,1 + D) True ==> start0(A,B,C,D) = 3347 + -104*A + -11*C >= 3347 + -104*A + -11*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 >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [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 + C && C >= 6 && 29 >= A && B = C && D = A] (1,1) 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (1,1) 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (1,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (?,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (3347 + 104*A + 11*C,1) && 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) [D >= 1 + B (1642 + 51*A + 6*C,1) && 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) = 1562 + -35*x1 + 2*x2 + -7*x3 + -14*x4 p(lbl171) = 1600 + -35*x1 + 2*x2 + -7*x3 + -14*x4 p(start) = 1562 + -35*x1 + 2*x2 + -7*x3 + -14*x4 p(start0) = 1562 + -49*x1 + -5*x3 p(stop) = 1562 + -35*x1 + 2*x2 + -7*x3 + -14*x4 Following rules are strictly oriented: [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) = 1562 + -35*A + 2*B + -7*C + -14*D > 1552 + -35*A + 2*B + -7*C + -14*D = lbl171(A,-10 + B,C,2 + D) [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) = 1562 + -35*A + 2*B + -7*C + -14*D > 1552 + -35*A + 2*B + -7*C + -14*D = lbl151(A,2 + B,C,1 + D) Following rules are weakly oriented: [A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 1562 + -35*A + 2*B + -7*C + -14*D >= 1562 + -35*A + 2*B + -7*C + -14*D = stop(A,B,C,D) [C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 1562 + -35*A + 2*B + -7*C + -14*D >= 1552 + -35*A + 2*B + -7*C + -14*D = lbl171(A,-10 + B,C,2 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 1562 + -35*A + 2*B + -7*C + -14*D >= 1562 + -35*A + 2*B + -7*C + -14*D = lbl151(A,7 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 1562 + -35*A + 2*B + -7*C + -14*D >= 1552 + -35*A + 2*B + -7*C + -14*D = lbl151(A,2 + B,C,1 + D) [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) = 1600 + -35*A + 2*B + -7*C + -14*D >= 1562 + -35*A + 2*B + -7*C + -14*D = stop(A,B,C,D) [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) = 1600 + -35*A + 2*B + -7*C + -14*D >= 1552 + -35*A + 2*B + -7*C + -14*D = lbl171(A,-10 + B,C,2 + D) [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) = 1600 + -35*A + 2*B + -7*C + -14*D >= 1562 + -35*A + 2*B + -7*C + -14*D = lbl151(A,7 + B,C,1 + D) [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) = 1600 + -35*A + 2*B + -7*C + -14*D >= 1552 + -35*A + 2*B + -7*C + -14*D = lbl151(A,2 + B,C,1 + D) [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) = 1562 + -35*A + 2*B + -7*C + -14*D >= 1562 + -35*A + 2*B + -7*C + -14*D = lbl151(A,7 + B,C,1 + D) True ==> start0(A,B,C,D) = 1562 + -49*A + -5*C >= 1562 + -49*A + -5*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 >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [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 + C && C >= 6 && 29 >= A && B = C && D = A] (1,1) 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (1,1) 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (1,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (?,1) && 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) [D >= 1 + B (?,1) && 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) [B >= D (1562 + 49*A + 5*C,1) && 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) [D >= 1 + B (3347 + 104*A + 11*C,1) && 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) [D >= 1 + B (1642 + 51*A + 6*C,1) && 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) = 2458 + -91*x1 + x3 + -1*x4 p(lbl171) = 2460 + -91*x1 + x3 + -1*x4 p(start) = 2479 + -90*x1 + x2 + -2*x4 p(start0) = 2479 + -92*x1 + x3 p(stop) = 2460 + -91*x1 + x3 + -1*x4 Following rules are strictly oriented: [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) = 2460 + -91*A + C + -1*D > 2457 + -91*A + C + -1*D = lbl151(A,7 + B,C,1 + D) Following rules are weakly oriented: [A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 2479 + -90*A + B + -2*D >= 2460 + -91*A + C + -1*D = stop(A,B,C,D) [C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 2479 + -90*A + B + -2*D >= 2458 + -91*A + C + -1*D = lbl171(A,-10 + B,C,2 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 2479 + -90*A + B + -2*D >= 2457 + -91*A + C + -1*D = lbl151(A,7 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 2479 + -90*A + B + -2*D >= 2457 + -91*A + C + -1*D = lbl151(A,2 + B,C,1 + D) [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) = 2460 + -91*A + C + -1*D >= 2460 + -91*A + C + -1*D = stop(A,B,C,D) [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) = 2460 + -91*A + C + -1*D >= 2458 + -91*A + C + -1*D = lbl171(A,-10 + B,C,2 + D) [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) = 2460 + -91*A + C + -1*D >= 2457 + -91*A + C + -1*D = lbl151(A,2 + B,C,1 + D) [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) = 2458 + -91*A + C + -1*D >= 2458 + -91*A + C + -1*D = lbl171(A,-10 + B,C,2 + D) [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) = 2458 + -91*A + C + -1*D >= 2457 + -91*A + C + -1*D = lbl151(A,7 + B,C,1 + D) [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) = 2458 + -91*A + C + -1*D >= 2457 + -91*A + C + -1*D = lbl151(A,2 + B,C,1 + D) True ==> start0(A,B,C,D) = 2479 + -92*A + C >= 2479 + -92*A + 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 >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [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 + C && C >= 6 && 29 >= A && B = C && D = A] (1,1) 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (1,1) 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (1,1) && 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) [B >= D (?,1) && 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) [D >= 1 + B (2479 + 92*A + C,1) && 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) [D >= 1 + B (?,1) && 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) [B >= D (1562 + 49*A + 5*C,1) && 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) [D >= 1 + B (3347 + 104*A + 11*C,1) && 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) [D >= 1 + B (1642 + 51*A + 6*C,1) && 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) = 2731 + -91*x1 + x3 + -2*x4 p(lbl171) = 2734 + -91*x1 + x3 + -2*x4 p(start) = 2732 + -91*x1 + x3 + -2*x4 p(start0) = 2732 + -93*x1 + x3 p(stop) = 2732 + -91*x1 + x3 + -2*x4 Following rules are strictly oriented: [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) = 2734 + -91*A + C + -2*D > 2730 + -91*A + C + -2*D = lbl171(A,-10 + B,C,2 + D) [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) = 2734 + -91*A + C + -2*D > 2729 + -91*A + C + -2*D = lbl151(A,2 + B,C,1 + D) Following rules are weakly oriented: [A >= 30 && B = C && D = A] ==> start(A,B,C,D) = 2732 + -91*A + C + -2*D >= 2732 + -91*A + C + -2*D = stop(A,B,C,D) [C >= A && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 2732 + -91*A + C + -2*D >= 2730 + -91*A + C + -2*D = lbl171(A,-10 + B,C,2 + D) [A >= 1 + C && C >= 6 && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 2732 + -91*A + C + -2*D >= 2729 + -91*A + C + -2*D = lbl151(A,7 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] ==> start(A,B,C,D) = 2732 + -91*A + C + -2*D >= 2729 + -91*A + C + -2*D = lbl151(A,2 + B,C,1 + D) [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) = 2734 + -91*A + C + -2*D >= 2732 + -91*A + C + -2*D = stop(A,B,C,D) [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) = 2734 + -91*A + C + -2*D >= 2729 + -91*A + C + -2*D = lbl151(A,7 + B,C,1 + D) [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) = 2731 + -91*A + C + -2*D >= 2730 + -91*A + C + -2*D = lbl171(A,-10 + B,C,2 + D) [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) = 2731 + -91*A + C + -2*D >= 2729 + -91*A + C + -2*D = lbl151(A,7 + B,C,1 + D) [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) = 2731 + -91*A + C + -2*D >= 2729 + -91*A + C + -2*D = lbl151(A,2 + B,C,1 + D) True ==> start0(A,B,C,D) = 2732 + -93*A + C >= 2732 + -93*A + C = start(A,C,C,A) * Step 8: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> stop(A,B,C,D) [A >= 30 && B = C && D = A] (1,1) 1. start(A,B,C,D) -> lbl171(A,-10 + B,C,2 + D) [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 + C && C >= 6 && 29 >= A && B = C && D = A] (1,1) 3. start(A,B,C,D) -> lbl151(A,2 + B,C,1 + D) [A >= 1 + C && 5 >= C && 29 >= A && B = C && D = A] (1,1) 4. lbl171(A,B,C,D) -> stop(A,B,C,D) [D >= 30 (1,1) && 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) [B >= D (2732 + 93*A + C,1) && 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) [D >= 1 + B (2479 + 92*A + C,1) && 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) [D >= 1 + B (2732 + 93*A + C,1) && 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) [B >= D (1562 + 49*A + 5*C,1) && 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) [D >= 1 + B (3347 + 104*A + 11*C,1) && 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) [D >= 1 + B (1642 + 51*A + 6*C,1) && 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))