YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B && C >= 0] (?,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] (?,1) 2. 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] (?,1) 3. 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] (?,1) 4. 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] (?,1) 5. 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] (?,1) 6. 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] (?,1) 7. 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] (?,1) 8. 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] (?,1) 9. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] (?,1) 10. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 11. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] (?,1) 12. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,1) 13. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] (?,1) 14. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 15. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] (?,1) 16. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,1) 17. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,2,3,4,5,6,7,8},10->{1,2,3,4,5,6,7,8},11->{1,2,3,4,5,6,7,8},12->{1,2 ,3,4,5,6,7,8},13->{1,2,3,4,5,6,7,8},14->{1,2,3,4,5,6,7,8},15->{1,2,3,4,5,6,7,8},16->{1,2,3,4,5,6,7,8},17->{0 ,9,10,11,12,13,14,15,16}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(9,2) ,(9,4) ,(9,6) ,(9,8) ,(10,2) ,(10,4) ,(10,6) ,(10,8) ,(11,1) ,(11,3) ,(11,5) ,(11,7) ,(12,1) ,(12,3) ,(12,5) ,(12,7) ,(13,2) ,(13,4) ,(13,6) ,(13,8) ,(14,2) ,(14,4) ,(14,6) ,(14,8) ,(15,1) ,(15,3) ,(15,5) ,(15,7) ,(16,1) ,(16,3) ,(16,5) ,(16,7) ,(17,9) ,(17,10) ,(17,11) ,(17,12) ,(17,13) ,(17,14) ,(17,15) ,(17,16)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [A >= 1 + B && C >= 0] (?,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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 1] (?,1) 2. 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 1] (?,1) 3. 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] (?,1) 4. 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] (?,1) 5. 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] (?,1) 6. 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] (?,1) 7. 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] (?,1) 8. 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S,T,U,I,B1,X,Y,Z,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] (?,1) 9. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] (?,1) 10. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 11. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] (?,1) 12. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,1) 13. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] (?,1) 14. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] (?,1) 15. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] (?,1) 16. f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] (?,1) 17. f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S,T,U,V,W,X,Y,Z,A1) True (1,1) Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Flow Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,3,5,7},10->{1,3,5,7},11->{2,4,6,8},12->{2,4,6,8},13->{1,3,5,7} ,14->{1,3,5,7},15->{2,4,6,8},16->{2,4,6,8},17->{0}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= 1 + B && C >= 0] 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S ,T,U,I,B1,X,Y,Z ,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S ,T,U,I,B1,X,Y,Z ,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S ,T,U,V,W,X,Y,Z ,A1) True Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Rule Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,3,5,7},10->{1,3,5,7},11->{2,4,6,8},12->{2,4,6,8},13->{1,3,5,7} ,14->{1,3,5,7},15->{2,4,6,8},16->{2,4,6,8},17->{0}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | +- p:[0] c: [0] | `- p:[3,4,5,6] c: [6] | `- p:[3,4,5] c: [5] | `- p:[3,4] c: [4] | `- p:[3] c: [3] * Step 4: CloseWith YES + Considered Problem: (Rules: f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(A,1 + B,1 + C,B1,B1,B1,G,H,I,J,K,L,M,N,O ,P,Q,R,S,T,U,V,W,X,Y,Z ,A1) [A >= 1 + B && C >= 0] 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [D1 >= 1 + C1 && G >= 0 && H >= 1 && I >= 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) -> f0(A,B,C,D,E,F,G,B1,I,H,E1,F1,C1,D1,G1,P,Q,R ,S,T,U,V,W,X,Y,Z ,A1) [D1 >= 1 + C1 && G >= 0 && 0 >= 1 + H && I >= 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && H >= 1 && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [M >= D1 && G >= 0 && I >= 0 && P >= 1 && 0 >= 1 + H && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && H >= 1 && J = 0] 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) -> f5(A,B,C,D,E,F,-1 + G,R,1 + I,0,F1,C1,M,D1,O ,E1,R,P,B1,1 + I,-1 + G,I,W,X,Y,Z ,A1) [M >= D1 && G >= 0 && I >= 0 && 0 >= 1 + P && 0 >= 1 + H && J = 0] 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S ,T,U,I,B1,X,Y,Z ,A1) [M >= C1 && G >= 0 && H >= 1 && I >= 0 && P = 0 && J = 0] 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) -> f12(A,B,C,D,E,F,G,H,I,0,E1,F1,M,C1,O,0,R,R,S ,T,U,I,B1,X,Y,Z ,A1) [M >= C1 && G >= 0 && 0 >= 1 + H && I >= 0 && P = 0 && J = 0] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && D >= 1] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && B1 >= 1 && B >= A && 0 >= 1 + D] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && D >= 1] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && E1 >= 1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && D >= 1] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && B1 >= 1 && B >= A && 0 >= 1 + D] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && D >= 1] f9(A,B,C,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,-3 + C,B1,1,0,H1,I1,M,N,O,C1 ,B1,E1,F1,1,-3 + C,V,D,D,-2 + C,D1 ,G1) [D1 >= G1 && C >= 2 && 0 >= 1 + E1 && 0 >= 1 + B1 && B >= A && 0 >= 1 + D] f6(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) -> f9(17,1,0,B1,B1,B1,G,H,I,J,K,L,M,N,O,P,E1,R,S ,T,U,V,W,X,Y,Z ,A1) True Signature: {(f0,27);(f12,27);(f5,27);(f6,27);(f9,27)} Rule Graph: [0->{0,9,10,11,12,13,14,15,16},1->{},2->{},3->{1,2,3,4,5,6,7,8},4->{1,2,3,4,5,6,7,8},5->{1,2,3,4,5,6,7,8} ,6->{1,2,3,4,5,6,7,8},7->{},8->{},9->{1,3,5,7},10->{1,3,5,7},11->{2,4,6,8},12->{2,4,6,8},13->{1,3,5,7} ,14->{1,3,5,7},15->{2,4,6,8},16->{2,4,6,8},17->{0}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17] | +- p:[0] c: [0] | `- p:[3,4,5,6] c: [6] | `- p:[3,4,5] c: [5] | `- p:[3,4] c: [4] | `- p:[3] c: [3]) + Applied Processor: CloseWith True + Details: () YES