YES * Step 1: FromIts YES + Considered Problem: Rules: 0. evalNestedMultipleDepstart(A,B,C,D,E) -> evalNestedMultipleDepentryin(A,B,C,D,E) True (1,1) 1. evalNestedMultipleDepentryin(A,B,C,D,E) -> evalNestedMultipleDepbb3in(0,B,C,D,E) True (?,1) 2. evalNestedMultipleDepbb3in(A,B,C,D,E) -> evalNestedMultipleDepbbin(A,B,C,D,E) [A >= 0 && B >= 1 + A] (?,1) 3. evalNestedMultipleDepbb3in(A,B,C,D,E) -> evalNestedMultipleDepreturnin(A,B,C,D,E) [A >= 0 && A >= B] (?,1) 4. evalNestedMultipleDepbbin(A,B,C,D,E) -> evalNestedMultipleDepbb2in(A,B,1 + A,0,E) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] (?,1) 5. evalNestedMultipleDepbb2in(A,B,C,D,E) -> evalNestedMultipleDepbb1in(A,B,C,D,E) [D >= 0 (?,1) && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && 1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && E >= 1 + D] 6. evalNestedMultipleDepbb2in(A,B,C,D,E) -> evalNestedMultipleDepbb3in(C,B,C,D,E) [D >= 0 (?,1) && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && 1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= E] 7. evalNestedMultipleDepbb1in(A,B,C,D,E) -> evalNestedMultipleDepbb2in(A,B,C,1 + D,E) [-1 + E >= 0 (?,1) && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && 1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] 8. evalNestedMultipleDepreturnin(A,B,C,D,E) -> evalNestedMultipleDepstop(A,B,C,D,E) [A + -1*B >= 0 && A >= 0] (?,1) Signature: {(evalNestedMultipleDepbb1in,5) ;(evalNestedMultipleDepbb2in,5) ;(evalNestedMultipleDepbb3in,5) ;(evalNestedMultipleDepbbin,5) ;(evalNestedMultipleDepentryin,5) ;(evalNestedMultipleDepreturnin,5) ;(evalNestedMultipleDepstart,5) ;(evalNestedMultipleDepstop,5)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{8},4->{5,6},5->{7},6->{2,3},7->{5,6},8->{}] + Applied Processor: FromIts + Details: () * Step 2: Decompose YES + Considered Problem: Rules: evalNestedMultipleDepstart(A,B,C,D,E) -> evalNestedMultipleDepentryin(A,B,C,D,E) True evalNestedMultipleDepentryin(A,B,C,D,E) -> evalNestedMultipleDepbb3in(0,B,C,D,E) True evalNestedMultipleDepbb3in(A,B,C,D,E) -> evalNestedMultipleDepbbin(A,B,C,D,E) [A >= 0 && B >= 1 + A] evalNestedMultipleDepbb3in(A,B,C,D,E) -> evalNestedMultipleDepreturnin(A,B,C,D,E) [A >= 0 && A >= B] evalNestedMultipleDepbbin(A,B,C,D,E) -> evalNestedMultipleDepbb2in(A,B,1 + A,0,E) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalNestedMultipleDepbb2in(A,B,C,D,E) -> evalNestedMultipleDepbb1in(A,B,C,D,E) [D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && 1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && E >= 1 + D] evalNestedMultipleDepbb2in(A,B,C,D,E) -> evalNestedMultipleDepbb3in(C,B,C,D,E) [D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && 1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= E] evalNestedMultipleDepbb1in(A,B,C,D,E) -> evalNestedMultipleDepbb2in(A,B,C,1 + D,E) [-1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && 1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalNestedMultipleDepreturnin(A,B,C,D,E) -> evalNestedMultipleDepstop(A,B,C,D,E) [A + -1*B >= 0 && A >= 0] Signature: {(evalNestedMultipleDepbb1in,5) ;(evalNestedMultipleDepbb2in,5) ;(evalNestedMultipleDepbb3in,5) ;(evalNestedMultipleDepbbin,5) ;(evalNestedMultipleDepentryin,5) ;(evalNestedMultipleDepreturnin,5) ;(evalNestedMultipleDepstart,5) ;(evalNestedMultipleDepstop,5)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{8},4->{5,6},5->{7},6->{2,3},7->{5,6},8->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8] | `- p:[2,6,4,7,5] c: [2,4,6] | `- p:[5,7] c: [5,7] * Step 3: CloseWith YES + Considered Problem: (Rules: evalNestedMultipleDepstart(A,B,C,D,E) -> evalNestedMultipleDepentryin(A,B,C,D,E) True evalNestedMultipleDepentryin(A,B,C,D,E) -> evalNestedMultipleDepbb3in(0,B,C,D,E) True evalNestedMultipleDepbb3in(A,B,C,D,E) -> evalNestedMultipleDepbbin(A,B,C,D,E) [A >= 0 && B >= 1 + A] evalNestedMultipleDepbb3in(A,B,C,D,E) -> evalNestedMultipleDepreturnin(A,B,C,D,E) [A >= 0 && A >= B] evalNestedMultipleDepbbin(A,B,C,D,E) -> evalNestedMultipleDepbb2in(A,B,1 + A,0,E) [-1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalNestedMultipleDepbb2in(A,B,C,D,E) -> evalNestedMultipleDepbb1in(A,B,C,D,E) [D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && 1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && E >= 1 + D] evalNestedMultipleDepbb2in(A,B,C,D,E) -> evalNestedMultipleDepbb3in(C,B,C,D,E) [D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && 1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0 && D >= E] evalNestedMultipleDepbb1in(A,B,C,D,E) -> evalNestedMultipleDepbb2in(A,B,C,1 + D,E) [-1 + E >= 0 && -1 + D + E >= 0 && -1 + -1*D + E >= 0 && -2 + C + E >= 0 && -2 + B + E >= 0 && -1 + A + E >= 0 && D >= 0 && -1 + C + D >= 0 && -1 + B + D >= 0 && A + D >= 0 && B + -1*C >= 0 && 1 + A + -1*C >= 0 && -1 + C >= 0 && -2 + B + C >= 0 && -1 + A + C >= 0 && -1 + -1*A + C >= 0 && -1 + B >= 0 && -1 + A + B >= 0 && -1 + -1*A + B >= 0 && A >= 0] evalNestedMultipleDepreturnin(A,B,C,D,E) -> evalNestedMultipleDepstop(A,B,C,D,E) [A + -1*B >= 0 && A >= 0] Signature: {(evalNestedMultipleDepbb1in,5) ;(evalNestedMultipleDepbb2in,5) ;(evalNestedMultipleDepbb3in,5) ;(evalNestedMultipleDepbbin,5) ;(evalNestedMultipleDepentryin,5) ;(evalNestedMultipleDepreturnin,5) ;(evalNestedMultipleDepstart,5) ;(evalNestedMultipleDepstop,5)} Rule Graph: [0->{1},1->{2,3},2->{4},3->{8},4->{5,6},5->{7},6->{2,3},7->{5,6},8->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8] | `- p:[2,6,4,7,5] c: [2,4,6] | `- p:[5,7] c: [5,7]) + Applied Processor: CloseWith True + Details: () YES