YES * Step 1: UnsatRules YES + Considered Problem: Rules: 0. evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True (1,1) 1. evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True (?,1) 2. evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] (?,1) 3. evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True (?,1) 5. evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] (?,1) 6. evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] (?,1) 7. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 8. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] (?,1) 9. evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True (?,1) 10. evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True (?,1) 11. evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 12. evalfbb3in(A,B,C,D,E,F) -> evalfbb4in(A,B,C,D,E,F) [0 >= 3] (?,1) 13. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 14. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [G >= 1] (?,1) 15. evalfbb4in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 16. evalfbb2in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,1 + E,-2 + F) True (?,1) 17. evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True (?,1) 18. evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True (?,1) 19. evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True (?,1) Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{19},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11,12},11->{17} ,12->{13,14,15},13->{16},14->{16},15->{17},16->{11,12},17->{5,6},18->{2,3},19->{}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [12] * Step 2: UnreachableRules YES + Considered Problem: Rules: 0. evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True (1,1) 1. evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True (?,1) 2. evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] (?,1) 3. evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True (?,1) 5. evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] (?,1) 6. evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] (?,1) 7. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 8. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] (?,1) 9. evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True (?,1) 10. evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True (?,1) 11. evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 13. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 14. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [G >= 1] (?,1) 15. evalfbb4in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 16. evalfbb2in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,1 + E,-2 + F) True (?,1) 17. evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True (?,1) 18. evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True (?,1) 19. evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True (?,1) Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{19},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11},11->{17} ,13->{16},14->{16},15->{17},16->{11},17->{5,6},18->{2,3},19->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [13,14,15,16] * Step 3: FromIts YES + Considered Problem: Rules: 0. evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True (1,1) 1. evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True (?,1) 2. evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] (?,1) 3. evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True (?,1) 5. evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] (?,1) 6. evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] (?,1) 7. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 8. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] (?,1) 9. evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True (?,1) 10. evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True (?,1) 11. evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 17. evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True (?,1) 18. evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True (?,1) 19. evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True (?,1) Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{19},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11},11->{17} ,17->{5,6},18->{2,3},19->{}] + Applied Processor: FromIts + Details: () * Step 4: Decompose YES + Considered Problem: Rules: evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{19},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11},11->{17} ,17->{5,6},18->{2,3},19->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,17,18,19] | `- p:[2,18,5,4,17,11,10,7,6,8,9] c: [2,4,5,9,18] | `- p:[6,17,11,10,7,8] c: [6,7,8,10,11,17] * Step 5: CloseWith YES + Considered Problem: (Rules: evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{19},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11},11->{17} ,17->{5,6},18->{2,3},19->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,17,18,19] | `- p:[2,18,5,4,17,11,10,7,6,8,9] c: [2,4,5,9,18] | `- p:[6,17,11,10,7,8] c: [6,7,8,10,11,17]) + Applied Processor: CloseWith True + Details: () YES