MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f16(1,0,1,N,0,M,L,K,I,J) [K >= 0 && L >= K && L >= 0 && M >= L && N >= 0 && M >= 0] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,1 + E,F,G,H,0,J) [H >= 1 && 0 >= E && 0 >= D] (?,1) 2. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,E,F,G,H,N,J) [H >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 3. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,1 + B,C,D,E,F,G,H,1,J) [H >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 4. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,0,-1 + C,D,E,F,G,H,0,J) [H >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 5. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 6. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 7. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,-1 + D,E,F,G,H,N,J) [H >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 8. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,1 + E,F,G,H,I,0) [I >= 1 && 0 >= E && 0 >= D] (?,1) 9. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,E,F,G,H,I,N) [I >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 10. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,1 + B,C,D,E,F,G,H,I,1) [I >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 11. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,0,-1 + C,D,E,F,G,H,I,0) [I >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 12. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 13. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 14. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,-1 + D,E,F,G,H,I,N) [I >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 15. f25(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + F >= A && 0 >= I] (?,1) 16. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [J >= 1 && 1 + F >= A && H >= G] (?,1) 17. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,1 + H,I,J) [J >= 1 && 1 + F >= A && G >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,-1 + H,I,J) [1 + F >= A && 0 >= J] (?,1) 19. f16(A,B,C,D,E,F,G,H,I,J) -> f74(A,B,C,D,E,F,G,H,I,J) [0 >= H] (?,1) Signature: {(f0,10);(f16,10);(f25,10);(f50,10);(f74,10)} Flow Graph: [0->{1,2,3,4,5,6,7,19},1->{8,9,10,11,12,13,14,15},2->{8,9,10,11,12,13,14,15},3->{8,9,10,11,12,13,14,15} ,4->{8,9,10,11,12,13,14,15},5->{8,9,10,11,12,13,14,15},6->{8,9,10,11,12,13,14,15},7->{8,9,10,11,12,13,14,15} ,8->{16,17,18},9->{16,17,18},10->{16,17,18},11->{16,17,18},12->{16,17,18},13->{16,17,18},14->{16,17,18} ,15->{1,2,3,4,5,6,7,19},16->{1,2,3,4,5,6,7,19},17->{1,2,3,4,5,6,7,19},18->{1,2,3,4,5,6,7,19},19->{}] + 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) -> f16(1,0,1,N,0,M,L,K,I,J) [K >= 0 && L >= K && L >= 0 && M >= L && N >= 0 && M >= 0] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,1 + E,F,G,H,0,J) [H >= 1 && 0 >= E && 0 >= D] (?,1) 2. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,E,F,G,H,N,J) [H >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 3. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,1 + B,C,D,E,F,G,H,1,J) [H >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 4. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,0,-1 + C,D,E,F,G,H,0,J) [H >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 5. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 6. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 7. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,-1 + D,E,F,G,H,N,J) [H >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 8. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,1 + E,F,G,H,I,0) [I >= 1 && 0 >= E && 0 >= D] (?,1) 9. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,E,F,G,H,I,N) [I >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 10. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,1 + B,C,D,E,F,G,H,I,1) [I >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 11. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,0,-1 + C,D,E,F,G,H,I,0) [I >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 12. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 13. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 14. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,-1 + D,E,F,G,H,I,N) [I >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 15. f25(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + F >= A && 0 >= I] (?,1) 16. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [J >= 1 && 1 + F >= A && H >= G] (?,1) 17. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,1 + H,I,J) [J >= 1 && 1 + F >= A && G >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,-1 + H,I,J) [1 + F >= A && 0 >= J] (?,1) 19. f16(A,B,C,D,E,F,G,H,I,J) -> f74(A,B,C,D,E,F,G,H,I,J) [0 >= H] (1,1) Signature: {(f0,10);(f16,10);(f25,10);(f50,10);(f74,10)} Flow Graph: [0->{1,2,3,4,5,6,7,19},1->{8,9,10,11,12,13,14,15},2->{8,9,10,11,12,13,14,15},3->{8,9,10,11,12,13,14,15} ,4->{8,9,10,11,12,13,14,15},5->{8,9,10,11,12,13,14,15},6->{8,9,10,11,12,13,14,15},7->{8,9,10,11,12,13,14,15} ,8->{16,17,18},9->{16,17,18},10->{16,17,18},11->{16,17,18},12->{16,17,18},13->{16,17,18},14->{16,17,18} ,15->{1,2,3,4,5,6,7,19},16->{1,2,3,4,5,6,7,19},17->{1,2,3,4,5,6,7,19},18->{1,2,3,4,5,6,7,19},19->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2) ,(0,3) ,(0,4) ,(0,5) ,(0,6) ,(1,8) ,(1,9) ,(1,10) ,(1,11) ,(1,12) ,(1,13) ,(1,14) ,(2,8) ,(2,10) ,(2,11) ,(2,12) ,(2,13) ,(2,14) ,(3,8) ,(3,9) ,(3,12) ,(3,14) ,(3,15) ,(4,8) ,(4,9) ,(4,10) ,(4,11) ,(4,12) ,(4,13) ,(4,14) ,(5,9) ,(5,10) ,(5,11) ,(5,12) ,(5,13) ,(6,9) ,(6,10) ,(6,11) ,(6,12) ,(6,13) ,(8,16) ,(8,17) ,(10,18) ,(11,16) ,(11,17)] * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f16(1,0,1,N,0,M,L,K,I,J) [K >= 0 && L >= K && L >= 0 && M >= L && N >= 0 && M >= 0] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,1 + E,F,G,H,0,J) [H >= 1 && 0 >= E && 0 >= D] (?,1) 2. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,E,F,G,H,N,J) [H >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 3. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,1 + B,C,D,E,F,G,H,1,J) [H >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 4. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,0,-1 + C,D,E,F,G,H,0,J) [H >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 5. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 6. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 7. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,-1 + D,E,F,G,H,N,J) [H >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 8. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,1 + E,F,G,H,I,0) [I >= 1 && 0 >= E && 0 >= D] (?,1) 9. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,E,F,G,H,I,N) [I >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 10. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,1 + B,C,D,E,F,G,H,I,1) [I >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 11. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,0,-1 + C,D,E,F,G,H,I,0) [I >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 12. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 13. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 14. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,-1 + D,E,F,G,H,I,N) [I >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 15. f25(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + F >= A && 0 >= I] (?,1) 16. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [J >= 1 && 1 + F >= A && H >= G] (?,1) 17. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,1 + H,I,J) [J >= 1 && 1 + F >= A && G >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,-1 + H,I,J) [1 + F >= A && 0 >= J] (?,1) 19. f16(A,B,C,D,E,F,G,H,I,J) -> f74(A,B,C,D,E,F,G,H,I,J) [0 >= H] (1,1) Signature: {(f0,10);(f16,10);(f25,10);(f50,10);(f74,10)} Flow Graph: [0->{1,7,19},1->{15},2->{9,15},3->{10,11,13},4->{15},5->{8,14,15},6->{8,14,15},7->{8,9,10,11,12,13,14,15} ,8->{18},9->{16,17,18},10->{16,17},11->{18},12->{16,17,18},13->{16,17,18},14->{16,17,18},15->{1,2,3,4,5,6,7 ,19},16->{1,2,3,4,5,6,7,19},17->{1,2,3,4,5,6,7,19},18->{1,2,3,4,5,6,7,19},19->{}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f16(1,0,1,N,0,M,L,K,I,J) [K >= 0 && L >= K && L >= 0 && M >= L && N >= 0 && M >= 0] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,1 + E,F,G,H,0,J) [H >= 1 && 0 >= E && 0 >= D] (?,1) 2. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,E,F,G,H,N,J) [H >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 3. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,1 + B,C,D,E,F,G,H,1,J) [H >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 4. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,0,-1 + C,D,E,F,G,H,0,J) [H >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 5. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 6. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 7. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,-1 + D,E,F,G,H,N,J) [H >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 8. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,1 + E,F,G,H,I,0) [I >= 1 && 0 >= E && 0 >= D] (?,1) 9. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,E,F,G,H,I,N) [I >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 10. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,1 + B,C,D,E,F,G,H,I,1) [I >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 11. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,0,-1 + C,D,E,F,G,H,I,0) [I >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 12. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 13. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 14. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,-1 + D,E,F,G,H,I,N) [I >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 15. f25(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + F >= A && 0 >= I] (?,1) 16. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [J >= 1 && 1 + F >= A && H >= G] (?,1) 17. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,1 + H,I,J) [J >= 1 && 1 + F >= A && G >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,-1 + H,I,J) [1 + F >= A && 0 >= J] (?,1) 19. f16(A,B,C,D,E,F,G,H,I,J) -> f74(A,B,C,D,E,F,G,H,I,J) [0 >= H] (?,1) 20. f16(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) Signature: {(exitus616,10);(f0,10);(f16,10);(f25,10);(f50,10);(f74,10)} Flow Graph: [0->{1,2,3,4,5,6,7,19,20},1->{8,9,10,11,12,13,14,15},2->{8,9,10,11,12,13,14,15},3->{8,9,10,11,12,13,14,15} ,4->{8,9,10,11,12,13,14,15},5->{8,9,10,11,12,13,14,15},6->{8,9,10,11,12,13,14,15},7->{8,9,10,11,12,13,14,15} ,8->{16,17,18},9->{16,17,18},10->{16,17,18},11->{16,17,18},12->{16,17,18},13->{16,17,18},14->{16,17,18} ,15->{1,2,3,4,5,6,7,19,20},16->{1,2,3,4,5,6,7,19,20},17->{1,2,3,4,5,6,7,19,20},18->{1,2,3,4,5,6,7,19,20} ,19->{},20->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2) ,(0,3) ,(0,4) ,(0,5) ,(0,6) ,(1,8) ,(1,9) ,(1,10) ,(1,11) ,(1,12) ,(1,13) ,(1,14) ,(2,8) ,(2,10) ,(2,11) ,(2,12) ,(2,13) ,(2,14) ,(3,8) ,(3,9) ,(3,12) ,(3,14) ,(3,15) ,(4,8) ,(4,9) ,(4,10) ,(4,11) ,(4,12) ,(4,13) ,(4,14) ,(5,9) ,(5,10) ,(5,11) ,(5,12) ,(5,13) ,(6,9) ,(6,10) ,(6,11) ,(6,12) ,(6,13) ,(8,16) ,(8,17) ,(10,18) ,(11,16) ,(11,17)] * Step 5: Failure MAYBE + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J) -> f16(1,0,1,N,0,M,L,K,I,J) [K >= 0 && L >= K && L >= 0 && M >= L && N >= 0 && M >= 0] (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,1 + E,F,G,H,0,J) [H >= 1 && 0 >= E && 0 >= D] (?,1) 2. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,D,E,F,G,H,N,J) [H >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 3. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,1 + B,C,D,E,F,G,H,1,J) [H >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 4. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,0,-1 + C,D,E,F,G,H,0,J) [H >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 5. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 6. f16(A,B,C,D,E,F,G,H,I,J) -> f25(1 + A,0,1 + A,N,0,F,G,H,M,J) [H >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 7. f16(A,B,C,D,E,F,G,H,I,J) -> f25(A,B,C,-1 + D,E,F,G,H,N,J) [H >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 8. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,1 + E,F,G,H,I,0) [I >= 1 && 0 >= E && 0 >= D] (?,1) 9. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,D,E,F,G,H,I,N) [I >= 1 && E >= 2 && 0 >= D && 1 >= N && N >= 0] (?,1) 10. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,1 + B,C,D,E,F,G,H,I,1) [I >= 1 && 0 >= D && 0 >= B && E = 1] (?,1) 11. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,0,-1 + C,D,E,F,G,H,I,0) [I >= 1 && 0 >= D && C >= 1 && E = 1 && B = 1] (?,1) 12. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && M >= 0 && 1 >= M && B >= 2 && N >= 0 && E = 1] (?,1) 13. f25(A,B,C,D,E,F,G,H,I,J) -> f50(1 + A,0,1 + A,N,0,F,G,H,I,M) [I >= 1 && 0 >= D && 0 >= C && M >= 0 && 1 >= M && N >= 0 && E = 1 && B = 1] (?,1) 14. f25(A,B,C,D,E,F,G,H,I,J) -> f50(A,B,C,-1 + D,E,F,G,H,I,N) [I >= 1 && D >= 1 && 1 >= N && N >= 0] (?,1) 15. f25(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [1 + F >= A && 0 >= I] (?,1) 16. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,H,I,J) [J >= 1 && 1 + F >= A && H >= G] (?,1) 17. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,1 + H,I,J) [J >= 1 && 1 + F >= A && G >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J) -> f16(A,B,C,D,E,F,G,-1 + H,I,J) [1 + F >= A && 0 >= J] (?,1) 19. f16(A,B,C,D,E,F,G,H,I,J) -> f74(A,B,C,D,E,F,G,H,I,J) [0 >= H] (?,1) 20. f16(A,B,C,D,E,F,G,H,I,J) -> exitus616(A,B,C,D,E,F,G,H,I,J) True (?,1) Signature: {(exitus616,10);(f0,10);(f16,10);(f25,10);(f50,10);(f74,10)} Flow Graph: [0->{1,7,19,20},1->{15},2->{9,15},3->{10,11,13},4->{15},5->{8,14,15},6->{8,14,15},7->{8,9,10,11,12,13,14 ,15},8->{18},9->{16,17,18},10->{16,17},11->{18},12->{16,17,18},13->{16,17,18},14->{16,17,18},15->{1,2,3,4,5 ,6,7,19,20},16->{1,2,3,4,5,6,7,19,20},17->{1,2,3,4,5,6,7,19,20},18->{1,2,3,4,5,6,7,19,20},19->{},20->{}] + 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] | `- p:[1,15,2,16,9,7,17,10,3,18,8,5,6,11,12,13,14,4] c: [] MAYBE