NO * Step 1: TrivialSCCs NO + 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: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatPaths NO + 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,1) 2. evalrsdentryin(A,B,C) -> evalrsdreturnin(A,B,C) [0 >= 1 + A] (1,1) 3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) [A >= 0] (1,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,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,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 3: Looptree NO + 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,1) 2. evalrsdentryin(A,B,C) -> evalrsdreturnin(A,B,C) [0 >= 1 + A] (1,1) 3. evalrsdbbin(A,B,C) -> evalrsdbb4in(A,2*A,2*A) [A >= 0] (1,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,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,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: Looptree + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | `- p:[4,9,6,7,10,8] c: [] NO