MAYBE * Step 1: UnsatPaths MAYBE + 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: UnsatPaths + Details: We remove following edges from the transition graph: [(1,6),(4,0),(5,0),(12,14),(12,15)] * Step 2: FromIts MAYBE + 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,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: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f4(A,B,C,D,E,F) -> f14(A,B,C,D,E,F) [C + -1*E >= 0 && 0 >= A] f13(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [C + -1*E >= 0 && 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] f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] f2(A,B,C,D,E,F) -> f23(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,F) [1 + -1*E >= 0 && 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] f23(A,B,C,D,E,F) -> f4(A,B,C,D,E,1) [1 + -1*E >= 0 && 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] 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] 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] f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] f33(A,B,C,D,E,F) -> f6(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] 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] 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] 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] 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] 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] 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] 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] 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] f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f61(A,B,C,D,E,F) -> f63(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,F) [C + -1*E >= 0 && 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] f63(A,B,C,D,E,F) -> f71(A,B,C,1 + D,C,1) [C + -1*E >= 0 && 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] f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f71(A,B,C,D,E,F) -> f73(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,F) [C + -1*E >= 0 && 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] f73(A,B,C,D,E,F) -> f13(A,B,C,D,E,1) [C + -1*E >= 0 && 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)} Rule 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: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f4.0(A,B,C,D,E,F) -> f14.26(A,B,C,D,E,F) [C + -1*E >= 0 && 0 >= A] f13.1(A,B,C,D,E,F) -> f4.0(A,B,C,D,E,F) [C + -1*E >= 0 && 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] f13.1(A,B,C,D,E,F) -> f4.7(A,B,C,D,E,F) [C + -1*E >= 0 && 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] f2.2(A,B,C,D,E,F) -> f23.4(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] f2.2(A,B,C,D,E,F) -> f23.5(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] f2.3(A,B,C,D,E,F) -> f23.4(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] f2.3(A,B,C,D,E,F) -> f23.5(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] f23.4(A,B,C,D,E,F) -> f4.6(A,B,C,D,E,F) [1 + -1*E >= 0 && 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] f23.4(A,B,C,D,E,F) -> f4.7(A,B,C,D,E,F) [1 + -1*E >= 0 && 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] f23.5(A,B,C,D,E,F) -> f4.6(A,B,C,D,E,1) [1 + -1*E >= 0 && 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] f23.5(A,B,C,D,E,F) -> f4.7(A,B,C,D,E,1) [1 + -1*E >= 0 && 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] f4.6(A,B,C,D,E,F) -> f33.8(-1 + A,B,H,J,C,F) [C + -1*E >= 0 && H >= C && 0 >= B && A >= 1] f4.6(A,B,C,D,E,F) -> f33.9(-1 + A,B,H,J,C,F) [C + -1*E >= 0 && H >= C && 0 >= B && A >= 1] f4.7(A,B,C,D,E,F) -> f33.8(-1 + A,B,H,J,C,0) [C + -1*E >= 0 && H >= C && B >= 1 && A >= 1] f4.7(A,B,C,D,E,F) -> f33.9(-1 + A,B,H,J,C,0) [C + -1*E >= 0 && H >= C && B >= 1 && A >= 1] f33.8(A,B,C,D,E,F) -> f6.10(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] f33.8(A,B,C,D,E,F) -> f6.11(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] f33.8(A,B,C,D,E,F) -> f6.14(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] f33.8(A,B,C,D,E,F) -> f6.15(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] f33.9(A,B,C,D,E,F) -> f6.10(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] f33.9(A,B,C,D,E,F) -> f6.11(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] f33.9(A,B,C,D,E,F) -> f6.14(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] f33.9(A,B,C,D,E,F) -> f6.15(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] f6.10(A,B,C,D,E,F) -> f43.12(A,B,H,J,C,F) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && 0 >= B] f6.10(A,B,C,D,E,F) -> f43.13(A,B,H,J,C,F) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && 0 >= B] f6.11(A,B,C,D,E,F) -> f43.12(A,B,H,J,C,0) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && B >= 1] f6.11(A,B,C,D,E,F) -> f43.13(A,B,H,J,C,0) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && B >= 1] f43.12(A,B,C,D,E,F) -> f6.10(A,B,C,D,C,F) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C = E] f43.12(A,B,C,D,E,F) -> f6.11(A,B,C,D,C,F) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C = E] f43.13(A,B,C,D,E,F) -> f6.10(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] f43.13(A,B,C,D,E,F) -> f6.11(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] f43.13(A,B,C,D,E,F) -> f6.14(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] f43.13(A,B,C,D,E,F) -> f6.15(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] f6.14(A,B,C,D,E,F) -> f53.16(A,B,H,J,-1 + C,F) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && 0 >= B] f6.14(A,B,C,D,E,F) -> f53.17(A,B,H,J,-1 + C,F) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && 0 >= B] f6.15(A,B,C,D,E,F) -> f53.16(A,B,H,J,-1 + C,0) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && B >= 1] f6.15(A,B,C,D,E,F) -> f53.17(A,B,H,J,-1 + C,0) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && B >= 1] f53.16(A,B,C,D,E,F) -> f61.18(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] f53.16(A,B,C,D,E,F) -> f61.19(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] f53.17(A,B,C,D,E,F) -> f61.18(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] f53.17(A,B,C,D,E,F) -> f61.19(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] f61.18(A,B,C,D,E,F) -> f63.20(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f61.18(A,B,C,D,E,F) -> f63.21(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f61.19(A,B,C,D,E,F) -> f63.20(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f61.19(A,B,C,D,E,F) -> f63.21(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f63.20(A,B,C,D,E,F) -> f71.22(A,B,C,1 + D,C,F) [C + -1*E >= 0 && 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] f63.20(A,B,C,D,E,F) -> f71.23(A,B,C,1 + D,C,F) [C + -1*E >= 0 && 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] f63.21(A,B,C,D,E,F) -> f71.22(A,B,C,1 + D,C,1) [C + -1*E >= 0 && 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] f63.21(A,B,C,D,E,F) -> f71.23(A,B,C,1 + D,C,1) [C + -1*E >= 0 && 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] f71.22(A,B,C,D,E,F) -> f73.24(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f71.22(A,B,C,D,E,F) -> f73.25(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f71.23(A,B,C,D,E,F) -> f73.24(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f71.23(A,B,C,D,E,F) -> f73.25(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f73.24(A,B,C,D,E,F) -> f13.1(A,B,C,D,E,F) [C + -1*E >= 0 && 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] f73.25(A,B,C,D,E,F) -> f13.1(A,B,C,D,E,1) [C + -1*E >= 0 && 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.1,6) ;(f14.26,6) ;(f2.2,6) ;(f2.3,6) ;(f23.4,6) ;(f23.5,6) ;(f33.8,6) ;(f33.9,6) ;(f4.0,6) ;(f4.6,6) ;(f4.7,6) ;(f43.12,6) ;(f43.13,6) ;(f53.16,6) ;(f53.17,6) ;(f6.10,6) ;(f6.11,6) ;(f6.14,6) ;(f6.15,6) ;(f61.18,6) ;(f61.19,6) ;(f63.20,6) ;(f63.21,6) ;(f71.22,6) ;(f71.23,6) ;(f73.24,6) ;(f73.25,6)} Rule Graph: [0->{},1->{0},2->{13,14},3->{7,8},4->{9,10},5->{7,8},6->{9,10},7->{11,12},8->{13,14},9->{11,12},10->{13 ,14},11->{15,16,17,18},12->{19,20,21,22},13->{15,16,17,18},14->{19,20,21,22},15->{23,24},16->{25,26},17->{33 ,34},18->{35,36},19->{23,24},20->{25,26},21->{33,34},22->{35,36},23->{27,28},24->{29,30,31,32},25->{27,28} ,26->{29,30,31,32},27->{23,24},28->{25,26},29->{23,24},30->{25,26},31->{33,34},32->{35,36},33->{37,38} ,34->{39,40},35->{37,38},36->{39,40},37->{41,42},38->{43,44},39->{41,42},40->{43,44},41->{45,46},42->{47,48} ,43->{45,46},44->{47,48},45->{49,50},46->{51,52},47->{49,50},48->{51,52},49->{53},50->{54},51->{53},52->{54} ,53->{1,2},54->{1,2}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f4.0(A,B,C,D,E,F) -> f14.26(A,B,C,D,E,F) [C + -1*E >= 0 && 0 >= A] f13.1(A,B,C,D,E,F) -> f4.0(A,B,C,D,E,F) [C + -1*E >= 0 && 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] f13.1(A,B,C,D,E,F) -> f4.7(A,B,C,D,E,F) [C + -1*E >= 0 && 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] f2.2(A,B,C,D,E,F) -> f23.4(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] f2.2(A,B,C,D,E,F) -> f23.5(G,I,H,J,1,F) [G >= 1 && H >= 1 && 0 >= I] f2.3(A,B,C,D,E,F) -> f23.4(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] f2.3(A,B,C,D,E,F) -> f23.5(G,I,H,J,1,0) [G >= 1 && H >= 1 && I >= 1] f23.4(A,B,C,D,E,F) -> f4.6(A,B,C,D,E,F) [1 + -1*E >= 0 && 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] f23.4(A,B,C,D,E,F) -> f4.7(A,B,C,D,E,F) [1 + -1*E >= 0 && 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] f23.5(A,B,C,D,E,F) -> f4.6(A,B,C,D,E,1) [1 + -1*E >= 0 && 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] f23.5(A,B,C,D,E,F) -> f4.7(A,B,C,D,E,1) [1 + -1*E >= 0 && 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] f4.6(A,B,C,D,E,F) -> f33.8(-1 + A,B,H,J,C,F) [C + -1*E >= 0 && H >= C && 0 >= B && A >= 1] f4.6(A,B,C,D,E,F) -> f33.9(-1 + A,B,H,J,C,F) [C + -1*E >= 0 && H >= C && 0 >= B && A >= 1] f4.7(A,B,C,D,E,F) -> f33.8(-1 + A,B,H,J,C,0) [C + -1*E >= 0 && H >= C && B >= 1 && A >= 1] f4.7(A,B,C,D,E,F) -> f33.9(-1 + A,B,H,J,C,0) [C + -1*E >= 0 && H >= C && B >= 1 && A >= 1] f33.8(A,B,C,D,E,F) -> f6.10(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] f33.8(A,B,C,D,E,F) -> f6.11(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] f33.8(A,B,C,D,E,F) -> f6.14(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] f33.8(A,B,C,D,E,F) -> f6.15(A,B,C,D,E,F) [C + -1*E >= 0 && A >= 0 && E >= C] f33.9(A,B,C,D,E,F) -> f6.10(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] f33.9(A,B,C,D,E,F) -> f6.11(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] f33.9(A,B,C,D,E,F) -> f6.14(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] f33.9(A,B,C,D,E,F) -> f6.15(A,B,C,D,E,1) [C + -1*E >= 0 && A >= 0 && C >= 1 + E] f6.10(A,B,C,D,E,F) -> f43.12(A,B,H,J,C,F) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && 0 >= B] f6.10(A,B,C,D,E,F) -> f43.13(A,B,H,J,C,F) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && 0 >= B] f6.11(A,B,C,D,E,F) -> f43.12(A,B,H,J,C,0) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && B >= 1] f6.11(A,B,C,D,E,F) -> f43.13(A,B,H,J,C,0) [C + -1*E >= 0 && A >= 0 && H >= C && 0 >= C && B >= 1] f43.12(A,B,C,D,E,F) -> f6.10(A,B,C,D,C,F) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C = E] f43.12(A,B,C,D,E,F) -> f6.11(A,B,C,D,C,F) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C = E] f43.13(A,B,C,D,E,F) -> f6.10(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] f43.13(A,B,C,D,E,F) -> f6.11(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] f43.13(A,B,C,D,E,F) -> f6.14(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] f43.13(A,B,C,D,E,F) -> f6.15(A,B,C,D,E,1) [-1*E >= 0 && C + -1*E >= 0 && A + -1*E >= 0 && A >= 0 && C >= 1 + E] f6.14(A,B,C,D,E,F) -> f53.16(A,B,H,J,-1 + C,F) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && 0 >= B] f6.14(A,B,C,D,E,F) -> f53.17(A,B,H,J,-1 + C,F) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && 0 >= B] f6.15(A,B,C,D,E,F) -> f53.16(A,B,H,J,-1 + C,0) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && B >= 1] f6.15(A,B,C,D,E,F) -> f53.17(A,B,H,J,-1 + C,0) [C + -1*E >= 0 && A >= 0 && 1 + H >= C && C >= 1 && B >= 1] f53.16(A,B,C,D,E,F) -> f61.18(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] f53.16(A,B,C,D,E,F) -> f61.19(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] f53.17(A,B,C,D,E,F) -> f61.18(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] f53.17(A,B,C,D,E,F) -> f61.19(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] f61.18(A,B,C,D,E,F) -> f63.20(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f61.18(A,B,C,D,E,F) -> f63.21(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f61.19(A,B,C,D,E,F) -> f63.20(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f61.19(A,B,C,D,E,F) -> f63.21(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f63.20(A,B,C,D,E,F) -> f71.22(A,B,C,1 + D,C,F) [C + -1*E >= 0 && 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] f63.20(A,B,C,D,E,F) -> f71.23(A,B,C,1 + D,C,F) [C + -1*E >= 0 && 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] f63.21(A,B,C,D,E,F) -> f71.22(A,B,C,1 + D,C,1) [C + -1*E >= 0 && 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] f63.21(A,B,C,D,E,F) -> f71.23(A,B,C,1 + D,C,1) [C + -1*E >= 0 && 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] f71.22(A,B,C,D,E,F) -> f73.24(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f71.22(A,B,C,D,E,F) -> f73.25(A,B,H,J,E,F) [C + -1*E >= 0 && 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] f71.23(A,B,C,D,E,F) -> f73.24(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f71.23(A,B,C,D,E,F) -> f73.25(A,B,H,J,E,0) [C + -1*E >= 0 && 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] f73.24(A,B,C,D,E,F) -> f13.1(A,B,C,D,E,F) [C + -1*E >= 0 && 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] f73.25(A,B,C,D,E,F) -> f13.1(A,B,C,D,E,1) [C + -1*E >= 0 && 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] f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f14.26(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True Signature: {(exitus616,6) ;(f13.1,6) ;(f14.26,6) ;(f2.2,6) ;(f2.3,6) ;(f23.4,6) ;(f23.5,6) ;(f33.8,6) ;(f33.9,6) ;(f4.0,6) ;(f4.6,6) ;(f4.7,6) ;(f43.12,6) ;(f43.13,6) ;(f53.16,6) ;(f53.17,6) ;(f6.10,6) ;(f6.11,6) ;(f6.14,6) ;(f6.15,6) ;(f61.18,6) ;(f61.19,6) ;(f63.20,6) ;(f63.21,6) ;(f71.22,6) ;(f71.23,6) ;(f73.24,6) ;(f73.25,6)} Rule Graph: [0->{55,56,57,58,59,60,61,62,63,64,65,66},1->{0},2->{13,14},3->{7,8},4->{9,10},5->{7,8},6->{9,10},7->{11 ,12},8->{13,14},9->{11,12},10->{13,14},11->{15,16,17,18},12->{19,20,21,22},13->{15,16,17,18},14->{19,20,21 ,22},15->{23,24},16->{25,26},17->{33,34},18->{35,36},19->{23,24},20->{25,26},21->{33,34},22->{35,36},23->{27 ,28},24->{29,30,31,32},25->{27,28},26->{29,30,31,32},27->{23,24},28->{25,26},29->{23,24},30->{25,26},31->{33 ,34},32->{35,36},33->{37,38},34->{39,40},35->{37,38},36->{39,40},37->{41,42},38->{43,44},39->{41,42},40->{43 ,44},41->{45,46},42->{47,48},43->{45,46},44->{47,48},45->{49,50},46->{51,52},47->{49,50},48->{51,52} ,49->{53},50->{54},51->{53},52->{54},53->{1,2},54->{1,2}] + 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,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66] | `- p:[2,53,49,45,41,37,33,17,13,21,14,31,24,15,19,27,23,29,26,16,20,28,25,30,35,18,22,32,39,34,36,43,38,40,47,42,44,51,46,48,54,50,52] c: [2,13,14,15,16,17,18,19,20,21,22,24,26,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47,48,49,50,51,52,53,54] | `- p:[23,27,25,28] c: [] MAYBE