YES * Step 1: UnsatPaths YES + 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: FromIts YES + 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: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: evaleasy1start(A,B) -> evaleasy1entryin(A,B) True evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [39 >= A] evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 40] evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [B = 0] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [0 >= 1 + B] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [B >= 1] evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) True evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) True evaleasy1returnin(A,B) -> evaleasy1stop(A,B) True Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Rule 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: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | `- p:[2,7,4,8,5,6] c: [2,4,5,6,7,8] * Step 4: CloseWith YES + Considered Problem: (Rules: evaleasy1start(A,B) -> evaleasy1entryin(A,B) True evaleasy1entryin(A,B) -> evaleasy1bb3in(0,B) True evaleasy1bb3in(A,B) -> evaleasy1bbin(A,B) [39 >= A] evaleasy1bb3in(A,B) -> evaleasy1returnin(A,B) [A >= 40] evaleasy1bbin(A,B) -> evaleasy1bb1in(A,B) [B = 0] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [0 >= 1 + B] evaleasy1bbin(A,B) -> evaleasy1bb2in(A,B) [B >= 1] evaleasy1bb1in(A,B) -> evaleasy1bb3in(1 + A,B) True evaleasy1bb2in(A,B) -> evaleasy1bb3in(2 + A,B) True evaleasy1returnin(A,B) -> evaleasy1stop(A,B) True Signature: {(evaleasy1bb1in,2) ;(evaleasy1bb2in,2) ;(evaleasy1bb3in,2) ;(evaleasy1bbin,2) ;(evaleasy1entryin,2) ;(evaleasy1returnin,2) ;(evaleasy1start,2) ;(evaleasy1stop,2)} Rule Graph: [0->{1},1->{2},2->{4,5,6},3->{9},4->{7},5->{8},6->{8},7->{2,3},8->{2,3},9->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | `- p:[2,7,4,8,5,6] c: [2,4,5,6,7,8]) + Applied Processor: CloseWith True + Details: () YES