MAYBE * Step 1: UnsatPaths 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) [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 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) [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: Unfold MAYBE + 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: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: evalfstart.0(A,B,C,D) -> evalfentryin.1(A,B,C,D) True evalfentryin.1(A,B,C,D) -> evalfbb7in.3(0,B,C,D) True evalfentryin.1(A,B,C,D) -> evalfbb7in.5(0,B,C,D) True evalfentryin.1(A,B,C,D) -> evalfbb7in.6(0,B,C,D) True evalfentryin.1(A,B,C,D) -> evalfbb7in.7(0,B,C,D) True evalfbb7in.2(A,B,C,D) -> evalfbb5in.8(A,B,0,D) [B^3 >= 0 && 0 >= B^3 && 0 >= 1 + A] evalfbb7in.2(A,B,C,D) -> evalfbb5in.9(A,B,0,D) [B^3 >= 0 && 0 >= B^3 && 0 >= 1 + A] evalfbb7in.3(A,B,C,D) -> evalfbb5in.8(A,B,0,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && E >= 1 + A] evalfbb7in.3(A,B,C,D) -> evalfbb5in.9(A,B,0,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && E >= 1 + A] evalfbb7in.4(A,B,C,D) -> evalfbb5in.8(A,B,0,D) [0 >= 1 + B^3 && 0 >= E && E >= 1 + A && 2*E >= B^3 && 1 + B^3 >= 2*E] evalfbb7in.4(A,B,C,D) -> evalfbb5in.9(A,B,0,D) [0 >= 1 + B^3 && 0 >= E && E >= 1 + A && 2*E >= B^3 && 1 + B^3 >= 2*E] evalfbb7in.5(A,B,C,D) -> evalfreturnin.15(A,B,C,D) [B^3 >= 0 && 0 >= B^3 && A >= 0] evalfbb7in.6(A,B,C,D) -> evalfreturnin.15(A,B,C,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && A >= E] evalfbb7in.7(A,B,C,D) -> evalfreturnin.15(A,B,C,D) [0 >= 1 + B^3 && 0 >= E && A >= E && 2*E >= B^3 && 1 + B^3 >= 2*E] evalfbb5in.8(A,B,C,D) -> evalfbb3in.10(A,B,C,0) [B >= 1 + C] evalfbb5in.8(A,B,C,D) -> evalfbb3in.11(A,B,C,0) [B >= 1 + C] evalfbb5in.9(A,B,C,D) -> evalfbb6in.14(A,B,C,D) [C >= B] evalfbb3in.10(A,B,C,D) -> evalfbb2in.12(A,B,C,D) [C >= 1 + D] evalfbb3in.11(A,B,C,D) -> evalfbb4in.13(A,B,C,D) [D >= C] evalfbb2in.12(A,B,C,D) -> evalfbb3in.10(A,B,C,1 + D) True evalfbb2in.12(A,B,C,D) -> evalfbb3in.11(A,B,C,1 + D) True evalfbb4in.13(A,B,C,D) -> evalfbb5in.8(A,B,1 + C,D) True evalfbb4in.13(A,B,C,D) -> evalfbb5in.9(A,B,1 + C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.2(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.3(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.4(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.5(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.6(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.7(1 + A,B,C,D) True evalfreturnin.15(A,B,C,D) -> evalfstop.16(A,B,C,D) True Signature: {(evalfbb2in.12,4) ;(evalfbb3in.10,4) ;(evalfbb3in.11,4) ;(evalfbb4in.13,4) ;(evalfbb5in.8,4) ;(evalfbb5in.9,4) ;(evalfbb6in.14,4) ;(evalfbb7in.2,4) ;(evalfbb7in.3,4) ;(evalfbb7in.4,4) ;(evalfbb7in.5,4) ;(evalfbb7in.6,4) ;(evalfbb7in.7,4) ;(evalfentryin.1,4) ;(evalfreturnin.15,4) ;(evalfstart.0,4) ;(evalfstop.16,4)} Rule Graph: [0->{1,2,3,4},1->{7,8},2->{11},3->{12},4->{13},5->{14,15},6->{16},7->{14,15},8->{16},9->{14,15},10->{16} ,11->{29},12->{29},13->{29},14->{17},15->{18},16->{23,24,25,26,27,28},17->{19,20},18->{21,22},19->{17} ,20->{18},21->{14,15},22->{16},23->{5,6},24->{7,8},25->{9,10},26->{11},27->{12},28->{13},29->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: evalfstart.0(A,B,C,D) -> evalfentryin.1(A,B,C,D) True evalfentryin.1(A,B,C,D) -> evalfbb7in.3(0,B,C,D) True evalfentryin.1(A,B,C,D) -> evalfbb7in.5(0,B,C,D) True evalfentryin.1(A,B,C,D) -> evalfbb7in.6(0,B,C,D) True evalfentryin.1(A,B,C,D) -> evalfbb7in.7(0,B,C,D) True evalfbb7in.2(A,B,C,D) -> evalfbb5in.8(A,B,0,D) [B^3 >= 0 && 0 >= B^3 && 0 >= 1 + A] evalfbb7in.2(A,B,C,D) -> evalfbb5in.9(A,B,0,D) [B^3 >= 0 && 0 >= B^3 && 0 >= 1 + A] evalfbb7in.3(A,B,C,D) -> evalfbb5in.8(A,B,0,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && E >= 1 + A] evalfbb7in.3(A,B,C,D) -> evalfbb5in.9(A,B,0,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && E >= 1 + A] evalfbb7in.4(A,B,C,D) -> evalfbb5in.8(A,B,0,D) [0 >= 1 + B^3 && 0 >= E && E >= 1 + A && 2*E >= B^3 && 1 + B^3 >= 2*E] evalfbb7in.4(A,B,C,D) -> evalfbb5in.9(A,B,0,D) [0 >= 1 + B^3 && 0 >= E && E >= 1 + A && 2*E >= B^3 && 1 + B^3 >= 2*E] evalfbb7in.5(A,B,C,D) -> evalfreturnin.15(A,B,C,D) [B^3 >= 0 && 0 >= B^3 && A >= 0] evalfbb7in.6(A,B,C,D) -> evalfreturnin.15(A,B,C,D) [B^3 >= 1 && E >= 0 && B^3 >= 2*E && 1 + 2*E >= B^3 && A >= E] evalfbb7in.7(A,B,C,D) -> evalfreturnin.15(A,B,C,D) [0 >= 1 + B^3 && 0 >= E && A >= E && 2*E >= B^3 && 1 + B^3 >= 2*E] evalfbb5in.8(A,B,C,D) -> evalfbb3in.10(A,B,C,0) [B >= 1 + C] evalfbb5in.8(A,B,C,D) -> evalfbb3in.11(A,B,C,0) [B >= 1 + C] evalfbb5in.9(A,B,C,D) -> evalfbb6in.14(A,B,C,D) [C >= B] evalfbb3in.10(A,B,C,D) -> evalfbb2in.12(A,B,C,D) [C >= 1 + D] evalfbb3in.11(A,B,C,D) -> evalfbb4in.13(A,B,C,D) [D >= C] evalfbb2in.12(A,B,C,D) -> evalfbb3in.10(A,B,C,1 + D) True evalfbb2in.12(A,B,C,D) -> evalfbb3in.11(A,B,C,1 + D) True evalfbb4in.13(A,B,C,D) -> evalfbb5in.8(A,B,1 + C,D) True evalfbb4in.13(A,B,C,D) -> evalfbb5in.9(A,B,1 + C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.2(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.3(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.4(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.5(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.6(1 + A,B,C,D) True evalfbb6in.14(A,B,C,D) -> evalfbb7in.7(1 + A,B,C,D) True evalfreturnin.15(A,B,C,D) -> evalfstop.16(A,B,C,D) True evalfstop.16(A,B,C,D) -> exitus616(A,B,C,D) True evalfstop.16(A,B,C,D) -> exitus616(A,B,C,D) True evalfstop.16(A,B,C,D) -> exitus616(A,B,C,D) True evalfstop.16(A,B,C,D) -> exitus616(A,B,C,D) True evalfstop.16(A,B,C,D) -> exitus616(A,B,C,D) True evalfstop.16(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(evalfbb2in.12,4) ;(evalfbb3in.10,4) ;(evalfbb3in.11,4) ;(evalfbb4in.13,4) ;(evalfbb5in.8,4) ;(evalfbb5in.9,4) ;(evalfbb6in.14,4) ;(evalfbb7in.2,4) ;(evalfbb7in.3,4) ;(evalfbb7in.4,4) ;(evalfbb7in.5,4) ;(evalfbb7in.6,4) ;(evalfbb7in.7,4) ;(evalfentryin.1,4) ;(evalfreturnin.15,4) ;(evalfstart.0,4) ;(evalfstop.16,4) ;(exitus616,4)} Rule Graph: [0->{1,2,3,4},1->{7,8},2->{11},3->{12},4->{13},5->{14,15},6->{16},7->{14,15},8->{16},9->{14,15},10->{16} ,11->{29},12->{29},13->{29},14->{17},15->{18},16->{23,24,25,26,27,28},17->{19,20},18->{21,22},19->{17} ,20->{18},21->{14,15},22->{16},23->{5,6},24->{7,8},25->{9,10},26->{11},27->{12},28->{13},29->{30,31,32,33,34 ,35}] + 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,24,25,26,27,28,29,30,31,32,33,34,35] | `- p:[7,24,16,6,23,8,10,25,22,18,15,5,9,21,20,17,14,19] c: [5,6,9,10,23,25] | `- p:[7,24,16,8,22,18,15,21,20,17,14,19] c: [] MAYBE