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) -> f5(A,B,C,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. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,C,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. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(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. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f17(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. f27(A,B,C,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,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. 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) -> f34(A,B,C,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. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(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. f46(A,B,C,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,B1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [3 >= E] (?,1) 8. f46(A,B,C,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,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 4] (?,1) 9. 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) -> 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) [A >= 1 + B] (?,1) 10. f69(A,B,C,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,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. 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) -> f53(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. 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) -> f69(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. 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) -> f69(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. 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) -> f69(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. 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) -> f69(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. 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) -> f69(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. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(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. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(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. f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(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) -> f27(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. f119(A,B,C,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,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. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,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. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,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. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,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. 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) -> f50(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. 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) -> 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. f34(A,B,C,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,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. 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) -> f46(A,B,C,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. 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) -> f46(A,B,C,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. 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) -> f1(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. f27(A,B,C,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) [E >= 51] (?,1) 39. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,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. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(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. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f17(A,B,C,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: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,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. 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) -> f5(A,B,C,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. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,C,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. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(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. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f17(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. f27(A,B,C,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,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. 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) -> f34(A,B,C,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. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(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. f46(A,B,C,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,B1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [3 >= E] (?,1) 8. f46(A,B,C,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,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 4] (?,1) 9. 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) -> 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) [A >= 1 + B] (?,1) 10. f69(A,B,C,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,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. 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) -> f53(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. 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) -> f69(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. 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) -> f69(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. 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) -> f69(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. 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) -> f69(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. 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) -> f69(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. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(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. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(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. f119(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(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) -> f27(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. f119(A,B,C,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,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. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,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. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,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. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,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. 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) -> f50(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. 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) -> 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. f34(A,B,C,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,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. 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) -> f46(A,B,C,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. 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) -> f46(A,B,C,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. 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) -> f1(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. f27(A,B,C,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) [E >= 51] (?,1) 39. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,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. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(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. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f17(A,B,C,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: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,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. 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) -> f5(A,B,C,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. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,C,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. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(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. f27(A,B,C,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,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. 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) -> f34(A,B,C,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. f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(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. f46(A,B,C,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,B1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [3 >= E] (?,1) 8. f46(A,B,C,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,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [E >= 4] (?,1) 9. 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) -> 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) [A >= 1 + B] (?,1) 10. f69(A,B,C,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,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. 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) -> f53(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. 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) -> f69(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. 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) -> f69(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. 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) -> f69(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. 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) -> f69(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. 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) -> f69(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. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(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. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(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) -> f27(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. f119(A,B,C,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,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. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,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. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,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. f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,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. 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) -> f50(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. 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) -> 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. f34(A,B,C,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,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. 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) -> f46(A,B,C,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. 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) -> f46(A,B,C,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. 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) -> f1(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. f27(A,B,C,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) [E >= 51] (?,1) 39. f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,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. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(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. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f17(A,B,C,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: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,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: 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) -> f5(A,B,C,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 f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,C,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] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(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] f27(A,B,C,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,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [50 >= E] 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) -> f34(A,B,C,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] f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(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] f46(A,B,C,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,B1,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [3 >= E] f46(A,B,C,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,0,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [E >= 4] 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) -> 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) [A >= 1 + B] f69(A,B,C,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,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] 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) -> f53(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] 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) -> f69(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] 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) -> f69(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] 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) -> f69(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] 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) -> f69(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] 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) -> f69(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] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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] f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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] f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(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] f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(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) -> f27(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] f119(A,B,C,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,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] f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,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] f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,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] f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,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] 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) -> f50(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] 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) -> 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] f34(A,B,C,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,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] 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) -> f46(A,B,C,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] 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) -> f46(A,B,C,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] 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) -> f1(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] f27(A,B,C,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) [E >= 51] f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,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] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(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] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f17(A,B,C,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: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,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: 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) -> f5(A,B,C,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 f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(A,B,C,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] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f8(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] f27(A,B,C,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,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [50 >= E] 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) -> f34(A,B,C,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] f34(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f34(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] f46(A,B,C,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,B1,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [3 >= E] f46(A,B,C,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,0,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X,Y,Z ,A1) [E >= 4] 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) -> 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) [A >= 1 + B] f69(A,B,C,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,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] 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) -> f53(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] 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) -> f69(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] 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) -> f69(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] 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) -> f69(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] 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) -> f69(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] 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) -> f69(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] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f80(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] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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] f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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] f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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] f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f92(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] f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(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] f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(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) -> f27(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] f119(A,B,C,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,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] f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f119(A,B,C,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] f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f110(A,B,C,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] f92(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f101(A,B,C,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] 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) -> f50(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] 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) -> 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] f34(A,B,C,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,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] 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) -> f46(A,B,C,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] 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) -> f46(A,B,C,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] 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) -> f1(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] f27(A,B,C,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) [E >= 51] f17(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f27(A,B,C,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] f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f5(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] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f17(A,B,C,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: {(f1,27) ;(f101,27) ;(f110,27) ;(f119,27) ;(f132,27) ;(f17,27) ;(f2,27) ;(f27,27) ;(f31,27) ;(f34,27) ;(f46,27) ;(f5,27) ;(f50,27) ;(f53,27) ;(f69,27) ;(f8,27) ;(f80,27) ;(f92,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