MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1,-1,F,F,Z1,1 + F,A2,Z1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1 [A >= 2 && Y1 >= A && B >= 0 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,2,D,Z1,-1 + Z1,G,H,I,A2,2,-1,Y1,B2,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [E >= 0 && A >= 2] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 2. f116(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f300(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1[F >= O && P = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 3. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,S,Z1,S,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B >= 0 && Q >= 1 + B] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f116(A,Z1,0,D,E,F,G,H,I,J,K,L,M,N,O,P,A2,Y1,D2,B2,R,R,E2,F2,G2,Z1,C2,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1[A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 5. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,Z1,D1,D1,-1 + Z1,-1,G1,H1,I1,J1,K1,L1,M1,N1,O1[B1 >= 0] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 6. f7(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,E2,Z,A1,B1,F2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1,P1[B1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,Q1,R1,S1,T1,U1,V1,W1,X1) 7. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,H1,W,X,Y,Z,A1,B1,D1,D1,-1 + E1,F1,0,H1,0,H1,-1 + E1,L1,M1 [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 8. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(E2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,F2,Z,A1,B1,G2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1,N1,O1 [E1 >= 0 && G1 = D1] (?,1) ,S1,T1,U1,V1,W1,X1) ,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 9. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,P1,Q1[A >= 2 && U = 0 && E = 0 && C = 1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 10. f116(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f116(A,B,1 + C,D,E,-1 + F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,U [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,1 + C,-1 + F,P1,Q1,R1,S1,T1,U1,V1,W1,X1) 11. f116(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 -> f8(A,B,1 + E1,D,E,F,G,H,I,J,K,L,M,N,F,1,Q,R,S,T,0,V,W,X,Y,Z,A1,E1,V,V,E1,F1,0,V,0,V,K1,-1,M1,N1,O1,Z1,Q1[Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) ,R1,S1,T1,U1,V1,W1,X1) ,R1,S1,T1,U1,V1,W1,X1) 12. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f1(Z1,2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Z1,S,B2,S,U,V,S,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [Z1 >= 2 && S = W] (1,1) ,S1,T1,U1,V1,W1,X1) ,P1,A2,Y1,D2,2,E2,V1,W1,X1) 13. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(F2,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,C2,H2,J2,I2,0,0,K2,L2,M2,Z,A1,B1,N2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [0 >= F2] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,Q1,G2,S1,T1,U1,V1,W1,X1) 14. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1 -> f10(1,E2,C,D,E,F,G,H,I,J,K,L,M,N,O,0,H2,I2,K2,J2,0,0,M2,N2,O2,Z,A1,B1,Q2,D2,E1,F1,B2,Z1,A2,Y1,K1,L1,M1 [S = 0 && W = 0] (1,1) ,S1,T1,U1,V1,W1,X1) ,N1,O1,P1,G2,C2,L2,T1,U1,F2,G2,P2) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [0->{2,10,11},1->{2,10,11},2->{},3->{3,4},4->{2,10,11},5->{7,8},6->{},7->{7,8},8->{},9->{7,8},10->{2,10 ,11},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: ArgumentFilter [3,6,7,8,9,10,11,12,13,17,19,23,24,25,26,28,31,36,37,39,40,41,42,43,44,45,46,47,48,49] + Details: We remove following argument positions: [3 ,6 ,7 ,8 ,9 ,10 ,11 ,12 ,13 ,17 ,19 ,23 ,24 ,25 ,26 ,28 ,31 ,36 ,37 ,39 ,40 ,41 ,42 ,43 ,44 ,45 ,46 ,47 ,48 ,49]. * Step 2: UnreachableRules MAYBE + Considered Problem: Rules: 0. f12(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,B,1,F,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) [A >= 2 && Y1 >= A && B >= 0 && C = 1] (?,1) 1. f13(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,B,2,Z1,-1 + Z1,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) [E >= 0 && A >= 2] (?,1) 2. f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f300(A,B,C,E,F,O,1,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) [F >= O && P = 1] (?,1) 3. f1(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) [B >= 0 && Q >= 1 + B] (?,1) 4. f1(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1,H1,I1,J1,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) 5. f7(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,C,E,F,O,P,Q,S,U,V,W,Z1,D1,-1 + Z1,G1,H1,I1,J1,M1) [B1 >= 0] (?,1) 6. f7(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D2,E1,B2,Z1,A2,Y1,M1) [B1 >= 0 && G1 = D1] (?,1) 7. f8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0,H1,0,H1,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) 8. f8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(E2,B,C,E,F,O,P,Q,S,U,V,W,B1,D2,E1,B2,Z1,A2,Y1,M1) [E1 >= 0 && G1 = D1] (?,1) 9. f13(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,1 + E1,0,F,O,P,Q,S,0,V,W,E1,V,E1,0,V,0,V,M1) [A >= 2 && U = 0 && E = 0 && C = 1] (?,1) 10. f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,B,1 + C,E,-1 + F,F,1,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,U) [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) 11. f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0,V,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) 12. f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1,I1,J1,M1) [Z1 >= 2 && S = W] (1,1) 13. f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(F2,E2,C,E,F,O,0,C2,J2,0,0,K2,B1,D2,E1,B2,Z1,A2,Y1,M1) [0 >= F2] (1,1) 14. f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(1,E2,C,E,F,O,0,H2,K2,0,0,M2,B1,D2,E1,B2,Z1,A2,Y1,M1) [S = 0 && W = 0] (1,1) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [0->{2,10,11},1->{2,10,11},2->{},3->{3,4},4->{2,10,11},5->{7,8},6->{},7->{7,8},8->{},9->{7,8},10->{2,10 ,11},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [0,1,5,6,9] * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 2. f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f300(A,B,C,E,F,O,1,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) [F >= O && P = 1] (?,1) 3. f1(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) [B >= 0 && Q >= 1 + B] (?,1) 4. f1(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1,H1,I1,J1,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) 7. f8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0,H1,0,H1,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) 8. f8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(E2,B,C,E,F,O,P,Q,S,U,V,W,B1,D2,E1,B2,Z1,A2,Y1,M1) [E1 >= 0 && G1 = D1] (?,1) 10. f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,B,1 + C,E,-1 + F,F,1,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,U) [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) 11. f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0,V,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) 12. f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1,I1,J1,M1) [Z1 >= 2 && S = W] (1,1) 13. f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(F2,E2,C,E,F,O,0,C2,J2,0,0,K2,B1,D2,E1,B2,Z1,A2,Y1,M1) [0 >= F2] (1,1) 14. f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(1,E2,C,E,F,O,0,H2,K2,0,0,M2,B1,D2,E1,B2,Z1,A2,Y1,M1) [S = 0 && W = 0] (1,1) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [2->{},3->{3,4},4->{2,10,11},7->{7,8},8->{},10->{2,10,11},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(10,2),(10,10),(10,11)] * Step 4: FromIts MAYBE + Considered Problem: Rules: 2. f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f300(A,B,C,E,F,O,1,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) [F >= O && P = 1] (?,1) 3. f1(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) [B >= 0 && Q >= 1 + B] (?,1) 4. f1(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1,H1,I1,J1,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] (?,1) 7. f8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0,H1,0,H1,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] (?,1) 8. f8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(E2,B,C,E,F,O,P,Q,S,U,V,W,B1,D2,E1,B2,Z1,A2,Y1,M1) [E1 >= 0 && G1 = D1] (?,1) 10. f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,B,1 + C,E,-1 + F,F,1,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,U) [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] (?,1) 11. f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0,V,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] (?,1) 12. f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1,I1,J1,M1) [Z1 >= 2 && S = W] (1,1) 13. f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(F2,E2,C,E,F,O,0,C2,J2,0,0,K2,B1,D2,E1,B2,Z1,A2,Y1,M1) [0 >= F2] (1,1) 14. f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(1,E2,C,E,F,O,0,H2,K2,0,0,M2,B1,D2,E1,B2,Z1,A2,Y1,M1) [S = 0 && W = 0] (1,1) Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Flow Graph: [2->{},3->{3,4},4->{2,10,11},7->{7,8},8->{},10->{},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: FromIts + Details: () * Step 5: Unfold MAYBE + Considered Problem: Rules: f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f300(A,B,C,E,F,O,1,Q,S,U,V,W,B1,D1,E1,G1,H1,I1 ,J1 ,M1) [F >= O && P = 1] f1(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1,H1,I1 ,J1 ,M1) [B >= 0 && Q >= 1 + B] f1(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1,H1,I1 ,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0,H1,0 ,H1 ,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] f8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(E2,B,C,E,F,O,P,Q,S,U,V,W,B1,D2,E1,B2,Z1,A2,Y1 ,M1) [E1 >= 0 && G1 = D1] f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116(A,B,1 + C,E,-1 + F,F,1,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,U) [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] f116(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0,V ,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1,I1,J1 ,M1) [Z1 >= 2 && S = W] f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(F2,E2,C,E,F,O,0,C2,J2,0,0,K2,B1,D2,E1,B2,Z1,A2 ,Y1 ,M1) [0 >= F2] f9(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10(1,E2,C,E,F,O,0,H2,K2,0,0,M2,B1,D2,E1,B2,Z1,A2 ,Y1 ,M1) [S = 0 && W = 0] Signature: {(f1,50);(f10,50);(f116,50);(f12,50);(f13,50);(f300,50);(f7,50);(f8,50);(f9,50)} Rule Graph: [2->{},3->{3,4},4->{2,10,11},7->{7,8},8->{},10->{},11->{7,8},12->{3,4},13->{},14->{}] + Applied Processor: Unfold + Details: () * Step 6: AddSinks MAYBE + Considered Problem: Rules: f116.2(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f300.15(A,B,C,E,F,O,1,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [F >= O && P = 1] f1.3(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.3(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [B >= 0 && Q >= 1 + B] f1.3(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.4(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [B >= 0 && Q >= 1 + B] f1.4(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.2(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f1.4(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.10(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f1.4(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.11(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f8.7(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.7(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0 ,H1,0,H1 ,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] f8.7(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.8(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0 ,H1,0,H1 ,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] f8.8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10.15(E2,B,C,E,F,O,P,Q,S,U,V,W,B1,D2,E1,B2,Z1 ,A2,Y1 ,M1) [E1 >= 0 && G1 = D1] f116.10(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.15(A,B,1 + C,E,-1 + F,F,1,Q,S,U,V,W,B1,D1 ,E1,G1,H1,I1,J1 ,U) [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] f116.11(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.7(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0 ,V ,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] f116.11(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.8(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0 ,V ,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] f9.12(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.3(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1 ,I1,J1 ,M1) [Z1 >= 2 && S = W] f9.12(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.4(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1 ,I1,J1 ,M1) [Z1 >= 2 && S = W] f9.13(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10.15(F2,E2,C,E,F,O,0,C2,J2,0,0,K2,B1,D2,E1,B2 ,Z1,A2,Y1 ,M1) [0 >= F2] f9.14(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10.15(1,E2,C,E,F,O,0,H2,K2,0,0,M2,B1,D2,E1,B2 ,Z1,A2,Y1 ,M1) [S = 0 && W = 0] Signature: {(f1.3,20) ;(f1.4,20) ;(f10.15,20) ;(f116.10,20) ;(f116.11,20) ;(f116.15,20) ;(f116.2,20) ;(f300.15,20) ;(f8.7,20) ;(f8.8,20) ;(f9.12,20) ;(f9.13,20) ;(f9.14,20)} Rule Graph: [0->{},1->{1,2},2->{3,4,5},3->{0},4->{9},5->{10,11},6->{6,7},7->{8},8->{},9->{},10->{6,7},11->{8},12->{1 ,2},13->{3,4,5},14->{},15->{}] + Applied Processor: AddSinks + Details: () * Step 7: Decompose MAYBE + Considered Problem: Rules: f116.2(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f300.15(A,B,C,E,F,O,1,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [F >= O && P = 1] f1.3(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.3(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [B >= 0 && Q >= 1 + B] f1.3(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.4(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [B >= 0 && Q >= 1 + B] f1.4(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.2(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f1.4(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.10(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f1.4(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.11(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f8.7(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.7(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0 ,H1,0,H1 ,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] f8.7(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.8(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0 ,H1,0,H1 ,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] f8.8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10.15(E2,B,C,E,F,O,P,Q,S,U,V,W,B1,D2,E1,B2,Z1 ,A2,Y1 ,M1) [E1 >= 0 && G1 = D1] f116.10(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.15(A,B,1 + C,E,-1 + F,F,1,Q,S,U,V,W,B1,D1 ,E1,G1,H1,I1,J1 ,U) [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] f116.11(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.7(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0 ,V ,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] f116.11(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.8(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0 ,V ,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] f9.12(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.3(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1 ,I1,J1 ,M1) [Z1 >= 2 && S = W] f9.12(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.4(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1 ,I1,J1 ,M1) [Z1 >= 2 && S = W] f9.13(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10.15(F2,E2,C,E,F,O,0,C2,J2,0,0,K2,B1,D2,E1,B2 ,Z1,A2,Y1 ,M1) [0 >= F2] f9.14(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10.15(1,E2,C,E,F,O,0,H2,K2,0,0,M2,B1,D2,E1,B2 ,Z1,A2,Y1 ,M1) [S = 0 && W = 0] f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f116.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f300.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f116.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f300.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True Signature: {(exitus616,20) ;(f1.3,20) ;(f1.4,20) ;(f10.15,20) ;(f116.10,20) ;(f116.11,20) ;(f116.15,20) ;(f116.2,20) ;(f300.15,20) ;(f8.7,20) ;(f8.8,20) ;(f9.12,20) ;(f9.13,20) ;(f9.14,20)} Rule Graph: [0->{21,25},1->{1,2},2->{3,4,5},3->{0},4->{9},5->{10,11},6->{6,7},7->{8},8->{18,19,22,23},9->{20,24} ,10->{6,7},11->{8},12->{1,2},13->{3,4,5},14->{17},15->{16}] + Applied Processor: Decompose Greedy + 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,19,20,21,22,23,24,25] | +- p:[1] c: [1] | `- p:[6] c: [6] * Step 8: AbstractSize MAYBE + Considered Problem: (Rules: f116.2(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f300.15(A,B,C,E,F,O,1,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [F >= O && P = 1] f1.3(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.3(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [B >= 0 && Q >= 1 + B] f1.3(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.4(A,1 + B,C,E,F,O,P,Q,Z1,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [B >= 0 && Q >= 1 + B] f1.4(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.2(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f1.4(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.10(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f1.4(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.11(A,Z1,0,E,F,O,P,A2,D2,R,R,E2,B1,D1,E1,G1 ,H1,I1,J1 ,M1) [A >= 2 && C2 >= A && F >= A && B >= Q && B >= 0 && C = 0] f8.7(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.7(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0 ,H1,0,H1 ,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] f8.7(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.8(A,B,C,E,F,O,P,Q,S,0,H1,W,B1,D1,-1 + E1,0 ,H1,0,H1 ,M1) [E1 >= 0 && A >= 2 && I1 = 0 && H1 = V && G1 = 0 && U = 0 && J1 = V] f8.8(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10.15(E2,B,C,E,F,O,P,Q,S,U,V,W,B1,D2,E1,B2,Z1 ,A2,Y1 ,M1) [E1 >= 0 && G1 = D1] f116.10(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f116.15(A,B,1 + C,E,-1 + F,F,1,Q,S,U,V,W,B1,D1 ,E1,G1,H1,I1,J1 ,U) [A >= 2 && C >= 0 && F >= 0 && P = 0 && U = M1] f116.11(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.7(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0 ,V ,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] f116.11(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f8.8(A,B,1 + E1,E,F,F,1,Q,S,0,V,W,E1,V,E1,0,V,0 ,V ,M1) [Z1 >= 0 && A >= 2 && C >= 0 && F >= 0 && U = 0 && P = 0] f9.12(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.3(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1 ,I1,J1 ,M1) [Z1 >= 2 && S = W] f9.12(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f1.4(Z1,2,C,E,F,O,0,Z1,B2,U,V,S,B1,D1,E1,G1,H1 ,I1,J1 ,M1) [Z1 >= 2 && S = W] f9.13(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10.15(F2,E2,C,E,F,O,0,C2,J2,0,0,K2,B1,D2,E1,B2 ,Z1,A2,Y1 ,M1) [0 >= F2] f9.14(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> f10.15(1,E2,C,E,F,O,0,H2,K2,0,0,M2,B1,D2,E1,B2 ,Z1,A2,Y1 ,M1) [S = 0 && W = 0] f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f116.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f300.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f10.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f116.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True f300.15(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1) -> exitus616(A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1 ,H1,I1,J1 ,M1) True Signature: {(exitus616,20) ;(f1.3,20) ;(f1.4,20) ;(f10.15,20) ;(f116.10,20) ;(f116.11,20) ;(f116.15,20) ;(f116.2,20) ;(f300.15,20) ;(f8.7,20) ;(f8.8,20) ;(f9.12,20) ;(f9.13,20) ;(f9.14,20)} Rule Graph: [0->{21,25},1->{1,2},2->{3,4,5},3->{0},4->{9},5->{10,11},6->{6,7},7->{8},8->{18,19,22,23},9->{20,24} ,10->{6,7},11->{8},12->{1,2},13->{3,4,5},14->{17},15->{16}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25] | +- p:[1] c: [1] | `- p:[6] c: [6]) + Applied Processor: AbstractSize Minimize + Details: () * Step 9: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1,0.0,0.1] f116.2 ~> f300.15 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= K, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f1.3 ~> f1.3 [A <= A, B <= Q, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= unknown, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f1.3 ~> f1.4 [A <= A, B <= Q, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= unknown, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f1.4 ~> f116.2 [A <= A, B <= unknown, C <= 0*K, E <= E, F <= F, O <= O, P <= P, Q <= unknown, S <= unknown, U <= unknown, V <= unknown, W <= unknown, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f1.4 ~> f116.10 [A <= A, B <= unknown, C <= 0*K, E <= E, F <= F, O <= O, P <= P, Q <= unknown, S <= unknown, U <= unknown, V <= unknown, W <= unknown, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f1.4 ~> f116.11 [A <= A, B <= unknown, C <= 0*K, E <= E, F <= F, O <= O, P <= P, Q <= unknown, S <= unknown, U <= unknown, V <= unknown, W <= unknown, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f8.7 ~> f8.7 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= 0*K, V <= H1, W <= W, B1 <= B1, D1 <= D1, E1 <= K + E1, G1 <= 0*K, H1 <= H1, I1 <= 0*K, J1 <= H1, M1 <= M1] f8.7 ~> f8.8 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= 0*K, V <= H1, W <= W, B1 <= B1, D1 <= D1, E1 <= K + E1, G1 <= 0*K, H1 <= H1, I1 <= 0*K, J1 <= H1, M1 <= M1] f8.8 ~> f10.15 [A <= unknown, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= unknown, E1 <= E1, G1 <= unknown, H1 <= unknown, I1 <= unknown, J1 <= unknown, M1 <= M1] f116.10 ~> f116.15 [A <= A, B <= B, C <= K + C, E <= E, F <= K + F, O <= F, P <= K, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= U] f116.11 ~> f8.7 [A <= A, B <= B, C <= K + E1, E <= E, F <= F, O <= F, P <= K, Q <= Q, S <= S, U <= 0*K, V <= V, W <= W, B1 <= E1, D1 <= V, E1 <= E1, G1 <= 0*K, H1 <= V, I1 <= 0*K, J1 <= V, M1 <= M1] f116.11 ~> f8.8 [A <= A, B <= B, C <= K + E1, E <= E, F <= F, O <= F, P <= K, Q <= Q, S <= S, U <= 0*K, V <= V, W <= W, B1 <= E1, D1 <= V, E1 <= E1, G1 <= 0*K, H1 <= V, I1 <= 0*K, J1 <= V, M1 <= M1] f9.12 ~> f1.3 [A <= unknown, B <= 2*K, C <= C, E <= E, F <= F, O <= O, P <= 0*K, Q <= unknown, S <= unknown, U <= U, V <= V, W <= S, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f9.12 ~> f1.4 [A <= unknown, B <= 2*K, C <= C, E <= E, F <= F, O <= O, P <= 0*K, Q <= unknown, S <= unknown, U <= U, V <= V, W <= S, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f9.13 ~> f10.15 [A <= unknown, B <= unknown, C <= C, E <= E, F <= F, O <= O, P <= 0*K, Q <= unknown, S <= unknown, U <= 0*K, V <= 0*K, W <= unknown, B1 <= B1, D1 <= unknown, E1 <= E1, G1 <= unknown, H1 <= unknown, I1 <= unknown, J1 <= unknown, M1 <= M1] f9.14 ~> f10.15 [A <= K, B <= unknown, C <= C, E <= E, F <= F, O <= O, P <= 0*K, Q <= unknown, S <= unknown, U <= 0*K, V <= 0*K, W <= unknown, B1 <= B1, D1 <= unknown, E1 <= E1, G1 <= unknown, H1 <= unknown, I1 <= unknown, J1 <= unknown, M1 <= M1] f10.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f10.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f10.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f10.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f116.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f300.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f10.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f10.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f116.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] f300.15 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] + Loop: [0.0 <= K + B + Q] f1.3 ~> f1.3 [A <= A, B <= Q, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= unknown, U <= U, V <= V, W <= W, B1 <= B1, D1 <= D1, E1 <= E1, G1 <= G1, H1 <= H1, I1 <= I1, J1 <= J1, M1 <= M1] + Loop: [0.1 <= E1] f8.7 ~> f8.7 [A <= A, B <= B, C <= C, E <= E, F <= F, O <= O, P <= P, Q <= Q, S <= S, U <= 0*K, V <= H1, W <= W, B1 <= B1, D1 <= D1, E1 <= K + E1, G1 <= 0*K, H1 <= H1, I1 <= 0*K, J1 <= H1, M1 <= M1] + Applied Processor: AbstractFlow + Details: () * Step 10: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,E,F,O,P,Q,S,U,V,W,B1,D1,E1,G1,H1,I1,J1,M1,0.0,0.1] f116.2 ~> f300.15 [K ~=> P] f1.3 ~> f1.3 [Q ~=> B,huge ~=> S] f1.3 ~> f1.4 [Q ~=> B,huge ~=> S] f1.4 ~> f116.2 [K ~=> C,huge ~=> B,huge ~=> Q,huge ~=> S,huge ~=> U,huge ~=> V,huge ~=> W] f1.4 ~> f116.10 [K ~=> C,huge ~=> B,huge ~=> Q,huge ~=> S,huge ~=> U,huge ~=> V,huge ~=> W] f1.4 ~> f116.11 [K ~=> C,huge ~=> B,huge ~=> Q,huge ~=> S,huge ~=> U,huge ~=> V,huge ~=> W] f8.7 ~> f8.7 [H1 ~=> J1,H1 ~=> V,K ~=> G1,K ~=> I1,K ~=> U,E1 ~+> E1,K ~+> E1] f8.7 ~> f8.8 [H1 ~=> J1,H1 ~=> V,K ~=> G1,K ~=> I1,K ~=> U,E1 ~+> E1,K ~+> E1] f8.8 ~> f10.15 [huge ~=> A,huge ~=> D1,huge ~=> G1,huge ~=> H1,huge ~=> I1,huge ~=> J1] f116.10 ~> f116.15 [F ~=> O,U ~=> M1,K ~=> P,C ~+> C,F ~+> F,K ~+> C,K ~+> F] f116.11 ~> f8.7 [E1 ~=> B1 ,F ~=> O ,V ~=> D1 ,V ~=> H1 ,V ~=> J1 ,K ~=> G1 ,K ~=> I1 ,K ~=> P ,K ~=> U ,E1 ~+> C ,K ~+> C] f116.11 ~> f8.8 [E1 ~=> B1 ,F ~=> O ,V ~=> D1 ,V ~=> H1 ,V ~=> J1 ,K ~=> G1 ,K ~=> I1 ,K ~=> P ,K ~=> U ,E1 ~+> C ,K ~+> C] f9.12 ~> f1.3 [S ~=> W,K ~=> B,K ~=> P,huge ~=> A,huge ~=> Q,huge ~=> S] f9.12 ~> f1.4 [S ~=> W,K ~=> B,K ~=> P,huge ~=> A,huge ~=> Q,huge ~=> S] f9.13 ~> f10.15 [K ~=> P ,K ~=> U ,K ~=> V ,huge ~=> A ,huge ~=> B ,huge ~=> D1 ,huge ~=> G1 ,huge ~=> H1 ,huge ~=> I1 ,huge ~=> J1 ,huge ~=> Q ,huge ~=> S ,huge ~=> W] f9.14 ~> f10.15 [K ~=> A ,K ~=> P ,K ~=> U ,K ~=> V ,huge ~=> B ,huge ~=> D1 ,huge ~=> G1 ,huge ~=> H1 ,huge ~=> I1 ,huge ~=> J1 ,huge ~=> Q ,huge ~=> S ,huge ~=> W] f10.15 ~> exitus616 [] f10.15 ~> exitus616 [] f10.15 ~> exitus616 [] f10.15 ~> exitus616 [] f116.15 ~> exitus616 [] f300.15 ~> exitus616 [] f10.15 ~> exitus616 [] f10.15 ~> exitus616 [] f116.15 ~> exitus616 [] f300.15 ~> exitus616 [] + Loop: [B ~+> 0.0,Q ~+> 0.0,K ~+> 0.0] f1.3 ~> f1.3 [Q ~=> B,huge ~=> S] + Loop: [E1 ~=> 0.1] f8.7 ~> f8.7 [H1 ~=> J1,H1 ~=> V,K ~=> G1,K ~=> I1,K ~=> U,E1 ~+> E1,K ~+> E1] + Applied Processor: Lare + Details: Unknown bound. MAYBE