YES * Step 1: TrivialSCCs YES + 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths YES + 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,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,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,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,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,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,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,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,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: Looptree YES + 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,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,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,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,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,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,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,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,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: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16] | +- p:[1] c: [1] | +- p:[2] c: [2] | +- p:[3] c: [3] | +- p:[4] c: [4] | +- p:[5] c: [5] | +- p:[6] c: [6] | +- p:[7] c: [7] | `- p:[8] c: [8] YES