NO * Step 1: UnsatPaths NO + Considered Problem: Rules: 0. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1] (?,1) 1. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [0 >= D && 0 >= A] (?,1) 2. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [D >= 1 && 0 >= A] (?,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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [C >= E] (?,1) 4. 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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [Z >= 1 && E >= 1 + C] (?,1) 5. 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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [E >= 1 + C && 0 >= Z && 0 >= A1] (?,1) 6. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [H >= 1 + I] (?,1) 7. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H && 1 + J = 0] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H && 0 >= 2 + J] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H && J >= 0] (?,1) 10. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H] (?,1) 11. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,B1,B1,P,Q,R,S,T,U,V,W,X,Y) [0 >= A1 && H >= 1 + I && 0 >= Z] (?,1) 12. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,C1,C1,B1,Q,R,S,T,U,V,W,X,Y) [0 >= B1 && A1 >= 1 && H >= 1 + I && 0 >= Z] (?,1) 13. 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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [O >= 0 && 0 >= Z && Q = 3] (?,1) 14. 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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [O >= 0 && Z >= 2 && Q = 3] (?,1) 15. 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [O >= 0 && 2 >= Q] (?,1) 16. 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [O >= 0 && Q >= 4] (?,1) 17. 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,1,Z,T,U,V,W,X,Y) [O >= 0 && Q = 3] (?,1) 18. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,S,Z,U,V,W,X,Y) [10 >= S] (?,1) 19. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,10,Z,U,V,W,X,Y) [S >= 11] (?,1) 20. f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(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) [0 >= 1 + O] (?,1) 21. 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) -> f26(A,B,1 + C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [E >= 1 + C && 0 >= Z && A1 >= 1] (?,1) 22. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [H >= 1 + I && Z >= 1] (?,1) 23. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,A1,N,O,B1,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 && A1 >= 1 && H >= 1 + I && 0 >= Z] (?,1) 24. 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) -> f26(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) [0 >= 1 + O] (?,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,L,K,L,M,N,O,P,Q,R,S,T,1 + U,V,W,X,Y) [O >= 0] (?,1) 26. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) True (?,1) 27. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [0 >= U] (?,1) 28. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(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) [U >= 1] (?,1) 29. f73(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) True (?,1) 30. 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,3,1,B1,C1) [A1 >= 0 && B1 >= 1 && V = 3] (1,1) 31. 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [2 >= V && A1 >= 0 && B1 >= 1] (1,1) 32. 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [V >= 4 && A1 >= 0 && B1 >= 1] (1,1) Signature: {(f0,25) ;(f20,25) ;(f26,25) ;(f33,25) ;(f39,25) ;(f52,25) ;(f59,25) ;(f63,25) ;(f68,25) ;(f71,25) ;(f73,25) ;(f76,25)} Flow Graph: [0->{3,4,5,21},1->{3,4,5,21},2->{3,4,5,21},3->{27,28},4->{6,7,8,9},5->{6,7,8,9},6->{10,11,12,22,23},7->{10 ,11,12,22,23},8->{6,7,8,9},9->{6,7,8,9},10->{27,28},11->{13,14,15,16,17,24},12->{13,14,15,16,17,24},13->{27 ,28},14->{27,28},15->{18,19},16->{18,19},17->{18,19},18->{20,25},19->{20,25},20->{3,4,5,21},21->{3,4,5,21} ,22->{3,4,5,21},23->{3,4,5,21},24->{3,4,5,21},25->{3,4,5,21},26->{26},27->{26},28->{26},29->{},30->{0,1,2} ,31->{0,1,2},32->{0,1,2}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(6,10) ,(7,11) ,(7,12) ,(7,22) ,(7,23) ,(8,6) ,(8,7) ,(8,9) ,(9,6) ,(9,7) ,(9,8)] * Step 2: UnreachableRules NO + Considered Problem: Rules: 0. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1] (?,1) 1. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [0 >= D && 0 >= A] (?,1) 2. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [D >= 1 && 0 >= A] (?,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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [C >= E] (?,1) 4. 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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [Z >= 1 && E >= 1 + C] (?,1) 5. 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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [E >= 1 + C && 0 >= Z && 0 >= A1] (?,1) 6. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [H >= 1 + I] (?,1) 7. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H && 1 + J = 0] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H && 0 >= 2 + J] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H && J >= 0] (?,1) 10. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H] (?,1) 11. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,B1,B1,P,Q,R,S,T,U,V,W,X,Y) [0 >= A1 && H >= 1 + I && 0 >= Z] (?,1) 12. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,C1,C1,B1,Q,R,S,T,U,V,W,X,Y) [0 >= B1 && A1 >= 1 && H >= 1 + I && 0 >= Z] (?,1) 13. 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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [O >= 0 && 0 >= Z && Q = 3] (?,1) 14. 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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [O >= 0 && Z >= 2 && Q = 3] (?,1) 15. 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [O >= 0 && 2 >= Q] (?,1) 16. 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [O >= 0 && Q >= 4] (?,1) 17. 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,1,Z,T,U,V,W,X,Y) [O >= 0 && Q = 3] (?,1) 18. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,S,Z,U,V,W,X,Y) [10 >= S] (?,1) 19. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,10,Z,U,V,W,X,Y) [S >= 11] (?,1) 20. f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(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) [0 >= 1 + O] (?,1) 21. 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) -> f26(A,B,1 + C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [E >= 1 + C && 0 >= Z && A1 >= 1] (?,1) 22. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [H >= 1 + I && Z >= 1] (?,1) 23. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,A1,N,O,B1,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 && A1 >= 1 && H >= 1 + I && 0 >= Z] (?,1) 24. 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) -> f26(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) [0 >= 1 + O] (?,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,L,K,L,M,N,O,P,Q,R,S,T,1 + U,V,W,X,Y) [O >= 0] (?,1) 26. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) True (?,1) 27. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [0 >= U] (?,1) 28. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(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) [U >= 1] (?,1) 29. f73(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f76(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) True (?,1) 30. 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,3,1,B1,C1) [A1 >= 0 && B1 >= 1 && V = 3] (1,1) 31. 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [2 >= V && A1 >= 0 && B1 >= 1] (1,1) 32. 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [V >= 4 && A1 >= 0 && B1 >= 1] (1,1) Signature: {(f0,25) ;(f20,25) ;(f26,25) ;(f33,25) ;(f39,25) ;(f52,25) ;(f59,25) ;(f63,25) ;(f68,25) ;(f71,25) ;(f73,25) ;(f76,25)} Flow Graph: [0->{3,4,5,21},1->{3,4,5,21},2->{3,4,5,21},3->{27,28},4->{6,7,8,9},5->{6,7,8,9},6->{11,12,22,23},7->{10} ,8->{8},9->{9},10->{27,28},11->{13,14,15,16,17,24},12->{13,14,15,16,17,24},13->{27,28},14->{27,28},15->{18 ,19},16->{18,19},17->{18,19},18->{20,25},19->{20,25},20->{3,4,5,21},21->{3,4,5,21},22->{3,4,5,21},23->{3,4,5 ,21},24->{3,4,5,21},25->{3,4,5,21},26->{26},27->{26},28->{26},29->{},30->{0,1,2},31->{0,1,2},32->{0,1,2}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [29] * Step 3: FromIts NO + Considered Problem: Rules: 0. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [A >= 1] (?,1) 1. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [0 >= D && 0 >= A] (?,1) 2. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [D >= 1 && 0 >= A] (?,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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [C >= E] (?,1) 4. 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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [Z >= 1 && E >= 1 + C] (?,1) 5. 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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [E >= 1 + C && 0 >= Z && 0 >= A1] (?,1) 6. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [H >= 1 + I] (?,1) 7. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H && 1 + J = 0] (?,1) 8. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H && 0 >= 2 + J] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H && J >= 0] (?,1) 10. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [I >= H] (?,1) 11. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,B1,B1,P,Q,R,S,T,U,V,W,X,Y) [0 >= A1 && H >= 1 + I && 0 >= Z] (?,1) 12. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,C1,C1,B1,Q,R,S,T,U,V,W,X,Y) [0 >= B1 && A1 >= 1 && H >= 1 + I && 0 >= Z] (?,1) 13. 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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [O >= 0 && 0 >= Z && Q = 3] (?,1) 14. 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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W,X,Y) [O >= 0 && Z >= 2 && Q = 3] (?,1) 15. 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [O >= 0 && 2 >= Q] (?,1) 16. 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W,X,Y) [O >= 0 && Q >= 4] (?,1) 17. 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,1,Z,T,U,V,W,X,Y) [O >= 0 && Q = 3] (?,1) 18. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,S,Z,U,V,W,X,Y) [10 >= S] (?,1) 19. f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,10,Z,U,V,W,X,Y) [S >= 11] (?,1) 20. f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(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) [0 >= 1 + O] (?,1) 21. 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) -> f26(A,B,1 + C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [E >= 1 + C && 0 >= Z && A1 >= 1] (?,1) 22. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [H >= 1 + I && Z >= 1] (?,1) 23. f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,A1,N,O,B1,Q,R,S,T,U,V,W,X,Y) [B1 >= 1 && A1 >= 1 && H >= 1 + I && 0 >= Z] (?,1) 24. 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) -> f26(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) [0 >= 1 + O] (?,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,L,K,L,M,N,O,P,Q,R,S,T,1 + U,V,W,X,Y) [O >= 0] (?,1) 26. f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) True (?,1) 27. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) [0 >= U] (?,1) 28. f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(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) [U >= 1] (?,1) 30. 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,3,1,B1,C1) [A1 >= 0 && B1 >= 1 && V = 3] (1,1) 31. 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [2 >= V && A1 >= 0 && B1 >= 1] (1,1) 32. 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V,1,B1,C1) [V >= 4 && A1 >= 0 && B1 >= 1] (1,1) Signature: {(f0,25) ;(f20,25) ;(f26,25) ;(f33,25) ;(f39,25) ;(f52,25) ;(f59,25) ;(f63,25) ;(f68,25) ;(f71,25) ;(f73,25) ;(f76,25)} Flow Graph: [0->{3,4,5,21},1->{3,4,5,21},2->{3,4,5,21},3->{27,28},4->{6,7,8,9},5->{6,7,8,9},6->{11,12,22,23},7->{10} ,8->{8},9->{9},10->{27,28},11->{13,14,15,16,17,24},12->{13,14,15,16,17,24},13->{27,28},14->{27,28},15->{18 ,19},16->{18,19},17->{18,19},18->{20,25},19->{20,25},20->{3,4,5,21},21->{3,4,5,21},22->{3,4,5,21},23->{3,4,5 ,21},24->{3,4,5,21},25->{3,4,5,21},26->{26},27->{26},28->{26},30->{0,1,2},31->{0,1,2},32->{0,1,2}] + Applied Processor: FromIts + Details: () * Step 4: CloseWith NO + Considered Problem: Rules: f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W,X ,Y) [A >= 1] f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,1,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [0 >= D && 0 >= A] f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,0,D,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [D >= 1 && 0 >= A] 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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [C >= E] 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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W,X ,Y) [Z >= 1 && E >= 1 + C] 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) -> f33(A,B,C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V ,W,X ,Y) [E >= 1 + C && 0 >= Z && 0 >= A1] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [H >= 1 + I] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f39(A,B,C,D,E,F,G,H,I,-1,K,L,M,N,O,P,Q,R,S,T,U,V ,W,X ,Y) [I >= H && 1 + J = 0] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U ,V,W,X ,Y) [I >= H && 0 >= 2 + J] f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f33(A,B,C,D,E,F,G,H,1 + I,J,K,L,M,N,O,P,Q,R,S,T,U ,V,W,X ,Y) [I >= H && J >= 0] f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [I >= H] f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,B1,B1,P,Q,R,S,T,U ,V,W,X ,Y) [0 >= A1 && H >= 1 + I && 0 >= Z] f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f52(A,B,C,D,E,F,G,H,I,J,Z,Z,A1,C1,C1,B1,Q,R,S,T,U ,V,W,X ,Y) [0 >= B1 && A1 >= 1 && H >= 1 + I && 0 >= Z] 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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W ,X ,Y) [O >= 0 && 0 >= Z && Q = 3] 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) -> f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,Z,S,T,U,V,W ,X ,Y) [O >= 0 && Z >= 2 && Q = 3] 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W ,X ,Y) [O >= 0 && 2 >= Q] 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,Z,T,U,V,W ,X ,Y) [O >= 0 && Q >= 4] 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) -> f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3,1,Z,T,U,V,W ,X ,Y) [O >= 0 && Q = 3] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,S,Z,U,V,W ,X ,Y) [10 >= S] f59(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,Z,P,Q,R,10,Z,U,V ,W,X ,Y) [S >= 11] f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(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) [0 >= 1 + O] 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) -> f26(A,B,1 + C,D,E,Z,A1,H,I,J,K,L,M,N,O,P,Q,R,S,T ,U,V,W,X ,Y) [E >= 1 + C && 0 >= Z && A1 >= 1] f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,M,N,O,P,Q,R,S,T,U ,V,W,X ,Y) [H >= 1 + I && Z >= 1] f39(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,J,Z,Z,A1,N,O,B1,Q,R,S,T ,U,V,W,X ,Y) [B1 >= 1 && A1 >= 1 && H >= 1 + I && 0 >= Z] 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) -> f26(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) [0 >= 1 + O] f63(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f26(A,B,1 + C,D,E,F,G,H,I,L,K,L,M,N,O,P,Q,R,S,T ,1 + U,V,W,X ,Y) [O >= 0] f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) True f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W ,X ,Y) [0 >= U] f68(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y) -> f71(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) [U >= 1] 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,3 ,1,B1 ,C1) [A1 >= 0 && B1 >= 1 && V = 3] 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V ,1,B1 ,C1) [2 >= V && A1 >= 0 && B1 >= 1] 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) -> f20(C1,B,C,A1,Z,F,G,H,0,J,K,L,M,N,O,P,Q,R,S,T,0,V ,1,B1 ,C1) [V >= 4 && A1 >= 0 && B1 >= 1] Signature: {(f0,25) ;(f20,25) ;(f26,25) ;(f33,25) ;(f39,25) ;(f52,25) ;(f59,25) ;(f63,25) ;(f68,25) ;(f71,25) ;(f73,25) ;(f76,25)} Rule Graph: [0->{3,4,5,21},1->{3,4,5,21},2->{3,4,5,21},3->{27,28},4->{6,7,8,9},5->{6,7,8,9},6->{11,12,22,23},7->{10} ,8->{8},9->{9},10->{27,28},11->{13,14,15,16,17,24},12->{13,14,15,16,17,24},13->{27,28},14->{27,28},15->{18 ,19},16->{18,19},17->{18,19},18->{20,25},19->{20,25},20->{3,4,5,21},21->{3,4,5,21},22->{3,4,5,21},23->{3,4,5 ,21},24->{3,4,5,21},25->{3,4,5,21},26->{26},27->{26},28->{26},30->{0,1,2},31->{0,1,2},32->{0,1,2}] + Applied Processor: CloseWith False + Details: () NO