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