YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> lbl51(E,B,0,D) [C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = B && C = D] (?,1) 1. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && C >= A && 9 >= C] (?,1) 2. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 3 + C && 9 >= C] (?,1) 3. lbl51(A,B,C,D) -> cut(A,B,C,D) [C >= 0 && A >= 1 + C && 2 + C >= A && 9 >= A && 9 >= C] (?,1) 4. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 10 && A >= 1 + C && 2 + C >= A && 9 >= C] (?,1) 5. cut(A,B,C,D) -> lbl51(E,B,A,D) [8 + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && 17 + -1*A + -1*C >= 0 && C >= 0 && -1 + A + C >= 0 && 2 + -1*A + C >= 0 && 9 + -1*A >= 0 && -1 + A >= 0 && 2 + C >= A && 9 >= A && A >= 1 + C] 6. start0(A,B,C,D) -> start(B,B,D,D) True (1,1) Signature: {(cut,4);(lbl51,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{1,2,3,4},1->{},2->{},3->{5},4->{},5->{1,2,3,4},6->{0}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> lbl51(E,B,0,D) [C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = B && C = D] (1,1) 1. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && C >= A && 9 >= C] (1,1) 2. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 3 + C && 9 >= C] (1,1) 3. lbl51(A,B,C,D) -> cut(A,B,C,D) [C >= 0 && A >= 1 + C && 2 + C >= A && 9 >= A && 9 >= C] (?,1) 4. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 10 && A >= 1 + C && 2 + C >= A && 9 >= C] (1,1) 5. cut(A,B,C,D) -> lbl51(E,B,A,D) [8 + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && 17 + -1*A + -1*C >= 0 && C >= 0 && -1 + A + C >= 0 && 2 + -1*A + C >= 0 && 9 + -1*A >= 0 && -1 + A >= 0 && 2 + C >= A && 9 >= A && A >= 1 + C] 6. start0(A,B,C,D) -> start(B,B,D,D) True (1,1) Signature: {(cut,4);(lbl51,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{1,2,3,4},1->{},2->{},3->{5},4->{},5->{1,2,3,4},6->{0}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,4)] * Step 3: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> lbl51(E,B,0,D) [C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = B && C = D] (1,1) 1. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && C >= A && 9 >= C] (1,1) 2. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 3 + C && 9 >= C] (1,1) 3. lbl51(A,B,C,D) -> cut(A,B,C,D) [C >= 0 && A >= 1 + C && 2 + C >= A && 9 >= A && 9 >= C] (?,1) 4. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 10 && A >= 1 + C && 2 + C >= A && 9 >= C] (1,1) 5. cut(A,B,C,D) -> lbl51(E,B,A,D) [8 + -1*C >= 0 (?,1) && -1 + A + -1*C >= 0 && 17 + -1*A + -1*C >= 0 && C >= 0 && -1 + A + C >= 0 && 2 + -1*A + C >= 0 && 9 + -1*A >= 0 && -1 + A >= 0 && 2 + C >= A && 9 >= A && A >= 1 + C] 6. start0(A,B,C,D) -> start(B,B,D,D) True (1,1) Signature: {(cut,4);(lbl51,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{1,2,3},1->{},2->{},3->{5},4->{},5->{1,2,3,4},6->{0}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(cut) = 9 + -1*x3 p(lbl51) = 9 + -1*x3 p(start) = 9 p(start0) = 9 p(stop) = 9 + -1*x3 Following rules are strictly oriented: [8 + -1*C >= 0 ==> && -1 + A + -1*C >= 0 && 17 + -1*A + -1*C >= 0 && C >= 0 && -1 + A + C >= 0 && 2 + -1*A + C >= 0 && 9 + -1*A >= 0 && -1 + A >= 0 && 2 + C >= A && 9 >= A && A >= 1 + C] cut(A,B,C,D) = 9 + -1*C > 9 + -1*A = lbl51(E,B,A,D) Following rules are weakly oriented: [C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = B && C = D] ==> start(A,B,C,D) = 9 >= 9 = lbl51(E,B,0,D) [C >= 0 && C >= A && 9 >= C] ==> lbl51(A,B,C,D) = 9 + -1*C >= 9 + -1*C = stop(A,B,C,D) [C >= 0 && A >= 3 + C && 9 >= C] ==> lbl51(A,B,C,D) = 9 + -1*C >= 9 + -1*C = stop(A,B,C,D) [C >= 0 && A >= 1 + C && 2 + C >= A && 9 >= A && 9 >= C] ==> lbl51(A,B,C,D) = 9 + -1*C >= 9 + -1*C = cut(A,B,C,D) [C >= 0 && A >= 10 && A >= 1 + C && 2 + C >= A && 9 >= C] ==> lbl51(A,B,C,D) = 9 + -1*C >= 9 + -1*C = stop(A,B,C,D) True ==> start0(A,B,C,D) = 9 >= 9 = start(B,B,D,D) * Step 4: KnowledgePropagation WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> lbl51(E,B,0,D) [C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = B && C = D] (1,1) 1. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && C >= A && 9 >= C] (1,1) 2. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 3 + C && 9 >= C] (1,1) 3. lbl51(A,B,C,D) -> cut(A,B,C,D) [C >= 0 && A >= 1 + C && 2 + C >= A && 9 >= A && 9 >= C] (?,1) 4. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 10 && A >= 1 + C && 2 + C >= A && 9 >= C] (1,1) 5. cut(A,B,C,D) -> lbl51(E,B,A,D) [8 + -1*C >= 0 (9,1) && -1 + A + -1*C >= 0 && 17 + -1*A + -1*C >= 0 && C >= 0 && -1 + A + C >= 0 && 2 + -1*A + C >= 0 && 9 + -1*A >= 0 && -1 + A >= 0 && 2 + C >= A && 9 >= A && A >= 1 + C] 6. start0(A,B,C,D) -> start(B,B,D,D) True (1,1) Signature: {(cut,4);(lbl51,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{1,2,3},1->{},2->{},3->{5},4->{},5->{1,2,3,4},6->{0}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 5: PolyRank WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. start(A,B,C,D) -> lbl51(E,B,0,D) [C + -1*D >= 0 && -1*C + D >= 0 && A + -1*B >= 0 && -1*A + B >= 0 && A = B && C = D] (1,1) 1. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && C >= A && 9 >= C] (1,1) 2. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 3 + C && 9 >= C] (1,1) 3. lbl51(A,B,C,D) -> cut(A,B,C,D) [C >= 0 && A >= 1 + C && 2 + C >= A && 9 >= A && 9 >= C] (10,1) 4. lbl51(A,B,C,D) -> stop(A,B,C,D) [C >= 0 && A >= 10 && A >= 1 + C && 2 + C >= A && 9 >= C] (1,1) 5. cut(A,B,C,D) -> lbl51(E,B,A,D) [8 + -1*C >= 0 (9,1) && -1 + A + -1*C >= 0 && 17 + -1*A + -1*C >= 0 && C >= 0 && -1 + A + C >= 0 && 2 + -1*A + C >= 0 && 9 + -1*A >= 0 && -1 + A >= 0 && 2 + C >= A && 9 >= A && A >= 1 + C] 6. start0(A,B,C,D) -> start(B,B,D,D) True (1,1) Signature: {(cut,4);(lbl51,4);(start,4);(start0,4);(stop,4)} Flow Graph: [0->{1,2,3},1->{},2->{},3->{5},4->{},5->{1,2,3,4},6->{0}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(1))