MAYBE * Step 1: UnsatRules 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) [2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] (?,1) 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) [A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] (?,1) 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) [2 + 2*N + P >= A (?,1) && P >= 0 && 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) [A >= 3 + 2*N + P (?,1) && P >= 0 && 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) [A >= 3 + 2*N + P (?,1) && P >= 0 && 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) [A >= 4 + 2*N + P (?,1) && P >= 0 && 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) [A >= 4 + 2*N + P (?,1) && P >= 0 && 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) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] (?,1) 8. lbl281(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) [0 >= 3 + A + P && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] (?,1) 9. lbl281(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) [0 >= 3 + A + P && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] (?,1) 10. lbl281(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) [0 >= 4 + A + P && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] (?,1) 11. lbl281(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) [0 >= 4 + A + P && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] (?,1) 12. 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) [2 + L >= A (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && 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) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S,T) [N + R >= 1 (?,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] 14. 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) [A >= 4 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 15. 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) [A >= 4 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 16. 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) [A >= 5 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 17. 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) [A >= 5 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 18. 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) [R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] (?,1) 19. 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) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] (?,1) 20. 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) [R >= 1 + 2*H (?,1) && 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] 21. 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 + 2*H >= 0 (?,1) && 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] 22. 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) [R >= 1 + 2*F (?,1) && 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] 23. 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) [R >= 1 + 2*D (?,1) && 2 + 2*D >= R && A >= 3 && R >= 1 && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 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) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T) [A >= 2 + B (?,1) && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 25. lbl43(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,0,Q,R,S,T) [1 + B >= A (?,1) && 1 >= A && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 26. lbl43(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,0,M,0,O,1,Q,0,S,T) [B >= 1 (?,1) && 0 >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && B >= R && T = 2 && P = 1 + B && L = M && N = O && A = 2] 27. 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 >= 3 (?,1) && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 28. 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 >= 3 (?,1) && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 29. 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 >= 4 (?,1) && 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] 30. 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 >= 4 (?,1) && 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] 31. 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->{18,19},2->{12,13,14,15,16,17},3->{7,8,9,10,11},4->{2,3,4,5,6},5->{7,8,9,10,11},6->{2,3,4,5,6} ,7->{12,13,14,15,16,17},8->{7,8,9,10,11},9->{2,3,4,5,6},10->{7,8,9,10,11},11->{2,3,4,5,6},12->{},13->{12,13 ,14,15,16,17},14->{7,8,9,10,11},15->{2,3,4,5,6},16->{7,8,9,10,11},17->{2,3,4,5,6},18->{23},19->{24,25,26,27 ,28,29,30},20->{21},21->{18,19},22->{20},23->{22},24->{18,19},25->{},26->{12,13,14,15,16,17},27->{7,8,9,10 ,11},28->{2,3,4,5,6},29->{7,8,9,10,11},30->{2,3,4,5,6},31->{0,1}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [8,9,10,11,25,26] * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) [2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] (?,1) 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) [A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] (?,1) 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) [2 + 2*N + P >= A (?,1) && P >= 0 && 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) [A >= 3 + 2*N + P (?,1) && P >= 0 && 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) [A >= 3 + 2*N + P (?,1) && P >= 0 && 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) [A >= 4 + 2*N + P (?,1) && P >= 0 && 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) [A >= 4 + 2*N + P (?,1) && P >= 0 && 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) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] (?,1) 12. 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) [2 + L >= A (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && 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) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S,T) [N + R >= 1 (?,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] 14. 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) [A >= 4 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 15. 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) [A >= 4 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 16. 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) [A >= 5 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 17. 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) [A >= 5 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 18. 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) [R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] (?,1) 19. 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) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] (?,1) 20. 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) [R >= 1 + 2*H (?,1) && 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] 21. 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 + 2*H >= 0 (?,1) && 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] 22. 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) [R >= 1 + 2*F (?,1) && 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] 23. 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) [R >= 1 + 2*D (?,1) && 2 + 2*D >= R && A >= 3 && R >= 1 && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 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) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T) [A >= 2 + B (?,1) && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 27. 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 >= 3 (?,1) && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 28. 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 >= 3 (?,1) && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 29. 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 >= 4 (?,1) && 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] 30. 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 >= 4 (?,1) && 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] 31. 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->{18,19},2->{12,13,14,15,16,17},3->{7},4->{2,3,4,5,6},5->{7},6->{2,3,4,5,6},7->{12,13,14,15,16 ,17},12->{},13->{12,13,14,15,16,17},14->{7},15->{2,3,4,5,6},16->{7},17->{2,3,4,5,6},18->{23},19->{24,27,28 ,29,30},20->{21},21->{18,19},22->{20},23->{22},24->{18,19},27->{7},28->{2,3,4,5,6},29->{7},30->{2,3,4,5,6} ,31->{0,1}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,12),(7,12),(13,13),(13,14),(13,15),(13,16),(13,17)] * Step 3: 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) [2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] (?,1) 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) [A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] (?,1) 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) [2 + 2*N + P >= A (?,1) && P >= 0 && 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) [A >= 3 + 2*N + P (?,1) && P >= 0 && 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) [A >= 3 + 2*N + P (?,1) && P >= 0 && 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) [A >= 4 + 2*N + P (?,1) && P >= 0 && 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) [A >= 4 + 2*N + P (?,1) && P >= 0 && 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) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] (?,1) 12. 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) [2 + L >= A (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && 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) -> lbl133(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S,T) [N + R >= 1 (?,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] 14. 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) [A >= 4 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 15. 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) [A >= 4 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 16. 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) [A >= 5 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 17. 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) [A >= 5 + L (?,1) && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] 18. 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) [R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] (?,1) 19. 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) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] (?,1) 20. 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) [R >= 1 + 2*H (?,1) && 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] 21. 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 + 2*H >= 0 (?,1) && 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] 22. 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) [R >= 1 + 2*F (?,1) && 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] 23. 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) [R >= 1 + 2*D (?,1) && 2 + 2*D >= R && A >= 3 && R >= 1 && R >= 1 + 2*J && P >= R && 2 + 2*J >= R && 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) -> lbl71(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S,T) [A >= 2 + B (?,1) && A >= 3 && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 27. 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 >= 3 (?,1) && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 28. 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 >= 3 (?,1) && 1 + B >= A && R >= 1 + 2*J && B >= 1 && 2 + 2*J >= R && B >= R && P = 1 + B && L = M && N = O && T = A] 29. 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 >= 4 (?,1) && 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] 30. 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 >= 4 (?,1) && 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] 31. 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->{18,19},2->{13,14,15,16,17},3->{7},4->{2,3,4,5,6},5->{7},6->{2,3,4,5,6},7->{13,14,15,16,17} ,12->{},13->{12},14->{7},15->{2,3,4,5,6},16->{7},17->{2,3,4,5,6},18->{23},19->{24,27,28,29,30},20->{21} ,21->{18,19},22->{20},23->{22},24->{18,19},27->{7},28->{2,3,4,5,6},29->{7},30->{2,3,4,5,6},31->{0,1}] + Applied Processor: FromIts + Details: () * Step 4: Unfold 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) [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) [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) [2 + 2*N + P >= A && P >= 0 && 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) [A >= 3 + 2*N + P && P >= 0 && 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) [A >= 3 + 2*N + P && P >= 0 && 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) [A >= 4 + 2*N + P && P >= 0 && 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) [A >= 4 + 2*N + P && P >= 0 && 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) [2 + A + P >= 0 && N >= 1 && P >= 0 && 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) [2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && 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) [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) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && 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) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && 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) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && 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) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && 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) [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) [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) [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 + 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) [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) [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 >= 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 >= 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 >= 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 >= 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 >= 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->{18,19},2->{13,14,15,16,17},3->{7},4->{2,3,4,5,6},5->{7},6->{2,3,4,5,6},7->{13,14,15,16,17} ,12->{},13->{12},14->{7},15->{2,3,4,5,6},16->{7},17->{2,3,4,5,6},18->{23},19->{24,27,28,29,30},20->{21} ,21->{18,19},22->{20},23->{22},24->{18,19},27->{7},28->{2,3,4,5,6},29->{7},30->{2,3,4,5,6},31->{0,1}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: start.0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop.32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] start.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.18(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S ,T) [A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] start.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.19(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S ,T) [A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.13(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.14(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.15(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.16(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.17(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,T,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,T,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.13(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.14(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.15(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.16(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.17(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl133.12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop.32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.12(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S ,T) [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.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl71.18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl101.23(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.24(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.27(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.28(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.29(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.30(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl121.20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl123.21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S ,T) [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.21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.18(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S ,T) [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] lbl123.21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.19(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S ,T) [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.22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl121.20(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S ,T) [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.23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl111.22(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [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.24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.18(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S ,T) [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.24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.19(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S ,T) [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.27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start.0(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S ,A) True start0.31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start.1(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S ,A) True Signature: {(lbl101.23,20) ;(lbl111.22,20) ;(lbl121.20,20) ;(lbl123.21,20) ;(lbl133.12,20) ;(lbl133.13,20) ;(lbl133.14,20) ;(lbl133.15,20) ;(lbl133.16,20) ;(lbl133.17,20) ;(lbl271.2,20) ;(lbl271.3,20) ;(lbl271.4,20) ;(lbl271.5,20) ;(lbl271.6,20) ;(lbl281.7,20) ;(lbl43.24,20) ;(lbl43.27,20) ;(lbl43.28,20) ;(lbl43.29,20) ;(lbl43.30,20) ;(lbl71.18,20) ;(lbl71.19,20) ;(start.0,20) ;(start.1,20) ;(start0.31,20) ;(stop.32,20)} Rule Graph: [0->{},1->{39},2->{40,41,42,43,44},3->{26},4->{27},5->{28,29,30,31,32},6->{33},7->{34,35,36,37,38},8->{20 ,21,22,23,24},9->{3,4,5,6,7},10->{8},11->{9,10,11,12,13},12->{14},13->{15,16,17,18,19},14->{20,21,22,23,24} ,15->{3,4,5,6,7},16->{8},17->{9,10,11,12,13},18->{14},19->{15,16,17,18,19},20->{26},21->{27},22->{28,29,30 ,31,32},23->{33},24->{34,35,36,37,38},25->{},26->{25},27->{20,21,22,23,24},28->{3,4,5,6,7},29->{8},30->{9,10 ,11,12,13},31->{14},32->{15,16,17,18,19},33->{20,21,22,23,24},34->{3,4,5,6,7},35->{8},36->{9,10,11,12,13} ,37->{14},38->{15,16,17,18,19},39->{49},40->{50,51},41->{52},42->{53,54,55,56,57},43->{58},44->{59,60,61,62 ,63},45->{46,47},46->{39},47->{40,41,42,43,44},48->{45},49->{48},50->{39},51->{40,41,42,43,44},52->{20,21,22 ,23,24},53->{3,4,5,6,7},54->{8},55->{9,10,11,12,13},56->{14},57->{15,16,17,18,19},58->{20,21,22,23,24} ,59->{3,4,5,6,7},60->{8},61->{9,10,11,12,13},62->{14},63->{15,16,17,18,19},64->{0},65->{1,2}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose MAYBE + Considered Problem: Rules: start.0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop.32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] start.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.18(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S ,T) [A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] start.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.19(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S ,T) [A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.13(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.14(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.15(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.16(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.17(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,T,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,T,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.13(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.14(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.15(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.16(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.17(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl133.12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop.32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.12(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S ,T) [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.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl71.18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl101.23(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.24(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.27(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.28(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.29(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.30(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl121.20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl123.21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S ,T) [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.21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.18(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S ,T) [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] lbl123.21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.19(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S ,T) [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.22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl121.20(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S ,T) [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.23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl111.22(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [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.24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.18(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S ,T) [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.24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.19(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S ,T) [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.27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start.0(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S ,A) True start0.31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start.1(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S ,A) True stop.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.23,20) ;(lbl111.22,20) ;(lbl121.20,20) ;(lbl123.21,20) ;(lbl133.12,20) ;(lbl133.13,20) ;(lbl133.14,20) ;(lbl133.15,20) ;(lbl133.16,20) ;(lbl133.17,20) ;(lbl271.2,20) ;(lbl271.3,20) ;(lbl271.4,20) ;(lbl271.5,20) ;(lbl271.6,20) ;(lbl281.7,20) ;(lbl43.24,20) ;(lbl43.27,20) ;(lbl43.28,20) ;(lbl43.29,20) ;(lbl43.30,20) ;(lbl71.18,20) ;(lbl71.19,20) ;(start.0,20) ;(start.1,20) ;(start0.31,20) ;(stop.32,20)} Rule Graph: [0->{114},1->{39},2->{40,41,42,43,44},3->{26},4->{27},5->{28,29,30,31,32},6->{33},7->{34,35,36,37,38} ,8->{20,21,22,23,24},9->{3,4,5,6,7},10->{8},11->{9,10,11,12,13},12->{14},13->{15,16,17,18,19},14->{20,21,22 ,23,24},15->{3,4,5,6,7},16->{8},17->{9,10,11,12,13},18->{14},19->{15,16,17,18,19},20->{26},21->{27},22->{28 ,29,30,31,32},23->{33},24->{34,35,36,37,38},25->{66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85 ,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113},26->{25} ,27->{20,21,22,23,24},28->{3,4,5,6,7},29->{8},30->{9,10,11,12,13},31->{14},32->{15,16,17,18,19},33->{20,21 ,22,23,24},34->{3,4,5,6,7},35->{8},36->{9,10,11,12,13},37->{14},38->{15,16,17,18,19},39->{49},40->{50,51} ,41->{52},42->{53,54,55,56,57},43->{58},44->{59,60,61,62,63},45->{46,47},46->{39},47->{40,41,42,43,44} ,48->{45},49->{48},50->{39},51->{40,41,42,43,44},52->{20,21,22,23,24},53->{3,4,5,6,7},54->{8},55->{9,10,11 ,12,13},56->{14},57->{15,16,17,18,19},58->{20,21,22,23,24},59->{3,4,5,6,7},60->{8},61->{9,10,11,12,13} ,62->{14},63->{15,16,17,18,19},64->{0},65->{1,2}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114] | +- p:[39,46,45,48,49,50,40,47,51] c: [40,47,50,51] | | | `- p:[39,46,45,48,49] c: [39,45,46,48,49] | `- p:[21,8,10,11,17,13,30,5,9,36,7,15,19,32,22,14,12,18,38,24,27,4,28,34,33,6,23,31,37,16,29,35] c: [4,5,6,7,8,9,10,12,14,15,16,18,21,22,23,24,27,28,29,30,31,32,33,34,35,36,37,38] | `- p:[11,17,13,19] c: [11,13,17,19] * Step 7: AbstractSize MAYBE + Considered Problem: (Rules: start.0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop.32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [2 >= A && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] start.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.18(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S ,T) [A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] start.1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.19(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,1,Q,1,S ,T) [A >= 3 && B = C && D = E && F = G && H = I && J = K && L = M && N = O && P = Q && R = S && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.13(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.14(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.15(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.16(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.17(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + 2*N + P >= A && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q,T,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,1 + 2*R,O,P,Q ,1 + 2*R,S ,T) [A >= 3 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q,T,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,2 + 2*R,O,P,Q ,2 + 2*R,S ,T) [A >= 4 + 2*N + P && P >= 0 && N >= 1 && A >= 2*N + P && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && R = N && T = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.13(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.14(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.15(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.16(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.17(A,B,C,D,E,F,G,H,I,J,K,P,M,N,O,1 + P,Q,R,S ,T) [2 + A + P >= 0 && N >= 1 && P >= 0 && A >= 2 + N + P && B >= 1 + 2*J && 1 + B >= A && T = A && R = A] lbl133.12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> stop.32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [2 + L >= A && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl133.12(A,B,C,D,E,F,G,H,I,J,K,P,M,0,O,1 + P,Q,0,S ,T) [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.14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,T,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,P,Q,1,S ,T) [A >= 4 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,T,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl133.17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,P,Q,2,S ,T) [A >= 5 + L && 2 + L + N + R >= A && R >= N && L + N >= 1 && L >= 0 && A >= 2 + L + N && B >= 1 + 2*J && 1 + B >= A && P = 1 + L && T = A] lbl71.18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl101.23(A,B,C,U,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [R >= 1 && R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.24(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.27(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.28(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.29(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl71.19(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl43.30(A,P,C,D,E,F,G,H,I,J,K,L,M,N,O,1 + P,Q,R,S ,T) [R >= 1 + 2*J && 2 + 2*J >= R && P >= 1 && A >= 3 && P >= R && T = A && N = O && L = M] lbl121.20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl123.21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,H,S ,T) [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.21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.18(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S ,T) [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] lbl123.21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.19(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,R,S ,T) [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.22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl121.20(A,B,C,D,E,F,G,U,I,J,K,L,M,N,O,P,Q,R,S ,T) [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.23(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl111.22(A,B,C,D,E,U,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T) [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.24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.18(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S ,T) [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.24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl71.19(A,B,C,D,E,F,G,H,I,U,K,L,M,N,O,P,Q,P,S ,T) [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.27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,T,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,1,O,0,Q,1,S ,T) [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.29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl281.7(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,T,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.2(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.3(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.4(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.5(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> lbl271.6(A,B,C,D,E,F,G,H,I,J,K,L,M,2,O,0,Q,2,S ,T) [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.31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start.0(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S ,A) True start0.31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T) -> start.1(A,C,C,E,E,G,G,I,I,K,K,M,M,O,O,Q,Q,S,S ,A) True stop.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.32(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.23,20) ;(lbl111.22,20) ;(lbl121.20,20) ;(lbl123.21,20) ;(lbl133.12,20) ;(lbl133.13,20) ;(lbl133.14,20) ;(lbl133.15,20) ;(lbl133.16,20) ;(lbl133.17,20) ;(lbl271.2,20) ;(lbl271.3,20) ;(lbl271.4,20) ;(lbl271.5,20) ;(lbl271.6,20) ;(lbl281.7,20) ;(lbl43.24,20) ;(lbl43.27,20) ;(lbl43.28,20) ;(lbl43.29,20) ;(lbl43.30,20) ;(lbl71.18,20) ;(lbl71.19,20) ;(start.0,20) ;(start.1,20) ;(start0.31,20) ;(stop.32,20)} Rule Graph: [0->{114},1->{39},2->{40,41,42,43,44},3->{26},4->{27},5->{28,29,30,31,32},6->{33},7->{34,35,36,37,38} ,8->{20,21,22,23,24},9->{3,4,5,6,7},10->{8},11->{9,10,11,12,13},12->{14},13->{15,16,17,18,19},14->{20,21,22 ,23,24},15->{3,4,5,6,7},16->{8},17->{9,10,11,12,13},18->{14},19->{15,16,17,18,19},20->{26},21->{27},22->{28 ,29,30,31,32},23->{33},24->{34,35,36,37,38},25->{66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85 ,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113},26->{25} ,27->{20,21,22,23,24},28->{3,4,5,6,7},29->{8},30->{9,10,11,12,13},31->{14},32->{15,16,17,18,19},33->{20,21 ,22,23,24},34->{3,4,5,6,7},35->{8},36->{9,10,11,12,13},37->{14},38->{15,16,17,18,19},39->{49},40->{50,51} ,41->{52},42->{53,54,55,56,57},43->{58},44->{59,60,61,62,63},45->{46,47},46->{39},47->{40,41,42,43,44} ,48->{45},49->{48},50->{39},51->{40,41,42,43,44},52->{20,21,22,23,24},53->{3,4,5,6,7},54->{8},55->{9,10,11 ,12,13},56->{14},57->{15,16,17,18,19},58->{20,21,22,23,24},59->{3,4,5,6,7},60->{8},61->{9,10,11,12,13} ,62->{14},63->{15,16,17,18,19},64->{0},65->{1,2}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114] | +- p:[39,46,45,48,49,50,40,47,51] c: [40,47,50,51] | | | `- p:[39,46,45,48,49] c: [39,45,46,48,49] | `- p:[21,8,10,11,17,13,30,5,9,36,7,15,19,32,22,14,12,18,38,24,27,4,28,34,33,6,23,31,37,16,29,35] c: [4,5,6,7,8,9,10,12,14,15,16,18,21,22,23,24,27,28,29,30,31,32,33,34,35,36,37,38] | `- p:[11,17,13,19] c: [11,13,17,19]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: 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.0 ~> stop.32 [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.1 ~> lbl71.18 [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] start.1 ~> lbl71.19 [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.2 ~> lbl133.13 [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.2 ~> lbl133.14 [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.2 ~> lbl133.15 [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.2 ~> lbl133.16 [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.2 ~> lbl133.17 [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.3 ~> lbl281.7 [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 <= A, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl271.4 ~> lbl271.2 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.4 ~> lbl271.3 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.4 ~> lbl271.4 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.4 ~> lbl271.5 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.4 ~> lbl271.6 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.5 ~> lbl281.7 [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 <= A, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl271.6 ~> lbl271.2 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.6 ~> lbl271.3 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.6 ~> lbl271.4 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.6 ~> lbl271.5 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.6 ~> lbl271.6 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl281.7 ~> lbl133.13 [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] lbl281.7 ~> lbl133.14 [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] lbl281.7 ~> lbl133.15 [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] lbl281.7 ~> lbl133.16 [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] lbl281.7 ~> lbl133.17 [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.12 ~> stop.32 [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.13 ~> lbl133.12 [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 <= A, Q <= Q, R <= 0*K, S <= S, T <= T] lbl133.14 ~> lbl281.7 [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.15 ~> lbl271.2 [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.15 ~> lbl271.3 [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.15 ~> lbl271.4 [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.15 ~> lbl271.5 [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.15 ~> lbl271.6 [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.16 ~> lbl281.7 [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.17 ~> lbl271.2 [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] lbl133.17 ~> lbl271.3 [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] lbl133.17 ~> lbl271.4 [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] lbl133.17 ~> lbl271.5 [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] lbl133.17 ~> lbl271.6 [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.18 ~> lbl101.23 [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.19 ~> lbl43.24 [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 <= K + P, Q <= Q, R <= R, S <= S, T <= T] lbl71.19 ~> lbl43.27 [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 <= K + P, Q <= Q, R <= R, S <= S, T <= T] lbl71.19 ~> lbl43.28 [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 <= K + P, Q <= Q, R <= R, S <= S, T <= T] lbl71.19 ~> lbl43.29 [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 <= K + P, Q <= Q, R <= R, S <= S, T <= T] lbl71.19 ~> lbl43.30 [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 <= K + P, Q <= Q, R <= R, S <= S, T <= T] lbl121.20 ~> lbl123.21 [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.21 ~> lbl71.18 [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] lbl123.21 ~> lbl71.19 [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.22 ~> lbl121.20 [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.23 ~> lbl111.22 [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.24 ~> lbl71.18 [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.24 ~> lbl71.19 [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.27 ~> lbl281.7 [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.28 ~> lbl271.2 [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.28 ~> lbl271.3 [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.28 ~> lbl271.4 [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.28 ~> lbl271.5 [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.28 ~> lbl271.6 [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.29 ~> lbl281.7 [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.30 ~> lbl271.2 [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] lbl43.30 ~> lbl271.3 [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] lbl43.30 ~> lbl271.4 [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] lbl43.30 ~> lbl271.5 [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] lbl43.30 ~> lbl271.6 [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.31 ~> start.0 [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] start0.31 ~> start.1 [A <= A, B <= C, C <= C, D <= E, E <= E, F <= G, G <= G, H <= I, I <= I, J <= K, K <= K, L <= M, M <= M, N <= O, O <= O, P <= Q, Q <= Q, R <= S, S <= S, T <= A] stop.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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.32 ~> 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 <= 2*K + A + P + T] lbl71.18 ~> lbl101.23 [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.21 ~> lbl71.18 [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.20 ~> lbl123.21 [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.22 ~> lbl121.20 [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.23 ~> lbl111.22 [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.24 ~> lbl71.18 [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.19 ~> lbl43.24 [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 <= K + P, Q <= Q, R <= R, S <= S, T <= T] lbl123.21 ~> lbl71.19 [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] lbl43.24 ~> lbl71.19 [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] + Loop: [0.0.0 <= 2*K + P + 2*R] lbl71.18 ~> lbl101.23 [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.21 ~> lbl71.18 [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.20 ~> lbl123.21 [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.22 ~> lbl121.20 [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.23 ~> lbl111.22 [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 <= 5*K + A + P] lbl281.7 ~> lbl133.14 [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.3 ~> lbl281.7 [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 <= A, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl271.4 ~> lbl271.3 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.4 ~> lbl271.4 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.6 ~> lbl271.4 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.4 ~> lbl271.6 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl133.15 ~> lbl271.4 [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.2 ~> lbl133.15 [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.4 ~> lbl271.2 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl133.17 ~> lbl271.4 [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.2 ~> lbl133.17 [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.6 ~> lbl271.2 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.6 ~> lbl271.6 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl133.15 ~> lbl271.6 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= K, O <= O, P <= P, Q <= Q, R <= K, S <= S, T <= T] lbl281.7 ~> lbl133.15 [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.5 ~> lbl281.7 [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 <= A, O <= O, P <= P, Q <= Q, R <= T, S <= S, T <= T] lbl271.4 ~> lbl271.5 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.6 ~> lbl271.5 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl133.17 ~> lbl271.6 [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] lbl281.7 ~> lbl133.17 [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.14 ~> lbl281.7 [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] lbl271.2 ~> lbl133.14 [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.15 ~> lbl271.2 [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.17 ~> lbl271.2 [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] lbl133.16 ~> lbl281.7 [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] lbl271.2 ~> lbl133.16 [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] lbl281.7 ~> lbl133.16 [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.15 ~> lbl271.5 [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.17 ~> lbl271.5 [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.6 ~> lbl271.3 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl133.15 ~> lbl271.3 [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.17 ~> lbl271.3 [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] + Loop: [0.1.0 <= 3*K + 2*A + N + 2*P + 2*R] lbl271.4 ~> lbl271.4 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.6 ~> lbl271.4 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.4 ~> lbl271.6 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] lbl271.6 ~> lbl271.6 [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 <= A, O <= O, P <= P, Q <= Q, R <= A, S <= S, T <= T] + Applied Processor: AbstractFlow + Details: () * Step 9: 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.0 ~> stop.32 [] start.1 ~> lbl71.18 [K ~=> P,K ~=> R,huge ~=> J] start.1 ~> lbl71.19 [K ~=> P,K ~=> R,huge ~=> J] lbl271.2 ~> lbl133.13 [A ~=> P,P ~=> L] lbl271.2 ~> lbl133.14 [A ~=> P,P ~=> L] lbl271.2 ~> lbl133.15 [A ~=> P,P ~=> L] lbl271.2 ~> lbl133.16 [A ~=> P,P ~=> L] lbl271.2 ~> lbl133.17 [A ~=> P,P ~=> L] lbl271.3 ~> lbl281.7 [A ~=> N,T ~=> R] lbl271.4 ~> lbl271.2 [A ~=> N,A ~=> R] lbl271.4 ~> lbl271.3 [A ~=> N,A ~=> R] lbl271.4 ~> lbl271.4 [A ~=> N,A ~=> R] lbl271.4 ~> lbl271.5 [A ~=> N,A ~=> R] lbl271.4 ~> lbl271.6 [A ~=> N,A ~=> R] lbl271.5 ~> lbl281.7 [A ~=> N,T ~=> R] lbl271.6 ~> lbl271.2 [A ~=> N,A ~=> R] lbl271.6 ~> lbl271.3 [A ~=> N,A ~=> R] lbl271.6 ~> lbl271.4 [A ~=> N,A ~=> R] lbl271.6 ~> lbl271.5 [A ~=> N,A ~=> R] lbl271.6 ~> lbl271.6 [A ~=> N,A ~=> R] lbl281.7 ~> lbl133.13 [A ~=> P,P ~=> L] lbl281.7 ~> lbl133.14 [A ~=> P,P ~=> L] lbl281.7 ~> lbl133.15 [A ~=> P,P ~=> L] lbl281.7 ~> lbl133.16 [A ~=> P,P ~=> L] lbl281.7 ~> lbl133.17 [A ~=> P,P ~=> L] lbl133.12 ~> stop.32 [] lbl133.13 ~> lbl133.12 [A ~=> P,P ~=> L,K ~=> N,K ~=> R] lbl133.14 ~> lbl281.7 [T ~=> R,K ~=> N] lbl133.15 ~> lbl271.2 [K ~=> N,K ~=> R] lbl133.15 ~> lbl271.3 [K ~=> N,K ~=> R] lbl133.15 ~> lbl271.4 [K ~=> N,K ~=> R] lbl133.15 ~> lbl271.5 [K ~=> N,K ~=> R] lbl133.15 ~> lbl271.6 [K ~=> N,K ~=> R] lbl133.16 ~> lbl281.7 [T ~=> R,K ~=> N] lbl133.17 ~> lbl271.2 [K ~=> N,K ~=> R] lbl133.17 ~> lbl271.3 [K ~=> N,K ~=> R] lbl133.17 ~> lbl271.4 [K ~=> N,K ~=> R] lbl133.17 ~> lbl271.5 [K ~=> N,K ~=> R] lbl133.17 ~> lbl271.6 [K ~=> N,K ~=> R] lbl71.18 ~> lbl101.23 [huge ~=> D] lbl71.19 ~> lbl43.24 [P ~=> B,P ~+> P,K ~+> P] lbl71.19 ~> lbl43.27 [P ~=> B,P ~+> P,K ~+> P] lbl71.19 ~> lbl43.28 [P ~=> B,P ~+> P,K ~+> P] lbl71.19 ~> lbl43.29 [P ~=> B,P ~+> P,K ~+> P] lbl71.19 ~> lbl43.30 [P ~=> B,P ~+> P,K ~+> P] lbl121.20 ~> lbl123.21 [H ~=> R] lbl123.21 ~> lbl71.18 [huge ~=> J] lbl123.21 ~> lbl71.19 [huge ~=> J] lbl111.22 ~> lbl121.20 [huge ~=> H] lbl101.23 ~> lbl111.22 [huge ~=> F] lbl43.24 ~> lbl71.18 [P ~=> R,huge ~=> J] lbl43.24 ~> lbl71.19 [P ~=> R,huge ~=> J] lbl43.27 ~> lbl281.7 [T ~=> R,K ~=> N,K ~=> P] lbl43.28 ~> lbl271.2 [K ~=> N,K ~=> P,K ~=> R] lbl43.28 ~> lbl271.3 [K ~=> N,K ~=> P,K ~=> R] lbl43.28 ~> lbl271.4 [K ~=> N,K ~=> P,K ~=> R] lbl43.28 ~> lbl271.5 [K ~=> N,K ~=> P,K ~=> R] lbl43.28 ~> lbl271.6 [K ~=> N,K ~=> P,K ~=> R] lbl43.29 ~> lbl281.7 [T ~=> R,K ~=> N,K ~=> P] lbl43.30 ~> lbl271.2 [K ~=> N,K ~=> P,K ~=> R] lbl43.30 ~> lbl271.3 [K ~=> N,K ~=> P,K ~=> R] lbl43.30 ~> lbl271.4 [K ~=> N,K ~=> P,K ~=> R] lbl43.30 ~> lbl271.5 [K ~=> N,K ~=> P,K ~=> R] lbl43.30 ~> lbl271.6 [K ~=> N,K ~=> P,K ~=> R] start0.31 ~> start.0 [A ~=> T ,C ~=> B ,E ~=> D ,G ~=> F ,I ~=> H ,K ~=> J ,M ~=> L ,O ~=> N ,Q ~=> P ,S ~=> R] start0.31 ~> start.1 [A ~=> T ,C ~=> B ,E ~=> D ,G ~=> F ,I ~=> H ,K ~=> J ,M ~=> L ,O ~=> N ,Q ~=> P ,S ~=> R] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] stop.32 ~> exitus616 [] + Loop: [A ~+> 0.0,P ~+> 0.0,T ~+> 0.0,K ~*> 0.0] lbl71.18 ~> lbl101.23 [huge ~=> D] lbl123.21 ~> lbl71.18 [huge ~=> J] lbl121.20 ~> lbl123.21 [H ~=> R] lbl111.22 ~> lbl121.20 [huge ~=> H] lbl101.23 ~> lbl111.22 [huge ~=> F] lbl43.24 ~> lbl71.18 [P ~=> R,huge ~=> J] lbl71.19 ~> lbl43.24 [P ~=> B,P ~+> P,K ~+> P] lbl123.21 ~> lbl71.19 [huge ~=> J] lbl43.24 ~> lbl71.19 [P ~=> R,huge ~=> J] + Loop: [P ~+> 0.0.0,R ~*> 0.0.0,K ~*> 0.0.0] lbl71.18 ~> lbl101.23 [huge ~=> D] lbl123.21 ~> lbl71.18 [huge ~=> J] lbl121.20 ~> lbl123.21 [H ~=> R] lbl111.22 ~> lbl121.20 [huge ~=> H] lbl101.23 ~> lbl111.22 [huge ~=> F] + Loop: [A ~+> 0.1,P ~+> 0.1,K ~*> 0.1] lbl281.7 ~> lbl133.14 [A ~=> P,P ~=> L] lbl271.3 ~> lbl281.7 [A ~=> N,T ~=> R] lbl271.4 ~> lbl271.3 [A ~=> N,A ~=> R] lbl271.4 ~> lbl271.4 [A ~=> N,A ~=> R] lbl271.6 ~> lbl271.4 [A ~=> N,A ~=> R] lbl271.4 ~> lbl271.6 [A ~=> N,A ~=> R] lbl133.15 ~> lbl271.4 [K ~=> N,K ~=> R] lbl271.2 ~> lbl133.15 [A ~=> P,P ~=> L] lbl271.4 ~> lbl271.2 [A ~=> N,A ~=> R] lbl133.17 ~> lbl271.4 [K ~=> N,K ~=> R] lbl271.2 ~> lbl133.17 [A ~=> P,P ~=> L] lbl271.6 ~> lbl271.2 [A ~=> N,A ~=> R] lbl271.6 ~> lbl271.6 [A ~=> N,A ~=> R] lbl133.15 ~> lbl271.6 [K ~=> N,K ~=> R] lbl281.7 ~> lbl133.15 [A ~=> P,P ~=> L] lbl271.5 ~> lbl281.7 [A ~=> N,T ~=> R] lbl271.4 ~> lbl271.5 [A ~=> N,A ~=> R] lbl271.6 ~> lbl271.5 [A ~=> N,A ~=> R] lbl133.17 ~> lbl271.6 [K ~=> N,K ~=> R] lbl281.7 ~> lbl133.17 [A ~=> P,P ~=> L] lbl133.14 ~> lbl281.7 [T ~=> R,K ~=> N] lbl271.2 ~> lbl133.14 [A ~=> P,P ~=> L] lbl133.15 ~> lbl271.2 [K ~=> N,K ~=> R] lbl133.17 ~> lbl271.2 [K ~=> N,K ~=> R] lbl133.16 ~> lbl281.7 [T ~=> R,K ~=> N] lbl271.2 ~> lbl133.16 [A ~=> P,P ~=> L] lbl281.7 ~> lbl133.16 [A ~=> P,P ~=> L] lbl133.15 ~> lbl271.5 [K ~=> N,K ~=> R] lbl133.17 ~> lbl271.5 [K ~=> N,K ~=> R] lbl271.6 ~> lbl271.3 [A ~=> N,A ~=> R] lbl133.15 ~> lbl271.3 [K ~=> N,K ~=> R] lbl133.17 ~> lbl271.3 [K ~=> N,K ~=> R] + Loop: [N ~+> 0.1.0,A ~*> 0.1.0,P ~*> 0.1.0,R ~*> 0.1.0,K ~*> 0.1.0] lbl271.4 ~> lbl271.4 [A ~=> N,A ~=> R] lbl271.6 ~> lbl271.4 [A ~=> N,A ~=> R] lbl271.4 ~> lbl271.6 [A ~=> N,A ~=> R] lbl271.6 ~> lbl271.6 [A ~=> N,A ~=> R] + Applied Processor: Lare + Details: Unknown bound. MAYBE