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