NO * Step 1: UnsatPaths NO + 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: 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 2: UnreachableRules NO + 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},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 3: FromIts NO + 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) 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: FromIts + Details: () * Step 4: CloseWith NO + Considered Problem: Rules: 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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] 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 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] 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 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] 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] 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] 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] 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] 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)} Rule 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: CloseWith False + Details: () NO