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) -> f1(A,1 + B,D,Z,D,A1,B,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1 + B && B >= 0] (?,1) 1. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 + H && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (?,1) 2. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 + H && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 3. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [H >= 1 + B1 && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (?,1) 4. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [H >= 1 + B1 && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 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) -> f10(A,B,C,D,E,F,G,G1,I,F1,Z,B1,C1,D1,E1,H1,A1,R,S,T,U,V,W,X,Y) [I >= 0 && 0 >= 1 + B1 && Z >= 2 && J = H] (?,1) 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) -> f10(A,B,C,D,E,F,G,G1,I,F1,Z,B1,C1,D1,E1,H1,A1,R,S,T,U,V,W,X,Y) [I >= 0 && B1 >= 1 && Z >= 2 && J = H] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. 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) -> f10(A,B,C,D,E,F,G,F1,I,E1,Z,L,B1,C1,D1,G1,A1,R,S,T,U,V,W,X,Y) [Z >= 2 && R >= 0 && J = H] (?,1) 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) -> f10(B1,D1,C1,K1,H1,F,G,P1,I,O1,A1,0,L1,M1,N1,Q1,F1,R,S,T,Z,E1,G1,X,Y) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 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) -> f1(A1,2,B1,C1,B1,F,G,H,I,J,A1,L,M,N,O,P,Q,R,S,T,Z,V,B1,D1,Y) [A1 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2 && 0 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2 && C >= 1] (?,1) Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} 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}] + 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) -> f1(A,1 + B,D,Z,D,A1,B,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1 + B && B >= 0] (?,1) 1. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 + H && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (1,1) 2. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 + H && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (1,1) 3. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [H >= 1 + B1 && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (1,1) 4. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [H >= 1 + B1 && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (1,1) 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) -> f10(A,B,C,D,E,F,G,G1,I,F1,Z,B1,C1,D1,E1,H1,A1,R,S,T,U,V,W,X,Y) [I >= 0 && 0 >= 1 + B1 && Z >= 2 && J = H] (1,1) 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) -> f10(A,B,C,D,E,F,G,G1,I,F1,Z,B1,C1,D1,E1,H1,A1,R,S,T,U,V,W,X,Y) [I >= 0 && B1 >= 1 && Z >= 2 && J = H] (1,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. 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) -> f10(A,B,C,D,E,F,G,F1,I,E1,Z,L,B1,C1,D1,G1,A1,R,S,T,U,V,W,X,Y) [Z >= 2 && R >= 0 && J = H] (1,1) 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) -> f10(B1,D1,C1,K1,H1,F,G,P1,I,O1,A1,0,L1,M1,N1,Q1,F1,R,S,T,Z,E1,G1,X,Y) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 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) -> f1(A1,2,B1,C1,B1,F,G,H,I,J,A1,L,M,N,O,P,Q,R,S,T,Z,V,B1,D1,Y) [A1 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2 && 0 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2 && C >= 1] (1,1) Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} 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}] + 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) -> f1(A,1 + B,D,Z,D,A1,B,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1 + B && B >= 0] (?,1) 1. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 + H && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (1,1) 2. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 + H && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (1,1) 3. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [H >= 1 + B1 && I >= 0 && A1 >= 1 + B1 && Z >= 2 && J = 0] (1,1) 4. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,R,S,T,U,V,W,X,Y) [H >= 1 + B1 && I >= 0 && B1 >= 1 + A1 && Z >= 2 && J = 0] (1,1) 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) -> f10(A,B,C,D,E,F,G,G1,I,F1,Z,B1,C1,D1,E1,H1,A1,R,S,T,U,V,W,X,Y) [I >= 0 && 0 >= 1 + B1 && Z >= 2 && J = H] (1,1) 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) -> f10(A,B,C,D,E,F,G,G1,I,F1,Z,B1,C1,D1,E1,H1,A1,R,S,T,U,V,W,X,Y) [I >= 0 && B1 >= 1 && Z >= 2 && J = H] (1,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. 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) -> f10(A,B,C,D,E,F,G,F1,I,E1,Z,L,B1,C1,D1,G1,A1,R,S,T,U,V,W,X,Y) [Z >= 2 && R >= 0 && J = H] (1,1) 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) -> f10(B1,D1,C1,K1,H1,F,G,P1,I,O1,A1,0,L1,M1,N1,Q1,F1,R,S,T,Z,E1,G1,X,Y) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 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) -> f1(A1,2,B1,C1,B1,F,G,H,I,J,A1,L,M,N,O,P,Q,R,S,T,Z,V,B1,D1,Y) [A1 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 2 && 0 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2 && C >= 1] (1,1) Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} 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->{}] + 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) -> f1(A,1 + B,D,Z,D,A1,B,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1 + B && B >= 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. 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) -> f10(A,B,C,D,E,F,G,F1,I,E1,Z,L,B1,C1,D1,G1,A1,R,S,T,U,V,W,X,Y) [Z >= 2 && R >= 0 && J = H] (1,1) 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) -> f10(B1,D1,C1,K1,H1,F,G,P1,I,O1,A1,0,L1,M1,N1,Q1,F1,R,S,T,Z,E1,G1,X,Y) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 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) -> f1(A1,2,B1,C1,B1,F,G,H,I,J,A1,L,M,N,O,P,Q,R,S,T,Z,V,B1,D1,Y) [A1 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] (1,1) Signature: {(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} 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}] + 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) -> f1(A,1 + B,D,Z,D,A1,B,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1 + B && B >= 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. 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) -> f10(A,B,C,D,E,F,G,F1,I,E1,Z,L,B1,C1,D1,G1,A1,R,S,T,U,V,W,X,Y) [Z >= 2 && R >= 0 && J = H] (?,1) 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) -> f10(B1,D1,C1,K1,H1,F,G,P1,I,O1,A1,0,L1,M1,N1,Q1,F1,R,S,T,Z,E1,G1,X,Y) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 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) -> f1(A1,2,B1,C1,B1,F,G,H,I,J,A1,L,M,N,O,P,Q,R,S,T,Z,V,B1,D1,Y) [A1 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] (?,1) 17. 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) -> 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) True (?,1) 18. 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) -> 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) True (1,1) Signature: {(exitus616,25);(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} Flow Graph: [0->{0,15,16},7->{7,8,9,10,11,17},8->{7,8,9,10,11,17},9->{7,8,9,10,11,17},10->{7,8,9,10,11,17},11->{} ,12->{},13->{0,15,16},15->{7,8,9,10,11,17},16->{7,8,9,10,11,17},17->{},18->{}] + 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) -> f1(A,1 + B,D,Z,D,A1,B,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1 + B && B >= 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. 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) -> f10(A,B,C,D,E,F,G,F1,I,E1,Z,L,B1,C1,D1,G1,A1,R,S,T,U,V,W,X,Y) [Z >= 2 && R >= 0 && J = H] (?,1) 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) -> f10(B1,D1,C1,K1,H1,F,G,P1,I,O1,A1,0,L1,M1,N1,Q1,F1,R,S,T,Z,E1,G1,X,Y) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 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) -> f1(A1,2,B1,C1,B1,F,G,H,I,J,A1,L,M,N,O,P,Q,R,S,T,Z,V,B1,D1,Y) [A1 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] (?,1) 17. 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) -> 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) True (?,1) 18. 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) -> 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) True (1,1) Signature: {(exitus616,25);(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} Flow Graph: [0->{0,15,16},7->{7,8,9,10,11,17},8->{7,8,9,10,11,17},9->{7,8,9,10,11,17},10->{7,8,9,10,11,17},11->{} ,12->{},13->{0,15,16},15->{7,8,9,10,17},16->{7,8,9,10,17},17->{},18->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,7,8,9,10,11,12,13,15,16,17,18] | +- 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) -> f1(A,1 + B,D,Z,D,A1,B,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1 + B && B >= 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [C1 >= 1 + H && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 9. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && A1 >= 1 + C1 && Z >= 2 && J = 0] (?,1) 10. 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) -> f8(A,B,C,D,E,F,G,H,I,0,Z,A1,A1,0,A1,H,Q,-1 + R,B1,-1 + R,U,V,W,X,Y) [H >= 1 + C1 && R >= 0 && C1 >= 1 + A1 && Z >= 2 && J = 0] (?,1) 11. 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) -> f10(A,B,C,D,E,F,G,F1,I,E1,Z,L,B1,C1,D1,G1,A1,R,S,T,U,V,W,X,Y) [Z >= 2 && R >= 0 && J = H] (?,1) 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) -> f10(B1,D1,C1,K1,H1,F,G,P1,I,O1,A1,0,L1,M1,N1,Q1,F1,R,S,T,Z,E1,G1,X,Y) [0 >= I1 && 0 >= A1 && 0 >= J1] (1,1) 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) -> f1(A1,2,B1,C1,B1,F,G,H,I,J,A1,L,M,N,O,P,Q,R,S,T,Z,V,B1,D1,Y) [A1 >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && C >= 1 && C1 >= 0 && Z >= 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) -> f8(A1,C1,B1,H1,G1,F,G,C,R,0,Z,C,C,0,C,C,E1,R,S,T,U,D1,F1,X,1 + R) [K1 >= Z && L1 >= 2 && C1 >= L1 && B >= A && B >= 0 && 0 >= 1 + C && C1 >= 0 && Z >= 2] (?,1) 17. 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) -> 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) True (?,1) 18. 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) -> 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) True (1,1) Signature: {(exitus616,25);(f1,25);(f10,25);(f7,25);(f8,25);(f9,25)} Flow Graph: [0->{0,15,16},7->{7,8,9,10,11,17},8->{7,8,9,10,11,17},9->{7,8,9,10,11,17},10->{7,8,9,10,11,17},11->{} ,12->{},13->{0,15,16},15->{7,8,9,10,17},16->{7,8,9,10,17},17->{},18->{}] ,We construct a looptree: P: [0,7,8,9,10,11,12,13,15,16,17,18] | +- 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,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 <= 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] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f10 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown, I <= I, J <= unknown, K <= unknown, L <= L, M <= unknown, N <= unknown, O <= unknown, P <= unknown, Q <= unknown, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y] f9 ~> f10 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= unknown, I <= I, J <= unknown, K <= unknown, L <= 0*K, M <= unknown, N <= unknown, O <= unknown, P <= unknown, Q <= unknown, R <= R, S <= S, T <= T, U <= unknown, V <= unknown, W <= unknown, X <= X, Y <= Y] f9 ~> f1 [A <= unknown, B <= 2*K, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= H, I <= I, J <= J, K <= unknown, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= unknown, V <= V, W <= unknown, X <= unknown, Y <= Y] f1 ~> f8 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= C, I <= R, J <= 0*K, K <= unknown, L <= C, M <= C, N <= 0*K, O <= C, P <= C, Q <= unknown, R <= R, S <= S, T <= T, U <= U, V <= unknown, W <= unknown, X <= X, Y <= K + R] f1 ~> f8 [A <= unknown, B <= unknown, C <= unknown, D <= unknown, E <= unknown, F <= F, G <= G, H <= C, I <= R, J <= 0*K, K <= unknown, L <= C, M <= C, N <= 0*K, O <= C, P <= C, Q <= unknown, R <= R, S <= S, T <= T, U <= U, V <= unknown, W <= unknown, X <= X, Y <= K + R] 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] 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] + Loop: [0.0 <= A + B] f1 ~> f1 [A <= A, B <= A, C <= D, D <= unknown, E <= D, F <= unknown, G <= B, 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] + Loop: [0.1 <= K + R] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] + Loop: [0.1.0 <= K + R] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] + Loop: [0.1.0.0 <= K + R] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] + Loop: [0.1.0.0.0 <= K + R] f8 ~> f8 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= unknown, L <= unknown, M <= unknown, N <= 0*K, O <= unknown, P <= H, Q <= Q, R <= K + R, S <= unknown, T <= K + R, U <= U, V <= V, W <= W, X <= X, Y <= Y] + 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,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,huge ~=> D,huge ~=> F] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f10 [huge ~=> H ,huge ~=> J ,huge ~=> K ,huge ~=> M ,huge ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q] f9 ~> f10 [K ~=> L ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> H ,huge ~=> J ,huge ~=> K ,huge ~=> M ,huge ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> U ,huge ~=> V ,huge ~=> W] f9 ~> f1 [K ~=> B ,huge ~=> A ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> K ,huge ~=> U ,huge ~=> W ,huge ~=> X] f1 ~> f8 [C ~=> H ,C ~=> L ,C ~=> M ,C ~=> O ,C ~=> P ,R ~=> I ,K ~=> J ,K ~=> N ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> K ,huge ~=> Q ,huge ~=> V ,huge ~=> W ,R ~+> Y ,K ~+> Y] f1 ~> f8 [C ~=> H ,C ~=> L ,C ~=> M ,C ~=> O ,C ~=> P ,R ~=> I ,K ~=> J ,K ~=> N ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> D ,huge ~=> E ,huge ~=> K ,huge ~=> Q ,huge ~=> V ,huge ~=> W ,R ~+> Y ,K ~+> Y] f8 ~> exitus616 [] f9 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] f1 ~> f1 [A ~=> B,B ~=> G,D ~=> C,D ~=> E,huge ~=> D,huge ~=> F] + Loop: [R ~+> 0.1,K ~+> 0.1] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] + Loop: [R ~+> 0.1.0,K ~+> 0.1.0] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] + Loop: [R ~+> 0.1.0.0,K ~+> 0.1.0.0] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] + Loop: [R ~+> 0.1.0.0.0,K ~+> 0.1.0.0.0] f8 ~> f8 [H ~=> P ,K ~=> J ,K ~=> N ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> O ,huge ~=> S ,R ~+> R ,R ~+> T ,K ~+> R ,K ~+> T] + Applied Processor: LareProcessor + Details: Unknown bound. MAYBE