MAYBE * Step 1: 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) 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 2: FromIts 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->{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: FromIts + Details: () * Step 3: AddSinks MAYBE + Considered Problem: Rules: 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*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] 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*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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && -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] 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 && -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] 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 && 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] 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 && 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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 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)} Rule 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: Decompose MAYBE + Considered Problem: Rules: 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*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] 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*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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && -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] 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 && -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] 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 && 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] 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 && 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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 stop(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 stop(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 stop(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 stop(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 stop(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 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)} Rule Graph: [0->{30},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->{26,27,28,29},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: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30] | +- p:[14,17,16,18,19,20,15] c: [15,20] | | | `- p:[14,17,16,18,19] c: [14,16,17,18,19] | `- p:[7,3,4,6,11,2,13,5,10,12] c: [2,3,5,7,10,11,12,13] | `- p:[4,6] c: [4,6] * Step 5: AbstractSize MAYBE + Considered Problem: (Rules: 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*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] 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*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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && 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] 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 && -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] 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 && -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] 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 && 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] 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 && 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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 && -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] 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 stop(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 stop(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 stop(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 stop(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 stop(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 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)} Rule Graph: [0->{30},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->{26,27,28,29},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}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30] | +- p:[14,17,16,18,19,20,15] c: [15,20] | | | `- p:[14,17,16,18,19] c: [14,16,17,18,19] | `- p:[7,3,4,6,11,2,13,5,10,12] c: [2,3,5,7,10,11,12,13] | `- p:[4,6] c: [4,6]) + Applied Processor: AbstractSize Minimize + Details: () * Step 6: AbstractFlow 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] 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] stop ~> 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] stop ~> 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] stop ~> 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] stop ~> 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] stop ~> 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 <= A + 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 <= 4*K + 2*P + 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 + 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 ~> 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 <= 8*K + 2*A + 2*P + R + 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] + Applied Processor: AbstractFlow + Details: () * Step 7: 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] 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] stop ~> exitus616 [] stop ~> exitus616 [] stop ~> exitus616 [] stop ~> exitus616 [] stop ~> exitus616 [] + Loop: [A ~+> 0.0,P ~+> 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: [P ~*> 0.0.0,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,T ~+> 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: [R ~+> 0.1.0,T ~+> 0.1.0,A ~*> 0.1.0,P ~*> 0.1.0,K ~*> 0.1.0] lbl271 ~> lbl271 [B ~=> N,B ~=> R] lbl271 ~> lbl271 [B ~=> N,B ~=> R] + Applied Processor: Lare + Details: Unknown bound. MAYBE