NO * Step 1: UnsatPaths NO + Considered Problem: Rules: 0. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [A >= 1] (?,1) 1. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= B] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f10(A,B,R,S,0,1,0,H,I,J,K,L,M,N,O,P,Q) [R >= 1 && S >= 0] (1,1) 3. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f14(A,B,C,D,E,F,G,1,I,J,K,L,M,N,O,P,Q) [C >= 1 + G && 0 >= G] (?,1) 4. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f14(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q) [C >= 1 + G && G >= 1] (?,1) 5. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,K,L,M,N,O,P,Q) [R >= 0 && 0 >= I && 1 >= R] (?,1) 6. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,K,L,M,N,O,P,Q) [R >= 0 && I >= 2 && 1 >= R] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,K,L,M,N,O,P,Q) [0 >= J && 1 >= R && R >= 0] (?,1) 8. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,1,M,M,N,O,P,Q) [1 + G >= C && 1 >= R && R >= 0] (?,1) 9. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,0,M,M,N,O,P,Q) [C >= 2 + G && 1 >= R && R >= 0] (?,1) 10. f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [J >= 1 && 0 >= D && 0 >= E] (?,1) 11. f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [J >= 1 && 0 >= D && E = 1] (?,1) 12. f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,R,0,1 + F,G,H,I,J,K,L,M,N,O,P,Q) [E >= 2 && 0 >= D && R >= 0] (?,1) 13. f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,-1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [D >= 1] (?,1) 14. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(H,K,C,D,E,F,G,H,I,J,K,L,M,1,L,P,Q) [N >= 1 && J >= 1] (?,1) 15. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(H,K,C,D,E,F,G,H,I,J,K,L,M,1,L,L,Q) [0 >= N && J >= 1] (?,1) 16. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,O,Q) [0 >= 1 + A && O = P] (?,1) 17. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,O,Q) [A >= 1 && O = P] (?,1) 18. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f47(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,O,Q) [A = 0 && O = P] (?,1) 19. f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1) [B = 0] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= 1 + B] (?,1) 21. f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [B >= 1] (?,1) 22. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,2) [0 >= B && 0 >= A] (?,1) 23. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [B >= 1 && 0 >= A] (?,1) 24. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3) [B >= 1] (?,1) 25. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,P,Q) [R >= 0 && O >= 1 + P && 1 >= R] (?,1) 26. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,P,Q) [R >= 0 && P >= 1 + O && 1 >= R] (?,1) 27. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,0,Q) [R >= 0 && P >= 1 && 1 >= R] (?,1) 28. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,1,Q) [R >= 0 && 0 >= P && 1 >= R] (?,1) 29. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= E && 0 >= D && I >= 1] (?,1) 30. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= D && I >= 1 && E = 1] (?,1) 31. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,R,0,1 + F,G,H,I,J,K,L,M,N,O,P,Q) [E >= 2 && 0 >= D && R >= 0] (?,1) 32. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,-1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [D >= 1] (?,1) 33. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f10(A,B,C,D,E,F,1 + G,H,1,J,K,L,0,N,O,P,Q) [M >= 1 && I = 1] (?,1) 34. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f10(A,B,C,D,E,F,1 + G,H,1,J,K,L,1,N,O,P,Q) [0 >= M && I = 1] (?,1) 35. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f79(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [G >= C] (?,1) Signature: {(f0,17) ;(f10,17) ;(f14,17) ;(f22,17) ;(f26,17) ;(f41,17) ;(f43,17) ;(f45,17) ;(f47,17) ;(f51,17) ;(f58,17) ;(f62,17) ;(f79,17)} Flow Graph: [0->{1,24},1->{27,28},2->{3,4,35},3->{8,9},4->{8,9},5->{10,11,12,13},6->{10,11,12,13},7->{10,11,12,13} ,8->{10,11,12,13},9->{10,11,12,13},10->{7,14,15},11->{7,14,15},12->{7,14,15},13->{7,14,15},14->{16,17,18,25 ,26},15->{16,17,18,25,26},16->{19,20,21},17->{19,20,21},18->{0,22,23},19->{27,28},20->{0,22,23},21->{0,22 ,23},22->{27,28},23->{1,24},24->{27,28},25->{29,30,31,32},26->{29,30,31,32},27->{29,30,31,32},28->{29,30,31 ,32},29->{5,6,33,34},30->{5,6,33,34},31->{5,6,33,34},32->{5,6,33,34},33->{3,4,35},34->{3,4,35},35->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,4) ,(2,35) ,(10,7) ,(11,7) ,(15,25) ,(15,26) ,(18,0) ,(20,23) ,(21,22) ,(23,1) ,(29,5) ,(30,5)] * Step 2: FromIts NO + Considered Problem: Rules: 0. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [A >= 1] (?,1) 1. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= B] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f10(A,B,R,S,0,1,0,H,I,J,K,L,M,N,O,P,Q) [R >= 1 && S >= 0] (1,1) 3. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f14(A,B,C,D,E,F,G,1,I,J,K,L,M,N,O,P,Q) [C >= 1 + G && 0 >= G] (?,1) 4. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f14(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q) [C >= 1 + G && G >= 1] (?,1) 5. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,K,L,M,N,O,P,Q) [R >= 0 && 0 >= I && 1 >= R] (?,1) 6. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,K,L,M,N,O,P,Q) [R >= 0 && I >= 2 && 1 >= R] (?,1) 7. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,K,L,M,N,O,P,Q) [0 >= J && 1 >= R && R >= 0] (?,1) 8. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,1,M,M,N,O,P,Q) [1 + G >= C && 1 >= R && R >= 0] (?,1) 9. f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,0,M,M,N,O,P,Q) [C >= 2 + G && 1 >= R && R >= 0] (?,1) 10. f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [J >= 1 && 0 >= D && 0 >= E] (?,1) 11. f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [J >= 1 && 0 >= D && E = 1] (?,1) 12. f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,R,0,1 + F,G,H,I,J,K,L,M,N,O,P,Q) [E >= 2 && 0 >= D && R >= 0] (?,1) 13. f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,-1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [D >= 1] (?,1) 14. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(H,K,C,D,E,F,G,H,I,J,K,L,M,1,L,P,Q) [N >= 1 && J >= 1] (?,1) 15. f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(H,K,C,D,E,F,G,H,I,J,K,L,M,1,L,L,Q) [0 >= N && J >= 1] (?,1) 16. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,O,Q) [0 >= 1 + A && O = P] (?,1) 17. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,O,Q) [A >= 1 && O = P] (?,1) 18. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f47(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,O,Q) [A = 0 && O = P] (?,1) 19. f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1) [B = 0] (?,1) 20. f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= 1 + B] (?,1) 21. f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [B >= 1] (?,1) 22. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,2) [0 >= B && 0 >= A] (?,1) 23. f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [B >= 1 && 0 >= A] (?,1) 24. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3) [B >= 1] (?,1) 25. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,P,Q) [R >= 0 && O >= 1 + P && 1 >= R] (?,1) 26. f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,P,Q) [R >= 0 && P >= 1 + O && 1 >= R] (?,1) 27. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,0,Q) [R >= 0 && P >= 1 && 1 >= R] (?,1) 28. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,1,Q) [R >= 0 && 0 >= P && 1 >= R] (?,1) 29. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= E && 0 >= D && I >= 1] (?,1) 30. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= D && I >= 1 && E = 1] (?,1) 31. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,R,0,1 + F,G,H,I,J,K,L,M,N,O,P,Q) [E >= 2 && 0 >= D && R >= 0] (?,1) 32. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,-1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [D >= 1] (?,1) 33. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f10(A,B,C,D,E,F,1 + G,H,1,J,K,L,0,N,O,P,Q) [M >= 1 && I = 1] (?,1) 34. f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f10(A,B,C,D,E,F,1 + G,H,1,J,K,L,1,N,O,P,Q) [0 >= M && I = 1] (?,1) 35. f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f79(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [G >= C] (?,1) Signature: {(f0,17) ;(f10,17) ;(f14,17) ;(f22,17) ;(f26,17) ;(f41,17) ;(f43,17) ;(f45,17) ;(f47,17) ;(f51,17) ;(f58,17) ;(f62,17) ;(f79,17)} Flow Graph: [0->{1,24},1->{27,28},2->{3},3->{8,9},4->{8,9},5->{10,11,12,13},6->{10,11,12,13},7->{10,11,12,13},8->{10 ,11,12,13},9->{10,11,12,13},10->{14,15},11->{14,15},12->{7,14,15},13->{7,14,15},14->{16,17,18,25,26},15->{16 ,17,18},16->{19,20,21},17->{19,20,21},18->{22,23},19->{27,28},20->{0,22},21->{0,23},22->{27,28},23->{24} ,24->{27,28},25->{29,30,31,32},26->{29,30,31,32},27->{29,30,31,32},28->{29,30,31,32},29->{6,33,34},30->{6,33 ,34},31->{5,6,33,34},32->{5,6,33,34},33->{3,4,35},34->{3,4,35},35->{}] + Applied Processor: FromIts + Details: () * Step 3: CloseWith NO + Considered Problem: Rules: f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [A >= 1] f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= B] f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f10(A,B,R,S,0,1,0,H,I,J,K,L,M,N,O,P,Q) [R >= 1 && S >= 0] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f14(A,B,C,D,E,F,G,1,I,J,K,L,M,N,O,P,Q) [C >= 1 + G && 0 >= G] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f14(A,B,C,D,E,F,G,0,I,J,K,L,M,N,O,P,Q) [C >= 1 + G && G >= 1] f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,K,L,M,N,O,P,Q) [R >= 0 && 0 >= I && 1 >= R] f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,K,L,M,N,O,P,Q) [R >= 0 && I >= 2 && 1 >= R] f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,K,L,M,N,O,P,Q) [0 >= J && 1 >= R && R >= 0] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,1,M,M,N,O,P,Q) [1 + G >= C && 1 >= R && R >= 0] f14(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f22(A,B,C,D,E,F,G,H,I,R,0,M,M,N,O,P,Q) [C >= 2 + G && 1 >= R && R >= 0] f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [J >= 1 && 0 >= D && 0 >= E] f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [J >= 1 && 0 >= D && E = 1] f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,R,0,1 + F,G,H,I,J,K,L,M,N,O,P,Q) [E >= 2 && 0 >= D && R >= 0] f22(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f26(A,B,C,-1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [D >= 1] f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(H,K,C,D,E,F,G,H,I,J,K,L,M,1,L,P,Q) [N >= 1 && J >= 1] f26(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f41(H,K,C,D,E,F,G,H,I,J,K,L,M,1,L,L,Q) [0 >= N && J >= 1] f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,O,Q) [0 >= 1 + A && O = P] f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,O,Q) [A >= 1 && O = P] f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f47(0,B,C,D,E,F,G,H,I,J,K,L,M,N,O,O,Q) [A = 0 && O = P] f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,1) [B = 0] f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= 1 + B] f43(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [B >= 1] f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,2) [0 >= B && 0 >= A] f47(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [B >= 1 && 0 >= A] f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,3) [B >= 1] f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,P,Q) [R >= 0 && O >= 1 + P && 1 >= R] f41(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,P,Q) [R >= 0 && P >= 1 + O && 1 >= R] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,0,Q) [R >= 0 && P >= 1 && 1 >= R] f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f58(A,B,C,D,E,F,G,H,R,J,K,L,M,N,O,1,Q) [R >= 0 && 0 >= P && 1 >= R] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= E && 0 >= D && I >= 1] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,D,1 + E,F,G,H,I,J,K,L,M,N,O,P,Q) [0 >= D && I >= 1 && E = 1] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,R,0,1 + F,G,H,I,J,K,L,M,N,O,P,Q) [E >= 2 && 0 >= D && R >= 0] f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f62(A,B,C,-1 + D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [D >= 1] f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f10(A,B,C,D,E,F,1 + G,H,1,J,K,L,0,N,O,P,Q) [M >= 1 && I = 1] f62(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f10(A,B,C,D,E,F,1 + G,H,1,J,K,L,1,N,O,P,Q) [0 >= M && I = 1] f10(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) -> f79(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q) [G >= C] Signature: {(f0,17) ;(f10,17) ;(f14,17) ;(f22,17) ;(f26,17) ;(f41,17) ;(f43,17) ;(f45,17) ;(f47,17) ;(f51,17) ;(f58,17) ;(f62,17) ;(f79,17)} Rule Graph: [0->{1,24},1->{27,28},2->{3},3->{8,9},4->{8,9},5->{10,11,12,13},6->{10,11,12,13},7->{10,11,12,13},8->{10 ,11,12,13},9->{10,11,12,13},10->{14,15},11->{14,15},12->{7,14,15},13->{7,14,15},14->{16,17,18,25,26},15->{16 ,17,18},16->{19,20,21},17->{19,20,21},18->{22,23},19->{27,28},20->{0,22},21->{0,23},22->{27,28},23->{24} ,24->{27,28},25->{29,30,31,32},26->{29,30,31,32},27->{29,30,31,32},28->{29,30,31,32},29->{6,33,34},30->{6,33 ,34},31->{5,6,33,34},32->{5,6,33,34},33->{3,4,35},34->{3,4,35},35->{}] + Applied Processor: CloseWith False + Details: () NO