YES(?,POLY) * Step 1: TrivialSCCs WORST_CASE(?,POLY) + 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: AddSinks WORST_CASE(?,POLY) + 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: AddSinks + Details: () * Step 3: LooptreeTransformer WORST_CASE(?,POLY) + 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] 23. evalrandom2dreturnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 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) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3},2->{4,23},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},23->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] | `- p:[3,5,6,19,15,11,9,8,7,20,16,12,21,17,13,10,22,18,14] c: [22] | `- p:[3,5,6,19,15,11,9,8,7,20,16,12,21,17,13,10] c: [21] | `- p:[3,5,6,19,15,11,9,8,7,20,16,12] c: [20] | `- p:[3,5,6,19,15,11,9,8,7] c: [19] | `- p:[3,5,6] c: [6] | `- p:[3,5] c: [5] * Step 4: SizeAbstraction WORST_CASE(?,POLY) + 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] 23. evalrandom2dreturnin(A,B,C,D) -> exitus616(A,B,C,D) True (?,1) 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) ;(exitus616,4)} Flow Graph: [0->{1},1->{2,3},2->{4,23},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},23->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23] | `- p:[3,5,6,19,15,11,9,8,7,20,16,12,21,17,13,10,22,18,14] c: [22] | `- p:[3,5,6,19,15,11,9,8,7,20,16,12,21,17,13,10] c: [21] | `- p:[3,5,6,19,15,11,9,8,7,20,16,12] c: [20] | `- p:[3,5,6,19,15,11,9,8,7] c: [19] | `- p:[3,5,6] c: [6] | `- p:[3,5] c: [5]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 5: FlowAbstraction WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0,0.0.0,0.0.0.0,0.0.0.0.0,0.0.0.0.0.0,0.0.0.0.0.0.0] evalrandom2dstart ~> evalrandom2dentryin [A <= A, B <= B, C <= C, D <= D] evalrandom2dentryin ~> evalrandom2dbb10in [A <= 0*K, B <= B, C <= C, D <= D] evalrandom2dbb10in ~> evalrandom2dreturnin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb10in ~> evalrandom2dbbin [A <= A, B <= B, C <= C, D <= D] evalrandom2dreturnin ~> evalrandom2dstop [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb2in [A <= A, B <= B, C <= B, D <= 3*K] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlockin [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dLeafBlockin ~> evalrandom2dbb3in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb9in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dbb7in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dbb5in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dbb3in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dreturnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A + B + C] evalrandom2dbb10in ~> evalrandom2dbbin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbb9in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb2in [A <= A, B <= B, C <= B, D <= 3*K] evalrandom2dbb7in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb5in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb3in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlockin ~> evalrandom2dbb3in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlockin [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0 <= K + A + B + C] evalrandom2dbb10in ~> evalrandom2dbbin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbb9in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb2in [A <= A, B <= B, C <= B, D <= 3*K] evalrandom2dbb7in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb5in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0.0 <= K + A + B + C] evalrandom2dbb10in ~> evalrandom2dbbin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbb9in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb2in [A <= A, B <= B, C <= B, D <= 3*K] evalrandom2dbb7in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0.0.0.0 <= K + A + B + C] evalrandom2dbb10in ~> evalrandom2dbbin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbb9in ~> evalrandom2dbb10in [A <= C, B <= B, C <= C, D <= D] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [A <= A, B <= B, C <= C, D <= D] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb2in [A <= A, B <= B, C <= B, D <= 3*K] + Loop: [0.0.0.0.0.0 <= A + B] evalrandom2dbb10in ~> evalrandom2dbbin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] + Loop: [0.0.0.0.0.0.0 <= A + B] evalrandom2dbb10in ~> evalrandom2dbbin [A <= A, B <= B, C <= C, D <= D] evalrandom2dbbin ~> evalrandom2dbb10in [A <= B, B <= B, C <= C, D <= D] + Applied Processor: FlowAbstraction + Details: () * Step 6: LareProcessor WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0,0.0.0,0.0.0.0,0.0.0.0.0,0.0.0.0.0.0,0.0.0.0.0.0.0] evalrandom2dstart ~> evalrandom2dentryin [] evalrandom2dentryin ~> evalrandom2dbb10in [K ~=> A] evalrandom2dbb10in ~> evalrandom2dreturnin [] evalrandom2dbb10in ~> evalrandom2dbbin [] evalrandom2dreturnin ~> evalrandom2dstop [] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbbin ~> evalrandom2dbb2in [B ~=> C,K ~=> D] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlockin [] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [] evalrandom2dLeafBlockin ~> evalrandom2dbb3in [] evalrandom2dbb9in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dbb7in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dbb5in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dbb3in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dreturnin ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,C ~+> 0.0,K ~+> 0.0] evalrandom2dbb10in ~> evalrandom2dbbin [] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbb9in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [] evalrandom2dbbin ~> evalrandom2dbb2in [B ~=> C,K ~=> D] evalrandom2dbb7in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [] evalrandom2dbb5in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [] evalrandom2dbb3in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlockin ~> evalrandom2dbb3in [] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlockin [] + Loop: [A ~+> 0.0.0,B ~+> 0.0.0,C ~+> 0.0.0,K ~+> 0.0.0] evalrandom2dbb10in ~> evalrandom2dbbin [] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbb9in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [] evalrandom2dbbin ~> evalrandom2dbb2in [B ~=> C,K ~=> D] evalrandom2dbb7in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [] evalrandom2dbb5in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock1in ~> evalrandom2dbb5in [] evalrandom2dNodeBlockin ~> evalrandom2dLeafBlock1in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlockin [] + Loop: [A ~+> 0.0.0.0,B ~+> 0.0.0.0,C ~+> 0.0.0.0,K ~+> 0.0.0.0] evalrandom2dbb10in ~> evalrandom2dbbin [] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbb9in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [] evalrandom2dbbin ~> evalrandom2dbb2in [B ~=> C,K ~=> D] evalrandom2dbb7in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock3in ~> evalrandom2dbb7in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock3in [] + Loop: [A ~+> 0.0.0.0.0,B ~+> 0.0.0.0.0,C ~+> 0.0.0.0.0,K ~+> 0.0.0.0.0] evalrandom2dbb10in ~> evalrandom2dbbin [] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbb9in ~> evalrandom2dbb10in [C ~=> A] evalrandom2dLeafBlock5in ~> evalrandom2dbb9in [] evalrandom2dNodeBlock7in ~> evalrandom2dLeafBlock5in [] evalrandom2dNodeBlock9in ~> evalrandom2dNodeBlock7in [] evalrandom2dbb2in ~> evalrandom2dNodeBlock9in [] evalrandom2dbbin ~> evalrandom2dbb2in [B ~=> C,K ~=> D] + Loop: [A ~+> 0.0.0.0.0.0,B ~+> 0.0.0.0.0.0] evalrandom2dbb10in ~> evalrandom2dbbin [] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] + Loop: [A ~+> 0.0.0.0.0.0.0,B ~+> 0.0.0.0.0.0.0] evalrandom2dbb10in ~> evalrandom2dbbin [] evalrandom2dbbin ~> evalrandom2dbb10in [B ~=> A] + Applied Processor: LareProcessor + Details: evalrandom2dstart ~> exitus616 [B ~=> A ,B ~=> C ,C ~=> A ,K ~=> A ,K ~=> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> 0.0.0 ,C ~+> 0.0.0.0 ,C ~+> 0.0.0.0.0 ,C ~+> 0.0.0.0.0.0 ,C ~+> 0.0.0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,B ~*> 0.0.0 ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> 0.0.0 ,C ~*> 0.0.0.0 ,C ~*> 0.0.0.0.0 ,C ~*> tick ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> tick] evalrandom2dstart ~> evalrandom2dstop [B ~=> A ,B ~=> C ,C ~=> A ,K ~=> A ,K ~=> D ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> 0.0.0 ,C ~+> 0.0.0.0 ,C ~+> 0.0.0.0.0 ,C ~+> 0.0.0.0.0.0 ,C ~+> 0.0.0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> 0.0.0.0.0.0 ,K ~+> 0.0.0.0.0.0.0 ,K ~+> tick ,B ~*> 0.0.0 ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> 0.0.0 ,C ~*> 0.0.0.0 ,C ~*> 0.0.0.0.0 ,C ~*> tick ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> 0.0.0.0 ,K ~*> 0.0.0.0.0 ,K ~*> tick] + evalrandom2dbb10in> [B ~=> A ,B ~=> C ,C ~=> A ,K ~=> D ,A ~+> 0.0 ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> 0.0.0 ,C ~+> 0.0.0.0 ,C ~+> 0.0.0.0.0 ,C ~+> 0.0.0.0.0.0 ,C ~+> 0.0.0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.0.0 ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> 0.0.0 ,C ~*> 0.0.0.0 ,C ~*> 0.0.0.0.0 ,C ~*> tick ,K ~*> tick] + evalrandom2dbb10in> [B ~=> A ,B ~=> C ,C ~=> A ,K ~=> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> 0.0.0.0 ,C ~+> 0.0.0.0.0 ,C ~+> 0.0.0.0.0.0 ,C ~+> 0.0.0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> 0.0.0.0 ,C ~*> 0.0.0.0.0 ,C ~*> tick ,K ~*> tick] evalrandom2dNodeBlockin> [B ~=> A ,B ~=> C ,C ~=> A ,K ~=> D ,A ~+> 0.0.0 ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0 ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0.0 ,C ~+> 0.0.0.0 ,C ~+> 0.0.0.0.0 ,C ~+> 0.0.0.0.0.0 ,C ~+> 0.0.0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0 ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.0.0.0 ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> 0.0.0.0 ,C ~*> 0.0.0.0.0 ,C ~*> tick ,K ~*> tick] + evalrandom2dbb10in> [B ~=> A ,B ~=> C ,C ~=> A ,K ~=> D ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0.0.0 ,C ~+> 0.0.0.0.0 ,C ~+> 0.0.0.0.0.0 ,C ~+> 0.0.0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> 0.0.0.0.0 ,C ~*> tick ,K ~*> tick] evalrandom2dNodeBlock9in> [B ~=> A ,B ~=> C ,C ~=> A ,K ~=> D ,A ~+> 0.0.0.0 ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0 ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0.0.0 ,C ~+> 0.0.0.0.0 ,C ~+> 0.0.0.0.0.0 ,C ~+> 0.0.0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0 ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.0.0.0.0 ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> 0.0.0.0.0 ,C ~*> tick ,K ~*> tick] + evalrandom2dNodeBlock9in> [B ~=> A ,B ~=> C ,K ~=> D ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> tick ,K ~*> tick] evalrandom2dbb10in> [B ~=> A ,B ~=> C ,K ~=> D ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> tick ,K ~*> tick] evalrandom2dNodeBlock7in> [B ~=> A ,B ~=> C ,K ~=> D ,A ~+> 0.0.0.0.0 ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0.0 ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,C ~+> 0.0.0.0.0 ,C ~+> tick ,tick ~+> tick ,K ~+> 0.0.0.0.0 ,K ~+> tick ,A ~*> tick ,B ~*> 0.0.0.0.0.0 ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick ,C ~*> tick ,K ~*> tick] + evalrandom2dbbin> [B ~=> A ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,tick ~+> tick ,A ~*> tick ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick] evalrandom2dbb10in> [B ~=> A ,A ~+> 0.0.0.0.0.0 ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0.0.0 ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,tick ~+> tick ,A ~*> tick ,B ~*> 0.0.0.0.0.0.0 ,B ~*> tick] + evalrandom2dbbin> [B ~=> A ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,tick ~+> tick] evalrandom2dbb10in> [B ~=> A ,A ~+> 0.0.0.0.0.0.0 ,A ~+> tick ,B ~+> 0.0.0.0.0.0.0 ,B ~+> tick ,tick ~+> tick] YES(?,POLY)