NO * Step 1: UnsatPaths NO + 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) [B^3 >= 0 && 0 >= B^3 && 0 >= 1 + A] (?,1) 3. evalfbb7in(A,B,C,D) -> evalfbb5in(A,B,0,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && E >= 1 + A] (?,1) 4. evalfbb7in(A,B,C,D) -> evalfbb5in(A,B,0,D) [0 >= 1 + B^3 && 0 >= E && E >= 1 + A && 2*E >= B^3 && 1 + B^3 >= 2*E] (?,1) 5. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [B^3 >= 0 && 0 >= B^3 && A >= 0] (?,1) 6. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && A >= E] (?,1) 7. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [0 >= 1 + B^3 && 0 >= E && A >= E && 2*E >= B^3 && 1 + B^3 >= 2*E] (?,1) 8. evalfbb5in(A,B,C,D) -> evalfbb3in(A,B,C,0) [B >= 1 + C] (?,1) 9. evalfbb5in(A,B,C,D) -> evalfbb6in(A,B,C,D) [C >= B] (?,1) 10. evalfbb3in(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= 1 + D] (?,1) 11. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [D >= C] (?,1) 12. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,1 + D) True (?,1) 13. evalfbb4in(A,B,C,D) -> evalfbb5in(A,B,1 + C,D) True (?,1) 14. evalfbb6in(A,B,C,D) -> evalfbb7in(1 + A,B,C,D) True (?,1) 15. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,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,6,7},2->{8,9},3->{8,9},4->{8,9},5->{15},6->{15},7->{15},8->{10,11},9->{14},10->{12} ,11->{13},12->{10,11},13->{8,9},14->{2,3,4,5,6,7},15->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,2),(1,4)] * Step 2: FromIts NO + 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) [B^3 >= 0 && 0 >= B^3 && 0 >= 1 + A] (?,1) 3. evalfbb7in(A,B,C,D) -> evalfbb5in(A,B,0,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && E >= 1 + A] (?,1) 4. evalfbb7in(A,B,C,D) -> evalfbb5in(A,B,0,D) [0 >= 1 + B^3 && 0 >= E && E >= 1 + A && 2*E >= B^3 && 1 + B^3 >= 2*E] (?,1) 5. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [B^3 >= 0 && 0 >= B^3 && A >= 0] (?,1) 6. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && A >= E] (?,1) 7. evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [0 >= 1 + B^3 && 0 >= E && A >= E && 2*E >= B^3 && 1 + B^3 >= 2*E] (?,1) 8. evalfbb5in(A,B,C,D) -> evalfbb3in(A,B,C,0) [B >= 1 + C] (?,1) 9. evalfbb5in(A,B,C,D) -> evalfbb6in(A,B,C,D) [C >= B] (?,1) 10. evalfbb3in(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= 1 + D] (?,1) 11. evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [D >= C] (?,1) 12. evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,1 + D) True (?,1) 13. evalfbb4in(A,B,C,D) -> evalfbb5in(A,B,1 + C,D) True (?,1) 14. evalfbb6in(A,B,C,D) -> evalfbb7in(1 + A,B,C,D) True (?,1) 15. evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True (?,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->{3,5,6,7},2->{8,9},3->{8,9},4->{8,9},5->{15},6->{15},7->{15},8->{10,11},9->{14},10->{12} ,11->{13},12->{10,11},13->{8,9},14->{2,3,4,5,6,7},15->{}] + Applied Processor: FromIts + Details: () * Step 3: CloseWith NO + Considered Problem: Rules: evalfstart(A,B,C,D) -> evalfentryin(A,B,C,D) True evalfentryin(A,B,C,D) -> evalfbb7in(0,B,C,D) True evalfbb7in(A,B,C,D) -> evalfbb5in(A,B,0,D) [B^3 >= 0 && 0 >= B^3 && 0 >= 1 + A] evalfbb7in(A,B,C,D) -> evalfbb5in(A,B,0,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && E >= 1 + A] evalfbb7in(A,B,C,D) -> evalfbb5in(A,B,0,D) [0 >= 1 + B^3 && 0 >= E && E >= 1 + A && 2*E >= B^3 && 1 + B^3 >= 2*E] evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [B^3 >= 0 && 0 >= B^3 && A >= 0] evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && A >= E] evalfbb7in(A,B,C,D) -> evalfreturnin(A,B,C,D) [0 >= 1 + B^3 && 0 >= E && A >= E && 2*E >= B^3 && 1 + B^3 >= 2*E] evalfbb5in(A,B,C,D) -> evalfbb3in(A,B,C,0) [B >= 1 + C] evalfbb5in(A,B,C,D) -> evalfbb6in(A,B,C,D) [C >= B] evalfbb3in(A,B,C,D) -> evalfbb2in(A,B,C,D) [C >= 1 + D] evalfbb3in(A,B,C,D) -> evalfbb4in(A,B,C,D) [D >= C] evalfbb2in(A,B,C,D) -> evalfbb3in(A,B,C,1 + D) True evalfbb4in(A,B,C,D) -> evalfbb5in(A,B,1 + C,D) True evalfbb6in(A,B,C,D) -> evalfbb7in(1 + A,B,C,D) True evalfreturnin(A,B,C,D) -> evalfstop(A,B,C,D) True Signature: {(evalfbb2in,4) ;(evalfbb3in,4) ;(evalfbb4in,4) ;(evalfbb5in,4) ;(evalfbb6in,4) ;(evalfbb7in,4) ;(evalfentryin,4) ;(evalfreturnin,4) ;(evalfstart,4) ;(evalfstop,4)} Rule Graph: [0->{1},1->{3,5,6,7},2->{8,9},3->{8,9},4->{8,9},5->{15},6->{15},7->{15},8->{10,11},9->{14},10->{12} ,11->{13},12->{10,11},13->{8,9},14->{2,3,4,5,6,7},15->{}] + Applied Processor: CloseWith False + Details: () NO