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