MAYBE * Step 1: 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) [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) [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) [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) [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) [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) [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) [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) [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) [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) [29 >= J] (?,1) 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) [J >= 31] (?,1) 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) [J = 30] (?,1) 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) [K >= 0] (?,1) 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) [0 >= 1 + K] (?,1) 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) [C >= 1 + B] (?,1) 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) [B >= C] (?,1) 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) [B >= C && 0 >= 1 + Y] (?,1) 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) [B >= C && Y >= 1] (?,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) [A >= U] (?,1) 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) [B >= C && L = 0] (?,1) 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) [0 >= 1 + L] (?,1) 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) [L >= 1] (?,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) [C >= 1 + B && L = 0] (?,1) 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) [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) [U >= 1 + A] (?,1) 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: 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) [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) [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) [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) [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) [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) [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) [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) [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) [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) [29 >= J] (?,1) 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) [J >= 31] (?,1) 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) [J = 30] (?,1) 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) [K >= 0] (?,1) 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) [0 >= 1 + K] (?,1) 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) [C >= 1 + B] (?,1) 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) [B >= C] (?,1) 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) [B >= C && 0 >= 1 + Y] (?,1) 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) [B >= C && Y >= 1] (?,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) [A >= U] (?,1) 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) [B >= C && L = 0] (?,1) 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) [0 >= 1 + L] (?,1) 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) [L >= 1] (?,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) [C >= 1 + B && L = 0] (?,1) 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) [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) [U >= 1 + A] (?,1) 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->{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: [(8,1),(8,2),(16,21),(17,22),(17,23),(17,24)] * Step 3: AddSinks 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) [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) [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) [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) [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) [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) [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) [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) [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) [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) [29 >= J] (?,1) 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) [J >= 31] (?,1) 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) [J = 30] (?,1) 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) [K >= 0] (?,1) 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) [0 >= 1 + K] (?,1) 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) [C >= 1 + B] (?,1) 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) [B >= C] (?,1) 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) [B >= C && 0 >= 1 + Y] (?,1) 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) [B >= C && Y >= 1] (?,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) [A >= U] (?,1) 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) [B >= C && L = 0] (?,1) 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) [0 >= 1 + L] (?,1) 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) [L >= 1] (?,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) [C >= 1 + B && L = 0] (?,1) 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) [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) [U >= 1 + A] (?,1) 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->{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->{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: AddSinks + Details: () * Step 4: 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) [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) [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) [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) [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) [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) [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) [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) [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) [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) [29 >= J] (?,1) 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) [J >= 31] (?,1) 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) [J = 30] (?,1) 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) [K >= 0] (?,1) 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) [0 >= 1 + K] (?,1) 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) [C >= 1 + B] (?,1) 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) [B >= C] (?,1) 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) [B >= C && 0 >= 1 + Y] (?,1) 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) [B >= C && Y >= 1] (?,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) [A >= U] (?,1) 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) [B >= C && L = 0] (?,1) 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) [0 >= 1 + L] (?,1) 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) [L >= 1] (?,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) [C >= 1 + B && L = 0] (?,1) 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) [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) [U >= 1 + A] (?,1) 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) 30. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) Signature: {(exitus616,21) ;(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,30},26->{16,17,18,19},27->{},28->{3,27,30},29->{0,28},30->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(8,1),(8,2),(16,21),(17,22),(17,23),(17,24)] * Step 5: 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) [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) [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) [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) [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) [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) [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) [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) [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) [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) [29 >= J] (?,1) 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) [J >= 31] (?,1) 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) [J = 30] (?,1) 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) [K >= 0] (?,1) 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) [0 >= 1 + K] (?,1) 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) [C >= 1 + B] (?,1) 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) [B >= C] (?,1) 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) [B >= C && 0 >= 1 + Y] (?,1) 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) [B >= C && Y >= 1] (?,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) [A >= U] (?,1) 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) [B >= C && L = 0] (?,1) 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) [0 >= 1 + L] (?,1) 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) [L >= 1] (?,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) [C >= 1 + B && L = 0] (?,1) 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) [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) [U >= 1 + A] (?,1) 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) 30. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) Signature: {(exitus616,21) ;(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->{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,30},26->{16,17,18,19},27->{},28->{3,27,30},29->{0,28},30->{}] + Applied Processor: LooptreeTransformer + 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] | +- p:[0] c: [0] | `- p:[3,25,8,4,1,21,17,14,11,9,5,2,22,16,15,12,10,13,26,18,19,20,23,24,6,7] c: [20] | `- p:[1,21,17,14,11,9,4,2,22,16,15,12,10,5,3,25,8,23,24,6,7,13,26,18,19] c: [18] | `- p:[1,21,17,14,11,9,4,2,22,16,15,12,10,5,3,25,8,23,24,6,7,13,26,19] c: [19] | `- p:[1,21,17,14,11,9,4,2,22,16,15,12,10,5,3,25,8,23,24,6,7,13] c: [7] | `- p:[1,21,17,14,11,9,4,2,22,16,15,12,10,5,3,25,8,23,24,6,13] c: [6] | `- p:[1,21,17,14,11,9,4,2,22,16,15,12,10,5,3,25,8,23,24,13] c: [25] | `- p:[1,21,17,14,11,9,4,2,22,16,15,12,10,5,13,23,24] c: [] MAYBE