MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. evalcyclicstart(A,B,C) -> evalcyclicentryin(A,B,C) True (1,1) 1. evalcyclicentryin(A,B,C) -> evalcyclicbb3in(A,B,1 + A) [A >= 0 && B >= 1 + A] (?,1) 2. evalcyclicbb3in(A,B,C) -> evalcyclicreturnin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = A] (?,1) 3. evalcyclicbb3in(A,B,C) -> evalcyclicbb4in(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 1 + C] (?,1) 4. evalcyclicbb3in(A,B,C) -> evalcyclicbb4in(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + A] (?,1) 5. evalcyclicbb4in(A,B,C) -> evalcyclicbbin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + D] (?,1) 6. evalcyclicbb4in(A,B,C) -> evalcyclicbbin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1] (?,1) 7. evalcyclicbb4in(A,B,C) -> evalcyclicreturnin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) 8. evalcyclicbbin(A,B,C) -> evalcyclicbb3in(A,B,1 + C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && B >= C] (?,1) 9. evalcyclicbbin(A,B,C) -> evalcyclicbb3in(A,B,0) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + B] (?,1) 10. evalcyclicreturnin(A,B,C) -> evalcyclicstop(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) Signature: {(evalcyclicbb3in,3) ;(evalcyclicbb4in,3) ;(evalcyclicbbin,3) ;(evalcyclicentryin,3) ;(evalcyclicreturnin,3) ;(evalcyclicstart,3) ;(evalcyclicstop,3)} Flow Graph: [0->{1},1->{2,3,4},2->{10},3->{5,6,7},4->{5,6,7},5->{8,9},6->{8,9},7->{10},8->{2,3,4},9->{2,3,4},10->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2),(1,3),(9,4)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. evalcyclicstart(A,B,C) -> evalcyclicentryin(A,B,C) True (1,1) 1. evalcyclicentryin(A,B,C) -> evalcyclicbb3in(A,B,1 + A) [A >= 0 && B >= 1 + A] (?,1) 2. evalcyclicbb3in(A,B,C) -> evalcyclicreturnin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = A] (?,1) 3. evalcyclicbb3in(A,B,C) -> evalcyclicbb4in(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 1 + C] (?,1) 4. evalcyclicbb3in(A,B,C) -> evalcyclicbb4in(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + A] (?,1) 5. evalcyclicbb4in(A,B,C) -> evalcyclicbbin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + D] (?,1) 6. evalcyclicbb4in(A,B,C) -> evalcyclicbbin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1] (?,1) 7. evalcyclicbb4in(A,B,C) -> evalcyclicreturnin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) 8. evalcyclicbbin(A,B,C) -> evalcyclicbb3in(A,B,1 + C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && B >= C] (?,1) 9. evalcyclicbbin(A,B,C) -> evalcyclicbb3in(A,B,0) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + B] (?,1) 10. evalcyclicreturnin(A,B,C) -> evalcyclicstop(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) Signature: {(evalcyclicbb3in,3) ;(evalcyclicbb4in,3) ;(evalcyclicbbin,3) ;(evalcyclicentryin,3) ;(evalcyclicreturnin,3) ;(evalcyclicstart,3) ;(evalcyclicstop,3)} Flow Graph: [0->{1},1->{4},2->{10},3->{5,6,7},4->{5,6,7},5->{8,9},6->{8,9},7->{10},8->{2,3,4},9->{2,3},10->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: evalcyclicstart(A,B,C) -> evalcyclicentryin(A,B,C) True evalcyclicentryin(A,B,C) -> evalcyclicbb3in(A,B,1 + A) [A >= 0 && B >= 1 + A] evalcyclicbb3in(A,B,C) -> evalcyclicreturnin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = A] evalcyclicbb3in(A,B,C) -> evalcyclicbb4in(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 1 + C] evalcyclicbb3in(A,B,C) -> evalcyclicbb4in(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + A] evalcyclicbb4in(A,B,C) -> evalcyclicbbin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + D] evalcyclicbb4in(A,B,C) -> evalcyclicbbin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1] evalcyclicbb4in(A,B,C) -> evalcyclicreturnin(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalcyclicbbin(A,B,C) -> evalcyclicbb3in(A,B,1 + C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && B >= C] evalcyclicbbin(A,B,C) -> evalcyclicbb3in(A,B,0) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + B] evalcyclicreturnin(A,B,C) -> evalcyclicstop(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] Signature: {(evalcyclicbb3in,3) ;(evalcyclicbb4in,3) ;(evalcyclicbbin,3) ;(evalcyclicentryin,3) ;(evalcyclicreturnin,3) ;(evalcyclicstart,3) ;(evalcyclicstop,3)} Rule Graph: [0->{1},1->{4},2->{10},3->{5,6,7},4->{5,6,7},5->{8,9},6->{8,9},7->{10},8->{2,3,4},9->{2,3},10->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: evalcyclicstart.0(A,B,C) -> evalcyclicentryin.1(A,B,C) True evalcyclicentryin.1(A,B,C) -> evalcyclicbb3in.4(A,B,1 + A) [A >= 0 && B >= 1 + A] evalcyclicbb3in.2(A,B,C) -> evalcyclicreturnin.10(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = A] evalcyclicbb3in.3(A,B,C) -> evalcyclicbb4in.5(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 1 + C] evalcyclicbb3in.3(A,B,C) -> evalcyclicbb4in.6(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 1 + C] evalcyclicbb3in.3(A,B,C) -> evalcyclicbb4in.7(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 1 + C] evalcyclicbb3in.4(A,B,C) -> evalcyclicbb4in.5(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + A] evalcyclicbb3in.4(A,B,C) -> evalcyclicbb4in.6(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + A] evalcyclicbb3in.4(A,B,C) -> evalcyclicbb4in.7(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + A] evalcyclicbb4in.5(A,B,C) -> evalcyclicbbin.8(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + D] evalcyclicbb4in.5(A,B,C) -> evalcyclicbbin.9(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + D] evalcyclicbb4in.6(A,B,C) -> evalcyclicbbin.8(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1] evalcyclicbb4in.6(A,B,C) -> evalcyclicbbin.9(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1] evalcyclicbb4in.7(A,B,C) -> evalcyclicreturnin.10(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalcyclicbbin.8(A,B,C) -> evalcyclicbb3in.2(A,B,1 + C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && B >= C] evalcyclicbbin.8(A,B,C) -> evalcyclicbb3in.3(A,B,1 + C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && B >= C] evalcyclicbbin.8(A,B,C) -> evalcyclicbb3in.4(A,B,1 + C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && B >= C] evalcyclicbbin.9(A,B,C) -> evalcyclicbb3in.2(A,B,0) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + B] evalcyclicbbin.9(A,B,C) -> evalcyclicbb3in.3(A,B,0) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + B] evalcyclicreturnin.10(A,B,C) -> evalcyclicstop.11(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] Signature: {(evalcyclicbb3in.2,3) ;(evalcyclicbb3in.3,3) ;(evalcyclicbb3in.4,3) ;(evalcyclicbb4in.5,3) ;(evalcyclicbb4in.6,3) ;(evalcyclicbb4in.7,3) ;(evalcyclicbbin.8,3) ;(evalcyclicbbin.9,3) ;(evalcyclicentryin.1,3) ;(evalcyclicreturnin.10,3) ;(evalcyclicstart.0,3) ;(evalcyclicstop.11,3)} Rule Graph: [0->{1},1->{6,7,8},2->{19},3->{9,10},4->{11,12},5->{13},6->{9,10},7->{11,12},8->{13},9->{14,15,16},10->{17 ,18},11->{14,15,16},12->{17,18},13->{19},14->{2},15->{3,4,5},16->{6,7,8},17->{2},18->{3,4,5},19->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: evalcyclicstart.0(A,B,C) -> evalcyclicentryin.1(A,B,C) True evalcyclicentryin.1(A,B,C) -> evalcyclicbb3in.4(A,B,1 + A) [A >= 0 && B >= 1 + A] evalcyclicbb3in.2(A,B,C) -> evalcyclicreturnin.10(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C = A] evalcyclicbb3in.3(A,B,C) -> evalcyclicbb4in.5(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 1 + C] evalcyclicbb3in.3(A,B,C) -> evalcyclicbb4in.6(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 1 + C] evalcyclicbb3in.3(A,B,C) -> evalcyclicbb4in.7(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && A >= 1 + C] evalcyclicbb3in.4(A,B,C) -> evalcyclicbb4in.5(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + A] evalcyclicbb3in.4(A,B,C) -> evalcyclicbb4in.6(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + A] evalcyclicbb3in.4(A,B,C) -> evalcyclicbb4in.7(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + A] evalcyclicbb4in.5(A,B,C) -> evalcyclicbbin.8(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + D] evalcyclicbb4in.5(A,B,C) -> evalcyclicbbin.9(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && 0 >= 1 + D] evalcyclicbb4in.6(A,B,C) -> evalcyclicbbin.8(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1] evalcyclicbb4in.6(A,B,C) -> evalcyclicbbin.9(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= 1] evalcyclicbb4in.7(A,B,C) -> evalcyclicreturnin.10(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalcyclicbbin.8(A,B,C) -> evalcyclicbb3in.2(A,B,1 + C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && B >= C] evalcyclicbbin.8(A,B,C) -> evalcyclicbb3in.3(A,B,1 + C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && B >= C] evalcyclicbbin.8(A,B,C) -> evalcyclicbb3in.4(A,B,1 + C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && B >= C] evalcyclicbbin.9(A,B,C) -> evalcyclicbb3in.2(A,B,0) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + B] evalcyclicbbin.9(A,B,C) -> evalcyclicbb3in.3(A,B,0) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && C >= 1 + B] evalcyclicreturnin.10(A,B,C) -> evalcyclicstop.11(A,B,C) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalcyclicstop.11(A,B,C) -> exitus616(A,B,C) True evalcyclicstop.11(A,B,C) -> exitus616(A,B,C) True evalcyclicstop.11(A,B,C) -> exitus616(A,B,C) True evalcyclicstop.11(A,B,C) -> exitus616(A,B,C) True Signature: {(evalcyclicbb3in.2,3) ;(evalcyclicbb3in.3,3) ;(evalcyclicbb3in.4,3) ;(evalcyclicbb4in.5,3) ;(evalcyclicbb4in.6,3) ;(evalcyclicbb4in.7,3) ;(evalcyclicbbin.8,3) ;(evalcyclicbbin.9,3) ;(evalcyclicentryin.1,3) ;(evalcyclicreturnin.10,3) ;(evalcyclicstart.0,3) ;(evalcyclicstop.11,3) ;(exitus616,3)} Rule Graph: [0->{1},1->{6,7,8},2->{19},3->{9,10},4->{11,12},5->{13},6->{9,10},7->{11,12},8->{13},9->{14,15,16},10->{17 ,18},11->{14,15,16},12->{17,18},13->{19},14->{2},15->{3,4,5},16->{6,7,8},17->{2},18->{3,4,5},19->{20,21,22 ,23}] + 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,20,21,22,23] | `- p:[6,16,9,3,15,11,4,18,10,12,7] c: [] MAYBE