MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f74(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f33(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,L,W,W,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 && K >= 0] 15. f33(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,L,M,-1*W,1,1,0,W,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 + 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,V,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) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && 0 >= 1 + Y] 19. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] 20. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(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) -> f74(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) -> f74(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) -> f74(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) -> f74(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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. f59(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f80(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. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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) -> f0(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: {(f0,21) ;(f13,21) ;(f16,21) ;(f26,21) ;(f29,21) ;(f33,21) ;(f42,21) ;(f59,21) ;(f68,21) ;(f74,21) ;(f80,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 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f74(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f33(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,L,W,W,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 && K >= 0] 15. f33(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,L,M,-1*W,1,1,0,W,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 + 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,V,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) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && 0 >= 1 + Y] 19. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] 20. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(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) -> f74(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) -> f74(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) -> f74(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) -> f74(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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. f59(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f80(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. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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) -> f0(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: {(f0,21) ;(f13,21) ;(f16,21) ;(f26,21) ;(f29,21) ;(f33,21) ;(f42,21) ;(f59,21) ;(f68,21) ;(f74,21) ;(f80,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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f74(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f33(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,L,W,W,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 && K >= 0] 15. f33(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,L,M,-1*W,1,1,0,W,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 + 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,V,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) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && 0 >= 1 + Y] 19. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] 20. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(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) -> f74(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) -> f74(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) -> f74(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) -> f74(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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. f59(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f80(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,1) 28. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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,1) 29. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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: {(f0,21) ;(f13,21) ;(f16,21) ;(f26,21) ;(f29,21) ;(f33,21) ;(f42,21) ;(f59,21) ;(f68,21) ;(f74,21) ;(f80,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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 1 + x1 + -1*x3 p(f13) = 1 + x1 + -1*x3 p(f16) = 1 + x1 + -1*x3 p(f26) = 1 + x1 + -1*x3 p(f29) = 1 + x1 + -1*x3 p(f33) = 1 + x1 + -1*x3 p(f42) = 1 + x1 + -1*x3 p(f59) = 1 + x1 + -1*x3 p(f68) = 1 + x1 + -1*x3 p(f74) = 1 + x1 + -1*x3 p(f80) = 1 + x1 + -1*x3 p(start) = 1 + x1 + -1*x3 Following rules are strictly oriented: [E >= 0 && A + -1*C >= 0 && C = D] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C > A + -1*C = f13(A,B,1 + C,C,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) Following rules are weakly oriented: [A >= B] ==> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f0(A,1 + 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] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f16(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] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= C] ==> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f16(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && D >= A] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f26(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 && A >= 1 + D] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f26(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 && 0 >= 1 + X && A >= 1 + D] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f16(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] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f16(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 && C = D] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f74(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 >= 1 + D] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f29(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] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f29(A,B,C,D,1 + E,F,G,H,I,E,K,L,M,N,O,P,Q,R,S,T,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] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K >= 0] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f42(A,B,C,D,E,F,G,H,I,J,V,L,W,W,1,1,0,R,S,T,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 + K] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f42(A,B,C,D,E,F,G,H,I,J,V,L,M,-1*W,1,1,0,W,S,T,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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = 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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f68(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,V,W,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 && 0 >= 1 + Y] f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f59(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f74(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f74(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f74(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f74(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && B + -1*C >= 0 && A + -1*C >= 0 && J >= 0 && U >= 1 + A] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f42(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 1 + A] ==> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [B >= 1 + A] ==> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True ==> start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*C >= 1 + A + -1*C = f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) * Step 4: KnowledgePropagation MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f74(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f33(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,L,W,W,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 && K >= 0] 15. f33(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,L,M,-1*W,1,1,0,W,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 + 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,V,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) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && 0 >= 1 + Y] 19. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] 20. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(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) -> f74(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) -> f74(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) -> f74(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) -> f74(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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 + A + C,1) 26. f59(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f80(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,1) 28. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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,1) 29. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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: {(f0,21) ;(f13,21) ;(f16,21) ;(f26,21) ;(f29,21) ;(f33,21) ;(f42,21) ;(f59,21) ;(f68,21) ;(f74,21) ;(f80,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: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 5: PolyRank MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= C] (2 + A + C,1) 4. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f74(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f33(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,L,W,W,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 && K >= 0] 15. f33(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,L,M,-1*W,1,1,0,W,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 + 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,V,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) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && 0 >= 1 + Y] 19. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] 20. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(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) -> f74(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) -> f74(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) -> f74(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) -> f74(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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 + A + C,1) 26. f59(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f80(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,1) 28. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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,1) 29. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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: {(f0,21) ;(f13,21) ;(f16,21) ;(f26,21) ;(f29,21) ;(f33,21) ;(f42,21) ;(f59,21) ;(f68,21) ;(f74,21) ;(f80,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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = 1 + x1 + -1*x21 p(f13) = 1 + x1 + -1*x21 p(f16) = 1 + x1 + -1*x21 p(f26) = 1 + x1 + -1*x21 p(f29) = 1 + x1 + -1*x21 p(f33) = 1 + x1 + -1*x21 p(f42) = 1 + x1 + -1*x21 p(f59) = 1 + x1 + -1*x21 p(f68) = 1 + x1 + -1*x21 p(f74) = 1 + x1 + -1*x21 p(f80) = 1 + x1 + -1*x21 p(start) = 1 + x1 + -1*x21 Following rules are strictly oriented: [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] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U > A + -1*U = f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,V,T,1 + U) Following rules are weakly oriented: [A >= B] ==> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f0(A,1 + 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] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f16(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] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= C] ==> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f16(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && D >= A] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f26(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 && A >= 1 + D] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f26(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 && 0 >= 1 + X && A >= 1 + D] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f16(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] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f16(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 && C = D] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f74(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 >= 1 + D] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f29(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] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f29(A,B,C,D,1 + E,F,G,H,I,E,K,L,M,N,O,P,Q,R,S,T,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] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K >= 0] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f42(A,B,C,D,E,F,G,H,I,J,V,L,W,W,1,1,0,R,S,T,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 + K] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f42(A,B,C,D,E,F,G,H,I,J,V,L,M,-1*W,1,1,0,W,S,T,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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f68(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,V,W,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 && 0 >= 1 + Y] f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f74(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f74(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f74(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f74(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && C = D] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f13(A,B,1 + C,C,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,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] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f42(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 1 + A] ==> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [B >= 1 + A] ==> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True ==> start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = 1 + A + -1*U >= 1 + A + -1*U = f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) * Step 6: PolyRank MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= C] (2 + A + C,1) 4. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f74(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f33(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,L,W,W,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 && K >= 0] 15. f33(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,L,M,-1*W,1,1,0,W,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 + 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,V,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) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && 0 >= 1 + Y] 19. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] 20. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(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 + A + U,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) -> f74(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) -> f74(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) -> f74(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) -> f74(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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 + A + C,1) 26. f59(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f80(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,1) 28. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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,1) 29. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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: {(f0,21) ;(f13,21) ;(f16,21) ;(f26,21) ;(f29,21) ;(f33,21) ;(f42,21) ;(f59,21) ;(f68,21) ;(f74,21) ;(f80,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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = x1 + -1*x4 p(f13) = x1 + -1*x4 p(f16) = x1 + -1*x4 p(f26) = x1 + -1*x4 p(f29) = x1 + -1*x4 p(f33) = x1 + -1*x4 p(f42) = x1 + -1*x4 p(f59) = x1 + -1*x4 p(f68) = x1 + -1*x4 p(f74) = x1 + -1*x4 p(f80) = x1 + -1*x4 p(start) = x1 + -1*x4 Following rules are strictly oriented: [E >= 0 && A + -1*C >= 0 && X >= 1 && A >= 1 + D] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D > -1 + A + -1*D = f16(A,B,C,1 + D,E,V,W,V + W,X,J,K,L,M,N,O,P,Q,R,S,T,U) Following rules are weakly oriented: [A >= B] ==> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f0(A,1 + 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] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f16(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] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= C] ==> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f16(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && D >= A] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f26(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 && A >= 1 + D] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f26(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 && 0 >= 1 + X && A >= 1 + D] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= -1 + A + -1*D = f16(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 && C = D] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*C = f74(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 >= 1 + D] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f29(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] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f29(A,B,C,D,1 + E,F,G,H,I,E,K,L,M,N,O,P,Q,R,S,T,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] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K >= 0] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f42(A,B,C,D,E,F,G,H,I,J,V,L,W,W,1,1,0,R,S,T,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 + K] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f42(A,B,C,D,E,F,G,H,I,J,V,L,M,-1*W,1,1,0,W,S,T,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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = 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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f68(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,V,W,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 && 0 >= 1 + Y] f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f59(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f74(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f74(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f74(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f74(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && C = D] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*C = f13(A,B,1 + C,C,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,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] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f42(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 1 + A] ==> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [B >= 1 + A] ==> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True ==> start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) * Step 7: PolyRank MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= C] (2 + A + C,1) 4. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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] (A + D,1) 8. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f74(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f33(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,L,W,W,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 && K >= 0] 15. f33(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,L,M,-1*W,1,1,0,W,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 + 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,V,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) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && 0 >= 1 + Y] 19. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] 20. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(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 + A + U,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) -> f74(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) -> f74(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) -> f74(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) -> f74(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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 + A + C,1) 26. f59(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f80(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,1) 28. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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,1) 29. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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: {(f0,21) ;(f13,21) ;(f16,21) ;(f26,21) ;(f29,21) ;(f33,21) ;(f42,21) ;(f59,21) ;(f68,21) ;(f74,21) ;(f80,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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(f0) = x1 + -1*x4 p(f13) = x1 + -1*x4 p(f16) = x1 + -1*x4 p(f26) = x1 + -1*x4 p(f29) = x1 + -1*x4 p(f33) = x1 + -1*x4 p(f42) = x1 + -1*x4 p(f59) = x1 + -1*x4 p(f68) = x1 + -1*x4 p(f74) = x1 + -1*x4 p(f80) = x1 + -1*x4 p(start) = x1 + -1*x4 Following rules are strictly oriented: [E >= 0 && A + -1*C >= 0 && 0 >= 1 + X && A >= 1 + D] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D > -1 + A + -1*D = f16(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] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D > -1 + A + -1*D = f16(A,B,C,1 + D,E,V,W,V + W,X,J,K,L,M,N,O,P,Q,R,S,T,U) Following rules are weakly oriented: [A >= B] ==> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f0(A,1 + 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] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f16(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] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= C] ==> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f16(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && D >= A] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f26(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 && A >= 1 + D] ==> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f26(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 && C = D] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*C = f74(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 >= 1 + D] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f29(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] ==> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f29(A,B,C,D,1 + E,F,G,H,I,E,K,L,M,N,O,P,Q,R,S,T,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] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J >= 31] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && J = 30] f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f33(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && K >= 0] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f42(A,B,C,D,E,F,G,H,I,J,V,L,W,W,1,1,0,R,S,T,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 + K] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f42(A,B,C,D,E,F,G,H,I,J,V,L,M,-1*W,1,1,0,W,S,T,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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = 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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f68(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,V,W,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 && 0 >= 1 + Y] f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f59(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f74(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f74(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 + 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,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f74(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 + E >= 0 && -1 + E + J >= 0 && -1 + E + -1*J >= 0 && A + -1*C >= 0 && J >= 0 && C >= 1 + B && L = 0] f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f74(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,U) [E >= 0 && A + -1*C >= 0 && C = D] ==> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*C = f13(A,B,1 + C,C,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,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] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f42(A,-1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [C >= 1 + A] ==> f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [B >= 1 + A] ==> f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True ==> start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) = A + -1*D >= A + -1*D = f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) * Step 8: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [A >= C] (2 + A + C,1) 4. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f26(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. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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] (A + D,1) 7. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f16(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] (A + D,1) 8. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f74(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f29(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f29(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f33(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. f33(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,L,W,W,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 && K >= 0] 15. f33(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,L,M,-1*W,1,1,0,W,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 + 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,V,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) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && 0 >= 1 + Y] 19. f42(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(A,B,C,D,E,F,G,H,I,J,V,W,M,N,X,Z,A1,R,B1,C1,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 && Y >= 1] 20. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f59(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 + A + U,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) -> f74(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) -> f74(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) -> f74(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) -> f74(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. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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 + A + C,1) 26. f59(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. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f80(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,1) 28. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(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,1) 29. start(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f0(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: {(f0,21) ;(f13,21) ;(f16,21) ;(f26,21) ;(f29,21) ;(f33,21) ;(f42,21) ;(f59,21) ;(f68,21) ;(f74,21) ;(f80,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: Failing "Open problems left." + Details: Open problems left. MAYBE