MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [I1 >= 1 + J && K >= 0 && H1 >= 1 + I1 && G1 >= 2] (?,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [I1 >= 1 + J && K >= 0 && I1 >= 1 + H1 && G1 >= 2] (?,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + I1 && K >= 0 && H1 >= 1 + I1 && G1 >= 2] (?,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + I1 && K >= 0 && I1 >= 1 + H1 && G1 >= 2] (?,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,M1,K,G1,L1,N,H1,J1,K1,N1,I1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [K >= 0 && G1 >= 1 + J1 && H1 >= 2 && M = J] (?,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,M1,K,G1,L1,N,H1,J1,K1,N1,I1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [K >= 0 && J1 >= 1 + G1 && H1 >= 2 && M = J] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [G1 >= 2 && T >= 0 && M = J] (?,1) 12. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] (1,1) 13. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1,F1) [J1 >= 2] (1,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2 && N >= 1 + C] (?,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] (?,1) 16. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] (?,1) 17. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2 && C >= 1 + N] (?,1) 18. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 20. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 21. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) Signature: {(f1,32);(f10,32);(f3,32);(f4,32);(f9,32)} Flow Graph: [0->{0,14,15,16,17},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7 ,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,14,15,16,17},14->{7,8,9 ,10,11},15->{7,8,9,10,11},16->{7,8,9,10,11},17->{7,8,9,10,11},18->{},19->{},20->{},21->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [I1 >= 1 + J && K >= 0 && H1 >= 1 + I1 && G1 >= 2] (1,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [I1 >= 1 + J && K >= 0 && I1 >= 1 + H1 && G1 >= 2] (1,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + I1 && K >= 0 && H1 >= 1 + I1 && G1 >= 2] (1,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + I1 && K >= 0 && I1 >= 1 + H1 && G1 >= 2] (1,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,M1,K,G1,L1,N,H1,J1,K1,N1,I1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [K >= 0 && G1 >= 1 + J1 && H1 >= 2 && M = J] (1,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,M1,K,G1,L1,N,H1,J1,K1,N1,I1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [K >= 0 && J1 >= 1 + G1 && H1 >= 2 && M = J] (1,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [G1 >= 2 && T >= 0 && M = J] (1,1) 12. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] (1,1) 13. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1,F1) [J1 >= 2] (1,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2 && N >= 1 + C] (1,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] (1,1) 16. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] (1,1) 17. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2 && C >= 1 + N] (1,1) 18. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 20. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 21. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) Signature: {(f1,32);(f10,32);(f3,32);(f4,32);(f9,32)} Flow Graph: [0->{0,14,15,16,17},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7 ,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,14,15,16,17},14->{7,8,9 ,10,11},15->{7,8,9,10,11},16->{7,8,9,10,11},17->{7,8,9,10,11},18->{},19->{},20->{},21->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,14) ,(0,17) ,(13,14) ,(13,17) ,(14,7) ,(14,8) ,(14,9) ,(14,10) ,(14,11) ,(15,11) ,(16,11) ,(17,7) ,(17,8) ,(17,9) ,(17,10) ,(17,11)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 + B && B >= 0] (?,1) 1. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [I1 >= 1 + J && K >= 0 && H1 >= 1 + I1 && G1 >= 2] (1,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [I1 >= 1 + J && K >= 0 && I1 >= 1 + H1 && G1 >= 2] (1,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + I1 && K >= 0 && H1 >= 1 + I1 && G1 >= 2] (1,1) 4. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + I1 && K >= 0 && I1 >= 1 + H1 && G1 >= 2] (1,1) 5. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,M1,K,G1,L1,N,H1,J1,K1,N1,I1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [K >= 0 && G1 >= 1 + J1 && H1 >= 2 && M = J] (1,1) 6. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,M1,K,G1,L1,N,H1,J1,K1,N1,I1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [K >= 0 && J1 >= 1 + G1 && H1 >= 2 && M = J] (1,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [G1 >= 2 && T >= 0 && M = J] (1,1) 12. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] (1,1) 13. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1,F1) [J1 >= 2] (1,1) 14. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2 && N >= 1 + C] (1,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] (1,1) 16. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] (1,1) 17. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2 && C >= 1 + N] (1,1) 18. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 20. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 21. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) Signature: {(f1,32);(f10,32);(f3,32);(f4,32);(f9,32)} Flow Graph: [0->{0,15,16},1->{7,8,9,10,11},2->{7,8,9,10,11},3->{7,8,9,10,11},4->{7,8,9,10,11},5->{},6->{},7->{7,8,9,10 ,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,15,16},14->{},15->{7,8,9,10} ,16->{7,8,9,10},17->{},18->{},19->{},20->{},21->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1,2,3,4,5,6,14,17] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [G1 >= 2 && T >= 0 && M = J] (1,1) 12. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] (1,1) 13. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1,F1) [J1 >= 2] (1,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] (1,1) 16. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] (1,1) 18. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 20. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 21. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) Signature: {(f1,32);(f10,32);(f3,32);(f4,32);(f9,32)} Flow Graph: [0->{0,15,16},7->{7,8,9,10,11},8->{7,8,9,10,11},9->{7,8,9,10,11},10->{7,8,9,10,11},11->{},12->{},13->{0,15 ,16},15->{7,8,9,10},16->{7,8,9,10},18->{},19->{},20->{},21->{}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [G1 >= 2 && T >= 0 && M = J] (?,1) 12. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] (1,1) 13. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1,F1) [J1 >= 2] (1,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] (?,1) 16. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] (?,1) 18. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 20. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 21. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 22. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (1,1) 23. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (?,1) Signature: {(exitus616,32);(f1,32);(f10,32);(f3,32);(f4,32);(f9,32)} Flow Graph: [0->{0,15,16},7->{7,8,9,10,11,23},8->{7,8,9,10,11,23},9->{7,8,9,10,11,23},10->{7,8,9,10,11,23},11->{} ,12->{},13->{0,15,16},15->{7,8,9,10,11,23},16->{7,8,9,10,11,23},18->{},19->{},20->{},21->{},22->{},23->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(15,11),(16,11)] * Step 6: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [G1 >= 2 && T >= 0 && M = J] (?,1) 12. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] (1,1) 13. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1,F1) [J1 >= 2] (1,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] (?,1) 16. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] (?,1) 18. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 20. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 21. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 22. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (1,1) 23. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (?,1) Signature: {(exitus616,32);(f1,32);(f10,32);(f3,32);(f4,32);(f9,32)} Flow Graph: [0->{0,15,16},7->{7,8,9,10,11,23},8->{7,8,9,10,11,23},9->{7,8,9,10,11,23},10->{7,8,9,10,11,23},11->{} ,12->{},13->{0,15,16},15->{7,8,9,10,23},16->{7,8,9,10,23},18->{},19->{},20->{},21->{},22->{},23->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,7,8,9,10,11,12,13,15,16,18,19,20,21,22,23] | +- p:[0] c: [0] | `- p:[7,8,9,10] c: [10] | `- p:[7,8,9] c: [9] | `- p:[7,8] c: [8] | `- p:[7] c: [7] * Step 7: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 + B && B >= 0] (?,1) 7. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 8. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 9. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] (?,1) 10. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] (?,1) 11. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [G1 >= 2 && T >= 0 && M = J] (?,1) 12. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] (1,1) 13. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1,F1) [J1 >= 2] (1,1) 15. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] (?,1) 16. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] (?,1) 18. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 19. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 20. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && G1 >= 1 + U1] (1,1) 21. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,X1,K,G1,W1,D,1,U1,V1,O1,Q1,T,U,V,W,H1,I1,K1,N1,R1,C1,D1,E1,F1) [0 >= 1 && U1 >= 1 + G1] (1,1) 22. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (1,1) 23. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (?,1) Signature: {(exitus616,32);(f1,32);(f10,32);(f3,32);(f4,32);(f9,32)} Flow Graph: [0->{0,15,16},7->{7,8,9,10,11,23},8->{7,8,9,10,11,23},9->{7,8,9,10,11,23},10->{7,8,9,10,11,23},11->{} ,12->{},13->{0,15,16},15->{7,8,9,10,23},16->{7,8,9,10,23},18->{},19->{},20->{},21->{},22->{},23->{}] ,We construct a looptree: P: [0,7,8,9,10,11,12,13,15,16,18,19,20,21,22,23] | +- p:[0] c: [0] | `- p:[7,8,9,10] c: [10] | `- p:[7,8,9] c: [9] | `- p:[7,8] c: [8] | `- p:[7] c: [7]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 8: 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 ,U ,V ,W ,X ,Y ,Z ,A1 ,B1 ,C1 ,D1 ,E1 ,F1 ,0.0 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0] f1 ~> f1 [A <= A, B <= A, C <= D, D <= unknown, E <= D, F <= unknown, G <= B, H <= I, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f4 [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 <= unknown, N <= N, O <= unknown, P <= P, Q <= unknown, R <= unknown, S <= unknown, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f3 ~> f4 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= X, M <= unknown, N <= X, O <= unknown, P <= X, Q <= unknown, R <= unknown, S <= unknown, T <= T, U <= U, V <= V, W <= W, X <= unknown, Y <= unknown, Z <= unknown, A1 <= unknown, B1 <= unknown, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f3 ~> f1 [A <= unknown, B <= 2*K, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= unknown, M <= M, N <= unknown, O <= unknown, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= unknown, Y <= unknown, Z <= unknown, A1 <= A1, B1 <= unknown, C1 <= unknown, D1 <= D1, E1 <= E1, F1 <= F1] f1 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= H, I <= I, J <= C, K <= T, L <= N, M <= N, N <= N, O <= unknown, P <= C, Q <= C, R <= C, S <= unknown, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= unknown, A1 <= unknown, B1 <= unknown, C1 <= C1, D1 <= K + T, E1 <= I, F1 <= unknown] f1 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= H, I <= I, J <= C, K <= T, L <= N, M <= N, N <= N, O <= unknown, P <= C, Q <= C, R <= C, S <= unknown, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= unknown, A1 <= unknown, B1 <= unknown, C1 <= C1, D1 <= K + T, E1 <= I, F1 <= unknown] f3 ~> f4 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= unknown, M <= unknown, N <= D, O <= K, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= T, U <= U, V <= V, W <= W, X <= unknown, Y <= unknown, Z <= unknown, A1 <= unknown, B1 <= unknown, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f3 ~> f4 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= unknown, M <= unknown, N <= D, O <= K, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= T, U <= U, V <= V, W <= W, X <= unknown, Y <= unknown, Z <= unknown, A1 <= unknown, B1 <= unknown, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f3 ~> f4 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= unknown, M <= unknown, N <= D, O <= K, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= T, U <= U, V <= V, W <= W, X <= unknown, Y <= unknown, Z <= unknown, A1 <= unknown, B1 <= unknown, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f3 ~> f4 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= unknown, M <= unknown, N <= D, O <= K, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= T, U <= U, V <= V, W <= W, X <= unknown, Y <= unknown, Z <= unknown, A1 <= unknown, B1 <= unknown, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f3 ~> 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, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> 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, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] + Loop: [0.0 <= A + B] f1 ~> f1 [A <= A, B <= A, C <= D, D <= unknown, E <= D, F <= unknown, G <= B, H <= I, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] + Loop: [0.1 <= K + T] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] + Loop: [0.1.0 <= K + T] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] + Loop: [0.1.0.0 <= K + T] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] + Loop: [0.1.0.0.0 <= K + T] f10 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= M, M <= M, N <= M, O <= unknown, P <= unknown, Q <= unknown, R <= J, S <= S, T <= K + T, U <= unknown, V <= I, W <= K + T, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1] + Applied Processor: FlowAbstraction + 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 ,U ,V ,W ,X ,Y ,Z ,A1 ,B1 ,C1 ,D1 ,E1 ,F1 ,0.0 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0] f1 ~> f1 [A ~=> B,B ~=> G,D ~=> C,D ~=> E,I ~=> H,huge ~=> D,huge ~=> F] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f4 [huge ~=> J,huge ~=> M,huge ~=> O,huge ~=> Q,huge ~=> R,huge ~=> S] f3 ~> f4 [X ~=> L ,X ~=> N ,X ~=> P ,huge ~=> A ,huge ~=> A1 ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> J ,huge ~=> M ,huge ~=> O ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> X ,huge ~=> Y ,huge ~=> Z] f3 ~> f1 [K ~=> B ,huge ~=> A ,huge ~=> B1 ,huge ~=> C ,huge ~=> C1 ,huge ~=> D ,huge ~=> E ,huge ~=> L ,huge ~=> N ,huge ~=> O ,huge ~=> X ,huge ~=> Y ,huge ~=> Z] f1 ~> f10 [C ~=> J ,C ~=> P ,C ~=> Q ,C ~=> R ,I ~=> E1 ,N ~=> L ,N ~=> M ,T ~=> K ,huge ~=> A ,huge ~=> A1 ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> F1 ,huge ~=> O ,huge ~=> S ,huge ~=> Z ,T ~+> D1 ,K ~+> D1] f1 ~> f10 [C ~=> J ,C ~=> P ,C ~=> Q ,C ~=> R ,I ~=> E1 ,N ~=> L ,N ~=> M ,T ~=> K ,huge ~=> A ,huge ~=> A1 ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> F1 ,huge ~=> O ,huge ~=> S ,huge ~=> Z ,T ~+> D1 ,K ~+> D1] f3 ~> f4 [D ~=> N ,K ~=> O ,huge ~=> A ,huge ~=> A1 ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> J ,huge ~=> L ,huge ~=> M ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> X ,huge ~=> Y ,huge ~=> Z] f3 ~> f4 [D ~=> N ,K ~=> O ,huge ~=> A ,huge ~=> A1 ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> J ,huge ~=> L ,huge ~=> M ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> X ,huge ~=> Y ,huge ~=> Z] f3 ~> f4 [D ~=> N ,K ~=> O ,huge ~=> A ,huge ~=> A1 ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> J ,huge ~=> L ,huge ~=> M ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> X ,huge ~=> Y ,huge ~=> Z] f3 ~> f4 [D ~=> N ,K ~=> O ,huge ~=> A ,huge ~=> A1 ,huge ~=> B ,huge ~=> B1 ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> J ,huge ~=> L ,huge ~=> M ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> X ,huge ~=> Y ,huge ~=> Z] f3 ~> exitus616 [] f10 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] f1 ~> f1 [A ~=> B,B ~=> G,D ~=> C,D ~=> E,I ~=> H,huge ~=> D,huge ~=> F] + Loop: [T ~+> 0.1,K ~+> 0.1] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] + Loop: [T ~+> 0.1.0,K ~+> 0.1.0] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] + Loop: [T ~+> 0.1.0.0,K ~+> 0.1.0.0] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] + Loop: [T ~+> 0.1.0.0.0,K ~+> 0.1.0.0.0] f10 ~> f10 [I ~=> V ,J ~=> R ,M ~=> L ,M ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,T ~+> T ,T ~+> W ,K ~+> T ,K ~+> W] + Applied Processor: LareProcessor + Details: Unknown bound. MAYBE