YES(?,O(1)) * Step 1: TrivialSCCs WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] (?,1) 1. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] (?,1) 5. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] (?,1) 6. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] (?,1) 7. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] (?,1) 8. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] (?,1) 9. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] (?,1) 10. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] (?,1) 11. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] (?,1) 12. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] (?,1) 13. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] (?,1) 14. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True (?,1) 15. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True (?,1) 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] (?,1) 17. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] (?,1) 19. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] (?,1) 20. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] (?,1) 21. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] (?,1) 22. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True (?,1) 23. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] (?,1) 24. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] (?,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] (?,1) 26. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] (?,1) 27. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] (?,1) 28. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] (?,1) 29. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] (?,1) 30. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] (?,1) 31. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] (?,1) 32. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] (?,1) 33. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) 34. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{24,25,26},1->{24,25,26},2->{3,34},3->{3,34},4->{6,7,8},5->{6,7,8},6->{4,5,9,33},7->{4,5,9,33},8->{4,5 ,9,33},9->{4,5,9,33},10->{11,12,16,31},11->{13,14,15},12->{13,14,15},13->{11,12,16,31},14->{11,12,16,31} ,15->{11,12,16,31},16->{11,12,16,31},17->{19,20,21,22},18->{19,20,21,22},19->{17,18,23,28,29,30},20->{17,18 ,23,28,29,30},21->{17,18,23,28,29,30},22->{17,18,23,28,29,30},23->{17,18,23,28,29,30},24->{},25->{},26->{} ,27->{},28->{0,1,27},29->{0,1,27},30->{},31->{10,32},32->{17,18,23,28,29,30},33->{10,32},34->{4,5,9,33}] + 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. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] (1,1) 1. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] (?,1) 5. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] (?,1) 6. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] (?,1) 7. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] (?,1) 8. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] (?,1) 9. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] (?,1) 10. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] (?,1) 11. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] (?,1) 12. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] (?,1) 13. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] (?,1) 14. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True (?,1) 15. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True (?,1) 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] (?,1) 17. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] (?,1) 19. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] (?,1) 20. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] (?,1) 21. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] (?,1) 22. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True (?,1) 23. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] (?,1) 24. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] (1,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] (1,1) 26. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] (1,1) 27. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] (1,1) 28. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] (1,1) 29. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] (1,1) 30. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] (1,1) 31. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] (?,1) 32. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] (1,1) 33. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (1,1) 34. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (1,1) Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{24,25,26},1->{24,25,26},2->{3,34},3->{3,34},4->{6,7,8},5->{6,7,8},6->{4,5,9,33},7->{4,5,9,33},8->{4,5 ,9,33},9->{4,5,9,33},10->{11,12,16,31},11->{13,14,15},12->{13,14,15},13->{11,12,16,31},14->{11,12,16,31} ,15->{11,12,16,31},16->{11,12,16,31},17->{19,20,21,22},18->{19,20,21,22},19->{17,18,23,28,29,30},20->{17,18 ,23,28,29,30},21->{17,18,23,28,29,30},22->{17,18,23,28,29,30},23->{17,18,23,28,29,30},24->{},25->{},26->{} ,27->{},28->{0,1,27},29->{0,1,27},30->{},31->{10,32},32->{17,18,23,28,29,30},33->{10,32},34->{4,5,9,33}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,34) ,(6,4) ,(6,9) ,(7,4) ,(7,5) ,(8,4) ,(8,5) ,(9,4) ,(9,5) ,(10,31) ,(13,11) ,(13,16) ,(14,11) ,(14,16) ,(15,11) ,(15,12) ,(16,11) ,(16,12) ,(19,17) ,(19,23) ,(20,17) ,(20,23) ,(21,17) ,(21,18) ,(22,17) ,(22,18) ,(23,17) ,(23,18)] * Step 3: AddSinks WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] (1,1) 1. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] (1,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] (?,1) 5. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] (?,1) 6. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] (?,1) 7. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] (?,1) 8. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] (?,1) 9. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] (?,1) 10. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] (?,1) 11. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] (?,1) 12. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] (?,1) 13. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] (?,1) 14. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True (?,1) 15. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True (?,1) 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] (?,1) 17. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] (?,1) 19. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] (?,1) 20. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] (?,1) 21. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] (?,1) 22. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True (?,1) 23. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] (?,1) 24. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] (1,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] (1,1) 26. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] (1,1) 27. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] (1,1) 28. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] (1,1) 29. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] (1,1) 30. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] (1,1) 31. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] (?,1) 32. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] (1,1) 33. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (1,1) 34. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (1,1) Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{24,25,26},1->{24,25,26},2->{3},3->{3,34},4->{6,7,8},5->{6,7,8},6->{5,33},7->{9,33},8->{9,33},9->{9 ,33},10->{11,12,16},11->{13,14,15},12->{13,14,15},13->{12,31},14->{12,31},15->{16,31},16->{16,31},17->{19,20 ,21,22},18->{19,20,21,22},19->{18,28,29,30},20->{18,28,29,30},21->{23,28,29,30},22->{23,28,29,30},23->{23,28 ,29,30},24->{},25->{},26->{},27->{},28->{0,1,27},29->{0,1,27},30->{},31->{10,32},32->{17,18,23,28,29,30} ,33->{10,32},34->{4,5,9,33}] + Applied Processor: AddSinks + Details: () * Step 4: UnsatPaths WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] (?,1) 1. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] (?,1) 5. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] (?,1) 6. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] (?,1) 7. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] (?,1) 8. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] (?,1) 9. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] (?,1) 10. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] (?,1) 11. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] (?,1) 12. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] (?,1) 13. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] (?,1) 14. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True (?,1) 15. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True (?,1) 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] (?,1) 17. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] (?,1) 19. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] (?,1) 20. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] (?,1) 21. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] (?,1) 22. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True (?,1) 23. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] (?,1) 24. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] (?,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] (?,1) 26. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] (?,1) 27. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] (?,1) 28. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] (?,1) 29. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] (?,1) 30. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] (?,1) 31. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] (?,1) 32. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] (?,1) 33. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) 34. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) 35. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True (?,1) 36. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True (?,1) 37. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True (?,1) Signature: {(exitus616,12) ;(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{24,25,26,37},1->{24,25,26,37},2->{3,34},3->{3,34},4->{6,7,8},5->{6,7,8},6->{4,5,9,33},7->{4,5,9,33} ,8->{4,5,9,33},9->{4,5,9,33},10->{11,12,16,31},11->{13,14,15},12->{13,14,15},13->{11,12,16,31},14->{11,12,16 ,31},15->{11,12,16,31},16->{11,12,16,31},17->{19,20,21,22},18->{19,20,21,22},19->{17,18,23,28,29,30,35} ,20->{17,18,23,28,29,30,35},21->{17,18,23,28,29,30,35},22->{17,18,23,28,29,30,35},23->{17,18,23,28,29,30,35} ,24->{},25->{},26->{},27->{},28->{0,1,27,36},29->{0,1,27,36},30->{},31->{10,32},32->{17,18,23,28,29,30,35} ,33->{10,32},34->{4,5,9,33},35->{},36->{},37->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,34) ,(6,4) ,(6,9) ,(7,4) ,(7,5) ,(8,4) ,(8,5) ,(9,4) ,(9,5) ,(10,31) ,(13,11) ,(13,16) ,(14,11) ,(14,16) ,(15,11) ,(15,12) ,(16,11) ,(16,12) ,(19,17) ,(19,23) ,(20,17) ,(20,23) ,(21,17) ,(21,18) ,(22,17) ,(22,18) ,(23,17) ,(23,18)] * Step 5: LooptreeTransformer WORST_CASE(?,O(1)) + Considered Problem: Rules: 0. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] (?,1) 1. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] (?,1) 5. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] (?,1) 6. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] (?,1) 7. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] (?,1) 8. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] (?,1) 9. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] (?,1) 10. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] (?,1) 11. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] (?,1) 12. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] (?,1) 13. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] (?,1) 14. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True (?,1) 15. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True (?,1) 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] (?,1) 17. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] (?,1) 19. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] (?,1) 20. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] (?,1) 21. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] (?,1) 22. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True (?,1) 23. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] (?,1) 24. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] (?,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] (?,1) 26. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] (?,1) 27. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] (?,1) 28. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] (?,1) 29. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] (?,1) 30. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] (?,1) 31. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] (?,1) 32. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] (?,1) 33. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) 34. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) 35. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True (?,1) 36. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True (?,1) 37. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True (?,1) Signature: {(exitus616,12) ;(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{24,25,26,37},1->{24,25,26,37},2->{3},3->{3,34},4->{6,7,8},5->{6,7,8},6->{5,33},7->{9,33},8->{9,33} ,9->{9,33},10->{11,12,16},11->{13,14,15},12->{13,14,15},13->{12,31},14->{12,31},15->{16,31},16->{16,31} ,17->{19,20,21,22},18->{19,20,21,22},19->{18,28,29,30,35},20->{18,28,29,30,35},21->{23,28,29,30,35},22->{23 ,28,29,30,35},23->{23,28,29,30,35},24->{},25->{},26->{},27->{},28->{0,1,27,36},29->{0,1,27,36},30->{} ,31->{10,32},32->{17,18,23,28,29,30,35},33->{10,32},34->{4,5,9,33},35->{},36->{},37->{}] + 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,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37] | +- p:[3] c: [3] | +- p:[6,5] c: [5] | +- p:[9] c: [9] | +- p:[10,31,13,11,12,14,15,16] c: [10] | | | +- p:[13,12,14] c: [12] | | | `- p:[16] c: [16] | +- p:[19,18,20] c: [18] | `- p:[23] c: [23] * Step 6: SizeAbstraction WORST_CASE(?,O(1)) + Considered Problem: (Rules: 0. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] (?,1) 1. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] (?,1) 5. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] (?,1) 6. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] (?,1) 7. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] (?,1) 8. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] (?,1) 9. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] (?,1) 10. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] (?,1) 11. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] (?,1) 12. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] (?,1) 13. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] (?,1) 14. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True (?,1) 15. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True (?,1) 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] (?,1) 17. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] (?,1) 19. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] (?,1) 20. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] (?,1) 21. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] (?,1) 22. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True (?,1) 23. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] (?,1) 24. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] (?,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] (?,1) 26. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] (?,1) 27. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] (?,1) 28. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] (?,1) 29. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] (?,1) 30. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] (?,1) 31. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] (?,1) 32. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] (?,1) 33. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) 34. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) 35. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True (?,1) 36. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True (?,1) 37. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> exitus616(A,B,C,D,E,F,G,H,I,J,K,L) True (?,1) Signature: {(exitus616,12) ;(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{24,25,26,37},1->{24,25,26,37},2->{3},3->{3,34},4->{6,7,8},5->{6,7,8},6->{5,33},7->{9,33},8->{9,33} ,9->{9,33},10->{11,12,16},11->{13,14,15},12->{13,14,15},13->{12,31},14->{12,31},15->{16,31},16->{16,31} ,17->{19,20,21,22},18->{19,20,21,22},19->{18,28,29,30,35},20->{18,28,29,30,35},21->{23,28,29,30,35},22->{23 ,28,29,30,35},23->{23,28,29,30,35},24->{},25->{},26->{},27->{},28->{0,1,27,36},29->{0,1,27,36},30->{} ,31->{10,32},32->{17,18,23,28,29,30,35},33->{10,32},34->{4,5,9,33},35->{},36->{},37->{}] ,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,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37] | +- p:[3] c: [3] | +- p:[6,5] c: [5] | +- p:[9] c: [9] | +- p:[10,31,13,11,12,14,15,16] c: [10] | | | +- p:[13,12,14] c: [12] | | | `- p:[16] c: [16] | +- p:[19,18,20] c: [18] | `- p:[23] c: [23]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [A,B,C,D,E,F,G,H,I,J,K,L,0.0,0.1,0.2,0.3,0.3.0,0.3.1,0.4,0.5] f62 ~> f63 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f62 ~> f63 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f0 ~> f13 [A <= K, B <= 12*K, C <= K, D <= K, E <= unknown, F <= 0*K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f13 ~> f13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= B + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f19 ~> f22 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f19 ~> f22 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f22 ~> f19 [A <= A, B <= B, C <= K, D <= D, E <= E, F <= K + F, G <= K, H <= H, I <= I, J <= J, K <= K, L <= L] f22 ~> f19 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= K + F, G <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L] f22 ~> f19 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= K + F, G <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L] f19 ~> f19 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= B + F, G <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L] f32 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= B + F, I <= I, J <= J, K <= K, L <= L] f35 ~> f38 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f35 ~> f38 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f38 ~> f35 [A <= K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= K, J <= J, K <= K, L <= L] f38 ~> f35 [A <= K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= K, J <= J, K <= K, L <= L] f38 ~> f35 [A <= 0*K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= 0*K, J <= J, K <= K, L <= L] f35 ~> f35 [A <= 0*K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= B + H, I <= 0*K, J <= J, K <= K, L <= L] f48 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= L] f48 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= L] f52 ~> f48 [A <= A, B <= B, C <= C, D <= K, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f52 ~> f48 [A <= A, B <= B, C <= C, D <= K, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f52 ~> f48 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= 0*K, K <= 0*K, L <= L] f52 ~> f48 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= 0*K, L <= L] f48 ~> f48 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= B + F, G <= G, H <= H, I <= I, J <= unknown, K <= 0*K, L <= L] f63 ~> f71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= 0*K] f63 ~> f71 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= 0*K] f63 ~> f71 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= K] f62 ~> f71 [A <= 0*K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= K] f48 ~> f62 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f48 ~> f62 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f48 ~> f71 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= K] f35 ~> f32 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f32 ~> f48 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= 0*K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f19 ~> f32 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= 0*K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f13 ~> f19 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= 0*K, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f48 ~> 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] f62 ~> 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] f63 ~> 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] + Loop: [0.0 <= B + F] f13 ~> f13 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= B + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] + Loop: [0.1 <= 2*K + B + F] f22 ~> f19 [A <= A, B <= B, C <= K, D <= D, E <= E, F <= K + F, G <= K, H <= H, I <= I, J <= J, K <= K, L <= L] f19 ~> f22 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] + Loop: [0.2 <= B + F] f19 ~> f19 [A <= A, B <= B, C <= 0*K, D <= D, E <= E, F <= B + F, G <= 0*K, H <= H, I <= I, J <= J, K <= K, L <= L] + Loop: [0.3 <= 2*K + B + F] f32 ~> f35 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= B + F, I <= I, J <= J, K <= K, L <= L] f35 ~> f32 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f38 ~> f35 [A <= K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= K, J <= J, K <= K, L <= L] f35 ~> f38 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f35 ~> f38 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f38 ~> f35 [A <= K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= K, J <= J, K <= K, L <= L] f38 ~> f35 [A <= 0*K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= 0*K, J <= J, K <= K, L <= L] f35 ~> f35 [A <= 0*K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= B + H, I <= 0*K, J <= J, K <= K, L <= L] + Loop: [0.3.0 <= 2*K + B + H] f38 ~> f35 [A <= K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= K, J <= J, K <= K, L <= L] f35 ~> f38 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f38 ~> f35 [A <= K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= K + H, I <= K, J <= J, K <= K, L <= L] + Loop: [0.3.1 <= B + H] f35 ~> f35 [A <= 0*K, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= B + H, I <= 0*K, J <= J, K <= K, L <= L] + Loop: [0.4 <= 2*K + B + F] f52 ~> f48 [A <= A, B <= B, C <= C, D <= K, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] f48 ~> f52 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F, G <= G, H <= H, I <= I, J <= unknown, K <= K, L <= L] f52 ~> f48 [A <= A, B <= B, C <= C, D <= K, E <= E, F <= K + F, G <= G, H <= H, I <= I, J <= J, K <= K, L <= L] + Loop: [0.5 <= K + B + F] f48 ~> f48 [A <= A, B <= B, C <= C, D <= 0*K, E <= E, F <= B + F, G <= G, H <= H, I <= I, J <= unknown, K <= 0*K, L <= L] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,O(1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,G,H,I,J,K,L,0.0,0.1,0.2,0.3,0.3.0,0.3.1,0.4,0.5] f62 ~> f63 [] f62 ~> f63 [] f0 ~> f13 [K ~=> A,K ~=> B,K ~=> C,K ~=> D,K ~=> F,huge ~=> E] f13 ~> f13 [B ~+> F,F ~+> F] f19 ~> f22 [] f19 ~> f22 [] f22 ~> f19 [K ~=> C,K ~=> G,F ~+> F,K ~+> F] f22 ~> f19 [K ~=> C,K ~=> G,F ~+> F,K ~+> F] f22 ~> f19 [K ~=> C,K ~=> G,F ~+> F,K ~+> F] f19 ~> f19 [K ~=> C,K ~=> G,B ~+> F,F ~+> F] f32 ~> f35 [B ~+> H,F ~+> H] f35 ~> f38 [] f35 ~> f38 [] f38 ~> f35 [K ~=> A,K ~=> I,H ~+> H,K ~+> H] f38 ~> f35 [K ~=> A,K ~=> I,H ~+> H,K ~+> H] f38 ~> f35 [K ~=> A,K ~=> I,H ~+> H,K ~+> H] f35 ~> f35 [K ~=> A,K ~=> I,B ~+> H,H ~+> H] f48 ~> f52 [huge ~=> J] f48 ~> f52 [huge ~=> J] f52 ~> f48 [K ~=> D,K ~=> K,F ~+> F,K ~+> F] f52 ~> f48 [K ~=> D,K ~=> K,F ~+> F,K ~+> F] f52 ~> f48 [K ~=> D,K ~=> J,K ~=> K,F ~+> F,K ~+> F] f52 ~> f48 [K ~=> D,K ~=> K,F ~+> F,K ~+> F] f48 ~> f48 [K ~=> D,K ~=> K,huge ~=> J,B ~+> F,F ~+> F] f63 ~> f71 [K ~=> L] f63 ~> f71 [K ~=> L] f63 ~> f71 [K ~=> D,K ~=> L] f62 ~> f71 [K ~=> A,K ~=> L] f48 ~> f62 [] f48 ~> f62 [] f48 ~> f71 [K ~=> C,K ~=> L] f35 ~> f32 [F ~+> F,K ~+> F] f32 ~> f48 [K ~=> F] f19 ~> f32 [K ~=> F] f13 ~> f19 [K ~=> F] f48 ~> exitus616 [] f62 ~> exitus616 [] f63 ~> exitus616 [] + Loop: [B ~+> 0.0,F ~+> 0.0] f13 ~> f13 [B ~+> F,F ~+> F] + Loop: [B ~+> 0.1,F ~+> 0.1,K ~*> 0.1] f22 ~> f19 [K ~=> C,K ~=> G,F ~+> F,K ~+> F] f19 ~> f22 [] + Loop: [B ~+> 0.2,F ~+> 0.2] f19 ~> f19 [K ~=> C,K ~=> G,B ~+> F,F ~+> F] + Loop: [B ~+> 0.3,F ~+> 0.3,K ~*> 0.3] f32 ~> f35 [B ~+> H,F ~+> H] f35 ~> f32 [F ~+> F,K ~+> F] f38 ~> f35 [K ~=> A,K ~=> I,H ~+> H,K ~+> H] f35 ~> f38 [] f35 ~> f38 [] f38 ~> f35 [K ~=> A,K ~=> I,H ~+> H,K ~+> H] f38 ~> f35 [K ~=> A,K ~=> I,H ~+> H,K ~+> H] f35 ~> f35 [K ~=> A,K ~=> I,B ~+> H,H ~+> H] + Loop: [B ~+> 0.3.0,H ~+> 0.3.0,K ~*> 0.3.0] f38 ~> f35 [K ~=> A,K ~=> I,H ~+> H,K ~+> H] f35 ~> f38 [] f38 ~> f35 [K ~=> A,K ~=> I,H ~+> H,K ~+> H] + Loop: [B ~+> 0.3.1,H ~+> 0.3.1] f35 ~> f35 [K ~=> A,K ~=> I,B ~+> H,H ~+> H] + Loop: [B ~+> 0.4,F ~+> 0.4,K ~*> 0.4] f52 ~> f48 [K ~=> D,K ~=> K,F ~+> F,K ~+> F] f48 ~> f52 [huge ~=> J] f52 ~> f48 [K ~=> D,K ~=> K,F ~+> F,K ~+> F] + Loop: [B ~+> 0.5,F ~+> 0.5,K ~+> 0.5] f48 ~> f48 [K ~=> D,K ~=> K,huge ~=> J,B ~+> F,F ~+> F] + Applied Processor: LareProcessor + Details: f0 ~> exitus616 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> F ,K ~=> G ,K ~=> I ,K ~=> J ,K ~=> K ,huge ~=> E ,huge ~=> J ,tick ~+> tick ,K ~+> F ,K ~+> H ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> 0.3.0 ,K ~+> 0.3.1 ,K ~+> 0.4 ,K ~+> 0.5 ,K ~+> tick ,K ~*> F ,K ~*> H ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> 0.3.0 ,K ~*> 0.3.1 ,K ~*> 0.4 ,K ~*> 0.5 ,K ~*> tick ,K ~^> H] f0 ~> f71 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> F ,K ~=> G ,K ~=> I ,K ~=> J ,K ~=> K ,K ~=> L ,huge ~=> E ,huge ~=> J ,tick ~+> tick ,K ~+> F ,K ~+> H ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> 0.3.0 ,K ~+> 0.3.1 ,K ~+> 0.4 ,K ~+> 0.5 ,K ~+> tick ,K ~*> F ,K ~*> H ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> 0.3.0 ,K ~*> 0.3.1 ,K ~*> 0.4 ,K ~*> 0.5 ,K ~*> tick ,K ~^> H] f0 ~> f22 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> F ,K ~=> G ,huge ~=> E ,tick ~+> tick ,K ~+> F ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> tick ,K ~*> F ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> tick] f0 ~> f38 [K ~=> A ,K ~=> B ,K ~=> C ,K ~=> D ,K ~=> F ,K ~=> G ,K ~=> I ,huge ~=> E ,tick ~+> tick ,K ~+> F ,K ~+> H ,K ~+> 0.0 ,K ~+> 0.1 ,K ~+> 0.2 ,K ~+> 0.3 ,K ~+> 0.3.0 ,K ~+> 0.3.1 ,K ~+> tick ,K ~*> F ,K ~*> H ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> 0.2 ,K ~*> 0.3 ,K ~*> 0.3.0 ,K ~*> 0.3.1 ,K ~*> tick ,K ~^> H ,K ~^> 0.3.0 ,K ~^> tick] + f13> [B ~+> F,B ~+> 0.0,B ~+> tick,F ~+> F,F ~+> 0.0,F ~+> tick,tick ~+> tick,B ~*> F,F ~*> F] + f19> [K ~=> C ,K ~=> G ,B ~+> 0.1 ,B ~+> tick ,F ~+> F ,F ~+> 0.1 ,F ~+> tick ,tick ~+> tick ,K ~+> F ,B ~*> F ,F ~*> F ,K ~*> F ,K ~*> 0.1 ,K ~*> tick] f22> [K ~=> C ,K ~=> G ,B ~+> 0.1 ,B ~+> tick ,F ~+> F ,F ~+> 0.1 ,F ~+> tick ,tick ~+> tick ,K ~+> F ,B ~*> F ,F ~*> F ,K ~*> F ,K ~*> 0.1 ,K ~*> tick] + f19> [K ~=> C ,K ~=> G ,B ~+> F ,B ~+> 0.2 ,B ~+> tick ,F ~+> F ,F ~+> 0.2 ,F ~+> tick ,tick ~+> tick ,B ~*> F ,F ~*> F] + f32> [K ~=> A ,K ~=> I ,B ~+> H ,B ~+> 0.3 ,B ~+> 0.3.0 ,B ~+> 0.3.1 ,B ~+> tick ,F ~+> F ,F ~+> H ,F ~+> 0.3 ,F ~+> 0.3.0 ,F ~+> 0.3.1 ,F ~+> tick ,tick ~+> tick ,K ~+> F ,K ~+> H ,K ~+> 0.3.0 ,K ~+> 0.3.1 ,K ~+> tick ,B ~*> F ,B ~*> H ,B ~*> 0.3.0 ,B ~*> 0.3.1 ,B ~*> tick ,F ~*> F ,F ~*> H ,F ~*> 0.3.0 ,F ~*> 0.3.1 ,F ~*> tick ,K ~*> F ,K ~*> H ,K ~*> 0.3 ,K ~*> 0.3.0 ,K ~*> 0.3.1 ,K ~*> tick ,B ~^> H ,F ~^> H ,K ~^> H] f38 [K ~=> A ,K ~=> I ,B ~+> H ,B ~+> 0.3 ,B ~+> 0.3.0 ,B ~+> 0.3.1 ,B ~+> tick ,F ~+> F ,F ~+> H ,F ~+> 0.3 ,F ~+> 0.3.0 ,F ~+> 0.3.1 ,F ~+> tick ,tick ~+> tick ,K ~+> F ,K ~+> H ,K ~+> 0.3.0 ,K ~+> 0.3.1 ,K ~+> tick ,B ~*> F ,B ~*> H ,B ~*> 0.3.0 ,B ~*> 0.3.1 ,B ~*> tick ,F ~*> F ,F ~*> H ,F ~*> 0.3.0 ,F ~*> 0.3.1 ,F ~*> tick ,K ~*> F ,K ~*> H ,K ~*> 0.3 ,K ~*> 0.3.0 ,K ~*> 0.3.1 ,K ~*> tick ,B ~^> H ,B ~^> 0.3.0 ,B ~^> tick ,F ~^> H ,F ~^> 0.3.0 ,F ~^> tick ,K ~^> H ,K ~^> 0.3.0 ,K ~^> tick] + f35> [K ~=> A ,K ~=> I ,B ~+> 0.3.0 ,B ~+> tick ,H ~+> H ,H ~+> 0.3.0 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,B ~*> H ,H ~*> H ,K ~*> H ,K ~*> 0.3.0 ,K ~*> tick] f38> [K ~=> A ,K ~=> I ,B ~+> 0.3.0 ,B ~+> tick ,H ~+> H ,H ~+> 0.3.0 ,H ~+> tick ,tick ~+> tick ,K ~+> H ,B ~*> H ,H ~*> H ,K ~*> H ,K ~*> 0.3.0 ,K ~*> tick] + f35> [K ~=> A ,K ~=> I ,B ~+> H ,B ~+> 0.3.1 ,B ~+> tick ,H ~+> H ,H ~+> 0.3.1 ,H ~+> tick ,tick ~+> tick ,B ~*> H ,H ~*> H] + f48> [K ~=> D ,K ~=> K ,huge ~=> J ,B ~+> 0.4 ,B ~+> tick ,F ~+> F ,F ~+> 0.4 ,F ~+> tick ,tick ~+> tick ,K ~+> F ,B ~*> F ,F ~*> F ,K ~*> F ,K ~*> 0.4 ,K ~*> tick] f52> [K ~=> D ,K ~=> K ,huge ~=> J ,B ~+> 0.4 ,B ~+> tick ,F ~+> F ,F ~+> 0.4 ,F ~+> tick ,tick ~+> tick ,K ~+> F ,B ~*> F ,F ~*> F ,K ~*> F ,K ~*> 0.4 ,K ~*> tick] + f48> [K ~=> D ,K ~=> K ,huge ~=> J ,B ~+> F ,B ~+> 0.5 ,B ~+> tick ,F ~+> F ,F ~+> 0.5 ,F ~+> tick ,tick ~+> tick ,K ~+> 0.5 ,K ~+> tick ,B ~*> F ,F ~*> F ,K ~*> F] YES(?,O(1))