YES(?,POLY) * Step 1: FromIts WORST_CASE(?,POLY) + 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) [H + -1*I >= 0 (?,1) && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && 0 >= A && B = C && D = E && F = G && H = I && J = A] 1. start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [H + -1*I >= 0 (?,1) && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && A >= 1 && B = C && D = E && F = G && H = I && J = A] 2. lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] 3. lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] 4. lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] 5. lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] 6. lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] 7. lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] 8. lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] 9. lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] 10. lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] 11. lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] 12. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 0 >= 1 + F && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] 13. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && F >= 4 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && J = A] 14. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 0 && J = A] 15. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 1 && J = A] 16. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 2 && J = A] 17. lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 (?,1) && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] 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: FromIts + Details: () * Step 2: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [H + -1*I >= 0 && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && 0 >= A && B = C && D = E && F = G && H = I && J = A] start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [H + -1*I >= 0 && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && A >= 1 && B = C && D = E && F = G && H = I && J = A] lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True Signature: {(lbl121,10);(lbl141,10);(lbl171,10);(lbl191,10);(lbl21,10);(lbl81,10);(start,10);(start0,10);(stop,10)} Rule 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: AddSinks + Details: () * Step 3: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [H + -1*I >= 0 && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && 0 >= A && B = C && D = E && F = G && H = I && J = A] start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [H + -1*I >= 0 && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && A >= 1 && B = C && D = E && F = G && H = I && J = A] lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True Signature: {(exitus616,10) ;(lbl121,10) ;(lbl141,10) ;(lbl171,10) ;(lbl191,10) ;(lbl21,10) ;(lbl81,10) ;(start,10) ;(start0,10) ;(stop,10)} Rule Graph: [0->{24},1->{12,13,14,15,16,17},2->{23},3->{12,13,14,15,16,17},4->{22},5->{12,13,14,15,16,17},6->{21} ,7->{12,13,14,15,16,17},8->{20},9->{12,13,14,15,16,17},10->{19},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: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24] | `- p:[12,3,13,5,14,7,15,9,16,11,17] c: [3,5,7,9,11,12,13,14,15,16,17] * Step 4: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: start(A,B,C,D,E,F,G,H,I,J) -> stop(A,0,C,0,E,F,G,0,I,J) [H + -1*I >= 0 && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && 0 >= A && B = C && D = E && F = G && H = I && J = A] start(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,0,C,0,E,K,G,1,I,J) [H + -1*I >= 0 && -1*H + I >= 0 && F + -1*G >= 0 && -1*F + G >= 0 && D + -1*E >= 0 && -1*D + E >= 0 && B + -1*C >= 0 && -1*B + C >= 0 && A + -1*J >= 0 && -1*A + J >= 0 && A >= 1 && B = C && D = E && F = G && H = I && J = A] lbl21(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 1 && A + D >= 1 + B && A + B >= 1 + D && A >= 1 + B + D && H = A && J = A] lbl21(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 1 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && J = A] lbl121(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= 2 + B && A + B >= D && A >= B + D && H = A && F = 0 && J = A] lbl121(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -1 + -1*F + H >= 0 && -2 + D + H >= 0 && -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1*F >= 0 && -1 + -1*F + J >= 0 && -1 + A + -1*F >= 0 && F >= 0 && -1 + F + J >= 0 && -1 + A + F >= 0 && -1*D + J >= 0 && A + -1*D >= 0 && -2 + D + J >= 0 && -2 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= 2 + B && B + H >= D && H >= B + D && F = 0 && J = A] lbl141(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= B && A + B >= 2 + D && A >= 2 + B + D && H = A && F = 1 && J = A] lbl141(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -1*F + H >= 0 && D + H >= 0 && -2 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 1 + -1*F >= 0 && -1*F + J >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + F + J >= 0 && -2 + A + F >= 0 && -2 + -1*D + J >= 0 && -2 + A + -1*D >= 0 && D + J >= 0 && A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= B && B + H >= 2 + D && H >= 2 + B + D && F = 1 && J = A] lbl171(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 2 && A + D >= B && A + B >= 2 + D && A >= B + D && H = A && F = 2 && J = A] lbl171(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -3 + F + H >= 0 && 1 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -2 + B + H >= 0 && -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 2 + -1*F >= 0 && 1 + -1*F + J >= 0 && 1 + A + -1*F >= 0 && -2 + F >= 0 && -3 + F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1*B + J >= 0 && A + -1*B >= 0 && -2 + B + J >= 0 && -2 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 2 && D + H >= B && B + H >= 2 + D && H >= B + D && F = 2 && J = A] lbl191(A,B,C,D,E,F,G,H,I,J) -> stop(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A + B + D >= 0 && A + D >= 2 + B && A + B >= D && A >= 2 + B + D && H = A && F = 3 && J = A] lbl191(A,B,C,D,E,F,G,H,I,J) -> lbl81(A,B,C,D,E,K,G,1 + H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -4 + F + H >= 0 && 2 + -1*F + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && B + H >= 0 && -2 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && 3 + -1*F >= 0 && 2 + -1*F + J >= 0 && 2 + A + -1*F >= 0 && -3 + F >= 0 && -4 + F + J >= 0 && -4 + A + F >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -2 + -1*B + J >= 0 && -2 + A + -1*B >= 0 && B + J >= 0 && A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && A >= 1 + H && A >= H && B + D + H >= 0 && D + H >= 2 + B && B + H >= D && H >= 2 + B + D && F = 3 && J = A] lbl81(A,B,C,D,E,F,G,H,I,J) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl21(A,B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl121(A,B,C,1 + D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl141(A,B,C,-1 + D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl171(A,1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && 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) -> lbl191(A,-1 + B,C,D,E,F,G,H,I,J) [-1*H + J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -1 + D + H >= 0 && -1 + -1*D + H >= 0 && -1 + B + H >= 0 && -1 + -1*B + H >= 0 && -2 + H + J >= 0 && -2 + A + H >= 0 && -1 + -1*D + J >= 0 && -1 + A + -1*D >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && -1 + -1*B + J >= 0 && -1 + A + -1*B >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1*A + J >= 0 && -1 + A >= 0 && D + H >= 1 + B && B + H >= 1 + D && H >= 1 + B + D && B + D + H >= 1 && A >= H && F = 3 && J = A] start0(A,B,C,D,E,F,G,H,I,J) -> start(A,C,C,E,E,G,G,I,I,A) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True stop(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True Signature: {(exitus616,10) ;(lbl121,10) ;(lbl141,10) ;(lbl171,10) ;(lbl191,10) ;(lbl21,10) ;(lbl81,10) ;(start,10) ;(start0,10) ;(stop,10)} Rule Graph: [0->{24},1->{12,13,14,15,16,17},2->{23},3->{12,13,14,15,16,17},4->{22},5->{12,13,14,15,16,17},6->{21} ,7->{12,13,14,15,16,17},8->{20},9->{12,13,14,15,16,17},10->{19},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}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24] | `- p:[12,3,13,5,14,7,15,9,16,11,17] c: [3,5,7,9,11,12,13,14,15,16,17]) + Applied Processor: AbstractSize Minimize + Details: () * Step 5: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,0.0] start ~> stop [A <= A, B <= 0*K, C <= C, D <= 0*K, E <= E, F <= F, G <= G, H <= 0*K, I <= I, J <= J] start ~> lbl81 [A <= A, B <= 0*K, C <= C, D <= 0*K, E <= E, F <= unknown, G <= G, H <= K, I <= I, J <= J] lbl21 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl21 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl121 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl121 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl141 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl141 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl171 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl171 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl191 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl191 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl121 [A <= A, B <= B, C <= C, D <= H, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl141 [A <= A, B <= B, C <= C, D <= A, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl171 [A <= A, B <= H, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl81 ~> lbl191 [A <= A, B <= A, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] start0 ~> start [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= A] stop ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] stop ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] stop ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] stop ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] stop ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] stop ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.0 <= 2*K + A + B + H + 2*J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl21 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl81 ~> lbl21 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl121 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl81 ~> lbl121 [A <= A, B <= B, C <= C, D <= H, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl141 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= A, I <= I, J <= J] lbl81 ~> lbl141 [A <= A, B <= B, C <= C, D <= A, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl171 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl171 [A <= A, B <= H, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] lbl191 ~> lbl81 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= J, I <= I, J <= J] lbl81 ~> lbl191 [A <= A, B <= A, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Applied Processor: AbstractFlow + Details: () * Step 6: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,0.0] start ~> stop [K ~=> B,K ~=> D,K ~=> H] start ~> lbl81 [K ~=> B,K ~=> D,K ~=> H,huge ~=> F] lbl21 ~> stop [] lbl21 ~> lbl81 [A ~=> H,huge ~=> F] lbl121 ~> stop [] lbl121 ~> lbl81 [A ~=> H,huge ~=> F] lbl141 ~> stop [] lbl141 ~> lbl81 [A ~=> H,huge ~=> F] lbl171 ~> stop [] lbl171 ~> lbl81 [J ~=> H,huge ~=> F] lbl191 ~> stop [] lbl191 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl21 [] lbl81 ~> lbl21 [] lbl81 ~> lbl121 [H ~=> D] lbl81 ~> lbl141 [A ~=> D] lbl81 ~> lbl171 [H ~=> B] lbl81 ~> lbl191 [A ~=> B] start0 ~> start [A ~=> J,C ~=> B,E ~=> D,G ~=> F,I ~=> H] stop ~> exitus616 [] stop ~> exitus616 [] stop ~> exitus616 [] stop ~> exitus616 [] stop ~> exitus616 [] stop ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,H ~+> 0.0,J ~*> 0.0,K ~*> 0.0] lbl81 ~> lbl21 [] lbl21 ~> lbl81 [A ~=> H,huge ~=> F] lbl81 ~> lbl21 [] lbl121 ~> lbl81 [A ~=> H,huge ~=> F] lbl81 ~> lbl121 [H ~=> D] lbl141 ~> lbl81 [A ~=> H,huge ~=> F] lbl81 ~> lbl141 [A ~=> D] lbl171 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl171 [H ~=> B] lbl191 ~> lbl81 [J ~=> H,huge ~=> F] lbl81 ~> lbl191 [A ~=> B] + Applied Processor: Lare + Details: start0 ~> exitus616 [A ~=> B ,A ~=> D ,A ~=> H ,A ~=> J ,G ~=> F ,K ~=> B ,K ~=> D ,K ~=> H ,huge ~=> F ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick ,A ~*> 0.0 ,A ~*> tick ,K ~*> 0.0 ,K ~*> tick] + lbl21> [A ~=> B ,A ~=> D ,A ~=> H ,H ~=> B ,H ~=> D ,J ~=> B ,J ~=> D ,J ~=> H ,huge ~=> F ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,H ~+> 0.0 ,H ~+> tick ,tick ~+> tick ,J ~*> 0.0 ,J ~*> tick ,K ~*> 0.0 ,K ~*> tick] lbl141> [A ~=> B ,A ~=> D ,A ~=> H ,H ~=> B ,H ~=> D ,J ~=> B ,J ~=> D ,J ~=> H ,huge ~=> F ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,H ~+> 0.0 ,H ~+> tick ,tick ~+> tick ,J ~*> 0.0 ,J ~*> tick ,K ~*> 0.0 ,K ~*> tick] lbl191> [A ~=> B ,A ~=> D ,A ~=> H ,H ~=> B ,H ~=> D ,J ~=> B ,J ~=> D ,J ~=> H ,huge ~=> F ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,H ~+> 0.0 ,H ~+> tick ,tick ~+> tick ,J ~*> 0.0 ,J ~*> tick ,K ~*> 0.0 ,K ~*> tick] lbl171> [A ~=> B ,A ~=> D ,A ~=> H ,H ~=> B ,H ~=> D ,J ~=> B ,J ~=> D ,J ~=> H ,huge ~=> F ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,H ~+> 0.0 ,H ~+> tick ,tick ~+> tick ,J ~*> 0.0 ,J ~*> tick ,K ~*> 0.0 ,K ~*> tick] lbl121> [A ~=> B ,A ~=> D ,A ~=> H ,H ~=> B ,H ~=> D ,J ~=> B ,J ~=> D ,J ~=> H ,huge ~=> F ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,H ~+> 0.0 ,H ~+> tick ,tick ~+> tick ,J ~*> 0.0 ,J ~*> tick ,K ~*> 0.0 ,K ~*> tick] YES(?,POLY)