YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G,H,I,J) -> f19(A,0,C,D,E,F,G,H,I,J) [A >= 0 && 19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,0,E,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,0,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= E] 3. f55(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,0,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= F] 4. f59(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,1 + G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= G] 5. f59(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,1 + F,G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && G >= 20] 6. f55(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,1 + E,F,G,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && F >= 20] 7. f52(A,B,C,D,E,F,G,H,I,J) -> f73(A,B,C,D,E,F,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && E >= 20] 8. f36(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,1 + D,E,F,G,K,K,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,1 + C,D,E,F,G,H,I,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,0,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G,H,I,J) -> f19(A,1 + B,C,D,E,F,G,K,I,K) [B >= 0 && A + B >= 0 && A >= 0 && 19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G,H,I,J) -> f16(1 + A,B,C,D,E,F,G,H,I,J) [B >= 0 && A + B >= 0 && A >= 0 && B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,0,D,E,F,G,H,I,J) [A >= 0 && A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G,H,I,J) -> f16(0,B,C,D,E,F,G,0,I,J) True (1,1) Signature: {(f0,10);(f16,10);(f19,10);(f33,10);(f36,10);(f52,10);(f55,10);(f59,10);(f73,10)} Flow Graph: [0->{11,12},1->{8,9},2->{3,6},3->{4,5},4->{4,5},5->{3,6},6->{2,7},7->{},8->{8,9},9->{1,10},10->{2,7} ,11->{11,12},12->{0,13},13->{1,10},14->{0,13}] + 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. f16(A,B,C,D,E,F,G,H,I,J) -> f19(A,0,C,D,E,F,G,H,I,J) [A >= 0 && 19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,0,E,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,0,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= E] 3. f55(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,0,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= F] 4. f59(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,1 + G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= G] 5. f59(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,1 + F,G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && G >= 20] 6. f55(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,1 + E,F,G,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && F >= 20] 7. f52(A,B,C,D,E,F,G,H,I,J) -> f73(A,B,C,D,E,F,G,H,I,J) [E >= 0 (1,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && E >= 20] 8. f36(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,1 + D,E,F,G,K,K,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,1 + C,D,E,F,G,H,I,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,0,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G,H,I,J) -> f19(A,1 + B,C,D,E,F,G,K,I,K) [B >= 0 && A + B >= 0 && A >= 0 && 19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G,H,I,J) -> f16(1 + A,B,C,D,E,F,G,H,I,J) [B >= 0 && A + B >= 0 && A >= 0 && B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,0,D,E,F,G,H,I,J) [A >= 0 && A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G,H,I,J) -> f16(0,B,C,D,E,F,G,0,I,J) True (1,1) Signature: {(f0,10);(f16,10);(f19,10);(f33,10);(f36,10);(f52,10);(f55,10);(f59,10);(f73,10)} Flow Graph: [0->{11,12},1->{8,9},2->{3,6},3->{4,5},4->{4,5},5->{3,6},6->{2,7},7->{},8->{8,9},9->{1,10},10->{2,7} ,11->{11,12},12->{0,13},13->{1,10},14->{0,13}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,12),(1,9),(2,6),(3,5),(10,7),(13,10),(14,13)] * Step 3: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G,H,I,J) -> f19(A,0,C,D,E,F,G,H,I,J) [A >= 0 && 19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,0,E,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,0,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= E] 3. f55(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,0,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= F] 4. f59(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,1 + G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= G] 5. f59(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,1 + F,G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && G >= 20] 6. f55(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,1 + E,F,G,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && F >= 20] 7. f52(A,B,C,D,E,F,G,H,I,J) -> f73(A,B,C,D,E,F,G,H,I,J) [E >= 0 (1,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && E >= 20] 8. f36(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,1 + D,E,F,G,K,K,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,1 + C,D,E,F,G,H,I,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,0,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && C >= 20] (1,1) 11. f19(A,B,C,D,E,F,G,H,I,J) -> f19(A,1 + B,C,D,E,F,G,K,I,K) [B >= 0 && A + B >= 0 && A >= 0 && 19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G,H,I,J) -> f16(1 + A,B,C,D,E,F,G,H,I,J) [B >= 0 && A + B >= 0 && A >= 0 && B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,0,D,E,F,G,H,I,J) [A >= 0 && A >= 20] (1,1) 14. f0(A,B,C,D,E,F,G,H,I,J) -> f16(0,B,C,D,E,F,G,0,I,J) True (1,1) Signature: {(f0,10);(f16,10);(f19,10);(f33,10);(f36,10);(f52,10);(f55,10);(f59,10);(f73,10)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2,7},7->{},8->{8,9},9->{1,10},10->{2},11->{11,12} ,12->{0,13},13->{1},14->{0}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G,H,I,J) -> f19(A,0,C,D,E,F,G,H,I,J) [A >= 0 && 19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,0,E,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,0,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= E] 3. f55(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,0,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= F] 4. f59(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,1 + G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= G] 5. f59(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,1 + F,G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && G >= 20] 6. f55(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,1 + E,F,G,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && F >= 20] 7. f52(A,B,C,D,E,F,G,H,I,J) -> f73(A,B,C,D,E,F,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && E >= 20] 8. f36(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,1 + D,E,F,G,K,K,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,1 + C,D,E,F,G,H,I,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,0,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G,H,I,J) -> f19(A,1 + B,C,D,E,F,G,K,I,K) [B >= 0 && A + B >= 0 && A >= 0 && 19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G,H,I,J) -> f16(1 + A,B,C,D,E,F,G,H,I,J) [B >= 0 && A + B >= 0 && A >= 0 && B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,0,D,E,F,G,H,I,J) [A >= 0 && A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G,H,I,J) -> f16(0,B,C,D,E,F,G,0,I,J) True (1,1) 15. f52(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) Signature: {(exitus616,10);(f0,10);(f16,10);(f19,10);(f33,10);(f36,10);(f52,10);(f55,10);(f59,10);(f73,10)} Flow Graph: [0->{11,12},1->{8,9},2->{3,6},3->{4,5},4->{4,5},5->{3,6},6->{2,7,15},7->{},8->{8,9},9->{1,10},10->{2,7,15} ,11->{11,12},12->{0,13},13->{1,10},14->{0,13},15->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,12),(1,9),(2,6),(3,5),(10,7),(13,10),(14,13)] * Step 5: LooptreeTransformer WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G,H,I,J) -> f19(A,0,C,D,E,F,G,H,I,J) [A >= 0 && 19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,0,E,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,0,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= E] 3. f55(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,0,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= F] 4. f59(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,1 + G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= G] 5. f59(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,1 + F,G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && G >= 20] 6. f55(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,1 + E,F,G,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && F >= 20] 7. f52(A,B,C,D,E,F,G,H,I,J) -> f73(A,B,C,D,E,F,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && E >= 20] 8. f36(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,1 + D,E,F,G,K,K,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,1 + C,D,E,F,G,H,I,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,0,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G,H,I,J) -> f19(A,1 + B,C,D,E,F,G,K,I,K) [B >= 0 && A + B >= 0 && A >= 0 && 19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G,H,I,J) -> f16(1 + A,B,C,D,E,F,G,H,I,J) [B >= 0 && A + B >= 0 && A >= 0 && B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,0,D,E,F,G,H,I,J) [A >= 0 && A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G,H,I,J) -> f16(0,B,C,D,E,F,G,0,I,J) True (1,1) 15. f52(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) Signature: {(exitus616,10);(f0,10);(f16,10);(f19,10);(f33,10);(f36,10);(f52,10);(f55,10);(f59,10);(f73,10)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2,7,15},7->{},8->{8,9},9->{1,10},10->{2,15},11->{11 ,12},12->{0,13},13->{1},14->{0},15->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15] | +- p:[0,12,11] c: [0] | | | `- p:[11] c: [11] | +- p:[1,9,8] c: [1] | | | `- p:[8] c: [8] | `- p:[2,6,5,4,3] c: [2] | `- p:[3,5,4] c: [3] | `- p:[4] c: [4] * Step 6: SizeAbstraction WORST_CASE(?,O(1)) + Considered Problem: (Rules: 0. f16(A,B,C,D,E,F,G,H,I,J) -> f19(A,0,C,D,E,F,G,H,I,J) [A >= 0 && 19 >= A] (?,1) 1. f33(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,0,E,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= C] (?,1) 2. f52(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,0,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= E] 3. f55(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,0,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= F] 4. f59(A,B,C,D,E,F,G,H,I,J) -> f59(A,B,C,D,E,F,1 + G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && 19 >= G] 5. f59(A,B,C,D,E,F,G,H,I,J) -> f55(A,B,C,D,E,1 + F,G,H,I,J) [G >= 0 (?,1) && F + G >= 0 && E + G >= 0 && -20 + C + G >= 0 && -20 + A + G >= 0 && F >= 0 && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && G >= 20] 6. f55(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,1 + E,F,G,H,I,J) [F >= 0 (?,1) && E + F >= 0 && -20 + C + F >= 0 && -20 + A + F >= 0 && E >= 0 && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && F >= 20] 7. f52(A,B,C,D,E,F,G,H,I,J) -> f73(A,B,C,D,E,F,G,H,I,J) [E >= 0 (?,1) && -20 + C + E >= 0 && -20 + A + E >= 0 && -20 + C >= 0 && -40 + A + C >= 0 && -20 + A >= 0 && E >= 20] 8. f36(A,B,C,D,E,F,G,H,I,J) -> f36(A,B,C,1 + D,E,F,G,K,K,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && 19 >= D] (?,1) 9. f36(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,1 + C,D,E,F,G,H,I,J) [D >= 0 && C + D >= 0 && -20 + A + D >= 0 && C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && D >= 20] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J) -> f52(A,B,C,D,0,F,G,H,I,J) [C >= 0 && -20 + A + C >= 0 && -20 + A >= 0 && C >= 20] (?,1) 11. f19(A,B,C,D,E,F,G,H,I,J) -> f19(A,1 + B,C,D,E,F,G,K,I,K) [B >= 0 && A + B >= 0 && A >= 0 && 19 >= B] (?,1) 12. f19(A,B,C,D,E,F,G,H,I,J) -> f16(1 + A,B,C,D,E,F,G,H,I,J) [B >= 0 && A + B >= 0 && A >= 0 && B >= 20] (?,1) 13. f16(A,B,C,D,E,F,G,H,I,J) -> f33(A,B,0,D,E,F,G,H,I,J) [A >= 0 && A >= 20] (?,1) 14. f0(A,B,C,D,E,F,G,H,I,J) -> f16(0,B,C,D,E,F,G,0,I,J) True (1,1) 15. f52(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) Signature: {(exitus616,10);(f0,10);(f16,10);(f19,10);(f33,10);(f36,10);(f52,10);(f55,10);(f59,10);(f73,10)} Flow Graph: [0->{11},1->{8},2->{3},3->{4},4->{4,5},5->{3,6},6->{2,7,15},7->{},8->{8,9},9->{1,10},10->{2,15},11->{11 ,12},12->{0,13},13->{1},14->{0},15->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15] | +- p:[0,12,11] c: [0] | | | `- p:[11] c: [11] | +- p:[1,9,8] c: [1] | | | `- p:[8] c: [8] | `- p:[2,6,5,4,3] c: [2] | `- p:[3,5,4] c: [3] | `- p:[4] c: [4]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,0.0,0.0.0,0.1,0.1.0,0.2,0.2.0,0.2.0.0] f16 ~> f19 [A <= A, B <= 0*K, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f33 ~> f36 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f52 ~> f55 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= 0*K, G <= G, H <= H, I <= I, J <= J] f55 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 0*K, H <= H, I <= I, J <= J] f59 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 20*K, H <= H, I <= I, J <= J] f59 ~> f55 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F + G, G <= G, H <= H, I <= I, J <= J] f55 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E + F, F <= F, G <= G, H <= H, I <= I, J <= J] f52 ~> f73 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f36 ~> f36 [A <= A, B <= B, C <= C, D <= 20*K, E <= E, F <= F, G <= G, H <= unknown, I <= unknown, J <= J] f36 ~> f33 [A <= A, B <= B, C <= C + D, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f33 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= 0*K, F <= F, G <= G, H <= H, I <= I, J <= J] f19 ~> f19 [A <= A, B <= 20*K, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown, I <= I, J <= unknown] f19 ~> f16 [A <= A + B, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f16 ~> f33 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f0 ~> f16 [A <= 0*K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= I, J <= J] f52 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] + Loop: [0.0 <= 20*K + A] f16 ~> f19 [A <= A, B <= 0*K, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f19 ~> f16 [A <= A + B, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f19 ~> f19 [A <= A, B <= 20*K, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown, I <= I, J <= unknown] + Loop: [0.0.0 <= 20*K + B] f19 ~> f19 [A <= A, B <= 20*K, C <= C, D <= D, E <= E, F <= F, G <= G, H <= unknown, I <= I, J <= unknown] + Loop: [0.1 <= 20*K + C] f33 ~> f36 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f36 ~> f33 [A <= A, B <= B, C <= C + D, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J] f36 ~> f36 [A <= A, B <= B, C <= C, D <= 20*K, E <= E, F <= F, G <= G, H <= unknown, I <= unknown, J <= J] + Loop: [0.1.0 <= 20*K + D] f36 ~> f36 [A <= A, B <= B, C <= C, D <= 20*K, E <= E, F <= F, G <= G, H <= unknown, I <= unknown, J <= J] + Loop: [0.2 <= 20*K + E] f52 ~> f55 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= 0*K, G <= G, H <= H, I <= I, J <= J] f55 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E + F, F <= F, G <= G, H <= H, I <= I, J <= J] f59 ~> f55 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F + G, G <= G, H <= H, I <= I, J <= J] f59 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 20*K, H <= H, I <= I, J <= J] f55 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 0*K, H <= H, I <= I, J <= J] + Loop: [0.2.0 <= 20*K + F] f55 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 0*K, H <= H, I <= I, J <= J] f59 ~> f55 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F + G, G <= G, H <= H, I <= I, J <= J] f59 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 20*K, H <= H, I <= I, J <= J] + Loop: [0.2.0.0 <= 20*K + G] f59 ~> f59 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 20*K, H <= H, I <= I, J <= J] + 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,H,I,J,0.0,0.0.0,0.1,0.1.0,0.2,0.2.0,0.2.0.0] f16 ~> f19 [K ~=> B] f33 ~> f36 [K ~=> D] f52 ~> f55 [K ~=> F] f55 ~> f59 [K ~=> G] f59 ~> f59 [K ~=> G] f59 ~> f55 [F ~+> F,G ~+> F] f55 ~> f52 [E ~+> E,F ~+> E] f52 ~> f73 [] f36 ~> f36 [K ~=> D,huge ~=> H,huge ~=> I] f36 ~> f33 [C ~+> C,D ~+> C] f33 ~> f52 [K ~=> E] f19 ~> f19 [K ~=> B,huge ~=> H,huge ~=> J] f19 ~> f16 [A ~+> A,B ~+> A] f16 ~> f33 [K ~=> C] f0 ~> f16 [K ~=> A,K ~=> H] f52 ~> exitus616 [] + Loop: [A ~+> 0.0,K ~*> 0.0] f16 ~> f19 [K ~=> B] f19 ~> f16 [A ~+> A,B ~+> A] f19 ~> f19 [K ~=> B,huge ~=> H,huge ~=> J] + Loop: [B ~+> 0.0.0,K ~*> 0.0.0] f19 ~> f19 [K ~=> B,huge ~=> H,huge ~=> J] + Loop: [C ~+> 0.1,K ~*> 0.1] f33 ~> f36 [K ~=> D] f36 ~> f33 [C ~+> C,D ~+> C] f36 ~> f36 [K ~=> D,huge ~=> H,huge ~=> I] + Loop: [D ~+> 0.1.0,K ~*> 0.1.0] f36 ~> f36 [K ~=> D,huge ~=> H,huge ~=> I] + Loop: [E ~+> 0.2,K ~*> 0.2] f52 ~> f55 [K ~=> F] f55 ~> f52 [E ~+> E,F ~+> E] f59 ~> f55 [F ~+> F,G ~+> F] f59 ~> f59 [K ~=> G] f55 ~> f59 [K ~=> G] + Loop: [F ~+> 0.2.0,K ~*> 0.2.0] f55 ~> f59 [K ~=> G] f59 ~> f55 [F ~+> F,G ~+> F] f59 ~> f59 [K ~=> G] + Loop: [G ~+> 0.2.0.0,K ~*> 0.2.0.0] f59 ~> f59 [K ~=> G] + Applied Processor: LareProcessor + Details: f0 ~> exitus616 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> E ,K ~=> F ,K ~=> G ,K ~=> H ,huge ~=> H ,huge ~=> I ,huge ~=> J ,tick ~+> tick ,K ~+> A ,K ~+> C ,K ~+> E ,K ~+> F ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.2 ,K ~+> 0.2.0 ,K ~+> 0.2.0.0 ,K ~+> tick ,K ~*> A ,K ~*> C ,K ~*> E ,K ~*> F ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.2 ,K ~*> 0.2.0 ,K ~*> 0.2.0.0 ,K ~*> tick ,K ~^> E ,K ~^> F] f0 ~> f73 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> E ,K ~=> F ,K ~=> G ,K ~=> H ,huge ~=> H ,huge ~=> I ,huge ~=> J ,tick ~+> tick ,K ~+> A ,K ~+> C ,K ~+> E ,K ~+> F ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.1 ,K ~+> 0.1.0 ,K ~+> 0.2 ,K ~+> 0.2.0 ,K ~+> 0.2.0.0 ,K ~+> tick ,K ~*> A ,K ~*> C ,K ~*> E ,K ~*> F ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> 0.2 ,K ~*> 0.2.0 ,K ~*> 0.2.0.0 ,K ~*> tick ,K ~^> E ,K ~^> F] + f16> [K ~=> B ,huge ~=> H ,huge ~=> J ,A ~+> A ,A ~+> 0.0 ,A ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> tick ,K ~*> A ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick] + f19> [K ~=> B ,huge ~=> H ,huge ~=> J ,B ~+> 0.0.0 ,B ~+> tick ,tick ~+> tick ,K ~*> 0.0.0 ,K ~*> tick] + f33> [K ~=> D ,huge ~=> H ,huge ~=> I ,C ~+> C ,C ~+> 0.1 ,C ~+> tick ,tick ~+> tick ,K ~+> C ,K ~+> 0.1.0 ,K ~+> tick ,C ~*> C ,C ~*> tick ,K ~*> C ,K ~*> 0.1 ,K ~*> 0.1.0 ,K ~*> tick] + f36> [K ~=> D ,huge ~=> H ,huge ~=> I ,D ~+> 0.1.0 ,D ~+> tick ,tick ~+> tick ,K ~*> 0.1.0 ,K ~*> tick] + f52> [K ~=> F ,K ~=> G ,E ~+> E ,E ~+> 0.2 ,E ~+> tick ,tick ~+> tick ,K ~+> E ,K ~+> F ,K ~+> 0.2.0 ,K ~+> 0.2.0.0 ,K ~+> tick ,E ~*> E ,E ~*> F ,E ~*> tick ,K ~*> E ,K ~*> F ,K ~*> 0.2 ,K ~*> 0.2.0 ,K ~*> 0.2.0.0 ,K ~*> tick ,E ~^> E ,E ~^> F ,K ~^> E ,K ~^> F] + f55> [K ~=> G ,F ~+> F ,F ~+> 0.2.0 ,F ~+> tick ,tick ~+> tick ,K ~+> F ,K ~+> 0.2.0.0 ,K ~+> tick ,F ~*> F ,F ~*> tick ,K ~*> F ,K ~*> 0.2.0 ,K ~*> 0.2.0.0 ,K ~*> tick] + f59> [K ~=> G,G ~+> 0.2.0.0,G ~+> tick,tick ~+> tick,K ~*> 0.2.0.0,K ~*> tick] YES(?,O(1))