YES(?,O(1)) * Step 1: ArgumentFilter WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,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) -> f422(3,43690,3,Q1,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 True (1,1) ,O1,P1) 1. f422(A,B,C,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) -> f422(A,B,Q1,R1,1 + 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[149 >= E] (?,1) ,O1,P1) 2. f437(A,B,C,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) -> f441(A,B,C,D,E,F,0,0,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 [49 >= F] (?,1) ,P1) 3. f441(A,B,C,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) -> f441(A,B,C,D,E,F,Q1,1 + 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 [49 >= H] (?,1) ,O1,P1) 4. f455(A,B,C,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) -> f461(A,B,C,D,E,F,G,H,I,0,0,Q1,0,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 [99 >= I] (?,1) ,P1) 5. f461(A,B,C,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) -> f461(A,B,C,D,E,F,G,H,I,Q1,R1,S1,2 + M,T1,U1,V1,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1 [31 >= M] (?,1) ,M1,N1,O1,P1) 6. f485(A,B,C,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) -> f485(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,-1 + Q,Q1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1[Q >= 0] (?,1) ,O1,P1) 7. f501(A,B,C,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) -> f501(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,1 + S,Q1,R1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1[49 >= S] (?,1) ,O1,P1) 8. f526(A,B,C,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) -> f526(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,1 + W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [V >= W] (?,1) ,O1,P1) 9. f540(A,B,C,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) -> f543(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,0,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [8 >= X] (?,1) ,P1) 10. f543(A,B,C,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) -> f546(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1 [7 >= Y] (?,1) ,P1) 11. f546(A,B,C,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) -> f546(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,1 + Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [3 >= Z] (?,1) ,O1,P1) 12. f546(A,B,C,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) -> f543(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,1 + Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1 [Z >= 4] (?,1) ,O1,P1) 13. f543(A,B,C,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) -> f540(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,7 + X,Y,Z,3 + A1,3 + B1,-7 + C1,D1,E1,F1,G1,H1,I1,J1 [Y >= 8] (?,1) ,K1,L1,M1,N1,O1,P1) 14. f540(A,B,C,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) -> f584(A,B,C,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 [X >= 9] (?,1) ,P1) 15. f526(A,B,C,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) -> f540(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,1,Y,Z,0,13,8,E1,E1,E1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1) [W >= 1 + V] (?,1) 16. f501(A,B,C,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) -> f526(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,17,2,X,Y,Z,A1,B1,C1,D1,B,F1,B,1,Q1,A,1,R1,M1,N1,O1,P1) [S >= 50] (?,1) 17. f485(A,B,C,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) -> f501(A,R,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,Q1,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,R,N1,O1 [0 >= 1 + Q] (?,1) ,P1) 18. f461(A,B,C,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) -> f455(A,B,C,D,E,F,G,H,2 + 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 [M >= 32] (?,1) ,O1,P1) 19. f455(A,B,C,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) -> f485(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,98,Q1,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,100,O1[I >= 100] (?,1) ,P1) 20. f441(A,B,C,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) -> f437(A,B,C,D,E,1 + 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 [H >= 50] (?,1) ,O1,P1) 21. f437(A,B,C,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) -> f455(A,B,C,D,E,F,G,H,0,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 [F >= 50] (?,1) ,P1) 22. f422(A,B,C,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) -> f437(C,B,C,D,E,0,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,C,C) [E >= 150] (?,1) Signature: {(f0,42) ;(f422,42) ;(f437,42) ;(f441,42) ;(f455,42) ;(f461,42) ;(f485,42) ;(f501,42) ;(f526,42) ;(f540,42) ;(f543,42) ;(f546,42) ;(f584,42)} Flow Graph: [0->{1,22},1->{1,22},2->{3,20},3->{3,20},4->{5,18},5->{5,18},6->{6,17},7->{7,16},8->{8,15},9->{10,13} ,10->{11,12},11->{11,12},12->{10,13},13->{9,14},14->{},15->{9,14},16->{8,15},17->{7,16},18->{4,19},19->{6 ,17},20->{2,21},21->{4,19},22->{2,21}] + Applied Processor: ArgumentFilter [0,1,2,3,6,9,10,11,13,14,15,17,19,20,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41] + Details: We remove following argument positions: [0 ,1 ,2 ,3 ,6 ,9 ,10 ,11 ,13 ,14 ,15 ,17 ,19 ,20 ,26 ,27 ,28 ,29 ,30 ,31 ,32 ,33 ,34 ,35 ,36 ,37 ,38 ,39 ,40 ,41]. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422(0,F,H,I,M,Q,S,V,W,X,Y,Z) True (1,1) 1. f422(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422(1 + E,F,H,I,M,Q,S,V,W,X,Y,Z) [149 >= E] (?,1) 2. f437(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441(E,F,0,I,M,Q,S,V,W,X,Y,Z) [49 >= F] (?,1) 3. f441(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441(E,F,1 + H,I,M,Q,S,V,W,X,Y,Z) [49 >= H] (?,1) 4. f455(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461(E,F,H,I,0,Q,S,V,W,X,Y,Z) [99 >= I] (?,1) 5. f461(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461(E,F,H,I,2 + M,Q,S,V,W,X,Y,Z) [31 >= M] (?,1) 6. f485(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485(E,F,H,I,M,-1 + Q,S,V,W,X,Y,Z) [Q >= 0] (?,1) 7. f501(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501(E,F,H,I,M,Q,1 + S,V,W,X,Y,Z) [49 >= S] (?,1) 8. f526(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526(E,F,H,I,M,Q,S,V,1 + W,X,Y,Z) [V >= W] (?,1) 9. f540(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543(E,F,H,I,M,Q,S,V,W,X,0,Z) [8 >= X] (?,1) 10. f543(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546(E,F,H,I,M,Q,S,V,W,X,Y,0) [7 >= Y] (?,1) 11. f546(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546(E,F,H,I,M,Q,S,V,W,X,Y,1 + Z) [3 >= Z] (?,1) 12. f546(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543(E,F,H,I,M,Q,S,V,W,X,1 + Y,Z) [Z >= 4] (?,1) 13. f543(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540(E,F,H,I,M,Q,S,V,W,7 + X,Y,Z) [Y >= 8] (?,1) 14. f540(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f584(E,F,H,I,M,Q,S,V,W,X,Y,Z) [X >= 9] (?,1) 15. f526(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540(E,F,H,I,M,Q,S,V,W,1,Y,Z) [W >= 1 + V] (?,1) 16. f501(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526(E,F,H,I,M,Q,S,17,2,X,Y,Z) [S >= 50] (?,1) 17. f485(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501(E,F,H,I,M,Q,0,V,W,X,Y,Z) [0 >= 1 + Q] (?,1) 18. f461(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455(E,F,H,2 + I,M,Q,S,V,W,X,Y,Z) [M >= 32] (?,1) 19. f455(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485(E,F,H,I,M,98,S,V,W,X,Y,Z) [I >= 100] (?,1) 20. f441(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437(E,1 + F,H,I,M,Q,S,V,W,X,Y,Z) [H >= 50] (?,1) 21. f437(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455(E,F,H,0,M,Q,S,V,W,X,Y,Z) [F >= 50] (?,1) 22. f422(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437(E,0,H,I,M,Q,S,V,W,X,Y,Z) [E >= 150] (?,1) Signature: {(f0,42) ;(f422,42) ;(f437,42) ;(f441,42) ;(f455,42) ;(f461,42) ;(f485,42) ;(f501,42) ;(f526,42) ;(f540,42) ;(f543,42) ;(f546,42) ;(f584,42)} Flow Graph: [0->{1,22},1->{1,22},2->{3,20},3->{3,20},4->{5,18},5->{5,18},6->{6,17},7->{7,16},8->{8,15},9->{10,13} ,10->{11,12},11->{11,12},12->{10,13},13->{9,14},14->{},15->{9,14},16->{8,15},17->{7,16},18->{4,19},19->{6 ,17},20->{2,21},21->{4,19},22->{2,21}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,22) ,(2,20) ,(4,18) ,(9,13) ,(10,12) ,(15,14) ,(16,15) ,(17,16) ,(19,17) ,(21,19) ,(22,21)] * Step 3: FromIts WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422(0,F,H,I,M,Q,S,V,W,X,Y,Z) True (1,1) 1. f422(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422(1 + E,F,H,I,M,Q,S,V,W,X,Y,Z) [149 >= E] (?,1) 2. f437(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441(E,F,0,I,M,Q,S,V,W,X,Y,Z) [49 >= F] (?,1) 3. f441(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441(E,F,1 + H,I,M,Q,S,V,W,X,Y,Z) [49 >= H] (?,1) 4. f455(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461(E,F,H,I,0,Q,S,V,W,X,Y,Z) [99 >= I] (?,1) 5. f461(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461(E,F,H,I,2 + M,Q,S,V,W,X,Y,Z) [31 >= M] (?,1) 6. f485(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485(E,F,H,I,M,-1 + Q,S,V,W,X,Y,Z) [Q >= 0] (?,1) 7. f501(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501(E,F,H,I,M,Q,1 + S,V,W,X,Y,Z) [49 >= S] (?,1) 8. f526(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526(E,F,H,I,M,Q,S,V,1 + W,X,Y,Z) [V >= W] (?,1) 9. f540(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543(E,F,H,I,M,Q,S,V,W,X,0,Z) [8 >= X] (?,1) 10. f543(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546(E,F,H,I,M,Q,S,V,W,X,Y,0) [7 >= Y] (?,1) 11. f546(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546(E,F,H,I,M,Q,S,V,W,X,Y,1 + Z) [3 >= Z] (?,1) 12. f546(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543(E,F,H,I,M,Q,S,V,W,X,1 + Y,Z) [Z >= 4] (?,1) 13. f543(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540(E,F,H,I,M,Q,S,V,W,7 + X,Y,Z) [Y >= 8] (?,1) 14. f540(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f584(E,F,H,I,M,Q,S,V,W,X,Y,Z) [X >= 9] (?,1) 15. f526(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540(E,F,H,I,M,Q,S,V,W,1,Y,Z) [W >= 1 + V] (?,1) 16. f501(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526(E,F,H,I,M,Q,S,17,2,X,Y,Z) [S >= 50] (?,1) 17. f485(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501(E,F,H,I,M,Q,0,V,W,X,Y,Z) [0 >= 1 + Q] (?,1) 18. f461(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455(E,F,H,2 + I,M,Q,S,V,W,X,Y,Z) [M >= 32] (?,1) 19. f455(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485(E,F,H,I,M,98,S,V,W,X,Y,Z) [I >= 100] (?,1) 20. f441(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437(E,1 + F,H,I,M,Q,S,V,W,X,Y,Z) [H >= 50] (?,1) 21. f437(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455(E,F,H,0,M,Q,S,V,W,X,Y,Z) [F >= 50] (?,1) 22. f422(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437(E,0,H,I,M,Q,S,V,W,X,Y,Z) [E >= 150] (?,1) Signature: {(f0,42) ;(f422,42) ;(f437,42) ;(f441,42) ;(f455,42) ;(f461,42) ;(f485,42) ;(f501,42) ;(f526,42) ;(f540,42) ;(f543,42) ;(f546,42) ;(f584,42)} Flow Graph: [0->{1},1->{1,22},2->{3},3->{3,20},4->{5},5->{5,18},6->{6,17},7->{7,16},8->{8,15},9->{10},10->{11},11->{11 ,12},12->{10,13},13->{9,14},14->{},15->{9},16->{8},17->{7},18->{4,19},19->{6},20->{2,21},21->{4},22->{2}] + Applied Processor: FromIts + Details: () * Step 4: Unfold WORST_CASE(?,O(1)) + Considered Problem: Rules: f0(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422(0,F,H,I,M,Q,S,V,W,X,Y,Z) True f422(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422(1 + E,F,H,I,M,Q,S,V,W,X,Y,Z) [149 >= E] f437(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441(E,F,0,I,M,Q,S,V,W,X,Y,Z) [49 >= F] f441(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441(E,F,1 + H,I,M,Q,S,V,W,X,Y,Z) [49 >= H] f455(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461(E,F,H,I,0,Q,S,V,W,X,Y,Z) [99 >= I] f461(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461(E,F,H,I,2 + M,Q,S,V,W,X,Y,Z) [31 >= M] f485(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485(E,F,H,I,M,-1 + Q,S,V,W,X,Y,Z) [Q >= 0] f501(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501(E,F,H,I,M,Q,1 + S,V,W,X,Y,Z) [49 >= S] f526(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526(E,F,H,I,M,Q,S,V,1 + W,X,Y,Z) [V >= W] f540(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543(E,F,H,I,M,Q,S,V,W,X,0,Z) [8 >= X] f543(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546(E,F,H,I,M,Q,S,V,W,X,Y,0) [7 >= Y] f546(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546(E,F,H,I,M,Q,S,V,W,X,Y,1 + Z) [3 >= Z] f546(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543(E,F,H,I,M,Q,S,V,W,X,1 + Y,Z) [Z >= 4] f543(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540(E,F,H,I,M,Q,S,V,W,7 + X,Y,Z) [Y >= 8] f540(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f584(E,F,H,I,M,Q,S,V,W,X,Y,Z) [X >= 9] f526(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540(E,F,H,I,M,Q,S,V,W,1,Y,Z) [W >= 1 + V] f501(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526(E,F,H,I,M,Q,S,17,2,X,Y,Z) [S >= 50] f485(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501(E,F,H,I,M,Q,0,V,W,X,Y,Z) [0 >= 1 + Q] f461(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455(E,F,H,2 + I,M,Q,S,V,W,X,Y,Z) [M >= 32] f455(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485(E,F,H,I,M,98,S,V,W,X,Y,Z) [I >= 100] f441(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437(E,1 + F,H,I,M,Q,S,V,W,X,Y,Z) [H >= 50] f437(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455(E,F,H,0,M,Q,S,V,W,X,Y,Z) [F >= 50] f422(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437(E,0,H,I,M,Q,S,V,W,X,Y,Z) [E >= 150] Signature: {(f0,42) ;(f422,42) ;(f437,42) ;(f441,42) ;(f455,42) ;(f461,42) ;(f485,42) ;(f501,42) ;(f526,42) ;(f540,42) ;(f543,42) ;(f546,42) ;(f584,42)} Rule Graph: [0->{1},1->{1,22},2->{3},3->{3,20},4->{5},5->{5,18},6->{6,17},7->{7,16},8->{8,15},9->{10},10->{11},11->{11 ,12},12->{10,13},13->{9,14},14->{},15->{9},16->{8},17->{7},18->{4,19},19->{6},20->{2,21},21->{4},22->{2}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: f0.0(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422.1(0,F,H,I,M,Q,S,V,W,X,Y,Z) True f422.1(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422.1(1 + E,F,H,I,M,Q,S,V,W,X,Y,Z) [149 >= E] f422.1(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422.22(1 + E,F,H,I,M,Q,S,V,W,X,Y,Z) [149 >= E] f437.2(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441.3(E,F,0,I,M,Q,S,V,W,X,Y,Z) [49 >= F] f441.3(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441.3(E,F,1 + H,I,M,Q,S,V,W,X,Y,Z) [49 >= H] f441.3(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441.20(E,F,1 + H,I,M,Q,S,V,W,X,Y,Z) [49 >= H] f455.4(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461.5(E,F,H,I,0,Q,S,V,W,X,Y,Z) [99 >= I] f461.5(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461.5(E,F,H,I,2 + M,Q,S,V,W,X,Y,Z) [31 >= M] f461.5(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461.18(E,F,H,I,2 + M,Q,S,V,W,X,Y,Z) [31 >= M] f485.6(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485.6(E,F,H,I,M,-1 + Q,S,V,W,X,Y,Z) [Q >= 0] f485.6(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485.17(E,F,H,I,M,-1 + Q,S,V,W,X,Y,Z) [Q >= 0] f501.7(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501.7(E,F,H,I,M,Q,1 + S,V,W,X,Y,Z) [49 >= S] f501.7(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501.16(E,F,H,I,M,Q,1 + S,V,W,X,Y,Z) [49 >= S] f526.8(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526.8(E,F,H,I,M,Q,S,V,1 + W,X,Y,Z) [V >= W] f526.8(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526.15(E,F,H,I,M,Q,S,V,1 + W,X,Y,Z) [V >= W] f540.9(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543.10(E,F,H,I,M,Q,S,V,W,X,0,Z) [8 >= X] f543.10(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546.11(E,F,H,I,M,Q,S,V,W,X,Y,0) [7 >= Y] f546.11(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546.11(E,F,H,I,M,Q,S,V,W,X,Y,1 + Z) [3 >= Z] f546.11(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546.12(E,F,H,I,M,Q,S,V,W,X,Y,1 + Z) [3 >= Z] f546.12(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543.10(E,F,H,I,M,Q,S,V,W,X,1 + Y,Z) [Z >= 4] f546.12(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543.13(E,F,H,I,M,Q,S,V,W,X,1 + Y,Z) [Z >= 4] f543.13(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540.9(E,F,H,I,M,Q,S,V,W,7 + X,Y,Z) [Y >= 8] f543.13(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540.14(E,F,H,I,M,Q,S,V,W,7 + X,Y,Z) [Y >= 8] f540.14(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f584.23(E,F,H,I,M,Q,S,V,W,X,Y,Z) [X >= 9] f526.15(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540.9(E,F,H,I,M,Q,S,V,W,1,Y,Z) [W >= 1 + V] f501.16(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526.8(E,F,H,I,M,Q,S,17,2,X,Y,Z) [S >= 50] f485.17(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501.7(E,F,H,I,M,Q,0,V,W,X,Y,Z) [0 >= 1 + Q] f461.18(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455.4(E,F,H,2 + I,M,Q,S,V,W,X,Y,Z) [M >= 32] f461.18(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455.19(E,F,H,2 + I,M,Q,S,V,W,X,Y,Z) [M >= 32] f455.19(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485.6(E,F,H,I,M,98,S,V,W,X,Y,Z) [I >= 100] f441.20(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437.2(E,1 + F,H,I,M,Q,S,V,W,X,Y,Z) [H >= 50] f441.20(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437.21(E,1 + F,H,I,M,Q,S,V,W,X,Y,Z) [H >= 50] f437.21(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455.4(E,F,H,0,M,Q,S,V,W,X,Y,Z) [F >= 50] f422.22(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437.2(E,0,H,I,M,Q,S,V,W,X,Y,Z) [E >= 150] Signature: {(f0.0,12) ;(f422.1,12) ;(f422.22,12) ;(f437.2,12) ;(f437.21,12) ;(f441.20,12) ;(f441.3,12) ;(f455.19,12) ;(f455.4,12) ;(f461.18,12) ;(f461.5,12) ;(f485.17,12) ;(f485.6,12) ;(f501.16,12) ;(f501.7,12) ;(f526.15,12) ;(f526.8,12) ;(f540.14,12) ;(f540.9,12) ;(f543.10,12) ;(f543.13,12) ;(f546.11,12) ;(f546.12,12) ;(f584.23,12)} Rule Graph: [0->{1,2},1->{1,2},2->{33},3->{4,5},4->{4,5},5->{30,31},6->{7,8},7->{7,8},8->{27,28},9->{9,10},10->{26} ,11->{11,12},12->{25},13->{13,14},14->{24},15->{16},16->{17,18},17->{17,18},18->{19,20},19->{16},20->{21,22} ,21->{15},22->{23},23->{},24->{15},25->{13,14},26->{11,12},27->{6},28->{29},29->{9,10},30->{3},31->{32} ,32->{6},33->{3}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose WORST_CASE(?,O(1)) + Considered Problem: Rules: f0.0(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422.1(0,F,H,I,M,Q,S,V,W,X,Y,Z) True f422.1(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422.1(1 + E,F,H,I,M,Q,S,V,W,X,Y,Z) [149 >= E] f422.1(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422.22(1 + E,F,H,I,M,Q,S,V,W,X,Y,Z) [149 >= E] f437.2(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441.3(E,F,0,I,M,Q,S,V,W,X,Y,Z) [49 >= F] f441.3(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441.3(E,F,1 + H,I,M,Q,S,V,W,X,Y,Z) [49 >= H] f441.3(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441.20(E,F,1 + H,I,M,Q,S,V,W,X,Y,Z) [49 >= H] f455.4(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461.5(E,F,H,I,0,Q,S,V,W,X,Y,Z) [99 >= I] f461.5(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461.5(E,F,H,I,2 + M,Q,S,V,W,X,Y,Z) [31 >= M] f461.5(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461.18(E,F,H,I,2 + M,Q,S,V,W,X,Y,Z) [31 >= M] f485.6(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485.6(E,F,H,I,M,-1 + Q,S,V,W,X,Y,Z) [Q >= 0] f485.6(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485.17(E,F,H,I,M,-1 + Q,S,V,W,X,Y,Z) [Q >= 0] f501.7(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501.7(E,F,H,I,M,Q,1 + S,V,W,X,Y,Z) [49 >= S] f501.7(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501.16(E,F,H,I,M,Q,1 + S,V,W,X,Y,Z) [49 >= S] f526.8(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526.8(E,F,H,I,M,Q,S,V,1 + W,X,Y,Z) [V >= W] f526.8(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526.15(E,F,H,I,M,Q,S,V,1 + W,X,Y,Z) [V >= W] f540.9(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543.10(E,F,H,I,M,Q,S,V,W,X,0,Z) [8 >= X] f543.10(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546.11(E,F,H,I,M,Q,S,V,W,X,Y,0) [7 >= Y] f546.11(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546.11(E,F,H,I,M,Q,S,V,W,X,Y,1 + Z) [3 >= Z] f546.11(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546.12(E,F,H,I,M,Q,S,V,W,X,Y,1 + Z) [3 >= Z] f546.12(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543.10(E,F,H,I,M,Q,S,V,W,X,1 + Y,Z) [Z >= 4] f546.12(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543.13(E,F,H,I,M,Q,S,V,W,X,1 + Y,Z) [Z >= 4] f543.13(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540.9(E,F,H,I,M,Q,S,V,W,7 + X,Y,Z) [Y >= 8] f543.13(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540.14(E,F,H,I,M,Q,S,V,W,7 + X,Y,Z) [Y >= 8] f540.14(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f584.23(E,F,H,I,M,Q,S,V,W,X,Y,Z) [X >= 9] f526.15(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540.9(E,F,H,I,M,Q,S,V,W,1,Y,Z) [W >= 1 + V] f501.16(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526.8(E,F,H,I,M,Q,S,17,2,X,Y,Z) [S >= 50] f485.17(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501.7(E,F,H,I,M,Q,0,V,W,X,Y,Z) [0 >= 1 + Q] f461.18(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455.4(E,F,H,2 + I,M,Q,S,V,W,X,Y,Z) [M >= 32] f461.18(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455.19(E,F,H,2 + I,M,Q,S,V,W,X,Y,Z) [M >= 32] f455.19(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485.6(E,F,H,I,M,98,S,V,W,X,Y,Z) [I >= 100] f441.20(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437.2(E,1 + F,H,I,M,Q,S,V,W,X,Y,Z) [H >= 50] f441.20(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437.21(E,1 + F,H,I,M,Q,S,V,W,X,Y,Z) [H >= 50] f437.21(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455.4(E,F,H,0,M,Q,S,V,W,X,Y,Z) [F >= 50] f422.22(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437.2(E,0,H,I,M,Q,S,V,W,X,Y,Z) [E >= 150] f584.23(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> exitus616(E,F,H,I,M,Q,S,V,W,X,Y,Z) True Signature: {(exitus616,12) ;(f0.0,12) ;(f422.1,12) ;(f422.22,12) ;(f437.2,12) ;(f437.21,12) ;(f441.20,12) ;(f441.3,12) ;(f455.19,12) ;(f455.4,12) ;(f461.18,12) ;(f461.5,12) ;(f485.17,12) ;(f485.6,12) ;(f501.16,12) ;(f501.7,12) ;(f526.15,12) ;(f526.8,12) ;(f540.14,12) ;(f540.9,12) ;(f543.10,12) ;(f543.13,12) ;(f546.11,12) ;(f546.12,12) ;(f584.23,12)} Rule Graph: [0->{1,2},1->{1,2},2->{33},3->{4,5},4->{4,5},5->{30,31},6->{7,8},7->{7,8},8->{27,28},9->{9,10},10->{26} ,11->{11,12},12->{25},13->{13,14},14->{24},15->{16},16->{17,18},17->{17,18},18->{19,20},19->{16},20->{21,22} ,21->{15},22->{23},23->{34},24->{15},25->{13,14},26->{11,12},27->{6},28->{29},29->{9,10},30->{3},31->{32} ,32->{6},33->{3}] + 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,26,27,28,29,30,31,32,33,34] | +- p:[1] c: [1] | +- p:[3,30,5,4] c: [3,5,30] | | | `- p:[4] c: [4] | +- p:[6,27,8,7] c: [6,8,27] | | | `- p:[7] c: [7] | +- p:[9] c: [9] | +- p:[11] c: [11] | +- p:[13] c: [13] | `- p:[15,21,20,18,16,19,17] c: [15,20,21] | `- p:[16,19,18,17] c: [16,18,19] | `- p:[17] c: [17] * Step 7: AbstractSize WORST_CASE(?,O(1)) + Considered Problem: (Rules: f0.0(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422.1(0,F,H,I,M,Q,S,V,W,X,Y,Z) True f422.1(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422.1(1 + E,F,H,I,M,Q,S,V,W,X,Y,Z) [149 >= E] f422.1(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f422.22(1 + E,F,H,I,M,Q,S,V,W,X,Y,Z) [149 >= E] f437.2(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441.3(E,F,0,I,M,Q,S,V,W,X,Y,Z) [49 >= F] f441.3(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441.3(E,F,1 + H,I,M,Q,S,V,W,X,Y,Z) [49 >= H] f441.3(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f441.20(E,F,1 + H,I,M,Q,S,V,W,X,Y,Z) [49 >= H] f455.4(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461.5(E,F,H,I,0,Q,S,V,W,X,Y,Z) [99 >= I] f461.5(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461.5(E,F,H,I,2 + M,Q,S,V,W,X,Y,Z) [31 >= M] f461.5(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f461.18(E,F,H,I,2 + M,Q,S,V,W,X,Y,Z) [31 >= M] f485.6(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485.6(E,F,H,I,M,-1 + Q,S,V,W,X,Y,Z) [Q >= 0] f485.6(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485.17(E,F,H,I,M,-1 + Q,S,V,W,X,Y,Z) [Q >= 0] f501.7(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501.7(E,F,H,I,M,Q,1 + S,V,W,X,Y,Z) [49 >= S] f501.7(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501.16(E,F,H,I,M,Q,1 + S,V,W,X,Y,Z) [49 >= S] f526.8(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526.8(E,F,H,I,M,Q,S,V,1 + W,X,Y,Z) [V >= W] f526.8(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526.15(E,F,H,I,M,Q,S,V,1 + W,X,Y,Z) [V >= W] f540.9(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543.10(E,F,H,I,M,Q,S,V,W,X,0,Z) [8 >= X] f543.10(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546.11(E,F,H,I,M,Q,S,V,W,X,Y,0) [7 >= Y] f546.11(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546.11(E,F,H,I,M,Q,S,V,W,X,Y,1 + Z) [3 >= Z] f546.11(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f546.12(E,F,H,I,M,Q,S,V,W,X,Y,1 + Z) [3 >= Z] f546.12(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543.10(E,F,H,I,M,Q,S,V,W,X,1 + Y,Z) [Z >= 4] f546.12(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f543.13(E,F,H,I,M,Q,S,V,W,X,1 + Y,Z) [Z >= 4] f543.13(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540.9(E,F,H,I,M,Q,S,V,W,7 + X,Y,Z) [Y >= 8] f543.13(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540.14(E,F,H,I,M,Q,S,V,W,7 + X,Y,Z) [Y >= 8] f540.14(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f584.23(E,F,H,I,M,Q,S,V,W,X,Y,Z) [X >= 9] f526.15(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f540.9(E,F,H,I,M,Q,S,V,W,1,Y,Z) [W >= 1 + V] f501.16(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f526.8(E,F,H,I,M,Q,S,17,2,X,Y,Z) [S >= 50] f485.17(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f501.7(E,F,H,I,M,Q,0,V,W,X,Y,Z) [0 >= 1 + Q] f461.18(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455.4(E,F,H,2 + I,M,Q,S,V,W,X,Y,Z) [M >= 32] f461.18(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455.19(E,F,H,2 + I,M,Q,S,V,W,X,Y,Z) [M >= 32] f455.19(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f485.6(E,F,H,I,M,98,S,V,W,X,Y,Z) [I >= 100] f441.20(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437.2(E,1 + F,H,I,M,Q,S,V,W,X,Y,Z) [H >= 50] f441.20(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437.21(E,1 + F,H,I,M,Q,S,V,W,X,Y,Z) [H >= 50] f437.21(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f455.4(E,F,H,0,M,Q,S,V,W,X,Y,Z) [F >= 50] f422.22(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> f437.2(E,0,H,I,M,Q,S,V,W,X,Y,Z) [E >= 150] f584.23(E,F,H,I,M,Q,S,V,W,X,Y,Z) -> exitus616(E,F,H,I,M,Q,S,V,W,X,Y,Z) True Signature: {(exitus616,12) ;(f0.0,12) ;(f422.1,12) ;(f422.22,12) ;(f437.2,12) ;(f437.21,12) ;(f441.20,12) ;(f441.3,12) ;(f455.19,12) ;(f455.4,12) ;(f461.18,12) ;(f461.5,12) ;(f485.17,12) ;(f485.6,12) ;(f501.16,12) ;(f501.7,12) ;(f526.15,12) ;(f526.8,12) ;(f540.14,12) ;(f540.9,12) ;(f543.10,12) ;(f543.13,12) ;(f546.11,12) ;(f546.12,12) ;(f584.23,12)} Rule Graph: [0->{1,2},1->{1,2},2->{33},3->{4,5},4->{4,5},5->{30,31},6->{7,8},7->{7,8},8->{27,28},9->{9,10},10->{26} ,11->{11,12},12->{25},13->{13,14},14->{24},15->{16},16->{17,18},17->{17,18},18->{19,20},19->{16},20->{21,22} ,21->{15},22->{23},23->{34},24->{15},25->{13,14},26->{11,12},27->{6},28->{29},29->{9,10},30->{3},31->{32} ,32->{6},33->{3}] ,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,26,27,28,29,30,31,32,33,34] | +- p:[1] c: [1] | +- p:[3,30,5,4] c: [3,5,30] | | | `- p:[4] c: [4] | +- p:[6,27,8,7] c: [6,8,27] | | | `- p:[7] c: [7] | +- p:[9] c: [9] | +- p:[11] c: [11] | +- p:[13] c: [13] | `- p:[15,21,20,18,16,19,17] c: [15,20,21] | `- p:[16,19,18,17] c: [16,18,19] | `- p:[17] c: [17]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [E,F,H,I,M,Q,S,V,W,X,Y,Z,0.0,0.1,0.1.0,0.2,0.2.0,0.3,0.4,0.5,0.6,0.6.0,0.6.0.0] f0.0 ~> f422.1 [E <= 0*K, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f422.1 ~> f422.1 [E <= K + E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f422.1 ~> f422.22 [E <= K + E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f437.2 ~> f441.3 [E <= E, F <= F, H <= 0*K, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f441.3 ~> f441.3 [E <= E, F <= F, H <= K + H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f441.3 ~> f441.20 [E <= E, F <= F, H <= K + H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f455.4 ~> f461.5 [E <= E, F <= F, H <= H, I <= I, M <= 0*K, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f461.5 ~> f461.5 [E <= E, F <= F, H <= H, I <= I, M <= 2*K + M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f461.5 ~> f461.18 [E <= E, F <= F, H <= H, I <= I, M <= 2*K + M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f485.6 ~> f485.6 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= K + Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f485.6 ~> f485.17 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= K + Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f501.7 ~> f501.7 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= K + S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f501.7 ~> f501.16 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= K + S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f526.8 ~> f526.8 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= K + W, X <= X, Y <= Y, Z <= Z] f526.8 ~> f526.15 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= K + W, X <= X, Y <= Y, Z <= Z] f540.9 ~> f543.10 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= 0*K, Z <= Z] f543.10 ~> f546.11 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= 0*K] f546.11 ~> f546.11 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= K + Z] f546.11 ~> f546.12 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= K + Z] f546.12 ~> f543.10 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= K + Y, Z <= Z] f546.12 ~> f543.13 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= K + Y, Z <= Z] f543.13 ~> f540.9 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= 7*K + X, Y <= Y, Z <= Z] f543.13 ~> f540.14 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= 7*K + X, Y <= Y, Z <= Z] f540.14 ~> f584.23 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f526.15 ~> f540.9 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= K, Y <= Y, Z <= Z] f501.16 ~> f526.8 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= 17*K, W <= 2*K, X <= X, Y <= Y, Z <= Z] f485.17 ~> f501.7 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= 0*K, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f461.18 ~> f455.4 [E <= E, F <= F, H <= H, I <= 2*K + I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f461.18 ~> f455.19 [E <= E, F <= F, H <= H, I <= 2*K + I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f455.19 ~> f485.6 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= 98*K, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f441.20 ~> f437.2 [E <= E, F <= K + F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f441.20 ~> f437.21 [E <= E, F <= K + F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f437.21 ~> f455.4 [E <= E, F <= F, H <= H, I <= 0*K, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f422.22 ~> f437.2 [E <= E, F <= 0*K, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f584.23 ~> exitus616 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] + Loop: [0.0 <= 149*K + E] f422.1 ~> f422.1 [E <= K + E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] + Loop: [0.1 <= 49*K + F] f437.2 ~> f441.3 [E <= E, F <= F, H <= 0*K, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f441.20 ~> f437.2 [E <= E, F <= K + F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f441.3 ~> f441.20 [E <= E, F <= F, H <= K + H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f441.3 ~> f441.3 [E <= E, F <= F, H <= K + H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] + Loop: [0.1.0 <= 49*K + H] f441.3 ~> f441.3 [E <= E, F <= F, H <= K + H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] + Loop: [0.2 <= 99*K + I] f455.4 ~> f461.5 [E <= E, F <= F, H <= H, I <= I, M <= 0*K, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f461.18 ~> f455.4 [E <= E, F <= F, H <= H, I <= 2*K + I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f461.5 ~> f461.18 [E <= E, F <= F, H <= H, I <= I, M <= 2*K + M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] f461.5 ~> f461.5 [E <= E, F <= F, H <= H, I <= I, M <= 2*K + M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] + Loop: [0.2.0 <= 31*K + M] f461.5 ~> f461.5 [E <= E, F <= F, H <= H, I <= I, M <= 2*K + M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] + Loop: [0.3 <= Q] f485.6 ~> f485.6 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= K + Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] + Loop: [0.4 <= 49*K + S] f501.7 ~> f501.7 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= K + S, V <= V, W <= W, X <= X, Y <= Y, Z <= Z] + Loop: [0.5 <= V + W] f526.8 ~> f526.8 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= K + W, X <= X, Y <= Y, Z <= Z] + Loop: [0.6 <= 8*K + X] f540.9 ~> f543.10 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= 0*K, Z <= Z] f543.13 ~> f540.9 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= 7*K + X, Y <= Y, Z <= Z] f546.12 ~> f543.13 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= K + Y, Z <= Z] f546.11 ~> f546.12 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= K + Z] f543.10 ~> f546.11 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= 0*K] f546.12 ~> f543.10 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= K + Y, Z <= Z] f546.11 ~> f546.11 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= K + Z] + Loop: [0.6.0 <= 7*K + Y] f543.10 ~> f546.11 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= 0*K] f546.12 ~> f543.10 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= K + Y, Z <= Z] f546.11 ~> f546.12 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= K + Z] f546.11 ~> f546.11 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= K + Z] + Loop: [0.6.0.0 <= 3*K + Z] f546.11 ~> f546.11 [E <= E, F <= F, H <= H, I <= I, M <= M, Q <= Q, S <= S, V <= V, W <= W, X <= X, Y <= Y, Z <= K + Z] + Applied Processor: AbstractFlow + Details: () * Step 9: Lare WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,E,F,H,I,M,Q,S,V,W,X,Y,Z,0.0,0.1,0.1.0,0.2,0.2.0,0.3,0.4,0.5,0.6,0.6.0,0.6.0.0] f0.0 ~> f422.1 [K ~=> E] f422.1 ~> f422.1 [E ~+> E,K ~+> E] f422.1 ~> f422.22 [E ~+> E,K ~+> E] f437.2 ~> f441.3 [K ~=> H] f441.3 ~> f441.3 [H ~+> H,K ~+> H] f441.3 ~> f441.20 [H ~+> H,K ~+> H] f455.4 ~> f461.5 [K ~=> M] f461.5 ~> f461.5 [M ~+> M,K ~*> M] f461.5 ~> f461.18 [M ~+> M,K ~*> M] f485.6 ~> f485.6 [Q ~+> Q,K ~+> Q] f485.6 ~> f485.17 [Q ~+> Q,K ~+> Q] f501.7 ~> f501.7 [S ~+> S,K ~+> S] f501.7 ~> f501.16 [S ~+> S,K ~+> S] f526.8 ~> f526.8 [W ~+> W,K ~+> W] f526.8 ~> f526.15 [W ~+> W,K ~+> W] f540.9 ~> f543.10 [K ~=> Y] f543.10 ~> f546.11 [K ~=> Z] f546.11 ~> f546.11 [Z ~+> Z,K ~+> Z] f546.11 ~> f546.12 [Z ~+> Z,K ~+> Z] f546.12 ~> f543.10 [Y ~+> Y,K ~+> Y] f546.12 ~> f543.13 [Y ~+> Y,K ~+> Y] f543.13 ~> f540.9 [X ~+> X,K ~*> X] f543.13 ~> f540.14 [X ~+> X,K ~*> X] f540.14 ~> f584.23 [] f526.15 ~> f540.9 [K ~=> X] f501.16 ~> f526.8 [K ~=> V,K ~=> W] f485.17 ~> f501.7 [K ~=> S] f461.18 ~> f455.4 [I ~+> I,K ~*> I] f461.18 ~> f455.19 [I ~+> I,K ~*> I] f455.19 ~> f485.6 [K ~=> Q] f441.20 ~> f437.2 [F ~+> F,K ~+> F] f441.20 ~> f437.21 [F ~+> F,K ~+> F] f437.21 ~> f455.4 [K ~=> I] f422.22 ~> f437.2 [K ~=> F] f584.23 ~> exitus616 [] + Loop: [E ~+> 0.0,K ~*> 0.0] f422.1 ~> f422.1 [E ~+> E,K ~+> E] + Loop: [F ~+> 0.1,K ~*> 0.1] f437.2 ~> f441.3 [K ~=> H] f441.20 ~> f437.2 [F ~+> F,K ~+> F] f441.3 ~> f441.20 [H ~+> H,K ~+> H] f441.3 ~> f441.3 [H ~+> H,K ~+> H] + Loop: [H ~+> 0.1.0,K ~*> 0.1.0] f441.3 ~> f441.3 [H ~+> H,K ~+> H] + Loop: [I ~+> 0.2,K ~*> 0.2] f455.4 ~> f461.5 [K ~=> M] f461.18 ~> f455.4 [I ~+> I,K ~*> I] f461.5 ~> f461.18 [M ~+> M,K ~*> M] f461.5 ~> f461.5 [M ~+> M,K ~*> M] + Loop: [M ~+> 0.2.0,K ~*> 0.2.0] f461.5 ~> f461.5 [M ~+> M,K ~*> M] + Loop: [Q ~=> 0.3] f485.6 ~> f485.6 [Q ~+> Q,K ~+> Q] + Loop: [S ~+> 0.4,K ~*> 0.4] f501.7 ~> f501.7 [S ~+> S,K ~+> S] + Loop: [V ~+> 0.5,W ~+> 0.5] f526.8 ~> f526.8 [W ~+> W,K ~+> W] + Loop: [X ~+> 0.6,K ~*> 0.6] f540.9 ~> f543.10 [K ~=> Y] f543.13 ~> f540.9 [X ~+> X,K ~*> X] f546.12 ~> f543.13 [Y ~+> Y,K ~+> Y] f546.11 ~> f546.12 [Z ~+> Z,K ~+> Z] f543.10 ~> f546.11 [K ~=> Z] f546.12 ~> f543.10 [Y ~+> Y,K ~+> Y] f546.11 ~> f546.11 [Z ~+> Z,K ~+> Z] + Loop: [Y ~+> 0.6.0,K ~*> 0.6.0] f543.10 ~> f546.11 [K ~=> Z] f546.12 ~> f543.10 [Y ~+> Y,K ~+> Y] f546.11 ~> f546.12 [Z ~+> Z,K ~+> Z] f546.11 ~> f546.11 [Z ~+> Z,K ~+> Z] + Loop: [Z ~+> 0.6.0.0,K ~*> 0.6.0.0] f546.11 ~> f546.11 [Z ~+> Z,K ~+> Z] + Applied Processor: Lare + Details: f0.0 ~> exitus616 [K ~=> V ,K ~=> 0.3 ,tick ~+> tick ,K ~+> E ,K ~+> F ,K ~+> H ,K ~+> I ,K ~+> M ,K ~+> Q ,K ~+> S ,K ~+> W ,K ~+> X ,K ~+> Y ,K ~+> Z ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.2 ,K ~+> 0.2.0 ,K ~+> 0.4 ,K ~+> 0.5 ,K ~+> 0.6 ,K ~+> 0.6.0 ,K ~+> 0.6.0.0 ,K ~+> tick ,K ~*> E ,K ~*> F ,K ~*> H ,K ~*> I ,K ~*> M ,K ~*> Q ,K ~*> S ,K ~*> W ,K ~*> X ,K ~*> Y ,K ~*> Z ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.2 ,K ~*> 0.2.0 ,K ~*> 0.4 ,K ~*> 0.5 ,K ~*> 0.6 ,K ~*> 0.6.0 ,K ~*> 0.6.0.0 ,K ~*> tick ,K ~^> H ,K ~^> M ,K ~^> Z] + f422.1> [E ~+> E ,E ~+> 0.0 ,E ~+> tick ,tick ~+> tick ,K ~+> E ,E ~*> E ,K ~*> E ,K ~*> 0.0 ,K ~*> tick] + f441.20> [F ~+> F ,F ~+> 0.1 ,F ~+> tick ,tick ~+> tick ,K ~+> F ,K ~+> H ,K ~+> 0.1.0 ,K ~+> tick ,F ~*> F ,F ~*> H ,F ~*> tick ,K ~*> F ,K ~*> H ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick ,F ~^> H ,K ~^> H] + f441.3> [H ~+> H ,H ~+> 0.1.0 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,H ~*> H ,K ~*> H ,K ~*> 0.1.0 ,K ~*> tick] + f461.18> [I ~+> I ,I ~+> 0.2 ,I ~+> tick ,tick ~+> tick ,K ~+> M ,K ~+> 0.2.0 ,K ~+> tick ,I ~*> I ,I ~*> M ,I ~*> tick ,K ~*> I ,K ~*> M ,K ~*> 0.2 ,K ~*> 0.2.0 ,K ~*> tick ,I ~^> M ,K ~^> M] + f461.5> [M ~+> M ,M ~+> 0.2.0 ,M ~+> tick ,tick ~+> tick ,M ~*> M ,K ~*> M ,K ~*> 0.2.0 ,K ~*> tick] + f485.6> [Q ~=> 0.3,Q ~+> Q,Q ~+> tick,tick ~+> tick,K ~+> Q,Q ~*> Q,K ~*> Q] + f501.7> [S ~+> S ,S ~+> 0.4 ,S ~+> tick ,tick ~+> tick ,K ~+> S ,S ~*> S ,K ~*> S ,K ~*> 0.4 ,K ~*> tick] + f526.8> [V ~+> 0.5 ,V ~+> tick ,W ~+> W ,W ~+> 0.5 ,W ~+> tick ,tick ~+> tick ,K ~+> W ,V ~*> W ,W ~*> W ,K ~*> W] + f543.13> [X ~+> X ,X ~+> 0.6 ,X ~+> tick ,tick ~+> tick ,K ~+> Y ,K ~+> Z ,K ~+> 0.6.0 ,K ~+> 0.6.0.0 ,K ~+> tick ,X ~*> X ,X ~*> tick ,K ~*> X ,K ~*> Y ,K ~*> Z ,K ~*> 0.6 ,K ~*> 0.6.0 ,K ~*> 0.6.0.0 ,K ~*> tick ,K ~^> Z] + f546.12> [Y ~+> Y ,Y ~+> 0.6.0 ,Y ~+> tick ,tick ~+> tick ,K ~+> Y ,K ~+> Z ,K ~+> 0.6.0.0 ,K ~+> tick ,Y ~*> Y ,Y ~*> Z ,Y ~*> tick ,K ~*> Y ,K ~*> Z ,K ~*> 0.6.0 ,K ~*> 0.6.0.0 ,K ~*> tick ,Y ~^> Z ,K ~^> Z] + f546.11> [Z ~+> Z ,Z ~+> 0.6.0.0 ,Z ~+> tick ,tick ~+> tick ,K ~+> Z ,Z ~*> Z ,K ~*> Z ,K ~*> 0.6.0.0 ,K ~*> tick] YES(?,O(1))