MAYBE * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1) 1. evalfentryin(A,B,C,D) -> evalfbb7in(0,B,C,D) True (?,1) 2. evalfbb7in(A,B,C,D) -> evalfbb5in(A,B,0,D) [A >= 0 && B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && E >= 1 + A] (?,1) 3. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [A >= 0 && B^3 >= 0 && 0 >= B^3] (?,1) 4. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [A >= 0 && B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && A >= E] (?,1) 5. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [A >= 0 && 0 >= 1 + B^3 && 0 >= E && A >= E && 2*E >= B^3 && 1 + B^3 >= 2*E] (?,1) 6. evalfbb5in(A,B,C,D) -> evalfbb3in(A,B,C,0) [C >= 0 && A + C >= 0 && A >= 0 && B >= 1 + C] (?,1) 7. evalfbb5in(A,B,C,D) -> evalfbb6in(A,B,C,D) [C >= 0 && A + C >= 0 && A >= 0 && C >= B] (?,1) 8. evalfbb3in(A,B,C,D) -> evalfbb2in(A,B,C,D) [C + -1*D >= 0 (?,1) && -1 + B + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C >= 1 + D] 9. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C + -1*D >= 0 (?,1) && -1 + B + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && D >= C] 10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,1 + D) [-1 + C + -1*D >= 0 (?,1) && -2 + B + -1*D >= 0 && D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && A + D >= 0 && -1 + B + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -1 + A + C >= 0 && -2 + B >= 0 && -2 + A + B >= 0 && A >= 0] 11. evalfbb4in(A,B,C,D) -> evalfbb5in(A,B,1 + C,D) [C + -1*D >= 0 (?,1) && -1 + B + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0] 12. evalfbb6in(A,B,C,D) -> evalfbb7in(1 + A,B,C,D) [C >= 0 && -1*B + C >= 0 && A + C >= 0 && A >= 0] (?,1) 13. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) [A >= 0] (?,1) Signature: {(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbb6in,4) ;(evalfbb7in,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4)} Flow Graph: [0->{1},1->{2,3,4,5},2->{6,7},3->{13},4->{13},5->{13},6->{8,9},7->{12},8->{10},9->{11},10->{8,9},11->{6,7} ,12->{2,3,4,5},13->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: Failure MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True (1,1) 1. evalfentryin(A,B,C,D) -> evalfbb7in(0,B,C,D) True (1,1) 2. evalfbb7in(A,B,C,D) -> evalfbb5in(A,B,0,D) [A >= 0 && B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && E >= 1 + A] (?,1) 3. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [A >= 0 && B^3 >= 0 && 0 >= B^3] (1,1) 4. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [A >= 0 && B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && A >= E] (1,1) 5. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [A >= 0 && 0 >= 1 + B^3 && 0 >= E && A >= E && 2*E >= B^3 && 1 + B^3 >= 2*E] (1,1) 6. evalfbb5in(A,B,C,D) -> evalfbb3in(A,B,C,0) [C >= 0 && A + C >= 0 && A >= 0 && B >= 1 + C] (?,1) 7. evalfbb5in(A,B,C,D) -> evalfbb6in(A,B,C,D) [C >= 0 && A + C >= 0 && A >= 0 && C >= B] (?,1) 8. evalfbb3in(A,B,C,D) -> evalfbb2in(A,B,C,D) [C + -1*D >= 0 (?,1) && -1 + B + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && C >= 1 + D] 9. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [C + -1*D >= 0 (?,1) && -1 + B + -1*D >= 0 && D >= 0 && C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0 && D >= C] 10. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,1 + D) [-1 + C + -1*D >= 0 (?,1) && -2 + B + -1*D >= 0 && D >= 0 && -1 + C + D >= 0 && -2 + B + D >= 0 && A + D >= 0 && -1 + B + -1*C >= 0 && -1 + C >= 0 && -3 + B + C >= 0 && -1 + A + C >= 0 && -2 + B >= 0 && -2 + A + B >= 0 && A >= 0] 11. evalfbb4in(A,B,C,D) -> evalfbb5in(A,B,1 + C,D) [C + -1*D >= 0 (?,1) && -1 + B + -1*D >= 0 && D >= 0 && C + D >= 0 && -1*C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && -1 + B + -1*C >= 0 && C >= 0 && -1 + B + C >= 0 && A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && A >= 0] 12. evalfbb6in(A,B,C,D) -> evalfbb7in(1 + A,B,C,D) [C >= 0 && -1*B + C >= 0 && A + C >= 0 && A >= 0] (?,1) 13. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) [A >= 0] (1,1) Signature: {(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbb6in,4) ;(evalfbb7in,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4)} Flow Graph: [0->{1},1->{2,3,4,5},2->{6,7},3->{13},4->{13},5->{13},6->{8,9},7->{12},8->{10},9->{11},10->{8,9},11->{6,7} ,12->{2,3,4,5},13->{}] + Applied Processor: Failing "Open problems left." + Details: Open problems left. MAYBE