WORST_CASE(?,O(n^2)) * Step 1: UnsatRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,-1 + H,L) [1 >= A && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 4. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [B >= 0 && A >= 2 + B && I = 1 + B && D = 0 && K = 1 + B && H = A] (?,1) 5. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [0 >= 1 + D && B >= 0 && D >= 0 && 1 >= D && A >= 2 + B && I = 1 + B && K = 1 + B && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (?,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 9. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 2 && K = 0 && D = 1 && H = A && I = 1 && B = 0] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{},1->{3},2->{4,5,6,7,8},3->{4,5,6,7,8},4->{},5->{9,10,11},6->{9,10,11},7->{3},8->{4,5,6,7,8},9->{} ,10->{3},11->{4,5,6,7,8},12->{0,1,2}] + Applied Processor: UnsatRules + Details: The following transitions have unsatisfiable constraints and are removed: [5] * Step 2: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,-1 + H,L) [1 >= A && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 4. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [B >= 0 && A >= 2 + B && I = 1 + B && D = 0 && K = 1 + B && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (?,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 9. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 2 && K = 0 && D = 1 && H = A && I = 1 && B = 0] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{},1->{3},2->{4,6,7,8},3->{4,6,7,8},4->{},6->{9,10,11},7->{3},8->{4,6,7,8},9->{},10->{3},11->{4,6,7,8} ,12->{0,1,2}] + 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) (< 0,0,G>, G, .= 0) (< 0,0,H>, H, .= 0) (< 0,0,I>, I, .= 0) (< 0,0,J>, J, .= 0) (< 0,0,K>, 1 + H, .+ 1) (< 0,0,L>, L, .= 0) (< 1,0,A>, A, .= 0) (< 1,0,B>, B, .= 0) (< 1,0,C>, C, .= 0) (< 1,0,D>, 0, .= 0) (< 1,0,E>, E, .= 0) (< 1,0,F>, ?, .?) (< 1,0,G>, G, .= 0) (< 1,0,H>, H, .= 0) (< 1,0,I>, 0, .= 0) (< 1,0,J>, J, .= 0) (< 1,0,K>, 1 + H, .+ 1) (< 1,0,L>, L, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, 0, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, 0, .= 0) (< 2,0,E>, E, .= 0) (< 2,0,F>, F, .= 0) (< 2,0,G>, G, .= 0) (< 2,0,H>, H, .= 0) (< 2,0,I>, 1, .= 1) (< 2,0,J>, J, .= 0) (< 2,0,K>, 1 + H, .+ 1) (< 2,0,L>, L, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, I, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, 1, .= 1) (< 3,0,E>, E, .= 0) (< 3,0,F>, F, .= 0) (< 3,0,G>, G, .= 0) (< 3,0,H>, H, .= 0) (< 3,0,I>, 1 + I, .+ 1) (< 3,0,J>, J, .= 0) (< 3,0,K>, K, .= 0) (< 3,0,L>, L, .= 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) (< 4,0,G>, G, .= 0) (< 4,0,H>, H, .= 0) (< 4,0,I>, I, .= 0) (< 4,0,J>, J, .= 0) (< 4,0,K>, K, .= 0) (< 4,0,L>, L, .= 0) (< 6,0,A>, A, .= 0) (< 6,0,B>, B, .= 0) (< 6,0,C>, C, .= 0) (< 6,0,D>, D, .= 0) (< 6,0,E>, E, .= 0) (< 6,0,F>, F, .= 0) (< 6,0,G>, G, .= 0) (< 6,0,H>, H, .= 0) (< 6,0,I>, I, .= 0) (< 6,0,J>, J, .= 0) (< 6,0,K>, 1 + K, .+ 1) (< 6,0,L>, L, .= 0) (< 7,0,A>, A, .= 0) (< 7,0,B>, B, .= 0) (< 7,0,C>, C, .= 0) (< 7,0,D>, D, .= 0) (< 7,0,E>, E, .= 0) (< 7,0,F>, ?, .?) (< 7,0,G>, G, .= 0) (< 7,0,H>, H, .= 0) (< 7,0,I>, I, .= 0) (< 7,0,J>, J, .= 0) (< 7,0,K>, K, .= 0) (< 7,0,L>, L, .= 0) (< 8,0,A>, A, .= 0) (< 8,0,B>, I, .= 0) (< 8,0,C>, C, .= 0) (< 8,0,D>, D, .= 0) (< 8,0,E>, E, .= 0) (< 8,0,F>, F, .= 0) (< 8,0,G>, G, .= 0) (< 8,0,H>, H, .= 0) (< 8,0,I>, 1 + I, .+ 1) (< 8,0,J>, J, .= 0) (< 8,0,K>, K, .= 0) (< 8,0,L>, L, .= 0) (< 9,0,A>, A, .= 0) (< 9,0,B>, B, .= 0) (< 9,0,C>, C, .= 0) (< 9,0,D>, D, .= 0) (< 9,0,E>, E, .= 0) (< 9,0,F>, F, .= 0) (< 9,0,G>, G, .= 0) (< 9,0,H>, H, .= 0) (< 9,0,I>, I, .= 0) (< 9,0,J>, J, .= 0) (< 9,0,K>, K, .= 0) (< 9,0,L>, L, .= 0) (<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, 0, .= 0) (<10,0,E>, E, .= 0) (<10,0,F>, ?, .?) (<10,0,G>, G, .= 0) (<10,0,H>, H, .= 0) (<10,0,I>, 0, .= 0) (<10,0,J>, J, .= 0) (<10,0,K>, K, .= 0) (<10,0,L>, L, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, 0, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, 0, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, F, .= 0) (<11,0,G>, G, .= 0) (<11,0,H>, H, .= 0) (<11,0,I>, 1, .= 1) (<11,0,J>, J, .= 0) (<11,0,K>, K, .= 0) (<11,0,L>, L, .= 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>, G, .= 0) (<12,0,G>, G, .= 0) (<12,0,H>, A, .= 0) (<12,0,I>, J, .= 0) (<12,0,J>, J, .= 0) (<12,0,K>, L, .= 0) (<12,0,L>, L, .= 0) * Step 3: SizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,-1 + H,L) [1 >= A && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 4. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [B >= 0 && A >= 2 + B && I = 1 + B && D = 0 && K = 1 + B && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (?,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 9. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 2 && K = 0 && D = 1 && H = A && I = 1 && B = 0] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{},1->{3},2->{4,6,7,8},3->{4,6,7,8},4->{},6->{9,10,11},7->{3},8->{4,6,7,8},9->{},10->{3},11->{4,6,7,8} ,12->{0,1,2}] Sizebounds: (< 0,0,A>, ?) (< 0,0,B>, ?) (< 0,0,C>, ?) (< 0,0,D>, ?) (< 0,0,E>, ?) (< 0,0,F>, ?) (< 0,0,G>, ?) (< 0,0,H>, ?) (< 0,0,I>, ?) (< 0,0,J>, ?) (< 0,0,K>, ?) (< 0,0,L>, ?) (< 1,0,A>, ?) (< 1,0,B>, ?) (< 1,0,C>, ?) (< 1,0,D>, ?) (< 1,0,E>, ?) (< 1,0,F>, ?) (< 1,0,G>, ?) (< 1,0,H>, ?) (< 1,0,I>, ?) (< 1,0,J>, ?) (< 1,0,K>, ?) (< 1,0,L>, ?) (< 2,0,A>, ?) (< 2,0,B>, ?) (< 2,0,C>, ?) (< 2,0,D>, ?) (< 2,0,E>, ?) (< 2,0,F>, ?) (< 2,0,G>, ?) (< 2,0,H>, ?) (< 2,0,I>, ?) (< 2,0,J>, ?) (< 2,0,K>, ?) (< 2,0,L>, ?) (< 3,0,A>, ?) (< 3,0,B>, ?) (< 3,0,C>, ?) (< 3,0,D>, ?) (< 3,0,E>, ?) (< 3,0,F>, ?) (< 3,0,G>, ?) (< 3,0,H>, ?) (< 3,0,I>, ?) (< 3,0,J>, ?) (< 3,0,K>, ?) (< 3,0,L>, ?) (< 4,0,A>, ?) (< 4,0,B>, ?) (< 4,0,C>, ?) (< 4,0,D>, ?) (< 4,0,E>, ?) (< 4,0,F>, ?) (< 4,0,G>, ?) (< 4,0,H>, ?) (< 4,0,I>, ?) (< 4,0,J>, ?) (< 4,0,K>, ?) (< 4,0,L>, ?) (< 6,0,A>, ?) (< 6,0,B>, ?) (< 6,0,C>, ?) (< 6,0,D>, ?) (< 6,0,E>, ?) (< 6,0,F>, ?) (< 6,0,G>, ?) (< 6,0,H>, ?) (< 6,0,I>, ?) (< 6,0,J>, ?) (< 6,0,K>, ?) (< 6,0,L>, ?) (< 7,0,A>, ?) (< 7,0,B>, ?) (< 7,0,C>, ?) (< 7,0,D>, ?) (< 7,0,E>, ?) (< 7,0,F>, ?) (< 7,0,G>, ?) (< 7,0,H>, ?) (< 7,0,I>, ?) (< 7,0,J>, ?) (< 7,0,K>, ?) (< 7,0,L>, ?) (< 8,0,A>, ?) (< 8,0,B>, ?) (< 8,0,C>, ?) (< 8,0,D>, ?) (< 8,0,E>, ?) (< 8,0,F>, ?) (< 8,0,G>, ?) (< 8,0,H>, ?) (< 8,0,I>, ?) (< 8,0,J>, ?) (< 8,0,K>, ?) (< 8,0,L>, ?) (< 9,0,A>, ?) (< 9,0,B>, ?) (< 9,0,C>, ?) (< 9,0,D>, ?) (< 9,0,E>, ?) (< 9,0,F>, ?) (< 9,0,G>, ?) (< 9,0,H>, ?) (< 9,0,I>, ?) (< 9,0,J>, ?) (< 9,0,K>, ?) (< 9,0,L>, ?) (<10,0,A>, ?) (<10,0,B>, ?) (<10,0,C>, ?) (<10,0,D>, ?) (<10,0,E>, ?) (<10,0,F>, ?) (<10,0,G>, ?) (<10,0,H>, ?) (<10,0,I>, ?) (<10,0,J>, ?) (<10,0,K>, ?) (<10,0,L>, ?) (<11,0,A>, ?) (<11,0,B>, ?) (<11,0,C>, ?) (<11,0,D>, ?) (<11,0,E>, ?) (<11,0,F>, ?) (<11,0,G>, ?) (<11,0,H>, ?) (<11,0,I>, ?) (<11,0,J>, ?) (<11,0,K>, ?) (<11,0,L>, ?) (<12,0,A>, ?) (<12,0,B>, ?) (<12,0,C>, ?) (<12,0,D>, ?) (<12,0,E>, ?) (<12,0,F>, ?) (<12,0,G>, ?) (<12,0,H>, ?) (<12,0,I>, ?) (<12,0,J>, ?) (<12,0,K>, ?) (<12,0,L>, ?) + 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>, G) (< 0,0,G>, G) (< 0,0,H>, A) (< 0,0,I>, J) (< 0,0,J>, J) (< 0,0,K>, 1 + A) (< 0,0,L>, L) (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, 1) (< 4,0,E>, E) (< 4,0,F>, ?) (< 4,0,G>, G) (< 4,0,H>, A) (< 4,0,I>, ?) (< 4,0,J>, J) (< 4,0,K>, ?) (< 4,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, 1) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, ?) (< 9,0,J>, J) (< 9,0,K>, ?) (< 9,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) * Step 4: UnsatPaths WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,-1 + H,L) [1 >= A && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 4. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [B >= 0 && A >= 2 + B && I = 1 + B && D = 0 && K = 1 + B && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (?,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 9. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 2 && K = 0 && D = 1 && H = A && I = 1 && B = 0] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{},1->{3},2->{4,6,7,8},3->{4,6,7,8},4->{},6->{9,10,11},7->{3},8->{4,6,7,8},9->{},10->{3},11->{4,6,7,8} ,12->{0,1,2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, E) (< 0,0,E>, E) (< 0,0,F>, G) (< 0,0,G>, G) (< 0,0,H>, A) (< 0,0,I>, J) (< 0,0,J>, J) (< 0,0,K>, 1 + A) (< 0,0,L>, L) (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, 1) (< 4,0,E>, E) (< 4,0,F>, ?) (< 4,0,G>, G) (< 4,0,H>, A) (< 4,0,I>, ?) (< 4,0,J>, J) (< 4,0,K>, ?) (< 4,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, 1) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, ?) (< 9,0,J>, J) (< 9,0,K>, ?) (< 9,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,6),(3,4),(11,6)] * Step 5: LeafRules WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,-1 + H,L) [1 >= A && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 4. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [B >= 0 && A >= 2 + B && I = 1 + B && D = 0 && K = 1 + B && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (?,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 9. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 2 && K = 0 && D = 1 && H = A && I = 1 && B = 0] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{},1->{3},2->{4,7,8},3->{6,7,8},4->{},6->{9,10,11},7->{3},8->{4,6,7,8},9->{},10->{3},11->{4,7,8} ,12->{0,1,2}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, C) (< 0,0,C>, C) (< 0,0,D>, E) (< 0,0,E>, E) (< 0,0,F>, G) (< 0,0,G>, G) (< 0,0,H>, A) (< 0,0,I>, J) (< 0,0,J>, J) (< 0,0,K>, 1 + A) (< 0,0,L>, L) (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 4,0,A>, A) (< 4,0,B>, ?) (< 4,0,C>, C) (< 4,0,D>, 1) (< 4,0,E>, E) (< 4,0,F>, ?) (< 4,0,G>, G) (< 4,0,H>, A) (< 4,0,I>, ?) (< 4,0,J>, J) (< 4,0,K>, ?) (< 4,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (< 9,0,A>, A) (< 9,0,B>, ?) (< 9,0,C>, C) (< 9,0,D>, 1) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, ?) (< 9,0,J>, J) (< 9,0,K>, ?) (< 9,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [0,4,9] * Step 6: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (?,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [1->{3},2->{7,8},3->{6,7,8},6->{10,11},7->{3},8->{6,7,8},10->{3},11->{7,8},12->{1,2}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl13) = x2 p(lbl53) = -1 + x11 p(lbl71) = -1 + x11 p(start) = -2 + x8 p(start0) = 1 + x1 The following rules are strictly oriented: [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = B > -1 + K = lbl53(A,0,C,0,E,F,G,H,1,J,K,L) The following rules are weakly oriented: [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] ==> start(A,B,C,D,E,F,G,H,I,J,K,L) = -2 + H >= -2 + H = lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] ==> start(A,B,C,D,E,F,G,H,I,J,K,L) = -2 + H >= -2 + H = lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] ==> lbl71(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + K >= -1 + K = lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + K >= B = lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + K >= -1 + K = lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + K >= -1 + K = lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = B >= -1 + K = lbl71(A,B,C,0,E,M,G,H,0,J,K,L) True ==> start0(A,B,C,D,E,F,G,H,I,J,K,L) = 1 + A >= -2 + A = start(A,C,C,E,E,G,G,A,J,J,L,L) * Step 7: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (?,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (?,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (1 + A,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [1->{3},2->{7,8},3->{6,7,8},6->{10,11},7->{3},8->{6,7,8},10->{3},11->{7,8},12->{1,2}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 8: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (?,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (?,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (1 + A,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [1->{3},2->{7,8},3->{6,7,8},6->{10,11},7->{3},8->{6,7,8},10->{3},11->{7,8},12->{1,2}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl13) = 1 + x1 + x2 + -1*x8 p(lbl53) = x1 + -1*x8 + x11 p(lbl71) = x1 + -1*x8 + x11 p(start) = x1 p(start0) = x1 The following rules are strictly oriented: [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] ==> start(A,B,C,D,E,F,G,H,I,J,K,L) = A > -1 + A = lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] ==> start(A,B,C,D,E,F,G,H,I,J,K,L) = A > -1 + A = lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = 1 + A + B + -1*H > A + -1*H + K = lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = 1 + A + B + -1*H > A + -1*H + K = lbl53(A,0,C,0,E,F,G,H,1,J,K,L) The following rules are weakly oriented: [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] ==> lbl71(A,B,C,D,E,F,G,H,I,J,K,L) = A + -1*H + K >= A + -1*H + K = lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = A + -1*H + K >= 1 + A + B + -1*H = lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = A + -1*H + K >= A + -1*H + K = lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = A + -1*H + K >= A + -1*H + K = lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) True ==> start0(A,B,C,D,E,F,G,H,I,J,K,L) = A >= A = start(A,C,C,E,E,G,G,A,J,J,L,L) * Step 9: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (?,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [1->{3},2->{7,8},3->{6,7,8},6->{10,11},7->{3},8->{6,7,8},10->{3},11->{7,8},12->{1,2}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl13) = x2 p(lbl53) = x11 p(lbl71) = x11 p(start) = -1 + x1 p(start0) = -1 + x1 The following rules are strictly oriented: [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = K > B = lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) The following rules are weakly oriented: [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] ==> start(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A >= -1 + H = lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] ==> start(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A >= -1 + H = lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] ==> lbl71(A,B,C,D,E,F,G,H,I,J,K,L) = K >= K = lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = K >= K = lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = K >= K = lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = B >= K = lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = B >= K = lbl53(A,0,C,0,E,F,G,H,1,J,K,L) True ==> start0(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A >= -1 + A = start(A,C,C,E,E,G,G,A,J,J,L,L) * Step 10: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (1 + A,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [1->{3},2->{7,8},3->{6,7,8},6->{10,11},7->{3},8->{6,7,8},10->{3},11->{7,8},12->{1,2}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [3,7,8,11,10], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl13) = -1 + x1 p(lbl53) = -1 + x1 + -1*x9 p(lbl71) = -2 + x1 + -1*x9 The following rules are strictly oriented: [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A + -1*I > -2 + A + -1*I = lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A > -2 + A = lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A > -2 + A = lbl53(A,0,C,0,E,F,G,H,1,J,K,L) The following rules are weakly oriented: [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] ==> lbl71(A,B,C,D,E,F,G,H,I,J,K,L) = -2 + A + -1*I >= -2 + A + -1*I = lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A + -1*I >= -2 + A + -1*I = lbl71(A,B,C,D,E,M,G,H,I,J,K,L) We use the following global sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) * Step 11: PolyRank WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (1 + A,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (?,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (5 + 4*A + A^2,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [1->{3},2->{7,8},3->{6,7,8},6->{10,11},7->{3},8->{6,7,8},10->{3},11->{7,8},12->{1,2}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [3,7,8,11,10], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl13) = x1 p(lbl53) = x1 + -1*x9 p(lbl71) = -1 + x1 + -1*x9 The following rules are strictly oriented: [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = A + -1*I > -1 + A + -1*I = lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = A > -1 + A = lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] ==> lbl13(A,B,C,D,E,F,G,H,I,J,K,L) = A > -1 + A = lbl53(A,0,C,0,E,F,G,H,1,J,K,L) The following rules are weakly oriented: [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] ==> lbl71(A,B,C,D,E,F,G,H,I,J,K,L) = -1 + A + -1*I >= -1 + A + -1*I = lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] ==> lbl53(A,B,C,D,E,F,G,H,I,J,K,L) = A + -1*I >= -1 + A + -1*I = lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) We use the following global sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) * Step 12: KnowledgePropagation WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (?,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (1 + A,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (2 + 3*A + A^2,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (5 + 4*A + A^2,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [1->{3},2->{7,8},3->{6,7,8},6->{10,11},7->{3},8->{6,7,8},10->{3},11->{7,8},12->{1,2}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 13: LocalSizeboundsProc WORST_CASE(?,O(n^2)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,-1 + H,L) [A >= 2 && B = C && D = E && F = G && H = A && I = J && K = L] (1,1) 3. lbl71(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,1,E,F,G,H,1 + I,J,K,L) [D >= 0 && I >= D && K >= 1 + I && A >= 1 + K && H = A] (3 + 4*A + A^2,1) 6. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl13(A,B,C,D,E,F,G,H,I,J,-1 + K,L) [B >= 0 && A >= 2 + B && D = 1 && I = 1 + B && K = 1 + B && H = A] (1 + A,1) 7. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,D,E,M,G,H,I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (2 + 3*A + A^2,1) 8. lbl53(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,I,C,D,E,F,G,H,1 + I,J,K,L) [K >= 2 + B && B >= 0 && D >= 0 && K >= 1 + B && 1 >= D && A >= 1 + K && I = 1 + B && H = A] (5 + 4*A + A^2,1) 10. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl71(A,B,C,0,E,M,G,H,0,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 11. lbl13(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl53(A,0,C,0,E,F,G,H,1,J,K,L) [B >= 1 && B >= 0 && A >= 2 + B && D = 1 && H = A && K = B && I = 1 + B] (A,1) 12. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,A,J,J,L,L) True (1,1) Signature: {(lbl13,12);(lbl53,12);(lbl71,12);(start,12);(start0,12);(stop,12)} Flow Graph: [1->{3},2->{7,8},3->{6,7,8},6->{10,11},7->{3},8->{6,7,8},10->{3},11->{7,8},12->{1,2}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, C) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, A) (< 1,0,I>, 0) (< 1,0,J>, J) (< 1,0,K>, 1 + A) (< 1,0,L>, L) (< 2,0,A>, A) (< 2,0,B>, 0) (< 2,0,C>, C) (< 2,0,D>, 0) (< 2,0,E>, E) (< 2,0,F>, G) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, 1) (< 2,0,J>, J) (< 2,0,K>, 1 + A) (< 2,0,L>, L) (< 3,0,A>, A) (< 3,0,B>, ?) (< 3,0,C>, C) (< 3,0,D>, 1) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, ?) (< 3,0,J>, J) (< 3,0,K>, A) (< 3,0,L>, L) (< 6,0,A>, A) (< 6,0,B>, ?) (< 6,0,C>, C) (< 6,0,D>, 1) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, ?) (< 6,0,J>, J) (< 6,0,K>, ?) (< 6,0,L>, L) (< 7,0,A>, A) (< 7,0,B>, ?) (< 7,0,C>, C) (< 7,0,D>, 1) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, ?) (< 7,0,J>, J) (< 7,0,K>, A) (< 7,0,L>, L) (< 8,0,A>, A) (< 8,0,B>, ?) (< 8,0,C>, C) (< 8,0,D>, 1) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, ?) (< 8,0,J>, J) (< 8,0,K>, A) (< 8,0,L>, L) (<10,0,A>, A) (<10,0,B>, ?) (<10,0,C>, C) (<10,0,D>, 0) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, 0) (<10,0,J>, J) (<10,0,K>, ?) (<10,0,L>, L) (<11,0,A>, A) (<11,0,B>, 0) (<11,0,C>, C) (<11,0,D>, 0) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, 1) (<11,0,J>, J) (<11,0,K>, ?) (<11,0,L>, L) (<12,0,A>, A) (<12,0,B>, C) (<12,0,C>, C) (<12,0,D>, E) (<12,0,E>, E) (<12,0,F>, G) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, J) (<12,0,J>, J) (<12,0,K>, L) (<12,0,L>, L) + Applied Processor: LocalSizeboundsProc + Details: The problem is already solved. WORST_CASE(?,O(n^2))