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) -> f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 1 + B] (?,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,C,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 + S && A >= D] (?,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,S,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [S >= C && A >= D] (?,1) 4. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= D] (?,1) 5. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,1 + D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R) [A >= D] (?,1) 6. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,1 + D,E,F,G,S,S^2,J + S^2,K,L,M,N,O,P,Q,R) [0 >= 1 + S && A >= D] (?,1) 7. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,1 + D,E,F,G,S,S^2,J + S^2,K,L,M,N,O,P,Q,R) [S >= 1 && A >= D] (?,1) 8. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= K] (?,1) 9. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,1 + D,E,F,G,H,I,J + S*T,K,L,M,N,O,P,Q,R) [A >= D] (?,1) 10. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f62(A,B,C,1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= D] (?,1) 11. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N,O,P,Q,R) [D >= 1 + A] (?,1) 12. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f62(A,B,C,D,E,F,G,H,I,J,K,S,M,N,O,P,Q,R) [J >= T*U && T + T*U >= 1 + J && T >= S && J >= U*V && U*V + V >= 1 + J && S >= V && D >= 1 + A] (?,1) 13. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [K >= 1 + A] (?,1) 14. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,S,T,T,P,Q,R) [D >= 1 + A] (?,1) 15. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,-1*S,T,S,R) [D >= 1 + A] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [D >= 1 + A] (?,1) 17. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0) [D >= 1 + A && C = 0] (?,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 && D >= 1 + A] (?,1) 20. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && 0 >= 1 + S] (?,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && S >= 1] (?,1) 22. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A] (?,1) Signature: {(f1,18);(f2,18);(f26,18);(f32,18);(f5,18);(f52,18);(f55,18);(f62,18);(f9,18)} Flow Graph: [0->{1,20,21,22},1->{2,3,17,18,19},2->{2,3,17,18,19},3->{2,3,17,18,19},4->{4,16},5->{5,6,7,14,15},6->{5,6 ,7,14,15},7->{5,6,7,14,15},8->{9,12},9->{9,12},10->{10,11},11->{8,13},12->{10,11},13->{1,20,21,22},14->{8 ,13},15->{8,13},16->{5,6,7,14,15},17->{1,20,21,22},18->{4,16},19->{4,16},20->{},21->{},22->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,18) ,(1,19) ,(12,10) ,(16,5) ,(16,6) ,(16,7) ,(18,4) ,(19,4)] * 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) -> f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 1 + B] (?,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,C,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 + S && A >= D] (?,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,S,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [S >= C && A >= D] (?,1) 4. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= D] (?,1) 5. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,1 + D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R) [A >= D] (?,1) 6. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,1 + D,E,F,G,S,S^2,J + S^2,K,L,M,N,O,P,Q,R) [0 >= 1 + S && A >= D] (?,1) 7. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,1 + D,E,F,G,S,S^2,J + S^2,K,L,M,N,O,P,Q,R) [S >= 1 && A >= D] (?,1) 8. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= K] (?,1) 9. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,1 + D,E,F,G,H,I,J + S*T,K,L,M,N,O,P,Q,R) [A >= D] (?,1) 10. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f62(A,B,C,1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= D] (?,1) 11. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N,O,P,Q,R) [D >= 1 + A] (?,1) 12. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f62(A,B,C,D,E,F,G,H,I,J,K,S,M,N,O,P,Q,R) [J >= T*U && T + T*U >= 1 + J && T >= S && J >= U*V && U*V + V >= 1 + J && S >= V && D >= 1 + A] (?,1) 13. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [K >= 1 + A] (?,1) 14. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,S,T,T,P,Q,R) [D >= 1 + A] (?,1) 15. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,-1*S,T,S,R) [D >= 1 + A] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [D >= 1 + A] (?,1) 17. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0) [D >= 1 + A && C = 0] (?,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 && D >= 1 + A] (?,1) 20. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && 0 >= 1 + S] (?,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && S >= 1] (?,1) 22. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A] (?,1) Signature: {(f1,18);(f2,18);(f26,18);(f32,18);(f5,18);(f52,18);(f55,18);(f62,18);(f9,18)} Flow Graph: [0->{1,20,21,22},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},4->{4,16},5->{5,6,7,14,15},6->{5,6,7,14 ,15},7->{5,6,7,14,15},8->{9,12},9->{9,12},10->{10,11},11->{8,13},12->{11},13->{1,20,21,22},14->{8,13},15->{8 ,13},16->{14,15},17->{1,20,21,22},18->{16},19->{16},20->{},21->{},22->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [4,5,6,7,10] * 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) -> f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 1. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 1 + B] (?,1) 2. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,C,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 + S && A >= D] (?,1) 3. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,S,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [S >= C && A >= D] (?,1) 8. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= K] (?,1) 9. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,1 + D,E,F,G,H,I,J + S*T,K,L,M,N,O,P,Q,R) [A >= D] (?,1) 11. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N,O,P,Q,R) [D >= 1 + A] (?,1) 12. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f62(A,B,C,D,E,F,G,H,I,J,K,S,M,N,O,P,Q,R) [J >= T*U && T + T*U >= 1 + J && T >= S && J >= U*V && U*V + V >= 1 + J && S >= V && D >= 1 + A] (?,1) 13. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [K >= 1 + A] (?,1) 14. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,S,T,T,P,Q,R) [D >= 1 + A] (?,1) 15. f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,-1*S,T,S,R) [D >= 1 + A] (?,1) 16. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [D >= 1 + A] (?,1) 17. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0) [D >= 1 + A && C = 0] (?,1) 18. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + C && D >= 1 + A] (?,1) 19. f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 && D >= 1 + A] (?,1) 20. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && 0 >= 1 + S] (?,1) 21. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && S >= 1] (?,1) 22. f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A] (?,1) Signature: {(f1,18);(f2,18);(f26,18);(f32,18);(f5,18);(f52,18);(f55,18);(f62,18);(f9,18)} Flow Graph: [0->{1,20,21,22},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11} ,13->{1,20,21,22},14->{8,13},15->{8,13},16->{14,15},17->{1,20,21,22},18->{16},19->{16},20->{},21->{},22->{}] + 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) -> f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 1 + B] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,C,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 + S && A >= D] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,S,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [S >= C && A >= D] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= K] f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,1 + D,E,F,G,H,I,J + S*T,K,L,M,N,O,P,Q,R) [A >= D] f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N,O,P,Q,R) [D >= 1 + A] f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f62(A,B,C,D,E,F,G,H,I,J,K,S,M,N,O,P,Q,R) [J >= T*U && T + T*U >= 1 + J && T >= S && J >= U*V && U*V + V >= 1 + J && S >= V && D >= 1 + A] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [K >= 1 + A] f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,S,T,T,P,Q,R) [D >= 1 + A] f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,-1*S,T,S,R) [D >= 1 + A] f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [D >= 1 + A] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0) [D >= 1 + A && C = 0] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + C && D >= 1 + A] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 && D >= 1 + A] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && 0 >= 1 + S] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && S >= 1] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A] Signature: {(f1,18);(f2,18);(f26,18);(f32,18);(f5,18);(f52,18);(f55,18);(f62,18);(f9,18)} Rule Graph: [0->{1,20,21,22},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11} ,13->{1,20,21,22},14->{8,13},15->{8,13},16->{14,15},17->{1,20,21,22},18->{16},19->{16},20->{},21->{},22->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,8,9,11,12,13,14,15,16,17,18,19,20,21,22] | `- p:[1,13,11,12,8,14,16,18,2,3,19,15,9,17] c: [8] | +- p:[9] c: [9] | `- p:[1,13,14,16,18,2,3,19,15,17] c: [2] | `- p:[1,13,14,16,18,3,19,15,17] c: [3,13,14,15,16,18,19] | `- p:[1,17] c: [1,17] * 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) -> f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 1 + B] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,C,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 + S && A >= D] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f9(A,B,S,1 + D,C,S,S,H,I,J,K,L,M,N,O,P,Q,R) [S >= C && A >= D] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= K] f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f55(A,B,C,1 + D,E,F,G,H,I,J + S*T,K,L,M,N,O,P,Q,R) [A >= D] f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,1 + K,L,M,N,O,P,Q,R) [D >= 1 + A] f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f62(A,B,C,D,E,F,G,H,I,J,K,S,M,N,O,P,Q,R) [J >= T*U && T + T*U >= 1 + J && T >= S && J >= U*V && U*V + V >= 1 + J && S >= V && D >= 1 + A] f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [K >= 1 + A] f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,S,T,T,P,Q,R) [D >= 1 + A] f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,-1*S,T,S,R) [D >= 1 + A] f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f32(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [D >= 1 + A] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f5(A,1 + B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,0) [D >= 1 + A && C = 0] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + C && D >= 1 + A] f9(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [C >= 1 && D >= 1 + A] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && 0 >= 1 + S] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A && S >= 1] f5(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= A] Signature: {(f1,18);(f2,18);(f26,18);(f32,18);(f5,18);(f52,18);(f55,18);(f62,18);(f9,18)} Rule Graph: [0->{1,20,21,22},1->{2,3,17},2->{2,3,17,18,19},3->{2,3,17,18,19},8->{9,12},9->{9,12},11->{8,13},12->{11} ,13->{1,20,21,22},14->{8,13},15->{8,13},16->{14,15},17->{1,20,21,22},18->{16},19->{16},20->{},21->{},22->{}] ,We construct a looptree: P: [0,1,2,3,8,9,11,12,13,14,15,16,17,18,19,20,21,22] | `- p:[1,13,11,12,8,14,16,18,2,3,19,15,9,17] c: [8] | +- p:[9] c: [9] | `- p:[1,13,14,16,18,2,3,19,15,17] c: [2] | `- p:[1,13,14,16,18,3,19,15,17] c: [3,13,14,15,16,18,19] | `- p:[1,17] c: [1,17]) + Applied Processor: CloseWith True + Details: () YES