MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + A] (?,1) 1. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [A >= 1] (?,1) 2. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,1,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D = 0 && A = 0] (?,1) 3. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + D && A = 0] (?,1) 4. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D >= 1 && A = 0] (?,1) 5. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [C >= E] (?,1) 6. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 8. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,0,0,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [E >= 1 + C] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 1 + J = 0] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 2 + J] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && J >= 0] (?,1) 13. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (?,1) 14. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 15. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 16. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,0,W,O,P,Q,R,S,T,U,V) [M = 0] (?,1) 17. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,0,0,M,W,O,P,Q,R,S,T,U,V) [I >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && 0 >= W && O = 3] (?,1) 19. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && W >= 2 && O = 3] (?,1) 20. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && 2 >= O] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && O >= 4] (?,1) 22. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,P,1,W,S,T,U,V) [N >= 0 && O = 3] (?,1) 23. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,R,S,T,U,V) [10 >= R] (?,1) 24. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,10,S,T,U,V) [R >= 11] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 26. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 27. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 28. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 29. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + M] (?,1) 30. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [M >= 1] (?,1) 31. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 32. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 33. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,K,K,L,M,N,O,P,Q,R,1 + S,T,U,V) [N >= 0] (?,1) 34. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 35. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,T,U,V) [S = 0] (?,1) 36. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 37. f73(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 38. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + S] (?,1) 39. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [S >= 1] (?,1) 40. f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 41. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,3,1,Y) [X >= 0 && Y >= 1 && T = 3] (1,1) 42. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [2 >= T && X >= 0 && Y >= 1] (1,1) 43. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [T >= 4 && X >= 0 && Y >= 1] (1,1) Signature: {(f0,22) ;(f20,22) ;(f26,22) ;(f33,22) ;(f39,22) ;(f47,22) ;(f50,22) ;(f59,22) ;(f62,22) ;(f69,22) ;(f71,22) ;(f73,22) ;(f74,22) ;(f76,22) ;(f78,22)} Flow Graph: [0->{5,6,7,8,25,26},1->{5,6,7,8,25,26},2->{5,6,7,8,25,26},3->{5,6,7,8,25,26},4->{5,6,7,8,25,26},5->{35,38 ,39},6->{9,10,11,12},7->{9,10,11,12},8->{9,10,11,12},9->{13,14,15,17,27,28},10->{13,14,15,17,27,28},11->{9 ,10,11,12},12->{9,10,11,12},13->{35,38,39},14->{16,29,30},15->{16,29,30},16->{18,19,20,21,22,31},17->{18,19 ,20,21,22,31},18->{35,38,39},19->{35,38,39},20->{23,24},21->{23,24},22->{23,24},23->{32,33},24->{32,33} ,25->{5,6,7,8,25,26},26->{5,6,7,8,25,26},27->{5,6,7,8,25,26},28->{5,6,7,8,25,26},29->{5,6,7,8,25,26},30->{5 ,6,7,8,25,26},31->{5,6,7,8,25,26},32->{5,6,7,8,25,26},33->{5,6,7,8,25,26},34->{34},35->{34},36->{36} ,37->{36},38->{36},39->{36},40->{},41->{0,1,2,3,4},42->{0,1,2,3,4},43->{0,1,2,3,4}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + A] (1,1) 1. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [A >= 1] (1,1) 2. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,1,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D = 0 && A = 0] (1,1) 3. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + D && A = 0] (1,1) 4. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D >= 1 && A = 0] (1,1) 5. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [C >= E] (1,1) 6. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 8. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,0,0,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [E >= 1 + C] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 1 + J = 0] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 2 + J] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && J >= 0] (?,1) 13. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (1,1) 14. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 15. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 16. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,0,W,O,P,Q,R,S,T,U,V) [M = 0] (?,1) 17. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,0,0,M,W,O,P,Q,R,S,T,U,V) [I >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && 0 >= W && O = 3] (1,1) 19. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && W >= 2 && O = 3] (1,1) 20. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && 2 >= O] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && O >= 4] (?,1) 22. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,P,1,W,S,T,U,V) [N >= 0 && O = 3] (?,1) 23. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,R,S,T,U,V) [10 >= R] (?,1) 24. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,10,S,T,U,V) [R >= 11] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 26. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 27. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 28. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 29. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + M] (?,1) 30. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [M >= 1] (?,1) 31. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 32. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 33. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,K,K,L,M,N,O,P,Q,R,1 + S,T,U,V) [N >= 0] (?,1) 34. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 35. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,T,U,V) [S = 0] (1,1) 36. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 37. f73(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (1,1) 38. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + S] (1,1) 39. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [S >= 1] (1,1) 40. f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (1,1) 41. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,3,1,Y) [X >= 0 && Y >= 1 && T = 3] (1,1) 42. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [2 >= T && X >= 0 && Y >= 1] (1,1) 43. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [T >= 4 && X >= 0 && Y >= 1] (1,1) Signature: {(f0,22) ;(f20,22) ;(f26,22) ;(f33,22) ;(f39,22) ;(f47,22) ;(f50,22) ;(f59,22) ;(f62,22) ;(f69,22) ;(f71,22) ;(f73,22) ;(f74,22) ;(f76,22) ;(f78,22)} Flow Graph: [0->{5,6,7,8,25,26},1->{5,6,7,8,25,26},2->{5,6,7,8,25,26},3->{5,6,7,8,25,26},4->{5,6,7,8,25,26},5->{35,38 ,39},6->{9,10,11,12},7->{9,10,11,12},8->{9,10,11,12},9->{13,14,15,17,27,28},10->{13,14,15,17,27,28},11->{9 ,10,11,12},12->{9,10,11,12},13->{35,38,39},14->{16,29,30},15->{16,29,30},16->{18,19,20,21,22,31},17->{18,19 ,20,21,22,31},18->{35,38,39},19->{35,38,39},20->{23,24},21->{23,24},22->{23,24},23->{32,33},24->{32,33} ,25->{5,6,7,8,25,26},26->{5,6,7,8,25,26},27->{5,6,7,8,25,26},28->{5,6,7,8,25,26},29->{5,6,7,8,25,26},30->{5 ,6,7,8,25,26},31->{5,6,7,8,25,26},32->{5,6,7,8,25,26},33->{5,6,7,8,25,26},34->{34},35->{34},36->{36} ,37->{36},38->{36},39->{36},40->{},41->{0,1,2,3,4},42->{0,1,2,3,4},43->{0,1,2,3,4}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,14) ,(9,15) ,(9,17) ,(9,27) ,(9,28) ,(10,13) ,(11,10) ,(11,12) ,(12,10) ,(12,11) ,(41,3) ,(42,3) ,(43,3)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + A] (1,1) 1. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [A >= 1] (1,1) 2. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,1,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D = 0 && A = 0] (1,1) 3. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + D && A = 0] (1,1) 4. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D >= 1 && A = 0] (1,1) 5. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [C >= E] (1,1) 6. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 8. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,0,0,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [E >= 1 + C] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 1 + J = 0] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 2 + J] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && J >= 0] (?,1) 13. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (1,1) 14. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 15. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 16. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,0,W,O,P,Q,R,S,T,U,V) [M = 0] (?,1) 17. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,0,0,M,W,O,P,Q,R,S,T,U,V) [I >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && 0 >= W && O = 3] (1,1) 19. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && W >= 2 && O = 3] (1,1) 20. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && 2 >= O] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && O >= 4] (?,1) 22. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,P,1,W,S,T,U,V) [N >= 0 && O = 3] (?,1) 23. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,R,S,T,U,V) [10 >= R] (?,1) 24. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,10,S,T,U,V) [R >= 11] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 26. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 27. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 28. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 29. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + M] (?,1) 30. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [M >= 1] (?,1) 31. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 32. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 33. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,K,K,L,M,N,O,P,Q,R,1 + S,T,U,V) [N >= 0] (?,1) 34. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 35. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,T,U,V) [S = 0] (1,1) 36. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 37. f73(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (1,1) 38. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + S] (1,1) 39. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [S >= 1] (1,1) 40. f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (1,1) 41. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,3,1,Y) [X >= 0 && Y >= 1 && T = 3] (1,1) 42. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [2 >= T && X >= 0 && Y >= 1] (1,1) 43. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [T >= 4 && X >= 0 && Y >= 1] (1,1) Signature: {(f0,22) ;(f20,22) ;(f26,22) ;(f33,22) ;(f39,22) ;(f47,22) ;(f50,22) ;(f59,22) ;(f62,22) ;(f69,22) ;(f71,22) ;(f73,22) ;(f74,22) ;(f76,22) ;(f78,22)} Flow Graph: [0->{5,6,7,8,25,26},1->{5,6,7,8,25,26},2->{5,6,7,8,25,26},3->{5,6,7,8,25,26},4->{5,6,7,8,25,26},5->{35,38 ,39},6->{9,10,11,12},7->{9,10,11,12},8->{9,10,11,12},9->{13},10->{14,15,17,27,28},11->{9,11},12->{9,12} ,13->{35,38,39},14->{16,29,30},15->{16,29,30},16->{18,19,20,21,22,31},17->{18,19,20,21,22,31},18->{35,38,39} ,19->{35,38,39},20->{23,24},21->{23,24},22->{23,24},23->{32,33},24->{32,33},25->{5,6,7,8,25,26},26->{5,6,7,8 ,25,26},27->{5,6,7,8,25,26},28->{5,6,7,8,25,26},29->{5,6,7,8,25,26},30->{5,6,7,8,25,26},31->{5,6,7,8,25,26} ,32->{5,6,7,8,25,26},33->{5,6,7,8,25,26},34->{34},35->{34},36->{36},37->{36},38->{36},39->{36},40->{},41->{0 ,1,2,4},42->{0,1,2,4},43->{0,1,2,4}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [3,37,40] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + A] (1,1) 1. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [A >= 1] (1,1) 2. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,1,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D = 0 && A = 0] (1,1) 4. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D >= 1 && A = 0] (1,1) 5. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [C >= E] (1,1) 6. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 8. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,0,0,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [E >= 1 + C] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 1 + J = 0] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 2 + J] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && J >= 0] (?,1) 13. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (1,1) 14. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 15. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 16. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,0,W,O,P,Q,R,S,T,U,V) [M = 0] (?,1) 17. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,0,0,M,W,O,P,Q,R,S,T,U,V) [I >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && 0 >= W && O = 3] (1,1) 19. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && W >= 2 && O = 3] (1,1) 20. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && 2 >= O] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && O >= 4] (?,1) 22. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,P,1,W,S,T,U,V) [N >= 0 && O = 3] (?,1) 23. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,R,S,T,U,V) [10 >= R] (?,1) 24. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,10,S,T,U,V) [R >= 11] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 26. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 27. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 28. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 29. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + M] (?,1) 30. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [M >= 1] (?,1) 31. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 32. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 33. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,K,K,L,M,N,O,P,Q,R,1 + S,T,U,V) [N >= 0] (?,1) 34. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 35. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,T,U,V) [S = 0] (1,1) 36. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 38. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + S] (1,1) 39. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [S >= 1] (1,1) 41. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,3,1,Y) [X >= 0 && Y >= 1 && T = 3] (1,1) 42. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [2 >= T && X >= 0 && Y >= 1] (1,1) 43. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [T >= 4 && X >= 0 && Y >= 1] (1,1) Signature: {(f0,22) ;(f20,22) ;(f26,22) ;(f33,22) ;(f39,22) ;(f47,22) ;(f50,22) ;(f59,22) ;(f62,22) ;(f69,22) ;(f71,22) ;(f73,22) ;(f74,22) ;(f76,22) ;(f78,22)} Flow Graph: [0->{5,6,7,8,25,26},1->{5,6,7,8,25,26},2->{5,6,7,8,25,26},4->{5,6,7,8,25,26},5->{35,38,39},6->{9,10,11,12} ,7->{9,10,11,12},8->{9,10,11,12},9->{13},10->{14,15,17,27,28},11->{9,11},12->{9,12},13->{35,38,39},14->{16 ,29,30},15->{16,29,30},16->{18,19,20,21,22,31},17->{18,19,20,21,22,31},18->{35,38,39},19->{35,38,39},20->{23 ,24},21->{23,24},22->{23,24},23->{32,33},24->{32,33},25->{5,6,7,8,25,26},26->{5,6,7,8,25,26},27->{5,6,7,8,25 ,26},28->{5,6,7,8,25,26},29->{5,6,7,8,25,26},30->{5,6,7,8,25,26},31->{5,6,7,8,25,26},32->{5,6,7,8,25,26} ,33->{5,6,7,8,25,26},34->{34},35->{34},36->{36},38->{36},39->{36},41->{0,1,2,4},42->{0,1,2,4},43->{0,1,2,4}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + A] (?,1) 1. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [A >= 1] (?,1) 2. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,1,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D = 0 && A = 0] (?,1) 4. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D >= 1 && A = 0] (?,1) 5. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [C >= E] (?,1) 6. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 8. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,0,0,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [E >= 1 + C] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 1 + J = 0] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 2 + J] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && J >= 0] (?,1) 13. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (?,1) 14. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 15. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 16. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,0,W,O,P,Q,R,S,T,U,V) [M = 0] (?,1) 17. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,0,0,M,W,O,P,Q,R,S,T,U,V) [I >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && 0 >= W && O = 3] (?,1) 19. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && W >= 2 && O = 3] (?,1) 20. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && 2 >= O] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && O >= 4] (?,1) 22. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,P,1,W,S,T,U,V) [N >= 0 && O = 3] (?,1) 23. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,R,S,T,U,V) [10 >= R] (?,1) 24. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,10,S,T,U,V) [R >= 11] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 26. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 27. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 28. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 29. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + M] (?,1) 30. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [M >= 1] (?,1) 31. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 32. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 33. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,K,K,L,M,N,O,P,Q,R,1 + S,T,U,V) [N >= 0] (?,1) 34. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 35. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,T,U,V) [S = 0] (?,1) 36. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 38. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + S] (?,1) 39. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [S >= 1] (?,1) 41. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,3,1,Y) [X >= 0 && Y >= 1 && T = 3] (1,1) 42. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [2 >= T && X >= 0 && Y >= 1] (1,1) 43. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [T >= 4 && X >= 0 && Y >= 1] (1,1) 44. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 45. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) Signature: {(exitus616,22) ;(f0,22) ;(f20,22) ;(f26,22) ;(f33,22) ;(f39,22) ;(f47,22) ;(f50,22) ;(f59,22) ;(f62,22) ;(f69,22) ;(f71,22) ;(f73,22) ;(f74,22) ;(f76,22) ;(f78,22)} Flow Graph: [0->{5,6,7,8,25,26},1->{5,6,7,8,25,26},2->{5,6,7,8,25,26},4->{5,6,7,8,25,26},5->{35,38,39},6->{9,10,11,12} ,7->{9,10,11,12},8->{9,10,11,12},9->{13,14,15,17,27,28},10->{13,14,15,17,27,28},11->{9,10,11,12},12->{9,10 ,11,12},13->{35,38,39},14->{16,29,30},15->{16,29,30},16->{18,19,20,21,22,31},17->{18,19,20,21,22,31},18->{35 ,38,39},19->{35,38,39},20->{23,24},21->{23,24},22->{23,24},23->{32,33},24->{32,33},25->{5,6,7,8,25,26} ,26->{5,6,7,8,25,26},27->{5,6,7,8,25,26},28->{5,6,7,8,25,26},29->{5,6,7,8,25,26},30->{5,6,7,8,25,26},31->{5 ,6,7,8,25,26},32->{5,6,7,8,25,26},33->{5,6,7,8,25,26},34->{34,45},35->{34,45},36->{36,44},38->{36,44} ,39->{36,44},41->{0,1,2,4},42->{0,1,2,4},43->{0,1,2,4},44->{},45->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,14) ,(9,15) ,(9,17) ,(9,27) ,(9,28) ,(10,13) ,(11,10) ,(11,12) ,(12,10) ,(12,11)] * Step 6: Failure MAYBE + Considered Problem: Rules: 0. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + A] (?,1) 1. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [A >= 1] (?,1) 2. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,1,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D = 0 && A = 0] (?,1) 4. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(0,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [D >= 1 && A = 0] (?,1) 5. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [C >= E] (?,1) 6. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,W,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 8. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,0,0,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [E >= 1 + C] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (?,1) 10. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 1 + J = 0] (?,1) 11. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 2 + J] (?,1) 12. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f33(A,B,C,D,E,F,G,1 + H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && J >= 0] (?,1) 13. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [H >= I] (?,1) 14. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 15. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f47(A,B,C,D,E,F,G,H,I,J,0,W,X,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 16. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,0,W,O,P,Q,R,S,T,U,V) [M = 0] (?,1) 17. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f50(A,B,C,D,E,F,G,H,I,J,0,0,M,W,O,P,Q,R,S,T,U,V) [I >= 1 + H] (?,1) 18. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && 0 >= W && O = 3] (?,1) 19. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,1,W,R,S,T,U,V) [N >= 0 && W >= 2 && O = 3] (?,1) 20. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && 2 >= O] (?,1) 21. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,W,S,T,U,V) [N >= 0 && O >= 4] (?,1) 22. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,3,P,1,W,S,T,U,V) [N >= 0 && O = 3] (?,1) 23. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,R,S,T,U,V) [10 >= R] (?,1) 24. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f62(A,B,C,D,E,F,G,H,I,J,K,L,M,W,O,P,Q,10,S,T,U,V) [R >= 11] (?,1) 25. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + W && E >= 1 + C] (?,1) 26. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,0,W,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [W >= 1 && E >= 1 + C] (?,1) 27. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && 0 >= 1 + W] (?,1) 28. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,W,L,M,N,O,P,Q,R,S,T,U,V) [I >= 1 + H && W >= 1] (?,1) 29. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + M] (?,1) 30. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [M >= 1] (?,1) 31. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 32. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,1,Q,R,S,T,U,V) [0 >= 1 + N] (?,1) 33. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f26(A,B,1 + C,D,E,F,G,H,I,K,K,L,M,N,O,P,Q,R,1 + S,T,U,V) [N >= 0] (?,1) 34. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 35. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,0,T,U,V) [S = 0] (?,1) 36. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 38. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [0 >= 1 + S] (?,1) 39. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f74(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [S >= 1] (?,1) 41. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,3,1,Y) [X >= 0 && Y >= 1 && T = 3] (1,1) 42. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [2 >= T && X >= 0 && Y >= 1] (1,1) 43. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f20(Z,B,C,X,W,F,G,0,I,J,K,L,M,N,O,P,Q,R,0,T,1,Y) [T >= 4 && X >= 0 && Y >= 1] (1,1) 44. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 45. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) Signature: {(exitus616,22) ;(f0,22) ;(f20,22) ;(f26,22) ;(f33,22) ;(f39,22) ;(f47,22) ;(f50,22) ;(f59,22) ;(f62,22) ;(f69,22) ;(f71,22) ;(f73,22) ;(f74,22) ;(f76,22) ;(f78,22)} Flow Graph: [0->{5,6,7,8,25,26},1->{5,6,7,8,25,26},2->{5,6,7,8,25,26},4->{5,6,7,8,25,26},5->{35,38,39},6->{9,10,11,12} ,7->{9,10,11,12},8->{9,10,11,12},9->{13},10->{14,15,17,27,28},11->{9,11},12->{9,12},13->{35,38,39},14->{16 ,29,30},15->{16,29,30},16->{18,19,20,21,22,31},17->{18,19,20,21,22,31},18->{35,38,39},19->{35,38,39},20->{23 ,24},21->{23,24},22->{23,24},23->{32,33},24->{32,33},25->{5,6,7,8,25,26},26->{5,6,7,8,25,26},27->{5,6,7,8,25 ,26},28->{5,6,7,8,25,26},29->{5,6,7,8,25,26},30->{5,6,7,8,25,26},31->{5,6,7,8,25,26},32->{5,6,7,8,25,26} ,33->{5,6,7,8,25,26},34->{34,45},35->{34,45},36->{36,44},38->{36,44},39->{36,44},41->{0,1,2,4},42->{0,1,2,4} ,43->{0,1,2,4},44->{},45->{}] + 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,24,25,26,27,28,29,30,31,32,33,34,35,36,38,39,41,42,43,44,45] | +- p:[6,25,26,27,10,7,28,29,14,15,30,31,16,17,32,23,20,21,22,24,33,8] c: [25,26] | | | `- p:[6,27,10,7,28,29,14,15,30,31,16,17,32,23,20,21,22,24,33,8] c: [7] | | | `- p:[6,27,10,8,28,29,14,15,30,31,16,17,32,23,20,21,22,24,33] c: [8] | | | `- p:[6,27,10,28,29,14,15,30,31,16,17,32,23,20,21,22,24,33] c: [6] | +- p:[12] c: [12] | +- p:[11] c: [11] | +- p:[36] c: [] | `- p:[34] c: [] MAYBE