WORST_CASE(?,O(n^1)) * Step 1: UnsatRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (?,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (?,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 5. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [D >= B && 0 >= 1 + A && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 9. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [D >= B && 0 >= 1 + A && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,5,6,7},3->{8,9,10,11},4->{},5->{},6->{4,5,6,7},7->{8,9,10,11},8->{},9->{},10->{4,5,6,7} ,11->{8,9,10,11},12->{0,1,2,3}] + Applied Processor: UnsatRules + Details: The following transitions have unsatisfiable constraints and are removed: [5,9] * Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (?,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (?,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0 ,1,2,3}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, A, .= 0) (< 0,0,B>, B, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, D, .= 0) (< 0,0,E>, E, .= 0) (< 0,0,F>, F, .= 0) (< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, D, .= 0) (< 1,0,E>, E, .= 0) (< 1,0,F>, F, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, 1 + D + F, .* 1) (< 2,0,E>, E, .= 0) (< 2,0,F>, F, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, 1 + B + F, .* 1) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0) (< 3,0,E>, E, .= 0) (< 3,0,F>, F, .= 0) (< 4,0,A>, A, .= 0) (< 4,0,B>, B, .= 0) (< 4,0,C>, C, .= 0) (< 4,0,D>, D, .= 0) (< 4,0,E>, E, .= 0) (< 4,0,F>, F, .= 0) (< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, 1 + D + F, .* 1) (< 6,0,E>, E, .= 0) (< 6,0,F>, F, .= 0) (< 7,0,A>, A, .= 0) (< 7,0,B>, 1 + B + C + F, .* 1) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, F, .= 0) (< 8,0,A>, A, .= 0) (< 8,0,B>, B, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 8,0,F>, F, .= 0) (<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, 1 + D + F, .* 1) (<10,0,E>, E, .= 0) (<10,0,F>, F, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, 1 + B + F, .* 1) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, F, .= 0) (<12,0,A>, A, .= 0) (<12,0,B>, C, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, E, .= 0) (<12,0,E>, E, .= 0) (<12,0,F>, A, .= 0) * Step 3: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (?,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (?,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0 ,1,2,3}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, E) (< 0,0,E>, E) (< 0,0,F>, A) (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, E) (< 1,0,E>, E) (< 1,0,F>, A) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, A) (< 4,0,A>, A) (< 4,0,B>, C + E) (< 4,0,C>, C) (< 4,0,D>, 1 + A + E) (< 4,0,E>, E) (< 4,0,F>, A) (< 6,0,A>, A) (< 6,0,B>, E) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, A) (< 7,0,A>, A) (< 7,0,B>, 2 + E) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, A) (< 8,0,A>, A) (< 8,0,B>, 2 + A + C + E) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, A) (<10,0,A>, A) (<10,0,B>, E) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, A) (<11,0,A>, A) (<11,0,B>, 2 + E) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, A) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, A) * Step 4: LeafRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [0 >= 1 + A && B = C && D = E && F = A] (?,1) 1. start(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [A >= 0 && C >= 1 + E && B = C && D = E && F = A] (?,1) 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 4. lbl91(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && B >= C && A >= 0 && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 8. lbl101(A,B,C,D,E,F) -> stop(A,B,C,D,E,F) [B >= 1 + D && E >= D && A >= 0 && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [0->{},1->{},2->{4,6,7},3->{8,10,11},4->{},6->{4,6,7},7->{8,10,11},8->{},10->{4,6,7},11->{8,10,11},12->{0 ,1,2,3}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, E) (< 0,0,E>, E) (< 0,0,F>, A) (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, E) (< 1,0,E>, E) (< 1,0,F>, A) (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, A) (< 4,0,A>, A) (< 4,0,B>, C + E) (< 4,0,C>, C) (< 4,0,D>, 1 + A + E) (< 4,0,E>, E) (< 4,0,F>, A) (< 6,0,A>, A) (< 6,0,B>, E) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, A) (< 7,0,A>, A) (< 7,0,B>, 2 + E) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, A) (< 8,0,A>, A) (< 8,0,B>, 2 + A + C + E) (< 8,0,C>, C) (< 8,0,D>, E) (< 8,0,E>, E) (< 8,0,F>, A) (<10,0,A>, A) (<10,0,B>, E) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, A) (<11,0,A>, A) (<11,0,B>, 2 + E) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, A) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, A) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [0,1,4,8] * Step 5: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}] Sizebounds: (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, A) (< 6,0,A>, A) (< 6,0,B>, E) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, A) (< 7,0,A>, A) (< 7,0,B>, 2 + E) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, A) (<10,0,A>, A) (<10,0,B>, E) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, A) (<11,0,A>, A) (<11,0,B>, 2 + E) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, A) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl101) = 1 + -1*x2 + x5 p(lbl91) = -1*x2 + x5 p(start) = -1*x2 + x5 p(start0) = -1*x3 + x5 The following rules are strictly oriented: [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + -1*B + E > -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) The following rules are weakly oriented: [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + E >= -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*B + E >= -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*B + E >= -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = -1*B + E >= -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + -1*B + E >= -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) True ==> start0(A,B,C,D,E,F) = -1*C + E >= -1*C + E = start(A,C,C,E,E,A) * Step 6: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (?,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}] Sizebounds: (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, A) (< 6,0,A>, A) (< 6,0,B>, E) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, A) (< 7,0,A>, A) (< 7,0,B>, 2 + E) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, A) (<10,0,A>, A) (<10,0,B>, E) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, A) (<11,0,A>, A) (<11,0,B>, 2 + E) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, A) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, A) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 7: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (?,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}] Sizebounds: (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, A) (< 6,0,A>, A) (< 6,0,B>, E) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, A) (< 7,0,A>, A) (< 7,0,B>, 2 + E) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, A) (<10,0,A>, A) (<10,0,B>, E) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, A) (<11,0,A>, A) (<11,0,B>, 2 + E) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, A) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl101) = 1 + -1*x3 + x4 p(lbl91) = 1 + -1*x3 + x4 p(start) = 1 + -1*x3 + x4 p(start0) = 1 + -1*x3 + x5 The following rules are strictly oriented: [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = 1 + -1*C + D > -1*C + D + -1*F = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + -1*C + D > -1*C + D + -1*F = lbl91(A,B,C,-1 + D + -1*F,E,F) The following rules are weakly oriented: [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = 1 + -1*C + D >= 1 + -1*C + D = lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = 1 + -1*C + D >= -1*C + D + -1*F = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = 1 + -1*C + D >= 1 + -1*C + D = lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + -1*C + D >= 1 + -1*C + D = lbl101(A,1 + B + F,C,D,E,F) True ==> start0(A,B,C,D,E,F) = 1 + -1*C + E >= 1 + -1*C + E = start(A,C,C,E,E,A) * Step 8: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (1 + C + E,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}] Sizebounds: (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, A) (< 6,0,A>, A) (< 6,0,B>, E) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, A) (< 7,0,A>, A) (< 7,0,B>, 2 + E) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, A) (<10,0,A>, A) (<10,0,B>, E) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, A) (<11,0,A>, A) (<11,0,B>, 2 + E) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, A) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl101) = 1 + -1*x2 + x5 p(lbl91) = 1 + -1*x1 + -1*x2 + x5 p(start) = 1 + -1*x3 + x5 p(start0) = 1 + -1*x3 + x5 The following rules are strictly oriented: [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = 1 + -1*C + E > -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = 1 + -1*A + -1*B + E > -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + -1*B + E > -1*B + E + -1*F = lbl101(A,1 + B + F,C,D,E,F) The following rules are weakly oriented: [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = 1 + -1*C + E >= 1 + -1*A + -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = 1 + -1*A + -1*B + E >= 1 + -1*A + -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = 1 + -1*B + E >= 1 + -1*A + -1*B + E = lbl91(A,B,C,-1 + D + -1*F,E,F) True ==> start0(A,B,C,D,E,F) = 1 + -1*C + E >= 1 + -1*C + E = start(A,C,C,E,E,A) * Step 9: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (?,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (1 + C + E,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (1 + C + E,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}] Sizebounds: (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, A) (< 6,0,A>, A) (< 6,0,B>, E) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, A) (< 7,0,A>, A) (< 7,0,B>, 2 + E) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, A) (<10,0,A>, A) (<10,0,B>, E) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, A) (<11,0,A>, A) (<11,0,B>, 2 + E) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, A) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl101) = -1*x3 + x4 p(lbl91) = 1 + -1*x3 + x4 p(start) = -1*x3 + x4 p(start0) = -1*x3 + x5 The following rules are strictly oriented: [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = 1 + -1*C + D > -1*C + D + -1*F = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] ==> lbl91(A,B,C,D,E,F) = 1 + -1*C + D > -1*C + D = lbl101(A,1 + B + F,C,D,E,F) The following rules are weakly oriented: [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*C + D >= -1*C + D + -1*F = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] ==> start(A,B,C,D,E,F) = -1*C + D >= -1*C + D = lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = -1*C + D >= -1*C + D + -1*F = lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] ==> lbl101(A,B,C,D,E,F) = -1*C + D >= -1*C + D = lbl101(A,1 + B + F,C,D,E,F) True ==> start0(A,B,C,D,E,F) = -1*C + E >= -1*C + E = start(A,C,C,E,E,A) * Step 10: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 2. start(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 3. start(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && E >= C && B = C && D = E && F = A] (1,1) 6. lbl91(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (C + E,1) 7. lbl91(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && B >= C && 1 + A + D >= B && E >= 1 + A + D && F = A] (C + E,1) 10. lbl101(A,B,C,D,E,F) -> lbl91(A,B,C,-1 + D + -1*F,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (1 + C + E,1) 11. lbl101(A,B,C,D,E,F) -> lbl101(A,1 + B + F,C,D,E,F) [A >= 0 && D >= B && E >= D && B >= 1 + A + C && 1 + A + D >= B && F = A] (C + E,1) 12. start0(A,B,C,D,E,F) -> start(A,C,C,E,E,A) True (1,1) Signature: {(lbl101,6);(lbl91,6);(start,6);(start0,6);(stop,6)} Flow Graph: [2->{6,7},3->{10,11},6->{6,7},7->{10,11},10->{6,7},11->{10,11},12->{2,3}] Sizebounds: (< 2,0,A>, A) (< 2,0,B>, C) (< 2,0,C>, C) (< 2,0,D>, 1 + A + E) (< 2,0,E>, E) (< 2,0,F>, A) (< 3,0,A>, A) (< 3,0,B>, 1 + A + C) (< 3,0,C>, C) (< 3,0,D>, E) (< 3,0,E>, E) (< 3,0,F>, A) (< 6,0,A>, A) (< 6,0,B>, E) (< 6,0,C>, C) (< 6,0,D>, E) (< 6,0,E>, E) (< 6,0,F>, A) (< 7,0,A>, A) (< 7,0,B>, 2 + E) (< 7,0,C>, C) (< 7,0,D>, E) (< 7,0,E>, E) (< 7,0,F>, A) (<10,0,A>, A) (<10,0,B>, E) (<10,0,C>, C) (<10,0,D>, E) (<10,0,E>, E) (<10,0,F>, A) (<11,0,A>, A) (<11,0,B>, 2 + E) (<11,0,C>, C) (<11,0,D>, E) (<11,0,E>, E) (<11,0,F>, A) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, A) + Applied Processor: KnowledgePropagation + Details: The problem is already solved. WORST_CASE(?,O(n^1))