YES(?,O(n^1)) * Step 1: TrivialSCCs WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (?,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (?,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (?,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (?,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (1,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (1,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (?,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (1,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2,3},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3)] * Step 3: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (1,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (1,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (?,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (1,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evaleasy1bb1in) = 78 + -1*x1 p(evaleasy1bb2in) = 79 + -1*x1 p(evaleasy1bb3in) = 79 + -1*x1 p(evaleasy1bbin) = 79 + -1*x1 p(evaleasy1entryin) = 79 p(evaleasy1returnin) = 79 + -1*x1 p(evaleasy1start) = 79 p(evaleasy1stop) = 79 + -1*x1 Following rules are strictly oriented: [39 + -1*A >= 0 && A >= 0] ==> evaleasy1bb2in(A,B) = 79 + -1*A > 77 + -1*A = evaleasy1bb3in(2 + A,B) Following rules are weakly oriented: True ==> evaleasy1start(A,B) = 79 >= 79 = evaleasy1entryin(A,B) True ==> evaleasy1entryin(A,B) = 79 >= 79 = evaleasy1bb3in(0,B) [A >= 0 && 39 >= A] ==> evaleasy1bb3in(A,B) = 79 + -1*A >= 79 + -1*A = evaleasy1bbin(A,B) [A >= 0 && A >= 40] ==> evaleasy1bb3in(A,B) = 79 + -1*A >= 79 + -1*A = evaleasy1returnin(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] ==> evaleasy1bbin(A,B) = 79 + -1*A >= 78 + -1*A = evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] ==> evaleasy1bbin(A,B) = 79 + -1*A >= 79 + -1*A = evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] ==> evaleasy1bbin(A,B) = 79 + -1*A >= 79 + -1*A = evaleasy1bb2in(A,B) [-1*B >= 0 ==> && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb1in(A,B) = 78 + -1*A >= 78 + -1*A = evaleasy1bb3in(1 + A,B) [-40 + A >= 0] ==> evaleasy1returnin(A,B) = 79 + -1*A >= 79 + -1*A = evaleasy1stop(A,B) * Step 4: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (1,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (1,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (?,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (79,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (1,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: We apply a polynomial interpretation of shape linear: p(evaleasy1bb1in) = 40 + -1*x1 + x2 p(evaleasy1bb2in) = 40 + -1*x1 + x2 p(evaleasy1bb3in) = 40 + -1*x1 + x2 p(evaleasy1bbin) = 40 + -1*x1 + x2 p(evaleasy1entryin) = 40 + x2 p(evaleasy1returnin) = 40 + -1*x1 + x2 p(evaleasy1start) = 40 + x2 p(evaleasy1stop) = 40 + -1*x1 + x2 Following rules are strictly oriented: [-1*B >= 0 ==> && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] evaleasy1bb1in(A,B) = 40 + -1*A + B > 39 + -1*A + B = evaleasy1bb3in(1 + A,B) Following rules are weakly oriented: True ==> evaleasy1start(A,B) = 40 + B >= 40 + B = evaleasy1entryin(A,B) True ==> evaleasy1entryin(A,B) = 40 + B >= 40 + B = evaleasy1bb3in(0,B) [A >= 0 && 39 >= A] ==> evaleasy1bb3in(A,B) = 40 + -1*A + B >= 40 + -1*A + B = evaleasy1bbin(A,B) [A >= 0 && A >= 40] ==> evaleasy1bb3in(A,B) = 40 + -1*A + B >= 40 + -1*A + B = evaleasy1returnin(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] ==> evaleasy1bbin(A,B) = 40 + -1*A + B >= 40 + -1*A + B = evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] ==> evaleasy1bbin(A,B) = 40 + -1*A + B >= 40 + -1*A + B = evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] ==> evaleasy1bbin(A,B) = 40 + -1*A + B >= 40 + -1*A + B = evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0] ==> evaleasy1bb2in(A,B) = 40 + -1*A + B >= 38 + -1*A + B = evaleasy1bb3in(2 + A,B) [-40 + A >= 0] ==> evaleasy1returnin(A,B) = 40 + -1*A + B >= 40 + -1*A + B = evaleasy1stop(A,B) * Step 5: KnowledgePropagation WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (1,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (1,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (40 + B,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (79,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (1,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: KnowledgePropagation + Details: We propagate bounds from predecessors. * Step 6: PolyRank WORST_CASE(?,O(n^1)) + Considered Problem: Rules: 0. evaleasy1start(A,B) -> evaleasy1entryin(A,B) True (1,1) 1. evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True (1,1) 2. evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [A >= 0 && 39 >= A] (120 + B,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 0 && A >= 40] (1,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [39 + -1*A >= 0 && A >= 0 && B = 0] (120 + B,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && 0 >= 1 + B] (120 + B,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [39 + -1*A >= 0 && A >= 0 && B >= 1] (120 + B,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) [-1*B >= 0 (40 + B,1) && A + -1*B >= 0 && 39 + -1*A + -1*B >= 0 && B >= 0 && A + B >= 0 && 39 + -1*A + B >= 0 && 39 + -1*A >= 0 && A >= 0] 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) [39 + -1*A >= 0 && A >= 0] (79,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) [-40 + A >= 0] (1,1) Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Flow Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] + Applied Processor: PolyRank {useFarkas = True, withSizebounds = [], shape = Linear} + Details: The problem is already solved. YES(?,O(n^1))