MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. evalrsdstart(A,B,C) -> evalrsdentryin(A,B,C) True (1,1) 1. evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (?,1) 2. evalrsdentryin(A,B,C) -> evalrsdreturnin(A,B,C) [0 >= 1 + A] (?,1) 3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) [A >= 0] (?,1) 4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [A >= 0 && C >= A] (?,1) 5. evalrsdbb4in(A,B,C) -> evalrsdreturnin(A,B,C) [A >= 0 && A >= 1 + C] (?,1) 6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && 0 >= 1 + D] (?,1) 7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && D >= 1] (?,1) 8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] (?,1) 9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] (?,1) 10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] (?,1) 11. evalrsdreturnin(A,B,C) -> evalrsdstop(A,B,C) True (?,1) Signature: {(evalrsdbb1in,3) ;(evalrsdbb2in,3) ;(evalrsdbb3in,3) ;(evalrsdbb4in,3) ;(evalrsdbbin,3) ;(evalrsdentryin,3) ;(evalrsdreturnin,3) ;(evalrsdstart,3) ;(evalrsdstop,3)} Flow Graph: [0->{1,2},1->{3},2->{11},3->{4,5},4->{6,7,8},5->{11},6->{9},7->{9},8->{10},9->{4,5},10->{4,5},11->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(3,5)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. evalrsdstart(A,B,C) -> evalrsdentryin(A,B,C) True (1,1) 1. evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] (?,1) 2. evalrsdentryin(A,B,C) -> evalrsdreturnin(A,B,C) [0 >= 1 + A] (?,1) 3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) [A >= 0] (?,1) 4. evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [A >= 0 && C >= A] (?,1) 5. evalrsdbb4in(A,B,C) -> evalrsdreturnin(A,B,C) [A >= 0 && A >= 1 + C] (?,1) 6. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && 0 >= 1 + D] (?,1) 7. evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && D >= 1] (?,1) 8. evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] (?,1) 9. evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] (?,1) 10. evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] (?,1) 11. evalrsdreturnin(A,B,C) -> evalrsdstop(A,B,C) True (?,1) Signature: {(evalrsdbb1in,3) ;(evalrsdbb2in,3) ;(evalrsdbb3in,3) ;(evalrsdbb4in,3) ;(evalrsdbbin,3) ;(evalrsdentryin,3) ;(evalrsdreturnin,3) ;(evalrsdstart,3) ;(evalrsdstop,3)} Flow Graph: [0->{1,2},1->{3},2->{11},3->{4},4->{6,7,8},5->{11},6->{9},7->{9},8->{10},9->{4,5},10->{4,5},11->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: evalrsdstart(A,B,C) -> evalrsdentryin(A,B,C) True evalrsdentryin(A,B,C) -> evalrsdbbin(A,B,C) [A >= 0] evalrsdentryin(A,B,C) -> evalrsdreturnin(A,B,C) [0 >= 1 + A] evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) [A >= 0] evalrsdbb4in(A,B,C) -> evalrsdbb1in(A,B,C) [A >= 0 && C >= A] evalrsdbb4in(A,B,C) -> evalrsdreturnin(A,B,C) [A >= 0 && A >= 1 + C] evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && 0 >= 1 + D] evalrsdbb1in(A,B,C) -> evalrsdbb2in(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && D >= 1] evalrsdbb1in(A,B,C) -> evalrsdbb3in(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb2in(A,B,C) -> evalrsdbb4in(A,B,-1 + C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb3in(A,B,C) -> evalrsdbb4in(A,-1 + B,-1 + B) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdreturnin(A,B,C) -> evalrsdstop(A,B,C) True Signature: {(evalrsdbb1in,3) ;(evalrsdbb2in,3) ;(evalrsdbb3in,3) ;(evalrsdbb4in,3) ;(evalrsdbbin,3) ;(evalrsdentryin,3) ;(evalrsdreturnin,3) ;(evalrsdstart,3) ;(evalrsdstop,3)} Rule Graph: [0->{1,2},1->{3},2->{11},3->{4},4->{6,7,8},5->{11},6->{9},7->{9},8->{10},9->{4,5},10->{4,5},11->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: evalrsdstart.0(A,B,C) -> evalrsdentryin.1(A,B,C) True evalrsdstart.0(A,B,C) -> evalrsdentryin.2(A,B,C) True evalrsdentryin.1(A,B,C) -> evalrsdbbin.3(A,B,C) [A >= 0] evalrsdentryin.2(A,B,C) -> evalrsdreturnin.11(A,B,C) [0 >= 1 + A] evalrsdbbin.3(A,B,C) -> evalrsdbb4in.4(A,2*A,2*A) [A >= 0] evalrsdbb4in.4(A,B,C) -> evalrsdbb1in.6(A,B,C) [A >= 0 && C >= A] evalrsdbb4in.4(A,B,C) -> evalrsdbb1in.7(A,B,C) [A >= 0 && C >= A] evalrsdbb4in.4(A,B,C) -> evalrsdbb1in.8(A,B,C) [A >= 0 && C >= A] evalrsdbb4in.5(A,B,C) -> evalrsdreturnin.11(A,B,C) [A >= 0 && A >= 1 + C] evalrsdbb1in.6(A,B,C) -> evalrsdbb2in.9(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && 0 >= 1 + D] evalrsdbb1in.7(A,B,C) -> evalrsdbb2in.9(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && D >= 1] evalrsdbb1in.8(A,B,C) -> evalrsdbb3in.10(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb2in.9(A,B,C) -> evalrsdbb4in.4(A,B,-1 + C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb2in.9(A,B,C) -> evalrsdbb4in.5(A,B,-1 + C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb3in.10(A,B,C) -> evalrsdbb4in.4(A,-1 + B,-1 + B) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb3in.10(A,B,C) -> evalrsdbb4in.5(A,-1 + B,-1 + B) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdreturnin.11(A,B,C) -> evalrsdstop.12(A,B,C) True Signature: {(evalrsdbb1in.6,3) ;(evalrsdbb1in.7,3) ;(evalrsdbb1in.8,3) ;(evalrsdbb2in.9,3) ;(evalrsdbb3in.10,3) ;(evalrsdbb4in.4,3) ;(evalrsdbb4in.5,3) ;(evalrsdbbin.3,3) ;(evalrsdentryin.1,3) ;(evalrsdentryin.2,3) ;(evalrsdreturnin.11,3) ;(evalrsdstart.0,3) ;(evalrsdstop.12,3)} Rule Graph: [0->{2},1->{3},2->{4},3->{16},4->{5,6,7},5->{9},6->{10},7->{11},8->{16},9->{12,13},10->{12,13},11->{14,15} ,12->{5,6,7},13->{8},14->{5,6,7},15->{8},16->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: evalrsdstart.0(A,B,C) -> evalrsdentryin.1(A,B,C) True evalrsdstart.0(A,B,C) -> evalrsdentryin.2(A,B,C) True evalrsdentryin.1(A,B,C) -> evalrsdbbin.3(A,B,C) [A >= 0] evalrsdentryin.2(A,B,C) -> evalrsdreturnin.11(A,B,C) [0 >= 1 + A] evalrsdbbin.3(A,B,C) -> evalrsdbb4in.4(A,2*A,2*A) [A >= 0] evalrsdbb4in.4(A,B,C) -> evalrsdbb1in.6(A,B,C) [A >= 0 && C >= A] evalrsdbb4in.4(A,B,C) -> evalrsdbb1in.7(A,B,C) [A >= 0 && C >= A] evalrsdbb4in.4(A,B,C) -> evalrsdbb1in.8(A,B,C) [A >= 0 && C >= A] evalrsdbb4in.5(A,B,C) -> evalrsdreturnin.11(A,B,C) [A >= 0 && A >= 1 + C] evalrsdbb1in.6(A,B,C) -> evalrsdbb2in.9(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && 0 >= 1 + D] evalrsdbb1in.7(A,B,C) -> evalrsdbb2in.9(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0 && D >= 1] evalrsdbb1in.8(A,B,C) -> evalrsdbb3in.10(A,B,C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb2in.9(A,B,C) -> evalrsdbb4in.4(A,B,-1 + C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb2in.9(A,B,C) -> evalrsdbb4in.5(A,B,-1 + C) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb3in.10(A,B,C) -> evalrsdbb4in.4(A,-1 + B,-1 + B) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdbb3in.10(A,B,C) -> evalrsdbb4in.5(A,-1 + B,-1 + B) [C >= 0 && A + C >= 0 && -1*A + C >= 0 && A >= 0] evalrsdreturnin.11(A,B,C) -> evalrsdstop.12(A,B,C) True evalrsdstop.12(A,B,C) -> exitus616(A,B,C) True evalrsdstop.12(A,B,C) -> exitus616(A,B,C) True evalrsdstop.12(A,B,C) -> exitus616(A,B,C) True Signature: {(evalrsdbb1in.6,3) ;(evalrsdbb1in.7,3) ;(evalrsdbb1in.8,3) ;(evalrsdbb2in.9,3) ;(evalrsdbb3in.10,3) ;(evalrsdbb4in.4,3) ;(evalrsdbb4in.5,3) ;(evalrsdbbin.3,3) ;(evalrsdentryin.1,3) ;(evalrsdentryin.2,3) ;(evalrsdreturnin.11,3) ;(evalrsdstart.0,3) ;(evalrsdstop.12,3) ;(exitus616,3)} Rule Graph: [0->{2},1->{3},2->{4},3->{16},4->{5,6,7},5->{9},6->{10},7->{11},8->{16},9->{12,13},10->{12,13},11->{14,15} ,12->{5,6,7},13->{8},14->{5,6,7},15->{8},16->{17,18,19}] + Applied Processor: Decompose Greedy + 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] | `- p:[5,12,9,10,6,14,11,7] c: [] MAYBE