YES(?,O(n^1)) * Step 1: 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) 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: UnsatPaths + Details: We remove following edges from the transition graph: [(10,14),(11,17),(20,24),(21,27)] * Step 2: 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) 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} ,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 3: 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) 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) 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 4: PolyRank 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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalrandom2dLeafBlock1in) = x2 + -1*x3 p(evalrandom2dLeafBlock3in) = x2 + -1*x3 p(evalrandom2dLeafBlock5in) = x2 + -1*x3 p(evalrandom2dLeafBlockin) = x2 + -1*x3 p(evalrandom2dNewDefaultin) = x2 + -1*x3 p(evalrandom2dNodeBlock7in) = x2 + -1*x3 p(evalrandom2dNodeBlock9in) = x2 + -1*x3 p(evalrandom2dNodeBlockin) = x2 + -1*x3 p(evalrandom2dbb10in) = -1*x1 + x2 p(evalrandom2dbb2in) = x2 + -1*x3 p(evalrandom2dbb3in) = x2 + -1*x3 p(evalrandom2dbb5in) = x2 + -1*x3 p(evalrandom2dbb7in) = x2 + -1*x3 p(evalrandom2dbb9in) = x2 + -1*x3 p(evalrandom2dbbin) = -1 + -1*x1 + x2 p(evalrandom2dentryin) = x2 p(evalrandom2dreturnin) = -1*x1 + x2 p(evalrandom2dstart) = x2 p(evalrandom2dstop) = -1*x1 + x2 Following rules are strictly oriented: [B >= 1 + A] ==> evalrandom2dbb10in(A,B,C,D) = -1*A + B > -1 + -1*A + B = evalrandom2dbbin(A,B,C,D) Following rules are weakly oriented: True ==> evalrandom2dstart(A,B,C,D) = B >= B = evalrandom2dentryin(A,B,C,D) True ==> evalrandom2dentryin(A,B,C,D) = B >= B = evalrandom2dbb10in(0,B,C,D) [A >= B] ==> evalrandom2dbb10in(A,B,C,D) = -1*A + B >= -1*A + B = evalrandom2dreturnin(A,B,C,D) [E >= 0 && 3 >= E] ==> evalrandom2dbbin(A,B,C,D) = -1 + -1*A + B >= -1 + -1*A + B = evalrandom2dbb2in(A,B,1 + A,E) [0 >= 1 + E] ==> evalrandom2dbbin(A,B,C,D) = -1 + -1*A + B >= -1 + -1*A + B = evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] ==> evalrandom2dbbin(A,B,C,D) = -1 + -1*A + B >= -1 + -1*A + B = evalrandom2dbb10in(1 + A,B,C,D) True ==> evalrandom2dbb2in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dNodeBlock9in(A,B,C,D) [1 >= D] ==> evalrandom2dNodeBlock9in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dNodeBlockin(A,B,C,D) [D >= 2] ==> evalrandom2dNodeBlock9in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dNodeBlock7in(A,B,C,D) [0 >= D] ==> evalrandom2dNodeBlockin(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dLeafBlockin(A,B,C,D) [D >= 1] ==> evalrandom2dNodeBlockin(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dLeafBlock1in(A,B,C,D) [D = 0] ==> evalrandom2dLeafBlockin(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dbb3in(A,B,C,D) [0 >= 1 + D] ==> evalrandom2dLeafBlockin(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dNewDefaultin(A,B,C,D) True ==> evalrandom2dbb3in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dbb10in(C,B,C,D) [D = 1] ==> evalrandom2dLeafBlock1in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dbb5in(A,B,C,D) [D >= 2] ==> evalrandom2dLeafBlock1in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dNewDefaultin(A,B,C,D) True ==> evalrandom2dbb5in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dbb10in(C,B,C,D) [2 >= D] ==> evalrandom2dNodeBlock7in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dLeafBlock3in(A,B,C,D) [D >= 3] ==> evalrandom2dNodeBlock7in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dLeafBlock5in(A,B,C,D) [D = 2] ==> evalrandom2dLeafBlock3in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dbb7in(A,B,C,D) [1 >= D] ==> evalrandom2dLeafBlock3in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dNewDefaultin(A,B,C,D) True ==> evalrandom2dbb7in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dbb10in(C,B,C,D) [D = 3] ==> evalrandom2dLeafBlock5in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dbb9in(A,B,C,D) [D >= 4] ==> evalrandom2dLeafBlock5in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dNewDefaultin(A,B,C,D) True ==> evalrandom2dbb9in(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dbb10in(C,B,C,D) True ==> evalrandom2dNewDefaultin(A,B,C,D) = B + -1*C >= B + -1*C = evalrandom2dbb10in(C,B,C,D) True ==> evalrandom2dreturnin(A,B,C,D) = -1*A + B >= -1*A + B = evalrandom2dstop(A,B,C,D) * Step 5: KnowledgePropagation 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] (B,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: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank 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] (B,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] (B,1) 5. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [0 >= 1 + E] (B,1) 6. evalrandom2dbbin(A,B,C,D) -> evalrandom2dbb10in(1 + A,B,C,D) [E >= 4] (B,1) 7. evalrandom2dbb2in(A,B,C,D) -> evalrandom2dNodeBlock9in(A,B,C,D) True (B,1) 8. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlockin(A,B,C,D) [1 >= D] (B,1) 9. evalrandom2dNodeBlock9in(A,B,C,D) -> evalrandom2dNodeBlock7in(A,B,C,D) [D >= 2] (B,1) 10. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlockin(A,B,C,D) [0 >= D] (B,1) 11. evalrandom2dNodeBlockin(A,B,C,D) -> evalrandom2dLeafBlock1in(A,B,C,D) [D >= 1] (B,1) 12. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dbb3in(A,B,C,D) [D = 0] (B,1) 13. evalrandom2dLeafBlockin(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [0 >= 1 + D] (B,1) 15. evalrandom2dbb3in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (B,1) 16. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dbb5in(A,B,C,D) [D = 1] (B,1) 18. evalrandom2dLeafBlock1in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 2] (B,1) 19. evalrandom2dbb5in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (B,1) 20. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock3in(A,B,C,D) [2 >= D] (B,1) 21. evalrandom2dNodeBlock7in(A,B,C,D) -> evalrandom2dLeafBlock5in(A,B,C,D) [D >= 3] (B,1) 22. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dbb7in(A,B,C,D) [D = 2] (B,1) 23. evalrandom2dLeafBlock3in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [1 >= D] (B,1) 25. evalrandom2dbb7in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (B,1) 26. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dbb9in(A,B,C,D) [D = 3] (B,1) 28. evalrandom2dLeafBlock5in(A,B,C,D) -> evalrandom2dNewDefaultin(A,B,C,D) [D >= 4] (B,1) 29. evalrandom2dbb9in(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (B,1) 30. evalrandom2dNewDefaultin(A,B,C,D) -> evalrandom2dbb10in(C,B,C,D) True (4*B,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: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(n^1))