YES(?,O(n^1)) * Step 1: ArgumentFilter WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f1(A,2,Y,C1,Z,A1,B1,D1,E1,F1,Y,L,M,N,O,P,Q,R,S,T,U,V,W,G1) [A >= 2] (1,1) 1. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X) -> f4(D1,0,0,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [0 >= D1 && 0 >= A] (1,1) 2. 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) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 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) -> f10(Y,1 + U,C,D,E,F,G,H,I,J,C,L,M,C,U,0,C,0,C,C,U,V,W,X) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 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) -> f1(A,1 + B,D,B1,Y,Z,A1,C1,D1,E1,D,F1,B,N,O,P,Q,R,S,T,U,V,W,X) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. 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) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. 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) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 7. 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) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 8. 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) -> f10(A1,Z,Y,D,E,F,G,H,I,J,Y,L,M,N,O,0,Y,0,Y,N,-1 + U,B1,-1 + U,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 9. 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) -> f4(D1,B,C,D,E,F,G,H,E1,J,K,L,M,C1,O,B1,Y,Z,A1,F1,U,V,W,X) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,9},3->{5,6,7,8,9},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9} ,8->{5,6,7,8,9},9->{}] + Applied Processor: ArgumentFilter [3,4,5,6,7,8,9,10,11,12,16,18,21,22,23] + Details: We remove following argument positions: [3,4,5,6,7,8,9,10,11,12,16,18,21,22,23]. * Step 2: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f3(A,B,C,N,O,P,R,T,U) -> f1(A,2,Y,N,O,P,R,T,U) [A >= 2] (1,1) 1. f3(A,B,C,N,O,P,R,T,U) -> f4(D1,0,0,C1,O,B1,Z,F1,U) [0 >= D1 && 0 >= A] (1,1) 2. f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. f1(A,B,C,N,O,P,R,T,U) -> f1(A,1 + B,D,N,O,P,R,T,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 7. f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 8. f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 9. f10(A,B,C,N,O,P,R,T,U) -> f4(D1,B,C,C1,O,B1,Z,F1,U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,9},3->{5,6,7,8,9},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9} ,8->{5,6,7,8,9},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(3,9)] * Step 3: FromIts WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f3(A,B,C,N,O,P,R,T,U) -> f1(A,2,Y,N,O,P,R,T,U) [A >= 2] (1,1) 1. f3(A,B,C,N,O,P,R,T,U) -> f4(D1,0,0,C1,O,B1,Z,F1,U) [0 >= D1 && 0 >= A] (1,1) 2. f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] 3. f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 (?,1) && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] 4. f1(A,B,C,N,O,P,R,T,U) -> f1(A,1 + B,D,N,O,P,R,T,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] (?,1) 5. f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 6. f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 7. f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] 8. f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] 9. f10(A,B,C,N,O,P,R,T,U) -> f4(D1,B,C,C1,O,B1,Z,F1,U) [O + -1*U >= 0 (?,1) && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8},3->{5,6,7,8},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9},8->{5 ,6,7,8,9},9->{}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,O(n^1)) + Considered Problem: Rules: f3(A,B,C,N,O,P,R,T,U) -> f1(A,2,Y,N,O,P,R,T,U) [A >= 2] f3(A,B,C,N,O,P,R,T,U) -> f4(D1,0,0,C1,O,B1,Z,F1,U) [0 >= D1 && 0 >= A] f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1(A,B,C,N,O,P,R,T,U) -> f1(A,1 + B,D,N,O,P,R,T,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f4(D1,B,C,C1,O,B1,Z,F1,U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] Signature: {(f1,24);(f10,24);(f3,24);(f4,24)} Rule Graph: [0->{2,3,4},1->{},2->{5,6,7,8},3->{5,6,7,8},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9},8->{5 ,6,7,8,9},9->{}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: Rules: f3(A,B,C,N,O,P,R,T,U) -> f1(A,2,Y,N,O,P,R,T,U) [A >= 2] f3(A,B,C,N,O,P,R,T,U) -> f4(D1,0,0,C1,O,B1,Z,F1,U) [0 >= D1 && 0 >= A] f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1(A,B,C,N,O,P,R,T,U) -> f1(A,1 + B,D,N,O,P,R,T,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f4(D1,B,C,C1,O,B1,Z,F1,U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] f4(A,B,C,N,O,P,R,T,U) -> exitus616(A,B,C,N,O,P,R,T,U) True f4(A,B,C,N,O,P,R,T,U) -> exitus616(A,B,C,N,O,P,R,T,U) True f4(A,B,C,N,O,P,R,T,U) -> exitus616(A,B,C,N,O,P,R,T,U) True Signature: {(exitus616,9);(f1,24);(f10,24);(f3,24);(f4,24)} Rule Graph: [0->{2,3,4},1->{10},2->{5,6,7,8},3->{5,6,7,8},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9} ,8->{5,6,7,8,9},9->{11,12}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[4] c: [4] | `- p:[5,6,7,8] c: [5,6,7,8] * Step 6: AbstractSize WORST_CASE(?,O(n^1)) + Considered Problem: (Rules: f3(A,B,C,N,O,P,R,T,U) -> f1(A,2,Y,N,O,P,R,T,U) [A >= 2] f3(A,B,C,N,O,P,R,T,U) -> f4(D1,0,0,C1,O,B1,Z,F1,U) [0 >= D1 && 0 >= A] f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && 0 >= 1 + C] f1(A,B,C,N,O,P,R,T,U) -> f10(Y,1 + U,C,C,U,0,0,C,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && B >= A && B >= 0 && Z >= Y && Y >= 2 && C >= 1] f1(A,B,C,N,O,P,R,T,U) -> f1(A,1 + B,D,N,O,P,R,T,U) [A + -1*B >= 0 && -2 + B >= 0 && -4 + A + B >= 0 && -2 + A >= 0 && A >= 1 + B && B >= 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && N >= 1 + C1 && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && C1 >= 1 + Y && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f10(A1,Z,Y,N,O,0,0,N,-1 + U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && C1 >= 1 + N && U >= 0 && A1 >= 2 && Z >= A1 && Y >= 1 + C1 && P = 0] f10(A,B,C,N,O,P,R,T,U) -> f4(D1,B,C,C1,O,B1,Z,F1,U) [O + -1*U >= 0 && N + -1*T >= 0 && -1*N + T >= 0 && -1*R >= 0 && P + -1*R >= 0 && -1*P + -1*R >= 0 && -2 + A + -1*R >= 0 && R >= 0 && P + R >= 0 && -1*P + R >= 0 && -2 + A + R >= 0 && -1*P >= 0 && -2 + A + -1*P >= 0 && P >= 0 && -2 + A + P >= 0 && -2 + A >= 0 && D1 >= 2 && U >= 0 && P = N] f4(A,B,C,N,O,P,R,T,U) -> exitus616(A,B,C,N,O,P,R,T,U) True f4(A,B,C,N,O,P,R,T,U) -> exitus616(A,B,C,N,O,P,R,T,U) True f4(A,B,C,N,O,P,R,T,U) -> exitus616(A,B,C,N,O,P,R,T,U) True Signature: {(exitus616,9);(f1,24);(f10,24);(f3,24);(f4,24)} Rule Graph: [0->{2,3,4},1->{10},2->{5,6,7,8},3->{5,6,7,8},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9} ,8->{5,6,7,8,9},9->{11,12}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12] | +- p:[4] c: [4] | `- p:[5,6,7,8] c: [5,6,7,8]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,C,N,O,P,R,T,U,0.0,0.1] f3 ~> f1 [A <= A, B <= 2*K, C <= unknown, N <= N, O <= O, P <= P, R <= R, T <= T, U <= U] f3 ~> f4 [A <= unknown, B <= 0*K, C <= 0*K, N <= unknown, O <= O, P <= unknown, R <= unknown, T <= unknown, U <= U] f1 ~> f10 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, R <= 0*K, T <= C, U <= U] f1 ~> f10 [A <= unknown, B <= K + U, C <= C, N <= C, O <= U, P <= 0*K, R <= 0*K, T <= C, U <= U] f1 ~> f1 [A <= A, B <= A, C <= unknown, N <= N, O <= O, P <= P, R <= R, T <= T, U <= U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, R <= 0*K, T <= N, U <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, R <= 0*K, T <= N, U <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, R <= 0*K, T <= N, U <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, R <= 0*K, T <= N, U <= K + U] f10 ~> f4 [A <= unknown, B <= B, C <= C, N <= unknown, O <= O, P <= unknown, R <= unknown, T <= unknown, U <= U] f4 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, R <= R, T <= T, U <= U] f4 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, R <= R, T <= T, U <= U] f4 ~> exitus616 [A <= A, B <= B, C <= C, N <= N, O <= O, P <= P, R <= R, T <= T, U <= U] + Loop: [0.0 <= K + A + B] f1 ~> f1 [A <= A, B <= A, C <= unknown, N <= N, O <= O, P <= P, R <= R, T <= T, U <= U] + Loop: [0.1 <= U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, R <= 0*K, T <= N, U <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, R <= 0*K, T <= N, U <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, R <= 0*K, T <= N, U <= K + U] f10 ~> f10 [A <= unknown, B <= unknown, C <= unknown, N <= N, O <= O, P <= 0*K, R <= 0*K, T <= N, U <= K + U] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,N,O,P,R,T,U,0.0,0.1] f3 ~> f1 [K ~=> B,huge ~=> C] f3 ~> f4 [K ~=> B,K ~=> C,huge ~=> A,huge ~=> N,huge ~=> P,huge ~=> R,huge ~=> T] f1 ~> f10 [C ~=> N,C ~=> T,U ~=> O,K ~=> P,K ~=> R,huge ~=> A,U ~+> B,K ~+> B] f1 ~> f10 [C ~=> N,C ~=> T,U ~=> O,K ~=> P,K ~=> R,huge ~=> A,U ~+> B,K ~+> B] f1 ~> f1 [A ~=> B,huge ~=> C] f10 ~> f10 [N ~=> T,K ~=> P,K ~=> R,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10 ~> f10 [N ~=> T,K ~=> P,K ~=> R,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10 ~> f10 [N ~=> T,K ~=> P,K ~=> R,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10 ~> f10 [N ~=> T,K ~=> P,K ~=> R,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10 ~> f4 [huge ~=> A,huge ~=> N,huge ~=> P,huge ~=> R,huge ~=> T] f4 ~> exitus616 [] f4 ~> exitus616 [] f4 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f1 ~> f1 [A ~=> B,huge ~=> C] + Loop: [U ~=> 0.1] f10 ~> f10 [N ~=> T,K ~=> P,K ~=> R,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10 ~> f10 [N ~=> T,K ~=> P,K ~=> R,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10 ~> f10 [N ~=> T,K ~=> P,K ~=> R,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] f10 ~> f10 [N ~=> T,K ~=> P,K ~=> R,huge ~=> A,huge ~=> B,huge ~=> C,U ~+> U,K ~+> U] + Applied Processor: Lare + Details: f3 ~> exitus616 [U ~=> O ,U ~=> 0.1 ,K ~=> B ,K ~=> C ,huge ~=> A ,huge ~=> B ,huge ~=> C ,huge ~=> N ,huge ~=> P ,huge ~=> R ,huge ~=> T ,A ~+> 0.0 ,A ~+> tick ,U ~+> B ,U ~+> U ,U ~+> tick ,tick ~+> tick ,K ~+> B ,K ~+> U ,K ~+> 0.0 ,K ~+> tick ,U ~*> U ,K ~*> U ,K ~*> 0.0 ,K ~*> tick] + f1> [A ~=> B ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] + f10> [N ~=> T ,U ~=> 0.1 ,K ~=> P ,K ~=> R ,huge ~=> A ,huge ~=> B ,huge ~=> C ,U ~+> U ,U ~+> tick ,tick ~+> tick ,K ~+> U ,U ~*> U ,K ~*> U] YES(?,O(n^1))