YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f34(5,8,0,0,E,F,G) True (1,1) 1. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f34(A,B,C,D,E,F,G) -> f42(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f42(A,B,C,D,E,F,G) -> f56(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f42(A,B,C,D,E,F,G) -> f45(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f56(A,B,C,D,E,F,G) -> f66(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f56(A,B,C,D,E,F,G) -> f56(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f56(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f45(A,B,C,D,E,F,G) -> f42(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f45(A,B,C,D,E,F,G) -> f45(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f66(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f66(A,B,C,D,E,F,G) -> f66(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f34,7);(f42,7);(f45,7);(f56,7);(f62,7);(f66,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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f34(5,8,0,0,E,F,G) True (1,1) 1. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f34(A,B,C,D,E,F,G) -> f42(A,B,C,0,E,F,G) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f42(A,B,C,D,E,F,G) -> f56(A,B,C,0,E,F,G) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f42(A,B,C,D,E,F,G) -> f45(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f56(A,B,C,D,E,F,G) -> f66(A,B,C,0,E,F,G) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f56(A,B,C,D,E,F,G) -> f56(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f56(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,H,I) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f45(A,B,C,D,E,F,G) -> f42(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f45(A,B,C,D,E,F,G) -> f45(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f66(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,F,G) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f66(A,B,C,D,E,F,G) -> f66(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f34,7);(f42,7);(f45,7);(f56,7);(f62,7);(f66,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: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f34(5,8,0,0,E,F,G) True (1,1) 1. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f34(A,B,C,D,E,F,G) -> f42(A,B,C,0,E,F,G) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f42(A,B,C,D,E,F,G) -> f56(A,B,C,0,E,F,G) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f42(A,B,C,D,E,F,G) -> f45(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f56(A,B,C,D,E,F,G) -> f66(A,B,C,0,E,F,G) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f56(A,B,C,D,E,F,G) -> f56(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f56(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,H,I) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f45(A,B,C,D,E,F,G) -> f42(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f45(A,B,C,D,E,F,G) -> f45(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f66(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,F,G) [D >= 0 (1,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f66(A,B,C,D,E,F,G) -> f66(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] Signature: {(f0,7);(f34,7);(f42,7);(f45,7);(f56,7);(f62,7);(f66,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: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f34(5,8,0,0,E,F,G) True (1,1) 1. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f34(A,B,C,D,E,F,G) -> f42(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f42(A,B,C,D,E,F,G) -> f56(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f42(A,B,C,D,E,F,G) -> f45(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f56(A,B,C,D,E,F,G) -> f66(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f56(A,B,C,D,E,F,G) -> f56(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f56(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f45(A,B,C,D,E,F,G) -> f42(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f45(A,B,C,D,E,F,G) -> f45(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f66(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f66(A,B,C,D,E,F,G) -> f66(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 13. f56(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True (?,1) 14. f66(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True (?,1) Signature: {(exitus616,7);(f0,7);(f34,7);(f42,7);(f45,7);(f56,7);(f62,7);(f66,7)} Flow Graph: [0->{1,2,3},1->{1,2,3},2->{4,5},3->{1,2,3},4->{6,7,8,13},5->{9,10},6->{11,12,14},7->{6,7,8,13},8->{},9->{4 ,5},10->{9,10},11->{},12->{11,12,14},13->{},14->{}] + 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 5: LooptreeTransformer WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G) -> f34(5,8,0,0,E,F,G) True (1,1) 1. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f34(A,B,C,D,E,F,G) -> f42(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f42(A,B,C,D,E,F,G) -> f56(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f42(A,B,C,D,E,F,G) -> f45(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f56(A,B,C,D,E,F,G) -> f66(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f56(A,B,C,D,E,F,G) -> f56(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f56(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f45(A,B,C,D,E,F,G) -> f42(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f45(A,B,C,D,E,F,G) -> f45(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f66(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f66(A,B,C,D,E,F,G) -> f66(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 13. f56(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True (?,1) 14. f66(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True (?,1) Signature: {(exitus616,7);(f0,7);(f34,7);(f42,7);(f45,7);(f56,7);(f62,7);(f66,7)} Flow Graph: [0->{1},1->{3},2->{5},3->{2,3},4->{7,8,13},5->{10},6->{12,14},7->{6,7,8,13},8->{},9->{4,5},10->{9,10} ,11->{},12->{11,12,14},13->{},14->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | +- p:[3] c: [3] | +- p:[5,9,10] c: [5] | | | `- p:[10] c: [10] | +- p:[7] c: [7] | `- p:[12] c: [12] * Step 6: SizeAbstraction WORST_CASE(?,O(1)) + Considered Problem: (Rules: 0. f0(A,B,C,D,E,F,G) -> f34(5,8,0,0,E,F,G) True (1,1) 1. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + C,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && C = D] 2. f34(A,B,C,D,E,F,G) -> f42(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 3. f34(A,B,C,D,E,F,G) -> f34(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D && D >= 1 + C] 4. f42(A,B,C,D,E,F,G) -> f56(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 5. f42(A,B,C,D,E,F,G) -> f45(A,B,C,D,0,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 6. f56(A,B,C,D,E,F,G) -> f66(A,B,C,0,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= B] 7. f56(A,B,C,D,E,F,G) -> f56(A,B,C,1 + D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 8. f56(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,H,I) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + D] 9. f45(A,B,C,D,E,F,G) -> f42(A,B,C,1 + D,E,F,G) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && E >= B] 10. f45(A,B,C,D,E,F,G) -> f45(A,B,C,D,1 + E,H,I) [E >= 0 (?,1) && D + E >= 0 && C + E >= 0 && -1*C + E >= 0 && -8 + B + E >= 0 && 8 + -1*B + E >= 0 && -5 + A + E >= 0 && 5 + -1*A + E >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && B >= 1 + E] 11. f66(A,B,C,D,E,F,G) -> f62(A,B,C,D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && D >= A] 12. f66(A,B,C,D,E,F,G) -> f66(A,B,C,1 + D,E,F,G) [D >= 0 (?,1) && C + D >= 0 && -1*C + D >= 0 && -8 + B + D >= 0 && 8 + -1*B + D >= 0 && -5 + A + D >= 0 && 5 + -1*A + D >= 0 && -1*C >= 0 && -8 + B + -1*C >= 0 && 8 + -1*B + -1*C >= 0 && -5 + A + -1*C >= 0 && 5 + -1*A + -1*C >= 0 && C >= 0 && -8 + B + C >= 0 && 8 + -1*B + C >= 0 && -5 + A + C >= 0 && 5 + -1*A + C >= 0 && 8 + -1*B >= 0 && 3 + A + -1*B >= 0 && 13 + -1*A + -1*B >= 0 && -8 + B >= 0 && -13 + A + B >= 0 && -3 + -1*A + B >= 0 && 5 + -1*A >= 0 && -5 + A >= 0 && A >= 1 + D] 13. f56(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True (?,1) 14. f66(A,B,C,D,E,F,G) -> exitus616(A,B,C,D,E,F,G) True (?,1) Signature: {(exitus616,7);(f0,7);(f34,7);(f42,7);(f45,7);(f56,7);(f62,7);(f66,7)} Flow Graph: [0->{1},1->{3},2->{5},3->{2,3},4->{7,8,13},5->{10},6->{12,14},7->{6,7,8,13},8->{},9->{4,5},10->{9,10} ,11->{},12->{11,12,14},13->{},14->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | +- p:[3] c: [3] | +- p:[5,9,10] c: [5] | | | `- p:[10] c: [10] | +- p:[7] c: [7] | `- p:[12] c: [12]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,0.0,0.1,0.1.0,0.2,0.3] f0 ~> f34 [A <= 5*K, B <= 8*K, C <= 0*K, D <= 0*K, E <= E, F <= F, G <= G] f34 ~> f34 [A <= A, B <= B, C <= C, D <= K, E <= E, F <= F, G <= G] f34 ~> f42 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= F, G <= G] f34 ~> f34 [A <= A, B <= B, C <= C, D <= 5*K, E <= E, F <= F, G <= G] f42 ~> f56 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= F, G <= G] f42 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= 0*K, F <= F, G <= G] f56 ~> f66 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= F, G <= G] f56 ~> f56 [A <= A, B <= B, C <= C, D <= 8*K, E <= E, F <= unknown, G <= unknown] f56 ~> f62 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= unknown, G <= unknown] f45 ~> f42 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G] f45 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= 8*K, F <= unknown, G <= unknown] f66 ~> f62 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G] f66 ~> f66 [A <= A, B <= B, C <= C, D <= 5*K, E <= E, F <= F, G <= G] f56 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G] f66 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G] + Loop: [0.0 <= A + D] f34 ~> f34 [A <= A, B <= B, C <= C, D <= 5*K, E <= E, F <= F, G <= G] + Loop: [0.1 <= 2*K + A + D] f42 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= 0*K, F <= F, G <= G] f45 ~> f42 [A <= A, B <= B, C <= C, D <= D + E, E <= E, F <= F, G <= G] f45 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= 8*K, F <= unknown, G <= unknown] + Loop: [0.1.0 <= B + E] f45 ~> f45 [A <= A, B <= B, C <= C, D <= D, E <= 8*K, F <= unknown, G <= unknown] + Loop: [0.2 <= B + D] f56 ~> f56 [A <= A, B <= B, C <= C, D <= 8*K, E <= E, F <= unknown, G <= unknown] + Loop: [0.3 <= A + D] f66 ~> f66 [A <= A, B <= B, C <= C, D <= 5*K, E <= E, F <= F, G <= G] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,0.0,0.1,0.1.0,0.2,0.3] f0 ~> f34 [K ~=> A,K ~=> B,K ~=> C,K ~=> D] f34 ~> f34 [K ~=> D] f34 ~> f42 [K ~=> D] f34 ~> f34 [K ~=> D] f42 ~> f56 [K ~=> D] f42 ~> f45 [K ~=> E] f56 ~> f66 [K ~=> D] f56 ~> f56 [K ~=> D,huge ~=> F,huge ~=> G] f56 ~> f62 [huge ~=> F,huge ~=> G] f45 ~> f42 [D ~+> D,E ~+> D] f45 ~> f45 [K ~=> E,huge ~=> F,huge ~=> G] f66 ~> f62 [] f66 ~> f66 [K ~=> D] f56 ~> exitus616 [] f66 ~> exitus616 [] + Loop: [A ~+> 0.0,D ~+> 0.0] f34 ~> f34 [K ~=> D] + Loop: [A ~+> 0.1,D ~+> 0.1,K ~*> 0.1] f42 ~> f45 [K ~=> E] f45 ~> f42 [D ~+> D,E ~+> D] f45 ~> f45 [K ~=> E,huge ~=> F,huge ~=> G] + Loop: [B ~+> 0.1.0,E ~+> 0.1.0] f45 ~> f45 [K ~=> E,huge ~=> F,huge ~=> G] + Loop: [B ~+> 0.2,D ~+> 0.2] f56 ~> f56 [K ~=> D,huge ~=> F,huge ~=> G] + Loop: [A ~+> 0.3,D ~+> 0.3] f66 ~> f66 [K ~=> D] + Applied Processor: LareProcessor + Details: f0 ~> f62 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> E ,huge ~=> F ,huge ~=> G ,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] f0 ~> exitus616 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> E ,huge ~=> F ,huge ~=> G ,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] + f34> [K ~=> D,A ~+> 0.0,A ~+> tick,D ~+> 0.0,D ~+> tick,tick ~+> tick] + f42> [K ~=> E ,huge ~=> F ,huge ~=> G ,A ~+> 0.1 ,A ~+> tick ,B ~+> 0.1.0 ,B ~+> tick ,D ~+> D ,D ~+> 0.1 ,D ~+> tick ,tick ~+> tick ,K ~+> D ,K ~+> 0.1.0 ,K ~+> tick ,A ~*> D ,A ~*> tick ,B ~*> tick ,D ~*> D ,D ~*> tick ,K ~*> D ,K ~*> 0.1 ,K ~*> tick] + f45> [K ~=> E ,huge ~=> F ,huge ~=> G ,B ~+> 0.1.0 ,B ~+> tick ,E ~+> 0.1.0 ,E ~+> tick ,tick ~+> tick] + f56> [K ~=> D,huge ~=> F,huge ~=> G,B ~+> 0.2,B ~+> tick,D ~+> 0.2,D ~+> tick,tick ~+> tick] + f66> [K ~=> D,A ~+> 0.3,A ~+> tick,D ~+> 0.3,D ~+> tick,tick ~+> tick] YES(?,O(1))