YES * Step 1: TrivialSCCs YES + 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: Looptree YES + 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: Looptree + 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] | `- 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] YES