YES(?,O(1)) * Step 1: UnsatPaths WORST_CASE(?,O(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) [39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 40] (?,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) True (?,1) 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) True (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) True (?,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 2: TrivialSCCs WORST_CASE(?,O(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) [39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 40] (?,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) True (?,1) 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) True (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) True (?,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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: PolyRank WORST_CASE(?,O(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) [39 >= A] (?,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 40] (1,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) True (?,1) 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) True (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) True (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) = 39 + -1*x1 p(evaleasy1bb2in) = 38 + -1*x1 p(evaleasy1bb3in) = 40 + -1*x1 p(evaleasy1bbin) = 39 + -1*x1 p(evaleasy1entryin) = 40 p(evaleasy1returnin) = 40 + -1*x1 p(evaleasy1start) = 40 p(evaleasy1stop) = 40 + -1*x1 Following rules are strictly oriented: [39 >= A] ==> evaleasy1bb3in(A,B) = 40 + -1*A > 39 + -1*A = evaleasy1bbin(A,B) Following rules are weakly oriented: True ==> evaleasy1start(A,B) = 40 >= 40 = evaleasy1entryin(A,B) True ==> evaleasy1entryin(A,B) = 40 >= 40 = evaleasy1bb3in(0,B) [A >= 40] ==> evaleasy1bb3in(A,B) = 40 + -1*A >= 40 + -1*A = evaleasy1returnin(A,B) [B = 0] ==> evaleasy1bbin(A,B) = 39 + -1*A >= 39 + -1*A = evaleasy1bb1in(A,B) [0 >= 1 + B] ==> evaleasy1bbin(A,B) = 39 + -1*A >= 38 + -1*A = evaleasy1bb2in(A,B) [B >= 1] ==> evaleasy1bbin(A,B) = 39 + -1*A >= 38 + -1*A = evaleasy1bb2in(A,B) True ==> evaleasy1bb1in(A,B) = 39 + -1*A >= 39 + -1*A = evaleasy1bb3in(1 + A,B) True ==> evaleasy1bb2in(A,B) = 38 + -1*A >= 38 + -1*A = evaleasy1bb3in(2 + A,B) True ==> evaleasy1returnin(A,B) = 40 + -1*A >= 40 + -1*A = evaleasy1stop(A,B) * Step 4: KnowledgePropagation WORST_CASE(?,O(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) [39 >= A] (40,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 40] (1,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [B = 0] (?,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [0 >= 1 + B] (?,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [B >= 1] (?,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) True (?,1) 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) True (?,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) True (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 5: PolyRank WORST_CASE(?,O(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) [39 >= A] (40,1) 3. evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 40] (1,1) 4. evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [B = 0] (40,1) 5. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [0 >= 1 + B] (40,1) 6. evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [B >= 1] (40,1) 7. evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) True (40,1) 8. evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) True (80,1) 9. evaleasy1returnin(A,B) -> evaleasy1stop(A,B) True (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(1))