YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f18(100,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f18(100,10,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + B] (?,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B >= 1] (?,1) 4. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,0,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B = 0] (?,1) 5. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,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) True (?,1) 6. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,10,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 7. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,0,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D = 0] (?,1) 8. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [0 >= 1 + D] (?,1) 9. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [D >= 1] (?,1) 10. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 11. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,10,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 12. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + H] (?,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H >= 1] (?,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H = 0] (?,1) 15. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 16. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,10,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 17. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,0,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J = 0] (?,1) 18. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + J] (?,1) 19. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J >= 1] (?,1) 20. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,0,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 21. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,10,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 22. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + N] (?,1) 23. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N >= 1] (?,1) 24. 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) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,0,0,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N = 0] (?,1) 25. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 26. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,10,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P = 0] (?,1) 28. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + P] (?,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P >= 1] (?,1) 30. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,0,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 31. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,10,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 32. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + T] (?,1) 33. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [T >= 1] (?,1) 34. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1) [T = 0] (?,1) 35. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 36. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,10,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 37. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,0,X,Y,Z,A1,B1,C1,D1) [V = 0] (?,1) 38. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [0 >= 1 + V] (?,1) 39. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [V >= 1] (?,1) 40. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,0,A1,B1,C1,D1) True (?,1) 41. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,10,A1,B1,C1,D1) True (?,1) 42. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [0 >= 1 + Z] (?,1) 43. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [Z >= 1] (?,1) 44. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,C1,D1) True (?,1) 45. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,10,C1,D1) True (?,1) 46. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [0 >= 1 + B1] (?,1) 47. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [B1 >= 1] (?,1) 48. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,0,B1,C1,D1) [Z = 0] (?,1) 49. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,0,D1) [B1 = 0] (?,1) 50. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,1 + D1) [Y >= 1 + D1] (?,1) 51. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D1 >= Y] (?,1) 52. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,1 + X,Y,Z,A1,B1,C1,D1) [S >= 1 + X] (?,1) 53. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [X >= S] (?,1) 54. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,1 + R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [M >= 1 + R] (?,1) 55. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [R >= M] (?,1) 56. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [G >= 1 + L] (?,1) 57. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [L >= G] (?,1) 58. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [A >= 1 + F] (?,1) 59. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [F >= A] (?,1) Signature: {(f0,30) ;(f101,30) ;(f107,30) ;(f110,30) ;(f126,30) ;(f138,30) ;(f141,30) ;(f147,30) ;(f150,30) ;(f166,30) ;(f178,30) ;(f18,30) ;(f181,30) ;(f187,30) ;(f190,30) ;(f207,30) ;(f21,30) ;(f27,30) ;(f30,30) ;(f46,30) ;(f58,30) ;(f61,30) ;(f67,30) ;(f70,30) ;(f86,30) ;(f98,30)} Flow Graph: [0->{2,3,4},1->{2,3,4},2->{5,6},3->{5,6},4->{10,11},5->{7,8,9},6->{7,8,9},7->{10,11},8->{58,59},9->{58,59} ,10->{12,13,14},11->{12,13,14},12->{15,16},13->{15,16},14->{20,21},15->{17,18,19},16->{17,18,19},17->{20,21} ,18->{56,57},19->{56,57},20->{22,23,24},21->{22,23,24},22->{25,26},23->{25,26},24->{30,31},25->{27,28,29} ,26->{27,28,29},27->{30,31},28->{54,55},29->{54,55},30->{32,33,34},31->{32,33,34},32->{35,36},33->{35,36} ,34->{40,41},35->{37,38,39},36->{37,38,39},37->{40,41},38->{52,53},39->{52,53},40->{42,43,48},41->{42,43,48} ,42->{44,45},43->{44,45},44->{46,47,49},45->{46,47,49},46->{50,51},47->{50,51},48->{},49->{},50->{50,51} ,51->{},52->{52,53},53->{40,41},54->{54,55},55->{30,31},56->{56,57},57->{20,21},58->{58,59},59->{10,11}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f18(100,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f18(100,10,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + B] (1,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B >= 1] (1,1) 4. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,0,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B = 0] (1,1) 5. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,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) True (1,1) 6. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,10,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 7. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,0,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D = 0] (1,1) 8. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [0 >= 1 + D] (1,1) 9. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [D >= 1] (1,1) 10. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 11. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,10,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 12. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + H] (1,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H >= 1] (1,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H = 0] (1,1) 15. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 16. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,10,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 17. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,0,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J = 0] (1,1) 18. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + J] (1,1) 19. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J >= 1] (1,1) 20. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,0,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 21. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,10,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 22. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + N] (1,1) 23. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N >= 1] (1,1) 24. 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) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,0,0,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N = 0] (1,1) 25. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 26. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,10,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P = 0] (1,1) 28. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + P] (1,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P >= 1] (1,1) 30. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,0,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 31. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,10,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 32. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + T] (1,1) 33. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [T >= 1] (1,1) 34. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1) [T = 0] (1,1) 35. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 36. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,10,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 37. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,0,X,Y,Z,A1,B1,C1,D1) [V = 0] (1,1) 38. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [0 >= 1 + V] (1,1) 39. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [V >= 1] (1,1) 40. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,0,A1,B1,C1,D1) True (1,1) 41. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,10,A1,B1,C1,D1) True (1,1) 42. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [0 >= 1 + Z] (1,1) 43. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [Z >= 1] (1,1) 44. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,C1,D1) True (1,1) 45. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,10,C1,D1) True (1,1) 46. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [0 >= 1 + B1] (1,1) 47. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [B1 >= 1] (1,1) 48. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,0,B1,C1,D1) [Z = 0] (1,1) 49. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,0,D1) [B1 = 0] (1,1) 50. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,1 + D1) [Y >= 1 + D1] (?,1) 51. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D1 >= Y] (1,1) 52. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,1 + X,Y,Z,A1,B1,C1,D1) [S >= 1 + X] (?,1) 53. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [X >= S] (1,1) 54. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,1 + R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [M >= 1 + R] (?,1) 55. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [R >= M] (1,1) 56. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [G >= 1 + L] (?,1) 57. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [L >= G] (1,1) 58. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [A >= 1 + F] (?,1) 59. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [F >= A] (1,1) Signature: {(f0,30) ;(f101,30) ;(f107,30) ;(f110,30) ;(f126,30) ;(f138,30) ;(f141,30) ;(f147,30) ;(f150,30) ;(f166,30) ;(f178,30) ;(f18,30) ;(f181,30) ;(f187,30) ;(f190,30) ;(f207,30) ;(f21,30) ;(f27,30) ;(f30,30) ;(f46,30) ;(f58,30) ;(f61,30) ;(f67,30) ;(f70,30) ;(f86,30) ;(f98,30)} Flow Graph: [0->{2,3,4},1->{2,3,4},2->{5,6},3->{5,6},4->{10,11},5->{7,8,9},6->{7,8,9},7->{10,11},8->{58,59},9->{58,59} ,10->{12,13,14},11->{12,13,14},12->{15,16},13->{15,16},14->{20,21},15->{17,18,19},16->{17,18,19},17->{20,21} ,18->{56,57},19->{56,57},20->{22,23,24},21->{22,23,24},22->{25,26},23->{25,26},24->{30,31},25->{27,28,29} ,26->{27,28,29},27->{30,31},28->{54,55},29->{54,55},30->{32,33,34},31->{32,33,34},32->{35,36},33->{35,36} ,34->{40,41},35->{37,38,39},36->{37,38,39},37->{40,41},38->{52,53},39->{52,53},40->{42,43,48},41->{42,43,48} ,42->{44,45},43->{44,45},44->{46,47,49},45->{46,47,49},46->{50,51},47->{50,51},48->{},49->{},50->{50,51} ,51->{},52->{52,53},53->{40,41},54->{54,55},55->{30,31},56->{56,57},57->{20,21},58->{58,59},59->{10,11}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,2) ,(0,3) ,(1,2) ,(1,4) ,(5,8) ,(5,9) ,(6,7) ,(6,8) ,(10,12) ,(10,13) ,(11,12) ,(11,14) ,(15,18) ,(15,19) ,(16,17) ,(16,18) ,(20,22) ,(20,23) ,(21,22) ,(21,24) ,(25,28) ,(25,29) ,(26,27) ,(26,28) ,(30,32) ,(30,33) ,(31,32) ,(31,34) ,(35,38) ,(35,39) ,(36,37) ,(36,38) ,(40,42) ,(40,43) ,(41,42) ,(41,48) ,(44,46) ,(44,47) ,(45,46) ,(45,49)] * Step 3: UnreachableRules WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f18(100,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f18(100,10,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 2. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + B] (1,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B >= 1] (1,1) 4. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,0,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B = 0] (1,1) 5. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,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) True (1,1) 6. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,10,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 7. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,0,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D = 0] (1,1) 8. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [0 >= 1 + D] (1,1) 9. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [D >= 1] (1,1) 10. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 11. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,10,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 12. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + H] (1,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H >= 1] (1,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H = 0] (1,1) 15. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 16. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,10,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 17. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,0,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J = 0] (1,1) 18. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + J] (1,1) 19. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J >= 1] (1,1) 20. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,0,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 21. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,10,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 22. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + N] (1,1) 23. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N >= 1] (1,1) 24. 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) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,0,0,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N = 0] (1,1) 25. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 26. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,10,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P = 0] (1,1) 28. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + P] (1,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P >= 1] (1,1) 30. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,0,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 31. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,10,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 32. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [0 >= 1 + T] (1,1) 33. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [T >= 1] (1,1) 34. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1) [T = 0] (1,1) 35. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 36. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,10,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 37. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,0,X,Y,Z,A1,B1,C1,D1) [V = 0] (1,1) 38. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [0 >= 1 + V] (1,1) 39. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [V >= 1] (1,1) 40. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,0,A1,B1,C1,D1) True (1,1) 41. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,10,A1,B1,C1,D1) True (1,1) 42. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [0 >= 1 + Z] (1,1) 43. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [Z >= 1] (1,1) 44. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,C1,D1) True (1,1) 45. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,10,C1,D1) True (1,1) 46. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [0 >= 1 + B1] (1,1) 47. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [B1 >= 1] (1,1) 48. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,0,B1,C1,D1) [Z = 0] (1,1) 49. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,0,D1) [B1 = 0] (1,1) 50. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,1 + D1) [Y >= 1 + D1] (?,1) 51. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D1 >= Y] (1,1) 52. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,1 + X,Y,Z,A1,B1,C1,D1) [S >= 1 + X] (?,1) 53. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [X >= S] (1,1) 54. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,1 + R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [M >= 1 + R] (?,1) 55. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [R >= M] (1,1) 56. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [G >= 1 + L] (?,1) 57. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [L >= G] (1,1) 58. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [A >= 1 + F] (?,1) 59. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [F >= A] (1,1) Signature: {(f0,30) ;(f101,30) ;(f107,30) ;(f110,30) ;(f126,30) ;(f138,30) ;(f141,30) ;(f147,30) ;(f150,30) ;(f166,30) ;(f178,30) ;(f18,30) ;(f181,30) ;(f187,30) ;(f190,30) ;(f207,30) ;(f21,30) ;(f27,30) ;(f30,30) ;(f46,30) ;(f58,30) ;(f61,30) ;(f67,30) ;(f70,30) ;(f86,30) ;(f98,30)} Flow Graph: [0->{4},1->{3},2->{5,6},3->{5,6},4->{10,11},5->{7},6->{9},7->{10,11},8->{58,59},9->{58,59},10->{14} ,11->{13},12->{15,16},13->{15,16},14->{20,21},15->{17},16->{19},17->{20,21},18->{56,57},19->{56,57},20->{24} ,21->{23},22->{25,26},23->{25,26},24->{30,31},25->{27},26->{29},27->{30,31},28->{54,55},29->{54,55},30->{34} ,31->{33},32->{35,36},33->{35,36},34->{40,41},35->{37},36->{39},37->{40,41},38->{52,53},39->{52,53},40->{48} ,41->{43},42->{44,45},43->{44,45},44->{49},45->{47},46->{50,51},47->{50,51},48->{},49->{},50->{50,51},51->{} ,52->{52,53},53->{40,41},54->{54,55},55->{30,31},56->{56,57},57->{20,21},58->{58,59},59->{10,11}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [2 ,8 ,12 ,18 ,22 ,28 ,32 ,38 ,42 ,46] * Step 4: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f18(100,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f18(100,10,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B >= 1] (1,1) 4. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,0,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B = 0] (1,1) 5. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,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) True (1,1) 6. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,10,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 7. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,0,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D = 0] (1,1) 9. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [D >= 1] (1,1) 10. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 11. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,10,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H >= 1] (1,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H = 0] (1,1) 15. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 16. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,10,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 17. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,0,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J = 0] (1,1) 19. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J >= 1] (1,1) 20. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,0,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 21. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,10,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 23. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N >= 1] (1,1) 24. 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) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,0,0,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N = 0] (1,1) 25. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 26. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,10,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P = 0] (1,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P >= 1] (1,1) 30. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,0,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 31. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,10,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 33. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [T >= 1] (1,1) 34. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1) [T = 0] (1,1) 35. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 36. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,10,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 37. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,0,X,Y,Z,A1,B1,C1,D1) [V = 0] (1,1) 39. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [V >= 1] (1,1) 40. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,0,A1,B1,C1,D1) True (1,1) 41. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,10,A1,B1,C1,D1) True (1,1) 43. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [Z >= 1] (1,1) 44. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,C1,D1) True (1,1) 45. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,10,C1,D1) True (1,1) 47. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [B1 >= 1] (1,1) 48. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,0,B1,C1,D1) [Z = 0] (1,1) 49. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,0,D1) [B1 = 0] (1,1) 50. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,1 + D1) [Y >= 1 + D1] (?,1) 51. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D1 >= Y] (1,1) 52. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,1 + X,Y,Z,A1,B1,C1,D1) [S >= 1 + X] (?,1) 53. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [X >= S] (1,1) 54. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,1 + R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [M >= 1 + R] (?,1) 55. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [R >= M] (1,1) 56. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [G >= 1 + L] (?,1) 57. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [L >= G] (1,1) 58. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [A >= 1 + F] (?,1) 59. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [F >= A] (1,1) Signature: {(f0,30) ;(f101,30) ;(f107,30) ;(f110,30) ;(f126,30) ;(f138,30) ;(f141,30) ;(f147,30) ;(f150,30) ;(f166,30) ;(f178,30) ;(f18,30) ;(f181,30) ;(f187,30) ;(f190,30) ;(f207,30) ;(f21,30) ;(f27,30) ;(f30,30) ;(f46,30) ;(f58,30) ;(f61,30) ;(f67,30) ;(f70,30) ;(f86,30) ;(f98,30)} Flow Graph: [0->{4},1->{3},3->{5,6},4->{10,11},5->{7},6->{9},7->{10,11},9->{58,59},10->{14},11->{13},13->{15,16} ,14->{20,21},15->{17},16->{19},17->{20,21},19->{56,57},20->{24},21->{23},23->{25,26},24->{30,31},25->{27} ,26->{29},27->{30,31},29->{54,55},30->{34},31->{33},33->{35,36},34->{40,41},35->{37},36->{39},37->{40,41} ,39->{52,53},40->{48},41->{43},43->{44,45},44->{49},45->{47},47->{50,51},48->{},49->{},50->{50,51},51->{} ,52->{52,53},53->{40,41},54->{54,55},55->{30,31},56->{56,57},57->{20,21},58->{58,59},59->{10,11}] + Applied Processor: AddSinks + Details: () * Step 5: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f18(100,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f18(100,10,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B >= 1] (?,1) 4. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,0,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B = 0] (?,1) 5. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,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) True (?,1) 6. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,10,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 7. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,0,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D = 0] (?,1) 9. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [D >= 1] (?,1) 10. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 11. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,10,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H >= 1] (?,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H = 0] (?,1) 15. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 16. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,10,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 17. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,0,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J = 0] (?,1) 19. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J >= 1] (?,1) 20. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,0,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 21. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,10,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 23. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N >= 1] (?,1) 24. 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) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,0,0,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N = 0] (?,1) 25. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 26. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,10,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P = 0] (?,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P >= 1] (?,1) 30. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,0,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 31. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,10,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 33. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [T >= 1] (?,1) 34. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1) [T = 0] (?,1) 35. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 36. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,10,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 37. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,0,X,Y,Z,A1,B1,C1,D1) [V = 0] (?,1) 39. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [V >= 1] (?,1) 40. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,0,A1,B1,C1,D1) True (?,1) 41. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,10,A1,B1,C1,D1) True (?,1) 43. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [Z >= 1] (?,1) 44. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,C1,D1) True (?,1) 45. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,10,C1,D1) True (?,1) 47. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [B1 >= 1] (?,1) 48. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,0,B1,C1,D1) [Z = 0] (?,1) 49. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,0,D1) [B1 = 0] (?,1) 50. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,1 + D1) [Y >= 1 + D1] (?,1) 51. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D1 >= Y] (?,1) 52. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,1 + X,Y,Z,A1,B1,C1,D1) [S >= 1 + X] (?,1) 53. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [X >= S] (?,1) 54. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,1 + R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [M >= 1 + R] (?,1) 55. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [R >= M] (?,1) 56. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [G >= 1 + L] (?,1) 57. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [L >= G] (?,1) 58. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [A >= 1 + F] (?,1) 59. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [F >= A] (?,1) 60. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> 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) True (?,1) 61. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> 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) True (?,1) 62. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> 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) True (?,1) Signature: {(exitus616,30) ;(f0,30) ;(f101,30) ;(f107,30) ;(f110,30) ;(f126,30) ;(f138,30) ;(f141,30) ;(f147,30) ;(f150,30) ;(f166,30) ;(f178,30) ;(f18,30) ;(f181,30) ;(f187,30) ;(f190,30) ;(f207,30) ;(f21,30) ;(f27,30) ;(f30,30) ;(f46,30) ;(f58,30) ;(f61,30) ;(f67,30) ;(f70,30) ;(f86,30) ;(f98,30)} Flow Graph: [0->{3,4},1->{3,4},3->{5,6},4->{10,11},5->{7,9},6->{7,9},7->{10,11},9->{58,59},10->{13,14},11->{13,14} ,13->{15,16},14->{20,21},15->{17,19},16->{17,19},17->{20,21},19->{56,57},20->{23,24},21->{23,24},23->{25,26} ,24->{30,31},25->{27,29},26->{27,29},27->{30,31},29->{54,55},30->{33,34},31->{33,34},33->{35,36},34->{40,41} ,35->{37,39},36->{37,39},37->{40,41},39->{52,53},40->{43,48,62},41->{43,48,62},43->{44,45},44->{47,49,61} ,45->{47,49,61},47->{50,51,60},48->{},49->{},50->{50,51,60},51->{},52->{52,53},53->{40,41},54->{54,55} ,55->{30,31},56->{56,57},57->{20,21},58->{58,59},59->{10,11},60->{},61->{},62->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,3) ,(1,4) ,(5,9) ,(6,7) ,(10,13) ,(11,14) ,(15,19) ,(16,17) ,(20,23) ,(21,24) ,(25,29) ,(26,27) ,(30,33) ,(31,34) ,(35,39) ,(36,37) ,(40,43) ,(41,48) ,(44,47) ,(45,49)] * Step 6: LooptreeTransformer WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. 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) -> f18(100,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f18(100,10,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B >= 1] (?,1) 4. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,0,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B = 0] (?,1) 5. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,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) True (?,1) 6. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,10,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 7. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,0,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D = 0] (?,1) 9. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [D >= 1] (?,1) 10. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 11. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,10,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H >= 1] (?,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H = 0] (?,1) 15. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 16. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,10,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 17. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,0,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J = 0] (?,1) 19. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J >= 1] (?,1) 20. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,0,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 21. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,10,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 23. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N >= 1] (?,1) 24. 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) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,0,0,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N = 0] (?,1) 25. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 26. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,10,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P = 0] (?,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P >= 1] (?,1) 30. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,0,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 31. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,10,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 33. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [T >= 1] (?,1) 34. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1) [T = 0] (?,1) 35. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 36. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,10,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 37. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,0,X,Y,Z,A1,B1,C1,D1) [V = 0] (?,1) 39. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [V >= 1] (?,1) 40. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,0,A1,B1,C1,D1) True (?,1) 41. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,10,A1,B1,C1,D1) True (?,1) 43. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [Z >= 1] (?,1) 44. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,C1,D1) True (?,1) 45. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,10,C1,D1) True (?,1) 47. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [B1 >= 1] (?,1) 48. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,0,B1,C1,D1) [Z = 0] (?,1) 49. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,0,D1) [B1 = 0] (?,1) 50. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,1 + D1) [Y >= 1 + D1] (?,1) 51. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D1 >= Y] (?,1) 52. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,1 + X,Y,Z,A1,B1,C1,D1) [S >= 1 + X] (?,1) 53. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [X >= S] (?,1) 54. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,1 + R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [M >= 1 + R] (?,1) 55. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [R >= M] (?,1) 56. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [G >= 1 + L] (?,1) 57. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [L >= G] (?,1) 58. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [A >= 1 + F] (?,1) 59. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [F >= A] (?,1) 60. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> 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) True (?,1) 61. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> 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) True (?,1) 62. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> 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) True (?,1) Signature: {(exitus616,30) ;(f0,30) ;(f101,30) ;(f107,30) ;(f110,30) ;(f126,30) ;(f138,30) ;(f141,30) ;(f147,30) ;(f150,30) ;(f166,30) ;(f178,30) ;(f18,30) ;(f181,30) ;(f187,30) ;(f190,30) ;(f207,30) ;(f21,30) ;(f27,30) ;(f30,30) ;(f46,30) ;(f58,30) ;(f61,30) ;(f67,30) ;(f70,30) ;(f86,30) ;(f98,30)} Flow Graph: [0->{4},1->{3},3->{5,6},4->{10,11},5->{7},6->{9},7->{10,11},9->{58,59},10->{14},11->{13},13->{15,16} ,14->{20,21},15->{17},16->{19},17->{20,21},19->{56,57},20->{24},21->{23},23->{25,26},24->{30,31},25->{27} ,26->{29},27->{30,31},29->{54,55},30->{34},31->{33},33->{35,36},34->{40,41},35->{37},36->{39},37->{40,41} ,39->{52,53},40->{48,62},41->{43,62},43->{44,45},44->{49,61},45->{47,61},47->{50,51,60},48->{},49->{} ,50->{50,51,60},51->{},52->{52,53},53->{40,41},54->{54,55},55->{30,31},56->{56,57},57->{20,21},58->{58,59} ,59->{10,11},60->{},61->{},62->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,3,4,5,6,7,9,10,11,13,14,15,16,17,19,20,21,23,24,25,26,27,29,30,31,33,34,35,36,37,39,40,41,43,44,45,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62] | +- p:[58] c: [58] | +- p:[56] c: [56] | +- p:[54] c: [54] | +- p:[52] c: [52] | `- p:[50] c: [50] * Step 7: SizeAbstraction WORST_CASE(?,O(1)) + Considered Problem: (Rules: 0. 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) -> f18(100,0,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f18(100,10,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (1,1) 3. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f21(A,B,B,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B >= 1] (?,1) 4. f18(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,0,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [B = 0] (?,1) 5. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,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) True (?,1) 6. f21(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f27(A,B,C,10,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 7. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,0,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D = 0] (?,1) 9. f27(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,D,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) [D >= 1] (?,1) 10. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,0,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 11. f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f58(A,B,C,D,E,F,200,10,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 13. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f61(A,B,C,D,E,F,G,H,H,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H >= 1] (?,1) 14. f58(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,0,0,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [H = 0] (?,1) 15. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,0,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 16. f61(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f67(A,B,C,D,E,F,G,H,I,10,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 17. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,0,0,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J = 0] (?,1) 19. f67(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,J,0,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [J >= 1] (?,1) 20. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,0,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 21. f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f98(A,B,C,D,E,F,G,H,I,J,K,L,50,10,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 23. 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) -> f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,N,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N >= 1] (?,1) 24. 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) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,0,0,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [N = 0] (?,1) 25. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 26. f101(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,10,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 27. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,0,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P = 0] (?,1) 29. f107(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,P,0,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [P >= 1] (?,1) 30. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,0,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 31. f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,20,10,U,V,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 33. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,T,V,W,X,Y,Z,A1,B1,C1,D1) [T >= 1] (?,1) 34. f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,0,0,V,W,X,Y,Z,A1,B1,C1,D1) [T = 0] (?,1) 35. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 36. f141(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,10,W,X,Y,Z,A1,B1,C1,D1) True (?,1) 37. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,0,X,Y,Z,A1,B1,C1,D1) [V = 0] (?,1) 39. f147(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,V,0,Y,Z,A1,B1,C1,D1) [V >= 1] (?,1) 40. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,0,A1,B1,C1,D1) True (?,1) 41. f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,200,10,A1,B1,C1,D1) True (?,1) 43. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,Z,B1,C1,D1) [Z >= 1] (?,1) 44. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,C1,D1) True (?,1) 45. f181(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,10,C1,D1) True (?,1) 47. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,B1,0) [B1 >= 1] (?,1) 48. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,0,0,B1,C1,D1) [Z = 0] (?,1) 49. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,0,0,D1) [B1 = 0] (?,1) 50. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,1 + D1) [Y >= 1 + D1] (?,1) 51. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f207(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [D1 >= Y] (?,1) 52. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,1 + X,Y,Z,A1,B1,C1,D1) [S >= 1 + X] (?,1) 53. f150(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f166(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [X >= S] (?,1) 54. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,1 + R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [M >= 1 + R] (?,1) 55. f110(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f126(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [R >= M] (?,1) 56. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f70(A,B,C,D,E,F,G,H,I,J,K,1 + L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [G >= 1 + L] (?,1) 57. f70(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f86(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [L >= G] (?,1) 58. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f30(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [A >= 1 + F] (?,1) 59. f30(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> f46(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) [F >= A] (?,1) 60. f190(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> 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) True (?,1) 61. f187(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> 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) True (?,1) 62. f178(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1) -> 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) True (?,1) Signature: {(exitus616,30) ;(f0,30) ;(f101,30) ;(f107,30) ;(f110,30) ;(f126,30) ;(f138,30) ;(f141,30) ;(f147,30) ;(f150,30) ;(f166,30) ;(f178,30) ;(f18,30) ;(f181,30) ;(f187,30) ;(f190,30) ;(f207,30) ;(f21,30) ;(f27,30) ;(f30,30) ;(f46,30) ;(f58,30) ;(f61,30) ;(f67,30) ;(f70,30) ;(f86,30) ;(f98,30)} Flow Graph: [0->{4},1->{3},3->{5,6},4->{10,11},5->{7},6->{9},7->{10,11},9->{58,59},10->{14},11->{13},13->{15,16} ,14->{20,21},15->{17},16->{19},17->{20,21},19->{56,57},20->{24},21->{23},23->{25,26},24->{30,31},25->{27} ,26->{29},27->{30,31},29->{54,55},30->{34},31->{33},33->{35,36},34->{40,41},35->{37},36->{39},37->{40,41} ,39->{52,53},40->{48,62},41->{43,62},43->{44,45},44->{49,61},45->{47,61},47->{50,51,60},48->{},49->{} ,50->{50,51,60},51->{},52->{52,53},53->{40,41},54->{54,55},55->{30,31},56->{56,57},57->{20,21},58->{58,59} ,59->{10,11},60->{},61->{},62->{}] ,We construct a looptree: P: [0,1,3,4,5,6,7,9,10,11,13,14,15,16,17,19,20,21,23,24,25,26,27,29,30,31,33,34,35,36,37,39,40,41,43,44,45,47,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62] | +- p:[58] c: [58] | +- p:[56] c: [56] | +- p:[54] c: [54] | +- p:[52] c: [52] | `- p:[50] c: [50]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 8: FlowAbstraction WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,0.0,0.1,0.2,0.3,0.4] f0 ~> f18 [A <= 100*K, B <= 0*K, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f0 ~> f18 [A <= 100*K, B <= 10*K, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f18 ~> f21 [A <= A, B <= B, C <= B, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f18 ~> f46 [A <= A, B <= 0*K, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f21 ~> f27 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f21 ~> f27 [A <= A, B <= B, C <= C, D <= 10*K, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f27 ~> f46 [A <= A, B <= B, C <= C, D <= 0*K, E <= 0*K, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f27 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= D, F <= 0*K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f46 ~> f58 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 200*K, H <= 0*K, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f46 ~> f58 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= 200*K, H <= 10*K, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f58 ~> f61 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= H, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f58 ~> f86 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= 0*K, I <= 0*K, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f61 ~> f67 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f61 ~> f67 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 10*K, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f67 ~> f86 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= 0*K, K <= 0*K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f67 ~> f70 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= J, L <= 0*K, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f86 ~> f98 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= 50*K, N <= 0*K, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f86 ~> f98 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= 50*K, N <= 10*K, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f98 ~> f101 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= N, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f98 ~> f126 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= 0*K, O <= 0*K, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f101 ~> f107 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f101 ~> f107 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= 10*K, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f107 ~> f126 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= 0*K, Q <= 0*K, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f107 ~> f110 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= P, R <= 0*K, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f126 ~> f138 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= 20*K, T <= 0*K, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f126 ~> f138 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= 20*K, T <= 10*K, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f138 ~> f141 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= T, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f138 ~> f166 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= 0*K, U <= 0*K, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f141 ~> f147 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= 0*K, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f141 ~> f147 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= 10*K, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f147 ~> f166 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= 0*K, W <= 0*K, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f147 ~> f150 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= V, X <= 0*K, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f166 ~> f178 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= 200*K, Z <= 0*K, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f166 ~> f178 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= 200*K, Z <= 10*K, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f178 ~> f181 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= Z, B1 <= B1, C1 <= C1, D1 <= D1] f181 ~> f187 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= 0*K, C1 <= C1, D1 <= D1] f181 ~> f187 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= 10*K, C1 <= C1, D1 <= D1] f187 ~> f190 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= B1, D1 <= 0*K] f178 ~> f207 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= 0*K, A1 <= 0*K, B1 <= B1, C1 <= C1, D1 <= D1] f187 ~> f207 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= 0*K, C1 <= 0*K, D1 <= D1] f190 ~> f190 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1 + Y] f190 ~> f207 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f150 ~> f150 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= S + X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f150 ~> f166 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f110 ~> f110 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= M + R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f110 ~> f126 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f70 ~> f70 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= G + L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f70 ~> f86 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f30 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= A + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f30 ~> f46 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f190 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f187 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] f178 ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] + Loop: [0.0 <= A + F] f30 ~> f30 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= A + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] + Loop: [0.1 <= G + L] f70 ~> f70 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= G + L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] + Loop: [0.2 <= M + R] f110 ~> f110 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= M + R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] + Loop: [0.3 <= S + X] f150 ~> f150 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= S + X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1] + Loop: [0.4 <= D1 + Y] f190 ~> f190 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L, M <= M, N <= N, O <= O, P <= P, Q <= Q, R <= R, S <= S, T <= T, U <= U, V <= V, W <= W, X <= X, Y <= Y, Z <= Z, A1 <= A1, B1 <= B1, C1 <= C1, D1 <= D1 + Y] + Applied Processor: FlowAbstraction + Details: () * Step 9: LareProcessor WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,0.0,0.1,0.2,0.3,0.4] f0 ~> f18 [K ~=> A,K ~=> B] f0 ~> f18 [K ~=> A,K ~=> B] f18 ~> f21 [B ~=> C] f18 ~> f46 [K ~=> B,K ~=> C] f21 ~> f27 [K ~=> D] f21 ~> f27 [K ~=> D] f27 ~> f46 [K ~=> D,K ~=> E] f27 ~> f30 [D ~=> E,K ~=> F] f46 ~> f58 [K ~=> G,K ~=> H] f46 ~> f58 [K ~=> G,K ~=> H] f58 ~> f61 [H ~=> I] f58 ~> f86 [K ~=> H,K ~=> I] f61 ~> f67 [K ~=> J] f61 ~> f67 [K ~=> J] f67 ~> f86 [K ~=> J,K ~=> K] f67 ~> f70 [J ~=> K,K ~=> L] f86 ~> f98 [K ~=> M,K ~=> N] f86 ~> f98 [K ~=> M,K ~=> N] f98 ~> f101 [N ~=> O] f98 ~> f126 [K ~=> N,K ~=> O] f101 ~> f107 [K ~=> P] f101 ~> f107 [K ~=> P] f107 ~> f126 [K ~=> P,K ~=> Q] f107 ~> f110 [P ~=> Q,K ~=> R] f126 ~> f138 [K ~=> S,K ~=> T] f126 ~> f138 [K ~=> S,K ~=> T] f138 ~> f141 [T ~=> U] f138 ~> f166 [K ~=> T,K ~=> U] f141 ~> f147 [K ~=> V] f141 ~> f147 [K ~=> V] f147 ~> f166 [K ~=> V,K ~=> W] f147 ~> f150 [V ~=> W,K ~=> X] f166 ~> f178 [K ~=> Y,K ~=> Z] f166 ~> f178 [K ~=> Y,K ~=> Z] f178 ~> f181 [Z ~=> A1] f181 ~> f187 [K ~=> B1] f181 ~> f187 [K ~=> B1] f187 ~> f190 [B1 ~=> C1,K ~=> D1] f178 ~> f207 [K ~=> A1,K ~=> Z] f187 ~> f207 [K ~=> B1,K ~=> C1] f190 ~> f190 [D1 ~+> D1,Y ~+> D1] f190 ~> f207 [] f150 ~> f150 [S ~+> X,X ~+> X] f150 ~> f166 [] f110 ~> f110 [M ~+> R,R ~+> R] f110 ~> f126 [] f70 ~> f70 [G ~+> L,L ~+> L] f70 ~> f86 [] f30 ~> f30 [A ~+> F,F ~+> F] f30 ~> f46 [] f190 ~> exitus616 [] f187 ~> exitus616 [] f178 ~> exitus616 [] + Loop: [A ~+> 0.0,F ~+> 0.0] f30 ~> f30 [A ~+> F,F ~+> F] + Loop: [G ~+> 0.1,L ~+> 0.1] f70 ~> f70 [G ~+> L,L ~+> L] + Loop: [M ~+> 0.2,R ~+> 0.2] f110 ~> f110 [M ~+> R,R ~+> R] + Loop: [S ~+> 0.3,X ~+> 0.3] f150 ~> f150 [S ~+> X,X ~+> X] + Loop: [D1 ~+> 0.4,Y ~+> 0.4] f190 ~> f190 [D1 ~+> D1,Y ~+> D1] + Applied Processor: LareProcessor + Details: f0 ~> f207 [K ~=> A ,K ~=> A1 ,K ~=> B ,K ~=> B1 ,K ~=> C ,K ~=> C1 ,K ~=> D ,K ~=> D1 ,K ~=> E ,K ~=> F ,K ~=> G ,K ~=> H ,K ~=> I ,K ~=> J ,K ~=> K ,K ~=> L ,K ~=> M ,K ~=> N ,K ~=> O ,K ~=> P ,K ~=> Q ,K ~=> R ,K ~=> S ,K ~=> T ,K ~=> U ,K ~=> V ,K ~=> W ,K ~=> X ,K ~=> Y ,K ~=> Z ,tick ~+> tick ,K ~+> D1 ,K ~+> F ,K ~+> L ,K ~+> R ,K ~+> X ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> 0.4 ,K ~+> tick ,K ~*> D1 ,K ~*> F ,K ~*> L ,K ~*> R ,K ~*> X ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> 0.4 ,K ~*> tick] f0 ~> exitus616 [K ~=> A ,K ~=> A1 ,K ~=> B ,K ~=> B1 ,K ~=> C ,K ~=> C1 ,K ~=> D ,K ~=> D1 ,K ~=> E ,K ~=> F ,K ~=> G ,K ~=> H ,K ~=> I ,K ~=> J ,K ~=> K ,K ~=> L ,K ~=> M ,K ~=> N ,K ~=> O ,K ~=> P ,K ~=> Q ,K ~=> R ,K ~=> S ,K ~=> T ,K ~=> U ,K ~=> V ,K ~=> W ,K ~=> X ,K ~=> Y ,K ~=> Z ,tick ~+> tick ,K ~+> D1 ,K ~+> F ,K ~+> L ,K ~+> R ,K ~+> X ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> 0.4 ,K ~+> tick ,K ~*> D1 ,K ~*> F ,K ~*> L ,K ~*> R ,K ~*> X ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> 0.4 ,K ~*> tick] + f30> [A ~+> F,A ~+> 0.0,A ~+> tick,F ~+> F,F ~+> 0.0,F ~+> tick,tick ~+> tick,A ~*> F,F ~*> F] + f70> [G ~+> L,G ~+> 0.1,G ~+> tick,L ~+> L,L ~+> 0.1,L ~+> tick,tick ~+> tick,G ~*> L,L ~*> L] + f110> [M ~+> R ,M ~+> 0.2 ,M ~+> tick ,R ~+> R ,R ~+> 0.2 ,R ~+> tick ,tick ~+> tick ,M ~*> R ,R ~*> R] + f150> [S ~+> X ,S ~+> 0.3 ,S ~+> tick ,X ~+> X ,X ~+> 0.3 ,X ~+> tick ,tick ~+> tick ,S ~*> X ,X ~*> X] + f190> [D1 ~+> D1 ,D1 ~+> 0.4 ,D1 ~+> tick ,Y ~+> D1 ,Y ~+> 0.4 ,Y ~+> tick ,tick ~+> tick ,D1 ~*> D1 ,Y ~*> D1] YES(?,O(1))