WORST_CASE(?,O(n^1)) * Step 1: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (?,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (?,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] + Applied Processor: LocalSizeboundsProc + Details: LocalSizebounds generated; rvgraph (< 0,0,A>, A, .= 0) (< 0,0,B>, 0, .= 0) (< 0,0,C>, C, .= 0) (< 0,0,D>, 0, .= 0) (< 0,0,E>, E, .= 0) (< 0,0,F>, F, .= 0) (< 0,0,G>, G, .= 0) (< 0,0,H>, 0, .= 0) (< 0,0,I>, I, .= 0) (< 0,0,J>, J, .= 0) (< 1,0,A>, A, .= 0) (< 1,0,B>, 0, .= 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>, 1, .= 1) (< 1,0,I>, I, .= 0) (< 1,0,J>, J, .= 0) (< 2,0,A>, A, .= 0) (< 2,0,B>, B, .= 0) (< 2,0,C>, C, .= 0) (< 2,0,D>, D, .= 0) (< 2,0,E>, E, .= 0) (< 2,0,F>, F, .= 0) (< 2,0,G>, G, .= 0) (< 2,0,H>, H, .= 0) (< 2,0,I>, I, .= 0) (< 2,0,J>, J, .= 0) (< 3,0,A>, A, .= 0) (< 3,0,B>, B, .= 0) (< 3,0,C>, C, .= 0) (< 3,0,D>, D, .= 0) (< 3,0,E>, E, .= 0) (< 3,0,F>, ?, .?) (< 3,0,G>, G, .= 0) (< 3,0,H>, 1 + H, .+ 1) (< 3,0,I>, I, .= 0) (< 3,0,J>, J, .= 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) (< 5,0,A>, A, .= 0) (< 5,0,B>, B, .= 0) (< 5,0,C>, C, .= 0) (< 5,0,D>, D, .= 0) (< 5,0,E>, E, .= 0) (< 5,0,F>, ?, .?) (< 5,0,G>, G, .= 0) (< 5,0,H>, 1 + H, .+ 1) (< 5,0,I>, I, .= 0) (< 5,0,J>, J, .= 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) (< 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>, 1 + H, .+ 1) (< 7,0,I>, I, .= 0) (< 7,0,J>, J, .= 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) (< 8,0,G>, G, .= 0) (< 8,0,H>, H, .= 0) (< 8,0,I>, I, .= 0) (< 8,0,J>, J, .= 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>, ?, .?) (< 9,0,G>, G, .= 0) (< 9,0,H>, 1 + H, .+ 1) (< 9,0,I>, I, .= 0) (< 9,0,J>, J, .= 0) (<10,0,A>, A, .= 0) (<10,0,B>, B, .= 0) (<10,0,C>, C, .= 0) (<10,0,D>, D, .= 0) (<10,0,E>, E, .= 0) (<10,0,F>, F, .= 0) (<10,0,G>, G, .= 0) (<10,0,H>, H, .= 0) (<10,0,I>, I, .= 0) (<10,0,J>, J, .= 0) (<11,0,A>, A, .= 0) (<11,0,B>, B, .= 0) (<11,0,C>, C, .= 0) (<11,0,D>, D, .= 0) (<11,0,E>, E, .= 0) (<11,0,F>, ?, .?) (<11,0,G>, G, .= 0) (<11,0,H>, 1 + H, .+ 1) (<11,0,I>, I, .= 0) (<11,0,J>, J, .= 0) (<12,0,A>, A, .= 0) (<12,0,B>, B, .= 0) (<12,0,C>, C, .= 0) (<12,0,D>, D, .= 0) (<12,0,E>, E, .= 0) (<12,0,F>, F, .= 0) (<12,0,G>, G, .= 0) (<12,0,H>, H, .= 0) (<12,0,I>, I, .= 0) (<12,0,J>, J, .= 0) (<13,0,A>, A, .= 0) (<13,0,B>, B, .= 0) (<13,0,C>, C, .= 0) (<13,0,D>, D, .= 0) (<13,0,E>, E, .= 0) (<13,0,F>, F, .= 0) (<13,0,G>, G, .= 0) (<13,0,H>, H, .= 0) (<13,0,I>, I, .= 0) (<13,0,J>, J, .= 0) (<14,0,A>, A, .= 0) (<14,0,B>, B, .= 0) (<14,0,C>, C, .= 0) (<14,0,D>, 1 + D, .+ 1) (<14,0,E>, E, .= 0) (<14,0,F>, F, .= 0) (<14,0,G>, G, .= 0) (<14,0,H>, H, .= 0) (<14,0,I>, I, .= 0) (<14,0,J>, J, .= 0) (<15,0,A>, A, .= 0) (<15,0,B>, B, .= 0) (<15,0,C>, C, .= 0) (<15,0,D>, 1 + D, .+ 1) (<15,0,E>, E, .= 0) (<15,0,F>, F, .= 0) (<15,0,G>, G, .= 0) (<15,0,H>, H, .= 0) (<15,0,I>, I, .= 0) (<15,0,J>, J, .= 0) (<16,0,A>, A, .= 0) (<16,0,B>, 1 + B, .+ 1) (<16,0,C>, C, .= 0) (<16,0,D>, D, .= 0) (<16,0,E>, E, .= 0) (<16,0,F>, F, .= 0) (<16,0,G>, G, .= 0) (<16,0,H>, H, .= 0) (<16,0,I>, I, .= 0) (<16,0,J>, J, .= 0) (<17,0,A>, A, .= 0) (<17,0,B>, 1 + B, .+ 1) (<17,0,C>, C, .= 0) (<17,0,D>, D, .= 0) (<17,0,E>, E, .= 0) (<17,0,F>, F, .= 0) (<17,0,G>, G, .= 0) (<17,0,H>, H, .= 0) (<17,0,I>, I, .= 0) (<17,0,J>, J, .= 0) (<18,0,A>, A, .= 0) (<18,0,B>, C, .= 0) (<18,0,C>, C, .= 0) (<18,0,D>, E, .= 0) (<18,0,E>, E, .= 0) (<18,0,F>, G, .= 0) (<18,0,G>, G, .= 0) (<18,0,H>, I, .= 0) (<18,0,I>, I, .= 0) (<18,0,J>, A, .= 0) * Step 2: SizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (?,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (?,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] 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>, ?) (< 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>, ?) (< 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>, ?) (< 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>, ?) (< 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>, ?) (< 5,0,A>, ?) (< 5,0,B>, ?) (< 5,0,C>, ?) (< 5,0,D>, ?) (< 5,0,E>, ?) (< 5,0,F>, ?) (< 5,0,G>, ?) (< 5,0,H>, ?) (< 5,0,I>, ?) (< 5,0,J>, ?) (< 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>, ?) (< 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>, ?) (< 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>, ?) (< 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>, ?) (<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>, ?) (<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>, ?) (<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>, ?) (<13,0,A>, ?) (<13,0,B>, ?) (<13,0,C>, ?) (<13,0,D>, ?) (<13,0,E>, ?) (<13,0,F>, ?) (<13,0,G>, ?) (<13,0,H>, ?) (<13,0,I>, ?) (<13,0,J>, ?) (<14,0,A>, ?) (<14,0,B>, ?) (<14,0,C>, ?) (<14,0,D>, ?) (<14,0,E>, ?) (<14,0,F>, ?) (<14,0,G>, ?) (<14,0,H>, ?) (<14,0,I>, ?) (<14,0,J>, ?) (<15,0,A>, ?) (<15,0,B>, ?) (<15,0,C>, ?) (<15,0,D>, ?) (<15,0,E>, ?) (<15,0,F>, ?) (<15,0,G>, ?) (<15,0,H>, ?) (<15,0,I>, ?) (<15,0,J>, ?) (<16,0,A>, ?) (<16,0,B>, ?) (<16,0,C>, ?) (<16,0,D>, ?) (<16,0,E>, ?) (<16,0,F>, ?) (<16,0,G>, ?) (<16,0,H>, ?) (<16,0,I>, ?) (<16,0,J>, ?) (<17,0,A>, ?) (<17,0,B>, ?) (<17,0,C>, ?) (<17,0,D>, ?) (<17,0,E>, ?) (<17,0,F>, ?) (<17,0,G>, ?) (<17,0,H>, ?) (<17,0,I>, ?) (<17,0,J>, ?) (<18,0,A>, ?) (<18,0,B>, ?) (<18,0,C>, ?) (<18,0,D>, ?) (<18,0,E>, ?) (<18,0,F>, ?) (<18,0,G>, ?) (<18,0,H>, ?) (<18,0,I>, ?) (<18,0,J>, ?) + Applied Processor: SizeboundsProc + Details: Sizebounds computed: (< 0,0,A>, A) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, G) (< 0,0,G>, G) (< 0,0,H>, 0) (< 0,0,I>, I) (< 0,0,J>, A) (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 2,0,A>, A) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, A) (< 2,0,E>, E) (< 2,0,F>, ?) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, I) (< 2,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 4,0,A>, A) (< 4,0,B>, A) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, E) (< 4,0,F>, ?) (< 4,0,G>, G) (< 4,0,H>, A) (< 4,0,I>, I) (< 4,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 6,0,A>, A) (< 6,0,B>, A) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, I) (< 6,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 8,0,A>, A) (< 8,0,B>, A) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, I) (< 8,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<10,0,A>, A) (<10,0,B>, A) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, I) (<10,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) * Step 3: LeafRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [0 >= A && B = C && D = E && F = G && H = I && J = A] (?,1) 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (?,1) 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] (?,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [0->{},1->{12,13,14,15,16,17},2->{},3->{12,13,14,15,16,17},4->{},5->{12,13,14,15,16,17},6->{},7->{12,13,14 ,15,16,17},8->{},9->{12,13,14,15,16,17},10->{},11->{12,13,14,15,16,17},12->{2,3},13->{2,3},14->{4,5},15->{6 ,7},16->{8,9},17->{10,11},18->{0,1}] Sizebounds: (< 0,0,A>, A) (< 0,0,B>, 0) (< 0,0,C>, C) (< 0,0,D>, 0) (< 0,0,E>, E) (< 0,0,F>, G) (< 0,0,G>, G) (< 0,0,H>, 0) (< 0,0,I>, I) (< 0,0,J>, A) (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 2,0,A>, A) (< 2,0,B>, A) (< 2,0,C>, C) (< 2,0,D>, A) (< 2,0,E>, E) (< 2,0,F>, ?) (< 2,0,G>, G) (< 2,0,H>, A) (< 2,0,I>, I) (< 2,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 4,0,A>, A) (< 4,0,B>, A) (< 4,0,C>, C) (< 4,0,D>, A) (< 4,0,E>, E) (< 4,0,F>, ?) (< 4,0,G>, G) (< 4,0,H>, A) (< 4,0,I>, I) (< 4,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 6,0,A>, A) (< 6,0,B>, A) (< 6,0,C>, C) (< 6,0,D>, A) (< 6,0,E>, E) (< 6,0,F>, ?) (< 6,0,G>, G) (< 6,0,H>, A) (< 6,0,I>, I) (< 6,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 8,0,A>, A) (< 8,0,B>, A) (< 8,0,C>, C) (< 8,0,D>, A) (< 8,0,E>, E) (< 8,0,F>, ?) (< 8,0,G>, G) (< 8,0,H>, A) (< 8,0,I>, I) (< 8,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<10,0,A>, A) (<10,0,B>, A) (<10,0,C>, C) (<10,0,D>, A) (<10,0,E>, E) (<10,0,F>, ?) (<10,0,G>, G) (<10,0,H>, A) (<10,0,I>, I) (<10,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: LeafRules + Details: The following transitions are estimated by its predecessors and are removed [0,2,4,6,8,10] * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (?,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (?,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = -8 + 10*x1 + 3*x2 + -1*x4 + -3*x8 p(lbl141) = -6 + 10*x1 + 3*x2 + -1*x4 + -3*x8 p(lbl171) = -8 + 10*x1 + 3*x2 + -1*x4 + -3*x8 p(lbl191) = -8 + 10*x1 + 3*x2 + -1*x4 + -3*x8 p(lbl21) = -5 + 10*x1 + 3*x2 + -1*x4 + -3*x8 p(lbl81) = -5 + 10*x1 + 3*x2 + -1*x4 + -3*x8 p(start) = -8 + 10*x1 p(start0) = -8 + 10*x1 The following rules are strictly oriented: [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -5 + 10*A + 3*B + -1*D + -3*H > -11 + 10*A + 3*B + -1*D + -3*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) The following rules are weakly oriented: [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = -8 + 10*A >= -8 + 10*A = lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -5 + 10*A + 3*B + -1*D + -3*H >= -8 + 10*A + 3*B + -1*D + -3*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -8 + 10*A + 3*B + -1*D + -3*H >= -8 + 10*A + 3*B + -1*D + -3*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -6 + 10*A + 3*B + -1*D + -3*H >= -8 + 10*A + 3*B + -1*D + -3*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = -8 + 10*A + 3*B + -1*D + -3*H >= -8 + 10*A + 3*B + -1*D + -3*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -8 + 10*A + 3*B + -1*D + -3*H >= -8 + 10*A + 3*B + -1*D + -3*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -5 + 10*A + 3*B + -1*D + -3*H >= -5 + 10*A + 3*B + -1*D + -3*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -5 + 10*A + 3*B + -1*D + -3*H >= -5 + 10*A + 3*B + -1*D + -3*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -5 + 10*A + 3*B + -1*D + -3*H >= -9 + 10*A + 3*B + -1*D + -3*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -5 + 10*A + 3*B + -1*D + -3*H >= -5 + 10*A + 3*B + -1*D + -3*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -5 + 10*A + 3*B + -1*D + -3*H >= -5 + 10*A + 3*B + -1*D + -3*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = -8 + 10*A >= -8 + 10*A = start(A,C,C,E,E,G,G,I,I,A) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (?,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (?,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (8 + 10*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (?,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (8 + 10*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = -6 + 8*x1 + -4*x2 + -4*x8 p(lbl141) = -6 + 8*x1 + -4*x2 + -4*x8 p(lbl171) = 8*x1 + -4*x2 + -4*x8 p(lbl191) = -6 + 8*x1 + -4*x2 + -4*x8 p(lbl21) = -2 + 8*x1 + -4*x2 + -4*x8 p(lbl81) = -2 + 8*x1 + -4*x2 + -4*x8 p(start) = 8*x1 p(start0) = 8*x1 The following rules are strictly oriented: [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 8*A + -4*B + -4*H > -4 + 8*A + -4*B + -4*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) The following rules are weakly oriented: [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = 8*A >= -6 + 8*A = lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = -2 + 8*A + -4*B + -4*H >= -6 + 8*A + -4*B + -4*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = -6 + 8*A + -4*B + -4*H >= -6 + 8*A + -4*B + -4*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = -6 + 8*A + -4*B + -4*H >= -6 + 8*A + -4*B + -4*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = 8*A + -4*B + -4*H >= -6 + 8*A + -4*B + -4*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = -6 + 8*A + -4*B + -4*H >= -6 + 8*A + -4*B + -4*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 8*A + -4*B + -4*H >= -2 + 8*A + -4*B + -4*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 8*A + -4*B + -4*H >= -2 + 8*A + -4*B + -4*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 8*A + -4*B + -4*H >= -6 + 8*A + -4*B + -4*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 8*A + -4*B + -4*H >= -6 + 8*A + -4*B + -4*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = -2 + 8*A + -4*B + -4*H >= -2 + 8*A + -4*B + -4*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = 8*A >= 8*A = start(A,C,C,E,E,G,G,I,I,A) * Step 7: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (?,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (8*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (8 + 10*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 8: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (8*A,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (?,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (8*A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (8 + 10*A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = 1 + x1 + -1*x8 p(lbl141) = x1 + -1*x8 p(lbl171) = x1 + -1*x8 p(lbl191) = x1 + -1*x8 p(lbl21) = x1 + -1*x8 p(lbl81) = 1 + x1 + -1*x8 p(start) = x1 p(start0) = x1 The following rules are strictly oriented: [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) The following rules are weakly oriented: [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = A >= A = lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H >= A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H >= A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H >= 1 + A + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = A >= A = start(A,C,C,E,E,G,G,I,I,A) * Step 9: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (?,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (8*A,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 10: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (A,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (8*A,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (?,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = x1 + -1*x8 p(lbl141) = x1 + -1*x8 p(lbl171) = x1 + -1*x8 p(lbl191) = x1 + -1*x8 p(lbl21) = x1 + -1*x8 p(lbl81) = 1 + x1 + -1*x8 p(start) = x1 p(start0) = x1 The following rules are strictly oriented: [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) The following rules are weakly oriented: [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = A >= A = lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H >= A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H >= A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = A >= A = start(A,C,C,E,E,G,G,I,I,A) * Step 11: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (?,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (A,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (8*A,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 12: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (A,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (A,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (8*A,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = x1 + -1*x8 p(lbl141) = x1 + -1*x8 p(lbl171) = x1 + -1*x8 p(lbl191) = x1 + -1*x8 p(lbl21) = x1 + -1*x8 p(lbl81) = 1 + x1 + -1*x8 p(start) = x1 p(start0) = x1 The following rules are strictly oriented: [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) The following rules are weakly oriented: [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = A >= A = lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H >= A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = A >= A = start(A,C,C,E,E,G,G,I,I,A) * Step 13: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (A,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (A,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (8*A,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (?,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(lbl121) = x1 + -1*x8 p(lbl141) = x1 + -1*x8 p(lbl171) = x1 + -1*x8 p(lbl191) = x1 + -1*x8 p(lbl21) = x1 + -1*x8 p(lbl81) = 1 + x1 + -1*x8 p(start) = x1 p(start0) = x1 The following rules are strictly oriented: [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl21(A,B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] ==> lbl81(A,B,C,D,E,F,G,H,I,J) = 1 + A + -1*H > A + -1*H = lbl191(A,-1 + B,C,D,E,F,G,H,I,J) The following rules are weakly oriented: [A >= 1 && B = C && D = E && F = G && H = I && J = A] ==> start(A,B,C,D,E,F,G,H,I,J) = A >= A = lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] ==> lbl21(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] ==> lbl121(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] ==> lbl141(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] ==> lbl171(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] ==> lbl191(A,B,C,D,E,F,G,H,I,J) = A + -1*H >= A + -1*H = lbl81(A,B,C,D,E,K,G,1 + H,I,J) True ==> start0(A,B,C,D,E,F,G,H,I,J) = A >= A = start(A,C,C,E,E,G,G,I,I,A) * Step 14: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (?,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (A,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (A,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (8*A,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 15: LocalSizeboundsProc WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [A >= 1 && B = C && D = E && F = G && H = I && J = A] (1,1) 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] (2*A,1) 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] (A,1) 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] (A,1) 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] (8*A,1) 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] (8 + 10*A,1) 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] (A,1) 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] (A,1) 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] (A,1) 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] (A,1) 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] (A,1) 18. start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True (1,1) Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Flow Graph: [1->{12,13,14,15,16,17},3->{12,13,14,15,16,17},5->{12,13,14,15,16,17},7->{12,13,14,15,16,17},9->{12,13,14 ,15,16,17},11->{12,13,14,15,16,17},12->{3},13->{3},14->{5},15->{7},16->{9},17->{11},18->{1}] Sizebounds: (< 1,0,A>, A) (< 1,0,B>, 0) (< 1,0,C>, C) (< 1,0,D>, 0) (< 1,0,E>, E) (< 1,0,F>, ?) (< 1,0,G>, G) (< 1,0,H>, 1) (< 1,0,I>, I) (< 1,0,J>, A) (< 3,0,A>, A) (< 3,0,B>, A) (< 3,0,C>, C) (< 3,0,D>, A) (< 3,0,E>, E) (< 3,0,F>, ?) (< 3,0,G>, G) (< 3,0,H>, A) (< 3,0,I>, I) (< 3,0,J>, A) (< 5,0,A>, A) (< 5,0,B>, A) (< 5,0,C>, C) (< 5,0,D>, A) (< 5,0,E>, E) (< 5,0,F>, ?) (< 5,0,G>, G) (< 5,0,H>, A) (< 5,0,I>, I) (< 5,0,J>, A) (< 7,0,A>, A) (< 7,0,B>, A) (< 7,0,C>, C) (< 7,0,D>, A) (< 7,0,E>, E) (< 7,0,F>, ?) (< 7,0,G>, G) (< 7,0,H>, A) (< 7,0,I>, I) (< 7,0,J>, A) (< 9,0,A>, A) (< 9,0,B>, A) (< 9,0,C>, C) (< 9,0,D>, A) (< 9,0,E>, E) (< 9,0,F>, ?) (< 9,0,G>, G) (< 9,0,H>, A) (< 9,0,I>, I) (< 9,0,J>, A) (<11,0,A>, A) (<11,0,B>, A) (<11,0,C>, C) (<11,0,D>, A) (<11,0,E>, E) (<11,0,F>, ?) (<11,0,G>, G) (<11,0,H>, A) (<11,0,I>, I) (<11,0,J>, A) (<12,0,A>, A) (<12,0,B>, A) (<12,0,C>, C) (<12,0,D>, A) (<12,0,E>, E) (<12,0,F>, ?) (<12,0,G>, G) (<12,0,H>, A) (<12,0,I>, I) (<12,0,J>, A) (<13,0,A>, A) (<13,0,B>, A) (<13,0,C>, C) (<13,0,D>, A) (<13,0,E>, E) (<13,0,F>, ?) (<13,0,G>, G) (<13,0,H>, A) (<13,0,I>, I) (<13,0,J>, A) (<14,0,A>, A) (<14,0,B>, A) (<14,0,C>, C) (<14,0,D>, A) (<14,0,E>, E) (<14,0,F>, ?) (<14,0,G>, G) (<14,0,H>, A) (<14,0,I>, I) (<14,0,J>, A) (<15,0,A>, A) (<15,0,B>, A) (<15,0,C>, C) (<15,0,D>, A) (<15,0,E>, E) (<15,0,F>, ?) (<15,0,G>, G) (<15,0,H>, A) (<15,0,I>, I) (<15,0,J>, A) (<16,0,A>, A) (<16,0,B>, A) (<16,0,C>, C) (<16,0,D>, A) (<16,0,E>, E) (<16,0,F>, ?) (<16,0,G>, G) (<16,0,H>, A) (<16,0,I>, I) (<16,0,J>, A) (<17,0,A>, A) (<17,0,B>, A) (<17,0,C>, C) (<17,0,D>, A) (<17,0,E>, E) (<17,0,F>, ?) (<17,0,G>, G) (<17,0,H>, A) (<17,0,I>, I) (<17,0,J>, A) (<18,0,A>, A) (<18,0,B>, C) (<18,0,C>, C) (<18,0,D>, E) (<18,0,E>, E) (<18,0,F>, G) (<18,0,G>, G) (<18,0,H>, I) (<18,0,I>, I) (<18,0,J>, A) + Applied Processor: LocalSizeboundsProc + Details: The problem is already solved. WORST_CASE(?,O(n^1))