YES(?,O(n^1)) * Step 1: ArgumentFilter WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A = 1] (1,1) 1. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A] (1,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f20(A,B,1 + B,S,T,1,G,H,I,J,K,L,M,N,O,P,Q,R) [2 + -1*B >= 0 && -1 + B >= 0 && A >= B] (?,1) 4. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f20(A,B,C,D + S*T,E + U*V,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 5. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f31(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f45(A,B,C,D,E,1 + F,G + S*T,H + U*V,I + W*X,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 7. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1 + F,G,H,I,J,-1 + K,S,T,U,V,K,Q,R) [2 + -1*F + -1*K >= 0 (?,1) && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && J >= F] 8. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [2 + -1*F + -1*K >= 0 (?,1) && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && F >= 1 + J] 9. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1,G,H,I,S,B,L,M,N,O,P,T,U) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 1 + B >= 2*V && 3*V >= 2 + B && V >= S && 1 + B >= 2*W && 3*W >= 2 + B && S >= W && F >= 1 + B] 10. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] 11. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f45(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] 12. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f45(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] 13. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f31(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] 14. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f31(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] 15. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f31(A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] 16. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [2 + -1*B >= 0 && -1 + B >= 0 && B >= 1 + A] (?,1) Signature: {(f1,18);(f13,18);(f2,18);(f20,18);(f31,18);(f45,18);(f60,18)} Flow Graph: [0->{},1->{3,16},2->{3,16},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16} ,9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: ArgumentFilter [3,6,7,8,11,12,13,14,15,16,17] + Details: We remove following argument positions: [3,6,7,8,11,12,13,14,15,16,17]. * Step 2: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,B,C,E,F,J,K) -> f1(1,B,C,E,F,J,K) [A = 1] (1,1) 1. f2(A,B,C,E,F,J,K) -> f13(A,1,C,E,F,J,K) [0 >= A] (1,1) 2. f2(A,B,C,E,F,J,K) -> f13(A,1,C,E,F,J,K) [A >= 2] (1,1) 3. f13(A,B,C,E,F,J,K) -> f20(A,B,1 + B,T,1,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && A >= B] (?,1) 4. f20(A,B,C,E,F,J,K) -> f20(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 5. f31(A,B,C,E,F,J,K) -> f31(A,B,C,E,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 6. f45(A,B,C,E,F,J,K) -> f45(A,B,C,E,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 7. f60(A,B,C,E,F,J,K) -> f60(A,B,C,E,1 + F,J,-1 + K) [2 + -1*F + -1*K >= 0 (?,1) && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && J >= F] 8. f60(A,B,C,E,F,J,K) -> f13(A,1 + B,C,E,F,J,K) [2 + -1*F + -1*K >= 0 (?,1) && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && F >= 1 + J] 9. f45(A,B,C,E,F,J,K) -> f60(A,B,C,E,1,S,B) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 1 + B >= 2*V && 3*V >= 2 + B && V >= S && 1 + B >= 2*W && 3*W >= 2 + B && S >= W && F >= 1 + B] 10. f31(A,B,C,E,F,J,K) -> f1(A,B,A,E,F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] 11. f31(A,B,C,E,F,J,K) -> f45(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] 12. f31(A,B,C,E,F,J,K) -> f45(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] 13. f20(A,B,C,E,F,J,K) -> f31(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] 14. f20(A,B,C,E,F,J,K) -> f31(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] 15. f20(A,B,C,E,F,J,K) -> f31(A,B,C,0,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] 16. f13(A,B,C,E,F,J,K) -> f1(A,B,C,E,F,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && B >= 1 + A] (?,1) Signature: {(f1,18);(f13,18);(f2,18);(f20,18);(f31,18);(f45,18);(f60,18)} Flow Graph: [0->{},1->{3,16},2->{3,16},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16} ,9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3) ,(2,16) ,(3,13) ,(3,14) ,(3,15) ,(7,7) ,(9,8) ,(11,9) ,(12,9) ,(13,10) ,(13,11) ,(13,12) ,(14,10) ,(14,11) ,(14,12) ,(15,10) ,(15,11) ,(15,12)] * Step 3: FromIts WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. f2(A,B,C,E,F,J,K) -> f1(1,B,C,E,F,J,K) [A = 1] (1,1) 1. f2(A,B,C,E,F,J,K) -> f13(A,1,C,E,F,J,K) [0 >= A] (1,1) 2. f2(A,B,C,E,F,J,K) -> f13(A,1,C,E,F,J,K) [A >= 2] (1,1) 3. f13(A,B,C,E,F,J,K) -> f20(A,B,1 + B,T,1,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && A >= B] (?,1) 4. f20(A,B,C,E,F,J,K) -> f20(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 5. f31(A,B,C,E,F,J,K) -> f31(A,B,C,E,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 6. f45(A,B,C,E,F,J,K) -> f45(A,B,C,E,1 + F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] 7. f60(A,B,C,E,F,J,K) -> f60(A,B,C,E,1 + F,J,-1 + K) [2 + -1*F + -1*K >= 0 (?,1) && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && J >= F] 8. f60(A,B,C,E,F,J,K) -> f13(A,1 + B,C,E,F,J,K) [2 + -1*F + -1*K >= 0 (?,1) && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && F >= 1 + J] 9. f45(A,B,C,E,F,J,K) -> f60(A,B,C,E,1,S,B) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 1 + B >= 2*V && 3*V >= 2 + B && V >= S && 1 + B >= 2*W && 3*W >= 2 + B && S >= W && F >= 1 + B] 10. f31(A,B,C,E,F,J,K) -> f1(A,B,A,E,F,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] 11. f31(A,B,C,E,F,J,K) -> f45(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] 12. f31(A,B,C,E,F,J,K) -> f45(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] 13. f20(A,B,C,E,F,J,K) -> f31(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] 14. f20(A,B,C,E,F,J,K) -> f31(A,B,C,E,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] 15. f20(A,B,C,E,F,J,K) -> f31(A,B,C,0,1,J,K) [-1 + F >= 0 (?,1) && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] 16. f13(A,B,C,E,F,J,K) -> f1(A,B,C,E,F,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && B >= 1 + A] (?,1) Signature: {(f1,18);(f13,18);(f2,18);(f20,18);(f31,18);(f45,18);(f60,18)} Flow Graph: [0->{},1->{16},2->{3},3->{4},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{8},8->{3,16},9->{7},10->{} ,11->{6},12->{6},13->{5},14->{5},15->{5},16->{}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,O(n^1)) + Considered Problem: Rules: f2(A,B,C,E,F,J,K) -> f1(1,B,C,E,F,J,K) [A = 1] f2(A,B,C,E,F,J,K) -> f13(A,1,C,E,F,J,K) [0 >= A] f2(A,B,C,E,F,J,K) -> f13(A,1,C,E,F,J,K) [A >= 2] f13(A,B,C,E,F,J,K) -> f20(A,B,1 + B,T,1,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && A >= B] f20(A,B,C,E,F,J,K) -> f20(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31(A,B,C,E,F,J,K) -> f31(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f45(A,B,C,E,F,J,K) -> f45(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f60(A,B,C,E,F,J,K) -> f60(A,B,C,E,1 + F,J,-1 + K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && J >= F] f60(A,B,C,E,F,J,K) -> f13(A,1 + B,C,E,F,J,K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && F >= 1 + J] f45(A,B,C,E,F,J,K) -> f60(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 1 + B >= 2*V && 3*V >= 2 + B && V >= S && 1 + B >= 2*W && 3*W >= 2 + B && S >= W && F >= 1 + B] f31(A,B,C,E,F,J,K) -> f1(A,B,A,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] f31(A,B,C,E,F,J,K) -> f45(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] f31(A,B,C,E,F,J,K) -> f45(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] f20(A,B,C,E,F,J,K) -> f31(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] f20(A,B,C,E,F,J,K) -> f31(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] f20(A,B,C,E,F,J,K) -> f31(A,B,C,0,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] f13(A,B,C,E,F,J,K) -> f1(A,B,C,E,F,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && B >= 1 + A] Signature: {(f1,18);(f13,18);(f2,18);(f20,18);(f31,18);(f45,18);(f60,18)} Rule Graph: [0->{},1->{16},2->{3},3->{4},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{8},8->{3,16},9->{7},10->{} ,11->{6},12->{6},13->{5},14->{5},15->{5},16->{}] + Applied Processor: AddSinks + Details: () * Step 5: Unfold WORST_CASE(?,O(n^1)) + Considered Problem: Rules: f2(A,B,C,E,F,J,K) -> f1(1,B,C,E,F,J,K) [A = 1] f2(A,B,C,E,F,J,K) -> f13(A,1,C,E,F,J,K) [0 >= A] f2(A,B,C,E,F,J,K) -> f13(A,1,C,E,F,J,K) [A >= 2] f13(A,B,C,E,F,J,K) -> f20(A,B,1 + B,T,1,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && A >= B] f20(A,B,C,E,F,J,K) -> f20(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31(A,B,C,E,F,J,K) -> f31(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f45(A,B,C,E,F,J,K) -> f45(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f60(A,B,C,E,F,J,K) -> f60(A,B,C,E,1 + F,J,-1 + K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && J >= F] f60(A,B,C,E,F,J,K) -> f13(A,1 + B,C,E,F,J,K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && F >= 1 + J] f45(A,B,C,E,F,J,K) -> f60(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 1 + B >= 2*V && 3*V >= 2 + B && V >= S && 1 + B >= 2*W && 3*W >= 2 + B && S >= W && F >= 1 + B] f31(A,B,C,E,F,J,K) -> f1(A,B,A,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] f31(A,B,C,E,F,J,K) -> f45(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] f31(A,B,C,E,F,J,K) -> f45(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] f20(A,B,C,E,F,J,K) -> f31(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] f20(A,B,C,E,F,J,K) -> f31(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] f20(A,B,C,E,F,J,K) -> f31(A,B,C,0,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] f13(A,B,C,E,F,J,K) -> f1(A,B,C,E,F,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && B >= 1 + A] f1(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True f1(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True f1(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True f1(A,B,C,E,F,J,K) -> exitus616(A,B,C,E,F,J,K) True Signature: {(exitus616,7);(f1,18);(f13,18);(f2,18);(f20,18);(f31,18);(f45,18);(f60,18)} Rule Graph: [0->{20},1->{16},2->{3},3->{4},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{8},8->{3,16},9->{7},10->{17} ,11->{6},12->{6},13->{5},14->{5},15->{5},16->{18,19}] + Applied Processor: Unfold + Details: () * Step 6: Decompose WORST_CASE(?,O(n^1)) + Considered Problem: Rules: f2.0(A,B,C,E,F,J,K) -> f1.20(1,B,C,E,F,J,K) [A = 1] f2.1(A,B,C,E,F,J,K) -> f13.16(A,1,C,E,F,J,K) [0 >= A] f2.2(A,B,C,E,F,J,K) -> f13.3(A,1,C,E,F,J,K) [A >= 2] f13.3(A,B,C,E,F,J,K) -> f20.4(A,B,1 + B,T,1,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && A >= B] f20.4(A,B,C,E,F,J,K) -> f20.4(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f20.4(A,B,C,E,F,J,K) -> f20.13(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f20.4(A,B,C,E,F,J,K) -> f20.14(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f20.4(A,B,C,E,F,J,K) -> f20.15(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31.5(A,B,C,E,F,J,K) -> f31.5(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31.5(A,B,C,E,F,J,K) -> f31.10(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31.5(A,B,C,E,F,J,K) -> f31.11(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31.5(A,B,C,E,F,J,K) -> f31.12(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f45.6(A,B,C,E,F,J,K) -> f45.6(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f45.6(A,B,C,E,F,J,K) -> f45.9(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f60.7(A,B,C,E,F,J,K) -> f60.8(A,B,C,E,1 + F,J,-1 + K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && J >= F] f60.8(A,B,C,E,F,J,K) -> f13.3(A,1 + B,C,E,F,J,K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && F >= 1 + J] f60.8(A,B,C,E,F,J,K) -> f13.16(A,1 + B,C,E,F,J,K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && F >= 1 + J] f45.9(A,B,C,E,F,J,K) -> f60.7(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 1 + B >= 2*V && 3*V >= 2 + B && V >= S && 1 + B >= 2*W && 3*W >= 2 + B && S >= W && F >= 1 + B] f31.10(A,B,C,E,F,J,K) -> f1.17(A,B,A,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] f31.11(A,B,C,E,F,J,K) -> f45.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] f31.12(A,B,C,E,F,J,K) -> f45.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] f20.13(A,B,C,E,F,J,K) -> f31.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] f20.14(A,B,C,E,F,J,K) -> f31.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] f20.15(A,B,C,E,F,J,K) -> f31.5(A,B,C,0,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] f13.16(A,B,C,E,F,J,K) -> f1.18(A,B,C,E,F,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && B >= 1 + A] f13.16(A,B,C,E,F,J,K) -> f1.19(A,B,C,E,F,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && B >= 1 + A] f1.17(A,B,C,E,F,J,K) -> exitus616.21(A,B,C,E,F,J,K) True f1.18(A,B,C,E,F,J,K) -> exitus616.21(A,B,C,E,F,J,K) True f1.19(A,B,C,E,F,J,K) -> exitus616.21(A,B,C,E,F,J,K) True f1.20(A,B,C,E,F,J,K) -> exitus616.21(A,B,C,E,F,J,K) True Signature: {(exitus616.21,7) ;(f1.17,7) ;(f1.18,7) ;(f1.19,7) ;(f1.20,7) ;(f13.16,7) ;(f13.3,7) ;(f2.0,7) ;(f2.1,7) ;(f2.2,7) ;(f20.13,7) ;(f20.14,7) ;(f20.15,7) ;(f20.4,7) ;(f31.10,7) ;(f31.11,7) ;(f31.12,7) ;(f31.5,7) ;(f45.6,7) ;(f45.9,7) ;(f60.7,7) ;(f60.8,7)} Rule Graph: [0->{29},1->{24,25},2->{3},3->{4,5,6,7},4->{4,5,6,7},5->{21},6->{22},7->{23},8->{8,9,10,11},9->{18} ,10->{19},11->{20},12->{12,13},13->{17},14->{15,16},15->{3},16->{24,25},17->{14},18->{26},19->{12,13} ,20->{12,13},21->{8,9,10,11},22->{8,9,10,11},23->{8,9,10,11},24->{27},25->{28},26->{},27->{},28->{},29->{}] + 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] | `- p:[3,15,14,17,13,12,19,10,8,21,5,4,22,6,23,7,20,11] c: [3,4,5,6,7,8,10,11,12,13,14,15,17,19,20,21,22,23] * Step 7: AbstractSize WORST_CASE(?,O(n^1)) + Considered Problem: (Rules: f2.0(A,B,C,E,F,J,K) -> f1.20(1,B,C,E,F,J,K) [A = 1] f2.1(A,B,C,E,F,J,K) -> f13.16(A,1,C,E,F,J,K) [0 >= A] f2.2(A,B,C,E,F,J,K) -> f13.3(A,1,C,E,F,J,K) [A >= 2] f13.3(A,B,C,E,F,J,K) -> f20.4(A,B,1 + B,T,1,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && A >= B] f20.4(A,B,C,E,F,J,K) -> f20.4(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f20.4(A,B,C,E,F,J,K) -> f20.13(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f20.4(A,B,C,E,F,J,K) -> f20.14(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f20.4(A,B,C,E,F,J,K) -> f20.15(A,B,C,E + U*V,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31.5(A,B,C,E,F,J,K) -> f31.5(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31.5(A,B,C,E,F,J,K) -> f31.10(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31.5(A,B,C,E,F,J,K) -> f31.11(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f31.5(A,B,C,E,F,J,K) -> f31.12(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f45.6(A,B,C,E,F,J,K) -> f45.6(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f45.6(A,B,C,E,F,J,K) -> f45.9(A,B,C,E,1 + F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && B >= F] f60.7(A,B,C,E,F,J,K) -> f60.8(A,B,C,E,1 + F,J,-1 + K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && J >= F] f60.8(A,B,C,E,F,J,K) -> f13.3(A,1 + B,C,E,F,J,K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && F >= 1 + J] f60.8(A,B,C,E,F,J,K) -> f13.16(A,1 + B,C,E,F,J,K) [2 + -1*F + -1*K >= 0 && -1 + F >= 0 && -3 + C + F >= 0 && 1 + -1*C + F >= 0 && -2 + B + F >= 0 && -1*B + F >= 0 && -2 + F + K >= 0 && F + -1*K >= 0 && -2 + F + J >= 0 && F + -1*J >= 0 && -2 + A + F >= 0 && 2 + -1*C >= 0 && 1 + B + -1*C >= 0 && 3 + -1*B + -1*C >= 0 && 3 + -1*C + -1*K >= 0 && 1 + -1*C + J >= 0 && 3 + -1*C + -1*J >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -1 + C + -1*K >= 0 && -3 + C + J >= 0 && -1 + C + -1*J >= 0 && -3 + A + C >= 0 && 1 + -1*B >= 0 && 2 + -1*B + -1*K >= 0 && -1*B + J >= 0 && 2 + -1*B + -1*J >= 0 && A + -1*B >= 0 && -1 + B >= 0 && B + -1*K >= 0 && -2 + B + J >= 0 && B + -1*J >= 0 && -2 + A + B >= 0 && 1 + -1*K >= 0 && J + -1*K >= 0 && 2 + -1*J + -1*K >= 0 && A + -1*K >= 0 && 1 + -1*J >= 0 && A + -1*J >= 0 && -1 + J >= 0 && -2 + A + J >= 0 && -1 + A >= 0 && F >= 1 + J] f45.9(A,B,C,E,F,J,K) -> f60.7(A,B,C,E,1,S,B) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 1 + B >= 2*V && 3*V >= 2 + B && V >= S && 1 + B >= 2*W && 3*W >= 2 + B && S >= W && F >= 1 + B] f31.10(A,B,C,E,F,J,K) -> f1.17(A,B,A,E,F,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && A = C] f31.11(A,B,C,E,F,J,K) -> f45.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && A >= 1 + C && F >= 1 + B] f31.12(A,B,C,E,F,J,K) -> f45.6(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && C >= 1 + A && F >= 1 + B] f20.13(A,B,C,E,F,J,K) -> f31.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && 0 >= 1 + E && F >= 1 + B] f20.14(A,B,C,E,F,J,K) -> f31.5(A,B,C,E,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && E >= 1 && F >= 1 + B] f20.15(A,B,C,E,F,J,K) -> f31.5(A,B,C,0,1,J,K) [-1 + F >= 0 && -3 + C + F >= 0 && 2 + -1*C + F >= 0 && -2 + B + F >= 0 && 1 + -1*B + F >= 0 && -2 + A + F >= 0 && 3 + -1*C >= 0 && 1 + B + -1*C >= 0 && 5 + -1*B + -1*C >= 0 && 1 + A + -1*C >= 0 && -2 + C >= 0 && -3 + B + C >= 0 && -1 + -1*B + C >= 0 && -3 + A + C >= 0 && 2 + -1*B >= 0 && A + -1*B >= 0 && -1 + B >= 0 && -2 + A + B >= 0 && -1 + A >= 0 && F >= 1 + B && E = 0] f13.16(A,B,C,E,F,J,K) -> f1.18(A,B,C,E,F,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && B >= 1 + A] f13.16(A,B,C,E,F,J,K) -> f1.19(A,B,C,E,F,J,K) [2 + -1*B >= 0 && -1 + B >= 0 && B >= 1 + A] f1.17(A,B,C,E,F,J,K) -> exitus616.21(A,B,C,E,F,J,K) True f1.18(A,B,C,E,F,J,K) -> exitus616.21(A,B,C,E,F,J,K) True f1.19(A,B,C,E,F,J,K) -> exitus616.21(A,B,C,E,F,J,K) True f1.20(A,B,C,E,F,J,K) -> exitus616.21(A,B,C,E,F,J,K) True Signature: {(exitus616.21,7) ;(f1.17,7) ;(f1.18,7) ;(f1.19,7) ;(f1.20,7) ;(f13.16,7) ;(f13.3,7) ;(f2.0,7) ;(f2.1,7) ;(f2.2,7) ;(f20.13,7) ;(f20.14,7) ;(f20.15,7) ;(f20.4,7) ;(f31.10,7) ;(f31.11,7) ;(f31.12,7) ;(f31.5,7) ;(f45.6,7) ;(f45.9,7) ;(f60.7,7) ;(f60.8,7)} Rule Graph: [0->{29},1->{24,25},2->{3},3->{4,5,6,7},4->{4,5,6,7},5->{21},6->{22},7->{23},8->{8,9,10,11},9->{18} ,10->{19},11->{20},12->{12,13},13->{17},14->{15,16},15->{3},16->{24,25},17->{14},18->{26},19->{12,13} ,20->{12,13},21->{8,9,10,11},22->{8,9,10,11},23->{8,9,10,11},24->{27},25->{28},26->{},27->{},28->{},29->{}] ,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] | `- p:[3,15,14,17,13,12,19,10,8,21,5,4,22,6,23,7,20,11] c: [3,4,5,6,7,8,10,11,12,13,14,15,17,19,20,21,22,23]) + Applied Processor: AbstractSize NoMinimize + Details: () * Step 8: AbstractFlow WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,C,E,F,J,K,0.0] f2.0 ~> f1.20 [A <= K, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f2.1 ~> f13.16 [A <= A, B <= K, C <= C, E <= E, F <= F, J <= J, K <= K] f2.2 ~> f13.3 [A <= A, B <= K, C <= C, E <= E, F <= F, J <= J, K <= K] f13.3 ~> f20.4 [A <= A, B <= B, C <= 3*K, E <= unknown, F <= K, J <= J, K <= K] f20.4 ~> f20.4 [A <= A, B <= B, C <= C, E <= unknown, F <= 3*K, J <= J, K <= K] f20.4 ~> f20.13 [A <= A, B <= B, C <= C, E <= unknown, F <= 3*K, J <= J, K <= K] f20.4 ~> f20.14 [A <= A, B <= B, C <= C, E <= unknown, F <= 3*K, J <= J, K <= K] f20.4 ~> f20.15 [A <= A, B <= B, C <= C, E <= unknown, F <= 3*K, J <= J, K <= K] f31.5 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f31.5 ~> f31.10 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f31.5 ~> f31.11 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f31.5 ~> f31.12 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f45.6 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f45.6 ~> f45.9 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f60.7 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= 2*K, J <= J, K <= 0*K] f60.8 ~> f13.3 [A <= A, B <= 2*K, C <= C, E <= E, F <= F, J <= J, K <= K] f60.8 ~> f13.16 [A <= A, B <= 2*K, C <= C, E <= E, F <= F, J <= J, K <= K] f45.9 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= 2*K, K <= B] f31.10 ~> f1.17 [A <= A, B <= B, C <= A, E <= E, F <= F, J <= J, K <= K] f31.11 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f31.12 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f20.13 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f20.14 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f20.15 ~> f31.5 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J, K <= K] f13.16 ~> f1.18 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f13.16 ~> f1.19 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f1.17 ~> exitus616.21 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f1.18 ~> exitus616.21 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f1.19 ~> exitus616.21 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] f1.20 ~> exitus616.21 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J, K <= K] + Loop: [0.0 <= 2*K + A + B] f13.3 ~> f20.4 [A <= A, B <= B, C <= 3*K, E <= unknown, F <= K, J <= J, K <= K] f60.8 ~> f13.3 [A <= A, B <= 2*K, C <= C, E <= E, F <= F, J <= J, K <= K] f60.7 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= 2*K, J <= J, K <= 0*K] f45.9 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= 2*K, K <= B] f45.6 ~> f45.9 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f45.6 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f31.11 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f31.5 ~> f31.11 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f31.5 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] f20.13 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f20.4 ~> f20.13 [A <= A, B <= B, C <= C, E <= unknown, F <= 3*K, J <= J, K <= K] f20.4 ~> f20.4 [A <= A, B <= B, C <= C, E <= unknown, F <= 3*K, J <= J, K <= K] f20.14 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f20.4 ~> f20.14 [A <= A, B <= B, C <= C, E <= unknown, F <= 3*K, J <= J, K <= K] f20.15 ~> f31.5 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J, K <= K] f20.4 ~> f20.15 [A <= A, B <= B, C <= C, E <= unknown, F <= 3*K, J <= J, K <= K] f31.12 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J, K <= K] f31.5 ~> f31.12 [A <= A, B <= B, C <= C, E <= E, F <= 3*K, J <= J, K <= K] + Applied Processor: AbstractFlow + Details: () * Step 9: Lare WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,E,F,J,K,0.0] f2.0 ~> f1.20 [K ~=> A] f2.1 ~> f13.16 [K ~=> B] f2.2 ~> f13.3 [K ~=> B] f13.3 ~> f20.4 [K ~=> C,K ~=> F,huge ~=> E] f20.4 ~> f20.4 [K ~=> F,huge ~=> E] f20.4 ~> f20.13 [K ~=> F,huge ~=> E] f20.4 ~> f20.14 [K ~=> F,huge ~=> E] f20.4 ~> f20.15 [K ~=> F,huge ~=> E] f31.5 ~> f31.5 [K ~=> F] f31.5 ~> f31.10 [K ~=> F] f31.5 ~> f31.11 [K ~=> F] f31.5 ~> f31.12 [K ~=> F] f45.6 ~> f45.6 [K ~=> F] f45.6 ~> f45.9 [K ~=> F] f60.7 ~> f60.8 [K ~=> F,K ~=> K] f60.8 ~> f13.3 [K ~=> B] f60.8 ~> f13.16 [K ~=> B] f45.9 ~> f60.7 [B ~=> K,K ~=> F,K ~=> J] f31.10 ~> f1.17 [A ~=> C] f31.11 ~> f45.6 [K ~=> F] f31.12 ~> f45.6 [K ~=> F] f20.13 ~> f31.5 [K ~=> F] f20.14 ~> f31.5 [K ~=> F] f20.15 ~> f31.5 [K ~=> E,K ~=> F] f13.16 ~> f1.18 [] f13.16 ~> f1.19 [] f1.17 ~> exitus616.21 [] f1.18 ~> exitus616.21 [] f1.19 ~> exitus616.21 [] f1.20 ~> exitus616.21 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~*> 0.0] f13.3 ~> f20.4 [K ~=> C,K ~=> F,huge ~=> E] f60.8 ~> f13.3 [K ~=> B] f60.7 ~> f60.8 [K ~=> F,K ~=> K] f45.9 ~> f60.7 [B ~=> K,K ~=> F,K ~=> J] f45.6 ~> f45.9 [K ~=> F] f45.6 ~> f45.6 [K ~=> F] f31.11 ~> f45.6 [K ~=> F] f31.5 ~> f31.11 [K ~=> F] f31.5 ~> f31.5 [K ~=> F] f20.13 ~> f31.5 [K ~=> F] f20.4 ~> f20.13 [K ~=> F,huge ~=> E] f20.4 ~> f20.4 [K ~=> F,huge ~=> E] f20.14 ~> f31.5 [K ~=> F] f20.4 ~> f20.14 [K ~=> F,huge ~=> E] f20.15 ~> f31.5 [K ~=> E,K ~=> F] f20.4 ~> f20.15 [K ~=> F,huge ~=> E] f31.12 ~> f45.6 [K ~=> F] f31.5 ~> f31.12 [K ~=> F] + Applied Processor: Lare + Details: f2.2 ~> exitus616.21 [A ~=> C ,K ~=> B ,K ~=> C ,K ~=> E ,K ~=> F ,K ~=> J ,K ~=> K ,huge ~=> E ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick ,K ~*> 0.0 ,K ~*> tick] f2.1 ~> exitus616.21 [K ~=> B] f2.0 ~> exitus616.21 [K ~=> A] + f60.8> [K ~=> B ,K ~=> C ,K ~=> E ,K ~=> F ,K ~=> J ,K ~=> K ,huge ~=> E ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~*> 0.0 ,K ~*> tick] f31.5> [K ~=> B ,K ~=> C ,K ~=> E ,K ~=> F ,K ~=> J ,K ~=> K ,huge ~=> E ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~*> 0.0 ,K ~*> tick] YES(?,O(n^1))