YES * Step 1: UnsatPaths YES + 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 YES + 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: Decompose YES + 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: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | +- p:[12] c: [12] | +- p:[8] c: [8] | `- p:[10,14,11] c: [11,14] | `- p:[10] c: [10] * Step 4: CloseWith YES + 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}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | +- p:[12] c: [12] | +- p:[8] c: [8] | `- p:[10,14,11] c: [11,14] | `- p:[10] c: [10]) + Applied Processor: CloseWith True + Details: () YES