YES * Step 1: TrivialSCCs YES + 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 YES + 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: Looptree YES + 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: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] | +- 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] YES