MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 1. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S,T) [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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 2. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + 2*N + P >= A && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 3. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 4. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,1 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 5. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 6. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,2 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 7. lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && R + -1*T >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -6 + R + T >= 0 && -1*R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -5 + B + R >= 0 && 1 + B + -1*R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && -3 + R >= 0 && -3 + P + R >= 0 && -3 + -1*P + R >= 0 && -4 + N + R >= 0 && -6 + A + R >= 0 && -1*A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + A + P >= 0 && N >= 1 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] 8. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && 2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 9. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && N + R >= 1 && R >= N && A + N >= 4 && A >= 3 && 1 >= N && B >= 1 + 2*J && 1 + B >= A && T = A && 2 + P = A && 3 + L = A] 10. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 11. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 12. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 13. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 14. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl101(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 15. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 16. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S,T) [F >= 0 (?,1) && D + F >= 0 && -3 + F + T >= 0 && -1 + F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + R >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*H && 2 + 2*H >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*F && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*F >= R && 2 + 2*D >= R && L = M && N = O && T = A] 17. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S,T) [-1*H + R >= 0 (?,1) && H >= 0 && F + H >= 0 && D + H >= 0 && -3 + H + T >= 0 && H + R >= 0 && H + -1*R >= 0 && -1 + H + P >= 0 && H + J >= 0 && -3 + A + H >= 0 && -1 + -1*F + P >= 0 && F >= 0 && D + F >= 0 && -3 + F + T >= 0 && F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -3 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && R >= 0 && -1 + P + R >= 0 && J + R >= 0 && -3 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && 1 + 2*H >= 0 && P >= 1 && 1 + 2*F >= 0 && 1 + 2*J >= 0 && 1 + 2*D >= 0 && P >= 1 + 2*J && P >= 1 + 2*F && P >= 1 + 2*D && P >= 1 + 2*H && 1 + 2*D >= 2*F && 1 + 2*H >= 2*J && 1 + 2*H >= 2*D && 1 + 2*H >= 2*F && 1 + 2*J >= 2*D && 1 + 2*J >= 2*F && 1 + 2*D >= 2*J && 1 + 2*D >= 2*H && 1 + 2*F >= 2*D && 1 + 2*F >= 2*J && 1 + 2*F >= 2*H && 1 + 2*J >= 2*H && A >= 3 && R = H && L = M && T = A && N = O] 18. lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl121(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 0 (?,1) && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*F && 2 + 2*F >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*D >= R && L = M && N = O && T = A] 19. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl111(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*D && 2 + 2*D >= R && A >= 3 && R >= 1 && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && L = M && N = O && T = A] 20. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 2 + B && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 21. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 22. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 23. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 24. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 25. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S,A) True (1,1) Signature: {(lbl101,20) ;(lbl111,20) ;(lbl121,20) ;(lbl123,20) ;(lbl133,20) ;(lbl271,20) ;(lbl281,20) ;(lbl43,20) ;(lbl71,20) ;(start,20) ;(start0,20) ;(stop,20)} Flow Graph: [0->{},1->{14,15},2->{8,9,10,11,12,13},3->{7},4->{2,3,4,5,6},5->{7},6->{2,3,4,5,6},7->{8,9,10,11,12,13} ,8->{},9->{8,9,10,11,12,13},10->{7},11->{2,3,4,5,6},12->{7},13->{2,3,4,5,6},14->{19},15->{20,21,22,23,24} ,16->{17},17->{14,15},18->{16},19->{18},20->{14,15},21->{7},22->{2,3,4,5,6},23->{7},24->{2,3,4,5,6},25->{0 ,1}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [H + -1*I >= 0 (1,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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 1. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S,T) [H + -1*I >= 0 (1,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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 2. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + 2*N + P >= A && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 3. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 4. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,1 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 5. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 6. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,2 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 7. lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && R + -1*T >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -6 + R + T >= 0 && -1*R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -5 + B + R >= 0 && 1 + B + -1*R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && -3 + R >= 0 && -3 + P + R >= 0 && -3 + -1*P + R >= 0 && -4 + N + R >= 0 && -6 + A + R >= 0 && -1*A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + A + P >= 0 && N >= 1 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] 8. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 + B + -1*T >= 0 (1,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && 2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 9. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && N + R >= 1 && R >= N && A + N >= 4 && A >= 3 && 1 >= N && B >= 1 + 2*J && 1 + B >= A && T = A && 2 + P = A && 3 + L = A] 10. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 11. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 12. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 13. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 14. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl101(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 15. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 16. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S,T) [F >= 0 (?,1) && D + F >= 0 && -3 + F + T >= 0 && -1 + F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + R >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*H && 2 + 2*H >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*F && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*F >= R && 2 + 2*D >= R && L = M && N = O && T = A] 17. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S,T) [-1*H + R >= 0 (?,1) && H >= 0 && F + H >= 0 && D + H >= 0 && -3 + H + T >= 0 && H + R >= 0 && H + -1*R >= 0 && -1 + H + P >= 0 && H + J >= 0 && -3 + A + H >= 0 && -1 + -1*F + P >= 0 && F >= 0 && D + F >= 0 && -3 + F + T >= 0 && F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -3 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && R >= 0 && -1 + P + R >= 0 && J + R >= 0 && -3 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && 1 + 2*H >= 0 && P >= 1 && 1 + 2*F >= 0 && 1 + 2*J >= 0 && 1 + 2*D >= 0 && P >= 1 + 2*J && P >= 1 + 2*F && P >= 1 + 2*D && P >= 1 + 2*H && 1 + 2*D >= 2*F && 1 + 2*H >= 2*J && 1 + 2*H >= 2*D && 1 + 2*H >= 2*F && 1 + 2*J >= 2*D && 1 + 2*J >= 2*F && 1 + 2*D >= 2*J && 1 + 2*D >= 2*H && 1 + 2*F >= 2*D && 1 + 2*F >= 2*J && 1 + 2*F >= 2*H && 1 + 2*J >= 2*H && A >= 3 && R = H && L = M && T = A && N = O] 18. lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl121(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 0 (?,1) && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*F && 2 + 2*F >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*D >= R && L = M && N = O && T = A] 19. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl111(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*D && 2 + 2*D >= R && A >= 3 && R >= 1 && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && L = M && N = O && T = A] 20. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 2 + B && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 21. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S,T) [A + -1*T >= 0 (1,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 22. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S,T) [A + -1*T >= 0 (1,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 23. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S,T) [A + -1*T >= 0 (1,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 24. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S,T) [A + -1*T >= 0 (1,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 25. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S,A) True (1,1) Signature: {(lbl101,20) ;(lbl111,20) ;(lbl121,20) ;(lbl123,20) ;(lbl133,20) ;(lbl271,20) ;(lbl281,20) ;(lbl43,20) ;(lbl71,20) ;(start,20) ;(start0,20) ;(stop,20)} Flow Graph: [0->{},1->{14,15},2->{8,9,10,11,12,13},3->{7},4->{2,3,4,5,6},5->{7},6->{2,3,4,5,6},7->{8,9,10,11,12,13} ,8->{},9->{8,9,10,11,12,13},10->{7},11->{2,3,4,5,6},12->{7},13->{2,3,4,5,6},14->{19},15->{20,21,22,23,24} ,16->{17},17->{14,15},18->{16},19->{18},20->{14,15},21->{7},22->{2,3,4,5,6},23->{7},24->{2,3,4,5,6},25->{0 ,1}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,8),(7,8),(9,9),(9,10),(9,11),(9,12),(9,13)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [H + -1*I >= 0 (1,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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 1. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S,T) [H + -1*I >= 0 (1,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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 2. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + 2*N + P >= A && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 3. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 4. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,1 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 5. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 6. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,2 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 7. lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && R + -1*T >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -6 + R + T >= 0 && -1*R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -5 + B + R >= 0 && 1 + B + -1*R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && -3 + R >= 0 && -3 + P + R >= 0 && -3 + -1*P + R >= 0 && -4 + N + R >= 0 && -6 + A + R >= 0 && -1*A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + A + P >= 0 && N >= 1 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] 8. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 + B + -1*T >= 0 (1,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && 2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 9. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && N + R >= 1 && R >= N && A + N >= 4 && A >= 3 && 1 >= N && B >= 1 + 2*J && 1 + B >= A && T = A && 2 + P = A && 3 + L = A] 10. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 11. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 12. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 13. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 14. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl101(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 15. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 16. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S,T) [F >= 0 (?,1) && D + F >= 0 && -3 + F + T >= 0 && -1 + F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + R >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*H && 2 + 2*H >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*F && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*F >= R && 2 + 2*D >= R && L = M && N = O && T = A] 17. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S,T) [-1*H + R >= 0 (?,1) && H >= 0 && F + H >= 0 && D + H >= 0 && -3 + H + T >= 0 && H + R >= 0 && H + -1*R >= 0 && -1 + H + P >= 0 && H + J >= 0 && -3 + A + H >= 0 && -1 + -1*F + P >= 0 && F >= 0 && D + F >= 0 && -3 + F + T >= 0 && F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -3 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && R >= 0 && -1 + P + R >= 0 && J + R >= 0 && -3 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && 1 + 2*H >= 0 && P >= 1 && 1 + 2*F >= 0 && 1 + 2*J >= 0 && 1 + 2*D >= 0 && P >= 1 + 2*J && P >= 1 + 2*F && P >= 1 + 2*D && P >= 1 + 2*H && 1 + 2*D >= 2*F && 1 + 2*H >= 2*J && 1 + 2*H >= 2*D && 1 + 2*H >= 2*F && 1 + 2*J >= 2*D && 1 + 2*J >= 2*F && 1 + 2*D >= 2*J && 1 + 2*D >= 2*H && 1 + 2*F >= 2*D && 1 + 2*F >= 2*J && 1 + 2*F >= 2*H && 1 + 2*J >= 2*H && A >= 3 && R = H && L = M && T = A && N = O] 18. lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl121(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 0 (?,1) && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*F && 2 + 2*F >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*D >= R && L = M && N = O && T = A] 19. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl111(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*D && 2 + 2*D >= R && A >= 3 && R >= 1 && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && L = M && N = O && T = A] 20. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 2 + B && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 21. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S,T) [A + -1*T >= 0 (1,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 22. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S,T) [A + -1*T >= 0 (1,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 23. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S,T) [A + -1*T >= 0 (1,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 24. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S,T) [A + -1*T >= 0 (1,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 25. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S,A) True (1,1) Signature: {(lbl101,20) ;(lbl111,20) ;(lbl121,20) ;(lbl123,20) ;(lbl133,20) ;(lbl271,20) ;(lbl281,20) ;(lbl43,20) ;(lbl71,20) ;(start,20) ;(start0,20) ;(stop,20)} Flow Graph: [0->{},1->{14,15},2->{9,10,11,12,13},3->{7},4->{2,3,4,5,6},5->{7},6->{2,3,4,5,6},7->{9,10,11,12,13},8->{} ,9->{8},10->{7},11->{2,3,4,5,6},12->{7},13->{2,3,4,5,6},14->{19},15->{20,21,22,23,24},16->{17},17->{14,15} ,18->{16},19->{18},20->{14,15},21->{7},22->{2,3,4,5,6},23->{7},24->{2,3,4,5,6},25->{0,1}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 1. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S,T) [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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 2. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + 2*N + P >= A && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 3. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 4. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,1 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 5. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 6. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,2 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 7. lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && R + -1*T >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -6 + R + T >= 0 && -1*R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -5 + B + R >= 0 && 1 + B + -1*R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && -3 + R >= 0 && -3 + P + R >= 0 && -3 + -1*P + R >= 0 && -4 + N + R >= 0 && -6 + A + R >= 0 && -1*A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + A + P >= 0 && N >= 1 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] 8. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && 2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 9. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && N + R >= 1 && R >= N && A + N >= 4 && A >= 3 && 1 >= N && B >= 1 + 2*J && 1 + B >= A && T = A && 2 + P = A && 3 + L = A] 10. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 11. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 12. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 13. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 14. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl101(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 15. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 16. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S,T) [F >= 0 (?,1) && D + F >= 0 && -3 + F + T >= 0 && -1 + F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + R >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*H && 2 + 2*H >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*F && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*F >= R && 2 + 2*D >= R && L = M && N = O && T = A] 17. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S,T) [-1*H + R >= 0 (?,1) && H >= 0 && F + H >= 0 && D + H >= 0 && -3 + H + T >= 0 && H + R >= 0 && H + -1*R >= 0 && -1 + H + P >= 0 && H + J >= 0 && -3 + A + H >= 0 && -1 + -1*F + P >= 0 && F >= 0 && D + F >= 0 && -3 + F + T >= 0 && F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -3 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && R >= 0 && -1 + P + R >= 0 && J + R >= 0 && -3 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && 1 + 2*H >= 0 && P >= 1 && 1 + 2*F >= 0 && 1 + 2*J >= 0 && 1 + 2*D >= 0 && P >= 1 + 2*J && P >= 1 + 2*F && P >= 1 + 2*D && P >= 1 + 2*H && 1 + 2*D >= 2*F && 1 + 2*H >= 2*J && 1 + 2*H >= 2*D && 1 + 2*H >= 2*F && 1 + 2*J >= 2*D && 1 + 2*J >= 2*F && 1 + 2*D >= 2*J && 1 + 2*D >= 2*H && 1 + 2*F >= 2*D && 1 + 2*F >= 2*J && 1 + 2*F >= 2*H && 1 + 2*J >= 2*H && A >= 3 && R = H && L = M && T = A && N = O] 18. lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl121(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 0 (?,1) && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*F && 2 + 2*F >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*D >= R && L = M && N = O && T = A] 19. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl111(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*D && 2 + 2*D >= R && A >= 3 && R >= 1 && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && L = M && N = O && T = A] 20. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 2 + B && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 21. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 22. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 23. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 24. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 25. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S,A) True (1,1) 26. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 27. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) Signature: {(exitus616,20) ;(lbl101,20) ;(lbl111,20) ;(lbl121,20) ;(lbl123,20) ;(lbl133,20) ;(lbl271,20) ;(lbl281,20) ;(lbl43,20) ;(lbl71,20) ;(start,20) ;(start0,20) ;(stop,20)} Flow Graph: [0->{},1->{14,15},2->{8,9,10,11,12,13,26},3->{7},4->{2,3,4,5,6},5->{7},6->{2,3,4,5,6},7->{8,9,10,11,12,13 ,26},8->{},9->{8,9,10,11,12,13,26},10->{7},11->{2,3,4,5,6},12->{7},13->{2,3,4,5,6},14->{19},15->{20,21,22,23 ,24},16->{17},17->{14,15},18->{16},19->{18},20->{14,15},21->{7},22->{2,3,4,5,6},23->{7},24->{2,3,4,5,6} ,25->{0,1,27},26->{},27->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,8),(7,8),(9,9),(9,10),(9,11),(9,12),(9,13)] * Step 5: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 1. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S,T) [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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 2. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + 2*N + P >= A && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 3. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 4. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,1 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 5. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 6. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,2 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 7. lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && R + -1*T >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -6 + R + T >= 0 && -1*R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -5 + B + R >= 0 && 1 + B + -1*R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && -3 + R >= 0 && -3 + P + R >= 0 && -3 + -1*P + R >= 0 && -4 + N + R >= 0 && -6 + A + R >= 0 && -1*A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + A + P >= 0 && N >= 1 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] 8. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && 2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 9. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && N + R >= 1 && R >= N && A + N >= 4 && A >= 3 && 1 >= N && B >= 1 + 2*J && 1 + B >= A && T = A && 2 + P = A && 3 + L = A] 10. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 11. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 12. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 13. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 14. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl101(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 15. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 16. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S,T) [F >= 0 (?,1) && D + F >= 0 && -3 + F + T >= 0 && -1 + F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + R >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*H && 2 + 2*H >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*F && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*F >= R && 2 + 2*D >= R && L = M && N = O && T = A] 17. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S,T) [-1*H + R >= 0 (?,1) && H >= 0 && F + H >= 0 && D + H >= 0 && -3 + H + T >= 0 && H + R >= 0 && H + -1*R >= 0 && -1 + H + P >= 0 && H + J >= 0 && -3 + A + H >= 0 && -1 + -1*F + P >= 0 && F >= 0 && D + F >= 0 && -3 + F + T >= 0 && F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -3 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && R >= 0 && -1 + P + R >= 0 && J + R >= 0 && -3 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && 1 + 2*H >= 0 && P >= 1 && 1 + 2*F >= 0 && 1 + 2*J >= 0 && 1 + 2*D >= 0 && P >= 1 + 2*J && P >= 1 + 2*F && P >= 1 + 2*D && P >= 1 + 2*H && 1 + 2*D >= 2*F && 1 + 2*H >= 2*J && 1 + 2*H >= 2*D && 1 + 2*H >= 2*F && 1 + 2*J >= 2*D && 1 + 2*J >= 2*F && 1 + 2*D >= 2*J && 1 + 2*D >= 2*H && 1 + 2*F >= 2*D && 1 + 2*F >= 2*J && 1 + 2*F >= 2*H && 1 + 2*J >= 2*H && A >= 3 && R = H && L = M && T = A && N = O] 18. lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl121(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 0 (?,1) && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*F && 2 + 2*F >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*D >= R && L = M && N = O && T = A] 19. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl111(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*D && 2 + 2*D >= R && A >= 3 && R >= 1 && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && L = M && N = O && T = A] 20. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 2 + B && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 21. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 22. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 23. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 24. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 25. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S,A) True (1,1) 26. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 27. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) Signature: {(exitus616,20) ;(lbl101,20) ;(lbl111,20) ;(lbl121,20) ;(lbl123,20) ;(lbl133,20) ;(lbl271,20) ;(lbl281,20) ;(lbl43,20) ;(lbl71,20) ;(start,20) ;(start0,20) ;(stop,20)} Flow Graph: [0->{},1->{14,15},2->{9,10,11,12,13,26},3->{7},4->{2,3,4,5,6},5->{7},6->{2,3,4,5,6},7->{9,10,11,12,13,26} ,8->{},9->{8,26},10->{7},11->{2,3,4,5,6},12->{7},13->{2,3,4,5,6},14->{19},15->{20,21,22,23,24},16->{17} ,17->{14,15},18->{16},19->{18},20->{14,15},21->{7},22->{2,3,4,5,6},23->{7},24->{2,3,4,5,6},25->{0,1,27} ,26->{},27->{}] + Applied Processor: LooptreeTransformer + 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] | +- p:[14,17,16,18,19,20,15] c: [20] | | | `- p:[14,17,16,18,19] c: [19] | `- p:[7,3,4,6,11,2,13,5,10,12] c: [13] | `- p:[2,4,6,11,7,3,5,10,12] c: [12] | `- p:[2,4,6,11,7,3,5,10] c: [11] | +- p:[4,6] c: [6] | | | `- p:[4] c: [4] | `- p:[10,7] c: [10] * Step 6: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && 2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 1. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S,T) [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*T >= 0 && -1*A + T >= 0 && R + -1*S >= 0 && -1*R + S >= 0 && P + -1*Q >= 0 && -1*P + Q >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J + -1*K >= 0 && -1*J + K >= 0 && A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] 2. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + 2*N + P >= A && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 3. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 4. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,1 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 3 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 5. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 6. lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,2 + 2*R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -4 + R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -3 + B + R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && -1 + R >= 0 && -1 + P + R >= 0 && -2 + N + R >= 0 && -4 + A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && A >= 4 + 2*N + P && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] 7. lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && R + -1*T >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -6 + R + T >= 0 && -1*R + T >= 0 && -3 + P + T >= 0 && -3 + -1*P + T >= 0 && -4 + N + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && -5 + B + R >= 0 && 1 + B + -1*R >= 0 && -2 + B + P >= 0 && -2 + B + -1*P >= 0 && -3 + B + N >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && -3 + R >= 0 && -3 + P + R >= 0 && -3 + -1*P + R >= 0 && -4 + N + R >= 0 && -6 + A + R >= 0 && -1*A + R >= 0 && -3 + A + -1*P >= 0 && P >= 0 && -1 + N + P >= 0 && -3 + A + P >= 0 && -1 + N >= 0 && -4 + A + N >= 0 && -3 + A >= 0 && 2 + A + P >= 0 && N >= 1 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] 8. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && 2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 9. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && N + R >= 1 && R >= N && A + N >= 4 && A >= 3 && 1 >= N && B >= 1 + 2*J && 1 + B >= A && T = A && 2 + P = A && 3 + L = A] 10. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 11. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 12. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 13. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S,T) [1 + B + -1*T >= 0 (?,1) && A + -1*T >= 0 && -3 + T >= 0 && -5 + B + T >= 0 && -1*R + T >= 0 && -4 + P + T >= 0 && -2 + -1*N + T >= 0 && -3 + L + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -2 + B >= 0 && 1 + B + -1*R >= 0 && -3 + B + P >= 0 && -1 + B + -1*N >= 0 && -2 + B + L >= 0 && -5 + A + B >= 0 && 1 + -1*A + B >= 0 && A + -1*R >= 0 && 1 + L + -1*P >= 0 && -1 + P >= 0 && -2 + N + P >= 0 && -1 + L + P >= 0 && -1 + -1*L + P >= 0 && -4 + A + P >= 0 && -2 + A + -1*N >= 0 && -1 + L + N >= 0 && L >= 0 && -3 + A + L >= 0 && -3 + A >= 0 && A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 14. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl101(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 15. lbl71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] 16. lbl121(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S,T) [F >= 0 (?,1) && D + F >= 0 && -3 + F + T >= 0 && -1 + F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + R >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*H && 2 + 2*H >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*F && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*F >= R && 2 + 2*D >= R && L = M && N = O && T = A] 17. lbl123(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S,T) [-1*H + R >= 0 (?,1) && H >= 0 && F + H >= 0 && D + H >= 0 && -3 + H + T >= 0 && H + R >= 0 && H + -1*R >= 0 && -1 + H + P >= 0 && H + J >= 0 && -3 + A + H >= 0 && -1 + -1*F + P >= 0 && F >= 0 && D + F >= 0 && -3 + F + T >= 0 && F + R >= 0 && -1 + F + P >= 0 && F + J >= 0 && -3 + A + F >= 0 && -1 + -1*D + P >= 0 && D >= 0 && -3 + D + T >= 0 && D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -3 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && R >= 0 && -1 + P + R >= 0 && J + R >= 0 && -3 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && 1 + 2*H >= 0 && P >= 1 && 1 + 2*F >= 0 && 1 + 2*J >= 0 && 1 + 2*D >= 0 && P >= 1 + 2*J && P >= 1 + 2*F && P >= 1 + 2*D && P >= 1 + 2*H && 1 + 2*D >= 2*F && 1 + 2*H >= 2*J && 1 + 2*H >= 2*D && 1 + 2*H >= 2*F && 1 + 2*J >= 2*D && 1 + 2*J >= 2*F && 1 + 2*D >= 2*J && 1 + 2*D >= 2*H && 1 + 2*F >= 2*D && 1 + 2*F >= 2*J && 1 + 2*F >= 2*H && 1 + 2*J >= 2*H && A >= 3 && R = H && L = M && T = A && N = O] 18. lbl111(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl121(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S,T) [D >= 0 (?,1) && -3 + D + T >= 0 && -1 + D + R >= 0 && -1 + D + P >= 0 && D + J >= 0 && -3 + A + D >= 0 && A + -1*T >= 0 && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -1 + -1*J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -1 + -1*J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*F && 2 + 2*F >= R && A >= 3 && R >= 1 && R >= 1 + 2*D && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 2 + 2*D >= R && L = M && N = O && T = A] 19. lbl101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl111(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + R + T >= 0 && -4 + P + T >= 0 && -3 + J + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && P + -1*R >= 0 && -1 + R >= 0 && -2 + P + R >= 0 && -1 + J + R >= 0 && -4 + A + R >= 0 && -1 + P >= 0 && -1 + J + P >= 0 && -4 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 0 && -3 + A + J >= 0 && -3 + A >= 0 && R >= 1 + 2*D && 2 + 2*D >= R && A >= 3 && R >= 1 && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && L = M && N = O && T = A] 20. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 2 + B && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 21. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 22. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 3 && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 23. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 24. lbl43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S,T) [A + -1*T >= 0 (?,1) && -3 + T >= 0 && -4 + B + T >= 0 && -5 + P + T >= 0 && -6 + A + T >= 0 && -1*A + T >= 0 && -1 + -1*B + P >= 0 && -1 + B >= 0 && B + -1*R >= 0 && -3 + B + P >= 0 && 1 + B + -1*P >= 0 && -4 + A + B >= 0 && -1 + P + -1*R >= 0 && -2 + P >= 0 && -5 + A + P >= 0 && N + -1*O >= 0 && -1*N + O >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && -3 + A >= 0 && A >= 4 && 1 + B >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 25. start0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S,A) True (1,1) 26. lbl133(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) 27. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) True (?,1) Signature: {(exitus616,20) ;(lbl101,20) ;(lbl111,20) ;(lbl121,20) ;(lbl123,20) ;(lbl133,20) ;(lbl271,20) ;(lbl281,20) ;(lbl43,20) ;(lbl71,20) ;(start,20) ;(start0,20) ;(stop,20)} Flow Graph: [0->{},1->{14,15},2->{9,10,11,12,13,26},3->{7},4->{2,3,4,5,6},5->{7},6->{2,3,4,5,6},7->{9,10,11,12,13,26} ,8->{},9->{8,26},10->{7},11->{2,3,4,5,6},12->{7},13->{2,3,4,5,6},14->{19},15->{20,21,22,23,24},16->{17} ,17->{14,15},18->{16},19->{18},20->{14,15},21->{7},22->{2,3,4,5,6},23->{7},24->{2,3,4,5,6},25->{0,1,27} ,26->{},27->{}] ,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] | +- p:[14,17,16,18,19,20,15] c: [20] | | | `- p:[14,17,16,18,19] c: [19] | `- p:[7,3,4,6,11,2,13,5,10,12] c: [13] | `- p:[2,4,6,11,7,3,5,10,12] c: [12] | `- p:[2,4,6,11,7,3,5,10] c: [11] | +- p:[4,6] c: [6] | | | `- p:[4] c: [4] | `- p:[10,7] c: [10]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A ,B ,C ,D ,E ,F ,G ,H ,I ,J ,K ,L ,M ,N ,O ,P ,Q ,R ,S ,T ,0.0 ,0.0.0 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0 ,0.1.0.0.0.0 ,0.1.0.0.1] start ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] start ~> lbl71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= N, O <= O, P <= K, Q <= Q, R <= K, S <= S, T <= T] lbl271 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= N, O <= O, P <= B, Q <= Q, R <= R, S <= S, T <= T] lbl271 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] lbl271 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] lbl281 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= N, O <= O, P <= A, Q <= Q, R <= R, S <= S, T <= T] lbl133 ~> stop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl133 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= 0*K, O <= O, P <= B, Q <= Q, R <= 0*K, S <= S, T <= T] lbl133 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl133 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= K, S <= S, T <= T] lbl133 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= 2*K, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl133 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= 2*K, O <= O, P <= P, Q <= Q, R <= 2*K, S <= S, T <= T] lbl71 ~> lbl101 [A <= A, B <= B, C <= C, D <= unknown, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl71 ~> lbl43 [A <= A, B <= P, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P + T, Q <= Q, R <= R, S <= S, T <= T] lbl121 ~> lbl123 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= H, S <= S, T <= T] lbl123 ~> lbl71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl111 ~> lbl121 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl101 ~> lbl111 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl43 ~> lbl71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= P, S <= S, T <= T] lbl43 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= 0*K, Q <= Q, R <= T, S <= S, T <= T] lbl43 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= 0*K, Q <= Q, R <= K, S <= S, T <= T] lbl43 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= 2*K, O <= O, P <= 0*K, Q <= Q, R <= T, S <= S, T <= T] lbl43 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= 2*K, O <= O, P <= 0*K, Q <= Q, R <= 2*K, S <= S, T <= T] start0 ~> start [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= K, K <= K, L <= M, M <= M, N <= O, O <= O, P <= Q, Q <= Q, R <= S, S <= S, T <= A] lbl133 ~> 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, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] start ~> 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, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] + Loop: [0.0 <= K + A + B + P] lbl71 ~> lbl101 [A <= A, B <= B, C <= C, D <= unknown, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl123 ~> lbl71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl121 ~> lbl123 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= H, S <= S, T <= T] lbl111 ~> lbl121 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl101 ~> lbl111 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl43 ~> lbl71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= P, S <= S, T <= T] lbl71 ~> lbl43 [A <= A, B <= P, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P + T, Q <= Q, R <= R, S <= S, T <= T] + Loop: [0.0.0 <= 2*K + 2*R] lbl71 ~> lbl101 [A <= A, B <= B, C <= C, D <= unknown, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl123 ~> lbl71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl121 ~> lbl123 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= H, S <= S, T <= T] lbl111 ~> lbl121 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] lbl101 ~> lbl111 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T] + Loop: [0.1 <= 4*K + A + P] lbl281 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= N, O <= O, P <= A, Q <= Q, R <= R, S <= S, T <= T] lbl271 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] lbl133 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= K, S <= S, T <= T] lbl271 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= N, O <= O, P <= B, Q <= Q, R <= R, S <= S, T <= T] lbl133 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= 2*K, O <= O, P <= P, Q <= Q, R <= 2*K, S <= S, T <= T] lbl271 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl133 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl133 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= 2*K, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] + Loop: [0.1.0 <= 4*K + A + P] lbl271 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= N, O <= O, P <= B, Q <= Q, R <= R, S <= S, T <= T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] lbl133 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= K, S <= S, T <= T] lbl281 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= N, O <= O, P <= A, Q <= Q, R <= R, S <= S, T <= T] lbl271 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl271 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl133 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl133 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= 2*K, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] + Loop: [0.1.0.0 <= 3*K + A + P] lbl271 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= N, O <= O, P <= B, Q <= Q, R <= R, S <= S, T <= T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] lbl133 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= K, S <= S, T <= T] lbl281 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= N, O <= O, P <= A, Q <= Q, R <= R, S <= S, T <= T] lbl271 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl271 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl133 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] + Loop: [0.1.0.0.0 <= K + N + 2*T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] + Loop: [0.1.0.0.0.0 <= N + T] lbl271 ~> lbl271 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= B, O <= O, P <= P, Q <= Q, R <= B, S <= S, T <= T] + Loop: [0.1.0.0.1 <= A + L + P] lbl133 ~> lbl281 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl281 ~> lbl133 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= P, M <= M, N <= N, O <= O, P <= A, Q <= Q, R <= R, S <= S, T <= T] + Applied Processor: FlowAbstraction + Details: () * Step 8: Failure MAYBE + Considered Problem: Program: Domain: [tick ,huge ,K ,A ,B ,C ,D ,E ,F ,G ,H ,I ,J ,K ,L ,M ,N ,O ,P ,Q ,R ,S ,T ,0.0 ,0.0.0 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0 ,0.1.0.0.0.0 ,0.1.0.0.1] start ~> stop [] start ~> lbl71 [K ~=> P,K ~=> R,huge ~=> J] lbl271 ~> lbl133 [B ~=> P,P ~=> L] lbl271 ~> lbl281 [B ~=> N,T ~=> R] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl271 ~> lbl281 [B ~=> N,T ~=> R] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl281 ~> lbl133 [A ~=> P,P ~=> L] lbl133 ~> stop [] lbl133 ~> lbl133 [B ~=> P,P ~=> L,K ~=> N,K ~=> R] lbl133 ~> lbl281 [T ~=> R,K ~=> N] lbl133 ~> lbl271 [K ~=> N,K ~=> R] lbl133 ~> lbl281 [T ~=> R,K ~=> N] lbl133 ~> lbl271 [K ~=> N,K ~=> R] lbl71 ~> lbl101 [huge ~=> D] lbl71 ~> lbl43 [P ~=> B,P ~+> P,T ~+> P] lbl121 ~> lbl123 [H ~=> R] lbl123 ~> lbl71 [huge ~=> J] lbl111 ~> lbl121 [huge ~=> H] lbl101 ~> lbl111 [huge ~=> F] lbl43 ~> lbl71 [P ~=> R,huge ~=> J] lbl43 ~> lbl281 [T ~=> R,K ~=> N,K ~=> P] lbl43 ~> lbl271 [K ~=> N,K ~=> P,K ~=> R] lbl43 ~> lbl281 [T ~=> R,K ~=> N,K ~=> P] lbl43 ~> lbl271 [K ~=> N,K ~=> P,K ~=> R] start0 ~> start [A ~=> T,C ~=> B,E ~=> D,G ~=> F,I ~=> H,K ~=> J,M ~=> L,O ~=> N,Q ~=> P,S ~=> R] lbl133 ~> exitus616 [] start ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,P ~+> 0.0,K ~+> 0.0] lbl71 ~> lbl101 [huge ~=> D] lbl123 ~> lbl71 [huge ~=> J] lbl121 ~> lbl123 [H ~=> R] lbl111 ~> lbl121 [huge ~=> H] lbl101 ~> lbl111 [huge ~=> F] lbl43 ~> lbl71 [P ~=> R,huge ~=> J] lbl71 ~> lbl43 [P ~=> B,P ~+> P,T ~+> P] + Loop: [R ~*> 0.0.0,K ~*> 0.0.0] lbl71 ~> lbl101 [huge ~=> D] lbl123 ~> lbl71 [huge ~=> J] lbl121 ~> lbl123 [H ~=> R] lbl111 ~> lbl121 [huge ~=> H] lbl101 ~> lbl111 [huge ~=> F] + Loop: [A ~+> 0.1,P ~+> 0.1,K ~*> 0.1] lbl281 ~> lbl133 [A ~=> P,P ~=> L] lbl271 ~> lbl281 [B ~=> N,T ~=> R] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl133 ~> lbl271 [K ~=> N,K ~=> R] lbl271 ~> lbl133 [B ~=> P,P ~=> L] lbl133 ~> lbl271 [K ~=> N,K ~=> R] lbl271 ~> lbl281 [B ~=> N,T ~=> R] lbl133 ~> lbl281 [T ~=> R,K ~=> N] lbl133 ~> lbl281 [T ~=> R,K ~=> N] + Loop: [A ~+> 0.1.0,P ~+> 0.1.0,K ~*> 0.1.0] lbl271 ~> lbl133 [B ~=> P,P ~=> L] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl133 ~> lbl271 [K ~=> N,K ~=> R] lbl281 ~> lbl133 [A ~=> P,P ~=> L] lbl271 ~> lbl281 [B ~=> N,T ~=> R] lbl271 ~> lbl281 [B ~=> N,T ~=> R] lbl133 ~> lbl281 [T ~=> R,K ~=> N] lbl133 ~> lbl281 [T ~=> R,K ~=> N] + Loop: [A ~+> 0.1.0.0,P ~+> 0.1.0.0,K ~*> 0.1.0.0] lbl271 ~> lbl133 [B ~=> P,P ~=> L] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl133 ~> lbl271 [K ~=> N,K ~=> R] lbl281 ~> lbl133 [A ~=> P,P ~=> L] lbl271 ~> lbl281 [B ~=> N,T ~=> R] lbl271 ~> lbl281 [B ~=> N,T ~=> R] lbl133 ~> lbl281 [T ~=> R,K ~=> N] + Loop: [N ~+> 0.1.0.0.0,K ~+> 0.1.0.0.0,T ~*> 0.1.0.0.0] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl271 ~> lbl271 [B ~=> N,B ~=> R] + Loop: [N ~+> 0.1.0.0.0.0,T ~+> 0.1.0.0.0.0] lbl271 ~> lbl271 [B ~=> N,B ~=> R] + Loop: [A ~+> 0.1.0.0.1,L ~+> 0.1.0.0.1,P ~+> 0.1.0.0.1] lbl133 ~> lbl281 [T ~=> R,K ~=> N] lbl281 ~> lbl133 [A ~=> P,P ~=> L] + Applied Processor: LareProcessor + Details: Unknown bound. MAYBE