YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B && C >= 0] (?,1) 1. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] (?,1) 2. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] (?,1) 3. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] (?,1) 4. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] (?,1) 5. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] (?,1) 6. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] (?,1) 7. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] (?,1) 8. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] (?,1) 9. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] (?,1) 10. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 11. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] (?,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] (?,1) 16. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,1) 17. f6(A,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) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,2,3,4,5,6,7,8},10->{1,2,3,4,5,6,7,8},11->{1,2,3,4,5,6,7,8},12->{1,2 ,3,4,5,6,7,8},13->{1,2,3,4,5,6,7,8},14->{1,2,3,4,5,6,7,8},15->{1,2,3,4,5,6,7,8},16->{1,2,3,4,5,6,7,8},17->{0 ,9,10,11,12,13,14,15,16}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B && C >= 0] (?,1) 1. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] (1,1) 2. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] (1,1) 3. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] (?,1) 4. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] (?,1) 5. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] (?,1) 6. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] (?,1) 7. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] (1,1) 8. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] (1,1) 9. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] (1,1) 10. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] (1,1) 11. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] (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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] (1,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] (1,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] (1,1) 16. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (1,1) 17. f6(A,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) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,2,3,4,5,6,7,8},10->{1,2,3,4,5,6,7,8},11->{1,2,3,4,5,6,7,8},12->{1,2 ,3,4,5,6,7,8},13->{1,2,3,4,5,6,7,8},14->{1,2,3,4,5,6,7,8},15->{1,2,3,4,5,6,7,8},16->{1,2,3,4,5,6,7,8},17->{0 ,9,10,11,12,13,14,15,16}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,2) ,(9,4) ,(9,6) ,(9,8) ,(10,2) ,(10,4) ,(10,6) ,(10,8) ,(11,1) ,(11,3) ,(11,5) ,(11,7) ,(12,1) ,(12,3) ,(12,5) ,(12,7) ,(13,2) ,(13,4) ,(13,6) ,(13,8) ,(14,2) ,(14,4) ,(14,6) ,(14,8) ,(15,1) ,(15,3) ,(15,5) ,(15,7) ,(16,1) ,(16,3) ,(16,5) ,(16,7) ,(17,9) ,(17,10) ,(17,11) ,(17,12) ,(17,13) ,(17,14) ,(17,15) ,(17,16)] * Step 3: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B && C >= 0] (?,1) 1. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] (1,1) 2. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] (1,1) 3. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] (?,1) 4. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] (?,1) 5. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] (?,1) 6. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] (?,1) 7. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] (1,1) 8. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] (1,1) 9. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] (1,1) 10. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] (1,1) 11. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] (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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] (1,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] (1,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] (1,1) 16. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (1,1) 17. f6(A,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) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,3,5,7},10->{1,3,5,7},11->{2,4,6,8},12->{2,4,6,8},13->{1,3,5,7} ,14->{1,3,5,7},15->{2,4,6,8},16->{2,4,6,8},17->{0}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B && C >= 0] (?,1) 1. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] (?,1) 2. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] (?,1) 3. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] (?,1) 4. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] (?,1) 5. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] (?,1) 6. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] (?,1) 7. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] (?,1) 8. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] (?,1) 9. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] (?,1) 10. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 11. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] (?,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] (?,1) 16. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,1) 17. f6(A,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) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 18. f5(A,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) -> 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) True (?,1) Signature: {(exitus616,27);(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8,18},4->{1,2,3,4,5,6,7,8,18},5->{1,2,3,4,5,6 ,7,8,18},6->{1,2,3,4,5,6,7,8,18},7->{},8->{},9->{1,2,3,4,5,6,7,8,18},10->{1,2,3,4,5,6,7,8,18},11->{1,2,3,4,5 ,6,7,8,18},12->{1,2,3,4,5,6,7,8,18},13->{1,2,3,4,5,6,7,8,18},14->{1,2,3,4,5,6,7,8,18},15->{1,2,3,4,5,6,7,8 ,18},16->{1,2,3,4,5,6,7,8,18},17->{0,9,10,11,12,13,14,15,16},18->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,2) ,(9,4) ,(9,6) ,(9,8) ,(10,2) ,(10,4) ,(10,6) ,(10,8) ,(11,1) ,(11,3) ,(11,5) ,(11,7) ,(12,1) ,(12,3) ,(12,5) ,(12,7) ,(13,2) ,(13,4) ,(13,6) ,(13,8) ,(14,2) ,(14,4) ,(14,6) ,(14,8) ,(15,1) ,(15,3) ,(15,5) ,(15,7) ,(16,1) ,(16,3) ,(16,5) ,(16,7) ,(17,9) ,(17,10) ,(17,11) ,(17,12) ,(17,13) ,(17,14) ,(17,15) ,(17,16)] * Step 5: LooptreeTransformer WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B && C >= 0] (?,1) 1. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] (?,1) 2. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] (?,1) 3. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] (?,1) 4. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] (?,1) 5. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] (?,1) 6. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] (?,1) 7. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] (?,1) 8. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] (?,1) 9. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] (?,1) 10. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 11. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] (?,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] (?,1) 16. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,1) 17. f6(A,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) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 18. f5(A,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) -> 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) True (?,1) Signature: {(exitus616,27);(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8,18},4->{1,2,3,4,5,6,7,8,18},5->{1,2,3,4,5,6 ,7,8,18},6->{1,2,3,4,5,6,7,8,18},7->{},8->{},9->{1,3,5,7,18},10->{1,3,5,7,18},11->{2,4,6,8,18},12->{2,4,6,8 ,18},13->{1,3,5,7,18},14->{1,3,5,7,18},15->{2,4,6,8,18},16->{2,4,6,8,18},17->{0},18->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18] | +- p:[0] c: [0] | `- p:[3,4,5,6] c: [6] | `- p:[3,4,5] c: [5] | `- p:[3,4] c: [4] | `- p:[3] c: [3] * Step 6: SizeAbstraction WORST_CASE(?,O(1)) + Considered Problem: (Rules: 0. 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) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B && C >= 0] (?,1) 1. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] (?,1) 2. f5(A,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] (?,1) 3. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] (?,1) 4. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] (?,1) 5. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] (?,1) 6. f5(A,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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] (?,1) 7. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] (?,1) 8. f5(A,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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] (?,1) 9. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] (?,1) 10. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 11. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,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,Z,A1) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] (?,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] (?,1) 16. 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) -> f5(A,B,C,D,E,F,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,1) 17. f6(A,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) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 18. f5(A,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) -> 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) True (?,1) Signature: {(exitus616,27);(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8,18},4->{1,2,3,4,5,6,7,8,18},5->{1,2,3,4,5,6 ,7,8,18},6->{1,2,3,4,5,6,7,8,18},7->{},8->{},9->{1,3,5,7,18},10->{1,3,5,7,18},11->{2,4,6,8,18},12->{2,4,6,8 ,18},13->{1,3,5,7,18},14->{1,3,5,7,18},15->{2,4,6,8,18},16->{2,4,6,8,18},17->{0},18->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18] | +- p:[0] c: [0] | `- p:[3,4,5,6] c: [6] | `- p:[3,4,5] c: [5] | `- p:[3,4] c: [4] | `- p:[3] c: [3]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(1)) + 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,0.0,0.1,0.1.0,0.1.0.0,0.1.0.0.0] f9 ~> f9 [A <= A, B <= A + B, C <= K + C, D <= unknown, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f0 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown, I <= I, J <= H, K <= unknown, L <= unknown, M <= unknown, N <= unknown, O <= unknown, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f0 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown, I <= I, J <= H, K <= unknown, L <= unknown, M <= unknown, N <= unknown, O <= unknown, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f12 [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 <= M, N <= unknown, O <= O, P <= 0*K, Q <= R, R <= R, S <= S, T <= T, U <= U, V <= I, W <= unknown, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f12 [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 <= M, N <= unknown, O <= O, P <= 0*K, Q <= R, R <= R, S <= S, T <= T, U <= U, V <= I, W <= unknown, X <= X, Y <= Y, Z <= Z, A1 <= A1] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= C, H <= unknown, I <= K, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= N, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= K, U <= C, V <= V, W <= D, X <= D, Y <= C, Z <= unknown, A1 <= unknown] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= C, H <= unknown, I <= K, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= N, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= K, U <= C, V <= V, W <= D, X <= D, Y <= C, Z <= unknown, A1 <= unknown] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= C, H <= unknown, I <= K, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= N, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= K, U <= C, V <= V, W <= D, X <= D, Y <= C, Z <= unknown, A1 <= unknown] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= C, H <= unknown, I <= K, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= N, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= K, U <= C, V <= V, W <= D, X <= D, Y <= C, Z <= unknown, A1 <= unknown] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= C, H <= unknown, I <= K, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= N, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= K, U <= C, V <= V, W <= D, X <= D, Y <= C, Z <= unknown, A1 <= unknown] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= C, H <= unknown, I <= K, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= N, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= K, U <= C, V <= V, W <= D, X <= D, Y <= C, Z <= unknown, A1 <= unknown] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= C, H <= unknown, I <= K, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= N, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= K, U <= C, V <= V, W <= D, X <= D, Y <= C, Z <= unknown, A1 <= unknown] f9 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= C, H <= unknown, I <= K, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= N, O <= O, P <= unknown, Q <= unknown, R <= unknown, S <= unknown, T <= K, U <= C, V <= V, W <= D, X <= D, Y <= C, Z <= unknown, A1 <= unknown] f6 ~> f9 [A <= 17*K, B <= K, C <= 0*K, D <= unknown, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= unknown, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> 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] + Loop: [0.0 <= A + B] f9 ~> f9 [A <= A, B <= A + B, C <= K + C, D <= unknown, E <= unknown, F <= unknown, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.1 <= K + G] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.1.0 <= K + G] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.1.0.0 <= K + G] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Loop: [0.1.0.0.0 <= K + G] f5 ~> f5 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= K + G, H <= R, I <= K + I, J <= 0*K, K <= unknown, L <= unknown, M <= M, N <= unknown, O <= O, P <= unknown, Q <= R, R <= P, S <= unknown, T <= K + I, U <= K + G, V <= I, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,O(1)) + 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 ,0.0 ,0.1 ,0.1.0 ,0.1.0.0 ,0.1.0.0.0] f9 ~> f9 [huge ~=> D,huge ~=> E,huge ~=> F,A ~+> B,B ~+> B,C ~+> C,K ~+> C] f5 ~> f0 [H ~=> J,huge ~=> H,huge ~=> K,huge ~=> L,huge ~=> M,huge ~=> N,huge ~=> O] f5 ~> f0 [H ~=> J,huge ~=> H,huge ~=> K,huge ~=> L,huge ~=> M,huge ~=> N,huge ~=> O] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f12 [I ~=> V,R ~=> Q,K ~=> J,K ~=> P,huge ~=> K,huge ~=> L,huge ~=> N,huge ~=> W] f5 ~> f12 [I ~=> V,R ~=> Q,K ~=> J,K ~=> P,huge ~=> K,huge ~=> L,huge ~=> N,huge ~=> W] f9 ~> f5 [C ~=> G ,C ~=> U ,C ~=> Y ,D ~=> W ,D ~=> X ,K ~=> I ,K ~=> J ,K ~=> T ,huge ~=> A1 ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> Z] f9 ~> f5 [C ~=> G ,C ~=> U ,C ~=> Y ,D ~=> W ,D ~=> X ,K ~=> I ,K ~=> J ,K ~=> T ,huge ~=> A1 ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> Z] f9 ~> f5 [C ~=> G ,C ~=> U ,C ~=> Y ,D ~=> W ,D ~=> X ,K ~=> I ,K ~=> J ,K ~=> T ,huge ~=> A1 ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> Z] f9 ~> f5 [C ~=> G ,C ~=> U ,C ~=> Y ,D ~=> W ,D ~=> X ,K ~=> I ,K ~=> J ,K ~=> T ,huge ~=> A1 ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> Z] f9 ~> f5 [C ~=> G ,C ~=> U ,C ~=> Y ,D ~=> W ,D ~=> X ,K ~=> I ,K ~=> J ,K ~=> T ,huge ~=> A1 ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> Z] f9 ~> f5 [C ~=> G ,C ~=> U ,C ~=> Y ,D ~=> W ,D ~=> X ,K ~=> I ,K ~=> J ,K ~=> T ,huge ~=> A1 ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> Z] f9 ~> f5 [C ~=> G ,C ~=> U ,C ~=> Y ,D ~=> W ,D ~=> X ,K ~=> I ,K ~=> J ,K ~=> T ,huge ~=> A1 ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> Z] f9 ~> f5 [C ~=> G ,C ~=> U ,C ~=> Y ,D ~=> W ,D ~=> X ,K ~=> I ,K ~=> J ,K ~=> T ,huge ~=> A1 ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> Z] f6 ~> f9 [K ~=> A,K ~=> B,K ~=> C,huge ~=> D,huge ~=> E,huge ~=> F,huge ~=> Q] f5 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0] f9 ~> f9 [huge ~=> D,huge ~=> E,huge ~=> F,A ~+> B,B ~+> B,C ~+> C,K ~+> C] + Loop: [G ~+> 0.1,K ~+> 0.1] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] + Loop: [G ~+> 0.1.0,K ~+> 0.1.0] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] + Loop: [G ~+> 0.1.0.0,K ~+> 0.1.0.0] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] + Loop: [G ~+> 0.1.0.0.0,K ~+> 0.1.0.0.0] f5 ~> f5 [I ~=> V ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> S ,G ~+> G ,G ~+> U ,I ~+> I ,I ~+> T ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U] + Applied Processor: LareProcessor + Details: f6 ~> f0 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> G ,K ~=> I ,K ~=> T ,K ~=> U ,K ~=> V ,K ~=> Y ,huge ~=> A1 ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> H ,huge ~=> J ,huge ~=> K ,huge ~=> L ,huge ~=> M ,huge ~=> N ,huge ~=> O ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> W ,huge ~=> X ,huge ~=> Z ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U ,K ~+> V ,K ~+> Y ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,K ~*> B ,K ~*> C ,K ~*> G ,K ~*> I ,K ~*> T ,K ~*> U ,K ~*> V ,K ~*> Y ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> tick ,K ~^> G ,K ~^> I ,K ~^> T ,K ~^> U ,K ~^> V ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> tick] f6 ~> f12 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> G ,K ~=> I ,K ~=> J ,K ~=> P ,K ~=> T ,K ~=> U ,K ~=> V ,K ~=> Y ,huge ~=> A1 ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> W ,huge ~=> X ,huge ~=> Z ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U ,K ~+> V ,K ~+> Y ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,K ~*> B ,K ~*> C ,K ~*> G ,K ~*> I ,K ~*> T ,K ~*> U ,K ~*> V ,K ~*> Y ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> tick ,K ~^> G ,K ~^> I ,K ~^> T ,K ~^> U ,K ~^> V ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> tick] f6 ~> exitus616 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> G ,K ~=> I ,K ~=> J ,K ~=> T ,K ~=> U ,K ~=> V ,K ~=> Y ,huge ~=> A1 ,huge ~=> D ,huge ~=> E ,huge ~=> F ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,huge ~=> W ,huge ~=> X ,huge ~=> Z ,tick ~+> tick ,K ~+> B ,K ~+> C ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U ,K ~+> V ,K ~+> Y ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,K ~*> B ,K ~*> C ,K ~*> G ,K ~*> I ,K ~*> T ,K ~*> U ,K ~*> V ,K ~*> Y ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> tick ,K ~^> G ,K ~^> I ,K ~^> T ,K ~^> U ,K ~^> V ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> tick] + f9> [huge ~=> D ,huge ~=> E ,huge ~=> F ,A ~+> B ,A ~+> 0.0 ,A ~+> tick ,B ~+> B ,B ~+> 0.0 ,B ~+> tick ,C ~+> C ,tick ~+> tick ,K ~+> C ,A ~*> B ,A ~*> C ,B ~*> B ,B ~*> C ,K ~*> C] + f5> [I ~=> V ,P ~=> H ,P ~=> Q ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,G ~+> G ,G ~+> U ,G ~+> 0.1 ,G ~+> 0.1.0 ,G ~+> 0.1.0.0 ,G ~+> 0.1.0.0.0 ,G ~+> tick ,I ~+> I ,I ~+> T ,I ~+> V ,tick ~+> tick ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U ,K ~+> V ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,G ~*> G ,G ~*> I ,G ~*> T ,G ~*> U ,G ~*> V ,G ~*> 0.1.0 ,G ~*> 0.1.0.0 ,G ~*> 0.1.0.0.0 ,G ~*> tick ,K ~*> G ,K ~*> I ,K ~*> T ,K ~*> U ,K ~*> V ,K ~*> 0.1.0 ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> tick ,G ~^> G ,G ~^> I ,G ~^> T ,G ~^> U ,G ~^> V ,G ~^> 0.1.0 ,G ~^> 0.1.0.0 ,G ~^> 0.1.0.0.0 ,G ~^> tick ,K ~^> G ,K ~^> I ,K ~^> T ,K ~^> U ,K ~^> V ,K ~^> 0.1.0 ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> tick] + f5> [I ~=> V ,P ~=> H ,P ~=> Q ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,G ~+> G ,G ~+> U ,G ~+> 0.1.0 ,G ~+> 0.1.0.0 ,G ~+> 0.1.0.0.0 ,G ~+> tick ,I ~+> I ,I ~+> T ,I ~+> V ,tick ~+> tick ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U ,K ~+> V ,K ~+> 0.1.0 ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,G ~*> G ,G ~*> I ,G ~*> T ,G ~*> U ,G ~*> V ,G ~*> 0.1.0.0 ,G ~*> 0.1.0.0.0 ,G ~*> tick ,K ~*> G ,K ~*> I ,K ~*> T ,K ~*> U ,K ~*> V ,K ~*> 0.1.0.0 ,K ~*> 0.1.0.0.0 ,K ~*> tick ,G ~^> G ,G ~^> I ,G ~^> T ,G ~^> U ,G ~^> V ,G ~^> 0.1.0.0 ,G ~^> 0.1.0.0.0 ,G ~^> tick ,K ~^> G ,K ~^> I ,K ~^> T ,K ~^> U ,K ~^> V ,K ~^> 0.1.0.0 ,K ~^> 0.1.0.0.0 ,K ~^> tick] + f5> [I ~=> V ,P ~=> H ,P ~=> Q ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,G ~+> G ,G ~+> U ,G ~+> 0.1.0.0 ,G ~+> 0.1.0.0.0 ,G ~+> tick ,I ~+> I ,I ~+> T ,I ~+> V ,tick ~+> tick ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U ,K ~+> V ,K ~+> 0.1.0.0 ,K ~+> 0.1.0.0.0 ,K ~+> tick ,G ~*> G ,G ~*> I ,G ~*> T ,G ~*> U ,G ~*> V ,G ~*> 0.1.0.0.0 ,G ~*> tick ,K ~*> G ,K ~*> I ,K ~*> T ,K ~*> U ,K ~*> V ,K ~*> 0.1.0.0.0 ,K ~*> tick ,G ~^> G ,K ~^> G] + f5> [I ~=> V ,P ~=> H ,P ~=> Q ,P ~=> R ,R ~=> H ,R ~=> Q ,K ~=> J ,huge ~=> H ,huge ~=> K ,huge ~=> L ,huge ~=> N ,huge ~=> P ,huge ~=> Q ,huge ~=> R ,huge ~=> S ,G ~+> G ,G ~+> U ,G ~+> 0.1.0.0.0 ,G ~+> tick ,I ~+> I ,I ~+> T ,I ~+> V ,tick ~+> tick ,K ~+> G ,K ~+> I ,K ~+> T ,K ~+> U ,K ~+> V ,K ~+> 0.1.0.0.0 ,K ~+> tick ,G ~*> G ,G ~*> I ,K ~*> G ,K ~*> I ,K ~*> T ,K ~*> U ,K ~*> V] YES(?,O(1))