MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] (?,1) 3. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [1 + D >= E && E >= 2 + D && G = 0] (?,1) 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] (?,1) 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] (?,1) 10. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] (?,1) 11. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 12. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 13. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] (?,1) 15. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 16. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] (?,1) 17. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] (?,1) 19. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 21. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] (?,1) 22. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] (?,1) Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,3,4,5,6,21,22},1->{2,3,4,5,6,21,22},2->{2,3,4,5,6,21,22},3->{2,3,4,5,6,21,22},4->{2,3,4,5,6,21,22} ,5->{2,3,4,5,6,21,22},6->{7,8,9},7->{15,16},8->{15,16},9->{10,20},10->{10,20},11->{11,18,19},12->{7,8,9} ,13->{7,8,9},14->{7,8,9},15->{0,17},16->{0,17},17->{2,3,4,5,6,21,22},18->{12,13,14},19->{12,13,14},20->{11 ,18,19},21->{},22->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatRules MAYBE + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] (?,1) 3. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [1 + D >= E && E >= 2 + D && G = 0] (?,1) 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] (?,1) 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] (?,1) 10. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] (?,1) 11. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 12. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 13. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] (?,1) 15. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 16. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] (?,1) 17. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] (?,1) 19. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 21. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] (1,1) 22. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] (1,1) Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,3,4,5,6,21,22},1->{2,3,4,5,6,21,22},2->{2,3,4,5,6,21,22},3->{2,3,4,5,6,21,22},4->{2,3,4,5,6,21,22} ,5->{2,3,4,5,6,21,22},6->{7,8,9},7->{15,16},8->{15,16},9->{10,20},10->{10,20},11->{11,18,19},12->{7,8,9} ,13->{7,8,9},14->{7,8,9},15->{0,17},16->{0,17},17->{2,3,4,5,6,21,22},18->{12,13,14},19->{12,13,14},20->{11 ,18,19},21->{},22->{}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [3] * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] (?,1) 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] (?,1) 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] (?,1) 10. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] (?,1) 11. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 12. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 13. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] (?,1) 15. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 16. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] (?,1) 17. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] (?,1) 19. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 21. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] (1,1) 22. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] (1,1) Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,4,5,6,21,22},1->{2,4,5,6,21,22},2->{2,4,5,6,21,22},4->{2,4,5,6,21,22},5->{2,4,5,6,21,22},6->{7,8,9} ,7->{15,16},8->{15,16},9->{10,20},10->{10,20},11->{11,18,19},12->{7,8,9},13->{7,8,9},14->{7,8,9},15->{0,17} ,16->{0,17},17->{2,4,5,6,21,22},18->{12,13,14},19->{12,13,14},20->{11,18,19},21->{},22->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2) ,(1,4) ,(1,5) ,(1,21) ,(1,22) ,(2,2) ,(2,4) ,(2,5) ,(2,6) ,(2,21) ,(4,2) ,(4,4) ,(4,5) ,(4,6) ,(4,21) ,(5,2) ,(5,4) ,(5,5) ,(5,6) ,(5,21) ,(12,8) ,(12,9) ,(13,7) ,(13,9) ,(14,7) ,(14,8) ,(15,0) ,(19,12) ,(19,14)] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] (?,1) 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] (?,1) 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] (?,1) 10. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] (?,1) 11. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 12. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 13. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] (?,1) 15. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 16. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] (?,1) 17. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] (?,1) 19. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 21. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] (1,1) 22. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] (1,1) Signature: {(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,4,5,6,21,22},1->{6},2->{22},4->{22},5->{22},6->{7,8,9},7->{15,16},8->{15,16},9->{10,20},10->{10,20} ,11->{11,18,19},12->{7},13->{8},14->{9},15->{17},16->{0,17},17->{2,4,5,6,21,22},18->{12,13,14},19->{13} ,20->{11,18,19},21->{},22->{}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] (?,1) 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] (?,1) 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] (?,1) 10. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] (?,1) 11. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 12. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 13. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] (?,1) 15. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 16. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] (?,1) 17. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] (?,1) 19. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 21. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] (?,1) 22. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] (?,1) 23. f11(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True (?,1) Signature: {(exitus616,11);(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,4,5,6,21,22,23},1->{2,4,5,6,21,22,23},2->{2,4,5,6,21,22,23},4->{2,4,5,6,21,22,23},5->{2,4,5,6,21,22 ,23},6->{7,8,9},7->{15,16},8->{15,16},9->{10,20},10->{10,20},11->{11,18,19},12->{7,8,9},13->{7,8,9},14->{7,8 ,9},15->{0,17},16->{0,17},17->{2,4,5,6,21,22,23},18->{12,13,14},19->{12,13,14},20->{11,18,19},21->{},22->{} ,23->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2) ,(1,4) ,(1,5) ,(1,21) ,(1,22) ,(2,2) ,(2,4) ,(2,5) ,(2,6) ,(2,21) ,(4,2) ,(4,4) ,(4,5) ,(4,6) ,(4,21) ,(5,2) ,(5,4) ,(5,5) ,(5,6) ,(5,21) ,(12,8) ,(12,9) ,(13,7) ,(13,9) ,(14,7) ,(14,8) ,(15,0) ,(19,12) ,(19,14)] * Step 6: Failure MAYBE + Considered Problem: Rules: 0. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,G,H,I,J,K) [A >= 1 + B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,10,20,1,20,0,0,H,I,J,K) True (1,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,E,F,1,H,I,J,K) [D >= E && G = 0] (?,1) 4. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,H,I,J,K) [E = 1 + D && G = 0] (?,1) 5. f11(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,D,1 + D,F,1,N,I,J,K) [L >= 1 + M && E = 1 + D && G = 0] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K) -> f40(E,B,C,D,E,F,0,N,L,1 + D,M) [E >= 2 + D && G = 0] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K) -> f59(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 9. f40(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,0,G,H,I,1 + J,K) [F = 0] (?,1) 10. f43(A,B,C,D,E,F,G,H,I,J,K) -> f43(A,B,C,D,E,F,G,H,I,1 + J,K) [K >= 1 + N] (?,1) 11. f48(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 12. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + F] (?,1) 13. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,F,G,H,I,J,K) [F >= 1] (?,1) 14. f54(A,B,C,D,E,F,G,H,I,J,K) -> f40(A,B,C,D,E,0,G,N,I,J,K) [F = 0] (?,1) 15. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,E,F,G,H,I,J,K) [B >= 1 + A] (?,1) 16. f59(A,B,C,D,E,F,G,H,I,J,K) -> f63(A,B,C,D,-1 + A,F,G,H,I,J,K) [A >= B] (?,1) 17. f63(A,B,C,D,E,F,G,H,I,J,K) -> f11(A,B,C,J,E,F,G,H,I,J,K) [B >= A] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,F,G,H,I,J,K) [A >= J] (?,1) 19. f48(A,B,C,D,E,F,G,H,I,J,K) -> f54(A,B,C,D,E,1,G,H,I,J,K) [J >= 1 + A] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K) -> f48(-1 + A,B,C,D,E,F,G,H,I,J,K) True (?,1) 21. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [0 >= 1 + G] (?,1) 22. f11(A,B,C,D,E,F,G,H,I,J,K) -> f69(A,B,C,D,E,F,G,H,I,J,K) [G >= 1] (?,1) 23. f11(A,B,C,D,E,F,G,H,I,J,K) -> exitus616(A,B,C,D,E,F,G,H,I,J,K) True (?,1) Signature: {(exitus616,11);(f0,11);(f11,11);(f40,11);(f43,11);(f48,11);(f54,11);(f59,11);(f63,11);(f69,11)} Flow Graph: [0->{2,4,5,6,21,22,23},1->{6,23},2->{22,23},4->{22,23},5->{22,23},6->{7,8,9},7->{15,16},8->{15,16},9->{10 ,20},10->{10,20},11->{11,18,19},12->{7},13->{8},14->{9},15->{17},16->{0,17},17->{2,4,5,6,21,22,23},18->{12 ,13,14},19->{13},20->{11,18,19},21->{},22->{},23->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] | `- p:[0,16,7,6,17,15,8,13,18,11,20,9,14,10,19,12] c: [] MAYBE