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