MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f2(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= B] (?,1) 1. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] (?,1) 2. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] (?,1) 3. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f15(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= C] (?,1) 4. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && D >= A] (?,1) 5. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f24(A,B,C,D,E,V,W,V + W,0,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] (?,1) 6. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f15(A,B,C,1 + D,E,V,W,V + W,X,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] (?,1) 7. f15(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f15(A,B,C,1 + D,E,V,W,V + W,X,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] (?,1) 8. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f75(A,B,C,C,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && C = D] (?,1) 9. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f28(A,B,C,D,1 + E,F,G,H,I,E,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] (?,1) 10. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f28(A,B,C,D,1 + E,F,G,H,I,E,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] (?,1) 11. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f32(A,B,C,D,E,F,G,H,I,J,V,W,M,N,O,P,Q,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 29 >= J] 12. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f32(A,B,C,D,E,F,G,H,I,J,V,W,M,N,O,P,Q,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] 13. f28(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f32(A,B,C,D,E,F,G,H,I,30,V,W,M,N,O,P,Q,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] 14. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f42(A,B,C,D,E,F,G,H,I,J,V + -1*W + X,L,Z,Z,1,1,0,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] 15. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f42(A,B,C,D,E,F,G,H,I,J,V + -1*W + X,L,M,-1*Z,1,1,0,Z,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] 16. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] 17. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f68(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,P*V,O*W,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C] 18. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f60(A,B,C,D,E,F,G,H,I,J,-1*O*W + V,X,M,N,Z,Y,H1,R,B1*P,O*W,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && 0 >= 1 + A1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] 19. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f60(A,B,C,D,E,F,G,H,I,J,-1*O*W + V,X,M,N,Z,Y,H1,R,B1*P,O*W,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && A1 >= 1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] 20. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,V,T,1 + U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && A >= U] 21. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f75(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] 22. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] 23. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] 24. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f75(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] 25. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f10(A,B,1 + C,C,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && C = D] (?,1) 26. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f42(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] 27. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 1 + A] (?,1) 28. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [B >= 1 + A] (?,1) 29. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (1,1) Signature: {(f1,21) ;(f10,21) ;(f15,21) ;(f2,21) ;(f24,21) ;(f28,21) ;(f32,21) ;(f42,21) ;(f60,21) ;(f68,21) ;(f75,21) ;(start,21)} Flow Graph: [0->{0,28},1->{4,5,6,7},2->{4,5,6,7},3->{4,5,6,7},4->{8,9,10},5->{8,9,10},6->{4,5,6,7},7->{4,5,6,7},8->{1 ,2,25},9->{11,12,13},10->{11,12,13},11->{14,15},12->{14,15},13->{14,15},14->{16,17,18,19},15->{16,17,18,19} ,16->{21,22,23,24},17->{21,22,23,24},18->{20,26},19->{20,26},20->{20,26},21->{1,2,25},22->{1,2,25},23->{1,2 ,25},24->{1,2,25},25->{3,27},26->{16,17,18,19},27->{},28->{3,27},29->{0,28}] + Applied Processor: ArgumentFilter [5,6,7,8,12,13,14,16,17,18,19] + Details: We remove following argument positions: [5,6,7,8,12,13,14,16,17,18,19]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f2(A,B,C,D,E,J,K,L,P,U) -> f2(A,1 + B,C,D,E,J,K,L,P,U) [A >= B] (?,1) 1. f75(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] (?,1) 2. f75(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] (?,1) 3. f10(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,D,0,J,K,L,P,U) [A >= C] (?,1) 4. f15(A,B,C,D,E,J,K,L,P,U) -> f24(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= A] (?,1) 5. f15(A,B,C,D,E,J,K,L,P,U) -> f24(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] (?,1) 6. f15(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] (?,1) 7. f15(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] (?,1) 8. f24(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] (?,1) 9. f24(A,B,C,D,E,J,K,L,P,U) -> f28(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] (?,1) 10. f24(A,B,C,D,E,J,K,L,P,U) -> f28(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] (?,1) 11. f28(A,B,C,D,E,J,K,L,P,U) -> f32(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 29 >= J] 12. f28(A,B,C,D,E,J,K,L,P,U) -> f32(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] 13. f28(A,B,C,D,E,J,K,L,P,U) -> f32(A,B,C,D,E,30,V,W,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] 14. f32(A,B,C,D,E,J,K,L,P,U) -> f42(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] 15. f32(A,B,C,D,E,J,K,L,P,U) -> f42(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] 16. f42(A,B,C,D,E,J,K,L,P,U) -> f68(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] 17. f42(A,B,C,D,E,J,K,L,P,U) -> f68(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C] 18. f42(A,B,C,D,E,J,K,L,P,U) -> f60(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && 0 >= 1 + A1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] 19. f42(A,B,C,D,E,J,K,L,P,U) -> f60(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && A1 >= 1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] 20. f60(A,B,C,D,E,J,K,L,P,U) -> f60(A,B,C,D,E,J,K,L,P,1 + U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && A >= U] 21. f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] 22. f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] 23. f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] 24. f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] 25. f75(A,B,C,D,E,J,K,L,P,U) -> f10(A,B,1 + C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] (?,1) 26. f60(A,B,C,D,E,J,K,L,P,U) -> f42(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] 27. f10(A,B,C,D,E,J,K,L,P,U) -> f1(A,B,C,D,E,J,K,L,P,U) [C >= 1 + A] (?,1) 28. f2(A,B,C,D,E,J,K,L,P,U) -> f10(A,B,C,D,E,J,K,L,P,U) [B >= 1 + A] (?,1) 29. start(A,B,C,D,E,J,K,L,P,U) -> f2(A,B,C,D,E,J,K,L,P,U) True (1,1) Signature: {(f1,21) ;(f10,21) ;(f15,21) ;(f2,21) ;(f24,21) ;(f28,21) ;(f32,21) ;(f42,21) ;(f60,21) ;(f68,21) ;(f75,21) ;(start,21)} Flow Graph: [0->{0,28},1->{4,5,6,7},2->{4,5,6,7},3->{4,5,6,7},4->{8,9,10},5->{8,9,10},6->{4,5,6,7},7->{4,5,6,7},8->{1 ,2,25},9->{11,12,13},10->{11,12,13},11->{14,15},12->{14,15},13->{14,15},14->{16,17,18,19},15->{16,17,18,19} ,16->{21,22,23,24},17->{21,22,23,24},18->{20,26},19->{20,26},20->{20,26},21->{1,2,25},22->{1,2,25},23->{1,2 ,25},24->{1,2,25},25->{3,27},26->{16,17,18,19},27->{},28->{3,27},29->{0,28}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,4) ,(4,9) ,(8,1) ,(8,2) ,(16,21) ,(17,22) ,(17,23) ,(17,24)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f2(A,B,C,D,E,J,K,L,P,U) -> f2(A,1 + B,C,D,E,J,K,L,P,U) [A >= B] (?,1) 1. f75(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] (?,1) 2. f75(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] (?,1) 3. f10(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,D,0,J,K,L,P,U) [A >= C] (?,1) 4. f15(A,B,C,D,E,J,K,L,P,U) -> f24(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= A] (?,1) 5. f15(A,B,C,D,E,J,K,L,P,U) -> f24(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] (?,1) 6. f15(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] (?,1) 7. f15(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] (?,1) 8. f24(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] (?,1) 9. f24(A,B,C,D,E,J,K,L,P,U) -> f28(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] (?,1) 10. f24(A,B,C,D,E,J,K,L,P,U) -> f28(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] (?,1) 11. f28(A,B,C,D,E,J,K,L,P,U) -> f32(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 29 >= J] 12. f28(A,B,C,D,E,J,K,L,P,U) -> f32(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] 13. f28(A,B,C,D,E,J,K,L,P,U) -> f32(A,B,C,D,E,30,V,W,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] 14. f32(A,B,C,D,E,J,K,L,P,U) -> f42(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] 15. f32(A,B,C,D,E,J,K,L,P,U) -> f42(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] 16. f42(A,B,C,D,E,J,K,L,P,U) -> f68(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] 17. f42(A,B,C,D,E,J,K,L,P,U) -> f68(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C] 18. f42(A,B,C,D,E,J,K,L,P,U) -> f60(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && 0 >= 1 + A1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] 19. f42(A,B,C,D,E,J,K,L,P,U) -> f60(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && A1 >= 1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] 20. f60(A,B,C,D,E,J,K,L,P,U) -> f60(A,B,C,D,E,J,K,L,P,1 + U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && A >= U] 21. f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] 22. f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] 23. f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] 24. f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] 25. f75(A,B,C,D,E,J,K,L,P,U) -> f10(A,B,1 + C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] (?,1) 26. f60(A,B,C,D,E,J,K,L,P,U) -> f42(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 (?,1) && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] 27. f10(A,B,C,D,E,J,K,L,P,U) -> f1(A,B,C,D,E,J,K,L,P,U) [C >= 1 + A] (?,1) 28. f2(A,B,C,D,E,J,K,L,P,U) -> f10(A,B,C,D,E,J,K,L,P,U) [B >= 1 + A] (?,1) 29. start(A,B,C,D,E,J,K,L,P,U) -> f2(A,B,C,D,E,J,K,L,P,U) True (1,1) Signature: {(f1,21) ;(f10,21) ;(f15,21) ;(f2,21) ;(f24,21) ;(f28,21) ;(f32,21) ;(f42,21) ;(f60,21) ;(f68,21) ;(f75,21) ;(start,21)} Flow Graph: [0->{0,28},1->{5,6,7},2->{4,5,6,7},3->{4,5,6,7},4->{8,10},5->{8,9,10},6->{4,5,6,7},7->{4,5,6,7},8->{25} ,9->{11,12,13},10->{11,12,13},11->{14,15},12->{14,15},13->{14,15},14->{16,17,18,19},15->{16,17,18,19} ,16->{22,23,24},17->{21},18->{20,26},19->{20,26},20->{20,26},21->{1,2,25},22->{1,2,25},23->{1,2,25},24->{1,2 ,25},25->{3,27},26->{16,17,18,19},27->{},28->{3,27},29->{0,28}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f2(A,B,C,D,E,J,K,L,P,U) -> f2(A,1 + B,C,D,E,J,K,L,P,U) [A >= B] f75(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f75(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f10(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,D,0,J,K,L,P,U) [A >= C] f15(A,B,C,D,E,J,K,L,P,U) -> f24(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= A] f15(A,B,C,D,E,J,K,L,P,U) -> f24(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] f15(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] f15(A,B,C,D,E,J,K,L,P,U) -> f15(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] f24(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] f24(A,B,C,D,E,J,K,L,P,U) -> f28(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f24(A,B,C,D,E,J,K,L,P,U) -> f28(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f28(A,B,C,D,E,J,K,L,P,U) -> f32(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 29 >= J] f28(A,B,C,D,E,J,K,L,P,U) -> f32(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] f28(A,B,C,D,E,J,K,L,P,U) -> f32(A,B,C,D,E,30,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] f32(A,B,C,D,E,J,K,L,P,U) -> f42(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] f32(A,B,C,D,E,J,K,L,P,U) -> f42(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] f42(A,B,C,D,E,J,K,L,P,U) -> f68(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] f42(A,B,C,D,E,J,K,L,P,U) -> f68(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C] f42(A,B,C,D,E,J,K,L,P,U) -> f60(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && 0 >= 1 + A1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f42(A,B,C,D,E,J,K,L,P,U) -> f60(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && A1 >= 1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f60(A,B,C,D,E,J,K,L,P,U) -> f60(A,B,C,D,E,J,K,L,P,1 + U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && A >= U] f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] f68(A,B,C,D,E,J,K,L,P,U) -> f75(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f75(A,B,C,D,E,J,K,L,P,U) -> f10(A,B,1 + C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] f60(A,B,C,D,E,J,K,L,P,U) -> f42(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f10(A,B,C,D,E,J,K,L,P,U) -> f1(A,B,C,D,E,J,K,L,P,U) [C >= 1 + A] f2(A,B,C,D,E,J,K,L,P,U) -> f10(A,B,C,D,E,J,K,L,P,U) [B >= 1 + A] start(A,B,C,D,E,J,K,L,P,U) -> f2(A,B,C,D,E,J,K,L,P,U) True Signature: {(f1,21) ;(f10,21) ;(f15,21) ;(f2,21) ;(f24,21) ;(f28,21) ;(f32,21) ;(f42,21) ;(f60,21) ;(f68,21) ;(f75,21) ;(start,21)} Rule Graph: [0->{0,28},1->{5,6,7},2->{4,5,6,7},3->{4,5,6,7},4->{8,10},5->{8,9,10},6->{4,5,6,7},7->{4,5,6,7},8->{25} ,9->{11,12,13},10->{11,12,13},11->{14,15},12->{14,15},13->{14,15},14->{16,17,18,19},15->{16,17,18,19} ,16->{22,23,24},17->{21},18->{20,26},19->{20,26},20->{20,26},21->{1,2,25},22->{1,2,25},23->{1,2,25},24->{1,2 ,25},25->{3,27},26->{16,17,18,19},27->{},28->{3,27},29->{0,28}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f2.0(A,B,C,D,E,J,K,L,P,U) -> f2.0(A,1 + B,C,D,E,J,K,L,P,U) [A >= B] f2.0(A,B,C,D,E,J,K,L,P,U) -> f2.28(A,1 + B,C,D,E,J,K,L,P,U) [A >= B] f75.1(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f75.1(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f75.1(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f75.2(A,B,C,D,E,J,K,L,P,U) -> f15.4(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f75.2(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f75.2(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f75.2(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f10.3(A,B,C,D,E,J,K,L,P,U) -> f15.4(A,B,C,D,0,J,K,L,P,U) [A >= C] f10.3(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,D,0,J,K,L,P,U) [A >= C] f10.3(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,D,0,J,K,L,P,U) [A >= C] f10.3(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,D,0,J,K,L,P,U) [A >= C] f15.4(A,B,C,D,E,J,K,L,P,U) -> f24.8(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= A] f15.4(A,B,C,D,E,J,K,L,P,U) -> f24.10(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= A] f15.5(A,B,C,D,E,J,K,L,P,U) -> f24.8(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] f15.5(A,B,C,D,E,J,K,L,P,U) -> f24.9(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] f15.5(A,B,C,D,E,J,K,L,P,U) -> f24.10(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] f15.6(A,B,C,D,E,J,K,L,P,U) -> f15.4(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] f15.6(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] f15.6(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] f15.6(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] f15.7(A,B,C,D,E,J,K,L,P,U) -> f15.4(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] f15.7(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] f15.7(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] f15.7(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] f24.8(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] f24.9(A,B,C,D,E,J,K,L,P,U) -> f28.11(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f24.9(A,B,C,D,E,J,K,L,P,U) -> f28.12(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f24.9(A,B,C,D,E,J,K,L,P,U) -> f28.13(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f24.10(A,B,C,D,E,J,K,L,P,U) -> f28.11(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f24.10(A,B,C,D,E,J,K,L,P,U) -> f28.12(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f24.10(A,B,C,D,E,J,K,L,P,U) -> f28.13(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f28.11(A,B,C,D,E,J,K,L,P,U) -> f32.14(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 29 >= J] f28.11(A,B,C,D,E,J,K,L,P,U) -> f32.15(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 29 >= J] f28.12(A,B,C,D,E,J,K,L,P,U) -> f32.14(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] f28.12(A,B,C,D,E,J,K,L,P,U) -> f32.15(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] f28.13(A,B,C,D,E,J,K,L,P,U) -> f32.14(A,B,C,D,E,30,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] f28.13(A,B,C,D,E,J,K,L,P,U) -> f32.15(A,B,C,D,E,30,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] f32.14(A,B,C,D,E,J,K,L,P,U) -> f42.16(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] f32.14(A,B,C,D,E,J,K,L,P,U) -> f42.17(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] f32.14(A,B,C,D,E,J,K,L,P,U) -> f42.18(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] f32.14(A,B,C,D,E,J,K,L,P,U) -> f42.19(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] f32.15(A,B,C,D,E,J,K,L,P,U) -> f42.16(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] f32.15(A,B,C,D,E,J,K,L,P,U) -> f42.17(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] f32.15(A,B,C,D,E,J,K,L,P,U) -> f42.18(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] f32.15(A,B,C,D,E,J,K,L,P,U) -> f42.19(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] f42.16(A,B,C,D,E,J,K,L,P,U) -> f68.22(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] f42.16(A,B,C,D,E,J,K,L,P,U) -> f68.23(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] f42.16(A,B,C,D,E,J,K,L,P,U) -> f68.24(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] f42.17(A,B,C,D,E,J,K,L,P,U) -> f68.21(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C] f42.18(A,B,C,D,E,J,K,L,P,U) -> f60.20(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && 0 >= 1 + A1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f42.18(A,B,C,D,E,J,K,L,P,U) -> f60.26(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && 0 >= 1 + A1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f42.19(A,B,C,D,E,J,K,L,P,U) -> f60.20(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && A1 >= 1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f42.19(A,B,C,D,E,J,K,L,P,U) -> f60.26(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && A1 >= 1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f60.20(A,B,C,D,E,J,K,L,P,U) -> f60.20(A,B,C,D,E,J,K,L,P,1 + U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && A >= U] f60.20(A,B,C,D,E,J,K,L,P,U) -> f60.26(A,B,C,D,E,J,K,L,P,1 + U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && A >= U] f68.21(A,B,C,D,E,J,K,L,P,U) -> f75.1(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] f68.21(A,B,C,D,E,J,K,L,P,U) -> f75.2(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] f68.21(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] f68.22(A,B,C,D,E,J,K,L,P,U) -> f75.1(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] f68.22(A,B,C,D,E,J,K,L,P,U) -> f75.2(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] f68.22(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] f68.23(A,B,C,D,E,J,K,L,P,U) -> f75.1(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] f68.23(A,B,C,D,E,J,K,L,P,U) -> f75.2(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] f68.23(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] f68.24(A,B,C,D,E,J,K,L,P,U) -> f75.1(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f68.24(A,B,C,D,E,J,K,L,P,U) -> f75.2(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f68.24(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f75.25(A,B,C,D,E,J,K,L,P,U) -> f10.3(A,B,1 + C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] f75.25(A,B,C,D,E,J,K,L,P,U) -> f10.27(A,B,1 + C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] f60.26(A,B,C,D,E,J,K,L,P,U) -> f42.16(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f60.26(A,B,C,D,E,J,K,L,P,U) -> f42.17(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f60.26(A,B,C,D,E,J,K,L,P,U) -> f42.18(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f60.26(A,B,C,D,E,J,K,L,P,U) -> f42.19(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f10.27(A,B,C,D,E,J,K,L,P,U) -> f1.30(A,B,C,D,E,J,K,L,P,U) [C >= 1 + A] f2.28(A,B,C,D,E,J,K,L,P,U) -> f10.3(A,B,C,D,E,J,K,L,P,U) [B >= 1 + A] f2.28(A,B,C,D,E,J,K,L,P,U) -> f10.27(A,B,C,D,E,J,K,L,P,U) [B >= 1 + A] start.29(A,B,C,D,E,J,K,L,P,U) -> f2.0(A,B,C,D,E,J,K,L,P,U) True start.29(A,B,C,D,E,J,K,L,P,U) -> f2.28(A,B,C,D,E,J,K,L,P,U) True Signature: {(f1.30,10) ;(f10.27,10) ;(f10.3,10) ;(f15.4,10) ;(f15.5,10) ;(f15.6,10) ;(f15.7,10) ;(f2.0,10) ;(f2.28,10) ;(f24.10,10) ;(f24.8,10) ;(f24.9,10) ;(f28.11,10) ;(f28.12,10) ;(f28.13,10) ;(f32.14,10) ;(f32.15,10) ;(f42.16,10) ;(f42.17,10) ;(f42.18,10) ;(f42.19,10) ;(f60.20,10) ;(f60.26,10) ;(f68.21,10) ;(f68.22,10) ;(f68.23,10) ;(f68.24,10) ;(f75.1,10) ;(f75.2,10) ;(f75.25,10) ;(start.29,10)} Rule Graph: [0->{0,1},1->{76,77},2->{15,16,17},3->{18,19,20,21},4->{22,23,24,25},5->{13,14},6->{15,16,17},7->{18,19,20 ,21},8->{22,23,24,25},9->{13,14},10->{15,16,17},11->{18,19,20,21},12->{22,23,24,25},13->{26},14->{30,31,32} ,15->{26},16->{27,28,29},17->{30,31,32},18->{13,14},19->{15,16,17},20->{18,19,20,21},21->{22,23,24,25} ,22->{13,14},23->{15,16,17},24->{18,19,20,21},25->{22,23,24,25},26->{69,70},27->{33,34},28->{35,36},29->{37 ,38},30->{33,34},31->{35,36},32->{37,38},33->{39,40,41,42},34->{43,44,45,46},35->{39,40,41,42},36->{43,44,45 ,46},37->{39,40,41,42},38->{43,44,45,46},39->{47,48,49},40->{50},41->{51,52},42->{53,54},43->{47,48,49} ,44->{50},45->{51,52},46->{53,54},47->{60,61,62},48->{63,64,65},49->{66,67,68},50->{57,58,59},51->{55,56} ,52->{71,72,73,74},53->{55,56},54->{71,72,73,74},55->{55,56},56->{71,72,73,74},57->{2,3,4},58->{5,6,7,8} ,59->{69,70},60->{2,3,4},61->{5,6,7,8},62->{69,70},63->{2,3,4},64->{5,6,7,8},65->{69,70},66->{2,3,4},67->{5 ,6,7,8},68->{69,70},69->{9,10,11,12},70->{75},71->{47,48,49},72->{50},73->{51,52},74->{53,54},75->{},76->{9 ,10,11,12},77->{75},78->{0,1},79->{76,77}] + Applied Processor: AddSinks + Details: () * Step 6: Failure MAYBE + Considered Problem: Rules: f2.0(A,B,C,D,E,J,K,L,P,U) -> f2.0(A,1 + B,C,D,E,J,K,L,P,U) [A >= B] f2.0(A,B,C,D,E,J,K,L,P,U) -> f2.28(A,1 + B,C,D,E,J,K,L,P,U) [A >= B] f75.1(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f75.1(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f75.1(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f75.2(A,B,C,D,E,J,K,L,P,U) -> f15.4(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f75.2(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f75.2(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f75.2(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f10.3(A,B,C,D,E,J,K,L,P,U) -> f15.4(A,B,C,D,0,J,K,L,P,U) [A >= C] f10.3(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,D,0,J,K,L,P,U) [A >= C] f10.3(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,D,0,J,K,L,P,U) [A >= C] f10.3(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,D,0,J,K,L,P,U) [A >= C] f15.4(A,B,C,D,E,J,K,L,P,U) -> f24.8(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= A] f15.4(A,B,C,D,E,J,K,L,P,U) -> f24.10(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= A] f15.5(A,B,C,D,E,J,K,L,P,U) -> f24.8(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] f15.5(A,B,C,D,E,J,K,L,P,U) -> f24.9(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] f15.5(A,B,C,D,E,J,K,L,P,U) -> f24.10(A,B,C,D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && A >= 1 + D] f15.6(A,B,C,D,E,J,K,L,P,U) -> f15.4(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] f15.6(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] f15.6(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] f15.6(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] f15.7(A,B,C,D,E,J,K,L,P,U) -> f15.4(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] f15.7(A,B,C,D,E,J,K,L,P,U) -> f15.5(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] f15.7(A,B,C,D,E,J,K,L,P,U) -> f15.6(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] f15.7(A,B,C,D,E,J,K,L,P,U) -> f15.7(A,B,C,1 + D,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] f24.8(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] f24.9(A,B,C,D,E,J,K,L,P,U) -> f28.11(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f24.9(A,B,C,D,E,J,K,L,P,U) -> f28.12(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f24.9(A,B,C,D,E,J,K,L,P,U) -> f28.13(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C >= 1 + D] f24.10(A,B,C,D,E,J,K,L,P,U) -> f28.11(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f24.10(A,B,C,D,E,J,K,L,P,U) -> f28.12(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f24.10(A,B,C,D,E,J,K,L,P,U) -> f28.13(A,B,C,D,1 + E,E,K,L,P,U) [E >= 0 && A + -1*C >= 0 && D >= 1 + C] f28.11(A,B,C,D,E,J,K,L,P,U) -> f32.14(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 29 >= J] f28.11(A,B,C,D,E,J,K,L,P,U) -> f32.15(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 29 >= J] f28.12(A,B,C,D,E,J,K,L,P,U) -> f32.14(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] f28.12(A,B,C,D,E,J,K,L,P,U) -> f32.15(A,B,C,D,E,J,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] f28.13(A,B,C,D,E,J,K,L,P,U) -> f32.14(A,B,C,D,E,30,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] f28.13(A,B,C,D,E,J,K,L,P,U) -> f32.15(A,B,C,D,E,30,V,W,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] f32.14(A,B,C,D,E,J,K,L,P,U) -> f42.16(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] f32.14(A,B,C,D,E,J,K,L,P,U) -> f42.17(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] f32.14(A,B,C,D,E,J,K,L,P,U) -> f42.18(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] f32.14(A,B,C,D,E,J,K,L,P,U) -> f42.19(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && Y >= K*X + X*Z && K*X + X + X*Z >= 1 + Y && K >= 0] f32.15(A,B,C,D,E,J,K,L,P,U) -> f42.16(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] f32.15(A,B,C,D,E,J,K,L,P,U) -> f42.17(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] f32.15(A,B,C,D,E,J,K,L,P,U) -> f42.18(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] f32.15(A,B,C,D,E,J,K,L,P,U) -> f42.19(A,B,C,D,E,J,V + -1*W + X,L,1,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && X*Z + Y >= K*X && K*X + X >= 1 + X*Z + Y && 0 >= 1 + K] f42.16(A,B,C,D,E,J,K,L,P,U) -> f68.22(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] f42.16(A,B,C,D,E,J,K,L,P,U) -> f68.23(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] f42.16(A,B,C,D,E,J,K,L,P,U) -> f68.24(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B] f42.17(A,B,C,D,E,J,K,L,P,U) -> f68.21(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C] f42.18(A,B,C,D,E,J,K,L,P,U) -> f60.20(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && 0 >= 1 + A1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f42.18(A,B,C,D,E,J,K,L,P,U) -> f60.26(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && 0 >= 1 + A1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f42.19(A,B,C,D,E,J,K,L,P,U) -> f60.20(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && A1 >= 1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f42.19(A,B,C,D,E,J,K,L,P,U) -> f60.26(A,B,C,D,E,J,-1*O*W + V,X,Y,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K*X >= A1*V*X && A1*V*X + V >= 1 + K*X && A1 >= 1 && B >= C && B1*P >= A1*C1 && A1*C1 + C1 >= 1 + B1*P && C1 >= Y && B1*P >= A1*D1 && A1*D1 + D1 >= 1 + B1*P && Y >= D1 && K >= A1*E1 && A1*E1 + E1 >= 1 + K && E1 >= Z && K >= A1*F1 && A1*F1 + F1 >= 1 + K && Z >= F1 && B1*P*X >= A1*G1*X && A1*G1*X + G1 >= 1 + B1*P*X && G1 >= H1 && B1*P*X >= A1*I1*X && A1*I1*X + I1 >= 1 + B1*P*X && H1 >= I1] f60.20(A,B,C,D,E,J,K,L,P,U) -> f60.20(A,B,C,D,E,J,K,L,P,1 + U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && A >= U] f60.20(A,B,C,D,E,J,K,L,P,U) -> f60.26(A,B,C,D,E,J,K,L,P,1 + U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && A >= U] f68.21(A,B,C,D,E,J,K,L,P,U) -> f75.1(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] f68.21(A,B,C,D,E,J,K,L,P,U) -> f75.2(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] f68.21(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && B >= C && L = 0] f68.22(A,B,C,D,E,J,K,L,P,U) -> f75.1(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] f68.22(A,B,C,D,E,J,K,L,P,U) -> f75.2(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] f68.22(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && 0 >= 1 + L] f68.23(A,B,C,D,E,J,K,L,P,U) -> f75.1(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] f68.23(A,B,C,D,E,J,K,L,P,U) -> f75.2(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] f68.23(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && L >= 1] f68.24(A,B,C,D,E,J,K,L,P,U) -> f75.1(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f68.24(A,B,C,D,E,J,K,L,P,U) -> f75.2(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f68.24(A,B,C,D,E,J,K,L,P,U) -> f75.25(A,B,C,D,E,J,K,0,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f75.25(A,B,C,D,E,J,K,L,P,U) -> f10.3(A,B,1 + C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] f75.25(A,B,C,D,E,J,K,L,P,U) -> f10.27(A,B,1 + C,C,E,J,K,L,P,U) [E >= 0 && A + -1*C >= 0 && C = D] f60.26(A,B,C,D,E,J,K,L,P,U) -> f42.16(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f60.26(A,B,C,D,E,J,K,L,P,U) -> f42.17(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f60.26(A,B,C,D,E,J,K,L,P,U) -> f42.18(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f60.26(A,B,C,D,E,J,K,L,P,U) -> f42.19(A,-1 + B,C,D,E,J,K,L,P,U) [1 + -1*E + J >= 0 && -1 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f10.27(A,B,C,D,E,J,K,L,P,U) -> f1.30(A,B,C,D,E,J,K,L,P,U) [C >= 1 + A] f2.28(A,B,C,D,E,J,K,L,P,U) -> f10.3(A,B,C,D,E,J,K,L,P,U) [B >= 1 + A] f2.28(A,B,C,D,E,J,K,L,P,U) -> f10.27(A,B,C,D,E,J,K,L,P,U) [B >= 1 + A] start.29(A,B,C,D,E,J,K,L,P,U) -> f2.0(A,B,C,D,E,J,K,L,P,U) True start.29(A,B,C,D,E,J,K,L,P,U) -> f2.28(A,B,C,D,E,J,K,L,P,U) True f1.30(A,B,C,D,E,J,K,L,P,U) -> exitus616(A,B,C,D,E,J,K,L,P,U) True f1.30(A,B,C,D,E,J,K,L,P,U) -> exitus616(A,B,C,D,E,J,K,L,P,U) True f1.30(A,B,C,D,E,J,K,L,P,U) -> exitus616(A,B,C,D,E,J,K,L,P,U) True f1.30(A,B,C,D,E,J,K,L,P,U) -> exitus616(A,B,C,D,E,J,K,L,P,U) True Signature: {(exitus616,10) ;(f1.30,10) ;(f10.27,10) ;(f10.3,10) ;(f15.4,10) ;(f15.5,10) ;(f15.6,10) ;(f15.7,10) ;(f2.0,10) ;(f2.28,10) ;(f24.10,10) ;(f24.8,10) ;(f24.9,10) ;(f28.11,10) ;(f28.12,10) ;(f28.13,10) ;(f32.14,10) ;(f32.15,10) ;(f42.16,10) ;(f42.17,10) ;(f42.18,10) ;(f42.19,10) ;(f60.20,10) ;(f60.26,10) ;(f68.21,10) ;(f68.22,10) ;(f68.23,10) ;(f68.24,10) ;(f75.1,10) ;(f75.2,10) ;(f75.25,10) ;(start.29,10)} Rule Graph: [0->{0,1},1->{76,77},2->{15,16,17},3->{18,19,20,21},4->{22,23,24,25},5->{13,14},6->{15,16,17},7->{18,19,20 ,21},8->{22,23,24,25},9->{13,14},10->{15,16,17},11->{18,19,20,21},12->{22,23,24,25},13->{26},14->{30,31,32} ,15->{26},16->{27,28,29},17->{30,31,32},18->{13,14},19->{15,16,17},20->{18,19,20,21},21->{22,23,24,25} ,22->{13,14},23->{15,16,17},24->{18,19,20,21},25->{22,23,24,25},26->{69,70},27->{33,34},28->{35,36},29->{37 ,38},30->{33,34},31->{35,36},32->{37,38},33->{39,40,41,42},34->{43,44,45,46},35->{39,40,41,42},36->{43,44,45 ,46},37->{39,40,41,42},38->{43,44,45,46},39->{47,48,49},40->{50},41->{51,52},42->{53,54},43->{47,48,49} ,44->{50},45->{51,52},46->{53,54},47->{60,61,62},48->{63,64,65},49->{66,67,68},50->{57,58,59},51->{55,56} ,52->{71,72,73,74},53->{55,56},54->{71,72,73,74},55->{55,56},56->{71,72,73,74},57->{2,3,4},58->{5,6,7,8} ,59->{69,70},60->{2,3,4},61->{5,6,7,8},62->{69,70},63->{2,3,4},64->{5,6,7,8},65->{69,70},66->{2,3,4},67->{5 ,6,7,8},68->{69,70},69->{9,10,11,12},70->{75},71->{47,48,49},72->{50},73->{51,52},74->{53,54},75->{80,81,82 ,83},76->{9,10,11,12},77->{75},78->{0,1},79->{76,77}] + 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,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83] | +- p:[0] c: [0] | `- p:[9,69,26,13,5,58,50,40,33,27,16,2,57,60,47,39,35,28,31,14,18,3,63,48,43,34,30,17,6,61,64,67,49,71,52,41,37,29,32,45,36,38,73,54,42,46,74,56,51,53,55,10,19,7,11,20,24,4,66,8,12,21,25,23,22,44,72,15,59,62,65,68] c: [3,4,7,8,9,10,11,12,13,15,18,19,20,21,22,23,24,25,26,41,42,45,46,51,52,53,54,55,56,59,62,65,68,69,71,72,73,74] | `- p:[2,57,50,40,33,27,16,6,58,61,47,39,35,28,31,14,5,64,48,43,34,30,17,36,38,29,32,67,49,37,44,60,63,66] c: [27,29,30,32,33,34,37,38] | `- p:[2,57,50,40,35,28,16,6,58,61,47,39,43,36,31,14,5,64,48,67,49,17,44,60,63,66] c: [] MAYBE