YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 3. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f26(A,1 + B,C,B1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 4. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f38(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [50 >= E] (?,1) 5. f38(A,B,C,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) [A >= 1 + B] (?,1) 6. 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) -> f40(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 7. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [3 >= E] (?,1) 8. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 4] (?,1) 9. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B] (?,1) 10. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [H >= I] (?,1) 11. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,B1,C1,D1,C1 + D1,E1,C1 + E1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && E >= 5] (?,1) 12. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,D1,B1,C1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && 4 >= E] (?,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1,F1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && F1 >= 1 + C1 + E1] (?,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1,F1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && C1 + E1 >= 1 + F1] (?,1) 15. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && E1 >= 1 + C1 + D1] (?,1) 16. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && C1 + D1 >= 1 + E1] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z,A1) [I >= 1 + H && E1 >= 1 + D1 + K] (?,1) 18. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z,A1) [I >= 1 + H && D1 + K >= 1 + E1] (?,1) 19. f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S,T,U,V,C1,D1,E1,F1,A1) [T >= 0] (?,1) 20. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1,C1 + K,D1,T,U,V,E1,F1,G1,H1,A1) [I >= 1 + H] (?,1) 21. f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,-1*S,T,U,V,C1,D1,E1,F1,A1) [0 >= 1 + T] (?,1) 22. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [B >= 1 + A1] (?,1) 23. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [C >= 1 + A1] (?,1) 24. f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 25. f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f120(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 26. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 27. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 28. f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 29. f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 30. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= C] (?,1) 31. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= B] (?,1) 32. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 33. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A] (?,1) 34. 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) -> f38(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 35. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && 0 >= 1 + F] (?,1) 36. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F >= 1] (?,1) 37. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F = 0] (?,1) 38. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 51] (?,1) 39. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 40. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 41. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) Signature: {(f0,27) ;(f104,27) ;(f112,27) ;(f120,27) ;(f132,27) ;(f16,27) ;(f18,27) ;(f26,27) ;(f35,27) ;(f38,27) ;(f40,27) ;(f52,27) ;(f53,27) ;(f56,27) ;(f58,27) ;(f74,27) ;(f85,27) ;(f96,27)} Flow Graph: [0->{1,41},1->{2,40},2->{2,40},3->{3,39},4->{5,35,36,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12 ,13,14,15,16,32},10->{11,12,13,14,15,16,32},11->{11,12,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20} ,14->{10,17,18,20},15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31} ,21->{22,31},22->{22,31},23->{23,30},24->{24,29},25->{25,28},26->{26,27},27->{4,38},28->{11,12,13,14,15,16 ,32},29->{25,28},30->{24,29},31->{23,30},32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{} ,38->{},39->{4,38},40->{1,41},41->{3,39}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(4,35),(4,36),(11,12),(29,25),(41,3)] * Step 2: UnreachableRules YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 3. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f26(A,1 + B,C,B1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 4. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f38(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [50 >= E] (?,1) 5. f38(A,B,C,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) [A >= 1 + B] (?,1) 6. 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) -> f40(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 7. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [3 >= E] (?,1) 8. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 4] (?,1) 9. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B] (?,1) 10. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [H >= I] (?,1) 11. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,B1,C1,D1,C1 + D1,E1,C1 + E1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && E >= 5] (?,1) 12. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,D1,B1,C1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && 4 >= E] (?,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1,F1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && F1 >= 1 + C1 + E1] (?,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1,F1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && C1 + E1 >= 1 + F1] (?,1) 15. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && E1 >= 1 + C1 + D1] (?,1) 16. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && C1 + D1 >= 1 + E1] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z,A1) [I >= 1 + H && E1 >= 1 + D1 + K] (?,1) 18. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z,A1) [I >= 1 + H && D1 + K >= 1 + E1] (?,1) 19. f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S,T,U,V,C1,D1,E1,F1,A1) [T >= 0] (?,1) 20. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1,C1 + K,D1,T,U,V,E1,F1,G1,H1,A1) [I >= 1 + H] (?,1) 21. f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,-1*S,T,U,V,C1,D1,E1,F1,A1) [0 >= 1 + T] (?,1) 22. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [B >= 1 + A1] (?,1) 23. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [C >= 1 + A1] (?,1) 24. f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 25. f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f120(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 26. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 27. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 28. f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 29. f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 30. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= C] (?,1) 31. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= B] (?,1) 32. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 33. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A] (?,1) 34. 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) -> f38(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 35. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && 0 >= 1 + F] (?,1) 36. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F >= 1] (?,1) 37. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F = 0] (?,1) 38. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 51] (?,1) 39. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 40. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 41. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) Signature: {(f0,27) ;(f104,27) ;(f112,27) ;(f120,27) ;(f132,27) ;(f16,27) ;(f18,27) ;(f26,27) ;(f35,27) ;(f38,27) ;(f40,27) ;(f52,27) ;(f53,27) ;(f56,27) ;(f58,27) ;(f74,27) ;(f85,27) ;(f96,27)} Flow Graph: [0->{1,41},1->{2,40},2->{2,40},3->{3,39},4->{5,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12,13,14 ,15,16,32},10->{11,12,13,14,15,16,32},11->{11,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20},14->{10,17 ,18,20},15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31},21->{22,31} ,22->{22,31},23->{23,30},24->{24,29},25->{25,28},26->{26,27},27->{4,38},28->{11,12,13,14,15,16,32},29->{28} ,30->{24,29},31->{23,30},32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{},38->{},39->{4 ,38},40->{1,41},41->{39}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [3,25] * Step 3: FromIts YES + Considered Problem: Rules: 0. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 4. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f38(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [50 >= E] (?,1) 5. f38(A,B,C,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) [A >= 1 + B] (?,1) 6. 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) -> f40(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C] (?,1) 7. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [3 >= E] (?,1) 8. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 4] (?,1) 9. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B] (?,1) 10. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [H >= I] (?,1) 11. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,B1,C1,D1,C1 + D1,E1,C1 + E1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && E >= 5] (?,1) 12. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,D1,B1,C1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= C && 4 >= E] (?,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1,F1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && F1 >= 1 + C1 + E1] (?,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1,F1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && C1 + E1 >= 1 + F1] (?,1) 15. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && E1 >= 1 + C1 + D1] (?,1) 16. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 5 && A >= C && C1 + D1 >= 1 + E1] (?,1) 17. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z,A1) [I >= 1 + H && E1 >= 1 + D1 + K] (?,1) 18. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z,A1) [I >= 1 + H && D1 + K >= 1 + E1] (?,1) 19. f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S,T,U,V,C1,D1,E1,F1,A1) [T >= 0] (?,1) 20. f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1,C1 + K,D1,T,U,V,E1,F1,G1,H1,A1) [I >= 1 + H] (?,1) 21. f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,-1*S,T,U,V,C1,D1,E1,F1,A1) [0 >= 1 + T] (?,1) 22. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [B >= 1 + A1] (?,1) 23. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [C >= 1 + A1] (?,1) 24. f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S,T,U,V,W,X,Y,Z,1 + A1) [A >= A1] (?,1) 26. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= B] (?,1) 27. f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 28. f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 29. f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= 1 + A] (?,1) 30. f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= C] (?,1) 31. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A1 >= B] (?,1) 32. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 33. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A] (?,1) 34. 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) -> f38(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 35. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && 0 >= 1 + F] (?,1) 36. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F >= 1] (?,1) 37. f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= A && F = 0] (?,1) 38. f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 51] (?,1) 39. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 40. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [C >= 1 + A] (?,1) 41. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) Signature: {(f0,27) ;(f104,27) ;(f112,27) ;(f120,27) ;(f132,27) ;(f16,27) ;(f18,27) ;(f26,27) ;(f35,27) ;(f38,27) ;(f40,27) ;(f52,27) ;(f53,27) ;(f56,27) ;(f58,27) ;(f74,27) ;(f85,27) ;(f96,27)} Flow Graph: [0->{1,41},1->{2,40},2->{2,40},4->{5,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12,13,14,15,16,32} ,10->{11,12,13,14,15,16,32},11->{11,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20},14->{10,17,18,20} ,15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31},21->{22,31},22->{22,31} ,23->{23,30},24->{24,29},26->{26,27},27->{4,38},28->{11,12,13,14,15,16,32},29->{28},30->{24,29},31->{23,30} ,32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{},38->{},39->{4,38},40->{1,41},41->{39}] + Applied Processor: FromIts + Details: () * Step 4: Decompose YES + Considered Problem: Rules: f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) True f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= B] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A >= C] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f38(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [50 >= E] f38(A,B,C,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) [A >= 1 + B] 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) -> f40(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [3 >= E] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [E >= 4] f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= 1 + B] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [H >= I] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,B1,C1,D1,C1 + D1 ,E1,C1 + E1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C && E >= 5] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,D1,B1,C1,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A >= C && 4 >= E] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1 ,F1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && F1 >= 1 + C1 + E1] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1 ,F1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && C1 + E1 >= 1 + F1] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && E1 >= 1 + C1 + D1] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && C1 + D1 >= 1 + E1] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z ,A1) [I >= 1 + H && E1 >= 1 + D1 + K] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z ,A1) [I >= 1 + H && D1 + K >= 1 + E1] f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S ,T,U,V,C1,D1,E1,F1 ,A1) [T >= 0] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1 ,C1 + K,D1,T,U,V,E1,F1,G1,H1 ,A1) [I >= 1 + H] f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R ,-1*S,T,U,V,C1,D1,E1,F1 ,A1) [0 >= 1 + T] f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S ,T,U,V,W,X,Y,Z ,1 + A1) [B >= 1 + A1] f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R ,S,T,U,V,W,X,Y,Z ,1 + A1) [C >= 1 + A1] f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R ,S,T,U,V,W,X,Y,Z ,1 + A1) [A >= A1] f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [A >= B] f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A1 >= 1 + A] f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= 1 + A] f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= C] f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= B] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [B >= A] 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) -> f38(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && 0 >= 1 + F] f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && F >= 1] f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && F = 0] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [E >= 51] f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= 1 + A] Signature: {(f0,27) ;(f104,27) ;(f112,27) ;(f120,27) ;(f132,27) ;(f16,27) ;(f18,27) ;(f26,27) ;(f35,27) ;(f38,27) ;(f40,27) ;(f52,27) ;(f53,27) ;(f56,27) ;(f58,27) ;(f74,27) ;(f85,27) ;(f96,27)} Rule Graph: [0->{1,41},1->{2,40},2->{2,40},4->{5,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12,13,14,15,16,32} ,10->{11,12,13,14,15,16,32},11->{11,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20},14->{10,17,18,20} ,15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31},21->{22,31},22->{22,31} ,23->{23,30},24->{24,29},26->{26,27},27->{4,38},28->{11,12,13,14,15,16,32},29->{28},30->{24,29},31->{23,30} ,32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{},38->{},39->{4,38},40->{1,41},41->{39}] + Applied Processor: Decompose NoGreedy + 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,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41] | +- p:[1,40,2] c: [2] | | | `- p:[1,40] c: [1,40] | `- p:[4,27,26,33,7,35,34,5,6,36,8,32,9,10,12,28,29,24,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [24] | `- p:[4,27,26,33,7,35,34,5,6,36,8,32,9,10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [9] | +- p:[10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [22] | | | `- p:[10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21] c: [10,11,12,13,14,15,16,17,18,19,20,21,28,29,30,31] | | | `- p:[23] c: [23] | `- p:[4,27,26,33,7,35,34,5,6,36,8] c: [6] | `- p:[4,27,26,33,7,35,34,5,36,8] c: [7] | `- p:[4,27,26,33,8,35,34,5,36] c: [26] | `- p:[4,27,33,8,35,34,5,36] c: [4,5,8,27,33,34,35,36] * Step 5: CloseWith YES + Considered Problem: (Rules: f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) True f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= B] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f18(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A >= C] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f38(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [50 >= E] f38(A,B,C,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) [A >= 1 + B] 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) -> f40(A,B,1 + C,D,E,B1 + F,B1,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,B1,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [3 >= E] f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [E >= 4] f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [A >= 1 + B] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [H >= I] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,B1,C1,D1,C1 + D1 ,E1,C1 + E1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= C && E >= 5] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,D1,B1,C1,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A >= C && 4 >= E] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1 ,F1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && F1 >= 1 + C1 + E1] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,G1,B1,C1,D1,C1 + D1,E1 ,F1,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && C1 + E1 >= 1 + F1] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && E1 >= 1 + C1 + D1] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f74(A,B,C,D,E,F,G,H,F1,B1,C1,D1,E1,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [E >= 5 && A >= C && C1 + D1 >= 1 + E1] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z ,A1) [I >= 1 + H && E1 >= 1 + D1 + K] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O ,B1 + -1*C1,D1,E1,F1,G1,H1,I1,W,X,Y,Z ,A1) [I >= 1 + H && D1 + K >= 1 + E1] f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R,S ,T,U,V,C1,D1,E1,F1 ,A1) [T >= 0] f74(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,C1 ,C1 + K,D1,T,U,V,E1,F1,G1,H1 ,A1) [I >= 1 + H] f85(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,B1,Q,R ,-1*S,T,U,V,C1,D1,E1,F1 ,A1) [0 >= 1 + T] f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f96(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R,S ,T,U,V,W,X,Y,Z ,1 + A1) [B >= 1 + A1] f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R ,S,T,U,V,W,X,Y,Z ,1 + A1) [C >= 1 + A1] f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,B1,L,M,N,O,C1,Q,R ,S,T,U,V,W,X,Y,Z ,1 + A1) [A >= A1] f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q ,R,S,T,U,V,W,X,Y,Z ,A1) [A >= B] f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f58(A,B,1 + C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [A1 >= 1 + A] f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f120(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= 1 + A] f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f112(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= C] f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f104(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [A1 >= B] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f56(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f132(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [B >= A] 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) -> f38(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && 0 >= 1 + F] f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && F >= 1] f38(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= A && F = 0] f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [E >= 51] f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f35(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f16(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [C >= 1 + A] f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [B >= 1 + A] Signature: {(f0,27) ;(f104,27) ;(f112,27) ;(f120,27) ;(f132,27) ;(f16,27) ;(f18,27) ;(f26,27) ;(f35,27) ;(f38,27) ;(f40,27) ;(f52,27) ;(f53,27) ;(f56,27) ;(f58,27) ;(f74,27) ;(f85,27) ;(f96,27)} Rule Graph: [0->{1,41},1->{2,40},2->{2,40},4->{5,37},5->{6,34},6->{6,34},7->{9,33},8->{9,33},9->{11,12,13,14,15,16,32} ,10->{11,12,13,14,15,16,32},11->{11,13,14,15,16,32},12->{10,17,18,20},13->{10,17,18,20},14->{10,17,18,20} ,15->{10,17,18,20},16->{10,17,18,20},17->{19,21},18->{19,21},19->{22,31},20->{22,31},21->{22,31},22->{22,31} ,23->{23,30},24->{24,29},26->{26,27},27->{4,38},28->{11,12,13,14,15,16,32},29->{28},30->{24,29},31->{23,30} ,32->{9,33},33->{26,27},34->{5,35,36,37},35->{7,8},36->{7,8},37->{},38->{},39->{4,38},40->{1,41},41->{39}] ,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,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41] | +- p:[1,40,2] c: [2] | | | `- p:[1,40] c: [1,40] | `- p:[4,27,26,33,7,35,34,5,6,36,8,32,9,10,12,28,29,24,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [24] | `- p:[4,27,26,33,7,35,34,5,6,36,8,32,9,10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [9] | +- p:[10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21,22] c: [22] | | | `- p:[10,12,28,29,30,23,31,19,17,13,11,14,15,16,18,20,21] c: [10,11,12,13,14,15,16,17,18,19,20,21,28,29,30,31] | | | `- p:[23] c: [23] | `- p:[4,27,26,33,7,35,34,5,6,36,8] c: [6] | `- p:[4,27,26,33,7,35,34,5,36,8] c: [7] | `- p:[4,27,26,33,8,35,34,5,36] c: [26] | `- p:[4,27,33,8,35,34,5,36] c: [4,5,8,27,33,34,35,36]) + Applied Processor: CloseWith True + Details: () YES