MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. 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,Z,A1,B1,C1,D1,E1) -> f78(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,Z,A1,B1,C1,D1,E1) [A = 0] (?,1) 1. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + B] (?,1) 2. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B >= 1] (?,1) 3. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + E] (?,1) 4. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E >= 1] (?,1) 5. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + I] (?,1) 6. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I >= 1] (?,1) 7. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 8. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 9. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [0 >= 1 + M] (?,1) 10. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [M >= 1] (?,1) 11. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [M = 0] (?,1) 12. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + A] (?,1) 13. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [A >= 1] (?,1) 14. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [N >= 0] (?,1) 15. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 2 + N] (?,1) 16. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I = 0] (?,1) 17. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 18. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 19. 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,B1,C1,D1,E1) -> f91(A,0,1,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B = 0] (?,1) 20. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E = 0] (?,1) 21. f93(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f95(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 22. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 23. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 24. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 25. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 26. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 27. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,0,0,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 28. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 29. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 30. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1 && 1 + N = 0] (?,1) 31. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1 && 1 + N = 0] (?,1) 32. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1) [1 + N = 0] (?,1) 33. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + V] (?,1) 34. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [V >= 1] (?,1) 35. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,Y,Z,A1,B1,C1,D1,E1) [V = 0] (?,1) 36. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 37. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 38. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,F1,G1,G1,H1,I1,E1) [0 >= G1] (1,1) 39. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,5,G1,G1,H1,I1,J1) [G1 >= 1 && 4 >= J1] (1,1) 40. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,I1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,J1,W,X,F1,G1,H1,H1,I1,J1,G1) [H1 >= 1 && 20 >= G1 && G1 >= 5] (1,1) 41. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,20,G1,G1,H1,I1,J1) [G1 >= 1 && J1 >= 21] (1,1) Signature: {(f0,31) ;(f34,31) ;(f39,31) ;(f44,31) ;(f51,31) ;(f59,31) ;(f64,31) ;(f75,31) ;(f76,31) ;(f78,31) ;(f82,31) ;(f91,31) ;(f93,31) ;(f95,31)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37},4->{33,34,35,36,37},5->{25,26,27,28,29},6->{25,26 ,27,28,29},7->{17,22,23},8->{17,22,23},9->{0,12,13},10->{0,12,13},11->{7,8,24},12->{7,8,24},13->{7,8,24} ,14->{33,34,35,36,37},15->{33,34,35,36,37},16->{33,34,35,36,37},17->{33,34,35,36,37},18->{18},19->{18} ,20->{18},21->{},22->{33,34,35,36,37},23->{33,34,35,36,37},24->{17,22,23},25->{17,22,23},26->{17,22,23} ,27->{7,8,24},28->{9,10,11},29->{9,10,11},30->{5,6,16},31->{5,6,16},32->{33,34,35,36,37},33->{14,15,30,31 ,32},34->{14,15,30,31,32},35->{33,34,35,36,37},36->{18},37->{18},38->{18},39->{1,2,19},40->{1,2,19},41->{1,2 ,19}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. 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,Z,A1,B1,C1,D1,E1) -> f78(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,Z,A1,B1,C1,D1,E1) [A = 0] (?,1) 1. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + B] (1,1) 2. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B >= 1] (1,1) 3. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + E] (1,1) 4. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E >= 1] (1,1) 5. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + I] (?,1) 6. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I >= 1] (?,1) 7. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 8. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 9. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [0 >= 1 + M] (?,1) 10. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [M >= 1] (?,1) 11. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [M = 0] (?,1) 12. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + A] (?,1) 13. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [A >= 1] (?,1) 14. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [N >= 0] (?,1) 15. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 2 + N] (?,1) 16. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I = 0] (?,1) 17. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 18. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 19. 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,B1,C1,D1,E1) -> f91(A,0,1,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B = 0] (1,1) 20. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E = 0] (1,1) 21. f93(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f95(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (1,1) 22. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 23. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 24. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 25. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 26. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 27. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,0,0,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 28. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 29. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 30. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1 && 1 + N = 0] (?,1) 31. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1 && 1 + N = 0] (?,1) 32. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1) [1 + N = 0] (?,1) 33. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + V] (?,1) 34. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [V >= 1] (?,1) 35. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,Y,Z,A1,B1,C1,D1,E1) [V = 0] (?,1) 36. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (1,1) 37. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (1,1) 38. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,F1,G1,G1,H1,I1,E1) [0 >= G1] (1,1) 39. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,5,G1,G1,H1,I1,J1) [G1 >= 1 && 4 >= J1] (1,1) 40. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,I1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,J1,W,X,F1,G1,H1,H1,I1,J1,G1) [H1 >= 1 && 20 >= G1 && G1 >= 5] (1,1) 41. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,20,G1,G1,H1,I1,J1) [G1 >= 1 && J1 >= 21] (1,1) Signature: {(f0,31) ;(f34,31) ;(f39,31) ;(f44,31) ;(f51,31) ;(f59,31) ;(f64,31) ;(f75,31) ;(f76,31) ;(f78,31) ;(f82,31) ;(f91,31) ;(f93,31) ;(f95,31)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37},4->{33,34,35,36,37},5->{25,26,27,28,29},6->{25,26 ,27,28,29},7->{17,22,23},8->{17,22,23},9->{0,12,13},10->{0,12,13},11->{7,8,24},12->{7,8,24},13->{7,8,24} ,14->{33,34,35,36,37},15->{33,34,35,36,37},16->{33,34,35,36,37},17->{33,34,35,36,37},18->{18},19->{18} ,20->{18},21->{},22->{33,34,35,36,37},23->{33,34,35,36,37},24->{17,22,23},25->{17,22,23},26->{17,22,23} ,27->{7,8,24},28->{9,10,11},29->{9,10,11},30->{5,6,16},31->{5,6,16},32->{33,34,35,36,37},33->{14,15,30,31 ,32},34->{14,15,30,31,32},35->{33,34,35,36,37},36->{18},37->{18},38->{18},39->{1,2,19},40->{1,2,19},41->{1,2 ,19}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(7,17) ,(7,23) ,(8,17) ,(8,22) ,(12,7) ,(12,24) ,(13,7) ,(13,24) ,(24,22) ,(24,23) ,(35,33) ,(35,34)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. 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,Z,A1,B1,C1,D1,E1) -> f78(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,Z,A1,B1,C1,D1,E1) [A = 0] (?,1) 1. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + B] (1,1) 2. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B >= 1] (1,1) 3. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + E] (1,1) 4. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E >= 1] (1,1) 5. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + I] (?,1) 6. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I >= 1] (?,1) 7. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 8. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 9. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [0 >= 1 + M] (?,1) 10. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [M >= 1] (?,1) 11. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [M = 0] (?,1) 12. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + A] (?,1) 13. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [A >= 1] (?,1) 14. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [N >= 0] (?,1) 15. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 2 + N] (?,1) 16. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I = 0] (?,1) 17. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 18. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 19. 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,B1,C1,D1,E1) -> f91(A,0,1,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B = 0] (1,1) 20. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E = 0] (1,1) 21. f93(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f95(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (1,1) 22. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 23. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 24. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 25. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 26. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 27. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,0,0,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 28. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 29. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 30. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1 && 1 + N = 0] (?,1) 31. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1 && 1 + N = 0] (?,1) 32. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1) [1 + N = 0] (?,1) 33. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + V] (?,1) 34. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [V >= 1] (?,1) 35. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,Y,Z,A1,B1,C1,D1,E1) [V = 0] (?,1) 36. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (1,1) 37. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (1,1) 38. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,F1,G1,G1,H1,I1,E1) [0 >= G1] (1,1) 39. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,5,G1,G1,H1,I1,J1) [G1 >= 1 && 4 >= J1] (1,1) 40. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,I1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,J1,W,X,F1,G1,H1,H1,I1,J1,G1) [H1 >= 1 && 20 >= G1 && G1 >= 5] (1,1) 41. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,20,G1,G1,H1,I1,J1) [G1 >= 1 && J1 >= 21] (1,1) Signature: {(f0,31) ;(f34,31) ;(f39,31) ;(f44,31) ;(f51,31) ;(f59,31) ;(f64,31) ;(f75,31) ;(f76,31) ;(f78,31) ;(f82,31) ;(f91,31) ;(f93,31) ;(f95,31)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37},4->{33,34,35,36,37},5->{25,26,27,28,29},6->{25,26 ,27,28,29},7->{22},8->{23},9->{0,12,13},10->{0,12,13},11->{7,8,24},12->{8},13->{8},14->{33,34,35,36,37} ,15->{33,34,35,36,37},16->{33,34,35,36,37},17->{33,34,35,36,37},18->{18},19->{18},20->{18},21->{},22->{33,34 ,35,36,37},23->{33,34,35,36,37},24->{17},25->{17,22,23},26->{17,22,23},27->{7,8,24},28->{9,10,11},29->{9,10 ,11},30->{5,6,16},31->{5,6,16},32->{33,34,35,36,37},33->{14,15,30,31,32},34->{14,15,30,31,32},35->{35,36,37} ,36->{18},37->{18},38->{18},39->{1,2,19},40->{1,2,19},41->{1,2,19}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [21] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. 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,Z,A1,B1,C1,D1,E1) -> f78(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,Z,A1,B1,C1,D1,E1) [A = 0] (?,1) 1. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + B] (1,1) 2. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B >= 1] (1,1) 3. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + E] (1,1) 4. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E >= 1] (1,1) 5. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + I] (?,1) 6. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I >= 1] (?,1) 7. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 8. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 9. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [0 >= 1 + M] (?,1) 10. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [M >= 1] (?,1) 11. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [M = 0] (?,1) 12. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + A] (?,1) 13. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [A >= 1] (?,1) 14. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [N >= 0] (?,1) 15. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 2 + N] (?,1) 16. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I = 0] (?,1) 17. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 18. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 19. 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,B1,C1,D1,E1) -> f91(A,0,1,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B = 0] (1,1) 20. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E = 0] (1,1) 22. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 23. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 24. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 25. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 26. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 27. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,0,0,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 28. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 29. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 30. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1 && 1 + N = 0] (?,1) 31. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1 && 1 + N = 0] (?,1) 32. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1) [1 + N = 0] (?,1) 33. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + V] (?,1) 34. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [V >= 1] (?,1) 35. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,Y,Z,A1,B1,C1,D1,E1) [V = 0] (?,1) 36. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (1,1) 37. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (1,1) 38. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,F1,G1,G1,H1,I1,E1) [0 >= G1] (1,1) 39. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,5,G1,G1,H1,I1,J1) [G1 >= 1 && 4 >= J1] (1,1) 40. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,I1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,J1,W,X,F1,G1,H1,H1,I1,J1,G1) [H1 >= 1 && 20 >= G1 && G1 >= 5] (1,1) 41. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,20,G1,G1,H1,I1,J1) [G1 >= 1 && J1 >= 21] (1,1) Signature: {(f0,31) ;(f34,31) ;(f39,31) ;(f44,31) ;(f51,31) ;(f59,31) ;(f64,31) ;(f75,31) ;(f76,31) ;(f78,31) ;(f82,31) ;(f91,31) ;(f93,31) ;(f95,31)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37},4->{33,34,35,36,37},5->{25,26,27,28,29},6->{25,26 ,27,28,29},7->{22},8->{23},9->{0,12,13},10->{0,12,13},11->{7,8,24},12->{8},13->{8},14->{33,34,35,36,37} ,15->{33,34,35,36,37},16->{33,34,35,36,37},17->{33,34,35,36,37},18->{18},19->{18},20->{18},22->{33,34,35,36 ,37},23->{33,34,35,36,37},24->{17},25->{17,22,23},26->{17,22,23},27->{7,8,24},28->{9,10,11},29->{9,10,11} ,30->{5,6,16},31->{5,6,16},32->{33,34,35,36,37},33->{14,15,30,31,32},34->{14,15,30,31,32},35->{35,36,37} ,36->{18},37->{18},38->{18},39->{1,2,19},40->{1,2,19},41->{1,2,19}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. 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,Z,A1,B1,C1,D1,E1) -> f78(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,Z,A1,B1,C1,D1,E1) [A = 0] (?,1) 1. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + B] (?,1) 2. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B >= 1] (?,1) 3. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + E] (?,1) 4. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E >= 1] (?,1) 5. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + I] (?,1) 6. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I >= 1] (?,1) 7. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 8. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 9. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [0 >= 1 + M] (?,1) 10. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [M >= 1] (?,1) 11. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [M = 0] (?,1) 12. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + A] (?,1) 13. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [A >= 1] (?,1) 14. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [N >= 0] (?,1) 15. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 2 + N] (?,1) 16. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I = 0] (?,1) 17. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 18. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 19. 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,B1,C1,D1,E1) -> f91(A,0,1,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B = 0] (?,1) 20. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E = 0] (?,1) 22. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 23. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 24. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 25. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 26. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 27. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,0,0,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 28. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 29. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 30. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1 && 1 + N = 0] (?,1) 31. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1 && 1 + N = 0] (?,1) 32. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1) [1 + N = 0] (?,1) 33. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + V] (?,1) 34. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [V >= 1] (?,1) 35. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,Y,Z,A1,B1,C1,D1,E1) [V = 0] (?,1) 36. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 37. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 38. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,F1,G1,G1,H1,I1,E1) [0 >= G1] (1,1) 39. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,5,G1,G1,H1,I1,J1) [G1 >= 1 && 4 >= J1] (1,1) 40. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,I1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,J1,W,X,F1,G1,H1,H1,I1,J1,G1) [H1 >= 1 && 20 >= G1 && G1 >= 5] (1,1) 41. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,20,G1,G1,H1,I1,J1) [G1 >= 1 && J1 >= 21] (1,1) 42. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) Signature: {(exitus616,31) ;(f0,31) ;(f34,31) ;(f39,31) ;(f44,31) ;(f51,31) ;(f59,31) ;(f64,31) ;(f75,31) ;(f76,31) ;(f78,31) ;(f82,31) ;(f91,31) ;(f93,31) ;(f95,31)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37},4->{33,34,35,36,37},5->{25,26,27,28,29},6->{25,26 ,27,28,29},7->{17,22,23},8->{17,22,23},9->{0,12,13},10->{0,12,13},11->{7,8,24},12->{7,8,24},13->{7,8,24} ,14->{33,34,35,36,37},15->{33,34,35,36,37},16->{33,34,35,36,37},17->{33,34,35,36,37},18->{18,42},19->{18,42} ,20->{18,42},22->{33,34,35,36,37},23->{33,34,35,36,37},24->{17,22,23},25->{17,22,23},26->{17,22,23},27->{7,8 ,24},28->{9,10,11},29->{9,10,11},30->{5,6,16},31->{5,6,16},32->{33,34,35,36,37},33->{14,15,30,31,32},34->{14 ,15,30,31,32},35->{33,34,35,36,37},36->{18,42},37->{18,42},38->{18,42},39->{1,2,19},40->{1,2,19},41->{1,2 ,19},42->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(7,17) ,(7,23) ,(8,17) ,(8,22) ,(12,7) ,(12,24) ,(13,7) ,(13,24) ,(24,22) ,(24,23) ,(35,33) ,(35,34)] * Step 6: Failure MAYBE + Considered Problem: Rules: 0. 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,Z,A1,B1,C1,D1,E1) -> f78(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,Z,A1,B1,C1,D1,E1) [A = 0] (?,1) 1. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + B] (?,1) 2. 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,B1,C1,D1,E1) -> f39(A,B,1,B,F1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B >= 1] (?,1) 3. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + E] (?,1) 4. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,E,10,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E >= 1] (?,1) 5. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + I] (?,1) 6. 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,Z,A1,B1,C1,D1,E1) -> f64(A,B,C,D,E,F,G,H,I,I,0,F1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I >= 1] (?,1) 7. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 8. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 9. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [0 >= 1 + M] (?,1) 10. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> 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,Z,A1,B1,C1,D1,E1) [M >= 1] (?,1) 11. f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,0,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [M = 0] (?,1) 12. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + A] (?,1) 13. 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,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [A >= 1] (?,1) 14. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [N >= 0] (?,1) 15. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 2 + N] (?,1) 16. 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,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [I = 0] (?,1) 17. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 18. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 19. 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,B1,C1,D1,E1) -> f91(A,0,1,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [B = 0] (?,1) 20. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [E = 0] (?,1) 22. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + K] (?,1) 23. f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K >= 1] (?,1) 24. f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [K = 0] (?,1) 25. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 26. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f82(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,F1,F1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 27. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f78(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,0,0,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) 28. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 29. f64(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f75(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,F1,F1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 30. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1 && 1 + N = 0] (?,1) 31. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f59(A,B,C,D,E,F,G,H,G1,J,K,L,M,-1,O,P,Q,R,S,F1,F1,V,W,X,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1 && 1 + N = 0] (?,1) 32. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1) [1 + N = 0] (?,1) 33. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + V] (?,1) 34. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,0,0,Y,Z,A1,B1,C1,D1,E1) [V >= 1] (?,1) 35. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f44(A,B,C,D,E,F,G,F1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,Y,Z,A1,B1,C1,D1,E1) [V = 0] (?,1) 36. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [0 >= 1 + F1] (?,1) 37. f44(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,F1,F1,Y,Z,A1,B1,C1,D1,E1) [F1 >= 1] (?,1) 38. 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,Z,A1,B1,C1,D1,E1) -> f91(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,F1,G1,G1,H1,I1,E1) [0 >= G1] (1,1) 39. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,5,G1,G1,H1,I1,J1) [G1 >= 1 && 4 >= J1] (1,1) 40. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,I1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,J1,W,X,F1,G1,H1,H1,I1,J1,G1) [H1 >= 1 && 20 >= G1 && G1 >= 5] (1,1) 41. 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,Z,A1,B1,C1,D1,E1) -> f34(A,K1,H1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,I1,W,X,F1,20,G1,G1,H1,I1,J1) [G1 >= 1 && J1 >= 21] (1,1) 42. f91(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1) True (?,1) Signature: {(exitus616,31) ;(f0,31) ;(f34,31) ;(f39,31) ;(f44,31) ;(f51,31) ;(f59,31) ;(f64,31) ;(f75,31) ;(f76,31) ;(f78,31) ;(f82,31) ;(f91,31) ;(f93,31) ;(f95,31)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37},4->{33,34,35,36,37},5->{25,26,27,28,29},6->{25,26 ,27,28,29},7->{22},8->{23},9->{0,12,13},10->{0,12,13},11->{7,8,24},12->{8},13->{8},14->{33,34,35,36,37} ,15->{33,34,35,36,37},16->{33,34,35,36,37},17->{33,34,35,36,37},18->{18,42},19->{18,42},20->{18,42},22->{33 ,34,35,36,37},23->{33,34,35,36,37},24->{17},25->{17,22,23},26->{17,22,23},27->{7,8,24},28->{9,10,11},29->{9 ,10,11},30->{5,6,16},31->{5,6,16},32->{33,34,35,36,37},33->{14,15,30,31,32},34->{14,15,30,31,32},35->{35,36 ,37},36->{18,42},37->{18,42},38->{18,42},39->{1,2,19},40->{1,2,19},41->{1,2,19},42->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42] | +- p:[0,9,28,5,30,33,14,34,15,16,31,17,24,11,29,6,27,25,26,22,7,23,8,12,10,13,32] c: [] | +- p:[35] c: [] | `- p:[18] c: [] MAYBE