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