MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f12(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1,-1,F,F,Z1,1 + F,A2,Z1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= 2 && Y1 >= A && B >= 0 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 1. f13(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,2,D,Z1,-1 + Z1,G,H,I,A2,2,-1,Y1,B2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [E >= 0 && A >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 2. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[F >= O && P = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 5. f7(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(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,Z1,D1,D1,-1 + Z1,-1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B1 >= 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 6. f7(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> 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,E2,Z,A1,B1,F2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1[B1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 9. f13(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,P1,Q1[A >= 2 && U = 0 && E = 0 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 10. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [0->{2,10,11},1->{2,10,11},2->{},3->{3,4},4->{2,10,11},5->{7,8},6->{},7->{7,8},8->{},9->{7,8},10->{2,10 ,11},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f12(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1,-1,F,F,Z1,1 + F,A2,Z1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= 2 && Y1 >= A && B >= 0 && C = 1] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 1. f13(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,2,D,Z1,-1 + Z1,G,H,I,A2,2,-1,Y1,B2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [E >= 0 && A >= 2] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 2. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[F >= O && P = 1] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 5. f7(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(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,Z1,D1,D1,-1 + Z1,-1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B1 >= 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 6. f7(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> 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,E2,Z,A1,B1,F2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1[B1 >= 0 && G1 = D1] (1,1) ,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 9. f13(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,P1,Q1[A >= 2 && U = 0 && E = 0 && C = 1] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 10. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [0->{2,10,11},1->{2,10,11},2->{},3->{3,4},4->{2,10,11},5->{7,8},6->{},7->{7,8},8->{},9->{7,8},10->{2,10 ,11},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(10,2),(10,10),(10,11)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f12(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1,-1,F,F,Z1,1 + F,A2,Z1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= 2 && Y1 >= A && B >= 0 && C = 1] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 1. f13(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,2,D,Z1,-1 + Z1,G,H,I,A2,2,-1,Y1,B2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [E >= 0 && A >= 2] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 2. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[F >= O && P = 1] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 5. f7(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(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,Z1,D1,D1,-1 + Z1,-1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B1 >= 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 6. f7(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> 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,E2,Z,A1,B1,F2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1[B1 >= 0 && G1 = D1] (1,1) ,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 9. f13(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,P1,Q1[A >= 2 && U = 0 && E = 0 && C = 1] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 10. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [0->{2,10,11},1->{2,10,11},2->{},3->{3,4},4->{2,10,11},5->{7,8},6->{},7->{7,8},8->{},9->{7,8},10->{} ,11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [0,1,5,6,9] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 2. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[F >= O && P = 1] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 10. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (1,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [2->{},3->{3,4},4->{2,10,11},7->{7,8},8->{},10->{},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 2. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[F >= O && P = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 10. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) 15. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> 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,G1,H1,I1,J1,K1,L1,M1,N1 True (1,1) ,S1,T1,U1,V1,W1,X1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 16. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> 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,G1,H1,I1,J1,K1,L1,M1,N1 True (?,1) ,S1,T1,U1,V1,W1,X1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 17. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> 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,G1,H1,I1,J1,K1,L1,M1,N1 True (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) Signature: {(exitus616,50);(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [2->{},3->{3,4},4->{2,10,11,17},7->{7,8,16},8->{},10->{2,10,11,17},11->{7,8,16},12->{3,4},13->{},14->{} ,15->{},16->{},17->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(10,2),(10,10),(10,11)] * Step 6: LooptreeTransformer MAYBE + Considered Problem: Rules: 2. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[F >= O && P = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 10. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) 15. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> 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,G1,H1,I1,J1,K1,L1,M1,N1 True (1,1) ,S1,T1,U1,V1,W1,X1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 16. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> 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,G1,H1,I1,J1,K1,L1,M1,N1 True (?,1) ,S1,T1,U1,V1,W1,X1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 17. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> 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,G1,H1,I1,J1,K1,L1,M1,N1 True (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) Signature: {(exitus616,50);(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [2->{},3->{3,4},4->{2,10,11,17},7->{7,8,16},8->{},10->{17},11->{7,8,16},12->{3,4},13->{},14->{},15->{} ,16->{},17->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [2,3,4,7,8,10,11,12,13,14,15,16,17] | +- p:[3] c: [3] | `- p:[7] c: [7] * Step 7: SizeAbstraction MAYBE + Considered Problem: (Rules: 2. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[F >= O && P = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 10. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) 15. 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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> 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,G1,H1,I1,J1,K1,L1,M1,N1 True (1,1) ,S1,T1,U1,V1,W1,X1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 16. f8(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> 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,G1,H1,I1,J1,K1,L1,M1,N1 True (?,1) ,S1,T1,U1,V1,W1,X1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 17. f116(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> 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,G1,H1,I1,J1,K1,L1,M1,N1 True (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) Signature: {(exitus616,50);(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [2->{},3->{3,4},4->{2,10,11,17},7->{7,8,16},8->{},10->{17},11->{7,8,16},12->{3,4},13->{},14->{},15->{} ,16->{},17->{}] ,We construct a looptree: P: [2,3,4,7,8,10,11,12,13,14,15,16,17] | +- p:[3] c: [3] | `- 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 ,G1 ,H1 ,I1 ,J1 ,K1 ,L1 ,M1 ,N1 ,O1 ,P1 ,Q1 ,R1 ,S1 ,T1 ,U1 ,V1 ,W1 ,X1 ,0.0 ,0.1] f116 ~> f300 [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 <= K, 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, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f1 ~> f1 [A <= A, B <= Q, 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 <= S, S <= unknown, T <= S, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f1 ~> f116 [A <= A, B <= unknown, C <= 0*K, 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 <= unknown, R <= unknown, S <= unknown, T <= unknown, U <= R, V <= R, W <= unknown, X <= unknown, Y <= unknown, Z <= unknown, A1 <= unknown, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f8 ~> f8 [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 <= 0*K, V <= H1, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= D1, D1 <= D1, E1 <= K + E1, F1 <= F1, G1 <= 0*K, H1 <= H1, I1 <= 0*K, J1 <= H1, K1 <= K + E1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f8 ~> f10 [A <= unknown, 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 <= unknown, Z <= Z, A1 <= A1, B1 <= B1, C1 <= unknown, D1 <= unknown, E1 <= E1, F1 <= F1, G1 <= unknown, H1 <= unknown, I1 <= unknown, J1 <= unknown, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f116 ~> f116 [A <= A, B <= B, C <= K + C, D <= D, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= F, P <= K, 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, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, K1 <= K1, L1 <= L1, M1 <= U, N1 <= K + C, O1 <= K + F, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f116 ~> f8 [A <= A, B <= B, C <= K + E1, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= F, P <= K, Q <= Q, R <= R, S <= S, T <= T, U <= 0*K, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= E1, C1 <= V, D1 <= V, E1 <= E1, F1 <= F1, G1 <= 0*K, H1 <= V, I1 <= 0*K, J1 <= V, K1 <= K1, L1 <= K, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= unknown, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f9 ~> f1 [A <= unknown, B <= 2*K, 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 <= 0*K, Q <= unknown, R <= S, S <= unknown, T <= S, U <= U, V <= V, W <= S, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= unknown, R1 <= unknown, S1 <= unknown, T1 <= 2*K, U1 <= unknown, V1 <= V1, W1 <= W1, X1 <= X1] f9 ~> f10 [A <= unknown, B <= unknown, 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 <= 0*K, Q <= unknown, R <= unknown, S <= unknown, T <= unknown, U <= 0*K, V <= 0*K, W <= unknown, X <= unknown, Y <= unknown, Z <= Z, A1 <= A1, B1 <= B1, C1 <= unknown, D1 <= unknown, E1 <= E1, F1 <= F1, G1 <= unknown, H1 <= unknown, I1 <= unknown, J1 <= unknown, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= unknown, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f9 ~> f10 [A <= K, B <= unknown, 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 <= 0*K, Q <= unknown, R <= unknown, S <= unknown, T <= unknown, U <= 0*K, V <= 0*K, W <= unknown, X <= unknown, Y <= unknown, Z <= Z, A1 <= A1, B1 <= B1, C1 <= unknown, D1 <= unknown, E1 <= E1, F1 <= F1, G1 <= unknown, H1 <= unknown, I1 <= unknown, J1 <= unknown, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= unknown, R1 <= unknown, S1 <= unknown, T1 <= T1, U1 <= U1, V1 <= unknown, W1 <= unknown, X1 <= unknown] f9 ~> 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, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f8 ~> 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, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] f116 ~> 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, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] + Loop: [0.0 <= B + Q] f1 ~> f1 [A <= A, B <= Q, 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 <= S, S <= unknown, T <= S, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1, E1 <= E1, F1 <= F1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, K1 <= K1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] + Loop: [0.1 <= K + E1] f8 ~> f8 [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 <= 0*K, V <= H1, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= D1, D1 <= D1, E1 <= K + E1, F1 <= F1, G1 <= 0*K, H1 <= H1, I1 <= 0*K, J1 <= H1, K1 <= K + E1, L1 <= L1, M1 <= M1, N1 <= N1, O1 <= O1, P1 <= P1, Q1 <= Q1, R1 <= R1, S1 <= S1, T1 <= T1, U1 <= U1, V1 <= V1, W1 <= W1, X1 <= X1] + 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 ,G1 ,H1 ,I1 ,J1 ,K1 ,L1 ,M1 ,N1 ,O1 ,P1 ,Q1 ,R1 ,S1 ,T1 ,U1 ,V1 ,W1 ,X1 ,0.0 ,0.1] f116 ~> f300 [K ~=> P] f1 ~> f1 [Q ~=> B,S ~=> R,S ~=> T,huge ~=> S] f1 ~> f116 [R ~=> U ,R ~=> V ,K ~=> C ,huge ~=> A1 ,huge ~=> B ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> T ,huge ~=> W ,huge ~=> X ,huge ~=> Y ,huge ~=> Z] f8 ~> f8 [D1 ~=> C1 ,H1 ~=> J1 ,H1 ~=> V ,K ~=> G1 ,K ~=> I1 ,K ~=> U ,E1 ~+> E1 ,E1 ~+> K1 ,K ~+> E1 ,K ~+> K1] f8 ~> f10 [huge ~=> A ,huge ~=> C1 ,huge ~=> D1 ,huge ~=> G1 ,huge ~=> H1 ,huge ~=> I1 ,huge ~=> J1 ,huge ~=> Y] f116 ~> f116 [F ~=> O ,U ~=> M1 ,K ~=> P ,C ~+> C ,C ~+> N1 ,F ~+> F ,F ~+> O1 ,K ~+> C ,K ~+> F ,K ~+> N1 ,K ~+> O1] f116 ~> f8 [E1 ~=> B1 ,F ~=> O ,V ~=> C1 ,V ~=> D1 ,V ~=> H1 ,V ~=> J1 ,K ~=> G1 ,K ~=> I1 ,K ~=> L1 ,K ~=> P ,K ~=> U ,huge ~=> P1 ,E1 ~+> C ,K ~+> C] f9 ~> f1 [S ~=> R ,S ~=> T ,S ~=> W ,K ~=> B ,K ~=> P ,K ~=> T1 ,huge ~=> A ,huge ~=> Q ,huge ~=> Q1 ,huge ~=> R1 ,huge ~=> S ,huge ~=> S1 ,huge ~=> U1] f9 ~> f10 [K ~=> P ,K ~=> U ,K ~=> V ,huge ~=> A ,huge ~=> B ,huge ~=> C1 ,huge ~=> D1 ,huge ~=> G1 ,huge ~=> H1 ,huge ~=> I1 ,huge ~=> J1 ,huge ~=> Q ,huge ~=> R ,huge ~=> R1 ,huge ~=> S ,huge ~=> T ,huge ~=> W ,huge ~=> X ,huge ~=> Y] f9 ~> f10 [K ~=> A ,K ~=> P ,K ~=> U ,K ~=> V ,huge ~=> B ,huge ~=> C1 ,huge ~=> D1 ,huge ~=> G1 ,huge ~=> H1 ,huge ~=> I1 ,huge ~=> J1 ,huge ~=> Q ,huge ~=> Q1 ,huge ~=> R ,huge ~=> R1 ,huge ~=> S ,huge ~=> S1 ,huge ~=> T ,huge ~=> V1 ,huge ~=> W ,huge ~=> W1 ,huge ~=> X ,huge ~=> X1 ,huge ~=> Y] f9 ~> exitus616 [] f8 ~> exitus616 [] f116 ~> exitus616 [] + Loop: [B ~+> 0.0,Q ~+> 0.0] f1 ~> f1 [Q ~=> B,S ~=> R,S ~=> T,huge ~=> S] + Loop: [E1 ~+> 0.1,K ~+> 0.1] f8 ~> f8 [D1 ~=> C1 ,H1 ~=> J1 ,H1 ~=> V ,K ~=> G1 ,K ~=> I1 ,K ~=> U ,E1 ~+> E1 ,E1 ~+> K1 ,K ~+> E1 ,K ~+> K1] + Applied Processor: LareProcessor + Details: Unknown bound. MAYBE