MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [E >= 1] (?,1) 5. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I] (?,1) 6. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I >= 1] (?,1) 7. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 8. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 9. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + M] (?,1) 10. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [M >= 1] (?,1) 11. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [M = 0] (?,1) 12. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [0 >= 1 + A] (?,1) 13. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [A >= 1] (?,1) 14. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [N >= 0] (?,1) 15. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 2 + N] (?,1) 16. 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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I = 0] (?,1) 17. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K = 0] (?,1) 18. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) 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,F1,G1) -> f96(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,F1,G1) [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,F1,G1) -> f96(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,F1,G1) [E = 0] (?,1) 21. f98(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f100(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) True (?,1) 22. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 23. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 24. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(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,F1,G1) [K = 0] (?,1) 25. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 26. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 27. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) True (?,1) 28. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 29. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 30. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1 && 1 + N = 0] (?,1) 31. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1 && 1 + N = 0] (?,1) 32. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,0,0,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I1 && V = 0] (?,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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [I1 >= 1 && V = 0] (?,1) 38. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 39. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,H1,I1,I1,J1,K1,G1) [0 >= I1] (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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,5,I1,I1,J1,K1,L1) [I1 >= 1 && 4 >= L1] (1,1) 42. 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,F1,G1) -> f34(A,M1,K1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,L1,W,X,Y,Z,H1,I1,J1,J1,K1,L1,I1) [J1 >= 1 && 20 >= I1 && I1 >= 5] (1,1) 43. 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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,20,I1,I1,J1,K1,L1) [I1 >= 1 && L1 >= 21] (1,1) Signature: {(f0,33) ;(f100,33) ;(f34,33) ;(f39,33) ;(f44,33) ;(f56,33) ;(f64,33) ;(f69,33) ;(f80,33) ;(f81,33) ;(f83,33) ;(f87,33) ;(f96,33) ;(f98,33)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37,38,39},4->{33,34,35,36,37,38,39},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,38,39},15->{33,34,35,36,37,38,39},16->{33,34,35,36,37,38,39},17->{33,34,35 ,36,37,38,39},18->{18},19->{18},20->{18},21->{},22->{33,34,35,36,37,38,39},23->{33,34,35,36,37,38,39} ,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,38,39},33->{14,15,30,31,32},34->{14,15,30,31,32},35->{33,34,35,36,37,38,39},36->{33 ,34,35,36,37,38,39},37->{33,34,35,36,37,38,39},38->{18},39->{18},40->{18},41->{1,2,19},42->{1,2,19},43->{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. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [E >= 1] (1,1) 5. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I] (?,1) 6. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I >= 1] (?,1) 7. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 8. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 9. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + M] (?,1) 10. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [M >= 1] (?,1) 11. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [M = 0] (?,1) 12. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [0 >= 1 + A] (?,1) 13. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [A >= 1] (?,1) 14. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [N >= 0] (?,1) 15. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 2 + N] (?,1) 16. 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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I = 0] (?,1) 17. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K = 0] (?,1) 18. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) 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,F1,G1) -> f96(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,F1,G1) [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,F1,G1) -> f96(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,F1,G1) [E = 0] (1,1) 21. f98(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f100(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) True (1,1) 22. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 23. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 24. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(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,F1,G1) [K = 0] (?,1) 25. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 26. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 27. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) True (?,1) 28. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 29. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 30. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1 && 1 + N = 0] (?,1) 31. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1 && 1 + N = 0] (?,1) 32. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,0,0,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I1 && V = 0] (?,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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [I1 >= 1 && V = 0] (?,1) 38. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (1,1) 39. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,H1,I1,I1,J1,K1,G1) [0 >= I1] (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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,5,I1,I1,J1,K1,L1) [I1 >= 1 && 4 >= L1] (1,1) 42. 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,F1,G1) -> f34(A,M1,K1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,L1,W,X,Y,Z,H1,I1,J1,J1,K1,L1,I1) [J1 >= 1 && 20 >= I1 && I1 >= 5] (1,1) 43. 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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,20,I1,I1,J1,K1,L1) [I1 >= 1 && L1 >= 21] (1,1) Signature: {(f0,33) ;(f100,33) ;(f34,33) ;(f39,33) ;(f44,33) ;(f56,33) ;(f64,33) ;(f69,33) ;(f80,33) ;(f81,33) ;(f83,33) ;(f87,33) ;(f96,33) ;(f98,33)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37,38,39},4->{33,34,35,36,37,38,39},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,38,39},15->{33,34,35,36,37,38,39},16->{33,34,35,36,37,38,39},17->{33,34,35 ,36,37,38,39},18->{18},19->{18},20->{18},21->{},22->{33,34,35,36,37,38,39},23->{33,34,35,36,37,38,39} ,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,38,39},33->{14,15,30,31,32},34->{14,15,30,31,32},35->{33,34,35,36,37,38,39},36->{33 ,34,35,36,37,38,39},37->{33,34,35,36,37,38,39},38->{18},39->{18},40->{18},41->{1,2,19},42->{1,2,19},43->{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) ,(36,33) ,(36,34) ,(37,33) ,(37,34)] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [E >= 1] (1,1) 5. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I] (?,1) 6. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I >= 1] (?,1) 7. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 8. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 9. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + M] (?,1) 10. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [M >= 1] (?,1) 11. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [M = 0] (?,1) 12. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [0 >= 1 + A] (?,1) 13. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [A >= 1] (?,1) 14. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [N >= 0] (?,1) 15. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 2 + N] (?,1) 16. 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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I = 0] (?,1) 17. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K = 0] (?,1) 18. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) 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,F1,G1) -> f96(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,F1,G1) [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,F1,G1) -> f96(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,F1,G1) [E = 0] (1,1) 21. f98(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f100(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) True (1,1) 22. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 23. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 24. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(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,F1,G1) [K = 0] (?,1) 25. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 26. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 27. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) True (?,1) 28. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 29. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 30. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1 && 1 + N = 0] (?,1) 31. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1 && 1 + N = 0] (?,1) 32. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,0,0,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I1 && V = 0] (?,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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [I1 >= 1 && V = 0] (?,1) 38. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (1,1) 39. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,H1,I1,I1,J1,K1,G1) [0 >= I1] (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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,5,I1,I1,J1,K1,L1) [I1 >= 1 && 4 >= L1] (1,1) 42. 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,F1,G1) -> f34(A,M1,K1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,L1,W,X,Y,Z,H1,I1,J1,J1,K1,L1,I1) [J1 >= 1 && 20 >= I1 && I1 >= 5] (1,1) 43. 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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,20,I1,I1,J1,K1,L1) [I1 >= 1 && L1 >= 21] (1,1) Signature: {(f0,33) ;(f100,33) ;(f34,33) ;(f39,33) ;(f44,33) ;(f56,33) ;(f64,33) ;(f69,33) ;(f80,33) ;(f81,33) ;(f83,33) ;(f87,33) ;(f96,33) ;(f98,33)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37,38,39},4->{33,34,35,36,37,38,39},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,38,39},15->{33,34,35,36,37,38,39},16->{33,34,35,36,37,38,39},17->{33,34,35,36,37,38,39},18->{18} ,19->{18},20->{18},21->{},22->{33,34,35,36,37,38,39},23->{33,34,35,36,37,38,39},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,38 ,39},33->{14,15,30,31,32},34->{14,15,30,31,32},35->{35,36,37,38,39},36->{35,36,37,38,39},37->{35,36,37,38 ,39},38->{18},39->{18},40->{18},41->{1,2,19},42->{1,2,19},43->{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. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [E >= 1] (1,1) 5. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I] (?,1) 6. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I >= 1] (?,1) 7. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 8. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 9. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + M] (?,1) 10. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [M >= 1] (?,1) 11. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [M = 0] (?,1) 12. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [0 >= 1 + A] (?,1) 13. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [A >= 1] (?,1) 14. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [N >= 0] (?,1) 15. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 2 + N] (?,1) 16. 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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I = 0] (?,1) 17. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K = 0] (?,1) 18. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) 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,F1,G1) -> f96(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,F1,G1) [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,F1,G1) -> f96(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,F1,G1) [E = 0] (1,1) 22. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 23. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 24. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(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,F1,G1) [K = 0] (?,1) 25. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 26. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 27. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) True (?,1) 28. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 29. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 30. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1 && 1 + N = 0] (?,1) 31. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1 && 1 + N = 0] (?,1) 32. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,0,0,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I1 && V = 0] (?,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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [I1 >= 1 && V = 0] (?,1) 38. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (1,1) 39. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,H1,I1,I1,J1,K1,G1) [0 >= I1] (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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,5,I1,I1,J1,K1,L1) [I1 >= 1 && 4 >= L1] (1,1) 42. 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,F1,G1) -> f34(A,M1,K1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,L1,W,X,Y,Z,H1,I1,J1,J1,K1,L1,I1) [J1 >= 1 && 20 >= I1 && I1 >= 5] (1,1) 43. 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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,20,I1,I1,J1,K1,L1) [I1 >= 1 && L1 >= 21] (1,1) Signature: {(f0,33) ;(f100,33) ;(f34,33) ;(f39,33) ;(f44,33) ;(f56,33) ;(f64,33) ;(f69,33) ;(f80,33) ;(f81,33) ;(f83,33) ;(f87,33) ;(f96,33) ;(f98,33)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37,38,39},4->{33,34,35,36,37,38,39},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,38,39},15->{33,34,35,36,37,38,39},16->{33,34,35,36,37,38,39},17->{33,34,35,36,37,38,39},18->{18} ,19->{18},20->{18},22->{33,34,35,36,37,38,39},23->{33,34,35,36,37,38,39},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,38,39},33->{14 ,15,30,31,32},34->{14,15,30,31,32},35->{35,36,37,38,39},36->{35,36,37,38,39},37->{35,36,37,38,39},38->{18} ,39->{18},40->{18},41->{1,2,19},42->{1,2,19},43->{1,2,19}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths MAYBE + Considered Problem: Rules: 0. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [E >= 1] (?,1) 5. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I] (?,1) 6. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I >= 1] (?,1) 7. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 8. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 9. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + M] (?,1) 10. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [M >= 1] (?,1) 11. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [M = 0] (?,1) 12. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [0 >= 1 + A] (?,1) 13. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [A >= 1] (?,1) 14. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [N >= 0] (?,1) 15. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 2 + N] (?,1) 16. 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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I = 0] (?,1) 17. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K = 0] (?,1) 18. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) 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,F1,G1) -> f96(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,F1,G1) [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,F1,G1) -> f96(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,F1,G1) [E = 0] (?,1) 22. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 23. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 24. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(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,F1,G1) [K = 0] (?,1) 25. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 26. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 27. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) True (?,1) 28. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 29. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 30. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1 && 1 + N = 0] (?,1) 31. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1 && 1 + N = 0] (?,1) 32. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,0,0,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I1 && V = 0] (?,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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [I1 >= 1 && V = 0] (?,1) 38. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 39. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,H1,I1,I1,J1,K1,G1) [0 >= I1] (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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,5,I1,I1,J1,K1,L1) [I1 >= 1 && 4 >= L1] (1,1) 42. 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,F1,G1) -> f34(A,M1,K1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,L1,W,X,Y,Z,H1,I1,J1,J1,K1,L1,I1) [J1 >= 1 && 20 >= I1 && I1 >= 5] (1,1) 43. 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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,20,I1,I1,J1,K1,L1) [I1 >= 1 && L1 >= 21] (1,1) 44. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> 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,F1,G1) True (?,1) Signature: {(exitus616,33) ;(f0,33) ;(f100,33) ;(f34,33) ;(f39,33) ;(f44,33) ;(f56,33) ;(f64,33) ;(f69,33) ;(f80,33) ;(f81,33) ;(f83,33) ;(f87,33) ;(f96,33) ;(f98,33)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37,38,39},4->{33,34,35,36,37,38,39},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,38,39},15->{33,34,35,36,37,38,39},16->{33,34,35,36,37,38,39},17->{33,34,35 ,36,37,38,39},18->{18,44},19->{18,44},20->{18,44},22->{33,34,35,36,37,38,39},23->{33,34,35,36,37,38,39} ,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,38,39},33->{14,15,30,31,32},34->{14,15,30,31,32},35->{33,34,35,36,37,38,39},36->{33 ,34,35,36,37,38,39},37->{33,34,35,36,37,38,39},38->{18,44},39->{18,44},40->{18,44},41->{1,2,19},42->{1,2,19} ,43->{1,2,19},44->{}] + 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) ,(36,33) ,(36,34) ,(37,33) ,(37,34)] * Step 6: Failure MAYBE + Considered Problem: Rules: 0. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f39(A,B,1,B,H1,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,E,10,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [E >= 1] (?,1) 5. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I] (?,1) 6. 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,F1,G1) -> f69(A,B,C,D,E,F,G,H,I,I,0,H1,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I >= 1] (?,1) 7. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 8. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 9. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + M] (?,1) 10. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [M >= 1] (?,1) 11. f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [M = 0] (?,1) 12. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [0 >= 1 + A] (?,1) 13. f81(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) [A >= 1] (?,1) 14. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [N >= 0] (?,1) 15. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 2 + N] (?,1) 16. 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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,0,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [I = 0] (?,1) 17. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K = 0] (?,1) 18. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) 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,F1,G1) -> f96(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,F1,G1) [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,F1,G1) -> f96(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,F1,G1) [E = 0] (?,1) 22. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + K] (?,1) 23. f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [K >= 1] (?,1) 24. f83(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(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,F1,G1) [K = 0] (?,1) 25. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 26. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f87(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,H1,H1,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 27. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f83(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,F1,G1) True (?,1) 28. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 29. f69(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f80(A,B,C,D,E,F,G,H,I,J,K,L,M,N,L,0,0,H1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1] (?,1) 30. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1 && 1 + N = 0] (?,1) 31. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f64(A,B,C,D,E,F,G,H,I1,J,K,L,M,-1,O,P,Q,R,S,H1,H1,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 1 && 1 + N = 0] (?,1) 32. f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,-1,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f56(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,F1,G1) [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,F1,G1) -> f44(A,B,C,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,0,0,A1,B1,C1,D1,E1,F1,G1) [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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + I1 && V = 0] (?,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,F1,G1) -> f44(A,B,0,D,E,F,G,H1,I,J,K,L,M,H,O,P,Q,R,S,T,U,0,0,0,I1,I1,A1,B1,C1,D1,E1,F1,G1) [I1 >= 1 && V = 0] (?,1) 38. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [0 >= 1 + H1] (?,1) 39. 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,H,O,P,Q,R,S,T,U,V,H1,H1,Y,Z,A1,B1,C1,D1,E1,F1,G1) [H1 >= 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,F1,G1) -> f96(A,B,1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,H1,I1,I1,J1,K1,G1) [0 >= I1] (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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,5,I1,I1,J1,K1,L1) [I1 >= 1 && 4 >= L1] (1,1) 42. 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,F1,G1) -> f34(A,M1,K1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,L1,W,X,Y,Z,H1,I1,J1,J1,K1,L1,I1) [J1 >= 1 && 20 >= I1 && I1 >= 5] (1,1) 43. 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,F1,G1) -> f34(A,M1,J1,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,K1,W,X,Y,Z,H1,20,I1,I1,J1,K1,L1) [I1 >= 1 && L1 >= 21] (1,1) 44. f96(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1) -> 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,F1,G1) True (?,1) Signature: {(exitus616,33) ;(f0,33) ;(f100,33) ;(f34,33) ;(f39,33) ;(f44,33) ;(f56,33) ;(f64,33) ;(f69,33) ;(f80,33) ;(f81,33) ;(f83,33) ;(f87,33) ;(f96,33) ;(f98,33)} Flow Graph: [0->{7,8,24},1->{3,4,20},2->{3,4,20},3->{33,34,35,36,37,38,39},4->{33,34,35,36,37,38,39},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,38,39},15->{33,34,35,36,37,38,39},16->{33,34,35,36,37,38,39},17->{33,34,35,36,37,38,39},18->{18 ,44},19->{18,44},20->{18,44},22->{33,34,35,36,37,38,39},23->{33,34,35,36,37,38,39},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,38 ,39},33->{14,15,30,31,32},34->{14,15,30,31,32},35->{35,36,37,38,39},36->{35,36,37,38,39},37->{35,36,37,38 ,39},38->{18,44},39->{18,44},40->{18,44},41->{1,2,19},42->{1,2,19},43->{1,2,19},44->{}] + 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,43,44] | +- 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,36,37] c: [] | `- p:[18] c: [] MAYBE