YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(0,0,2*D,D,4*D,3 + 4*D,4 + 4*D,D,B1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= J] (?,1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C1 >= 2 && C >= J] (?,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= C1 && C >= J] (?,1) 4. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 5. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 6. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [N >= O] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= 1 + P && 0 >= Q] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [P >= 1 && 0 >= Q] (?,1) 9. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 10. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 11. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f57(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 12. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= Q && P = 0] (?,1) 13. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= J] (?,1) 14. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,2*J,B1,1 + -1*B1,U,V,W,X,Y,Z,A1) [C >= J] (?,1) 15. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [L = 0] (?,1) 16. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,B1,V,W,X,Y,Z,A1) [0 >= 1 + L] (?,1) 17. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,B1,V,W,X,Y,Z,A1) [L >= 1] (?,1) 18. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J,S,T,U,0,W,X,Y,Z,A1) [D >= J] (?,1) 19. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J,S,T,U,C1,W,X,Y,Z,A1) [0 >= 1 + D1 && D >= J] (?,1) 20. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J,S,T,U,C1,W,X,Y,Z,A1) [D1 >= 1 && D >= J] (?,1) 21. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,0,X,Y,Z,A1) [L = 0] (?,1) 22. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,C1,X,Y,Z,A1) [0 >= 1 + L] (?,1) 23. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,C1,X,Y,Z,A1) [L >= 1] (?,1) 24. f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,0,Y,Z,A1) [L = 0] (?,1) 25. f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,C1,Y,Z,A1) [0 >= 1 + L] (?,1) 26. f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,C1,Y,Z,A1) [L >= 1] (?,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,0,M,N,O,P,Q,R,S,T,U,V,W,X,0,Z,A1) [L = 0] (?,1) 28. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,B1,Z,A1) [0 >= 1 + L] (?,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,B1,Z,A1) [L >= 1] (?,1) 30. f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 31. f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 32. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,A + B,C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 33. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [J >= 1 + C] (?,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,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,C1,A1) [0 >= 1 + D1 && J >= 1 + C] (?,1) 35. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,C1,A1) [D1 >= 1 && J >= 1 + C] (?,1) 36. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + E] (?,1) 37. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 38. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,C + Q) [J >= 1 + D] (?,1) 39. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 40. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [Q >= 1] (?,1) 41. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [O >= 1 + N] (?,1) 42. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 43. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= 1 + P && J >= 1 + D] (?,1) 44. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [P >= 1 && J >= 1 + D] (?,1) 45. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D && P = 0] (?,1) 46. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + C] (?,1) Signature: {(f1,27) ;(f103,27) ;(f107,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27) ;(f99,27)} Flow Graph: [0->{1,2,3,46},1->{1,2,3,46},2->{1,2,3,46},3->{1,2,3,46},4->{4,43,44,45},5->{5,42},6->{7,8,12,40},7->{9 ,39},8->{9,39},9->{9,39},10->{10,38},11->{11,37},12->{13,36},13->{13,36},14->{14,33,34,35},15->{18,19,20,32} ,16->{18,19,20,32},17->{18,19,20,32},18->{21,22,23},19->{21,22,23},20->{21,22,23},21->{24,25,26},22->{24,25 ,26},23->{24,25,26},24->{27,28,29},25->{27,28,29},26->{27,28,29},27->{18,19,20,32},28->{18,19,20,32},29->{18 ,19,20,32},30->{30,31},31->{},32->{6,41},33->{15,16,17},34->{15,16,17},35->{15,16,17},36->{7,8,12,40},37->{7 ,8,12,40},38->{11,37},39->{10,38},40->{14,33,34,35},41->{30,31},42->{6,41},43->{5,42},44->{5,42},45->{6,41} ,46->{4,43,44,45}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(38,11),(39,10),(43,5),(44,5)] * Step 2: UnreachableRules YES + Considered Problem: Rules: 0. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(0,0,2*D,D,4*D,3 + 4*D,4 + 4*D,D,B1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= J] (?,1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C1 >= 2 && C >= J] (?,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= C1 && C >= J] (?,1) 4. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 5. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 6. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [N >= O] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= 1 + P && 0 >= Q] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [P >= 1 && 0 >= Q] (?,1) 9. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 10. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 11. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f57(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 12. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= Q && P = 0] (?,1) 13. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= J] (?,1) 14. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,2*J,B1,1 + -1*B1,U,V,W,X,Y,Z,A1) [C >= J] (?,1) 15. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [L = 0] (?,1) 16. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,B1,V,W,X,Y,Z,A1) [0 >= 1 + L] (?,1) 17. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,B1,V,W,X,Y,Z,A1) [L >= 1] (?,1) 18. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J,S,T,U,0,W,X,Y,Z,A1) [D >= J] (?,1) 19. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J,S,T,U,C1,W,X,Y,Z,A1) [0 >= 1 + D1 && D >= J] (?,1) 20. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J,S,T,U,C1,W,X,Y,Z,A1) [D1 >= 1 && D >= J] (?,1) 21. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,0,X,Y,Z,A1) [L = 0] (?,1) 22. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,C1,X,Y,Z,A1) [0 >= 1 + L] (?,1) 23. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,C1,X,Y,Z,A1) [L >= 1] (?,1) 24. f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,0,Y,Z,A1) [L = 0] (?,1) 25. f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,C1,Y,Z,A1) [0 >= 1 + L] (?,1) 26. f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,C1,Y,Z,A1) [L >= 1] (?,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,0,M,N,O,P,Q,R,S,T,U,V,W,X,0,Z,A1) [L = 0] (?,1) 28. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,B1,Z,A1) [0 >= 1 + L] (?,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,B1,Z,A1) [L >= 1] (?,1) 30. f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 31. f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 32. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,A + B,C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 33. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [J >= 1 + C] (?,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,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,C1,A1) [0 >= 1 + D1 && J >= 1 + C] (?,1) 35. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,C1,A1) [D1 >= 1 && J >= 1 + C] (?,1) 36. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + E] (?,1) 37. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 38. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,C + Q) [J >= 1 + D] (?,1) 39. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 40. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [Q >= 1] (?,1) 41. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [O >= 1 + N] (?,1) 42. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 43. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= 1 + P && J >= 1 + D] (?,1) 44. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [P >= 1 && J >= 1 + D] (?,1) 45. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D && P = 0] (?,1) 46. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + C] (?,1) Signature: {(f1,27) ;(f103,27) ;(f107,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27) ;(f99,27)} Flow Graph: [0->{1,2,3,46},1->{1,2,3,46},2->{1,2,3,46},3->{1,2,3,46},4->{4,43,44,45},5->{5,42},6->{7,8,12,40},7->{9 ,39},8->{9,39},9->{9,39},10->{10,38},11->{11,37},12->{13,36},13->{13,36},14->{14,33,34,35},15->{18,19,20,32} ,16->{18,19,20,32},17->{18,19,20,32},18->{21,22,23},19->{21,22,23},20->{21,22,23},21->{24,25,26},22->{24,25 ,26},23->{24,25,26},24->{27,28,29},25->{27,28,29},26->{27,28,29},27->{18,19,20,32},28->{18,19,20,32},29->{18 ,19,20,32},30->{30,31},31->{},32->{6,41},33->{15,16,17},34->{15,16,17},35->{15,16,17},36->{7,8,12,40},37->{7 ,8,12,40},38->{37},39->{38},40->{14,33,34,35},41->{30,31},42->{6,41},43->{42},44->{42},45->{6,41},46->{4,43 ,44,45}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [5,10,11] * Step 3: FromIts YES + Considered Problem: Rules: 0. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(0,0,2*D,D,4*D,3 + 4*D,4 + 4*D,D,B1,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 1. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= J] (?,1) 2. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C1 >= 2 && C >= J] (?,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= C1 && C >= J] (?,1) 4. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 6. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [N >= O] (?,1) 7. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= 1 + P && 0 >= Q] (?,1) 8. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [P >= 1 && 0 >= Q] (?,1) 9. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 12. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= Q && P = 0] (?,1) 13. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= J] (?,1) 14. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,2*J,B1,1 + -1*B1,U,V,W,X,Y,Z,A1) [C >= J] (?,1) 15. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T,0,V,W,X,Y,Z,A1) [L = 0] (?,1) 16. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,B1,V,W,X,Y,Z,A1) [0 >= 1 + L] (?,1) 17. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,B1,V,W,X,Y,Z,A1) [L >= 1] (?,1) 18. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J,S,T,U,0,W,X,Y,Z,A1) [D >= J] (?,1) 19. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J,S,T,U,C1,W,X,Y,Z,A1) [0 >= 1 + D1 && D >= J] (?,1) 20. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J,S,T,U,C1,W,X,Y,Z,A1) [D1 >= 1 && D >= J] (?,1) 21. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,0,X,Y,Z,A1) [L = 0] (?,1) 22. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,C1,X,Y,Z,A1) [0 >= 1 + L] (?,1) 23. f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,C1,X,Y,Z,A1) [L >= 1] (?,1) 24. f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,0,Y,Z,A1) [L = 0] (?,1) 25. f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,C1,Y,Z,A1) [0 >= 1 + L] (?,1) 26. f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,C1,Y,Z,A1) [L >= 1] (?,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,0,M,N,O,P,Q,R,S,T,U,V,W,X,0,Z,A1) [L = 0] (?,1) 28. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,B1,Z,A1) [0 >= 1 + L] (?,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,B1,Z,A1) [L >= 1] (?,1) 30. f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D >= J] (?,1) 31. f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 32. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,A + B,C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 33. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,A1) [J >= 1 + C] (?,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,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,C1,A1) [0 >= 1 + D1 && J >= 1 + C] (?,1) 35. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,C1,A1) [D1 >= 1 && J >= 1 + C] (?,1) 36. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + E] (?,1) 37. f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 38. f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,C + Q) [J >= 1 + D] (?,1) 39. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 40. f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [Q >= 1] (?,1) 41. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [O >= 1 + N] (?,1) 42. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D] (?,1) 43. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [0 >= 1 + P && J >= 1 + D] (?,1) 44. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [P >= 1 && J >= 1 + D] (?,1) 45. f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + D && P = 0] (?,1) 46. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [J >= 1 + C] (?,1) Signature: {(f1,27) ;(f103,27) ;(f107,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27) ;(f99,27)} Flow Graph: [0->{1,2,3,46},1->{1,2,3,46},2->{1,2,3,46},3->{1,2,3,46},4->{4,43,44,45},6->{7,8,12,40},7->{9,39},8->{9 ,39},9->{9,39},12->{13,36},13->{13,36},14->{14,33,34,35},15->{18,19,20,32},16->{18,19,20,32},17->{18,19,20 ,32},18->{21,22,23},19->{21,22,23},20->{21,22,23},21->{24,25,26},22->{24,25,26},23->{24,25,26},24->{27,28 ,29},25->{27,28,29},26->{27,28,29},27->{18,19,20,32},28->{18,19,20,32},29->{18,19,20,32},30->{30,31},31->{} ,32->{6,41},33->{15,16,17},34->{15,16,17},35->{15,16,17},36->{7,8,12,40},37->{7,8,12,40},38->{37},39->{38} ,40->{14,33,34,35},41->{30,31},42->{6,41},43->{42},44->{42},45->{6,41},46->{4,43,44,45}] + Applied Processor: FromIts + Details: () * Step 4: Decompose YES + Considered Problem: Rules: f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(0,0,2*D,D,4*D,3 + 4*D,4 + 4*D,D,B1,J ,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) True f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= J] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1 ,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [C1 >= 2 && C >= J] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1 ,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [0 >= C1 && C >= J] f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [D >= J] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [N >= O] f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [0 >= 1 + P && 0 >= Q] f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [P >= 1 && 0 >= Q] f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [D >= J] f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [0 >= Q && P = 0] f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [E >= J] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q ,2*J,B1,1 + -1*B1,U,V,W,X,Y,Z ,A1) [C >= J] f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T ,0,V,W,X,Y,Z ,A1) [L = 0] f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,B1,V,W,X,Y,Z ,A1) [0 >= 1 + L] f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,B1,V,W,X,Y,Z ,A1) [L >= 1] f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J ,S,T,U,0,W,X,Y,Z ,A1) [D >= J] f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J ,S,T,U,C1,W,X,Y,Z ,A1) [0 >= 1 + D1 && D >= J] f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J ,S,T,U,C1,W,X,Y,Z ,A1) [D1 >= 1 && D >= J] f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,0,X,Y,Z ,A1) [L = 0] f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,C1,X,Y,Z ,A1) [0 >= 1 + L] f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,C1,X,Y,Z ,A1) [L >= 1] f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,0,Y,Z ,A1) [L = 0] f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,C1,Y,Z ,A1) [0 >= 1 + L] f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,C1,Y,Z ,A1) [L >= 1] f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,0,M,N,O,P,Q,R ,S,T,U,V,W,X,0,Z ,A1) [L = 0] f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,B1,Z ,A1) [0 >= 1 + L] f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,B1,Z ,A1) [L >= 1] f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [D >= J] f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,A + B,C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P ,Q,R,S,T,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,0 ,A1) [J >= 1 + C] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,C1 ,A1) [0 >= 1 + D1 && J >= 1 + C] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,C1 ,A1) [D1 >= 1 && J >= 1 + C] f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R ,S,T,U,V,W,X,Y,Z ,A1) [J >= 1 + E] f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R ,S,T,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,C + Q) [J >= 1 + D] f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [Q >= 1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [O >= 1 + N] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [0 >= 1 + P && J >= 1 + D] f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [P >= 1 && J >= 1 + D] f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + D && P = 0] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + C] Signature: {(f1,27) ;(f103,27) ;(f107,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27) ;(f99,27)} Rule Graph: [0->{1,2,3,46},1->{1,2,3,46},2->{1,2,3,46},3->{1,2,3,46},4->{4,43,44,45},6->{7,8,12,40},7->{9,39},8->{9 ,39},9->{9,39},12->{13,36},13->{13,36},14->{14,33,34,35},15->{18,19,20,32},16->{18,19,20,32},17->{18,19,20 ,32},18->{21,22,23},19->{21,22,23},20->{21,22,23},21->{24,25,26},22->{24,25,26},23->{24,25,26},24->{27,28 ,29},25->{27,28,29},26->{27,28,29},27->{18,19,20,32},28->{18,19,20,32},29->{18,19,20,32},30->{30,31},31->{} ,32->{6,41},33->{15,16,17},34->{15,16,17},35->{15,16,17},36->{7,8,12,40},37->{7,8,12,40},38->{37},39->{38} ,40->{14,33,34,35},41->{30,31},42->{6,41},43->{42},44->{42},45->{6,41},46->{4,43,44,45}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,6,7,8,9,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,37,38,39,40,41,42,43,44,45,46] | +- p:[1,2,3] c: [3] | | | `- p:[1,2] c: [2] | | | `- p:[1] c: [1] | +- p:[4] c: [4] | +- p:[6,32,15,33,14,40,36,12,37,38,39,7,8,9,13,34,35,16,17,27,24,21,18,28,25,22,19,29,26,23,20] c: [8] | | | `- p:[6,32,15,33,14,40,36,12,37,38,39,7,9,13,34,35,16,17,27,24,21,18,28,25,22,19,29,26,23,20] c: [12] | | | +- p:[13] c: [13] | | | `- p:[6,32,15,33,14,40,37,38,39,7,9,34,35,16,17,27,24,21,18,28,25,22,19,29,26,23,20] c: [9,18,19,20,21,22,23,24,25,26,27,28,29] | | | `- p:[6,32,15,33,14,40,37,38,39,7,34,35,16,17] c: [14] | | | `- p:[6,32,15,33,40,37,38,39,7,34,35,16,17] c: [7,37,38,39] | | | `- p:[6,32,15,33,40,34,35,16,17] c: [6,15,16,17,32,33,34,35,40] | `- p:[30] c: [30] * Step 5: CloseWith YES + Considered Problem: (Rules: f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(0,0,2*D,D,4*D,3 + 4*D,4 + 4*D,D,B1,J ,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) True f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A,B,C,D,E,F,G,H,I,1 + J,1,0,0,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= J] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1 ,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [C1 >= 2 && C >= J] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f13(A + B1,B,C,D,E,F,G,H,I,1 + J,C1 ,1 + -1*C1,B1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [0 >= C1 && C >= J] f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [D >= J] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [N >= O] f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [0 >= 1 + P && 0 >= Q] f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [P >= 1 && 0 >= Q] f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f44(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [D >= J] f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [0 >= Q && P = 0] f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f64(A,B,C,D,E,F,G,H,I,2 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [E >= J] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q ,2*J,B1,1 + -1*B1,U,V,W,X,Y,Z ,A1) [C >= J] f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,0,M,N,O,P,Q,R,S,T ,0,V,W,X,Y,Z ,A1) [L = 0] f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,B1,V,W,X,Y,Z ,A1) [0 >= 1 + L] f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,B1,V,W,X,Y,Z ,A1) [L >= 1] f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J ,S,T,U,0,W,X,Y,Z ,A1) [D >= J] f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J ,S,T,U,C1,W,X,Y,Z ,A1) [0 >= 1 + D1 && D >= J] f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f99(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,2*J ,S,T,U,C1,W,X,Y,Z ,A1) [D1 >= 1 && D >= J] f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,0,X,Y,Z ,A1) [L = 0] f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,C1,X,Y,Z ,A1) [0 >= 1 + L] f99(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f103(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,C1,X,Y,Z ,A1) [L >= 1] f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,0,Y,Z ,A1) [L = 0] f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,C1,Y,Z ,A1) [0 >= 1 + L] f103(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f107(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,C1,Y,Z ,A1) [L >= 1] f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,0,M,N,O,P,Q,R ,S,T,U,V,W,X,0,Z ,A1) [L = 0] f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,B1,Z ,A1) [0 >= 1 + L] f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f91(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,B1,Z ,A1) [L >= 1] f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B,C,D,E,F,G,H,I,1 + J,K,L,M,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [D >= J] f118(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,A + B,C,D,E,F,G,H,I,J,K,L,M,N,1 + O,P ,Q,R,S,T,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,0 ,A1) [J >= 1 + C] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,C1 ,A1) [0 >= 1 + D1 && J >= 1 + C] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f86(A,B,C,D,E,F,G,H,I,J,K,B1,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,C1 ,A1) [D1 >= 1 && J >= 1 + C] f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R ,S,T,U,V,W,X,Y,Z ,A1) [J >= 1 + E] f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1 + Q,R ,S,T,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,C + Q) [J >= 1 + D] f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f50(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f40(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [Q >= 1] f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f118(A,B1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [O >= 1 + N] f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + D] f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [0 >= 1 + P && J >= 1 + D] f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [P >= 1 && J >= 1 + D] f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + D && P = 0] f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f24(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [J >= 1 + C] Signature: {(f1,27) ;(f103,27) ;(f107,27) ;(f118,27) ;(f13,27) ;(f2,27) ;(f24,27) ;(f31,27) ;(f37,27) ;(f40,27) ;(f44,27) ;(f50,27) ;(f57,27) ;(f64,27) ;(f71,27) ;(f86,27) ;(f91,27) ;(f99,27)} Rule Graph: [0->{1,2,3,46},1->{1,2,3,46},2->{1,2,3,46},3->{1,2,3,46},4->{4,43,44,45},6->{7,8,12,40},7->{9,39},8->{9 ,39},9->{9,39},12->{13,36},13->{13,36},14->{14,33,34,35},15->{18,19,20,32},16->{18,19,20,32},17->{18,19,20 ,32},18->{21,22,23},19->{21,22,23},20->{21,22,23},21->{24,25,26},22->{24,25,26},23->{24,25,26},24->{27,28 ,29},25->{27,28,29},26->{27,28,29},27->{18,19,20,32},28->{18,19,20,32},29->{18,19,20,32},30->{30,31},31->{} ,32->{6,41},33->{15,16,17},34->{15,16,17},35->{15,16,17},36->{7,8,12,40},37->{7,8,12,40},38->{37},39->{38} ,40->{14,33,34,35},41->{30,31},42->{6,41},43->{42},44->{42},45->{6,41},46->{4,43,44,45}] ,We construct a looptree: P: [0,1,2,3,4,6,7,8,9,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,37,38,39,40,41,42,43,44,45,46] | +- p:[1,2,3] c: [3] | | | `- p:[1,2] c: [2] | | | `- p:[1] c: [1] | +- p:[4] c: [4] | +- p:[6,32,15,33,14,40,36,12,37,38,39,7,8,9,13,34,35,16,17,27,24,21,18,28,25,22,19,29,26,23,20] c: [8] | | | `- p:[6,32,15,33,14,40,36,12,37,38,39,7,9,13,34,35,16,17,27,24,21,18,28,25,22,19,29,26,23,20] c: [12] | | | +- p:[13] c: [13] | | | `- p:[6,32,15,33,14,40,37,38,39,7,9,34,35,16,17,27,24,21,18,28,25,22,19,29,26,23,20] c: [9,18,19,20,21,22,23,24,25,26,27,28,29] | | | `- p:[6,32,15,33,14,40,37,38,39,7,34,35,16,17] c: [14] | | | `- p:[6,32,15,33,40,37,38,39,7,34,35,16,17] c: [7,37,38,39] | | | `- p:[6,32,15,33,40,34,35,16,17] c: [6,15,16,17,32,33,34,35,40] | `- p:[30] c: [30]) + Applied Processor: CloseWith True + Details: () YES