YES(?,O(1)) * Step 1: ArgumentFilter WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I) -> f17(0,J,K,0,E,F,G,H,I) True (1,1) 1. f17(A,B,C,D,E,F,G,H,I) -> f17(A,B,C,1 + D,E,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= D] (?,1) 2. f27(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,1 + E,F,G,H,I) [E >= 0 (?,1) && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= E] 3. f37(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,1 + F,G,H,I) [F >= 0 (?,1) && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= F] 4. f45(A,B,C,D,E,F,G,H,I) -> f45(1 + A,B,C,D,E,F,G,H,I) [-50 + F >= 0 (?,1) && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] 5. f55(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,1 + G,H,I) [G >= 0 (?,1) && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= G] 6. f65(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,1 + H,I) [H >= 0 (?,1) && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= H] 7. f75(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,1 + I) [I >= 0 (?,1) && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= I] 8. f83(A,B,C,D,E,F,G,H,I) -> f83(1 + A,B,C,D,E,F,G,H,I) [-50 + I >= 0 (?,1) && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] 9. f83(A,B,C,D,E,F,G,H,I) -> f93(A,B,C,D,E,F,G,H,I) [-50 + I >= 0 (?,1) && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] 10. f75(A,B,C,D,E,F,G,H,I) -> f83(0,B,C,D,E,F,G,H,I) [I >= 0 (?,1) && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && I >= 50] 11. f65(A,B,C,D,E,F,G,H,I) -> f75(A,B,C,D,E,F,G,H,0) [H >= 0 (?,1) && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && H >= 50] 12. f55(A,B,C,D,E,F,G,H,I) -> f65(A,B,C,D,E,F,G,0,I) [G >= 0 (?,1) && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && G >= 50] 13. f45(A,B,C,D,E,F,G,H,I) -> f55(A,B,C,D,E,F,0,H,I) [-50 + F >= 0 (?,1) && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] 14. f37(A,B,C,D,E,F,G,H,I) -> f45(0,B,C,D,E,F,G,H,I) [F >= 0 (?,1) && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 50] 15. f27(A,B,C,D,E,F,G,H,I) -> f37(A,B,C,D,E,0,G,H,I) [E >= 0 (?,1) && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 50] 16. f17(A,B,C,D,E,F,G,H,I) -> f27(A,B,C,D,0,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= 50] (?,1) Signature: {(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)} Flow Graph: [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9} ,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}] + Applied Processor: ArgumentFilter [1,2] + Details: We remove following argument positions: [1,2]. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1) 1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= D] (?,1) 2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [E >= 0 (?,1) && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= E] 3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [F >= 0 (?,1) && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= F] 4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [-50 + F >= 0 (?,1) && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] 5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [G >= 0 (?,1) && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= G] 6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [H >= 0 (?,1) && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= H] 7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [I >= 0 (?,1) && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= I] 8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [-50 + I >= 0 (?,1) && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] 9. f83(A,D,E,F,G,H,I) -> f93(A,D,E,F,G,H,I) [-50 + I >= 0 (?,1) && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] 10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 0 (?,1) && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && I >= 50] 11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 0 (?,1) && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && H >= 50] 12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 0 (?,1) && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && G >= 50] 13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [-50 + F >= 0 (?,1) && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] 14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 0 (?,1) && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 50] 15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 0 (?,1) && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 50] 16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= 50] (?,1) Signature: {(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)} Flow Graph: [0->{1,16},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8,9} ,11->{7,10},12->{6,11},13->{5,12},14->{4,13},15->{3,14},16->{2,15}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,16) ,(10,9) ,(11,10) ,(12,11) ,(13,12) ,(14,13) ,(15,14) ,(16,15)] * Step 3: FromIts WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True (1,1) 1. f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= D] (?,1) 2. f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [E >= 0 (?,1) && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= E] 3. f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [F >= 0 (?,1) && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= F] 4. f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [-50 + F >= 0 (?,1) && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] 5. f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [G >= 0 (?,1) && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= G] 6. f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [H >= 0 (?,1) && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= H] 7. f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [I >= 0 (?,1) && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= I] 8. f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [-50 + I >= 0 (?,1) && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] 9. f83(A,D,E,F,G,H,I) -> f93(A,D,E,F,G,H,I) [-50 + I >= 0 (?,1) && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] 10. f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 0 (?,1) && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && I >= 50] 11. f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 0 (?,1) && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && H >= 50] 12. f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 0 (?,1) && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && G >= 50] 13. f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [-50 + F >= 0 (?,1) && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] 14. f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 0 (?,1) && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 50] 15. f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 0 (?,1) && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 50] 16. f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= 50] (?,1) Signature: {(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)} Flow Graph: [0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8} ,11->{7},12->{6},13->{5},14->{4},15->{3},16->{2}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= D] f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= E] f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= F] f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= G] f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= H] f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= I] f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f83(A,D,E,F,G,H,I) -> f93(A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && I >= 50] f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && H >= 50] f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && G >= 50] f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 50] f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 50] f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= 50] Signature: {(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)} Rule Graph: [0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{},10->{8} ,11->{7},12->{6},13->{5},14->{4},15->{3},16->{2}] + Applied Processor: AddSinks + Details: () * Step 5: Unfold WORST_CASE(?,O(1)) + Considered Problem: Rules: f0(A,D,E,F,G,H,I) -> f17(0,0,E,F,G,H,I) True f17(A,D,E,F,G,H,I) -> f17(A,1 + D,E,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= D] f27(A,D,E,F,G,H,I) -> f27(A,D,1 + E,F,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= E] f37(A,D,E,F,G,H,I) -> f37(A,D,E,1 + F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= F] f45(A,D,E,F,G,H,I) -> f45(1 + A,D,E,F,G,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f55(A,D,E,F,G,H,I) -> f55(A,D,E,F,1 + G,H,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= G] f65(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,1 + H,I) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= H] f75(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,1 + I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= I] f83(A,D,E,F,G,H,I) -> f83(1 + A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f83(A,D,E,F,G,H,I) -> f93(A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] f75(A,D,E,F,G,H,I) -> f83(0,D,E,F,G,H,I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && I >= 50] f65(A,D,E,F,G,H,I) -> f75(A,D,E,F,G,H,0) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && H >= 50] f55(A,D,E,F,G,H,I) -> f65(A,D,E,F,G,0,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && G >= 50] f45(A,D,E,F,G,H,I) -> f55(A,D,E,F,0,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] f37(A,D,E,F,G,H,I) -> f45(0,D,E,F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 50] f27(A,D,E,F,G,H,I) -> f37(A,D,E,0,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 50] f17(A,D,E,F,G,H,I) -> f27(A,D,0,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= 50] f93(A,D,E,F,G,H,I) -> exitus616(A,D,E,F,G,H,I) True Signature: {(exitus616,7);(f0,9);(f17,9);(f27,9);(f37,9);(f45,9);(f55,9);(f65,9);(f75,9);(f83,9);(f93,9)} Rule Graph: [0->{1},1->{1,16},2->{2,15},3->{3,14},4->{4,13},5->{5,12},6->{6,11},7->{7,10},8->{8,9},9->{17},10->{8} ,11->{7},12->{6},13->{5},14->{4},15->{3},16->{2}] + Applied Processor: Unfold + Details: () * Step 6: Decompose WORST_CASE(?,O(1)) + Considered Problem: Rules: f0.0(A,D,E,F,G,H,I) -> f17.1(0,0,E,F,G,H,I) True f17.1(A,D,E,F,G,H,I) -> f17.1(A,1 + D,E,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= D] f17.1(A,D,E,F,G,H,I) -> f17.16(A,1 + D,E,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= D] f27.2(A,D,E,F,G,H,I) -> f27.2(A,D,1 + E,F,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= E] f27.2(A,D,E,F,G,H,I) -> f27.15(A,D,1 + E,F,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= E] f37.3(A,D,E,F,G,H,I) -> f37.3(A,D,E,1 + F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= F] f37.3(A,D,E,F,G,H,I) -> f37.14(A,D,E,1 + F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= F] f45.4(A,D,E,F,G,H,I) -> f45.4(1 + A,D,E,F,G,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f45.4(A,D,E,F,G,H,I) -> f45.13(1 + A,D,E,F,G,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f55.5(A,D,E,F,G,H,I) -> f55.5(A,D,E,F,1 + G,H,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= G] f55.5(A,D,E,F,G,H,I) -> f55.12(A,D,E,F,1 + G,H,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= G] f65.6(A,D,E,F,G,H,I) -> f65.6(A,D,E,F,G,1 + H,I) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= H] f65.6(A,D,E,F,G,H,I) -> f65.11(A,D,E,F,G,1 + H,I) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= H] f75.7(A,D,E,F,G,H,I) -> f75.7(A,D,E,F,G,H,1 + I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= I] f75.7(A,D,E,F,G,H,I) -> f75.10(A,D,E,F,G,H,1 + I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= I] f83.8(A,D,E,F,G,H,I) -> f83.8(1 + A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f83.8(A,D,E,F,G,H,I) -> f83.9(1 + A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f83.9(A,D,E,F,G,H,I) -> f93.17(A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] f75.10(A,D,E,F,G,H,I) -> f83.8(0,D,E,F,G,H,I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && I >= 50] f65.11(A,D,E,F,G,H,I) -> f75.7(A,D,E,F,G,H,0) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && H >= 50] f55.12(A,D,E,F,G,H,I) -> f65.6(A,D,E,F,G,0,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && G >= 50] f45.13(A,D,E,F,G,H,I) -> f55.5(A,D,E,F,0,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] f37.14(A,D,E,F,G,H,I) -> f45.4(0,D,E,F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 50] f27.15(A,D,E,F,G,H,I) -> f37.3(A,D,E,0,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 50] f17.16(A,D,E,F,G,H,I) -> f27.2(A,D,0,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= 50] f93.17(A,D,E,F,G,H,I) -> exitus616.18(A,D,E,F,G,H,I) True Signature: {(exitus616.18,7) ;(f0.0,7) ;(f17.1,7) ;(f17.16,7) ;(f27.15,7) ;(f27.2,7) ;(f37.14,7) ;(f37.3,7) ;(f45.13,7) ;(f45.4,7) ;(f55.12,7) ;(f55.5,7) ;(f65.11,7) ;(f65.6,7) ;(f75.10,7) ;(f75.7,7) ;(f83.8,7) ;(f83.9,7) ;(f93.17,7)} Rule Graph: [0->{1,2},1->{1,2},2->{24},3->{3,4},4->{23},5->{5,6},6->{22},7->{7,8},8->{21},9->{9,10},10->{20},11->{11 ,12},12->{19},13->{13,14},14->{18},15->{15,16},16->{17},17->{25},18->{15,16},19->{13,14},20->{11,12},21->{9 ,10},22->{7,8},23->{5,6},24->{3,4},25->{}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25] | +- p:[1] c: [1] | +- p:[3] c: [3] | +- p:[5] c: [5] | +- p:[7] c: [7] | +- p:[9] c: [9] | +- p:[11] c: [11] | +- p:[13] c: [13] | `- p:[15] c: [15] * Step 7: AbstractSize WORST_CASE(?,O(1)) + Considered Problem: (Rules: f0.0(A,D,E,F,G,H,I) -> f17.1(0,0,E,F,G,H,I) True f17.1(A,D,E,F,G,H,I) -> f17.1(A,1 + D,E,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= D] f17.1(A,D,E,F,G,H,I) -> f17.16(A,1 + D,E,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= D] f27.2(A,D,E,F,G,H,I) -> f27.2(A,D,1 + E,F,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= E] f27.2(A,D,E,F,G,H,I) -> f27.15(A,D,1 + E,F,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= E] f37.3(A,D,E,F,G,H,I) -> f37.3(A,D,E,1 + F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= F] f37.3(A,D,E,F,G,H,I) -> f37.14(A,D,E,1 + F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && 49 >= F] f45.4(A,D,E,F,G,H,I) -> f45.4(1 + A,D,E,F,G,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f45.4(A,D,E,F,G,H,I) -> f45.13(1 + A,D,E,F,G,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f55.5(A,D,E,F,G,H,I) -> f55.5(A,D,E,F,1 + G,H,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= G] f55.5(A,D,E,F,G,H,I) -> f55.12(A,D,E,F,1 + G,H,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= G] f65.6(A,D,E,F,G,H,I) -> f65.6(A,D,E,F,G,1 + H,I) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= H] f65.6(A,D,E,F,G,H,I) -> f65.11(A,D,E,F,G,1 + H,I) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= H] f75.7(A,D,E,F,G,H,I) -> f75.7(A,D,E,F,G,H,1 + I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= I] f75.7(A,D,E,F,G,H,I) -> f75.10(A,D,E,F,G,H,1 + I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && 49 >= I] f83.8(A,D,E,F,G,H,I) -> f83.8(1 + A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f83.8(A,D,E,F,G,H,I) -> f83.9(1 + A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && 49 >= A] f83.9(A,D,E,F,G,H,I) -> f93.17(A,D,E,F,G,H,I) [-50 + I >= 0 && -100 + H + I >= 0 && -100 + G + I >= 0 && -100 + F + I >= 0 && -100 + E + I >= 0 && -100 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] f75.10(A,D,E,F,G,H,I) -> f83.8(0,D,E,F,G,H,I) [I >= 0 && -50 + H + I >= 0 && -50 + G + I >= 0 && -50 + F + I >= 0 && -50 + E + I >= 0 && -50 + D + I >= 0 && -50 + A + I >= 0 && -50 + H >= 0 && -100 + G + H >= 0 && -100 + F + H >= 0 && -100 + E + H >= 0 && -100 + D + H >= 0 && -100 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && I >= 50] f65.11(A,D,E,F,G,H,I) -> f75.7(A,D,E,F,G,H,0) [H >= 0 && -50 + G + H >= 0 && -50 + F + H >= 0 && -50 + E + H >= 0 && -50 + D + H >= 0 && -50 + A + H >= 0 && -50 + G >= 0 && -100 + F + G >= 0 && -100 + E + G >= 0 && -100 + D + G >= 0 && -100 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && H >= 50] f55.12(A,D,E,F,G,H,I) -> f65.6(A,D,E,F,G,0,I) [G >= 0 && -50 + F + G >= 0 && -50 + E + G >= 0 && -50 + D + G >= 0 && -50 + A + G >= 0 && -50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -100 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -100 + A + E >= 0 && -50 + D >= 0 && -100 + A + D >= 0 && -50 + A >= 0 && G >= 50] f45.13(A,D,E,F,G,H,I) -> f55.5(A,D,E,F,0,H,I) [-50 + F >= 0 && -100 + E + F >= 0 && -100 + D + F >= 0 && -50 + A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && A >= 0 && A >= 50] f37.14(A,D,E,F,G,H,I) -> f45.4(0,D,E,F,G,H,I) [F >= 0 && -50 + E + F >= 0 && -50 + D + F >= 0 && A + F >= 0 && -1*A + F >= 0 && -50 + E >= 0 && -100 + D + E >= 0 && -50 + A + E >= 0 && -50 + -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && F >= 50] f27.15(A,D,E,F,G,H,I) -> f37.3(A,D,E,0,G,H,I) [E >= 0 && -50 + D + E >= 0 && A + E >= 0 && -1*A + E >= 0 && -50 + D >= 0 && -50 + A + D >= 0 && -50 + -1*A + D >= 0 && -1*A >= 0 && A >= 0 && E >= 50] f17.16(A,D,E,F,G,H,I) -> f27.2(A,D,0,F,G,H,I) [D >= 0 && A + D >= 0 && -1*A + D >= 0 && -1*A >= 0 && A >= 0 && D >= 50] f93.17(A,D,E,F,G,H,I) -> exitus616.18(A,D,E,F,G,H,I) True Signature: {(exitus616.18,7) ;(f0.0,7) ;(f17.1,7) ;(f17.16,7) ;(f27.15,7) ;(f27.2,7) ;(f37.14,7) ;(f37.3,7) ;(f45.13,7) ;(f45.4,7) ;(f55.12,7) ;(f55.5,7) ;(f65.11,7) ;(f65.6,7) ;(f75.10,7) ;(f75.7,7) ;(f83.8,7) ;(f83.9,7) ;(f93.17,7)} Rule Graph: [0->{1,2},1->{1,2},2->{24},3->{3,4},4->{23},5->{5,6},6->{22},7->{7,8},8->{21},9->{9,10},10->{20},11->{11 ,12},12->{19},13->{13,14},14->{18},15->{15,16},16->{17},17->{25},18->{15,16},19->{13,14},20->{11,12},21->{9 ,10},22->{7,8},23->{5,6},24->{3,4},25->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25] | +- p:[1] c: [1] | +- p:[3] c: [3] | +- p:[5] c: [5] | +- p:[7] c: [7] | +- p:[9] c: [9] | +- p:[11] c: [11] | +- p:[13] c: [13] | `- p:[15] c: [15]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,D,E,F,G,H,I,0.0,0.1,0.2,0.3,0.4,0.5,0.6,0.7] f0.0 ~> f17.1 [A <= 0*K, D <= 0*K, E <= E, F <= F, G <= G, H <= H, I <= I] f17.1 ~> f17.1 [A <= A, D <= 50*K, E <= E, F <= F, G <= G, H <= H, I <= I] f17.1 ~> f17.16 [A <= A, D <= 50*K, E <= E, F <= F, G <= G, H <= H, I <= I] f27.2 ~> f27.2 [A <= A, D <= D, E <= 50*K, F <= F, G <= G, H <= H, I <= I] f27.2 ~> f27.15 [A <= A, D <= D, E <= 50*K, F <= F, G <= G, H <= H, I <= I] f37.3 ~> f37.3 [A <= A, D <= D, E <= E, F <= 50*K, G <= G, H <= H, I <= I] f37.3 ~> f37.14 [A <= A, D <= D, E <= E, F <= 50*K, G <= G, H <= H, I <= I] f45.4 ~> f45.4 [A <= 50*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] f45.4 ~> f45.13 [A <= 50*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] f55.5 ~> f55.5 [A <= A, D <= D, E <= E, F <= F, G <= 50*K, H <= H, I <= I] f55.5 ~> f55.12 [A <= A, D <= D, E <= E, F <= F, G <= 50*K, H <= H, I <= I] f65.6 ~> f65.6 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= 50*K, I <= I] f65.6 ~> f65.11 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= 50*K, I <= I] f75.7 ~> f75.7 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= H, I <= 50*K] f75.7 ~> f75.10 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= H, I <= 50*K] f83.8 ~> f83.8 [A <= 50*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] f83.8 ~> f83.9 [A <= 50*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] f83.9 ~> f93.17 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] f75.10 ~> f83.8 [A <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] f65.11 ~> f75.7 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= H, I <= 0*K] f55.12 ~> f65.6 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= I] f45.13 ~> f55.5 [A <= A, D <= D, E <= E, F <= F, G <= 0*K, H <= H, I <= I] f37.14 ~> f45.4 [A <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] f27.15 ~> f37.3 [A <= A, D <= D, E <= E, F <= 0*K, G <= G, H <= H, I <= I] f17.16 ~> f27.2 [A <= A, D <= D, E <= 0*K, F <= F, G <= G, H <= H, I <= I] f93.17 ~> exitus616.18 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] + Loop: [0.0 <= 49*K + D] f17.1 ~> f17.1 [A <= A, D <= 50*K, E <= E, F <= F, G <= G, H <= H, I <= I] + Loop: [0.1 <= 49*K + E] f27.2 ~> f27.2 [A <= A, D <= D, E <= 50*K, F <= F, G <= G, H <= H, I <= I] + Loop: [0.2 <= 49*K + F] f37.3 ~> f37.3 [A <= A, D <= D, E <= E, F <= 50*K, G <= G, H <= H, I <= I] + Loop: [0.3 <= 49*K + A] f45.4 ~> f45.4 [A <= 50*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] + Loop: [0.4 <= 49*K + G] f55.5 ~> f55.5 [A <= A, D <= D, E <= E, F <= F, G <= 50*K, H <= H, I <= I] + Loop: [0.5 <= 49*K + H] f65.6 ~> f65.6 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= 50*K, I <= I] + Loop: [0.6 <= 49*K + I] f75.7 ~> f75.7 [A <= A, D <= D, E <= E, F <= F, G <= G, H <= H, I <= 50*K] + Loop: [0.7 <= 49*K + A] f83.8 ~> f83.8 [A <= 50*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I] + Applied Processor: AbstractFlow + Details: () * Step 9: Lare WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,D,E,F,G,H,I,0.0,0.1,0.2,0.3,0.4,0.5,0.6,0.7] f0.0 ~> f17.1 [K ~=> A,K ~=> D] f17.1 ~> f17.1 [K ~=> D] f17.1 ~> f17.16 [K ~=> D] f27.2 ~> f27.2 [K ~=> E] f27.2 ~> f27.15 [K ~=> E] f37.3 ~> f37.3 [K ~=> F] f37.3 ~> f37.14 [K ~=> F] f45.4 ~> f45.4 [K ~=> A] f45.4 ~> f45.13 [K ~=> A] f55.5 ~> f55.5 [K ~=> G] f55.5 ~> f55.12 [K ~=> G] f65.6 ~> f65.6 [K ~=> H] f65.6 ~> f65.11 [K ~=> H] f75.7 ~> f75.7 [K ~=> I] f75.7 ~> f75.10 [K ~=> I] f83.8 ~> f83.8 [K ~=> A] f83.8 ~> f83.9 [K ~=> A] f83.9 ~> f93.17 [] f75.10 ~> f83.8 [K ~=> A] f65.11 ~> f75.7 [K ~=> I] f55.12 ~> f65.6 [K ~=> H] f45.13 ~> f55.5 [K ~=> G] f37.14 ~> f45.4 [K ~=> A] f27.15 ~> f37.3 [K ~=> F] f17.16 ~> f27.2 [K ~=> E] f93.17 ~> exitus616.18 [] + Loop: [D ~+> 0.0,K ~*> 0.0] f17.1 ~> f17.1 [K ~=> D] + Loop: [E ~+> 0.1,K ~*> 0.1] f27.2 ~> f27.2 [K ~=> E] + Loop: [F ~+> 0.2,K ~*> 0.2] f37.3 ~> f37.3 [K ~=> F] + Loop: [A ~+> 0.3,K ~*> 0.3] f45.4 ~> f45.4 [K ~=> A] + Loop: [G ~+> 0.4,K ~*> 0.4] f55.5 ~> f55.5 [K ~=> G] + Loop: [H ~+> 0.5,K ~*> 0.5] f65.6 ~> f65.6 [K ~=> H] + Loop: [I ~+> 0.6,K ~*> 0.6] f75.7 ~> f75.7 [K ~=> I] + Loop: [A ~+> 0.7,K ~*> 0.7] f83.8 ~> f83.8 [K ~=> A] + Applied Processor: Lare + Details: f0.0 ~> exitus616.18 [K ~=> A ,K ~=> D ,K ~=> E ,K ~=> F ,K ~=> G ,K ~=> H ,K ~=> I ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> 0.4 ,K ~+> 0.5 ,K ~+> 0.6 ,K ~+> 0.7 ,K ~+> tick ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> 0.4 ,K ~*> 0.5 ,K ~*> 0.6 ,K ~*> 0.7 ,K ~*> tick] + f17.1> [K ~=> D,D ~+> 0.0,D ~+> tick,tick ~+> tick,K ~*> 0.0,K ~*> tick] + f27.2> [K ~=> E,E ~+> 0.1,E ~+> tick,tick ~+> tick,K ~*> 0.1,K ~*> tick] + f37.3> [K ~=> F,F ~+> 0.2,F ~+> tick,tick ~+> tick,K ~*> 0.2,K ~*> tick] + f45.4> [K ~=> A,A ~+> 0.3,A ~+> tick,tick ~+> tick,K ~*> 0.3,K ~*> tick] + f55.5> [K ~=> G,G ~+> 0.4,G ~+> tick,tick ~+> tick,K ~*> 0.4,K ~*> tick] + f65.6> [K ~=> H,H ~+> 0.5,H ~+> tick,tick ~+> tick,K ~*> 0.5,K ~*> tick] + f75.7> [K ~=> I,I ~+> 0.6,I ~+> tick,tick ~+> tick,K ~*> 0.6,K ~*> tick] + f83.8> [K ~=> A,A ~+> 0.7,A ~+> tick,tick ~+> tick,K ~*> 0.7,K ~*> tick] YES(?,O(1))