YES * Step 1: FromIts YES + Considered Problem: Rules: 0. evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True (?,1) 2. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] (?,1) 3. evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] (?,1) 4. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] (?,1) 5. evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] (?,1) 6. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] (?,1) 7. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] (?,1) 8. evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 9. evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] (?,1) 10. evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] (?,1) 11. evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) [-1*A + B >= 0] (?,1) Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Flow Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: FromIts + Details: () * Step 2: Decompose YES + Considered Problem: Rules: evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) [-1*A + B >= 0] Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Rule Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | `- p:[2,10,4,9,6,5,7,8] c: [2,4,8,10] | `- p:[5,9,6,7] c: [5,6,7,9] * Step 3: CloseWith YES + Considered Problem: (Rules: evalNestedMultiplestart(A,B,C,D,E) -> evalNestedMultipleentryin(A,B,C,D,E) True evalNestedMultipleentryin(A,B,C,D,E) -> evalNestedMultiplebb5in(B,A,D,C,E) True evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,D) [A >= 1 + B] evalNestedMultiplebb5in(A,B,C,D,E) -> evalNestedMultiplereturnin(A,B,C,D,E) [B >= A] evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && E >= C] evalNestedMultiplebb2in(A,B,C,D,E) -> evalNestedMultiplebb3in(A,B,C,D,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0 && C >= 1 + E] evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && 0 >= 1 + F] evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb1in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0 && F >= 1] evalNestedMultiplebb3in(A,B,C,D,E) -> evalNestedMultiplebb4in(A,B,C,D,E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] evalNestedMultiplebb1in(A,B,C,D,E) -> evalNestedMultiplebb2in(A,B,C,D,1 + E) [-1 + C + -1*E >= 0 && -1*D + E >= 0 && -1 + C + -1*D >= 0 && -1 + A + -1*B >= 0] evalNestedMultiplebb4in(A,B,C,D,E) -> evalNestedMultiplebb5in(A,1 + B,C,E,E) [-1*D + E >= 0 && -1 + A + -1*B >= 0] evalNestedMultiplereturnin(A,B,C,D,E) -> evalNestedMultiplestop(A,B,C,D,E) [-1*A + B >= 0] Signature: {(evalNestedMultiplebb1in,5) ;(evalNestedMultiplebb2in,5) ;(evalNestedMultiplebb3in,5) ;(evalNestedMultiplebb4in,5) ;(evalNestedMultiplebb5in,5) ;(evalNestedMultipleentryin,5) ;(evalNestedMultiplereturnin,5) ;(evalNestedMultiplestart,5) ;(evalNestedMultiplestop,5)} Rule Graph: [0->{1},1->{2,3},2->{4,5},3->{11},4->{10},5->{6,7,8},6->{9},7->{9},8->{10},9->{4,5},10->{2,3},11->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11] | `- p:[2,10,4,9,6,5,7,8] c: [2,4,8,10] | `- p:[5,9,6,7] c: [5,6,7,9]) + Applied Processor: CloseWith True + Details: () YES