YES(?,O(1)) * Step 1: ArgumentFilter WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f40(5,10,0,0,E,F,G) True (1,1) 1. f40(A,B,C,D,E,F,G) -> f40(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f40(A,B,C,D,E,F,G) -> f48(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f40(A,B,C,D,E,F,G) -> f40(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f48(A,B,C,D,E,F,G) -> f62(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f48(A,B,C,D,E,F,G) -> f51(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f62(A,B,C,D,E,F,G) -> f72(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f62(A,B,C,D,E,F,G) -> f62(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f62(A,B,C,D,E,F,G) -> f68(A,B,C,D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f51(A,B,C,D,E,F,G) -> f48(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f51(A,B,C,D,E,F,G) -> f51(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f72(A,B,C,D,E,F,G) -> f68(A,B,C,D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f72(A,B,C,D,E,F,G) -> f72(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f40,7);(f48,7);(f51,7);(f62,7);(f68,7);(f72,7)} Flow Graph: [0->{1,2,3},1->{1,2,3},2->{4,5},3->{1,2,3},4->{6,7,8},5->{9,10},6->{11,12},7->{6,7,8},8->{},9->{4,5} ,10->{9,10},11->{},12->{11,12}] + Applied Processor: ArgumentFilter [5,6] + Details: We remove following argument positions: [5,6]. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E) -> f40(5,10,0,0,E) True (1,1) 1. f40(A,B,C,D,E) -> f40(A,B,C,1 + C,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f40(A,B,C,D,E) -> f48(A,B,C,0,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f40(A,B,C,D,E) -> f40(A,B,C,1 + D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f48(A,B,C,D,E) -> f62(A,B,C,0,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f48(A,B,C,D,E) -> f51(A,B,C,D,0) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f62(A,B,C,D,E) -> f72(A,B,C,0,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f62(A,B,C,D,E) -> f62(A,B,C,1 + D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f62(A,B,C,D,E) -> f68(A,B,C,D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f51(A,B,C,D,E) -> f48(A,B,C,1 + D,E) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f51(A,B,C,D,E) -> f51(A,B,C,D,1 + E) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f72(A,B,C,D,E) -> f68(A,B,C,D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f72(A,B,C,D,E) -> f72(A,B,C,1 + D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f40,7);(f48,7);(f51,7);(f62,7);(f68,7);(f72,7)} Flow Graph: [0->{1,2,3},1->{1,2,3},2->{4,5},3->{1,2,3},4->{6,7,8},5->{9,10},6->{11,12},7->{6,7,8},8->{},9->{4,5} ,10->{9,10},11->{},12->{11,12}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2) ,(0,3) ,(1,1) ,(1,2) ,(2,4) ,(3,1) ,(4,6) ,(5,9) ,(6,11)] * Step 3: FromIts WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E) -> f40(5,10,0,0,E) True (1,1) 1. f40(A,B,C,D,E) -> f40(A,B,C,1 + C,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f40(A,B,C,D,E) -> f48(A,B,C,0,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f40(A,B,C,D,E) -> f40(A,B,C,1 + D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f48(A,B,C,D,E) -> f62(A,B,C,0,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f48(A,B,C,D,E) -> f51(A,B,C,D,0) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f62(A,B,C,D,E) -> f72(A,B,C,0,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f62(A,B,C,D,E) -> f62(A,B,C,1 + D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f62(A,B,C,D,E) -> f68(A,B,C,D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f51(A,B,C,D,E) -> f48(A,B,C,1 + D,E) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f51(A,B,C,D,E) -> f51(A,B,C,D,1 + E) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f72(A,B,C,D,E) -> f68(A,B,C,D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f72(A,B,C,D,E) -> f72(A,B,C,1 + D,E) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f40,7);(f48,7);(f51,7);(f62,7);(f68,7);(f72,7)} Flow Graph: [0->{1},1->{3},2->{5},3->{2,3},4->{7,8},5->{10},6->{12},7->{6,7,8},8->{},9->{4,5},10->{9,10},11->{} ,12->{11,12}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: f0(A,B,C,D,E) -> f40(5,10,0,0,E) True f40(A,B,C,D,E) -> f40(A,B,C,1 + C,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] f40(A,B,C,D,E) -> f48(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f40(A,B,C,D,E) -> f40(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f48(A,B,C,D,E) -> f62(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f48(A,B,C,D,E) -> f51(A,B,C,D,0) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f62(A,B,C,D,E) -> f72(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] f62(A,B,C,D,E) -> f62(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f62(A,B,C,D,E) -> f68(A,B,C,D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f51(A,B,C,D,E) -> f48(A,B,C,1 + D,E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f51(A,B,C,D,E) -> f51(A,B,C,D,1 + E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f72(A,B,C,D,E) -> f68(A,B,C,D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f72(A,B,C,D,E) -> f72(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f40,7);(f48,7);(f51,7);(f62,7);(f68,7);(f72,7)} Rule Graph: [0->{1},1->{3},2->{5},3->{2,3},4->{7,8},5->{10},6->{12},7->{6,7,8},8->{},9->{4,5},10->{9,10},11->{} ,12->{11,12}] + Applied Processor: AddSinks + Details: () * Step 5: Unfold WORST_CASE(?,O(1)) + Considered Problem: Rules: f0(A,B,C,D,E) -> f40(5,10,0,0,E) True f40(A,B,C,D,E) -> f40(A,B,C,1 + C,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] f40(A,B,C,D,E) -> f48(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f40(A,B,C,D,E) -> f40(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f48(A,B,C,D,E) -> f62(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f48(A,B,C,D,E) -> f51(A,B,C,D,0) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f62(A,B,C,D,E) -> f72(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] f62(A,B,C,D,E) -> f62(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f62(A,B,C,D,E) -> f68(A,B,C,D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f51(A,B,C,D,E) -> f48(A,B,C,1 + D,E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f51(A,B,C,D,E) -> f51(A,B,C,D,1 + E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f72(A,B,C,D,E) -> f68(A,B,C,D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f72(A,B,C,D,E) -> f72(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f68(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f68(A,B,C,D,E) -> exitus616(A,B,C,D,E) True Signature: {(exitus616,5);(f0,7);(f40,7);(f48,7);(f51,7);(f62,7);(f68,7);(f72,7)} Rule Graph: [0->{1},1->{3},2->{5},3->{2,3},4->{7,8},5->{10},6->{12},7->{6,7,8},8->{13},9->{4,5},10->{9,10},11->{14} ,12->{11,12}] + Applied Processor: Unfold + Details: () * Step 6: Decompose WORST_CASE(?,O(1)) + Considered Problem: Rules: f0.0(A,B,C,D,E) -> f40.1(5,10,0,0,E) True f40.1(A,B,C,D,E) -> f40.3(A,B,C,1 + C,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] f40.2(A,B,C,D,E) -> f48.5(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f40.3(A,B,C,D,E) -> f40.2(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f40.3(A,B,C,D,E) -> f40.3(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f48.4(A,B,C,D,E) -> f62.7(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f48.4(A,B,C,D,E) -> f62.8(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f48.5(A,B,C,D,E) -> f51.10(A,B,C,D,0) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f62.6(A,B,C,D,E) -> f72.12(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] f62.7(A,B,C,D,E) -> f62.6(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f62.7(A,B,C,D,E) -> f62.7(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f62.7(A,B,C,D,E) -> f62.8(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f62.8(A,B,C,D,E) -> f68.13(A,B,C,D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f51.9(A,B,C,D,E) -> f48.4(A,B,C,1 + D,E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f51.9(A,B,C,D,E) -> f48.5(A,B,C,1 + D,E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f51.10(A,B,C,D,E) -> f51.9(A,B,C,D,1 + E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f51.10(A,B,C,D,E) -> f51.10(A,B,C,D,1 + E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f72.11(A,B,C,D,E) -> f68.14(A,B,C,D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f72.12(A,B,C,D,E) -> f72.11(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f72.12(A,B,C,D,E) -> f72.12(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f68.13(A,B,C,D,E) -> exitus616.15(A,B,C,D,E) True f68.14(A,B,C,D,E) -> exitus616.15(A,B,C,D,E) True Signature: {(exitus616.15,5) ;(f0.0,5) ;(f40.1,5) ;(f40.2,5) ;(f40.3,5) ;(f48.4,5) ;(f48.5,5) ;(f51.10,5) ;(f51.9,5) ;(f62.6,5) ;(f62.7,5) ;(f62.8,5) ;(f68.13,5) ;(f68.14,5) ;(f72.11,5) ;(f72.12,5)} Rule Graph: [0->{1},1->{3,4},2->{7},3->{2},4->{3,4},5->{9,10,11},6->{12},7->{15,16},8->{18,19},9->{8},10->{9,10,11} ,11->{12},12->{20},13->{5,6},14->{7},15->{13,14},16->{15,16},17->{21},18->{17},19->{18,19},20->{},21->{}] + 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] | +- p:[4] c: [4] | +- p:[7,14,15,16] c: [7,14,15] | | | `- p:[16] c: [16] | +- p:[10] c: [10] | `- p:[19] c: [19] * Step 7: AbstractSize WORST_CASE(?,O(1)) + Considered Problem: (Rules: f0.0(A,B,C,D,E) -> f40.1(5,10,0,0,E) True f40.1(A,B,C,D,E) -> f40.3(A,B,C,1 + C,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] f40.2(A,B,C,D,E) -> f48.5(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f40.3(A,B,C,D,E) -> f40.2(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f40.3(A,B,C,D,E) -> f40.3(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] f48.4(A,B,C,D,E) -> f62.7(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f48.4(A,B,C,D,E) -> f62.8(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f48.5(A,B,C,D,E) -> f51.10(A,B,C,D,0) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f62.6(A,B,C,D,E) -> f72.12(A,B,C,0,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] f62.7(A,B,C,D,E) -> f62.6(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f62.7(A,B,C,D,E) -> f62.7(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f62.7(A,B,C,D,E) -> f62.8(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f62.8(A,B,C,D,E) -> f68.13(A,B,C,D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] f51.9(A,B,C,D,E) -> f48.4(A,B,C,1 + D,E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f51.9(A,B,C,D,E) -> f48.5(A,B,C,1 + D,E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] f51.10(A,B,C,D,E) -> f51.9(A,B,C,D,1 + E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f51.10(A,B,C,D,E) -> f51.10(A,B,C,D,1 + E) [E >= 0 && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -10 + B + E >= 0 && 10 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] f72.11(A,B,C,D,E) -> f68.14(A,B,C,D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] f72.12(A,B,C,D,E) -> f72.11(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f72.12(A,B,C,D,E) -> f72.12(A,B,C,1 + D,E) [D >= 0 && C + D >= 0 && -1*C + D >= 0 && -10 + B + D >= 0 && 10 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -10 + B + -1*C >= 0 && 10 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -10 + B + C >= 0 && 10 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 10 + -1*B >= 0 && 5 + A + -1*B >= 0 && 15 + -1*A + -1*B >= 0 && -10 + B >= 0 && -15 + A + B >= 0 && -5 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] f68.13(A,B,C,D,E) -> exitus616.15(A,B,C,D,E) True f68.14(A,B,C,D,E) -> exitus616.15(A,B,C,D,E) True Signature: {(exitus616.15,5) ;(f0.0,5) ;(f40.1,5) ;(f40.2,5) ;(f40.3,5) ;(f48.4,5) ;(f48.5,5) ;(f51.10,5) ;(f51.9,5) ;(f62.6,5) ;(f62.7,5) ;(f62.8,5) ;(f68.13,5) ;(f68.14,5) ;(f72.11,5) ;(f72.12,5)} Rule Graph: [0->{1},1->{3,4},2->{7},3->{2},4->{3,4},5->{9,10,11},6->{12},7->{15,16},8->{18,19},9->{8},10->{9,10,11} ,11->{12},12->{20},13->{5,6},14->{7},15->{13,14},16->{15,16},17->{21},18->{17},19->{18,19},20->{},21->{}] ,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] | +- p:[4] c: [4] | +- p:[7,14,15,16] c: [7,14,15] | | | `- p:[16] c: [16] | +- p:[10] c: [10] | `- p:[19] c: [19]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,C,D,E,0.0,0.1,0.1.0,0.2,0.3] f0.0 ~> f40.1 [A <= 5*K, B <= 10*K, C <= 0*K, D <= 0*K, E <= E] f40.1 ~> f40.3 [A <= A, B <= B, C <= C, D <= K, E <= E] f40.2 ~> f48.5 [A <= A, B <= B, C <= C, D <= 0*K, E <= E] f40.3 ~> f40.2 [A <= A, B <= B, C <= C, D <= 5*K, E <= E] f40.3 ~> f40.3 [A <= A, B <= B, C <= C, D <= 5*K, E <= E] f48.4 ~> f62.7 [A <= A, B <= B, C <= C, D <= 0*K, E <= E] f48.4 ~> f62.8 [A <= A, B <= B, C <= C, D <= 0*K, E <= E] f48.5 ~> f51.10 [A <= A, B <= B, C <= C, D <= D, E <= 0*K] f62.6 ~> f72.12 [A <= A, B <= B, C <= C, D <= 0*K, E <= E] f62.7 ~> f62.6 [A <= A, B <= B, C <= C, D <= 10*K, E <= E] f62.7 ~> f62.7 [A <= A, B <= B, C <= C, D <= 10*K, E <= E] f62.7 ~> f62.8 [A <= A, B <= B, C <= C, D <= 10*K, E <= E] f62.8 ~> f68.13 [A <= A, B <= B, C <= C, D <= D, E <= E] f51.9 ~> f48.4 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f51.9 ~> f48.5 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f51.10 ~> f51.9 [A <= A, B <= B, C <= C, D <= D, E <= 10*K] f51.10 ~> f51.10 [A <= A, B <= B, C <= C, D <= D, E <= 10*K] f72.11 ~> f68.14 [A <= A, B <= B, C <= C, D <= D, E <= E] f72.12 ~> f72.11 [A <= A, B <= B, C <= C, D <= 5*K, E <= E] f72.12 ~> f72.12 [A <= A, B <= B, C <= C, D <= 5*K, E <= E] f68.13 ~> exitus616.15 [A <= A, B <= B, C <= C, D <= D, E <= E] f68.14 ~> exitus616.15 [A <= A, B <= B, C <= C, D <= D, E <= E] + Loop: [0.0 <= K + A + D] f40.3 ~> f40.3 [A <= A, B <= B, C <= C, D <= 5*K, E <= E] + Loop: [0.1 <= K + A + D] f48.5 ~> f51.10 [A <= A, B <= B, C <= C, D <= D, E <= 0*K] f51.9 ~> f48.5 [A <= A, B <= B, C <= C, D <= D + E, E <= E] f51.10 ~> f51.9 [A <= A, B <= B, C <= C, D <= D, E <= 10*K] f51.10 ~> f51.10 [A <= A, B <= B, C <= C, D <= D, E <= 10*K] + Loop: [0.1.0 <= K + B + E] f51.10 ~> f51.10 [A <= A, B <= B, C <= C, D <= D, E <= 10*K] + Loop: [0.2 <= K + B + D] f62.7 ~> f62.7 [A <= A, B <= B, C <= C, D <= 10*K, E <= E] + Loop: [0.3 <= K + A + D] f72.12 ~> f72.12 [A <= A, B <= B, C <= C, D <= 5*K, E <= E] + Applied Processor: AbstractFlow + Details: () * Step 9: Lare WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,0.0,0.1,0.1.0,0.2,0.3] f0.0 ~> f40.1 [K ~=> A,K ~=> B,K ~=> C,K ~=> D] f40.1 ~> f40.3 [K ~=> D] f40.2 ~> f48.5 [K ~=> D] f40.3 ~> f40.2 [K ~=> D] f40.3 ~> f40.3 [K ~=> D] f48.4 ~> f62.7 [K ~=> D] f48.4 ~> f62.8 [K ~=> D] f48.5 ~> f51.10 [K ~=> E] f62.6 ~> f72.12 [K ~=> D] f62.7 ~> f62.6 [K ~=> D] f62.7 ~> f62.7 [K ~=> D] f62.7 ~> f62.8 [K ~=> D] f62.8 ~> f68.13 [] f51.9 ~> f48.4 [D ~+> D,E ~+> D] f51.9 ~> f48.5 [D ~+> D,E ~+> D] f51.10 ~> f51.9 [K ~=> E] f51.10 ~> f51.10 [K ~=> E] f72.11 ~> f68.14 [] f72.12 ~> f72.11 [K ~=> D] f72.12 ~> f72.12 [K ~=> D] f68.13 ~> exitus616.15 [] f68.14 ~> exitus616.15 [] + Loop: [A ~+> 0.0,D ~+> 0.0,K ~+> 0.0] f40.3 ~> f40.3 [K ~=> D] + Loop: [A ~+> 0.1,D ~+> 0.1,K ~+> 0.1] f48.5 ~> f51.10 [K ~=> E] f51.9 ~> f48.5 [D ~+> D,E ~+> D] f51.10 ~> f51.9 [K ~=> E] f51.10 ~> f51.10 [K ~=> E] + Loop: [B ~+> 0.1.0,E ~+> 0.1.0,K ~+> 0.1.0] f51.10 ~> f51.10 [K ~=> E] + Loop: [B ~+> 0.2,D ~+> 0.2,K ~+> 0.2] f62.7 ~> f62.7 [K ~=> D] + Loop: [A ~+> 0.3,D ~+> 0.3,K ~+> 0.3] f72.12 ~> f72.12 [K ~=> D] + Applied Processor: Lare + Details: f0.0 ~> exitus616.15 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> E ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> tick ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> tick] + f40.3> [K ~=> D,A ~+> 0.0,A ~+> tick,D ~+> 0.0,D ~+> tick,tick ~+> tick,K ~+> 0.0,K ~+> tick] + f51.9> [K ~=> E ,A ~+> 0.1 ,A ~+> tick ,B ~+> 0.1.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.1 ,D ~+> tick ,E ~+> D ,tick ~+> tick ,K ~+> D ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> D ,A ~*> tick ,B ~*> tick ,D ~*> D ,D ~*> tick ,K ~*> D ,K ~*> 0.1.0 ,K ~*> tick] + f51.10> [K ~=> E ,B ~+> 0.1.0 ,B ~+> tick ,E ~+> 0.1.0 ,E ~+> tick ,tick ~+> tick ,K ~+> 0.1.0 ,K ~+> tick] + f62.7> [K ~=> D,B ~+> 0.2,B ~+> tick,D ~+> 0.2,D ~+> tick,tick ~+> tick,K ~+> 0.2,K ~+> tick] + f72.12> [K ~=> D ,A ~+> 0.3 ,A ~+> tick ,D ~+> 0.3 ,D ~+> tick ,tick ~+> tick ,K ~+> 0.3 ,K ~+> tick] YES(?,O(1))