MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalEx5start(A,B,C,D,E) -> evalEx5entryin(A,B,C,D,E) True (1,1) 1. evalEx5entryin(A,B,C,D,E) -> evalEx5bb6in(0,A,C,D,E) True (?,1) 2. evalEx5bb6in(A,B,C,D,E) -> evalEx5bb3in(A,B,0,B,E) [A >= 0 && B >= 1 + A] (?,1) 3. evalEx5bb6in(A,B,C,D,E) -> evalEx5returnin(A,B,C,D,E) [A >= 0 && A >= B] (?,1) 4. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] 5. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] 6. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb4in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 7. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] 8. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] 9. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb3in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 10. evalEx5bb2in(A,B,C,D,E) -> evalEx5bb3in(A,B,1,E,E) [-1 + D + -1*E >= 0 (?,1) && -1 + B + -1*E >= 0 && 1 + -1*D + E >= 0 && B + -1*D >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 11. evalEx5bb4in(A,B,C,D,E) -> evalEx5bb6in(1 + A,D,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = 0] 12. evalEx5bb4in(A,B,C,D,E) -> evalEx5bb6in(A,D,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] 13. evalEx5returnin(A,B,C,D,E) -> evalEx5stop(A,B,C,D,E) [A + -1*B >= 0 && A >= 0] (?,1) Signature: {(evalEx5bb1in,5) ;(evalEx5bb2in,5) ;(evalEx5bb3in,5) ;(evalEx5bb4in,5) ;(evalEx5bb6in,5) ;(evalEx5entryin,5) ;(evalEx5returnin,5) ;(evalEx5start,5) ;(evalEx5stop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{13},4->{7,8,9},5->{7,8,9},6->{11,12},7->{10},8->{10},9->{4,5,6},10->{4,5 ,6},11->{2,3},12->{2,3},13->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: PolyRank MAYBE + Considered Problem: Rules: 0. evalEx5start(A,B,C,D,E) -> evalEx5entryin(A,B,C,D,E) True (1,1) 1. evalEx5entryin(A,B,C,D,E) -> evalEx5bb6in(0,A,C,D,E) True (1,1) 2. evalEx5bb6in(A,B,C,D,E) -> evalEx5bb3in(A,B,0,B,E) [A >= 0 && B >= 1 + A] (?,1) 3. evalEx5bb6in(A,B,C,D,E) -> evalEx5returnin(A,B,C,D,E) [A >= 0 && A >= B] (1,1) 4. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] 5. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] 6. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb4in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 7. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] 8. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] 9. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb3in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 10. evalEx5bb2in(A,B,C,D,E) -> evalEx5bb3in(A,B,1,E,E) [-1 + D + -1*E >= 0 (?,1) && -1 + B + -1*E >= 0 && 1 + -1*D + E >= 0 && B + -1*D >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 11. evalEx5bb4in(A,B,C,D,E) -> evalEx5bb6in(1 + A,D,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = 0] 12. evalEx5bb4in(A,B,C,D,E) -> evalEx5bb6in(A,D,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] 13. evalEx5returnin(A,B,C,D,E) -> evalEx5stop(A,B,C,D,E) [A + -1*B >= 0 && A >= 0] (1,1) Signature: {(evalEx5bb1in,5) ;(evalEx5bb2in,5) ;(evalEx5bb3in,5) ;(evalEx5bb4in,5) ;(evalEx5bb6in,5) ;(evalEx5entryin,5) ;(evalEx5returnin,5) ;(evalEx5start,5) ;(evalEx5stop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{13},4->{7,8,9},5->{7,8,9},6->{11,12},7->{10},8->{10},9->{4,5,6},10->{4,5 ,6},11->{2,3},12->{2,3},13->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalEx5bb1in) = -1*x1 + x2 p(evalEx5bb2in) = -1*x1 + x2 p(evalEx5bb3in) = -1*x1 + x2 p(evalEx5bb4in) = -1*x1 + x2 p(evalEx5bb6in) = -1*x1 + x2 p(evalEx5entryin) = x1 p(evalEx5returnin) = -1*x1 + x2 p(evalEx5start) = x1 p(evalEx5stop) = -1*x1 + x2 Following rules are strictly oriented: [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = 0] evalEx5bb4in(A,B,C,D,E) = -1*A + B > -1 + -1*A + D = evalEx5bb6in(1 + A,D,C,D,E) Following rules are weakly oriented: True ==> evalEx5start(A,B,C,D,E) = A >= A = evalEx5entryin(A,B,C,D,E) True ==> evalEx5entryin(A,B,C,D,E) = A >= A = evalEx5bb6in(0,A,C,D,E) [A >= 0 && B >= 1 + A] ==> evalEx5bb6in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5bb3in(A,B,0,B,E) [A >= 0 && A >= B] ==> evalEx5bb6in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5returnin(A,B,C,D,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] evalEx5bb3in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] evalEx5bb3in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalEx5bb3in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5bb4in(A,B,C,D,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] evalEx5bb1in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] evalEx5bb1in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalEx5bb1in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5bb3in(A,B,C,D,E) [-1 + D + -1*E >= 0 ==> && -1 + B + -1*E >= 0 && 1 + -1*D + E >= 0 && B + -1*D >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalEx5bb2in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5bb3in(A,B,1,E,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] evalEx5bb4in(A,B,C,D,E) = -1*A + B >= -1*A + D = evalEx5bb6in(A,D,C,D,E) [A + -1*B >= 0 && A >= 0] ==> evalEx5returnin(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5stop(A,B,C,D,E) * Step 3: PolyRank MAYBE + Considered Problem: Rules: 0. evalEx5start(A,B,C,D,E) -> evalEx5entryin(A,B,C,D,E) True (1,1) 1. evalEx5entryin(A,B,C,D,E) -> evalEx5bb6in(0,A,C,D,E) True (1,1) 2. evalEx5bb6in(A,B,C,D,E) -> evalEx5bb3in(A,B,0,B,E) [A >= 0 && B >= 1 + A] (?,1) 3. evalEx5bb6in(A,B,C,D,E) -> evalEx5returnin(A,B,C,D,E) [A >= 0 && A >= B] (1,1) 4. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] 5. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] 6. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb4in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 7. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] 8. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] 9. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb3in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 10. evalEx5bb2in(A,B,C,D,E) -> evalEx5bb3in(A,B,1,E,E) [-1 + D + -1*E >= 0 (?,1) && -1 + B + -1*E >= 0 && 1 + -1*D + E >= 0 && B + -1*D >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 11. evalEx5bb4in(A,B,C,D,E) -> evalEx5bb6in(1 + A,D,C,D,E) [B + -1*D >= 0 (A,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = 0] 12. evalEx5bb4in(A,B,C,D,E) -> evalEx5bb6in(A,D,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] 13. evalEx5returnin(A,B,C,D,E) -> evalEx5stop(A,B,C,D,E) [A + -1*B >= 0 && A >= 0] (1,1) Signature: {(evalEx5bb1in,5) ;(evalEx5bb2in,5) ;(evalEx5bb3in,5) ;(evalEx5bb4in,5) ;(evalEx5bb6in,5) ;(evalEx5entryin,5) ;(evalEx5returnin,5) ;(evalEx5start,5) ;(evalEx5stop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{13},4->{7,8,9},5->{7,8,9},6->{11,12},7->{10},8->{10},9->{4,5,6},10->{4,5 ,6},11->{2,3},12->{2,3},13->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evalEx5bb1in) = -1 + -1*x1 + x3 + x4 p(evalEx5bb2in) = -1*x1 + x3 + x5 p(evalEx5bb3in) = -1 + -1*x1 + x3 + x4 p(evalEx5bb4in) = -1 + -1*x1 + x3 + x4 p(evalEx5bb6in) = -1*x1 + x2 p(evalEx5entryin) = x1 p(evalEx5returnin) = -1*x1 + x2 p(evalEx5start) = x1 p(evalEx5stop) = -1*x1 + x2 Following rules are strictly oriented: [A >= 0 && B >= 1 + A] ==> evalEx5bb6in(A,B,C,D,E) = -1*A + B > -1 + -1*A + B = evalEx5bb3in(A,B,0,B,E) Following rules are weakly oriented: True ==> evalEx5start(A,B,C,D,E) = A >= A = evalEx5entryin(A,B,C,D,E) True ==> evalEx5entryin(A,B,C,D,E) = A >= A = evalEx5bb6in(0,A,C,D,E) [A >= 0 && A >= B] ==> evalEx5bb6in(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5returnin(A,B,C,D,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] evalEx5bb3in(A,B,C,D,E) = -1 + -1*A + C + D >= -1 + -1*A + C + D = evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] evalEx5bb3in(A,B,C,D,E) = -1 + -1*A + C + D >= -1 + -1*A + C + D = evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalEx5bb3in(A,B,C,D,E) = -1 + -1*A + C + D >= -1 + -1*A + C + D = evalEx5bb4in(A,B,C,D,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] evalEx5bb1in(A,B,C,D,E) = -1 + -1*A + C + D >= -1 + -1*A + C + D = evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] evalEx5bb1in(A,B,C,D,E) = -1 + -1*A + C + D >= -1 + -1*A + C + D = evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalEx5bb1in(A,B,C,D,E) = -1 + -1*A + C + D >= -1 + -1*A + C + D = evalEx5bb3in(A,B,C,D,E) [-1 + D + -1*E >= 0 ==> && -1 + B + -1*E >= 0 && 1 + -1*D + E >= 0 && B + -1*D >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalEx5bb2in(A,B,C,D,E) = -1*A + C + E >= -1*A + E = evalEx5bb3in(A,B,1,E,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = 0] evalEx5bb4in(A,B,C,D,E) = -1 + -1*A + C + D >= -1 + -1*A + D = evalEx5bb6in(1 + A,D,C,D,E) [B + -1*D >= 0 ==> && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] evalEx5bb4in(A,B,C,D,E) = -1 + -1*A + C + D >= -1*A + D = evalEx5bb6in(A,D,C,D,E) [A + -1*B >= 0 && A >= 0] ==> evalEx5returnin(A,B,C,D,E) = -1*A + B >= -1*A + B = evalEx5stop(A,B,C,D,E) * Step 4: Failure MAYBE + Considered Problem: Rules: 0. evalEx5start(A,B,C,D,E) -> evalEx5entryin(A,B,C,D,E) True (1,1) 1. evalEx5entryin(A,B,C,D,E) -> evalEx5bb6in(0,A,C,D,E) True (1,1) 2. evalEx5bb6in(A,B,C,D,E) -> evalEx5bb3in(A,B,0,B,E) [A >= 0 && B >= 1 + A] (A,1) 3. evalEx5bb6in(A,B,C,D,E) -> evalEx5returnin(A,B,C,D,E) [A >= 0 && A >= B] (1,1) 4. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] 5. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb1in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] 6. evalEx5bb3in(A,B,C,D,E) -> evalEx5bb4in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 7. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + F] 8. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb2in(A,B,C,D,-1 + D) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && F >= 1] 9. evalEx5bb1in(A,B,C,D,E) -> evalEx5bb3in(A,B,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 10. evalEx5bb2in(A,B,C,D,E) -> evalEx5bb3in(A,B,1,E,E) [-1 + D + -1*E >= 0 (?,1) && -1 + B + -1*E >= 0 && 1 + -1*D + E >= 0 && B + -1*D >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 11. evalEx5bb4in(A,B,C,D,E) -> evalEx5bb6in(1 + A,D,C,D,E) [B + -1*D >= 0 (A,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = 0] 12. evalEx5bb4in(A,B,C,D,E) -> evalEx5bb6in(A,D,C,D,E) [B + -1*D >= 0 (?,1) && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1] 13. evalEx5returnin(A,B,C,D,E) -> evalEx5stop(A,B,C,D,E) [A + -1*B >= 0 && A >= 0] (1,1) Signature: {(evalEx5bb1in,5) ;(evalEx5bb2in,5) ;(evalEx5bb3in,5) ;(evalEx5bb4in,5) ;(evalEx5bb6in,5) ;(evalEx5entryin,5) ;(evalEx5returnin,5) ;(evalEx5start,5) ;(evalEx5stop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{13},4->{7,8,9},5->{7,8,9},6->{11,12},7->{10},8->{10},9->{4,5,6},10->{4,5 ,6},11->{2,3},12->{2,3},13->{}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE