YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1) 1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (?,1) 2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (?,1) 4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1) 5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1) 6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1) 7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1) 8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1) 9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1) 10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1) 11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1) 12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1) 13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1) 14. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 1] (?,1) 15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1) 17. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= D] (?,1) 18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1) 19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1) 21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1) 22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1) 23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1) 24. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 3] (?,1) 25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1) 27. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [2 >= D] (?,1) 28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1) 29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (?,1) Signature: {(evalrandom2dLeafBlock1in,4) ;(evalrandom2dLeafBlock3in,4) ;(evalrandom2dLeafBlock5in,4) ;(evalrandom2dLeafBlockin,4) ;(evalrandom2dNewDefaultin,4) ;(evalrandom2dNodeBlock7in,4) ;(evalrandom2dNodeBlock9in,4) ;(evalrandom2dNodeBlockin,4) ;(evalrandom2dbb10in,4) ;(evalrandom2dbb2in,4) ;(evalrandom2dbb3in,4) ;(evalrandom2dbb5in,4) ;(evalrandom2dbb7in,4) ;(evalrandom2dbb9in,4) ;(evalrandom2dbbin,4) ;(evalrandom2dentryin,4) ;(evalrandom2dreturnin,4) ;(evalrandom2dstart,4) ;(evalrandom2dstop,4)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{31},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13,14} ,11->{16,17,18},12->{15},13->{30},14->{30},15->{2,3},16->{19},17->{30},18->{30},19->{2,3},20->{22,23,24} ,21->{26,27,28},22->{25},23->{30},24->{30},25->{2,3},26->{29},27->{30},28->{30},29->{2,3},30->{2,3},31->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1) 1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (1,1) 2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (1,1) 4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1) 5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1) 6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1) 7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1) 8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1) 9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1) 10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1) 11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1) 12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1) 13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1) 14. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 1] (?,1) 15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1) 17. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= D] (?,1) 18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1) 19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1) 21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1) 22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1) 23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1) 24. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 3] (?,1) 25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1) 27. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [2 >= D] (?,1) 28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1) 29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (1,1) Signature: {(evalrandom2dLeafBlock1in,4) ;(evalrandom2dLeafBlock3in,4) ;(evalrandom2dLeafBlock5in,4) ;(evalrandom2dLeafBlockin,4) ;(evalrandom2dNewDefaultin,4) ;(evalrandom2dNodeBlock7in,4) ;(evalrandom2dNodeBlock9in,4) ;(evalrandom2dNodeBlockin,4) ;(evalrandom2dbb10in,4) ;(evalrandom2dbb2in,4) ;(evalrandom2dbb3in,4) ;(evalrandom2dbb5in,4) ;(evalrandom2dbb7in,4) ;(evalrandom2dbb9in,4) ;(evalrandom2dbbin,4) ;(evalrandom2dentryin,4) ;(evalrandom2dreturnin,4) ;(evalrandom2dstart,4) ;(evalrandom2dstop,4)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{31},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13,14} ,11->{16,17,18},12->{15},13->{30},14->{30},15->{2,3},16->{19},17->{30},18->{30},19->{2,3},20->{22,23,24} ,21->{26,27,28},22->{25},23->{30},24->{30},25->{2,3},26->{29},27->{30},28->{30},29->{2,3},30->{2,3},31->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(10,14),(11,17),(20,24),(21,27)] * Step 3: UnreachableRules WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1) 1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (1,1) 2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (1,1) 4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1) 5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1) 6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1) 7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1) 8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1) 9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1) 10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1) 11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1) 12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1) 13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1) 14. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 1] (?,1) 15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1) 17. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= D] (?,1) 18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1) 19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1) 21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1) 22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1) 23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1) 24. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 3] (?,1) 25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1) 27. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [2 >= D] (?,1) 28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1) 29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (1,1) Signature: {(evalrandom2dLeafBlock1in,4) ;(evalrandom2dLeafBlock3in,4) ;(evalrandom2dLeafBlock5in,4) ;(evalrandom2dLeafBlockin,4) ;(evalrandom2dNewDefaultin,4) ;(evalrandom2dNodeBlock7in,4) ;(evalrandom2dNodeBlock9in,4) ;(evalrandom2dNodeBlockin,4) ;(evalrandom2dbb10in,4) ;(evalrandom2dbb2in,4) ;(evalrandom2dbb3in,4) ;(evalrandom2dbb5in,4) ;(evalrandom2dbb7in,4) ;(evalrandom2dbb9in,4) ;(evalrandom2dbbin,4) ;(evalrandom2dentryin,4) ;(evalrandom2dreturnin,4) ;(evalrandom2dstart,4) ;(evalrandom2dstop,4)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{31},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13} ,11->{16,18},12->{15},13->{30},14->{30},15->{2,3},16->{19},17->{30},18->{30},19->{2,3},20->{22,23},21->{26 ,28},22->{25},23->{30},24->{30},25->{2,3},26->{29},27->{30},28->{30},29->{2,3},30->{2,3},31->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [14,17,24,27] * Step 4: AddSinks WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1) 1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (1,1) 2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (1,1) 4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1) 5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1) 6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1) 7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1) 8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1) 9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1) 10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1) 11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1) 12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1) 13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1) 15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1) 18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1) 19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1) 21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1) 22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1) 23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1) 25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1) 28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1) 29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (1,1) Signature: {(evalrandom2dLeafBlock1in,4) ;(evalrandom2dLeafBlock3in,4) ;(evalrandom2dLeafBlock5in,4) ;(evalrandom2dLeafBlockin,4) ;(evalrandom2dNewDefaultin,4) ;(evalrandom2dNodeBlock7in,4) ;(evalrandom2dNodeBlock9in,4) ;(evalrandom2dNodeBlockin,4) ;(evalrandom2dbb10in,4) ;(evalrandom2dbb2in,4) ;(evalrandom2dbb3in,4) ;(evalrandom2dbb5in,4) ;(evalrandom2dbb7in,4) ;(evalrandom2dbb9in,4) ;(evalrandom2dbbin,4) ;(evalrandom2dentryin,4) ;(evalrandom2dreturnin,4) ;(evalrandom2dstart,4) ;(evalrandom2dstop,4)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{31},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13} ,11->{16,18},12->{15},13->{30},15->{2,3},16->{19},18->{30},19->{2,3},20->{22,23},21->{26,28},22->{25} ,23->{30},25->{2,3},26->{29},28->{30},29->{2,3},30->{2,3},31->{}] + Applied Processor: AddSinks + Details: () * Step 5: LooptreeTransformer WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1) 1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (?,1) 2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (?,1) 4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1) 5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1) 6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1) 7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1) 8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1) 9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1) 10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1) 11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1) 12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1) 13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1) 15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1) 18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1) 19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1) 21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1) 22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1) 23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1) 25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1) 28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1) 29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (?,1) 32. evalrandom2dreturnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalrandom2dLeafBlock1in,4) ;(evalrandom2dLeafBlock3in,4) ;(evalrandom2dLeafBlock5in,4) ;(evalrandom2dLeafBlockin,4) ;(evalrandom2dNewDefaultin,4) ;(evalrandom2dNodeBlock7in,4) ;(evalrandom2dNodeBlock9in,4) ;(evalrandom2dNodeBlockin,4) ;(evalrandom2dbb10in,4) ;(evalrandom2dbb2in,4) ;(evalrandom2dbb3in,4) ;(evalrandom2dbb5in,4) ;(evalrandom2dbb7in,4) ;(evalrandom2dbb9in,4) ;(evalrandom2dbbin,4) ;(evalrandom2dentryin,4) ;(evalrandom2dreturnin,4) ;(evalrandom2dstart,4) ;(evalrandom2dstop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{31,32},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13} ,11->{16,18},12->{15},13->{30},15->{2,3},16->{19},18->{30},19->{2,3},20->{22,23},21->{26,28},22->{25} ,23->{30},25->{2,3},26->{29},28->{30},29->{2,3},30->{2,3},31->{},32->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,15,16,18,19,20,21,22,23,25,26,28,29,30,31,32] | `- p:[2,5,6,15,12,10,8,7,4,19,16,11,25,22,20,9,29,26,21,30,13,18,23,28] c: [2] * Step 6: SizeAbstraction WORST_CASE(?,O(n^1)) + Considered Problem: (Rules: 0. evalrandom2dstart(A,B,C,D) -> evalrandom2dentryin(A,B,C,D) True (1,1) 1. evalrandom2dentryin(A,B,C,D) -> evalrandom2dbb10in(0,B,C,D) True (?,1) 2. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dbbin(A,B,C,D) [B >= 1 + A] (?,1) 3. evalrandom2dbb10in(A,B,C,D) -> evalrandom2dreturnin(A,B,C,D) [A >= B] (?,1) 4. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb2in(A,B,1 + A,E) [E >= 0 && 3 >= E] (?,1) 5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (?,1) 6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (?,1) 7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (?,1) 8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (?,1) 9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (?,1) 10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (?,1) 11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (?,1) 12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (?,1) 13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (?,1) 15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (?,1) 18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (?,1) 19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (?,1) 21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (?,1) 22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (?,1) 23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (?,1) 25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (?,1) 28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (?,1) 29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (?,1) 31. evalrandom2dreturnin(A,B,C,D) -> evalrandom2dstop(A,B,C,D) True (?,1) 32. evalrandom2dreturnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) Signature: {(evalrandom2dLeafBlock1in,4) ;(evalrandom2dLeafBlock3in,4) ;(evalrandom2dLeafBlock5in,4) ;(evalrandom2dLeafBlockin,4) ;(evalrandom2dNewDefaultin,4) ;(evalrandom2dNodeBlock7in,4) ;(evalrandom2dNodeBlock9in,4) ;(evalrandom2dNodeBlockin,4) ;(evalrandom2dbb10in,4) ;(evalrandom2dbb2in,4) ;(evalrandom2dbb3in,4) ;(evalrandom2dbb5in,4) ;(evalrandom2dbb7in,4) ;(evalrandom2dbb9in,4) ;(evalrandom2dbbin,4) ;(evalrandom2dentryin,4) ;(evalrandom2dreturnin,4) ;(evalrandom2dstart,4) ;(evalrandom2dstop,4) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{31,32},4->{7},5->{2,3},6->{2,3},7->{8,9},8->{10,11},9->{20,21},10->{12,13} ,11->{16,18},12->{15},13->{30},15->{2,3},16->{19},18->{30},19->{2,3},20->{22,23},21->{26,28},22->{25} ,23->{30},25->{2,3},26->{29},28->{30},29->{2,3},30->{2,3},31->{},32->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,15,16,18,19,20,21,22,23,25,26,28,29,30,31,32] | `- p:[2,5,6,15,12,10,8,7,4,19,16,11,25,22,20,9,29,26,21,30,13,18,23,28] c: [2]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [A,B,C,D,0.0] evalrandom2dstart ~> evalrandom2dentryin [A <= A, B <= B, C <= C, D <= D] evalrandom2dentryin ~> evalrandom2dbb10in [A <= 0*K, B <= B, C <= C, D <= D] evalrandom2dbb10in ~> evalrandom2dbbin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb10in ~> evalrandom2dreturnin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb2in [A <= A, B <= B, C <= K + A, D <= 3*K] evalrandom2dbbin ~> evalrandom2dbb10in [A <= K + A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= K + A, B <= B, C <= C, D <= D] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlockin [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlockin ~> evalrandom2dbb3in [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlockin ~> evalrandom2dNewDefaultin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb3in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock1in ~> evalrandom2dNewDefaultin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb5in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock3in ~> evalrandom2dNewDefaultin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb7in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock5in ~> evalrandom2dNewDefaultin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb9in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dNewDefaultin ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dreturnin ~> evalrandom2dstop [A <= A, B <= B, C <= C, D <= D] evalrandom2dreturnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A + B + C] evalrandom2dbb10in ~> evalrandom2dbbin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= K + A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= K + A, B <= B, C <= C, D <= D] evalrandom2dbb3in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlockin ~> evalrandom2dbb3in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlockin [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb2in [A <= A, B <= B, C <= K + A, D <= 3*K] evalrandom2dbb5in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb7in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb9in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNewDefaultin ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlockin ~> evalrandom2dNewDefaultin [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock1in ~> evalrandom2dNewDefaultin [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock3in ~> evalrandom2dNewDefaultin [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock5in ~> evalrandom2dNewDefaultin [A <= A, B <= B, C <= C, D <= D] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor WORST_CASE(?,O(n^1)) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0] evalrandom2dstart ~> evalrandom2dentryin [] evalrandom2dentryin ~> evalrandom2dbb10in [K ~=> A] evalrandom2dbb10in ~> evalrandom2dbbin [] evalrandom2dbb10in ~> evalrandom2dreturnin [] evalrandom2dbbin ~> evalrandom2dbb2in [K ~=> D,A ~+> C,K ~+> C] evalrandom2dbbin ~> evalrandom2dbb10in [A ~+> A,K ~+> A] evalrandom2dbbin ~> evalrandom2dbb10in [A ~+> A,K ~+> A] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlockin [] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [] evalrandom2dLeafBlockin ~> evalrandom2dbb3in [] evalrandom2dLeafBlockin ~> evalrandom2dNewDefaultin [] evalrandom2dbb3in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [] evalrandom2dLeafBlock1in ~> evalrandom2dNewDefaultin [] evalrandom2dbb5in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [] evalrandom2dLeafBlock3in ~> evalrandom2dNewDefaultin [] evalrandom2dbb7in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [] evalrandom2dLeafBlock5in ~> evalrandom2dNewDefaultin [] evalrandom2dbb9in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dNewDefaultin ~> evalrandom2dbb10in [C ~=> A] evalrandom2dreturnin ~> evalrandom2dstop [] evalrandom2dreturnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,C ~+> 0.0,K ~+> 0.0] evalrandom2dbb10in ~> evalrandom2dbbin [] evalrandom2dbbin ~> evalrandom2dbb10in [A ~+> A,K ~+> A] evalrandom2dbbin ~> evalrandom2dbb10in [A ~+> A,K ~+> A] evalrandom2dbb3in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlockin ~> evalrandom2dbb3in [] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlockin [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [] evalrandom2dbbin ~> evalrandom2dbb2in [K ~=> D,A ~+> C,K ~+> C] evalrandom2dbb5in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [] evalrandom2dbb7in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [] evalrandom2dbb9in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [] evalrandom2dNewDefaultin ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlockin ~> evalrandom2dNewDefaultin [] evalrandom2dLeafBlock1in ~> evalrandom2dNewDefaultin [] evalrandom2dLeafBlock3in ~> evalrandom2dNewDefaultin [] evalrandom2dLeafBlock5in ~> evalrandom2dNewDefaultin [] + Applied Processor: LareProcessor + Details: evalrandom2dstart ~> exitus616 [K ~=> A ,K ~=> D ,B ~+> 0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,B ~*> A ,C ~*> A ,K ~*> A ,K ~*> C ,K ~*> 0.0 ,K ~*> tick] evalrandom2dstart ~> evalrandom2dstop [K ~=> A ,K ~=> D ,B ~+> 0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,B ~*> A ,C ~*> A ,K ~*> A ,K ~*> C ,K ~*> 0.0 ,K ~*> tick] + evalrandom2dbb10in> [K ~=> D ,A ~+> A ,A ~+> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> C ,K ~+> 0.0 ,K ~+> tick ,A ~*> A ,B ~*> A ,C ~*> A ,K ~*> A ,K ~*> C] YES(?,O(n^1))