YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] 3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] 4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] 5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] 6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] 7. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] 8. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [1 + -1*H >= 0 (?,1) && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + F && F >= 1 + J && E >= 1 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] 9. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [1 + -1*H >= 0 (?,1) && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + J && E >= 1 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] 10. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && E >= 1 + H && F >= A && A + C >= 1 + F && E >= H && H >= 1 && J = F && L = A && D = E && B = C] 11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && A + C >= 1 + F && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] 12. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && C >= 1 + J && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] 13. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && J >= C && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] 14. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && E >= 1 && C >= 1 + J && J >= A && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] Signature: {(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{1,2,3,4,5,6,7},1->{8,9},2->{10,11},3->{12,13,14},4->{},5->{},6->{},7->{},8->{8,9},9->{10,11},10->{10 ,11},11->{12,13,14},12->{12,13,14},13->{},14->{10,11}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,14),(11,12),(12,14)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True (1,1) 1. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] 2. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] 3. start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] 4. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] 5. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] 6. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] 7. start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] 8. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [1 + -1*H >= 0 (?,1) && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + F && F >= 1 + J && E >= 1 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] 9. lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [1 + -1*H >= 0 (?,1) && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + J && E >= 1 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] 10. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && E >= 1 + H && F >= A && A + C >= 1 + F && E >= H && H >= 1 && J = F && L = A && D = E && B = C] 11. lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && A + C >= 1 + F && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] 12. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && C >= 1 + J && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] 13. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && J >= C && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] 14. lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E + -1*H >= 0 (?,1) && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && E >= 1 && C >= 1 + J && J >= A && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] Signature: {(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)} Flow Graph: [0->{1,2,3,4,5,6,7},1->{8,9},2->{10,11},3->{12,13},4->{},5->{},6->{},7->{},8->{8,9},9->{10,11},10->{10,11} ,11->{13,14},12->{12,13},13->{},14->{10,11}] + Applied Processor: FromIts + Details: () * Step 3: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: start0(A,B,C,D,E,F,G,H,I,J,K,L) -> start(A,C,C,E,E,G,G,I,I,K,K,A) True start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,0,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] start(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] start(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111(A,B,C,D,E,1 + F,G,H,I,J,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + F && F >= 1 + J && E >= 1 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] lbl111(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,F,G,H,I,F,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + J && E >= 1 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && E >= 1 + H && F >= A && A + C >= 1 + F && E >= H && H >= 1 && J = F && L = A && D = E && B = C] lbl121(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,H,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && A + C >= 1 + F && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131(A,B,C,D,E,F,G,0,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && C >= 1 + J && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> stop(A,B,C,D,E,F,G,H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && J >= C && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl131(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121(A,B,C,D,E,J,G,1,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && E >= 1 && C >= 1 + J && J >= A && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] Signature: {(lbl111,12);(lbl121,12);(lbl131,12);(start,12);(start0,12);(stop,12)} Rule Graph: [0->{1,2,3,4,5,6,7},1->{8,9},2->{10,11},3->{12,13},4->{},5->{},6->{},7->{},8->{8,9},9->{10,11},10->{10,11} ,11->{13,14},12->{12,13},13->{},14->{10,11}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.1(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.2(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.3(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.4(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.5(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.6(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.7(A,C,C,E,E,G,G,I,I,K,K,A) True start.1(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.8(A,B,C,D,E,1,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] start.1(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.9(A,B,C,D,E,1,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] start.2(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,0,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] start.2(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,0,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] start.3(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.12(A,B,C,D,E,F,G,0,I,1,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] start.3(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.13(A,B,C,D,E,F,G,0,I,1,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] start.4(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] start.5(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] start.6(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] start.7(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] lbl111.8(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.8(A,B,C,D,E,1 + F,G,H,I,J,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + F && F >= 1 + J && E >= 1 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] lbl111.8(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.9(A,B,C,D,E,1 + F,G,H,I,J,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + F && F >= 1 + J && E >= 1 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] lbl111.9(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,F,G,H,I,F,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + J && E >= 1 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] lbl111.9(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,F,G,H,I,F,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + J && E >= 1 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] lbl121.10(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && E >= 1 + H && F >= A && A + C >= 1 + F && E >= H && H >= 1 && J = F && L = A && D = E && B = C] lbl121.10(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && E >= 1 + H && F >= A && A + C >= 1 + F && E >= H && H >= 1 && J = F && L = A && D = E && B = C] lbl121.11(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.13(A,B,C,D,E,F,G,H,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && A + C >= 1 + F && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] lbl121.11(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.14(A,B,C,D,E,F,G,H,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && A + C >= 1 + F && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] lbl131.12(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.12(A,B,C,D,E,F,G,0,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && C >= 1 + J && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] lbl131.12(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.13(A,B,C,D,E,F,G,0,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && C >= 1 + J && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] lbl131.13(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && J >= C && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl131.14(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,J,G,1,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && E >= 1 && C >= 1 + J && J >= A && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl131.14(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,J,G,1,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && E >= 1 && C >= 1 + J && J >= A && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] Signature: {(lbl111.8,12) ;(lbl111.9,12) ;(lbl121.10,12) ;(lbl121.11,12) ;(lbl131.12,12) ;(lbl131.13,12) ;(lbl131.14,12) ;(start.1,12) ;(start.2,12) ;(start.3,12) ;(start.4,12) ;(start.5,12) ;(start.6,12) ;(start.7,12) ;(start0.0,12) ;(stop.15,12)} Rule Graph: [0->{7,8},1->{9,10},2->{11,12},3->{13},4->{14},5->{15},6->{16},7->{17,18},8->{19,20},9->{21,22},10->{23 ,24},11->{25,26},12->{27},13->{},14->{},15->{},16->{},17->{17,18},18->{19,20},19->{21,22},20->{23,24} ,21->{21,22},22->{23,24},23->{27},24->{28,29},25->{25,26},26->{27},27->{},28->{21,22},29->{23,24}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.1(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.2(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.3(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.4(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.5(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.6(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.7(A,C,C,E,E,G,G,I,I,K,K,A) True start.1(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.8(A,B,C,D,E,1,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] start.1(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.9(A,B,C,D,E,1,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] start.2(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,0,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] start.2(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,0,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] start.3(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.12(A,B,C,D,E,F,G,0,I,1,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] start.3(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.13(A,B,C,D,E,F,G,0,I,1,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] start.4(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] start.5(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] start.6(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] start.7(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] lbl111.8(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.8(A,B,C,D,E,1 + F,G,H,I,J,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + F && F >= 1 + J && E >= 1 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] lbl111.8(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.9(A,B,C,D,E,1 + F,G,H,I,J,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + F && F >= 1 + J && E >= 1 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] lbl111.9(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,F,G,H,I,F,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + J && E >= 1 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] lbl111.9(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,F,G,H,I,F,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + J && E >= 1 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] lbl121.10(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && E >= 1 + H && F >= A && A + C >= 1 + F && E >= H && H >= 1 && J = F && L = A && D = E && B = C] lbl121.10(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && E >= 1 + H && F >= A && A + C >= 1 + F && E >= H && H >= 1 && J = F && L = A && D = E && B = C] lbl121.11(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.13(A,B,C,D,E,F,G,H,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && A + C >= 1 + F && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] lbl121.11(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.14(A,B,C,D,E,F,G,H,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && A + C >= 1 + F && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] lbl131.12(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.12(A,B,C,D,E,F,G,0,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && C >= 1 + J && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] lbl131.12(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.13(A,B,C,D,E,F,G,0,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && C >= 1 + J && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] lbl131.13(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && J >= C && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl131.14(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,J,G,1,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && E >= 1 && C >= 1 + J && J >= A && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl131.14(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,J,G,1,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && E >= 1 && C >= 1 + J && J >= A && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True Signature: {(exitus616,12) ;(lbl111.8,12) ;(lbl111.9,12) ;(lbl121.10,12) ;(lbl121.11,12) ;(lbl131.12,12) ;(lbl131.13,12) ;(lbl131.14,12) ;(start.1,12) ;(start.2,12) ;(start.3,12) ;(start.4,12) ;(start.5,12) ;(start.6,12) ;(start.7,12) ;(start0.0,12) ;(stop.15,12)} Rule Graph: [0->{7,8},1->{9,10},2->{11,12},3->{13},4->{14},5->{15},6->{16},7->{17,18},8->{19,20},9->{21,22},10->{23 ,24},11->{25,26},12->{27},13->{33},14->{32},15->{31},16->{30},17->{17,18},18->{19,20},19->{21,22},20->{23 ,24},21->{21,22},22->{23,24},23->{27},24->{28,29},25->{25,26},26->{27},27->{34,35,36,37,38,39,40,41},28->{21 ,22},29->{23,24}] + 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,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41] | +- p:[25] c: [25] | +- p:[17] c: [17] | `- p:[21,28,24,22,29] c: [22,24,28,29] | `- p:[21] c: [21] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.1(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.2(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.3(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.4(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.5(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.6(A,C,C,E,E,G,G,I,I,K,K,A) True start0.0(A,B,C,D,E,F,G,H,I,J,K,L) -> start.7(A,C,C,E,E,G,G,I,I,K,K,A) True start.1(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.8(A,B,C,D,E,1,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] start.1(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.9(A,B,C,D,E,1,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 1 && E >= 1 && C >= 1 && B = C && D = E && F = G && H = I && J = K && L = A] start.2(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,0,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] start.2(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,0,G,1,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && E >= 1 && C >= 1 && L = 0 && B = C && D = E && F = G && H = I && J = K && A = 0] start.3(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.12(A,B,C,D,E,F,G,0,I,1,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] start.3(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.13(A,B,C,D,E,F,G,0,I,1,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && C >= 1 && D = 0 && B = C && E = 0 && F = G && H = I && J = K && L = A] start.4(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,0,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 0 && E >= 0 && B = 0 && C = 0 && D = E && F = G && H = I && J = K && L = A] start.5(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + C && B = C && D = E && F = G && H = I && J = K && L = A] start.6(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + E && B = C && D = E && F = G && H = I && J = K && L = A] start.7(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [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*L >= 0 && -1*A + L >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 0 >= 1 + A && B = C && D = E && F = G && H = I && J = K && L = A] lbl111.8(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.8(A,B,C,D,E,1 + F,G,H,I,J,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + F && F >= 1 + J && E >= 1 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] lbl111.8(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl111.9(A,B,C,D,E,1 + F,G,H,I,J,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + F && F >= 1 + J && E >= 1 && A >= F && C >= 1 + J && H = 1 && L = A && D = E && B = C] lbl111.9(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,F,G,H,I,F,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + J && E >= 1 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] lbl111.9(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,F,G,H,I,F,K,L) [1 + -1*H >= 0 && F + -1*H >= 0 && E + -1*H >= 0 && D + -1*H >= 0 && C + -1*H >= 0 && B + -1*H >= 0 && -1*H + L >= 0 && 1 + -1*H + J >= 0 && 1 + -1*H + -1*J >= 0 && A + -1*H >= 0 && -1 + H >= 0 && -2 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -2 + H + L >= 0 && -1 + H + J >= 0 && -1 + H + -1*J >= 0 && -2 + A + H >= 0 && -1*F + L >= 0 && A + -1*F >= 0 && -1 + F >= 0 && -2 + E + F >= 0 && -2 + D + F >= 0 && -2 + C + F >= 0 && -2 + B + F >= 0 && -2 + F + L >= 0 && -1 + F + J >= 0 && -1 + F + -1*J >= 0 && -2 + A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -2 + E + L >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && -2 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -2 + D + L >= 0 && -1 + D + J >= 0 && -1 + D + -1*J >= 0 && -2 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -2 + C + L >= 0 && -1 + C + J >= 0 && -1 + C + -1*J >= 0 && -2 + A + C >= 0 && -1 + B >= 0 && -2 + B + L >= 0 && -1 + B + J >= 0 && -1 + B + -1*J >= 0 && -2 + A + B >= 0 && A + -1*L >= 0 && -1 + L >= 0 && -1 + J + L >= 0 && -1 + -1*J + L >= 0 && -2 + A + L >= 0 && -1*A + L >= 0 && -1*J >= 0 && -1 + A + -1*J >= 0 && J >= 0 && -1 + A + J >= 0 && -1 + A >= 0 && A >= 1 + J && E >= 1 && C >= 1 + J && F = A && H = 1 && L = A && D = E && B = C] lbl121.10(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && E >= 1 + H && F >= A && A + C >= 1 + F && E >= H && H >= 1 && J = F && L = A && D = E && B = C] lbl121.10(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,J,G,1 + H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && E >= 1 + H && F >= A && A + C >= 1 + F && E >= H && H >= 1 && J = F && L = A && D = E && B = C] lbl121.11(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.13(A,B,C,D,E,F,G,H,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && A + C >= 1 + F && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] lbl121.11(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.14(A,B,C,D,E,F,G,H,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && -1 + H >= 0 && -1 + F + H >= 0 && -2 + E + H >= 0 && -2 + D + H >= 0 && -2 + C + H >= 0 && -2 + B + H >= 0 && -1 + H + L >= 0 && -1 + H + J >= 0 && -1 + A + H >= 0 && -1*F + J >= 0 && F >= 0 && -1 + E + F >= 0 && -1 + D + F >= 0 && -1 + C + F >= 0 && -1 + B + F >= 0 && F + L >= 0 && F + -1*L >= 0 && F + J >= 0 && F + -1*J >= 0 && A + F >= 0 && -1*A + F >= 0 && D + -1*E >= 0 && -1 + E >= 0 && -2 + D + E >= 0 && -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + E + L >= 0 && -1 + E + J >= 0 && -1 + A + E >= 0 && -1 + D >= 0 && -2 + C + D >= 0 && -2 + B + D >= 0 && -1 + D + L >= 0 && -1 + D + J >= 0 && -1 + A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -1 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -1 + B + J >= 0 && -1 + A + B >= 0 && J + -1*L >= 0 && A + -1*L >= 0 && L >= 0 && J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && J >= 0 && A + J >= 0 && -1*A + J >= 0 && A >= 0 && A + C >= 1 + F && F >= A && E >= 1 && H = E && J = F && L = A && D = E && B = C] lbl131.12(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.12(A,B,C,D,E,F,G,0,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && C >= 1 + J && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] lbl131.12(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl131.13(A,B,C,D,E,F,G,0,I,1 + J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && C >= 1 + J && C >= 1 && A + C >= J && J >= 1 && H = 0 && D = 0 && L = A && E = 0 && B = C] lbl131.13(A,B,C,D,E,F,G,H,I,J,K,L) -> stop.15(A,B,C,D,E,F,G,H,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && J >= C && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl131.14(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.10(A,B,C,D,E,J,G,1,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && E >= 1 && C >= 1 + J && J >= A && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] lbl131.14(A,B,C,D,E,F,G,H,I,J,K,L) -> lbl121.11(A,B,C,D,E,J,G,1,I,J,K,L) [E + -1*H >= 0 && D + -1*H >= 0 && H >= 0 && E + H >= 0 && -1*E + H >= 0 && D + H >= 0 && -1*D + H >= 0 && -1 + C + H >= 0 && -1 + B + H >= 0 && H + L >= 0 && -1 + H + J >= 0 && A + H >= 0 && D + -1*E >= 0 && E >= 0 && D + E >= 0 && -1*D + E >= 0 && -1 + C + E >= 0 && -1 + B + E >= 0 && E + L >= 0 && -1 + E + J >= 0 && A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && D + L >= 0 && -1 + D + J >= 0 && A + D >= 0 && B + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1*B + C >= 0 && -1 + C + L >= 0 && -2 + C + J >= 0 && -1 + A + C >= 0 && -1 + B >= 0 && -1 + B + L >= 0 && -2 + B + J >= 0 && -1 + A + B >= 0 && A + -1*L >= 0 && L >= 0 && -1 + J + L >= 0 && A + L >= 0 && -1*A + L >= 0 && -1 + J >= 0 && -1 + A + J >= 0 && A >= 0 && E >= 1 && C >= 1 + J && J >= A && C >= 1 && A + C >= J && J >= 1 && H = E && L = A && D = E && B = C] stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True stop.15(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True Signature: {(exitus616,12) ;(lbl111.8,12) ;(lbl111.9,12) ;(lbl121.10,12) ;(lbl121.11,12) ;(lbl131.12,12) ;(lbl131.13,12) ;(lbl131.14,12) ;(start.1,12) ;(start.2,12) ;(start.3,12) ;(start.4,12) ;(start.5,12) ;(start.6,12) ;(start.7,12) ;(start0.0,12) ;(stop.15,12)} Rule Graph: [0->{7,8},1->{9,10},2->{11,12},3->{13},4->{14},5->{15},6->{16},7->{17,18},8->{19,20},9->{21,22},10->{23 ,24},11->{25,26},12->{27},13->{33},14->{32},15->{31},16->{30},17->{17,18},18->{19,20},19->{21,22},20->{23 ,24},21->{21,22},22->{23,24},23->{27},24->{28,29},25->{25,26},26->{27},27->{34,35,36,37,38,39,40,41},28->{21 ,22},29->{23,24}] ,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,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41] | +- p:[25] c: [25] | +- p:[17] c: [17] | `- p:[21,28,24,22,29] c: [22,24,28,29] | `- p:[21] c: [21]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,K,L,0.0,0.1,0.2,0.2.0] start0.0 ~> start.1 [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= K, K <= K, L <= A] start0.0 ~> start.2 [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= K, K <= K, L <= A] start0.0 ~> start.3 [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= K, K <= K, L <= A] start0.0 ~> start.4 [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= K, K <= K, L <= A] start0.0 ~> start.5 [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= K, K <= K, L <= A] start0.0 ~> start.6 [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= K, K <= K, L <= A] start0.0 ~> start.7 [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= K, K <= K, L <= A] start.1 ~> lbl111.8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= G, H <= K, I <= I, J <= 0*K, K <= K, L <= L] start.1 ~> lbl111.9 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K, G <= G, H <= K, I <= I, J <= 0*K, K <= K, L <= L] start.2 ~> lbl121.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= 0*K, G <= G, H <= K, I <= I, J <= 0*K, K <= K, L <= L] start.2 ~> lbl121.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= 0*K, G <= G, H <= K, I <= I, J <= 0*K, K <= K, L <= L] start.3 ~> lbl131.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= I, J <= K, K <= K, L <= L] start.3 ~> lbl131.13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= I, J <= K, K <= K, L <= L] start.4 ~> stop.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= K, L <= L] start.5 ~> stop.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] start.6 ~> stop.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] start.7 ~> stop.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] lbl111.8 ~> lbl111.8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= L, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] lbl111.8 ~> lbl111.9 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= L, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] lbl111.9 ~> lbl121.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= F, K <= K, L <= L] lbl111.9 ~> lbl121.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= F, K <= K, L <= L] lbl121.10 ~> lbl121.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= J, G <= G, H <= E, I <= I, J <= J, K <= K, L <= L] lbl121.10 ~> lbl121.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= J, G <= G, H <= E, I <= I, J <= J, K <= K, L <= L] lbl121.11 ~> lbl131.13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= B + L, K <= K, L <= L] lbl121.11 ~> lbl131.14 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= B + L, K <= K, L <= L] lbl131.12 ~> lbl131.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= I, J <= C, K <= K, L <= L] lbl131.12 ~> lbl131.13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= I, J <= C, K <= K, L <= L] lbl131.13 ~> stop.15 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] lbl131.14 ~> lbl121.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= J, G <= G, H <= K, I <= I, J <= J, K <= K, L <= L] lbl131.14 ~> lbl121.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= J, G <= G, H <= K, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] stop.15 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] + Loop: [0.0 <= A + C + J] lbl131.12 ~> lbl131.12 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= I, J <= C, K <= K, L <= L] + Loop: [0.1 <= F + L] lbl111.8 ~> lbl111.8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= L, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] + Loop: [0.2 <= 2*K + C + J + L] lbl121.10 ~> lbl121.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= J, G <= G, H <= E, I <= I, J <= J, K <= K, L <= L] lbl131.14 ~> lbl121.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= J, G <= G, H <= K, I <= I, J <= J, K <= K, L <= L] lbl121.11 ~> lbl131.14 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= B + L, K <= K, L <= L] lbl121.10 ~> lbl121.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= J, G <= G, H <= E, I <= I, J <= J, K <= K, L <= L] lbl131.14 ~> lbl121.11 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= J, G <= G, H <= K, I <= I, J <= J, K <= K, L <= L] + Loop: [0.2.0 <= E + H] lbl121.10 ~> lbl121.10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= J, G <= G, H <= E, I <= I, J <= J, K <= K, L <= L] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,K,L,0.0,0.1,0.2,0.2.0] start0.0 ~> start.1 [A ~=> L,C ~=> B,E ~=> D,G ~=> F,I ~=> H,K ~=> J] start0.0 ~> start.2 [A ~=> L,C ~=> B,E ~=> D,G ~=> F,I ~=> H,K ~=> J] start0.0 ~> start.3 [A ~=> L,C ~=> B,E ~=> D,G ~=> F,I ~=> H,K ~=> J] start0.0 ~> start.4 [A ~=> L,C ~=> B,E ~=> D,G ~=> F,I ~=> H,K ~=> J] start0.0 ~> start.5 [A ~=> L,C ~=> B,E ~=> D,G ~=> F,I ~=> H,K ~=> J] start0.0 ~> start.6 [A ~=> L,C ~=> B,E ~=> D,G ~=> F,I ~=> H,K ~=> J] start0.0 ~> start.7 [A ~=> L,C ~=> B,E ~=> D,G ~=> F,I ~=> H,K ~=> J] start.1 ~> lbl111.8 [K ~=> F,K ~=> H,K ~=> J] start.1 ~> lbl111.9 [K ~=> F,K ~=> H,K ~=> J] start.2 ~> lbl121.10 [K ~=> F,K ~=> H,K ~=> J] start.2 ~> lbl121.11 [K ~=> F,K ~=> H,K ~=> J] start.3 ~> lbl131.12 [K ~=> H,K ~=> J] start.3 ~> lbl131.13 [K ~=> H,K ~=> J] start.4 ~> stop.15 [K ~=> J] start.5 ~> stop.15 [] start.6 ~> stop.15 [] start.7 ~> stop.15 [] lbl111.8 ~> lbl111.8 [L ~=> F] lbl111.8 ~> lbl111.9 [L ~=> F] lbl111.9 ~> lbl121.10 [F ~=> J] lbl111.9 ~> lbl121.11 [F ~=> J] lbl121.10 ~> lbl121.10 [E ~=> H,J ~=> F] lbl121.10 ~> lbl121.11 [E ~=> H,J ~=> F] lbl121.11 ~> lbl131.13 [B ~+> J,L ~+> J] lbl121.11 ~> lbl131.14 [B ~+> J,L ~+> J] lbl131.12 ~> lbl131.12 [C ~=> J,K ~=> H] lbl131.12 ~> lbl131.13 [C ~=> J,K ~=> H] lbl131.13 ~> stop.15 [] lbl131.14 ~> lbl121.10 [J ~=> F,K ~=> H] lbl131.14 ~> lbl121.11 [J ~=> F,K ~=> H] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] stop.15 ~> exitus616 [] + Loop: [A ~+> 0.0,C ~+> 0.0,J ~+> 0.0] lbl131.12 ~> lbl131.12 [C ~=> J,K ~=> H] + Loop: [F ~+> 0.1,L ~+> 0.1] lbl111.8 ~> lbl111.8 [L ~=> F] + Loop: [C ~+> 0.2,J ~+> 0.2,L ~+> 0.2,K ~*> 0.2] lbl121.10 ~> lbl121.10 [E ~=> H,J ~=> F] lbl131.14 ~> lbl121.10 [J ~=> F,K ~=> H] lbl121.11 ~> lbl131.14 [B ~+> J,L ~+> J] lbl121.10 ~> lbl121.11 [E ~=> H,J ~=> F] lbl131.14 ~> lbl121.11 [J ~=> F,K ~=> H] + Loop: [E ~+> 0.2.0,H ~+> 0.2.0] lbl121.10 ~> lbl121.10 [E ~=> H,J ~=> F] + Applied Processor: Lare + Details: start0.0 ~> exitus616 [A ~=> F ,A ~=> L ,C ~=> B ,C ~=> J ,E ~=> D ,E ~=> H ,G ~=> F ,I ~=> H ,K ~=> J ,K ~=> F ,K ~=> H ,K ~=> J ,A ~+> F ,A ~+> J ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> 0.2 ,A ~+> tick ,C ~+> F ,C ~+> J ,C ~+> 0.0 ,C ~+> 0.2 ,C ~+> tick ,E ~+> 0.2.0 ,E ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.2.0 ,K ~+> tick ,A ~*> 0.2 ,A ~*> tick ,C ~*> 0.2 ,C ~*> tick ,E ~*> 0.2.0 ,E ~*> tick ,K ~*> 0.2 ,K ~*> tick] + lbl131.12> [C ~=> J ,K ~=> H ,A ~+> 0.0 ,A ~+> tick ,C ~+> 0.0 ,C ~+> tick ,J ~+> 0.0 ,J ~+> tick ,tick ~+> tick] + lbl111.8> [L ~=> F,F ~+> 0.1,F ~+> tick,L ~+> 0.1,L ~+> tick,tick ~+> tick] + lbl121.11> [E ~=> H ,K ~=> H ,B ~+> F ,B ~+> J ,C ~+> 0.2 ,C ~+> tick ,E ~+> 0.2.0 ,E ~+> tick ,J ~+> 0.2 ,J ~+> tick ,L ~+> F ,L ~+> J ,L ~+> 0.2 ,L ~+> tick ,tick ~+> tick ,K ~+> 0.2.0 ,K ~+> tick ,C ~*> tick ,E ~*> 0.2.0 ,E ~*> tick ,J ~*> tick ,L ~*> tick ,K ~*> 0.2 ,K ~*> tick] lbl121.11> [E ~=> H ,J ~=> F ,K ~=> H ,B ~+> F ,B ~+> J ,C ~+> 0.2 ,C ~+> tick ,E ~+> 0.2.0 ,E ~+> tick ,H ~+> 0.2.0 ,H ~+> tick ,J ~+> 0.2 ,J ~+> tick ,L ~+> F ,L ~+> J ,L ~+> 0.2 ,L ~+> tick ,tick ~+> tick ,K ~+> 0.2.0 ,K ~+> tick ,C ~*> tick ,E ~*> 0.2.0 ,E ~*> tick ,H ~*> tick ,J ~*> tick ,L ~*> tick ,K ~*> 0.2 ,K ~*> tick] + lbl121.10> [E ~=> H,J ~=> F,E ~+> 0.2.0,E ~+> tick,H ~+> 0.2.0,H ~+> tick,tick ~+> tick] YES(?,POLY)