NO * Step 1: TrivialSCCs NO + Considered Problem: Rules: 0. f4(A,B,C,D,E,F) -> f14(A,B,C,D,E,F) [C + -1*E >= 0 && 0 >= A] (?,1) 1. f13(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 2. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] (1,1) 3. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] (1,1) 4. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [1 + -1*E >= 0 (?,1) && C + -1*E >= 0 && A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + A + E >= 0 && -1 + C >= 0 && -2 + A + C >= 0 && -1 + A >= 0 && E >= C] 5. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,1) [1 + -1*E >= 0 (?,1) && C + -1*E >= 0 && A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + A + E >= 0 && -1 + C >= 0 && -2 + A + C >= 0 && -1 + A >= 0 && C >= 1 + E] 6. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,F) [C + -1*E >= 0 && H >= C && 0 >= B && A >= 1] (?,1) 7. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,0) [C + -1*E >= 0 && H >= C && B >= 1 && A >= 1] (?,1) 8. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] (?,1) 9. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] (?,1) 10. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,F) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && 0 >= B] (?,1) 11. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,0) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && B >= 1] (?,1) 12. f43(A,B,C,D,E,F) -> f6(A,B,C,D,C,F) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C = E] (?,1) 13. f43(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] (?,1) 14. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,F) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && 0 >= B] (?,1) 15. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,0) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && B >= 1] (?,1) 16. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,F) [C + -1*E >= 0 && E >= 0 && C + E >= 0 && A + E >= 0 && C >= 0 && A + C >= 0 && A >= 0 && E >= C] (?,1) 17. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,1) [C + -1*E >= 0 && E >= 0 && C + E >= 0 && A + E >= 0 && C >= 0 && A + C >= 0 && A >= 0 && C >= 1 + E] (?,1) 18. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= B && H >= E] 19. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,0) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= 1 && H >= E] 20. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= C] 21. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,1) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + E] 22. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= B && H >= E] 23. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,0) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= 1 && H >= E] 24. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= C] 25. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,1) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + E] Signature: {(f13,6);(f14,6);(f2,6);(f23,6);(f33,6);(f4,6);(f43,6);(f53,6);(f6,6);(f61,6);(f63,6);(f71,6);(f73,6)} Flow Graph: [0->{},1->{0,6,7},2->{4,5},3->{4,5},4->{0,6,7},5->{0,6,7},6->{8,9},7->{8,9},8->{10,11,14,15},9->{10,11,14 ,15},10->{12,13},11->{12,13},12->{10,11,14,15},13->{10,11,14,15},14->{16,17},15->{16,17},16->{18,19},17->{18 ,19},18->{20,21},19->{20,21},20->{22,23},21->{22,23},22->{24,25},23->{24,25},24->{1},25->{1}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths NO + Considered Problem: Rules: 0. f4(A,B,C,D,E,F) -> f14(A,B,C,D,E,F) [C + -1*E >= 0 && 0 >= A] (1,1) 1. f13(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 2. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] (1,1) 3. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] (1,1) 4. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [1 + -1*E >= 0 (1,1) && C + -1*E >= 0 && A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + A + E >= 0 && -1 + C >= 0 && -2 + A + C >= 0 && -1 + A >= 0 && E >= C] 5. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,1) [1 + -1*E >= 0 (1,1) && C + -1*E >= 0 && A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + A + E >= 0 && -1 + C >= 0 && -2 + A + C >= 0 && -1 + A >= 0 && C >= 1 + E] 6. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,F) [C + -1*E >= 0 && H >= C && 0 >= B && A >= 1] (?,1) 7. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,0) [C + -1*E >= 0 && H >= C && B >= 1 && A >= 1] (?,1) 8. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] (?,1) 9. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] (?,1) 10. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,F) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && 0 >= B] (?,1) 11. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,0) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && B >= 1] (?,1) 12. f43(A,B,C,D,E,F) -> f6(A,B,C,D,C,F) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C = E] (?,1) 13. f43(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] (?,1) 14. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,F) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && 0 >= B] (?,1) 15. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,0) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && B >= 1] (?,1) 16. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,F) [C + -1*E >= 0 && E >= 0 && C + E >= 0 && A + E >= 0 && C >= 0 && A + C >= 0 && A >= 0 && E >= C] (?,1) 17. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,1) [C + -1*E >= 0 && E >= 0 && C + E >= 0 && A + E >= 0 && C >= 0 && A + C >= 0 && A >= 0 && C >= 1 + E] (?,1) 18. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= B && H >= E] 19. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,0) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= 1 && H >= E] 20. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= C] 21. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,1) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + E] 22. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= B && H >= E] 23. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,0) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= 1 && H >= E] 24. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= C] 25. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,1) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + E] Signature: {(f13,6);(f14,6);(f2,6);(f23,6);(f33,6);(f4,6);(f43,6);(f53,6);(f6,6);(f61,6);(f63,6);(f71,6);(f73,6)} Flow Graph: [0->{},1->{0,6,7},2->{4,5},3->{4,5},4->{0,6,7},5->{0,6,7},6->{8,9},7->{8,9},8->{10,11,14,15},9->{10,11,14 ,15},10->{12,13},11->{12,13},12->{10,11,14,15},13->{10,11,14,15},14->{16,17},15->{16,17},16->{18,19},17->{18 ,19},18->{20,21},19->{20,21},20->{22,23},21->{22,23},22->{24,25},23->{24,25},24->{1},25->{1}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,6),(4,0),(5,0),(12,14),(12,15)] * Step 3: Looptree NO + Considered Problem: Rules: 0. f4(A,B,C,D,E,F) -> f14(A,B,C,D,E,F) [C + -1*E >= 0 && 0 >= A] (1,1) 1. f13(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0] 2. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] (1,1) 3. f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] (1,1) 4. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [1 + -1*E >= 0 (1,1) && C + -1*E >= 0 && A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + A + E >= 0 && -1 + C >= 0 && -2 + A + C >= 0 && -1 + A >= 0 && E >= C] 5. f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,1) [1 + -1*E >= 0 (1,1) && C + -1*E >= 0 && A + -1*E >= 0 && -1 + E >= 0 && -2 + C + E >= 0 && -2 + A + E >= 0 && -1 + C >= 0 && -2 + A + C >= 0 && -1 + A >= 0 && C >= 1 + E] 6. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,F) [C + -1*E >= 0 && H >= C && 0 >= B && A >= 1] (?,1) 7. f4(A,B,C,D,E,F) -> f33(-1 + A,B,H,J,C,0) [C + -1*E >= 0 && H >= C && B >= 1 && A >= 1] (?,1) 8. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] (?,1) 9. f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] (?,1) 10. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,F) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && 0 >= B] (?,1) 11. f6(A,B,C,D,E,F) -> f43(A,B,H,J,C,0) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && B >= 1] (?,1) 12. f43(A,B,C,D,E,F) -> f6(A,B,C,D,C,F) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C = E] (?,1) 13. f43(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] (?,1) 14. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,F) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && 0 >= B] (?,1) 15. f6(A,B,C,D,E,F) -> f53(A,B,H,J,-1 + C,0) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && B >= 1] (?,1) 16. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,F) [C + -1*E >= 0 && E >= 0 && C + E >= 0 && A + E >= 0 && C >= 0 && A + C >= 0 && A >= 0 && E >= C] (?,1) 17. f53(A,B,C,D,E,F) -> f61(A,A,C,D,C,1) [C + -1*E >= 0 && E >= 0 && C + E >= 0 && A + E >= 0 && C >= 0 && A + C >= 0 && A >= 0 && C >= 1 + E] (?,1) 18. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= B && H >= E] 19. f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,0) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= 1 && H >= E] 20. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= C] 21. f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,1) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + E] 22. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && 0 >= B && H >= E] 23. f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,0) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && -1*C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && B >= 1 && H >= E] 24. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,F) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && E >= C] 25. f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,1) [C + -1*E >= 0 (?,1) && E >= 0 && C + E >= 0 && B + E >= 0 && A + E >= 0 && C >= 0 && B + C >= 0 && A + C >= 0 && A + -1*B >= 0 && B >= 0 && A + B >= 0 && -1*A + B >= 0 && A >= 0 && C >= 1 + E] Signature: {(f13,6);(f14,6);(f2,6);(f23,6);(f33,6);(f4,6);(f43,6);(f53,6);(f6,6);(f61,6);(f63,6);(f71,6);(f73,6)} Flow Graph: [0->{},1->{0,7},2->{4,5},3->{4,5},4->{6,7},5->{6,7},6->{8,9},7->{8,9},8->{10,11,14,15},9->{10,11,14,15} ,10->{12,13},11->{12,13},12->{10,11},13->{10,11,14,15},14->{16,17},15->{16,17},16->{18,19},17->{18,19} ,18->{20,21},19->{20,21},20->{22,23},21->{22,23},22->{24,25},23->{24,25},24->{1},25->{1}] + 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,17,18,19,20,21,22,23,24,25] | `- p:[1,24,22,20,18,16,14,8,7,9,13,10,12,11,15,17,19,21,23,25] c: [25] | `- p:[1,24,22,20,18,16,14,8,7,9,13,10,12,11,15,17,19,21,23] c: [24] | `- p:[10,12,11,13] c: [13] | `- p:[10,12,11] c: [] NO